From 12752a3e62a53c56753cb58f044cd6d277f19734 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 15:48:38 +0100
Subject: Make minor improvements to printing

---
 src/InterpreterUtils.ml |  2 ++
 src/Invariants.ml       |  5 +++++
 src/Print.ml            | 21 +++++++++++++--------
 3 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 9f6cf495..f0e3d420 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -17,6 +17,8 @@ let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
 
 let ety_to_string = Print.EvalCtxCfimAst.ety_to_string
 
+let rty_to_string = Print.EvalCtxCfimAst.rty_to_string
+
 let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string
 
 let place_to_string = Print.EvalCtxCfimAst.place_to_string
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 05373d1b..be3260be 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -496,6 +496,11 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             match lc with
             | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av)
               -> (
+                L.log#ldebug
+                  (lazy
+                    ("- child_av.ty: "
+                    ^ rty_to_string ctx child_av.V.ty
+                    ^ "\n- aty: " ^ rty_to_string ctx aty));
                 assert (child_av.V.ty = aty);
                 (* Lookup the borrowed value to check it has the proper type *)
                 let glc = lookup_borrow ek_all bid ctx in
diff --git a/src/Print.ml b/src/Print.ml
index f265cacb..e751d0a3 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -419,18 +419,20 @@ module Values = struct
         ^ abstract_shared_borrows_to_string fmt sb
         ^ ")"
 
-  let abs_to_string (fmt : value_formatter) (abs : V.abs) : string =
+  let abs_to_string (fmt : value_formatter) (indent : string)
+      (indent_incr : string) (abs : V.abs) : string =
+    let indent2 = indent ^ indent_incr in
     let avs =
-      List.map (fun av -> "  " ^ typed_avalue_to_string fmt av) abs.avalues
+      List.map (fun av -> indent2 ^ typed_avalue_to_string fmt av) abs.avalues
     in
     let avs = String.concat ",\n" avs in
-    "abs@"
+    indent ^ "abs@"
     ^ V.AbstractionId.to_string abs.abs_id
     ^ "{parents="
     ^ V.AbstractionId.set_to_string abs.parents
     ^ "}" ^ "{regions="
     ^ T.RegionId.set_to_string abs.regions
-    ^ "}" ^ " {\n" ^ avs ^ "\n}"
+    ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
 end
 
 module PV = Values (* local module *)
@@ -442,17 +444,20 @@ module Contexts = struct
     | None -> PV.var_id_to_string bv.index
     | Some name -> name
 
-  let env_elem_to_string (fmt : PV.value_formatter) (ev : C.env_elem) : string =
+  let env_elem_to_string (fmt : PV.value_formatter) (indent : string)
+      (indent_incr : string) (ev : C.env_elem) : string =
     match ev with
     | Var (var, tv) ->
-        binder_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
-    | Abs abs -> PV.abs_to_string fmt abs
+        indent ^ binder_to_string var ^ " -> "
+        ^ 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"
 
   let env_to_string (fmt : PV.value_formatter) (env : C.env) : string =
     "{\n"
     ^ String.concat "\n"
-        (List.map (fun ev -> "  " ^ env_elem_to_string fmt ev) env)
+        (List.map (fun ev -> env_elem_to_string fmt "  " "  " ev) env)
     ^ "\n}"
 
   type ctx_formatter = PV.value_formatter
-- 
cgit v1.2.3