Make minor modifications

3 files changed, 29 insertions, 16 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index dc2bb700..449463c8 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -157,7 +157,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       ^ "\n- inside_loop: "
       ^ Print.bool_to_string inside_loop
       ^ "\n- ctx:\n"
-      ^ Print.Contexts.eval_ctx_to_string_gen true true ctx));
+      ^ Print.Contexts.eval_ctx_to_string ctx));
   (* We need to instantiate the function signature - to retrieve
    * the return type. Note that it is important to re-generate
    * an instantiation of the signature, so that we use fresh
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index a726eda0..e73c09c4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -456,6 +456,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 List.iter
                   (fun (v : V.typed_value) -> assert (v.ty = vec_ty))
                   fvs
+            | T.Range, [ v0; v1 ], [], [ inner_ty ], [] ->
+                assert (v0.V.ty = inner_ty);
+                assert (v1.V.ty = inner_ty)
             | (T.Array | T.Slice | T.Str), _, _, _, _ ->
                 raise (Failure "Unexpected")
             | _ -> raise (Failure "Erroneous type"))
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 410b45e6..7d7e8549 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -124,6 +124,7 @@ module Values = struct
                   assert (field_values = []);
                   "@Option::None")
                 else raise (Failure "Unreachable")
+            | Range, _ -> "@Range{ " ^ String.concat ", " field_values ^ "}"
             | Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]"
             | _ -> raise (Failure "Inconsistent value"))
         | _ -> raise (Failure "Inconsistent typed value"))
@@ -362,20 +363,27 @@ module Contexts = struct
     | DummyBinder bid -> dummy_var_id_to_string bid
 
   let env_elem_to_string (fmt : PV.value_formatter) (verbose : bool)
-      (indent : string) (indent_incr : string) (ev : C.env_elem) : string =
+      (with_var_types : bool) (indent : string) (indent_incr : string)
+      (ev : C.env_elem) : string =
     match ev with
     | Var (var, tv) ->
         let bv = binder_to_string var in
-        indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
+        let ty =
+          if with_var_types then
+            " : " ^ PT.ty_to_string (PV.value_to_etype_formatter fmt) tv.V.ty
+          else ""
+        in
+        indent ^ bv ^ ty ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
     | Abs abs -> PV.abs_to_string fmt verbose indent indent_incr abs
     | Frame -> raise (Failure "Can't print a Frame element")
 
   let opt_env_elem_to_string (fmt : PV.value_formatter) (verbose : bool)
-      (indent : string) (indent_incr : string) (ev : C.env_elem option) : string
-      =
+      (with_var_types : bool) (indent : string) (indent_incr : string)
+      (ev : C.env_elem option) : string =
     match ev with
     | None -> indent ^ "..."
-    | Some ev -> env_elem_to_string fmt verbose indent indent_incr ev
+    | Some ev ->
+        env_elem_to_string fmt verbose with_var_types indent indent_incr ev
 
   (** Filters "dummy" bindings from an environment, to gain space and clarity/
       See [env_to_string]. *)
@@ -412,16 +420,18 @@ module Contexts = struct
   (** Environments can have a lot of dummy or uninitialized values: [filter]
       allows to filter them when printing, replacing groups of such bindings with
       "..." to gain space and clarity.
+      [with_var_types]: if true, print the type of the variables
    *)
   let env_to_string (filter : bool) (fmt : PV.value_formatter) (verbose : bool)
-      (env : C.env) : string =
+      (with_var_types : bool) (env : C.env) : string =
     let env =
       if filter then filter_env env else List.map (fun ev -> Some ev) env
     in
     "{\n"
     ^ String.concat "\n"
         (List.map
-           (fun ev -> opt_env_elem_to_string fmt verbose "  " "  " ev)
+           (fun ev ->
+             opt_env_elem_to_string fmt verbose with_var_types "  " "  " ev)
            env)
     ^ "\n}"
 
@@ -539,7 +549,7 @@ module Contexts = struct
     frames
 
   let fmt_eval_ctx_to_string_gen (fmt : ctx_formatter) (verbose : bool)
-      (filter : bool) (ctx : C.eval_ctx) : string =
+      (filter : bool) (with_var_types : bool) (ctx : C.eval_ctx) : string =
     let ended_regions = T.RegionId.Set.to_string None ctx.ended_regions in
     let frames = split_env_according_to_frames ctx.env in
     let num_frames = List.length frames in
@@ -561,23 +571,23 @@ module Contexts = struct
           ^ string_of_int !num_bindings
           ^ "\n- dummy bindings: " ^ string_of_int !num_dummies
           ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n"
-          ^ env_to_string filter fmt verbose f
+          ^ env_to_string filter fmt verbose with_var_types f
           ^ "\n")
         frames
     in
     "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
     ^ " frame(s)\n" ^ String.concat "" frames
 
-  let eval_ctx_to_string_gen (verbose : bool) (filter : bool) (ctx : C.eval_ctx)
-      : string =
+  let eval_ctx_to_string_gen (verbose : bool) (filter : bool)
+      (with_var_types : bool) (ctx : C.eval_ctx) : string =
     let fmt = eval_ctx_to_ctx_formatter ctx in
-    fmt_eval_ctx_to_string_gen fmt verbose filter ctx
+    fmt_eval_ctx_to_string_gen fmt verbose filter with_var_types ctx
 
   let eval_ctx_to_string (ctx : C.eval_ctx) : string =
-    eval_ctx_to_string_gen false true ctx
+    eval_ctx_to_string_gen false true true ctx
 
   let eval_ctx_to_string_no_filter (ctx : C.eval_ctx) : string =
-    eval_ctx_to_string_gen false false ctx
+    eval_ctx_to_string_gen false false true ctx
 end
 
 module PC = Contexts (* local module *)
@@ -647,7 +657,7 @@ module EvalCtxLlbcAst = struct
   let env_elem_to_string (ctx : C.eval_ctx) (indent : string)
       (indent_incr : string) (ev : C.env_elem) : string =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
-    PC.env_elem_to_string fmt false indent indent_incr ev
+    PC.env_elem_to_string fmt false true indent indent_incr ev
 
   let abs_to_string (ctx : C.eval_ctx) (indent : string) (indent_incr : string)
       (abs : V.abs) : string =