[sledge] Refactor Var0 into Trm.Var and Subst

Reviewed By: ngorogiannis

Differential Revision: D26250525

fbshipit-source-id: 5a61bc4ff

sledge/src/fol/arithmetic.ml

@@ -7,11 +7,10 @@
 
 (** Arithmetic terms *)
 
-open Var_intf
 include Arithmetic_intf
 
 module Representation
-    (Var : VAR)
+    (Var : Var_intf.S)
     (Trm : INDETERMINATE with type var := Var.t) =
 struct
   module Prod = struct

sledge/src/fol/arithmetic.mli

@@ -7,10 +7,9 @@
 
 (** Arithmetic terms *)
 
-open Var_intf
 include module type of Arithmetic_intf
 
 module Representation
-    (Var : VAR)
+    (Var : Var_intf.S)
     (Indeterminate : INDETERMINATE with type var := Var.t) :
   REPRESENTATION with type var := Var.t with type trm := Indeterminate.t

sledge/src/fol/subst.ml

@@ -0,0 +1,78 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Renaming Substitutions: injective maps from variables to variables *)
+
+include Subst_intf
+
+module Make (Var : VAR) = struct
+  module Set = Var.Set
+  module Map = Var.Map
+
+  type t = Var.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 Var.t_of_sexp
+  let pp = Map.pp Var.pp Var.pp
+
+  let invariant s =
+    let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
+    let domain, range =
+      Map.fold s (Set.empty, Set.empty)
+        ~f:(fun ~key ~data (domain, range) ->
+          (* substs are injective *)
+          assert (not (Set.mem data range)) ;
+          (Set.add key domain, Set.add data range) )
+    in
+    assert (Set.disjoint domain range)
+
+  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 (empty, Set.empty, wrt) ~f:(fun x (sub, rng, wrt) ->
+            let x', wrt = Var.freshen x ~wrt in
+            let sub = Map.add_exn ~key:x ~data:x' sub in
+            let rng = Set.add x' rng in
+            (sub, rng, wrt) )
+      in
+      ({sub; dom; rng}, wrt) )
+    |> check (fun ({sub; _}, _) -> invariant sub)
+
+  let fold sub z ~f = Map.fold ~f:(fun ~key ~data -> f key data) sub z
+  let domain sub = Set.of_iter (Map.keys sub)
+  let range sub = Set.of_iter (Map.values sub)
+
+  let invert sub =
+    Map.fold sub empty ~f:(fun ~key ~data sub' ->
+        Map.add_exn ~key:data ~data:key sub' )
+    |> check invariant
+
+  let restrict_dom sub0 vs =
+    Map.fold sub0 {sub= sub0; dom= Set.empty; rng= Set.empty}
+      ~f:(fun ~key ~data z ->
+        let rng = Set.add data z.rng in
+        if Set.mem key vs then {z with dom= Set.add key z.dom; rng}
+        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 data (range (Map.remove key sub0))))
+            || violates invariant sub0 ) ;
+          {z with sub= Map.remove key z.sub; rng} ) )
+    |> check (fun {sub; dom; rng} ->
+           assert (Set.equal dom (domain sub)) ;
+           assert (Set.equal rng (range sub0)) )
+
+  let apply sub v = Map.find v sub |> Option.value ~default:v
+end

sledge/src/fol/subst.mli

@@ -5,7 +5,9 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Var_intf
+(** Renaming Substitutions: injective maps from variables to variables *)
 
-(** Variables, parameterized over their representation *)
+include module type of Subst_intf
-module Make (R : REPR) : VAR with type t = R.t
+
+module Make (Var : VAR) :
+  S with type var := Var.t with type set := Var.Set.t

sledge/src/fol/subst_intf.ml

