From ae3c059fe9dcc0a050a094fab2dc22ae30b75861 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 23 Mar 2020 06:18:36 -0700
Subject: [PATCH] [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               |  4 +--
 sledge/lib/exp.ml             |  8 +----
 sledge/lib/import/dune        |  2 +-
 sledge/lib/import/set.ml      | 64 +++++++++++++++--------------------
 sledge/lib/import/set.mli     |  6 ++--
 sledge/lib/import/set_intf.ml | 37 +++++---------------
 sledge/lib/term.ml            |  7 +---
 7 files changed, 46 insertions(+), 82 deletions(-)

diff --git a/sledge/bin/dune b/sledge/bin/dune
index a4c8ed933..993508f6d 100644
--- a/sledge/bin/dune
+++ b/sledge/bin/dune
@@ -6,8 +6,8 @@
 (executable
  (public_name sledge)
  (package sledge)
- (libraries apron apron.boxMPQ core ctypes ctypes.foreign dune-build-info
-   llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
+ (libraries apron apron.boxMPQ ctypes ctypes.foreign dune-build-info llvm
+   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))
diff --git a/sledge/lib/exp.ml b/sledge/lib/exp.ml
index 87aebff8d..f6777df92 100644
--- a/sledge/lib/exp.ml
+++ b/sledge/lib/exp.ml
@@ -79,13 +79,7 @@ module T = struct
 end
 
 include T
-
-module Set = struct
-  include Set.Make (T)
-
-  let t_of_sexp = t_of_sexp T.t_of_sexp
-end
-
+module Set = struct include Set.Make (T) include Provide_of_sexp (T) end
 module Map = Map.Make (T)
 
 let term e = e.term
diff --git a/sledge/lib/import/dune b/sledge/lib/import/dune
index a57711243..00ec926ad 100644
--- a/sledge/lib/import/dune
+++ b/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))
diff --git a/sledge/lib/import/set.ml b/sledge/lib/import/set.ml
index 32f168a0e..1f95fa93e 100644
--- a/sledge/lib/import/set.ml
+++ b/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 S = Caml.Set.Make (Elt)
+module Make (Elt : sig
+  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
-  let equal = S.equal
-  let sexp_of_t s = List.sexp_of_t Elt.sexp_of_t (S.elements s)
+  include EltSet.Tree
 
-  let t_of_sexp elt_of_sexp sexp =
-    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 pp_elt fs x = List.pp ",@ " pp_elt fs (elements x)
 
   let pp_diff pp_elt fs (xs, ys) =
-    let lose = S.diff xs ys and gain = S.diff ys xs in
-    if not (S.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
-
-  let empty = S.empty
-  let of_ x = S.add x empty
-  let of_option = Option.fold ~f:(fun x y -> S.add y x) ~init:empty
-  let of_list = S.of_list
-  let of_vector x = S.of_list (IArray.to_list x)
-  let add s e = S.add e s
-  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 remove s e = S.remove e s
-  let filter s ~f = S.filter f s
-  let union = S.union
-  let union_list ss = List.fold ss ~init:empty ~f:union
-  let diff = S.diff
-  let inter = S.inter
-  let diff_inter x y = (S.diff x y, S.inter x y)
-  let is_empty = S.is_empty
-  let mem s e = S.mem e s
-  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
+    let lose = diff xs ys and gain = diff ys xs in
+    if not (is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ;
+    if not (is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain
+
+  let of_ x = add empty x
+  let of_option = Option.fold ~f:add ~init:empty
+  let of_iarray a = of_array (IArray.to_array a)
+  let add_option xo s = Option.fold ~f:add ~init:s xo
+  let add_list xs s = List.fold ~f:add ~init:s xs
+  let diff_inter s t = (diff s t, inter s t)
+
+  let rec disjoint s1 s2 =
+    match choose s1 with
+    | None -> true
+    | _ when is_empty s2 -> true
+    | _ when s1 == s2 -> false
+    | Some x -> (
+        let l1, _, r1 = split s1 x in
+        match split s2 x with
+        | _, Some _, _ -> false
+        | l2, None, r2 -> disjoint l1 l2 && disjoint r1 r2 )
 end
diff --git a/sledge/lib/import/set.mli b/sledge/lib/import/set.mli
index 4ef862c8d..20fed6478 100644
--- a/sledge/lib/import/set.mli
+++ b/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
diff --git a/sledge/lib/import/set_intf.ml b/sledge/lib/import/set_intf.ml
index 29b98cb6a..8db56475b 100644
--- a/sledge/lib/import/set_intf.ml
+++ b/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
-  val equal : t -> t -> bool
-  val sexp_of_t : t -> Sexp.t
-  val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
+  module Elt : sig
+    type t = elt
+
+    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_vector : elt IArray.t -> t
-
-  (* constructors *)
-  val add : t -> elt -> t
+  val of_iarray : elt IArray.t -> 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
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index db243c756..77b639ba6 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -101,12 +101,7 @@ end
 
 include T
 module Map = Map.Make (T)
-
-module Set = struct
-  include Set.Make (T)
-
-  let t_of_sexp = t_of_sexp T.t_of_sexp
-end
+module Set = struct include Set.Make (T) include Provide_of_sexp (T) end
 
 let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
   let rec fix_f seen e =