[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

@@ -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]

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. *)