[sledge] Define Set as a functor over the Tree underlying Core.Set

Summary:
This diff defines Set as a functorover the underlying implementation
of Core.Set. This results in set values that are just trees, with no
comparison function closures, and with the same interface (almost) and
underlying data structure implementation as Core.Set.

Reviewed By: ngorogiannis

Differential Revision: D20583754

fbshipit-source-id: 79aa7477a

sledge/bin/dune

@@ -6,8 +6,8 @@
 (executable
  (public_name sledge)
  (package sledge)
- (libraries apron apron.boxMPQ core ctypes ctypes.foreign dune-build-info
+ (libraries apron apron.boxMPQ ctypes ctypes.foreign dune-build-info llvm
-   llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
+   llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
    llvm.linker shexp.process yojson trace import sledgelib model)
  (flags
   (:standard -open Import -open Sledgelib -open Model))

sledge/lib/exp.ml

@@ -79,13 +79,7 @@ module T = struct
 end
 
 include T
-
+module Set = struct include Set.Make (T) include Provide_of_sexp (T) end
-module Set = struct
-  include Set.Make (T)
-
-  let t_of_sexp = t_of_sexp T.t_of_sexp
-end
-
 module Map = Map.Make (T)
 
 let term e = e.term

sledge/lib/import/dune

@@ -6,7 +6,7 @@
 (library
  (name import)
  (public_name sledge.import)
- (libraries core_kernel.fheap zarith trace)
+ (libraries core core_kernel.fheap zarith trace)
  (flags (:standard))
  (preprocess
   (pps ppx_sledge))

sledge/lib/import/set.ml

@@ -5,48 +5,40 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Import0
 include Set_intf
 
-module Make (Elt : OrderedType) : S with type elt = Elt.t = struct
+module Make (Elt : sig
-  module S = Caml.Set.Make (Elt)
+  type t [@@deriving compare, sexp_of]
+end) : S with type elt = Elt.t = struct
+  module EltSet = Core.Set.Make_plain (Elt)
+  module Elt = EltSet.Elt
 
   type elt = Elt.t
-  type t = S.t
 
-  let compare = S.compare
+  include EltSet.Tree
-  let equal = S.equal
-  let sexp_of_t s = List.sexp_of_t Elt.sexp_of_t (S.elements s)
 
-  let t_of_sexp elt_of_sexp sexp =
+  let pp pp_elt fs x = List.pp ",@ " pp_elt fs (elements x)
-    S.of_list (List.t_of_sexp elt_of_sexp sexp)
-
-  let pp pp_elt fs x = List.pp ",@ " pp_elt fs (S.elements x)
 
   let pp_diff pp_elt fs (xs, ys) =
-    let lose = S.diff xs ys and gain = S.diff ys xs in
+    let lose = diff xs ys and gain = diff ys xs in
-    if not (S.is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ;
+    if not (is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ;
-    if not (S.is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain
+    if not (is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain
-
+
-  let empty = S.empty
+  let of_ x = add empty x
-  let of_ x = S.add x empty
+  let of_option = Option.fold ~f:add ~init:empty
-  let of_option = Option.fold ~f:(fun x y -> S.add y x) ~init:empty
+  let of_iarray a = of_array (IArray.to_array a)
-  let of_list = S.of_list
+  let add_option xo s = Option.fold ~f:add ~init:s xo
-  let of_vector x = S.of_list (IArray.to_list x)
+  let add_list xs s = List.fold ~f:add ~init:s xs
-  let add s e = S.add e s
+  let diff_inter s t = (diff s t, inter s t)
-  let add_option yo x = Option.fold ~f:(fun x y -> S.add y x) ~init:x yo
+
-  let add_list ys x = List.fold ~f:(fun x y -> S.add y x) ~init:x ys
+  let rec disjoint s1 s2 =
-  let remove s e = S.remove e s
+    match choose s1 with
-  let filter s ~f = S.filter f s
+    | None -> true
-  let union = S.union
+    | _ when is_empty s2 -> true
-  let union_list ss = List.fold ss ~init:empty ~f:union
+    | _ when s1 == s2 -> false
-  let diff = S.diff
+    | Some x -> (
-  let inter = S.inter
+        let l1, _, r1 = split s1 x in
-  let diff_inter x y = (S.diff x y, S.inter x y)
+        match split s2 x with
-  let is_empty = S.is_empty
+        | _, Some _, _ -> false
-  let mem s e = S.mem e s
+        | l2, None, r2 -> disjoint l1 l2 && disjoint r1 r2 )
-  let is_subset x ~of_ = S.subset x of_
-  let disjoint = S.disjoint
-  let max_elt = S.max_elt_opt
-  let fold s ~init:z ~f = S.fold (fun z x -> f x z) s z
 end

sledge/lib/import/set.mli

@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Import0
 include module type of Set_intf
-module Make (Elt : OrderedType) : S with type elt = Elt.t
+
+module Make (Elt : sig
+  type t [@@deriving compare, sexp_of]
+end) : S with type elt = Elt.t

sledge/lib/import/set_intf.ml

@@ -9,41 +9,22 @@ open Import0
 
 module type S = sig
   type elt
-  type t
 
-  val compare : t -> t -> int
+  module Elt : sig
-  val equal : t -> t -> bool
+    type t = elt
-  val sexp_of_t : t -> Sexp.t
+
-  val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
+    include Core.Comparator.S with type t := t
+  end
+
+  include Core_kernel.Set_intf.Make_S_plain_tree(Elt).S
+
   val pp : elt pp -> t pp
   val pp_diff : elt pp -> (t * t) pp
-
-  (* initial constructors *)
-  val empty : t
   val of_ : elt -> t
   val of_option : elt option -> t
-  val of_list : elt list -> t
+  val of_iarray : elt IArray.t -> t
-  val of_vector : elt IArray.t -> t
-
-  (* constructors *)
-  val add : t -> elt -> t
   val add_option : elt option -> t -> t
   val add_list : elt list -> t -> t
-  val remove : t -> elt -> t
-  val filter : t -> f:(elt -> bool) -> t
-  val union : t -> t -> t
-  val union_list : t list -> t
-  val diff : t -> t -> t
-  val inter : t -> t -> t
   val diff_inter : t -> t -> t * t
-
-  (* queries *)
-  val is_empty : t -> bool
-  val mem : t -> elt -> bool
-  val is_subset : t -> of_:t -> bool
   val disjoint : t -> t -> bool
-  val max_elt : t -> elt option
-
-  (* traversals *)
-  val fold : t -> init:'s -> f:('s -> elt -> 's) -> 's
 end

sledge/lib/term.ml

@@ -101,12 +101,7 @@ end
 
 include T
 module Map = Map.Make (T)
-
+module Set = struct include Set.Make (T) include Provide_of_sexp (T) end
-module Set = struct
-  include Set.Make (T)
-
-  let t_of_sexp = t_of_sexp T.t_of_sexp
-end
 
 let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
   let rec fix_f seen e =