Start working on translate_typed_value_to_rvalue

2 files changed, 29 insertions, 15 deletions

diff --git a/src/Pure.ml b/src/Pure.ml
index 45907610..1f66906d 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -54,17 +54,6 @@ type scalar_value = V.scalar_value
 
 type constant_value = V.constant_value
 
-type symbolic_value = {
-  sv_id : SymbolicValueId.id;
-  sv_ty : ty;
-  sv_rty : T.rty;
-  sv_ended_regions : RegionId.Set.t;
-      (** We need to remember what was the set of ended regions at the time the
-          symbolic value was introduced.
-       *)
-}
-(** TODO: remove *)
-
 type value = Concrete of constant_value | Adt of adt_value
 
 and adt_value = {
@@ -96,8 +85,8 @@ type projection = projection_elem list
 type place = { var : VarId.id; projection : projection }
 
 type rvalue =
-  | RvPlace of place
   | RvConcrete of constant_value
+  | RvPlace of place
   | RvAdt of adt_rvalue
 
 and adt_rvalue = {
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index acd40017..91f355ee 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -543,15 +543,40 @@ let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
     contain ended regions.
     
     TODO: we might want to remember in the symbolic AST the set of ended
-    regions, at the points where we need it, for sanity checks.
+    regions, at the points where we need it, for sanity checks (though the
+    sanity checks in the symbolic interpreter should be enough).
     The points where we need this set so far:
     - function call
     - end abstraction
     - return
+    
+    TODO: we need the evaluation context to lookup shared borrows!!!
  *)
-let translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
+let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
     typed_rvalue =
-  raise Unimplemented
+  let translate = translate_typed_value_to_rvalue ctx in
+  let value =
+    match v.value with
+    | V.Concrete cv -> RvConcrete cv
+    | Adt av -> raise Unimplemented
+    | Bottom -> failwith "Unreachable"
+    | Loan lc -> (
+        match lc with
+        | SharedLoan (_, v) -> (translate v).value
+        | MutLoan _ -> failwith "Unreachable")
+    | Borrow bc -> (
+        match bc with
+        | V.SharedBorrow _ -> 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
+  in
+  let ty = translate_fwd_ty ctx v.ty in
+  { value; ty }
 
 let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
     typed_rvalue option =