From c52b49e6c08cdf3c0d3cb4fae7e6df6949c5ba6a Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 8 Jan 2020 08:03:42 -0800
Subject: [PATCH] [sledge] Add Term.Map and Var.Map

Reviewed By: ngorogiannis

Differential Revision: D19221871

fbshipit-source-id: bc83a6c8b
---
 sledge/src/llair/term.ml  | 27 +++++++++++++++------------
 sledge/src/llair/term.mli | 20 +++++++++++++++++++-
 2 files changed, 34 insertions(+), 13 deletions(-)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index fcd80dd78..e2b636af4 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -111,7 +111,17 @@ type _t = T0.t
 
 include T
 
-let empty_map = Map.empty (module T)
+module Map = struct
+  include (
+    Map :
+      module type of Map
+        with type ('key, 'value, 'cmp) t := ('key, 'value, 'cmp) Map.t )
+
+  type 'v t = 'v Map.M(T).t [@@deriving compare, equal, sexp]
+
+  let empty = empty (module T)
+end
+
 let empty_qset = Qset.empty (module T)
 
 let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
@@ -294,6 +304,8 @@ module Var = struct
 
   let pp = pp
 
+  module Map = Map
+
   module Set = struct
     include (
       Set :
@@ -310,15 +322,6 @@ module Var = struct
     let of_vector = Set.of_vector (module T)
   end
 
-  module Map = struct
-    include (
-      Map :
-        module type of Map
-          with type ('key, 'value, 'cmp) t := ('key, 'value, 'cmp) Map.t )
-
-    type 'v t = 'v Map.M(T).t [@@deriving compare, equal, sexp]
-  end
-
   let invariant x =
     Invariant.invariant [%here] x [%sexp_of: t]
     @@ fun () -> match x with Var _ -> invariant x | _ -> assert false
@@ -360,7 +363,7 @@ module Var = struct
              Format.fprintf fs "@[%a ↦ %a@]" pp_t k pp_t v ))
         (Map.to_alist s)
 
-    let empty = empty_map
+    let empty = Map.empty
     let is_empty = Map.is_empty
 
     let freshen vs ~wrt =
@@ -1070,7 +1073,7 @@ let solve e f =
       | _ -> solve_uninterp e f )
     | _ -> solve_uninterp e f
   in
-  solve_ e f empty_map
+  solve_ e f Map.empty
   |>
   [%Trace.retn fun {pf} ->
     function Some s -> pf "%a" Var.Subst.pp s | None -> pf "false"]
diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli
index c43c33165..7e2e0833e 100644
--- a/sledge/src/llair/term.mli
+++ b/sledge/src/llair/term.mli
@@ -109,6 +109,15 @@ module Var : sig
     val of_vector : var vector -> t
   end
 
+  module Map : sig
+    type var := t
+
+    type 'a t = (var, 'a, comparator_witness) Map.t
+    [@@deriving compare, equal, sexp]
+
+    val empty : 'a t
+  end
+
   val pp : t pp
 
   include Invariant.S with type t := t
@@ -136,6 +145,15 @@ module Var : sig
   end
 end
 
+module Map : sig
+  type term := t
+
+  type 'a t = (term, 'a, comparator_witness) Map.t
+  [@@deriving compare, equal, sexp]
+
+  val empty : 'a t
+end
+
 (** Construct *)
 
 (* variables *)
@@ -225,4 +243,4 @@ val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
 val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
-val solve : t -> t -> (t, t, comparator_witness) Map.t option
+val solve : t -> t -> t Map.t option