diff options
| -rw-r--r-- | src/Print.ml | 50 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 19 | ||||
| -rw-r--r-- | src/Translate.ml | 5 |
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 |