diff options
| -rw-r--r-- | src/Interpreter.ml | 11 | ||||
| -rw-r--r-- | src/Print.ml | 16 |
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 |