[sledge] Adapt Multiset to Comparer interface

Reviewed By: jvillard

Differential Revision: D26250523

fbshipit-source-id: 1d530785c

sledge/nonstdlib/multiset.ml

@@ -8,21 +8,31 @@
 (** Multiset - Set with multiplicity for each element *)
 
 open! NS0
+module Map = NSMap
 include Multiset_intf
 
+type ('elt, 'mul, 'compare_elt) t = ('elt, 'mul, 'compare_elt) Map.t
+[@@deriving compare, equal, sexp]
+
+type ('compare_elt, 'compare_mul) compare =
+  ('compare_elt, 'compare_mul) Map.compare
+[@@deriving compare, equal, sexp]
+
 module Make (Elt : sig
-  type t [@@deriving compare, equal, sexp_of]
+  type t [@@deriving equal, sexp_of]
+
+  include Comparer.S with type t := t
 end)
 (Mul : MULTIPLICITY) =
 struct
-  module M = NSMap.Make (Elt)
+  module M = Map.Make_from_Comparer (Elt)
 
   type mul = Mul.t
   type elt = Elt.t
-  type t = Mul.t M.t
+  type t = Mul.t M.t [@@deriving compare, equal, sexp_of]
+  type compare = Mul.compare M.compare [@@deriving compare, equal, sexp]
 
-  let compare = M.compare Mul.compare
+  let comparer = M.comparer Mul.comparer
-  let equal = M.equal Mul.equal
 
   let hash_fold_t hash_fold_elt s m =
     let hash_fold_mul s i = Hash.fold_int s (Mul.hash i) in
@@ -30,16 +40,14 @@ struct
     M.fold m init ~f:(fun ~key ~data state ->
         hash_fold_mul (hash_fold_elt state key) data )
 
-  let sexp_of_t s =
+  module Provide_of_sexp (Elt : sig
-    List.sexp_of_t
+    type t = elt [@@deriving of_sexp]
-      (Sexplib.Conv.sexp_of_pair Elt.sexp_of_t Mul.sexp_of_t)
+  end) =
-      (M.to_list s)
+  struct
+    include M.Provide_of_sexp (Elt)
 
-  let t_of_sexp elt_of_sexp sexp =
+    let t_of_sexp = t_of_sexp Mul.t_of_sexp
-    M.of_list
+  end
-      (List.t_of_sexp
-         (Sexplib.Conv.pair_of_sexp elt_of_sexp Mul.t_of_sexp)
-         sexp)
 
   let pp ?pre ?suf sep pp_elt fs s =
     List.pp ?pre ?suf sep pp_elt fs (Iter.to_list (M.to_iter s))

sledge/nonstdlib/multiset.mli

@@ -5,11 +5,21 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Multiset - Set with (signed) rational multiplicity for each element *)
+(** Multiset - Set with multiplicity for each element *)
 
 include module type of Multiset_intf
 
+type ('elt, 'mul, 'compare_elt) t [@@deriving compare, equal, sexp]
+type ('compare_elt, 'compare_mul) compare [@@deriving compare, equal, sexp]
+
 module Make (Elt : sig
-  type t [@@deriving compare, equal, sexp_of]
+  type t [@@deriving equal, sexp_of]
+
+  include Comparer.S with type t := t
 end)
-(Mul : MULTIPLICITY) : S with type mul = Mul.t with type elt = Elt.t
+(Mul : MULTIPLICITY) :
+  S
+    with type mul = Mul.t
+    with type elt = Elt.t
+    with type compare = (Elt.compare, Mul.compare) compare
+    with type t = (Elt.t, Mul.t, Elt.compare) t

sledge/nonstdlib/multiset_intf.ml

@@ -12,6 +12,8 @@ open! NS0
 module type MULTIPLICITY = sig
   type t [@@deriving compare, equal, hash, sexp]
 
+  include Comparer.S with type t := t
+
   val zero : t
   val add : t -> t -> t
   val sub : t -> t -> t
@@ -21,13 +23,18 @@ end
 module type S = sig
   type mul
   type elt
-  type t
+  type t [@@deriving compare, equal, sexp_of]
 
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
   val hash_fold_t : elt Hash.folder -> t Hash.folder
-  val sexp_of_t : t -> Sexp.t
+
-  val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
+  include Comparer.S with type t := t
+
+  module Provide_of_sexp (_ : sig
+    type t = elt [@@deriving of_sexp]
+  end) : sig
+    type t [@@deriving of_sexp]
+  end
+  with type t := t
 
   val pp :
        ?pre:(unit, unit) fmt

sledge/src/fol/arithmetic.ml

@@ -9,14 +9,23 @@
 
 include Arithmetic_intf
 
+module Int = struct
+  include Int
+  include Comparer.Make (Int)
+end
+
+module Q = struct
+  include Q
+  include Comparer.Make (Q)
+end
+
 module Representation
     (Var : Var_intf.S)
     (Trm : INDETERMINATE with type var := Var.t) =
 struct
   module Prod = struct
     include Multiset.Make (Trm) (Int)
-
+    include Provide_of_sexp (Trm)
-    let t_of_sexp = t_of_sexp Trm.t_of_sexp
   end
 
   module Mono = struct
@@ -78,9 +87,8 @@ struct
   end
 
   module Sum = struct
-    include Multiset.Make (Mono) (Q)
+    include Multiset.Make (Prod) (Q)
-
+    include Provide_of_sexp (Prod)
-    let t_of_sexp = t_of_sexp Mono.t_of_sexp
   end
 
   module Poly = Sum

sledge/src/fol/arithmetic_intf.ml

@@ -84,6 +84,9 @@ end
     be flattened using [EMBEDDING.get_arith]. *)
 module type INDETERMINATE = sig
   type t [@@deriving compare, equal, sexp]
+
+  include Comparer.S with type t := t
+
   type var
 
   val pp : t pp

sledge/src/fol/trm.ml

@@ -12,7 +12,12 @@ module rec Arith0 :
   (Arithmetic.REPRESENTATION
     with type var := Trm.Var1.t
     with type trm := Trm.t) =
-  Arithmetic.Representation (Trm.Var1) (Trm)
+  Arithmetic.Representation
+    (Trm.Var1)
+    (struct
+      include Trm
+      include Comparer.Make (Trm)
+    end)
 
 (** Arithmetic terms *)
 and Arith : (Arithmetic.S with type trm := Trm.t with type t = Arith0.t) =