summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-11-30 09:50:08 +0100
committerSon Ho2021-11-30 09:50:08 +0100
commitdf564c774866c3aa7316a336b3f48b7cfdeefdcf (patch)
tree93c656d2a4b9cc611c309b7893fd8586976ee39d /src
parent7b686ea3bcabf2178b666e141e773bed923ea55a (diff)
Add more debugging facilities
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml11
-rw-r--r--src/Print.ml16
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