Reorganize Print.ml

4 files changed, 279 insertions, 270 deletions

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 0f6ed530..83cdfc9b 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -117,7 +117,7 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
   log#ldebug
     (lazy
       ("primitive_to_typed_value:" ^ "\n- cv: "
-      ^ Print.Values.primitive_value_to_string cv));
+      ^ Print.PrimitiveValues.primitive_value_to_string cv));
   match (ty, cv) with
   (* Scalar, boolean... *)
   | T.Bool, Bool v -> { V.value = V.Primitive (Bool v); ty }
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 52a93a4d..cc25c780 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -164,10 +164,63 @@ module Types = struct
         let variants = String.concat "\n" variants in
         "enum " ^ name ^ params ^ " =\n" ^ variants
     | T.Opaque -> "opaque type " ^ name ^ params
+
+  let type_ctx_to_adt_variant_to_string_fun
+      (ctx : T.type_decl T.TypeDeclId.Map.t) :
+      T.TypeDeclId.id -> T.VariantId.id -> string =
+   fun def_id variant_id ->
+    let def = T.TypeDeclId.Map.find def_id ctx in
+    match def.kind with
+    | Struct _ | Opaque -> failwith "Unreachable"
+    | Enum variants ->
+        let variant = T.VariantId.nth variants variant_id in
+        name_to_string def.name ^ "::" ^ variant.variant_name
+
+  let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) :
+      T.TypeDeclId.id -> T.VariantId.id option -> string list option =
+   fun def_id opt_variant_id ->
+    let def = T.TypeDeclId.Map.find def_id ctx in
+    let fields = TU.type_decl_get_fields def opt_variant_id in
+    (* There are two cases: either all the fields have names, or none of them
+     * has names *)
+    let has_names =
+      List.exists (fun f -> Option.is_some f.T.field_name) fields
+    in
+    if has_names then
+      let fields = List.map (fun f -> Option.get f.T.field_name) fields in
+      Some fields
+    else None
+
+  let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t)
+      :
+      T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option
+      =
+   fun def_id opt_variant_id field_id ->
+    let def = T.TypeDeclId.Map.find def_id ctx in
+    let fields = TU.type_decl_get_fields def opt_variant_id in
+    let field = T.FieldId.nth fields field_id in
+    field.T.field_name
 end
 
 module PT = Types (* local module *)
 
