[sledge] Refactor: Generalize impl of Var over repr and move to separate module

Summary:
Variables are represented as a subtype of terms. The implementation of
the operations on variables is largely independent of this. This diff
generalizes the implementation over the concrete representation, and
moves it to a separate module.

Reviewed By: ngorogiannis

Differential Revision: D23660290

fbshipit-source-id: 90d8c3ca4

sledge/src/ses/term.ml

@@ -221,6 +221,29 @@ let invariant e =
   | _ -> ()
   [@@warning "-9"]
 
+(** Variables are the terms constructed by [Var] *)
+module Var : sig
+  include Var_intf.VAR with type t = private T.t
+
+  val of_ : T.t -> t
+  val of_term : T.t -> t option
+end = struct
+  let invariant x =
+    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+    match x with Var _ -> invariant x | _ -> assert false
+
+  include Var0.Make (struct
+    include T
+
+    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
+  end)
+
+  let of_ v = v |> check invariant
+  let of_term = function Var _ as v -> Some v | _ -> None
+end
+
 (** Pretty-print *)
 
 let rec ppx strength fs term =
@@ -230,14 +253,7 @@ let rec ppx strength fs term =
       Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
     in
     match term with
-    | Var {name; id= -1} -> Trace.pp_styled `Bold "%@%s" fs name
-    | Var {name; id= 0} -> Trace.pp_styled `Bold "%%%s" fs name
-    | Var {name; id} -> (
-      match strength term with
-      | None -> pf "%%%s_%d" name id
-      | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" fs name id
-      | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" fs name id
-      | Some `Anonymous -> Trace.pp_styled `Cyan "_" fs )
+    | Var _ as v -> Var.ppx strength fs (Var.of_ v)
     | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
     | Rational {data} -> Trace.pp_styled `Magenta "%a" fs Q.pp data
     | Float {data} -> pf "%s" data
@@ -311,14 +327,13 @@ and pp_record strength fs elts =
       elts]
 
 let pp = ppx (fun _ -> None)
-let pp_t = pp
 let pp_diff fs (x, y) = Format.fprintf fs "-- %a ++ %a" pp x pp y
 
 (** Construct *)
 
 (* variables *)
 
-let var x = x
+let var v = (v : Var.t :> t)
 
 (* constants *)
 
@@ -1017,49 +1032,6 @@ and of_exp e =
       update ~rcd:(of_exp rcd) ~idx ~elt:(of_exp elt)
   | RecRecord (i, _) -> rec_record i
 
-(** Variables are the terms constructed by [Var] *)
-module Var = struct
-  include T
-
-  let pp = pp
-
-  type strength = t -> [`Universal | `Existential | `Anonymous] option
-
-  let invariant x =
-    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
-    match x with Var _ -> invariant x | _ -> assert false
-
-  let id = function Var v -> v.id | x -> violates invariant x
-  let name = function Var v -> v.name | x -> violates invariant x
-  let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_"
-
-  let of_term = function
-    | Var _ as v -> Some (v |> check invariant)
-    | _ -> None
-
-  let program ~name ~global = Var {name; id= (if global then -1 else 0)}
-
-  let fresh name ~wrt =
-    let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
-    let x' = Var {name; id= max + 1} in
-    (x', Set.add wrt x')
-
-  let identified ~name ~id = Var {name; id}
-
-  module Map = Map
-
-  module Set = struct
-    include Set
-
-    let pp vs = Set.pp pp_t vs
-    let ppx strength vs = Set.pp (ppx strength) vs
-
-    let pp_xs fs xs =
-      if not (is_empty xs) then
-        Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
-  end
-end
-
 (** Destruct *)
 
 let d_int = function Integer {data} -> Some data | _ -> None
@@ -1143,7 +1115,8 @@ let disjuncts e =
   Set.elements (disjuncts_ e)
 
 let rename f e =
-  map_rec_pre e ~f:(function Var _ as v -> Some (f v) | _ -> None)
+  let f = (f : Var.t -> Var.t :> Var.t -> t) in
+  map_rec_pre ~f:(fun e -> Option.map ~f (Var.of_term e)) e
 
 (** Traverse *)
 
@@ -1228,7 +1201,7 @@ let rec fold_terms e ~init:s ~f =
   f s e
 
 let iter_vars e ~f =
