Make progress on translate_typed_value_to_rvalue

1 files changed, 11 insertions, 5 deletions

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 91f355ee..de13e1b3 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -550,7 +550,8 @@ let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
     - end abstraction
     - return
     
-    TODO: we need the evaluation context to lookup shared borrows!!!
+    TODO: we have a problem with shared borrows. I think the shared borrows
+    should carry the shared value as a meta-value.
  *)
 let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
     typed_rvalue =
@@ -558,7 +559,10 @@ let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
   let value =
     match v.value with
     | V.Concrete cv -> RvConcrete cv
-    | Adt av -> raise Unimplemented
+    | Adt av ->
+        let variant_id = av.variant_id in
+        let field_values = List.map translate av.field_values in
+        RvAdt { variant_id; field_values }
     | Bottom -> failwith "Unreachable"
     | Loan lc -> (
         match lc with
@@ -566,14 +570,16 @@ let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
         | MutLoan _ -> failwith "Unreachable")
     | Borrow bc -> (
         match bc with
-        | V.SharedBorrow _ -> raise Unimplemented
+        | V.SharedBorrow _ ->
+            (* TODO: *)
+            raise Unimplemented
         | V.InactivatedMutBorrow _ -> failwith "Unreachable"
         | V.MutBorrow (_, v) ->
             (* Borrows are the identity in the extraction *)
             (translate v).value)
     | Symbolic sv ->
-        (* TODO: add sanity checks *)
-        raise Unimplemented
+        let var = get_var_for_symbolic_value sv ctx in
+        (mk_typed_rvalue_from_var var).value
   in
   let ty = translate_fwd_ty ctx v.ty in
   { value; ty }