From 8f66a20afe7e5c1c473071720f41198e2111241d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sat, 15 Aug 2020 02:19:15 -0700
Subject: [PATCH] [sledge] Refactor: Expose Context.fold_vars instead of
 fold_terms

Summary: and define fv in terms of it.

Reviewed By: jvillard

Differential Revision: D22571134

fbshipit-source-id: 03c55281f
---
 sledge/src/fol.ml               | 7 ++++---
 sledge/src/fol.mli              | 9 +++++----
 sledge/src/ses/equality.ml      | 2 --
 sledge/src/ses/equality.mli     | 5 +----
 sledge/src/ses/equality_test.ml | 1 +
 sledge/src/sh.ml                | 3 +--
 6 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 693d33fd9..9b44ecda4 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1211,7 +1211,6 @@ module Context = struct
     (vs_of_ses vs', z)
 
   let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
-  let fv x = vs_of_ses (Ses.Equality.fv x)
   let is_true x = Ses.Equality.is_true x
   let is_false x = Ses.Equality.is_false x
   let implies x b = Ses.Equality.implies x (f_to_ses b)
@@ -1221,8 +1220,10 @@ module Context = struct
 
   let normalize x e = ses_map (Ses.Equality.normalize x) e
 
-  let fold_terms ~init x ~f =
-    Ses.Equality.fold_terms x ~init ~f:(fun s e -> f s (of_ses e))
+  let fold_vars ~init x ~f =
+    Ses.Equality.fold_vars x ~init ~f:(fun s v -> f s (v_of_ses v))
+
+  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 
   (* Classes *)
 
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 1c9364341..74b17f80b 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -204,9 +204,6 @@ module Context : sig
   val rename : t -> Var.Subst.t -> t
   (** Apply a renaming substitution to the relation. *)
 
-  val fv : t -> Var.Set.t
-  (** The variables occurring in the terms of the relation. *)
-
   val is_true : t -> bool
   (** Test if the relation is diagonal. *)
 
@@ -230,7 +227,11 @@ module Context : sig
       relation, where [e'] and its subterms are expressed in terms of the
       relation's canonical representatives of each equivalence class. *)
 
-  val fold_terms : init:'a -> t -> f:('a -> Term.t -> 'a) -> 'a
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
+  (** Enumerate the variables occurring in the terms of the context. *)
+
+  val fv : t -> Var.Set.t
+  (** The variables occurring in the terms of the context. *)
 
   (** Solution Substitutions *)
   module Subst : sig
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index 7a8b60d1c..92c53ab52 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -696,8 +696,6 @@ let fold_terms r ~init ~f =
 let fold_vars r ~init ~f =
   fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
-let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
-
 (** Existential Witnessing and Elimination *)
 
 let subst_invariant us s0 s =
diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli
index b945bc197..4b2d63dde 100644
--- a/sledge/src/ses/equality.mli
+++ b/sledge/src/ses/equality.mli
@@ -47,9 +47,6 @@ val orN : Var.Set.t -> t list -> Var.Set.t * t
 val rename : t -> (Var.t -> Var.t) -> t
 (** Apply a renaming substitution to the relation. *)
 
-val fv : t -> Var.Set.t
-(** The variables occurring in the terms of the relation. *)
-
 val is_true : t -> bool
 (** Test if the relation is diagonal. *)
 
@@ -68,7 +65,7 @@ val normalize : t -> Term.t -> Term.t
     relation, where [e'] and its subterms are expressed in terms of the
     relation's canonical representatives of each equivalence class. *)
 
-val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
+val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
 
 (** Solution Substitutions *)
 module Subst : sig
diff --git a/sledge/src/ses/equality_test.ml b/sledge/src/ses/equality_test.ml
index d9b5d8d5d..18802346f 100644
--- a/sledge/src/ses/equality_test.ml
+++ b/sledge/src/ses/equality_test.ml
@@ -53,6 +53,7 @@ let%test_module _ =
     let and_eq a b r = and_eq wrt a b r |> snd
     let and_ r s = and_ wrt r s |> snd
     let or_ r s = or_ wrt r s |> snd
+    let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 
     (* tests *)
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 6cbe90b5d..6dfbbf924 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -81,8 +81,7 @@ let fold_vars_stem ?ignore_ctx {us= _; xs= _; ctx; pure; heap; djns= _}
   |> fun init ->
   Term.fold_vars ~f ~init (Formula.inject pure)
   |> fun init ->
-  if Option.is_some ignore_ctx then init
-  else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init)
+  if Option.is_some ignore_ctx then init else Context.fold_vars ~f ~init ctx
 
 let fold_vars ?ignore_ctx fold_vars q ~init ~f =
   fold_vars_stem ?ignore_ctx ~init ~f q