@@ -0,0 +1,46 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Renaming Substitutions: injective maps from variables to variables *)
+
+module type VAR = sig
+  type t [@@deriving compare, equal, sexp]
+
+  val pp : t pp
+
+  module Map : sig
+    include Map.S with type key := t
+
+    val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t
+  end
+
+  module Set : Set.S with type elt := t
+
+  val freshen : t -> wrt:Set.t -> t * Set.t
+end
+
+module type S = sig
+  type var
+  type set
+  type t [@@deriving compare, equal, sexp]
+  type x = {sub: t; dom: set; rng: set}
+
+  val pp : t pp
+  val empty : t
+  val freshen : set -> wrt:set -> x * set
+  val invert : t -> t
+
+  val restrict_dom : t -> set -> x
+  (** restrict the domain of a substitution to a set, and yield the range of
+      the unrestricted substitution *)
+
+  val is_empty : t -> bool
+  val domain : t -> set
+  val range : t -> set
+  val fold : t -> 's -> f:(var -> var -> 's -> 's) -> 's
+  val apply : t -> var -> var
+end

sledge/src/fol/trm.ml

@@ -54,7 +54,7 @@ and Trm : sig
   module Var1 : sig
     type trm := t
 
-    include Var_intf.VAR with type t = private trm
+    include Var_intf.S with type t = private trm
 
     val of_ : trm -> t
     val of_trm : trm -> t option
@@ -153,9 +153,18 @@ end = struct
 
   let pp = ppx (fun _ -> None)
 
+  (* Define variables as a subtype of terms *)
   module Var1 = struct
+    module V = struct
       module T = struct
         type nonrec t = t [@@deriving compare, equal, sexp]