+(** Pretty-printing for primitive values *)
+module PrimitiveValues = struct
+  let big_int_to_string (bi : V.big_int) : string = Z.to_string bi
+
+  let scalar_value_to_string (sv : V.scalar_value) : string =
+    big_int_to_string sv.value ^ ": " ^ PT.integer_type_to_string sv.int_ty
+
+  let primitive_value_to_string (cv : V.primitive_value) : string =
+    match cv with
+    | Scalar sv -> scalar_value_to_string sv
+    | Bool b -> Bool.to_string b
+    | Char c -> String.make 1 c
+    | String s -> s
+end
+
+module PPV = PrimitiveValues (* local module *)
+
 (** Pretty-printing for values *)
 module Values = struct
   type value_formatter = {
@@ -205,18 +258,6 @@ module Values = struct
   let var_id_to_string (id : V.VarId.id) : string =
     "var@" ^ V.VarId.to_string id
 
-  let big_int_to_string (bi : V.big_int) : string = Z.to_string bi
-
-  let scalar_value_to_string (sv : V.scalar_value) : string =
-    big_int_to_string sv.value ^ ": " ^ PT.integer_type_to_string sv.int_ty
-
-  let primitive_value_to_string (cv : V.primitive_value) : string =
-    match cv with
-    | Scalar sv -> scalar_value_to_string sv
-    | Bool b -> Bool.to_string b
-    | Char c -> String.make 1 c
-    | String s -> s
-
   let symbolic_value_id_to_string (id : V.SymbolicValueId.id) : string =
     "s@" ^ V.SymbolicValueId.to_string id
 
@@ -240,7 +281,7 @@ module Values = struct
       string =
     let ty_fmt : PT.etype_formatter = value_to_etype_formatter fmt in
     match v.value with
-    | Primitive cv -> primitive_value_to_string cv
+    | Primitive cv -> PPV.primitive_value_to_string cv
     | Adt av -> (
         let field_values =
           List.map (typed_value_to_string fmt) av.field_values
@@ -352,7 +393,7 @@ module Values = struct
       string =
     let ty_fmt : PT.rtype_formatter = value_to_rtype_formatter fmt in
     match v.value with
-    | APrimitive cv -> primitive_value_to_string cv
+    | APrimitive cv -> PPV.primitive_value_to_string cv
     | AAdt av -> (
         let field_values =
           List.map (typed_avalue_to_string fmt) av.field_values
@@ -481,193 +522,7 @@ end
 
 module PV = Values (* local module *)
 
-(** Pretty-printing for contexts *)
-module Contexts = struct
-  let binder_to_string (bv : C.binder) : string =
-    match bv.name with
-    | None -> PV.var_id_to_string bv.index
-    | Some name -> name
-
-  let env_elem_to_string (fmt : PV.value_formatter) (indent : string)
-      (indent_incr : string) (ev : C.env_elem) : string =
-    match ev with
-    | Var (var, tv) ->
-        let bv =
-          match var with Some var -> binder_to_string var | None -> "_"
-        in
-        indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
-    | Abs abs -> PV.abs_to_string fmt indent indent_incr abs
-    | Frame -> failwith "Can't print a Frame element"
-
-  let opt_env_elem_to_string (fmt : PV.value_formatter) (indent : string)
-      (indent_incr : string) (ev : C.env_elem option) : string =
-    match ev with
-    | None -> indent ^ "..."
-    | Some ev -> env_elem_to_string fmt indent indent_incr ev
-
-  (** Filters "dummy" bindings from an environment, to gain space and clarity/
-      See [env_to_string]. *)
-  let filter_env (env : C.env) : C.env_elem option list =
-    (* We filter:
-     * - non-dummy bindings which point to ⊥
-     * - dummy bindings which don't contain loans nor borrows
-     * Note that the first case can sometimes be confusing: we may try to improve
-     * it...
-     *)
-    let filter_elem (ev : C.env_elem) : C.env_elem option =
-      match ev with
-      | Var (Some _, tv) ->
-          (* Not a dummy binding: check if the value is ⊥ *)
-          if VU.is_bottom tv.value then None else Some ev
-      | Var (None, tv) ->
-          (* Dummy binding: check if the value contains borrows or loans *)
-          if VU.borrows_in_value tv || VU.loans_in_value tv then Some ev
-          else None
-      | _ -> Some ev
-    in
-    let env = List.map filter_elem env in
-    (* We collapse groups of filtered values - so that we can print one
-     * single "..." for a whole group of filtered values *)
-    let rec group_filtered (env : C.env_elem option list) :
-        C.env_elem option list =
-      match env with
-      | [] -> []
-      | None :: None :: env -> group_filtered (None :: env)
-      | x :: env -> x :: group_filtered env
-    in
-    group_filtered env
-
-  (** 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.
-   *)
-  let env_to_string (filter : bool) (fmt : PV.value_formatter) (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 "  " "  " ev) env)
-    ^ "\n}"
-
-  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_decl T.TypeDeclId.Map.t) :
-      T.TypeDeclId.id -> T.VariantId.id -> string =
-   fun def_id variant_id ->
-    let def = T.TypeDeclId.Map.find def_id ctx in
-    match def.kind with
-    | Struct _ | Opaque -> failwith "Unreachable"
-    | Enum variants ->
-        let variant = T.VariantId.nth variants variant_id in
-        name_to_string def.name ^ "::" ^ variant.variant_name
-
-  let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) :
-      T.TypeDeclId.id -> T.VariantId.id option -> string list option =
-   fun def_id opt_variant_id ->
-    let def = T.TypeDeclId.Map.find def_id ctx in
-    let fields = TU.type_decl_get_fields def opt_variant_id in
-    (* There are two cases: either all the fields have names, or none of them
-     * has names *)
-    let has_names =
-      List.exists (fun f -> Option.is_some f.T.field_name) fields
-    in
-    if has_names then
-      let fields = List.map (fun f -> Option.get f.T.field_name) fields in
-      Some fields
-    else None
-
-  let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
-    (* We shouldn't use rvar_to_string *)
-    let rvar_to_string _r = failwith "Unexpected use of rvar_to_string" in
-    let r_to_string r = PT.region_id_to_string r in
-
-    let type_var_id_to_string vid =
-      let v = C.lookup_type_var ctx vid in
-      v.name
-    in
-    let type_decl_id_to_string def_id =
-      let def = C.ctx_lookup_type_decl ctx def_id in
-      name_to_string def.name
-    in
-    let adt_variant_to_string =
-      type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
-    in
-    let var_id_to_string vid =
-      let bv = C.ctx_lookup_binder ctx vid in
-      binder_to_string bv
-    in
-    let adt_field_names =
-      type_ctx_to_adt_field_names_fun ctx.type_context.type_decls
-    in
-    {
-      rvar_to_string;
-      r_to_string;
-      type_var_id_to_string;
-      type_decl_id_to_string;
-      adt_variant_to_string;
-      var_id_to_string;
-      adt_field_names;
-    }
-
-  (** Split an [env] at every occurrence of [Frame], eliminating those elements.
-          Also reorders the frames and the values in the frames according to the
-          following order:
-          * frames: from the current frame to the first pushed (oldest frame)
-          * values: from the first pushed (oldest) to the last pushed
-       *)
-  let split_env_according_to_frames (env : C.env) : C.env list =
-    let rec split_aux (frames : C.env list) (curr_frame : C.env) (env : C.env) =
-      match env with
-      | [] ->
-          if List.length curr_frame > 0 then curr_frame :: frames else frames
-      | Frame :: env' -> split_aux (curr_frame :: frames) [] env'
-      | ev :: env' -> split_aux frames (ev :: curr_frame) env'
-    in
-    let frames = split_aux [] [] env in
-    frames
-
-  let eval_ctx_to_string (ctx : C.eval_ctx) : string =
-    let fmt = eval_ctx_to_ctx_formatter ctx in
-    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
-    let frames =
-      List.mapi
-        (fun i f ->
-          let num_bindings = ref 0 in
-          let num_dummies = ref 0 in
-          let num_abs = ref 0 in
-          List.iter
-            (fun ev ->
-              match ev with
-              | C.Var (None, _) -> num_dummies := !num_abs + 1
-              | C.Var (Some _, _) -> num_bindings := !num_bindings + 1
-              | C.Abs _ -> num_abs := !num_abs + 1
-              | _ -> raise (Failure "Unreachable"))
-            f;
-          "\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: "
-          ^ string_of_int !num_bindings
-          ^ "\n- dummy bindings: " ^ string_of_int !num_dummies
-          ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n"
-          ^ env_to_string true fmt f ^ "\n")
-        frames
-    in
-    "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
-    ^ " frame(s)\n" ^ String.concat "" frames
-end
-
-module PC = Contexts (* local module *)
-
-(** Pretty-printing for contexts (generic functions) *)
+(** Pretty-printing for LLBC AST (generic functions) *)
 module LlbcAst = struct
   let var_to_string (var : A.var) : string =
     match var.name with
@@ -689,20 +544,6 @@ module LlbcAst = struct
     global_decl_id_to_string : A.GlobalDeclId.id -> string;
   }
 
