From 46390b3ea190b6307c87f10df1c375d5b30c6b52 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Jan 2022 15:51:57 +0100
Subject: Fix some mistakes

---
 src/PrintPure.ml      |  2 +-
 src/SymbolicToPure.ml | 22 +++++++++++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

(limited to 'src')

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
@@ -219,6 +219,14 @@ let type_def_to_string (ctx : bs_ctx) (def : type_def) : string =
   let fmt = PrintPure.mk_type_formatter type_defs type_params in
   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
@@ -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*.
-- 
cgit v1.2.3