[WIP] Attempt to replace a bunch of ugly code by generated code from ppx_compare

[Halbaroth]

This PR is an attempt to replace the current comparisons functions in the module Symbol and the comparison of triggers in Expr by generated ones with ppx_compare.

The current code looks like this

  let compare_operators op1 op2 =
  Util.compare_algebraic op1 op2
    (function
      | Access h1, Access h2 | Constr h1, Constr h2 -> Hstring.compare h1 h2
      | Destruct (h1, b1), Destruct(h2, b2) ->
        let c = Stdlib.compare b1 b2 in
        if c <> 0 then c else Hstring.compare h1 h2
      | _ , (Plus | Minus | Mult | Div | Modulo
            | Concat | Extract | Get | Set | Fixed | Float | Reach
            | Access _ | Record | Sqrt_real | Abs_int | Abs_real
            | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default
            | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int
            | Integer_log2 | Pow | Integer_round
            | Constr _ | Destruct _ | Tite) -> assert false
    )

where compare_algebraic is polymorphic comparison function for ADT defined in the module Util like this (their are other comparison functions using the same template in Symbol)

let [@inline always] compare_algebraic s1 s2 f_same_constrs_with_args =
  let r1 = Obj.repr s1 in
  let r2 = Obj.repr s2 in
  match Obj.is_int r1, Obj.is_int r2 with
  | true, true -> Stdlib.compare s1 s2 (* both constructors without args *)
  | true, false -> -1
  | false, true -> 1
  | false, false ->
    let cmp_tags = Obj.tag r1 - Obj.tag r2 in
    if cmp_tags <> 0 then cmp_tags else f_same_constrs_with_args (s1, s2)

The function compare_algebraic compares ADT values based on their memory representation and calls f_same_constrs_with_args to manage the case where s1 and s2 are the same constructor to compare their payload.

This code has many issues:

• It is ugly as hell. The assert false to exclude the case of two different contructors or a constructor without payload in f_same_with_args is terrible design.
• It depends on the memory representation of values. Even if this stable right now, it could change in the future.
• It is not even an efficient way to write an ADT comparison function. According to Vincent and Nathanaëlle, the function Obj.tag costs a lot because it is a C call.

Pros:

• We don't need to maintain these functions anymore.
• ppx_compare is stable and does not need memory representation.
• It is more efficient than the current implementation. I don't think this will be a substantial improvement nevertheless.

Cons:

• We depend on a ppx and a change in it could change the behavior of AE.

[Gbury]

For the last cons, there is a way to make it so that the code generated by ppx_deriving is added to the source file and promoted by dune, see https://ocaml-ppx.github.io/ppxlib/ppxlib/manual.html#@@deriving_inline . I think that's what we want, if only to be able to more easily check what the generated code looks like.

[Halbaroth]

It is amazing!

[CLAassistant]

All committers have signed the CLA.