[sledge] Refactor: Move Ses.Term.Var.Subst to Fol.Var.Subst

Summary:
The `Subst` module is not used by `Ses`, so move it out of the
Ses-internal APIs.

Reviewed By: ngorogiannis

Differential Revision: D22170513

fbshipit-source-id: a189a1440

sledge/src/fol.ml

@@ -5,10 +5,87 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module Var = Ses.Term.Var
+module Var = struct
+  include Ses.Term.Var
+
+  (** Variable renaming substitutions *)
+  module Subst = struct
+    type nonrec t = t Map.t [@@deriving compare, equal, sexp_of]
+    type x = {sub: t; dom: Set.t; rng: Set.t}
+
+    let t_of_sexp = Map.t_of_sexp t_of_sexp
+
+    let invariant s =
+      let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
+      let domain, range =
+        Map.fold s ~init:(Set.empty, Set.empty)
+          ~f:(fun ~key ~data (domain, range) ->
+            (* substs are injective *)
+            assert (not (Set.mem range data)) ;
+            (Set.add domain key, Set.add range data) )
+      in
+      assert (Set.disjoint domain range)
+
+    let pp = Map.pp pp pp
+    let empty = Map.empty
+    let is_empty = Map.is_empty
+
+    let freshen vs ~wrt =
+      let dom = Set.inter wrt vs in
+      ( if Set.is_empty dom then
+        ({sub= empty; dom= Set.empty; rng= Set.empty}, wrt)
+      else
+        let wrt = Set.union wrt vs in
+        let sub, rng, wrt =
+          Set.fold dom ~init:(empty, Set.empty, wrt)
+            ~f:(fun (sub, rng, wrt) x ->
+              let x', wrt = fresh (name x) ~wrt in
+              let sub = Map.add_exn sub ~key:x ~data:x' in
+              let rng = Set.add rng x' in
+              (sub, rng, wrt) )
+        in
+        ({sub; dom; rng}, wrt) )
+      |> check (fun ({sub; _}, _) -> invariant sub)
+
+    let fold sub ~init ~f =
+      Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s)
+
+    let domain sub =
+      Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
+          Set.add domain key )
+
+    let range sub =
+      Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range ->
+          Set.add range data )
+
+    let invert sub =
+      Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
+          Map.add_exn sub' ~key:data ~data:key )
+      |> check invariant
+
+    let restrict sub vs =
+      Map.fold sub ~init:{sub; dom= Set.empty; rng= Set.empty}
+        ~f:(fun ~key ~data z ->
+          if Set.mem vs key then
+            {z with dom= Set.add z.dom key; rng= Set.add z.rng data}
+          else (
+            assert (
+              (* all substs are injective, so the current mapping is the
+                 only one that can cause [data] to be in [rng] *)
+              (not (Set.mem (range (Map.remove sub key)) data))
+              || violates invariant sub ) ;
+            {z with sub= Map.remove z.sub key} ) )
+      |> check (fun {sub; dom; rng} ->
+             assert (Set.equal dom (domain sub)) ;
+             assert (Set.equal rng (range sub)) )
+
+    let apply sub v = Map.find sub v |> Option.value ~default:v
+  end
+end
 
 module Term = struct
-  include Ses.Term
+  include (
+    Ses.Term : module type of Ses.Term with module Var := Ses.Term.Var )
 
   let ite = conditional
   let rename s e = rename (Var.Subst.apply s) e

sledge/src/ses/term.ml

@@ -1062,80 +1062,6 @@ module Var = struct
     let of_regs =
       Llair.Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r))
   end
-
-  (** Variable renaming substitutions *)
-  module Subst = struct
-    type t = T.t Map.t [@@deriving compare, equal, sexp_of]
-    type x = {sub: t; dom: Set.t; rng: Set.t}
-
-    let t_of_sexp = Map.t_of_sexp T.t_of_sexp
-
-    let invariant s =
-      let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
-      let domain, range =
-        Map.fold s ~init:(Set.empty, Set.empty)
-          ~f:(fun ~key ~data (domain, range) ->
-            (* substs are injective *)
-            assert (not (Set.mem range data)) ;
-            (Set.add domain key, Set.add range data) )
-      in
-      assert (Set.disjoint domain range)
-
-    let pp = Map.pp pp_t pp_t
-    let empty = Map.empty
-    let is_empty = Map.is_empty
-
-    let freshen vs ~wrt =
-      let dom = Set.inter wrt vs in
-      ( if Set.is_empty dom then
-        ({sub= empty; dom= Set.empty; rng= Set.empty}, wrt)
-      else
-        let wrt = Set.union wrt vs in
-        let sub, rng, wrt =
-          Set.fold dom ~init:(empty, Set.empty, wrt)
-            ~f:(fun (sub, rng, wrt) x ->
-              let x', wrt = fresh (name x) ~wrt in
-              let sub = Map.add_exn sub ~key:x ~data:x' in
-              let rng = Set.add rng x' in
-              (sub, rng, wrt) )
-        in
-        ({sub; dom; rng}, wrt) )
-      |> check (fun ({sub; _}, _) -> invariant sub)
-
-    let fold sub ~init ~f =
-      Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s)
-
-    let domain sub =
-      Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
-          Set.add domain key )
-
-    let range sub =
-      Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range ->
-          Set.add range data )
-
-    let invert sub =
-      Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
-          Map.add_exn sub' ~key:data ~data:key )
-      |> check invariant
-
-    let restrict sub vs =
-      Map.fold sub ~init:{sub; dom= Set.empty; rng= Set.empty}
-        ~f:(fun ~key ~data z ->
-          if Set.mem vs key then
-            {z with dom= Set.add z.dom key; rng= Set.add z.rng data}
-          else (
-            assert (
-              (* all substs are injective, so the current mapping is the
-                 only one that can cause [data] to be in [rng] *)
-              (not (Set.mem (range (Map.remove sub key)) data))
-              || violates invariant sub ) ;
-            {z with sub= Map.remove z.sub key} ) )
-      |> check (fun {sub; dom; rng} ->
-             assert (Set.equal dom (domain sub)) ;
-             assert (Set.equal rng (range sub)) )
-
-    let apply sub v = Map.find sub v |> Option.value ~default:v
-  end
 end
 
 (** Destruct *)

sledge/src/ses/term.mli

@@ -102,7 +102,11 @@ module Var : sig
   type t = private term [@@deriving compare, equal, sexp]
   type strength = t -> [`Universal | `Existential | `Anonymous] option
 
-  module Map : Map.S with type key := t
+  module Map : sig
+    include Map.S with type key := t
+
+    val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t
+  end
 
   module Set : sig
     include NS.Set.S with type elt := t
@@ -132,23 +136,6 @@ module Var : sig
       variables do not clash with [fresh] variables is to pass the
       [identified] variables to [fresh] in [wrt]:
       [Var.fresh name ~wrt:(Var.Set.of_ (Var.identified ~name ~id))]. *)
-
-  module Subst : sig
-    type var := t
-    type t [@@deriving compare, equal, sexp]
-    type x = {sub: t; dom: Set.t; rng: Set.t}
-
-    val pp : t pp
-    val empty : t
-    val freshen : Set.t -> wrt:Set.t -> x * Set.t
-    val invert : t -> t
-    val restrict : t -> Set.t -> x
-    val is_empty : t -> bool
-    val domain : t -> Set.t
-    val range : t -> Set.t
-    val apply : t -> var -> var
-    val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a
-  end
 end
 
 module Map : sig