Remove the Records_rel module

[Halbaroth]

The record theory is just sugar syntax, there is no reason to build a dummy relation theory for it.

Rename the relation modules in Relations by their original name for sake of self documentation.

[bclement-ocp]

The record theory is just sugar syntax, there is no reason to build a dummy relation theory for it.

Fine by me. We probably want to remove Records from the Util.theories_extensions field in this case to avoid it being silently ignored if it is used (it was raising an error before, so it is fine to remove it).

Rename the relation modules in Relations by their original name for sake of self documentation.

I disagree with this part of the PR. The goal of the Relations module is to be a "blind" wrapper/adapter from a set of N Sig_rel.RELATION signatures to a single one (conceptually it is an inlined functor Make(Rel1)..(Rel7)). It doesn't care about the wrapped relations, it just calls any function from the signature on all of them and combines the results. In this sense, the module is already self-documenting by using generic names (r1, Rel1, etc.), and using the original module names obfuscates this.

(The situation is a bit different with the Shostak modules where we did a similar change because the code does dispatch to different theories depending on types)

[Halbaroth]

I disagree:

• using the original name doesn't obfuscate the code in my opinion.
• the order in which we combine the relations could be important and could be different in functions of Relations.

[bclement-ocp]

* using the original name doesn't obfuscate the code in my opinion.

The implementation has an implicit order on the relations based on their name: we treat Rel1, then Rel2, etc. Calling them IntervalCalculus and Bitv_rel hides this information: it was plainly obvious, and now one needs to read all the code to know this information (sure; you can put a comment; doesn't change the point that the code is less clear). It is somewhat implied by the field names, but while writing new code, it is plainly obvious that r1 should be of type Rel1.t, while knowing that r1 should be of type IntervalCalculus.t requires looking at the type definition. In both cases, relevant information is harder to find.

The stated goal of this PR is to remove the Records_rel module (which we agree on), not to rewrite the Relations module; can we reduce the scope to do just that and discuss Relations changes elsewhere?

* the order in which we combine the relations could be important and could be different in functions of `Relations`.

Currently, the order used is always the same. In this case, this fact is better conveyed by the implied order over Rel1 etc. so that the order is both expressed in a single place (rather than having to look at each function independently) and so that the existence of a global order on the relations is clear (even though AFAICT there is no theoretical reason for the current order, it is just the order in which theories were added historically). It is also much easier to change the order if needed/it becomes important: just swap out Rel1 = IntervalCalculus; Rel2 = Bitv_rel with Rel1 = Bitv_rel; Rel2 = IntervalCalculus in a single place rather than go through all the code.

It is possible to imagine scenarios where we would want different functions of Relations to use different orders on the modules (although we should avoid this if at all possible, it reeks of code smell) but I don't think we should change an existing design for the possibility of more complexity in the future that we are not even sure we will need.

[Halbaroth]

The stated goal of this PR is to remove the Records_rel module (which we agree on), not to rewrite the Relations module; can we reduce the scope to do just that and discuss Relations changes elsewhere?

I gave up. I can't contribute to this project anymore.