Implement greedy expansion of symbolic variables and expansion before

copy

1 files changed, 9 insertions, 10 deletions

diff --git a/src/Print.ml b/src/Print.ml
index 1eab6714..2b681ec8 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -290,7 +290,7 @@ module Values = struct
       string =
     match lc with
     | SharedLoan (loans, v) ->
-        let loans = V.BorrowId.set_to_string loans in
+        let loans = V.BorrowId.set_to_string None loans in
         "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")"
     | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋"
 
@@ -377,7 +377,7 @@ module Values = struct
         ^ typed_avalue_to_string fmt av
         ^ "⌋"
     | ASharedLoan (loans, v, av) ->
-        let loans = V.BorrowId.set_to_string loans in
+        let loans = V.BorrowId.set_to_string None loans in
         "@shared_loan(" ^ loans ^ ", "
         ^ typed_value_to_string fmt v
         ^ ", "
@@ -443,9 +443,9 @@ module Values = struct
     indent ^ "abs@"
     ^ V.AbstractionId.to_string abs.abs_id
     ^ "{parents="
-    ^ V.AbstractionId.set_to_string abs.parents
+    ^ V.AbstractionId.set_to_string None abs.parents
     ^ "}" ^ "{regions="
-    ^ T.RegionId.set_to_string abs.regions
+    ^ T.RegionId.set_to_string None abs.regions
     ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
 end
 
@@ -462,11 +462,10 @@ module Contexts = struct
       (indent_incr : string) (ev : C.env_elem) : string =
     match ev with
     | Var (var, tv) ->
-        indent
-        ^ option_to_string binder_to_string var
-        ^ " -> "
-        ^ PV.typed_value_to_string fmt tv
-        ^ " ;"
+        let bv =
+          match var with Some var -> binder_to_string var | None -> "_"
+        in
+        indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
     | Abs abs -> PV.abs_to_string fmt indent indent_incr abs
     | Frame -> failwith "Can't print a Frame element"
 
@@ -555,7 +554,7 @@ module Contexts = struct
 
   let eval_ctx_to_string (ctx : C.eval_ctx) : string =
     let fmt = eval_ctx_to_ctx_formatter ctx in
-    let ended_regions = T.RegionId.set_to_string ctx.ended_regions in
+    let ended_regions = T.RegionId.set_to_string None ctx.ended_regions in
     let frames = split_env_according_to_frames ctx.env in
     let num_frames = List.length frames in
     let frames =