diff options
| -rw-r--r-- | compiler/Interpreter.ml | 2 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 3 | ||||
| -rw-r--r-- | compiler/Print.ml | 40 |
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 = |