Start working on typed_avalue_to_consumed

2 files changed, 51 insertions, 2 deletions

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index de13e1b3..4dfe00c7 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -584,10 +584,53 @@ let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
   let ty = translate_fwd_ty ctx v.ty in
   { value; ty }
 
-let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
+let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
     typed_rvalue option =
+  let translate = typed_avalue_to_consumed ctx in
+  let value =
+    match av.value with
+    | AConcrete _ -> failwith "Unreachable"
+    | AAdt av -> raise Unimplemented
+    | ABottom -> raise Unimplemented
+    | ALoan lc -> raise Unimplemented
+    | ABorrow bc -> raise Unimplemented
+    | ASymbolic aproj -> raise Unimplemented
+    | AIgnored -> None
+  in
   raise Unimplemented
 
+and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
+  let translate = aproj_to_consumed ctx in
+  match aproj with
+  | V.AEndedProjLoans (msv, []) ->
+      (* The symbolic value was left unchanged *)
+      let var = get_var_for_symbolic_value msv ctx in
+      Some (mk_typed_rvalue_from_var var)
+  | V.AEndedProjLoans (_, [ (mnv, AIgnoredProjBorrows) ]) ->
+      (* The symbolic value was updated *)
+      let var = get_var_for_symbolic_value mnv ctx in
+      Some (mk_typed_rvalue_from_var var)
+  | AEndedProjBorrows _ -> (* We consider consumed values *) None
+  | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
+      failwith "Unreachable"
+
+(*
+  | V.AEndedProjLoans (_, _) ->
+      (* The symbolic value was through values given back by several abstractions *)
+      raise Unimplemented
+  | V.AEndedSharedLoan (_, _) ->
+      (* Shared loans don't consume anything *)
+      None
+  | AIgnoredMutLoan (_, _) ->
+      (* There can be *inner* mutable loans, but not outer ones *)
+      failwith "Unreachable"
+  | AEndedIgnoredMutLoan { child = _; given_back = _; given_back_meta = _ } ->
+      (* No nested borrows for now *)
+      raise Unimplemented
+  | AIgnoredSharedLoan _ ->
+      (* Ignore *)
+None*)
+
 let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
   List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
 
diff --git a/src/Values.ml b/src/Values.ml
index 92b9df35..fe8daf30 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -285,6 +285,8 @@ type aproj =
           We can later end the projector of loans if `s@0` is not referenced
           anywhere in the context below a projector of borrows which intersects
           this projector of loans.
+          
+          TODO: we should use an msymbolic_value, not an mvalue
        *)
   | AProjBorrows of symbolic_value * rty
       (** Note that an AProjBorrows only operates on a value which is not below
@@ -300,6 +302,8 @@ type aproj =
           See the explanations for [AProjLoans]
           
           Note that we keep the original symbolic value as a meta-value.
+
+          TODO: we should use an msymbolic_value, not an mvalue
        *)
   | AEndedProjBorrows of mvalue
       (** The only purpose of [AEndedProjBorrows] is to store, for synthesis
@@ -364,7 +368,9 @@ class ['self] map_typed_avalue_base =
 *)
 type avalue =
   | AConcrete of constant_value
-      (** TODO: remove
+      (** TODO: remove. We actually don't use that for the synthesis, but the
+          meta-values.
+       
           Note that this case is not used in the projections to keep track of the
           borrow graph (because there are no borrows in "concrete" values!) but
           to correctly instantiate the backward functions (we may give back some