+        type strength = t -> [`Universal | `Existential | `Anonymous] option
+
+        let pp = pp
+        let ppx = ppx
+      end
+
+      include T
 
       let invariant x =
         let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
@@ -166,14 +175,47 @@ end = struct
       let make ~id ~name = Var {id; name} |> check invariant
       let id = function Var v -> v.id | x -> violates invariant x
       let name = function Var v -> v.name | x -> violates invariant x
+
+      module Set = struct
+        module S = NS.Set.Make (T)
+        include S
+        include Provide_of_sexp (T)
+        include Provide_pp (T)
+
+        let ppx strength vs = S.pp_full (ppx strength) vs
+
+        let pp_xs fs xs =
+          if not (is_empty xs) then
+            Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
       end
 
-    include Var0.Make (T)
+      module Map = struct
+        include NS.Map.Make (T)
+        include Provide_of_sexp (T)
+      end
 
-    let of_ v = v |> check T.invariant
+      let fresh name ~wrt =
+        let max =
+          match Set.max_elt wrt with None -> 0 | Some m -> max 0 (id m)
+        in
+        let x' = make ~id:(max + 1) ~name in
+        (x', Set.add x' wrt)
+
+      let freshen v ~wrt = fresh (name v) ~wrt
+
+      let program ?(name = "") ~id =
+        assert (id > 0) ;
+        make ~id:(-id) ~name
+
+      let identified ~name ~id = make ~id ~name
+      let of_ v = v |> check invariant
       let of_trm = function Var _ as v -> Some v | _ -> None
     end
 
+    include V
+    module Subst = Subst.Make (V)
+  end
+
   let invariant e =
     let@ () = Invariant.invariant [%here] e [%sexp_of: t] in
     match e with

sledge/src/fol/trm.mli

@@ -30,7 +30,7 @@ module Arith : Arithmetic.S with type trm := t with type t = arith
 module Var : sig
   type trm := t
 
-  include Var_intf.VAR with type t = private trm
+  include Var_intf.S with type t = private trm
 
   val of_ : trm -> t
   val of_trm : trm -> t option

sledge/src/fol/var0.ml

@@ -1,129 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open Var_intf
-
-(** Variables, parameterized over their representation *)
-module Make (T : REPR) = struct
-  module T = struct
-    include T
-
-    type strength = t -> [`Universal | `Existential | `Anonymous] option
-
-    let ppx strength ppf v =
-      let id = id v in
-      let name = name v in
-      if id < 0 then Trace.pp_styled `Bold "%%%s!%i" ppf name (-id)
-      else
-        match strength v with
-        | None -> Format.fprintf ppf "%%%s_%i" name id
-        | Some `Universal -> Trace.pp_styled `Bold "%%%s_%i" ppf name id
-        | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%i" ppf name id
-        | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf
-
-    let pp = ppx (fun _ -> None)
-  end
-
-  include T
-
-  module Map = struct
-    include NS.Map.Make (T)
-    include Provide_of_sexp (T)
-  end
-
-  module Set = struct
-    module S = NS.Set.Make (T)
-    include S
-    include Provide_of_sexp (T)
-    include Provide_pp (T)
-
-    let ppx strength vs = S.pp_full (ppx strength) vs
-
-    let pp_xs fs xs =
-      if not (is_empty xs) then
-        Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
-  end
-
-  let fresh name ~wrt =
-    let max =
-      match Set.max_elt wrt with None -> 0 | Some m -> max 0 (id m)
-    in
-    let x' = make ~id:(max + 1) ~name in
-    (x', Set.add x' wrt)
-
-  let program ?(name = "") ~id =
-    assert (id > 0) ;
-    make ~id:(-id) ~name
-
-  let identified ~name ~id = make ~id ~name
-
-  (** 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_of_sexp
-    let pp = Map.pp pp pp
-
-    let invariant s =
-      let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
-      let domain, range =
-        Map.fold s (Set.empty, Set.empty)
-          ~f:(fun ~key ~data (domain, range) ->
-            (* substs are injective *)
-            assert (not (Set.mem data range)) ;
-            (Set.add key domain, Set.add data range) )
-      in
-      assert (Set.disjoint domain range)
-
-    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 (empty, Set.empty, wrt) ~f:(fun x (sub, rng, wrt) ->
-              let x', wrt = fresh (name x) ~wrt in
-              let sub = Map.add_exn ~key:x ~data:x' sub in
-              let rng = Set.add x' rng in
-              (sub, rng, wrt) )
-        in
-        ({sub; dom; rng}, wrt) )
-      |> check (fun ({sub; _}, _) -> invariant sub)
-
-    let fold sub z ~f = Map.fold ~f:(fun ~key ~data -> f key data) sub z
-    let domain sub = Set.of_iter (Map.keys sub)
-    let range sub = Set.of_iter (Map.values sub)
-
-    let invert sub =
-      Map.fold sub empty ~f:(fun ~key ~data sub' ->
-          Map.add_exn ~key:data ~data:key sub' )
-      |> check invariant
-
-    let restrict_dom sub0 vs =
-      Map.fold sub0 {sub= sub0; dom= Set.empty; rng= Set.empty}
-        ~f:(fun ~key ~data z ->
-          let rng = Set.add data z.rng in
-          if Set.mem key vs then {z with dom= Set.add key z.dom; rng}
-          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 data (range (Map.remove key sub0))))
-              || violates invariant sub0 ) ;
-            {z with sub= Map.remove key z.sub; rng} ) )
-      |> check (fun {sub; dom; rng} ->
-             assert (Set.equal dom (domain sub)) ;
-             assert (Set.equal rng (range sub0)) )
-
-    let apply sub v = Map.find v sub |> Option.value ~default:v
-  end
-end

sledge/src/fol/var_intf.ml

@@ -5,15 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module type REPR = sig
+(** Variables *)
-  type t [@@deriving compare, equal, sexp]
+module type S = sig
-
-  val make : id:int -> name:string -> t
-  val id : t -> int
-  val name : t -> string
-end
-
-module type VAR = sig
   type t [@@deriving compare, equal, sexp]
   type strength = t -> [`Universal | `Existential | `Anonymous] option
 
@@ -29,7 +22,6 @@ module type VAR = sig
   module Set : sig
     include NS.Set.S with type elt := t
 
-    val sexp_of_t : t -> Sexp.t
     val t_of_sexp : Sexp.t -> t
     val ppx : strength -> t pp
     val pp : t pp
@@ -54,24 +46,5 @@ module type VAR = sig
       [Var.fresh name ~wrt:(Var.Set.of_ (Var.identified ~name ~id))]. *)
 
   (** Variable renaming substitutions *)
-  module Subst : sig
+  module Subst : Subst.S with type var := t with type set := Set.t
-    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_dom : t -> Set.t -> x
-    (** restrict the domain of a substitution to a set, and yield the range
-        of the unrestricted substitution *)
-
-    val is_empty : t -> bool
-    val domain : t -> Set.t
-    val range : t -> Set.t
-    val fold : t -> 's -> f:(var -> var -> 's -> 's) -> 's
-    val apply : t -> var -> var
-  end
 end