-  iter_terms e ~f:(function Var _ as v -> f (v :> Var.t) | _ -> ())
+  iter_terms ~f:(fun e -> Option.iter ~f (Var.of_term e)) e
 
 let exists_vars e ~f =
   with_return (fun {return} ->
@@ -1236,12 +1209,11 @@ let exists_vars e ~f =
       false )
 
 let fold_vars e ~init ~f =
-  fold_terms e ~init ~f:(fun s -> function
-    | Var _ as v -> f s (v :> Var.t) | _ -> s )
+  fold_terms ~f:(fun s e -> Option.fold ~f ~init:s (Var.of_term e)) ~init e
 
 (** Query *)
 
-let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
+let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 let is_true = function Integer {data} -> Z.is_true data | _ -> false
 let is_false = function Integer {data} -> Z.is_false data | _ -> false
 

sledge/src/ses/term.mli

@@ -98,43 +98,12 @@ include module type of T with type t = T.t
 
 (** Term.Var is re-exported as Var *)
 module Var : sig
-  type term := t
-  type t = private term [@@deriving compare, equal, sexp]
-  type strength = t -> [`Universal | `Existential | `Anonymous] option
-
-  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
-
-    val sexp_of_t : t -> Sexp.t
-    val t_of_sexp : Sexp.t -> t
-    val ppx : strength -> t pp
-    val pp : t pp
-    val pp_xs : t pp
-  end
-
-  val pp : t pp
-
-  include Invariant.S with type t := t
-
-  val name : t -> string
-  val id : t -> int
-  val of_ : term -> t
-  val of_term : term -> t option
-  val program : name:string -> global:bool -> t
-  val fresh : string -> wrt:Set.t -> t * Set.t
-
-  val identified : name:string -> id:int -> t
-  (** Variable with the given [id]. Variables are compared by [id] alone,
-      [name] is used only for printing. The only way to ensure [identified]
-      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))]. *)
+  include Var_intf.VAR with type t = private T.t
+
+  val of_ : T.t -> t
+  (** [var (of_ e)] = [e] if [e] matches [Var _], otherwise undefined *)
+
+  val of_term : T.t -> t option
 end
 
 module Map : sig

sledge/src/ses/var0.ml

@@ -0,0 +1,57 @@
+(*
+ * 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
+  include T
+
+  type strength = t -> [`Universal | `Existential | `Anonymous] option
+
+  let ppx strength ppf v =
+    let id = id v in
+    let name = name v in
+    match id with
+    | -1 -> Trace.pp_styled `Bold "%@%s" ppf name
+    | 0 -> Trace.pp_styled `Bold "%%%s" ppf name
+    | _ -> (
+      match strength v with
+      | None -> Format.fprintf ppf "%%%s_%d" name id
+      | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" ppf name id
+      | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" ppf name id
+      | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf )
+
+  let pp = ppx (fun _ -> None)
+
+  module Map = struct
+    include NS.Map.Make (T)
+    include Provide_of_sexp (T)
+  end
+
+  module Set = struct
+    let pp_t = pp
+
+    include NS.Set.Make (T)
+    include Provide_of_sexp (T)
+
+    let ppx strength vs = pp (ppx strength) vs
+    let pp vs = pp pp_t 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 max -> id max in
+    let x' = make ~id:(max + 1) ~name in
+    (x', Set.add wrt x')
+
+  let program ~name ~global = make ~id:(if global then -1 else 0) ~name
+  let identified ~name ~id = make ~id ~name
+end

sledge/src/ses/var0.mli

@@ -0,0 +1,11 @@
+(*
+ * 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 (R : REPR) : VAR with type t = R.t

sledge/src/ses/var_intf.ml

@@ -0,0 +1,50 @@
+(*
+ * 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.
+ *)
+
+module type REPR = sig
+  type t [@@deriving compare, equal, sexp]
+
+  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
+
+  val ppx : strength -> t pp
+  val pp : t pp
+
+  module Map : sig
+    include NS.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
+
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : Sexp.t -> t
+    val ppx : strength -> t pp
+    val pp : t pp
+    val pp_xs : t pp
+  end
+
+  val id : t -> int
+  val name : t -> string
+  val program : name:string -> global:bool -> t
+  val fresh : string -> wrt:Set.t -> t * Set.t
+
+  val identified : name:string -> id:int -> t
+  (** Variable with the given [id]. Variables are compared by [id] alone,
+      [name] is used only for printing. The only way to ensure [identified]
+      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))]. *)
+end