From c7c06addfdd16c6e049236d643056dae5ef5f006 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 21 Feb 2021 13:17:40 -0800 Subject: [PATCH] [sledge] Adapt Multiset to Comparer interface Reviewed By: jvillard Differential Revision: D26250523 fbshipit-source-id: 1d530785c --- sledge/nonstdlib/multiset.ml | 36 +++++++++++++++++++------------ sledge/nonstdlib/multiset.mli | 16 +++++++++++--- sledge/nonstdlib/multiset_intf.ml | 17 ++++++++++----- sledge/src/fol/arithmetic.ml | 18 +++++++++++----- sledge/src/fol/arithmetic_intf.ml | 3 +++ sledge/src/fol/trm.ml | 7 +++++- 6 files changed, 69 insertions(+), 28 deletions(-) diff --git a/sledge/nonstdlib/multiset.ml b/sledge/nonstdlib/multiset.ml index d1a940bee..44daada33 100644 --- a/sledge/nonstdlib/multiset.ml +++ b/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 equal = M.equal Mul.equal + let comparer = M.comparer Mul.comparer 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 = - List.sexp_of_t - (Sexplib.Conv.sexp_of_pair Elt.sexp_of_t Mul.sexp_of_t) - (M.to_list s) + module Provide_of_sexp (Elt : sig + type t = elt [@@deriving of_sexp] + end) = + struct + include M.Provide_of_sexp (Elt) - let t_of_sexp elt_of_sexp sexp = - M.of_list - (List.t_of_sexp - (Sexplib.Conv.pair_of_sexp elt_of_sexp Mul.t_of_sexp) - sexp) + let t_of_sexp = t_of_sexp Mul.t_of_sexp + end let pp ?pre ?suf sep pp_elt fs s = List.pp ?pre ?suf sep pp_elt fs (Iter.to_list (M.to_iter s)) diff --git a/sledge/nonstdlib/multiset.mli b/sledge/nonstdlib/multiset.mli index b378f89b6..a11c34141 100644 --- a/sledge/nonstdlib/multiset.mli +++ b/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 diff --git a/sledge/nonstdlib/multiset_intf.ml b/sledge/nonstdlib/multiset_intf.ml index d2110c046..51492bc1a 100644 --- a/sledge/nonstdlib/multiset_intf.ml +++ b/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 diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml index c920c3b49..cdb69cc13 100644 --- a/sledge/src/fol/arithmetic.ml +++ b/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) - - let t_of_sexp = t_of_sexp Trm.t_of_sexp + include Provide_of_sexp (Trm) end module Mono = struct @@ -78,9 +87,8 @@ struct end module Sum = struct - include Multiset.Make (Mono) (Q) - - let t_of_sexp = t_of_sexp Mono.t_of_sexp + include Multiset.Make (Prod) (Q) + include Provide_of_sexp (Prod) end module Poly = Sum diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml index 753fa7861..0f44cbbba 100644 --- a/sledge/src/fol/arithmetic_intf.ml +++ b/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 diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index e33472f5a..ea2ee270a 100644 --- a/sledge/src/fol/trm.ml +++ b/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) =