[sledge] Simplify Sh.pp_us

Summary: Optional arguments no longer needed.

Reviewed By: jvillard

Differential Revision: D25756578

fbshipit-source-id: a207a1ed1

sledge/src/exec.ml

@@ -649,8 +649,7 @@ let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
 let exec_spec_ (xs, pre) (gs, {foot; sub; ms; post}) =
   ([%Trace.call fun {pf} ->
      pf "@[%a@]@ @[<2>%a@,@[<hv>{%a  %a}@;<1 -1>%a--@ {%a  }@]@]" Sh.pp pre
-       (Sh.pp_us ~pre:"@<2>∀ " ())
+       Sh.pp_us gs Sh.pp foot
-       gs Sh.pp foot
        (fun fs sub ->
          if not (Var.Subst.is_empty sub) then
            Format.fprintf fs "∧ %a" Var.Subst.pp sub )

sledge/src/sh.ml

@@ -175,21 +175,21 @@ let pp_heap x ?pre ctx fs heap =
   let blocks = List.group_succ ~eq (List.sort ~cmp heap) in
   List.pp ?pre "@ * " (pp_block x) fs blocks
 
-let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us =
+let pp_us ?vs fs us =
   match vs with
   | None ->
       if not (Var.Set.is_empty us) then
-        [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us]
+        [%Trace.fprintf fs "@<2>∀ @[%a@] .@ " Var.Set.pp us]
   | Some vs ->
       if not (Var.Set.equal vs us) then
         [%Trace.fprintf
-          fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)]
+          fs "@<2>∀ @[%a@] .@ " (Var.Set.pp_diff Var.pp) (vs, us)]
 
 let rec pp_ ?var_strength ?vs ancestor_xs parent_ctx fs
     {us; xs; ctx; pure; heap; djns} =
   Format.pp_open_hvbox fs 0 ;
   let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find v m) var_strength in
-  pp_us ~pre:"@<2>∀ " ?vs () fs us ;
+  pp_us ?vs fs us ;
   ( match djns with
   | [[]] when Option.is_some var_strength -> Format.fprintf fs "false"
   | _ ->
@@ -246,6 +246,8 @@ and pp_djn ?var_strength vs xs ctx fs = function
                sjn ))
         djn
 
+let pp_us fs us = pp_us fs us
+
 let pp_diff_eq ?us ?(xs = Var.Set.empty) ctx fs q =
   pp_ ~var_strength:(var_strength ~xs q) ?vs:us xs ctx fs q
 

sledge/src/sh.mli

@@ -31,7 +31,7 @@ and disjunction = starjunction list
 type t = starjunction [@@deriving compare, equal, sexp]
 
 val pp_seg_norm : Context.t -> seg pp
-val pp_us : ?pre:('a, 'a) fmt -> ?vs:Var.Set.t -> unit -> Var.Set.t pp
+val pp_us : Var.Set.t pp
 val pp : t pp
 val pp_raw : t pp
 val pp_diff_eq : ?us:Var.Set.t -> ?xs:Var.Set.t -> Context.t -> t pp