-  let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
-    {
-      PV.rvar_to_string = fmt.rvar_to_string;
-      PV.r_to_string = fmt.r_to_string;
-      PV.type_var_id_to_string = fmt.type_var_id_to_string;
-      PV.type_decl_id_to_string = fmt.type_decl_id_to_string;
-      PV.adt_variant_to_string = fmt.adt_variant_to_string;
-      PV.var_id_to_string = fmt.var_id_to_string;
-      PV.adt_field_names = fmt.adt_field_names;
-    }
-
-  let ast_to_value_formatter (fmt : ast_formatter) : PV.value_formatter =
-    ast_to_ctx_formatter fmt
-
   let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter =
     {
       PT.r_to_string = PT.erased_region_to_string;
@@ -724,42 +565,6 @@ module LlbcAst = struct
       PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
-  let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t)
-      :
-      T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option
-      =
-   fun def_id opt_variant_id field_id ->
-    let def = T.TypeDeclId.Map.find def_id ctx in
-    let fields = TU.type_decl_get_fields def opt_variant_id in
-    let field = T.FieldId.nth fields field_id in
-    field.T.field_name
-
-  let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : ast_formatter =
-    let ctx_fmt = PC.eval_ctx_to_ctx_formatter ctx in
-    let adt_field_to_string =
-      type_ctx_to_adt_field_to_string_fun ctx.type_context.type_decls
-    in
-    let fun_decl_id_to_string def_id =
-      let def = C.ctx_lookup_fun_decl ctx def_id in
-      fun_name_to_string def.name
-    in
-    let global_decl_id_to_string def_id =
-      let def = C.ctx_lookup_global_decl ctx def_id in
-      global_name_to_string def.name
-    in
-    {
-      rvar_to_string = ctx_fmt.PV.rvar_to_string;
-      r_to_string = ctx_fmt.PV.r_to_string;
-      type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string;
-      type_decl_id_to_string = ctx_fmt.PV.type_decl_id_to_string;
-      adt_variant_to_string = ctx_fmt.PV.adt_variant_to_string;
-      var_id_to_string = ctx_fmt.PV.var_id_to_string;
-      adt_field_names = ctx_fmt.PV.adt_field_names;
-      adt_field_to_string;
-      fun_decl_id_to_string;
-      global_decl_id_to_string;
-    }
-
   let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
       (fun_decls : A.fun_decl A.FunDeclId.Map.t)
       (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) :
