diff options
| -rw-r--r-- | src/PrintPure.ml | 2 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 22 |
2 files changed, 22 insertions, 2 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 5e9e110a..bf898424 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -437,4 +437,4 @@ let fun_def_to_string (fmt : ast_formatter) (def : fun_def) : string = if inputs = [] then "" else " fun " ^ String.concat " " inputs ^ " ->\n" in let body = expression_to_string fmt " " " " def.body in - "let " ^ name ^ " : " ^ signature ^ " =\n" ^ inputs ^ body + "let " ^ name ^ " :\n " ^ signature ^ " =\n" ^ inputs ^ body diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 63c40f20..420c7eda 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -220,6 +220,14 @@ let type_def_to_string (ctx : bs_ctx) (def : type_def) : string = PrintPure.type_def_to_string fmt def (* TODO: move *) +let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string = + let type_params = ctx.fun_def.signature.type_params in + let type_defs = ctx.type_context.cfim_type_defs in + let fun_defs = ctx.fun_context.cfim_fun_defs in + let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in + PrintPure.typed_rvalue_to_string fmt v + +(* TODO: move *) let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let type_params = sg.type_params in let type_defs = ctx.type_context.cfim_type_defs in @@ -591,6 +599,15 @@ let fresh_vars (tys : ty list) (ctx : bs_ctx) : bs_ctx * var list = let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var +(** Peel boxes as long as the value is of the form `Box<T>` *) +let rec unbox_typed_value (v : V.typed_value) : V.typed_value = + match (v.value, v.ty) with + | V.Adt av, T.Adt (T.Assumed T.Box, _, _) -> ( + match av.field_values with + | [ bv ] -> unbox_typed_value bv + | _ -> failwith "Unreachable") + | _ -> v + (** Translate a typed value. It is used, for instance, on values used as inputs for function calls. @@ -609,6 +626,8 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = *) let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue = + (* We need to ignore boxes *) + let v = unbox_typed_value v in let translate = typed_value_to_rvalue ctx in let value = match v.value with @@ -637,7 +656,8 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue (mk_typed_rvalue_from_var var).value in let ty = ctx_translate_fwd_ty ctx v.ty in - { value; ty } + let value = { value; ty } in + value (** Explore an abstraction value and convert it to a consumed value by collecting all the meta-values from the ended *loans*. |