summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-06 15:48:38 +0100
committerSon Ho2022-01-06 15:48:38 +0100
commit12752a3e62a53c56753cb58f044cd6d277f19734 (patch)
tree4b6cd96d130d7403dbcbf89ab43d43c1a553300e
parentef7141aab368f682a3846a56624f3c1b90dc445c (diff)
Make minor improvements to printing
Diffstat (limited to '')
-rw-r--r--src/InterpreterUtils.ml2
-rw-r--r--src/Invariants.ml5
-rw-r--r--src/Print.ml21
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