@@ -779,14 +584,16 @@ module LlbcAst = struct
       name_to_string def.name
     in
     let adt_variant_to_string =
-      PC.type_ctx_to_adt_variant_to_string_fun type_decls
+      PT.type_ctx_to_adt_variant_to_string_fun type_decls
     in
     let var_id_to_string vid =
       let var = V.VarId.nth (Option.get fdef.body).locals vid in
       var_to_string var
     in
-    let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in
-    let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in
+    let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_decls in
+    let adt_field_to_string =
+      PT.type_ctx_to_adt_field_to_string_fun type_decls
+    in
     let fun_decl_id_to_string def_id =
       let def = A.FunDeclId.Map.find def_id fun_decls in
       fun_name_to_string def.name
@@ -877,7 +684,7 @@ module LlbcAst = struct
     | E.Move p -> "move " ^ place_to_string fmt p
     | E.Constant (ty, cv) ->
         "("
-        ^ PV.primitive_value_to_string cv
+        ^ PPV.primitive_value_to_string cv
         ^ " : "
         ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
         ^ ")"
@@ -1024,7 +831,9 @@ module LlbcAst = struct
               List.map
                 (fun (svl, be) ->
                   let svl =
-                    List.map (fun sv -> "| " ^ PV.scalar_value_to_string sv) svl
+                    List.map
+                      (fun sv -> "| " ^ PPV.scalar_value_to_string sv)
+                      svl
                   in
                   let svl = String.concat " " svl in
                   indent1 ^ svl ^ " => {\n" ^ inner_to_string2 be ^ "\n"
@@ -1120,6 +929,206 @@ end
 
 module PA = LlbcAst (* local module *)
 
+(** Pretty-printing for contexts *)
+module Contexts = struct
+  let binder_to_string (bv : C.binder) : string =
+    match bv.name with
+    | None -> PV.var_id_to_string bv.index
+    | Some name -> name
+
+  let env_elem_to_string (fmt : PV.value_formatter) (indent : string)
+      (indent_incr : string) (ev : C.env_elem) : string =
+    match ev with
+    | Var (var, tv) ->
+        let bv =
+          match var with Some var -> binder_to_string var | None -> "_"
+        in
+        indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
+    | Abs abs -> PV.abs_to_string fmt indent indent_incr abs
+    | Frame -> failwith "Can't print a Frame element"
+
+  let opt_env_elem_to_string (fmt : PV.value_formatter) (indent : string)
+      (indent_incr : string) (ev : C.env_elem option) : string =
+    match ev with
+    | None -> indent ^ "..."
+    | Some ev -> env_elem_to_string fmt indent indent_incr ev
+
+  (** Filters "dummy" bindings from an environment, to gain space and clarity/
+      See [env_to_string]. *)
+  let filter_env (env : C.env) : C.env_elem option list =
+    (* We filter:
+     * - non-dummy bindings which point to ⊥
+     * - dummy bindings which don't contain loans nor borrows
+     * Note that the first case can sometimes be confusing: we may try to improve
+     * it...
+     *)
+    let filter_elem (ev : C.env_elem) : C.env_elem option =
+      match ev with
+      | Var (Some _, tv) ->
+          (* Not a dummy binding: check if the value is ⊥ *)
+          if VU.is_bottom tv.value then None else Some ev
+      | Var (None, tv) ->
+          (* Dummy binding: check if the value contains borrows or loans *)
+          if VU.borrows_in_value tv || VU.loans_in_value tv then Some ev
+          else None
+      | _ -> Some ev
+    in
+    let env = List.map filter_elem env in
+    (* We collapse groups of filtered values - so that we can print one
+     * single "..." for a whole group of filtered values *)
+    let rec group_filtered (env : C.env_elem option list) :
+        C.env_elem option list =
+      match env with
+      | [] -> []
+      | None :: None :: env -> group_filtered (None :: env)
+      | x :: env -> x :: group_filtered env
+    in
+    group_filtered env
+
+  (** 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.
+   *)
+  let env_to_string (filter : bool) (fmt : PV.value_formatter) (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 "  " "  " ev) env)
+    ^ "\n}"
+
+  type ctx_formatter = PV.value_formatter
+
+  let ast_to_ctx_formatter (fmt : PA.ast_formatter) : ctx_formatter =
+    {
+      PV.rvar_to_string = fmt.rvar_to_string;
+      PV.r_to_string = fmt.r_to_string;
+      PV.type_var_id_to_string = fmt.type_var_id_to_string;
+      PV.type_decl_id_to_string = fmt.type_decl_id_to_string;
+      PV.adt_variant_to_string = fmt.adt_variant_to_string;
+      PV.var_id_to_string = fmt.var_id_to_string;
+      PV.adt_field_names = fmt.adt_field_names;
+    }
+
+  let ast_to_value_formatter (fmt : PA.ast_formatter) : PV.value_formatter =
+    ast_to_ctx_formatter fmt
+
+  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 eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
+    (* We shouldn't use rvar_to_string *)
+    let rvar_to_string _r = failwith "Unexpected use of rvar_to_string" in
+    let r_to_string r = PT.region_id_to_string r in
+
+    let type_var_id_to_string vid =
+      let v = C.lookup_type_var ctx vid in
+      v.name
+    in
+    let type_decl_id_to_string def_id =
+      let def = C.ctx_lookup_type_decl ctx def_id in
+      name_to_string def.name
+    in
+    let adt_variant_to_string =
+      PT.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
+    in
+    let var_id_to_string vid =
+      let bv = C.ctx_lookup_binder ctx vid in
+      binder_to_string bv
+    in
+    let adt_field_names =
+      PT.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls
+    in
+    {
+      rvar_to_string;
+      r_to_string;
+      type_var_id_to_string;
+      type_decl_id_to_string;
+      adt_variant_to_string;
+      var_id_to_string;
+      adt_field_names;
+    }
+
+  let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : PA.ast_formatter =
+    let ctx_fmt = eval_ctx_to_ctx_formatter ctx in
+    let adt_field_to_string =
+      PT.type_ctx_to_adt_field_to_string_fun ctx.type_context.type_decls
+    in
+    let fun_decl_id_to_string def_id =
+      let def = C.ctx_lookup_fun_decl ctx def_id in
+      fun_name_to_string def.name
+    in
+    let global_decl_id_to_string def_id =
+      let def = C.ctx_lookup_global_decl ctx def_id in
+      global_name_to_string def.name
+    in
+    {
+      rvar_to_string = ctx_fmt.PV.rvar_to_string;
+      r_to_string = ctx_fmt.PV.r_to_string;
+      type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string;
+      type_decl_id_to_string = ctx_fmt.PV.type_decl_id_to_string;
+      adt_variant_to_string = ctx_fmt.PV.adt_variant_to_string;
+      var_id_to_string = ctx_fmt.PV.var_id_to_string;
+      adt_field_names = ctx_fmt.PV.adt_field_names;
+      adt_field_to_string;
+      fun_decl_id_to_string;
+      global_decl_id_to_string;
+    }
+
+  (** Split an [env] at every occurrence of [Frame], eliminating those elements.
+          Also reorders the frames and the values in the frames according to the
+          following order:
+          * frames: from the current frame to the first pushed (oldest frame)
+          * values: from the first pushed (oldest) to the last pushed
+       *)
+  let split_env_according_to_frames (env : C.env) : C.env list =
+    let rec split_aux (frames : C.env list) (curr_frame : C.env) (env : C.env) =
+      match env with
+      | [] ->
+          if List.length curr_frame > 0 then curr_frame :: frames else frames
+      | Frame :: env' -> split_aux (curr_frame :: frames) [] env'
+      | ev :: env' -> split_aux frames (ev :: curr_frame) env'
+    in
+    let frames = split_aux [] [] env in
+    frames
+
+  let eval_ctx_to_string (ctx : C.eval_ctx) : string =
+    let fmt = eval_ctx_to_ctx_formatter ctx in
+    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
+    let frames =
+      List.mapi
+        (fun i f ->
+          let num_bindings = ref 0 in
+          let num_dummies = ref 0 in
+          let num_abs = ref 0 in
+          List.iter
+            (fun ev ->
+              match ev with
+              | C.Var (None, _) -> num_dummies := !num_abs + 1
+              | C.Var (Some _, _) -> num_bindings := !num_bindings + 1
+              | C.Abs _ -> num_abs := !num_abs + 1
+              | _ -> raise (Failure "Unreachable"))
+            f;
+          "\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: "
+          ^ string_of_int !num_bindings
+          ^ "\n- dummy bindings: " ^ string_of_int !num_dummies
+          ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n"
+          ^ env_to_string true fmt f ^ "\n")
+        frames
+    in
+    "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
+    ^ " frame(s)\n" ^ String.concat "" frames
+end
+
+module PC = Contexts (* local module *)
+
 (** Pretty-printing for ASTs (functions based on a definition context) *)
 module Module = struct
   (** This function pretty-prints a type definition by using a definition
@@ -1167,12 +1176,12 @@ module Module = struct
       PA.var_to_string var
     in
     let adt_variant_to_string =
-      PC.type_ctx_to_adt_variant_to_string_fun type_context
+      PT.type_ctx_to_adt_variant_to_string_fun type_context
     in
     let adt_field_to_string =
-      PA.type_ctx_to_adt_field_to_string_fun type_context
+      PT.type_ctx_to_adt_field_to_string_fun type_context
     in
-    let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_context in
+    let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_context in
     {
       rvar_to_string;
       r_to_string;
@@ -1269,15 +1278,15 @@ module EvalCtxLlbcAst = struct
     PV.typed_avalue_to_string fmt v
 
   let place_to_string (ctx : C.eval_ctx) (op : E.place) : string =
-    let fmt = PA.eval_ctx_to_ast_formatter ctx in
+    let fmt = PC.eval_ctx_to_ast_formatter ctx in
     PA.place_to_string fmt op
 
   let operand_to_string (ctx : C.eval_ctx) (op : E.operand) : string =
-    let fmt = PA.eval_ctx_to_ast_formatter ctx in
+    let fmt = PC.eval_ctx_to_ast_formatter ctx in
     PA.operand_to_string fmt op
 
   let statement_to_string (ctx : C.eval_ctx) (indent : string)
       (indent_incr : string) (e : A.statement) : string =
-    let fmt = PA.eval_ctx_to_ast_formatter ctx in
+    let fmt = PC.eval_ctx_to_ast_formatter ctx in
     PA.statement_to_string fmt indent indent_incr e
 end
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 6fafa0a3..67353547 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -56,7 +56,7 @@ let global_name_to_string = Print.global_name_to_string
 let option_to_string = Print.option_to_string
 let type_var_to_string = Print.Types.type_var_to_string
 let integer_type_to_string = Print.Types.integer_type_to_string
-let scalar_value_to_string = Print.Values.scalar_value_to_string
+let scalar_value_to_string = Print.PrimitiveValues.scalar_value_to_string
 
 let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     (type_params : type_var list) : type_formatter =
@@ -89,17 +89,17 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     name_to_string def.name
   in
   let adt_variant_to_string =
-    Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_decls
+    Print.Types.type_ctx_to_adt_variant_to_string_fun type_decls
   in
   let var_id_to_string vid =
     (* TODO: somehow lookup in the context *)
     "^" ^ VarId.to_string vid
   in
   let adt_field_names =
-    Print.Contexts.type_ctx_to_adt_field_names_fun type_decls
+    Print.Types.type_ctx_to_adt_field_names_fun type_decls
   in
   let adt_field_to_string =
-    Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls
+    Print.Types.type_ctx_to_adt_field_to_string_fun type_decls
   in
   let fun_decl_id_to_string def_id =
     let def = FunDeclId.Map.find def_id fun_decls in
@@ -357,7 +357,7 @@ let adt_g_value_to_string (fmt : value_formatter)
 let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
     string =
   match v.value with
-  | PatConstant cv -> Print.Values.primitive_value_to_string cv
+  | PatConstant cv -> Print.PrimitiveValues.primitive_value_to_string cv
   | PatVar (v, None) -> var_to_string (ast_to_type_formatter fmt) v
   | PatVar (v, Some mp) ->
       let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
@@ -436,7 +436,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
   | Var var_id ->
       let s = fmt.var_id_to_string var_id in
       if inside then "(" ^ s ^ ")" else s
-  | Const cv -> Print.Values.primitive_value_to_string cv
+  | Const cv -> Print.PrimitiveValues.primitive_value_to_string cv
   | App _ ->
       (* Recursively destruct the app, to have a pair (app, arguments list) *)
       let app, args = destruct_apps e in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 749eae1d..f393b059 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -197,7 +197,7 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
 (* TODO: move *)
 let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   let fmt = bs_ctx_to_ast_formatter ctx in
-  let fmt = Print.LlbcAst.ast_to_value_formatter fmt in
+  let fmt = Print.Contexts.ast_to_value_formatter fmt in
   let indent = "" in
   let indent_incr = "  " in
   Print.Values.abs_to_string fmt indent indent_incr abs