[sledge] Use ppx_compare to define equal functions

Summary:
With ppx_compare 0.12, `[@deriving equal]` now generates efficient
`equal` functions.

Reviewed By: mbouaziz

Differential Revision: D14297866

fbshipit-source-id: a303090cb

sledge/src/control.ml

@@ -16,7 +16,7 @@ type stack =
   | Return of Llair.Jump.t * Domain.from_call * stack
   | Throw of Llair.Jump.t * stack
   | Empty
-[@@deriving compare, sexp_of]
+[@@deriving compare, equal, sexp_of]
 
 module Work : sig
   type t
@@ -41,7 +41,7 @@ end = struct
   module Edge = struct
     module T = struct
       type t = {dst: Llair.Block.t; src: Llair.Block.t option; stk: stack}
-      [@@deriving compare, sexp_of]
+      [@@deriving compare, equal, sexp_of]
     end
 
     include T
@@ -67,7 +67,7 @@ end = struct
         | `Both (d1, d2) -> Some (Int.min d1 d2) )
   end
 
-  type priority = int * Edge.t [@@deriving compare]
+  type priority = int * Edge.t [@@deriving compare, equal]
   type priority_queue = priority Fheap.t
   type waiting_states = (Domain.t * Depths.t) list Map.M(Llair.Block).t
   type t = priority_queue * waiting_states

sledge/src/import/import.ml

@@ -209,6 +209,8 @@ end
 module Map = struct
   include Base.Map
 
+  let equal_m__t (module Elt : Compare_m) equal_v = equal equal_v
+
   let find_and_remove_exn m k =
     let found = ref None in
     let m =
@@ -256,6 +258,7 @@ module Set = struct
 
   type ('elt, 'cmp) tree = ('elt, 'cmp) Using_comparator.Tree.t
 
+  let equal_m__t (module Elt : Compare_m) = equal
   let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x)
   let disjoint x y = is_empty (inter x y)
   let diff_inter_diff x y = (diff x y, inter x y, diff y x)

sledge/src/import/import.mli

@@ -162,6 +162,13 @@ end
 module Map : sig
   include module type of Base.Map
 
+  val equal_m__t :
+       (module Compare_m)
+    -> ('v -> 'v -> bool)
+    -> ('k, 'v, 'c) t
+    -> ('k, 'v, 'c) t
+    -> bool
+
   val find_and_remove_exn : ('k, 'v, 'c) t -> 'k -> 'v * ('k, 'v, 'c) t
   val find_and_remove : ('k, 'v, 'c) t -> 'k -> ('v * ('k, 'v, 'c) t) option
 
@@ -200,6 +207,9 @@ module Set : sig
 
   type ('e, 'c) tree
 
+  val equal_m__t :
+    (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> bool
+
   val pp : 'e pp -> ('e, 'c) t pp
   val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool
 

sledge/src/import/qset.ml

@@ -45,6 +45,7 @@ let m__t_of_sexp (type elt cmp)
   Map.m__t_of_sexp (module Elt) q_of_sexp sexp
 
 let compare_m__t (module Elt : Compare_m) = Map.compare_direct Q.compare
+let equal_m__t (module Elt : Compare_m) = Map.equal Q.equal
 
 let hash_fold_m__t (type elt) (module Elt : Hash_fold_m with type t = elt)
     state =

sledge/src/import/qset.mli

@@ -45,6 +45,9 @@ val m__t_of_sexp :
 val compare_m__t :
   (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> int
 
+val equal_m__t :
+  (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> bool
+
 val hash_fold_m__t :
      (module Hash_fold_m with type t = 'elt)
   -> Hash.state

sledge/src/import/vector.ml

@@ -17,12 +17,13 @@ let a (v : 'a t) : 'a array = Caml.Obj.magic v
 let _vl (al : 'a array list) : 'a t list = Caml.Obj.magic al
 let al (vl : 'a t list) : 'a array list = Caml.Obj.magic vl
 let compare cmp x y = Array.compare cmp (a x) (a y)
+let equal cmp x y = Array.equal cmp (a x) (a y)
 let hash_fold_t f s x = Hash.Builtin.hash_fold_array_frozen f s (a x)
 let t_of_sexp a_of_sexp s = v (Array.t_of_sexp a_of_sexp s)
 let sexp_of_t sexp_of_a x = Array.sexp_of_t sexp_of_a (a x)
 
 module Infix = struct
-  type +'a vector = 'a t [@@deriving compare, hash, sexp]
+  type +'a vector = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
 let concat_map x ~f = v (Array.concat_map (a x) ~f:(fun y -> a (f y)))

sledge/src/import/vector.mli

@@ -13,10 +13,10 @@
 
 open Base
 
-type +'a t [@@deriving compare, hash, sexp]
+type +'a t [@@deriving compare, equal, hash, sexp]
 
 module Infix : sig
-  type +'a vector = 'a t [@@deriving compare, hash, sexp]
+  type +'a vector = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
 (* val binary_search :
@@ -180,6 +180,5 @@ val reduce_exn : 'a t -> f:('a -> 'a -> 'a) -> 'a
 (* val last : 'a t -> 'a *)
 
 val empty : 'a t
-(* val equal : 'a t -> 'a t -> equal:('a -> 'a -> bool) -> bool *)
 (* val to_sequence : 'a t -> 'a Sequence.t *)
 (* val to_sequence_mutable : 'a t -> 'a Sequence.t *)

sledge/src/llair/exp.ml

@@ -54,7 +54,7 @@ module Z = struct
 end
 
 module rec T : sig
-  type qset = Qset.M(T).t [@@deriving compare, hash, sexp]
+  type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
     | App of {op: t; arg: t}
@@ -105,7 +105,7 @@ module rec T : sig
     | Struct_rec of {elts: t vector}  (** NOTE: may be cyclic *)
     (* unary: conversion *)
     | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
-  [@@deriving compare, hash, sexp]
+  [@@deriving compare, equal, hash, sexp]
 
   type comparator_witness
 
@@ -117,7 +117,7 @@ end
 
 (* auxiliary definition for safe recursive module initialization *)
 and T0 : sig
-  type qset = Qset.M(T).t [@@deriving compare, hash, sexp]
+  type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
     | App of {op: t; arg: t}
@@ -159,9 +159,9 @@ and T0 : sig
     | Update
     | Struct_rec of {elts: t vector}
     | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
-  [@@deriving compare, hash, sexp]
+  [@@deriving compare, equal, hash, sexp]
 end = struct
-  type qset = Qset.M(T).t [@@deriving compare, hash, sexp]
+  type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
     | App of {op: t; arg: t}
@@ -203,7 +203,7 @@ end = struct
     | Update
     | Struct_rec of {elts: t vector}
     | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
-  [@@deriving compare, hash, sexp]
+  [@@deriving compare, equal, hash, sexp]
 end
 
 (* suppress spurious "Warning 60: unused module T0." *)
@@ -212,7 +212,6 @@ type _t = T0.t
 include T
 
 let empty_qset = Qset.empty (module T)
-let equal = [%compare.equal: t]
 let sorted e f = compare e f <= 0
 let sort e f = if sorted e f then (e, f) else (f, e)
 
@@ -473,7 +472,6 @@ let bits_of_int exp =
 module Var = struct
   include T
 
-  let equal = equal
   let pp = pp
 
   type var = t
@@ -483,7 +481,7 @@ module Var = struct
       Set :
         module type of Set with type ('elt, 'cmp) t := ('elt, 'cmp) Set.t )
 
-    type t = Set.M(T).t [@@deriving compare, sexp]
+    type t = Set.M(T).t [@@deriving compare, equal, sexp]
 
     let pp vs = Set.pp pp_t vs
     let empty = Set.empty (module T)
@@ -535,7 +533,7 @@ module Var = struct
 
   (** Variable renaming substitutions *)
   module Subst = struct
-    type t = T.t Map.M(T).t [@@deriving compare, sexp]
+    type t = T.t Map.M(T).t [@@deriving compare, equal, sexp]
 
     let invariant s =
       Invariant.invariant [%here] s [%sexp_of: t]
@@ -571,7 +569,7 @@ module Var = struct
       | `Duplicate -> sub
       | `Ok sub ->
           Map.map_preserving_phys_equal sub ~f:(fun v ->
-              if equal v replace then with_ else v ) )
+              if T.equal v replace then with_ else v ) )
       |> check invariant
 
     let invert sub =

sledge/src/llair/exp.mli

@@ -74,13 +74,12 @@ and t = private
           (transitively) from [elts]. NOTE: represented by cyclic values. *)
   | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
       (** Convert between specified types, possibly with loss of information *)
-[@@deriving compare, hash, sexp]
+[@@deriving compare, equal, hash, sexp]
 
 val comparator : (t, comparator_witness) Comparator.t
 
 type exp = t
 
-val equal : t -> t -> bool
 val sort : t -> t -> t * t
 val sorted : t -> t -> bool
 val pp : t pp
@@ -88,20 +87,20 @@ val invariant : ?partial:bool -> t -> unit
 
 (** Exp.Var is re-exported as Var *)
 module Var : sig
-  type t = private exp [@@deriving compare, hash, sexp]
+  type t = private exp [@@deriving compare, equal, hash, sexp]
   type var = t
 
   include Comparator.S with type t := t
 
   module Set : sig
-    type t = (var, comparator_witness) Set.t [@@deriving compare, sexp]
+    type t = (var, comparator_witness) Set.t
+    [@@deriving compare, equal, sexp]
 
     val pp : t pp
     val empty : t
     val of_vector : var vector -> t
   end
 
-  val equal : t -> t -> bool
   val pp : t pp
   val pp_demangled : t pp
 
@@ -114,7 +113,7 @@ module Var : sig
   val name : t -> string
 
   module Subst : sig
-    type t [@@deriving compare, sexp]
+    type t [@@deriving compare, equal, sexp]
 
     val pp : t pp
     val empty : t

sledge/src/llair/global.ml

@@ -8,9 +8,7 @@
 (** Global variables *)
 
 type t = {var: Var.t; init: Exp.t option; siz: int; typ: Typ.t; loc: Loc.t}
-[@@deriving compare, hash, sexp]
-
-let equal = [%compare.equal: t]
+[@@deriving compare, equal, hash, sexp]
 
 let pp fs {var} =
   let name = Var.name var in

sledge/src/llair/global.mli

@@ -9,9 +9,8 @@
 
 type t = private
   {var: Var.t; init: Exp.t option; siz: int; typ: Typ.t; loc: Loc.t}
-[@@deriving compare, hash, sexp]
+[@@deriving compare, equal, hash, sexp]
 
-val equal : t -> t -> bool
 val pp : t pp
 val pp_defn : t pp
 

sledge/src/llair/llair.ml

@@ -25,7 +25,7 @@ type label = string [@@deriving sexp]
 
 type 'a control_transfer =
   {mutable dst: 'a; args: Exp.t list; mutable retreating: bool}
-[@@deriving compare, sexp_of]
+[@@deriving compare, equal, sexp_of]
 
 type jump = block control_transfer
 
@@ -79,6 +79,7 @@ and sexp_of_func f = [%sexp_of: func] f
 
 (* blocks in a [t] are uniquely identified by [sort_index] *)
 let compare_block x y = Int.compare x.sort_index y.sort_index
+let equal_block x y = Int.equal x.sort_index y.sort_index
 
 type t = {globals: Global.t vector; functions: func vector}
 [@@deriving sexp_of]
@@ -230,6 +231,7 @@ module Jump = struct
   type t = jump [@@deriving sexp_of]
 
   let compare = compare_control_transfer compare_block
+  let equal = equal_control_transfer equal_block
   let pp = pp_jump
 
   let invariant ?(accept_return = false) jmp =
@@ -311,7 +313,7 @@ end
 (** Basic-Blocks *)
 
 module Block = struct
-  module T = struct type t = block [@@deriving compare, sexp_of] end
+  module T = struct type t = block [@@deriving compare, equal, sexp_of] end
   include T
   include Comparator.Make (T)
 

sledge/src/llair/llair.mli

@@ -143,7 +143,7 @@ module Inst : sig
 end
 
 module Jump : sig
-  type t = jump [@@deriving compare, sexp_of]
+  type t = jump [@@deriving compare, equal, sexp_of]
 
   val pp : jump pp
   val mk : string -> Exp.t list -> jump
@@ -182,7 +182,7 @@ module Term : sig
 end
 
 module Block : sig
-  type t = block [@@deriving compare, sexp_of]
+  type t = block [@@deriving compare, equal, sexp_of]
 
   include Comparator.S with type t := t
 

sledge/src/llair/loc.ml

@@ -8,7 +8,7 @@
 (** Source code debug locations *)
 
 type t = {dir: string; file: string; line: int; col: int}
-[@@deriving compare, hash, sexp]
+[@@deriving compare, equal, hash, sexp]
 
 let none = {dir= ""; file= ""; line= 0; col= 0}
 let is_none loc = compare loc none = 0

sledge/src/llair/loc.mli

@@ -8,7 +8,7 @@
 (** Source code debug locations *)
 
 type t = {dir: string; file: string; line: int; col: int}
-[@@deriving compare, hash, sexp]
+[@@deriving compare, equal, hash, sexp]
 
 val pp : t pp
 val none : t

sledge/src/llair/typ.ml

@@ -17,12 +17,10 @@ type t =
   | Struct of
       { name: string
       ; elts: t vector (* possibly cyclic, name unique *)
-             [@compare.ignore] [@sexp_drop_if fun _ -> true]
+             [@compare.ignore] [@equal.ignore] [@sexp_drop_if fun _ -> true]
       ; packed: bool }
   | Opaque of {name: string}
-[@@deriving compare, hash, sexp]
-
-let equal x y = compare x y = 0
+[@@deriving compare, equal, hash, sexp]
 
 let rec pp fs typ =
   let pf pp =

sledge/src/llair/typ.mli

@@ -24,9 +24,8 @@ type t = private
           types are represented by cyclic values. *)
   | Opaque of {name: string}
       (** Uniquely named aggregate type whose definition is hidden. *)
-[@@deriving compare, hash, sexp]
+[@@deriving compare, equal, hash, sexp]
 
-val equal : t -> t -> bool
 val pp : t pp
 val pp_defn : t pp
 

sledge/src/symbheap/congruence.ml

@@ -69,9 +69,7 @@
 
 (** set of exps representing congruence classes *)
 module Cls = struct
-  type t = Exp.t list [@@deriving compare, sexp]
-
-  let equal = [%compare.equal: t]
+  type t = Exp.t list [@@deriving compare, equal, sexp]
 
   let pp fs cls =
     Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp)
@@ -91,9 +89,7 @@ end
 
 (** set of exps representing "use lists" encoding super-expression relation *)
 module Use = struct
-  type t = Exp.t list [@@deriving compare, sexp]
-
-  let equal = [%compare.equal: t]
+  type t = Exp.t list [@@deriving compare, equal, sexp]
 
   let pp fs uses =
     Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp) uses
@@ -109,7 +105,7 @@ module Use = struct
   let map = List.map_preserving_phys_equal
 end
 
-type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, sexp]
+type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, equal, sexp]
 
 (** see also [invariant] *)
 type t =
@@ -132,7 +128,7 @@ type t =
         (** equations of the form [a+i = b+j], where [a] and [b] are in the
             carrier, to be added to the relation by merging the classes of
             [a] and [b] *) }
-[@@deriving compare, sexp]
+[@@deriving compare, equal, sexp]
 
 (** Pretty-printing *)
 

sledge/src/symbheap/congruence.mli

@@ -7,7 +7,7 @@
 
 (** Constraints representing congruence relations *)
 
-type t [@@deriving compare, sexp]
+type t [@@deriving compare, equal, sexp]
 
 val pp : t pp
 val pp_classes : t pp

sledge/src/symbheap/domain.ml

@@ -24,7 +24,7 @@ let join = Sh.or_
 let assume q b = Exec.assume b q
 let exec_inst = Exec.inst
 
-type from_call = Var.Subst.t [@@deriving compare, sexp]
+type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
 
 (** Express formula in terms of formals instead of actuals, and enter scope
     of locals: rename formals to fresh vars in formula and actuals, add

sledge/src/symbheap/domain.mli

@@ -16,7 +16,7 @@ val join : t -> t -> t
 val assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, t * Llair.inst) result
 
-type from_call [@@deriving compare, sexp]
+type from_call [@@deriving compare, equal, sexp]
 
 val call : t -> Exp.t list -> Var.t list -> Var.Set.t -> t * from_call
 val retn : Var.Set.t -> from_call -> t -> t

sledge/src/symbheap/equality.ml

@@ -7,11 +7,11 @@
 
 (** Equality over uninterpreted functions and linear rational arithmetic *)
 
-type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, sexp]
+type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, equal, sexp]
 
 let empty_map = Map.empty (module Exp)
 
-type subst = Exp.t exp_map [@@deriving compare, sexp]
+type subst = Exp.t exp_map [@@deriving compare, equal, sexp]
 
 (** see also [invariant] *)
 type t =
@@ -20,7 +20,7 @@ type t =
         (** functional set of oriented equations: map [a] to [a'],
             indicating that [a = a'] holds, and that [a'] is the
             'rep(resentative)' of [a] *) }
-[@@deriving compare, sexp]
+[@@deriving compare, equal, sexp]
 
 (** Pretty-printing *)
 

sledge/src/symbheap/equality.mli

@@ -8,7 +8,7 @@
 (** Constraints representing equivalence relations over uninterpreted
     functions and linear rational arithmetic *)
 
-type t [@@deriving compare, sexp]
+type t [@@deriving compare, equal, sexp]
 
 val pp : t pp
 val pp_classes : t pp

sledge/src/symbheap/sh.ml

@@ -10,7 +10,7 @@
 [@@@warning "+9"]
 
 type seg = {loc: Exp.t; bas: Exp.t; len: Exp.t; siz: Exp.t; arr: Exp.t}
-[@@deriving compare, sexp]
+[@@deriving compare, equal, sexp]
 
 type starjunction =
   { us: Var.Set.t
@@ -19,11 +19,11 @@ type starjunction =
   ; pure: Exp.t list
   ; heap: seg list
   ; djns: disjunction list }
-[@@deriving compare, sexp]
+[@@deriving compare, equal, sexp]
 
 and disjunction = starjunction list
 
-type t = starjunction [@@deriving compare, sexp]
+type t = starjunction [@@deriving compare, equal, sexp]
 
 let map_seg {loc; bas; len; siz; arr} ~f =
   {loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr}