From fe42fc912de352713a34c70a5a92d68918ac02dc Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 15 Jun 2020 15:42:17 -0700
Subject: [PATCH] [sledge] Change: Minor improvement of Sh.extend_us and
 Sh.freshen

Summary: Minor code simplification and optimization of `extend_us` in no-op case.

Reviewed By: jvillard

Differential Revision: D21974021

fbshipit-source-id: a8b12b564
---
 sledge/src/sh.ml  | 20 ++++++++++++--------
 sledge/src/sh.mli |  2 +-
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 34530aac9..0020dd814 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -381,17 +381,21 @@ and freshen_xs q ~wrt =
 
 let extend_us us q =
   let us = Var.Set.union us q.us in
-  let q' = freshen_xs q ~wrt:us in
-  (if us == q.us && q' == q then q else {q' with us}) |> check invariant
+  (if us == q.us then q else {(freshen_xs q ~wrt:us) with us})
+  |> check invariant
 
-let freshen ~wrt q =
+let freshen q ~wrt =
+  [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q]
+  ;
   let xsub, _ = Var.Subst.freshen q.us ~wrt:(Var.Set.union wrt q.xs) in
   let q' = extend_us wrt (rename_ xsub q) in
-  (if q' == q then (q, xsub.sub) else (q', xsub.sub))
-  |> check (fun (q', _) ->
-         invariant q' ;
-         assert (Var.Set.is_subset wrt ~of_:q'.us) ;
-         assert (Var.Set.disjoint wrt (fv q')) )
+  (q', xsub.sub)
+  |>
+  [%Trace.retn fun {pf} (q', _) ->
+    pf "%a" pp q' ;
+    invariant q' ;
+    assert (Var.Set.is_subset wrt ~of_:q'.us) ;
+    assert (Var.Set.disjoint wrt (fv q'))]
 
 let bind_exists q ~wrt =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q]
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 1f36dd55d..9121034e0 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -104,7 +104,7 @@ val subst : Var.Subst.t -> t -> t
 (** Apply a substitution, remove its domain from vocabulary and add its
     range. *)
 
-val freshen : wrt:Var.Set.t -> t -> t * Var.Subst.t
+val freshen : t -> wrt:Var.Set.t -> t * Var.Subst.t
 (** Freshen free variables with respect to [wrt], and extend vocabulary with
     [wrt], renaming bound variables as needed. *)