Add more debugging facilities

2 files changed, 26 insertions, 1 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 93629a35..068c175c 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -23,6 +23,8 @@ module L = Logging
 
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
 
+let ety_to_string = Print.EvalCtxCfimAst.ety_to_string
+
 let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string
 
 let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
@@ -952,7 +954,14 @@ let rec access_projection (access : projection_access) (env : C.env)
   | [] ->
       let nv = update v in
       (* Type checking *)
-      assert (nv.ty = v.ty);
+      if nv.ty <> v.ty then (
+        L.log#lerror
+          (lazy
+            ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
+           ^ T.show_ety v.ty));
+        failwith
+          "Assertion failed: new value doesn't have the same type as its \
+           destination");
       Ok (env, { read = v; updated = nv })
   | pe :: p' -> (
       (* Match on the projection element and the value *)
diff --git a/src/Print.ml b/src/Print.ml
index d1bf5f47..9cc7a34c 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -422,6 +422,12 @@ module Contexts = struct
 
   type ctx_formatter = PV.value_formatter
 
+  let ctx_to_etype_formatter (fmt : ctx_formatter) : PT.etype_formatter =
+    PV.value_to_etype_formatter fmt
+
+  let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter =
+    PV.value_to_rtype_formatter fmt
+
   let type_ctx_to_adt_variant_to_string_fun
       (ctx : T.type_def T.TypeDefId.vector) :
       T.TypeDefId.id -> T.VariantId.id -> string =
@@ -914,6 +920,16 @@ end
 
 (** Pretty-printing for ASTs (functions based on an evaluation context) *)
 module EvalCtxCfimAst = struct
+  let ety_to_string (ctx : C.eval_ctx) (t : T.ety) : string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_etype_formatter fmt in
+    PT.ety_to_string fmt t
+
+  let rty_to_string (ctx : C.eval_ctx) (t : T.rty) : string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_rtype_formatter fmt in
+    PT.rty_to_string fmt t
+
   let typed_value_to_string (ctx : C.eval_ctx) (v : V.typed_value) : string =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     PV.typed_value_to_string fmt v