Add some printing facilities to SymbolicToPure

3 files changed, 70 insertions, 4 deletions

diff --git a/src/Print.ml b/src/Print.ml
index e1834ca6..69feeb6c 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -583,6 +583,11 @@ module PC = Contexts (* local module *)
 
 (** Pretty-printing for contexts (generic functions) *)
 module CfimAst = struct
+  let var_to_string (var : A.var) : string =
+    match var.name with
+    | None -> V.VarId.to_string var.index
+    | Some name -> name
+
   type ast_formatter = {
     rvar_to_string : T.RegionVarId.id -> string;
     r_to_string : T.RegionId.id -> string;
@@ -608,6 +613,9 @@ module CfimAst = struct
       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;
@@ -658,6 +666,48 @@ module CfimAst = struct
       fun_def_id_to_string;
     }
 
+  let fun_def_to_ast_formatter (type_defs : T.type_def T.TypeDefId.Map.t)
+      (fun_defs : A.fun_def A.FunDefId.Map.t) (fdef : A.fun_def) : ast_formatter
+      =
+    let rvar_to_string r =
+      let rvar = T.RegionVarId.nth fdef.signature.region_params r in
+      PT.region_var_to_string rvar
+    in
+    let r_to_string r = PT.region_id_to_string r in
+
+    let type_var_id_to_string vid =
+      let var = T.TypeVarId.nth fdef.signature.type_params vid in
+      PT.type_var_to_string var
+    in
+    let type_def_id_to_string def_id =
+      let def = T.TypeDefId.Map.find def_id type_defs in
+      name_to_string def.name
+    in
+    let adt_variant_to_string =
+      PC.type_ctx_to_adt_variant_to_string_fun type_defs
+    in
+    let var_id_to_string vid =
+      let var = V.VarId.nth fdef.locals vid in
+      var_to_string var
+    in
+    let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_defs in
+    let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_defs in
+    let fun_def_id_to_string def_id =
+      let def = A.FunDefId.Map.find def_id fun_defs in
+      name_to_string def.name
+    in
+    {
+      rvar_to_string;
+      r_to_string;
+      type_var_id_to_string;
+      type_def_id_to_string;
+      adt_variant_to_string;
+      var_id_to_string;
+      adt_field_names;
+      adt_field_to_string;
+      fun_def_id_to_string;
+    }
+
   let rec projection_to_string (fmt : ast_formatter) (inside : string)
       (p : E.projection) : string =
     match p with
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 884c7c8f..1985bfd3 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -190,6 +190,7 @@ type call_info = {
 type bs_ctx = {
   type_context : type_context;
   fun_context : fun_context;
+  fun_def : A.fun_def;
   bid : T.RegionGroupId.id option;  (** TODO: rename *)
   sv_to_var : var V.SymbolicValueId.Map.t;
       (** Whenever we encounter a new symbolic value (introduced because of
@@ -210,6 +211,19 @@ type bs_ctx = {
 }
 (** Body synthesis context *)
 
+(* TODO: move *)
+let bs_ctx_to_value_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter =
+  Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs
+    ctx.fun_context.cfim_fun_defs ctx.fun_def
+
+(* TODO: move *)
+let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
+  let fmt = bs_ctx_to_value_formatter ctx in
+  let fmt = Print.CfimAst.ast_to_value_formatter fmt in
+  let indent = "" in
+  let indent_incr = "  " in
+  Print.Values.abs_to_string fmt indent indent_incr abs
+
 let get_instantiated_fun_sig (fun_id : A.fun_id)
     (back_id : T.RegionGroupId.id option) (tys : ty list) (ctx : bs_ctx) :
     inst_fun_sig =
@@ -692,6 +706,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
     See [typed_avalue_to_consumed].
  *)
 let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
+  log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs));
   List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
 
 (** Explore an abstraction value and convert it to a given back value
@@ -1162,8 +1177,8 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
       let otherwise = translate_expression otherwise ctx in
       Switch (scrutinee, SwitchInt (int_ty, branches, otherwise))
 
-let translate_fun_def (def : A.fun_def) (ctx : bs_ctx) (body : S.expression) :
-    fun_def =
+let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def =
+  let def = ctx.fun_def in
   let bid = ctx.bid in
   log#ldebug
     (lazy
diff --git a/src/Translate.ml b/src/Translate.ml
index ec580258..ce9f085c 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -90,6 +90,7 @@ let translate_function_to_pure (config : C.partial_config)
       var_counter;
       type_context;
       fun_context;
+      fun_def = fdef;
       forward_inputs = [];
       (* Empty for now *)
       backward_inputs = T.RegionGroupId.Map.empty;
@@ -116,7 +117,7 @@ let translate_function_to_pure (config : C.partial_config)
 
   (* Translate the forward function *)
   let pure_forward =
-    SymbolicToPure.translate_fun_def fdef
+    SymbolicToPure.translate_fun_def
       (add_forward_inputs (fst symbolic_forward) ctx)
       (snd symbolic_forward)
   in
@@ -155,7 +156,7 @@ let translate_function_to_pure (config : C.partial_config)
     in
 
     (* Translate *)
-    SymbolicToPure.translate_fun_def fdef ctx symbolic
+    SymbolicToPure.translate_fun_def ctx symbolic
   in
   let pure_backwards =
     List.map translate_backward fdef.signature.regions_hierarchy