diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterUtils.ml | 2 | ||||
| -rw-r--r-- | src/Invariants.ml | 5 | ||||
| -rw-r--r-- | 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 |