summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-26 09:21:54 +0100
committerSon Ho2022-01-26 09:21:54 +0100
commit864b0dfe11641f56195de506011ea4dfdd847574 (patch)
tree1ad2bffc7978e6ecd0771db1c84974667f059502
parent3d4f1f02e0ff2dc0c634f800d79bd00a3097b761 (diff)
Add some comments
Diffstat (limited to '')
-rw-r--r--src/SymbolicToPure.ml34
1 files changed, 34 insertions, 0 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index b121ae33..dc792701 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -587,6 +587,21 @@ 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 }
+(** Explore an abstraction value and convert it to a consumed value
+ by collecting all the meta-values from the ended *loans*.
+
+ Consumed values are rvalues, because when an abstraction ends, we
+ introduce a call to a backward function in the synthesized program,
+ which takes as inputs those consumed values:
+ ```
+ // Rust:
+ fn choose<'a>(b: bool, x : &'a mut u32, y : &'a mut u32) -> &'a mut u32;
+
+ // Synthesis:
+ let ... = choose_back b x y nz in
+ ^^
+ ```
+ *)
let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
typed_rvalue option =
let translate = typed_avalue_to_consumed ctx in
@@ -674,9 +689,24 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
| AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
failwith "Unreachable"
+(** Convert the abstraction values in an abstraction to consumed values.
+
+ See [typed_avalue_to_consumed].
+ *)
let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
+(** Explore an abstraction value and convert it to a given back value
+ by collecting all the meta-values from the ended *borrows*.
+
+ Given back values are lvalues, because when an abstraction ends, we
+ introduce a call to a backward function in the synthesized program,
+ which introduces new values:
+ ```
+ let (nx, ny) = f_back ... in
+ ^^^^^^^^
+ ```
+ *)
let rec typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
bs_ctx * typed_lvalue option =
match av.value with
@@ -762,6 +792,10 @@ and aproj_to_given_back (aproj : V.aproj) (ctx : bs_ctx) :
| AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
failwith "Unreachable"
+(** Convert the abstraction values in an abstraction to given back values.
+
+ See [typed_avalue_to_given_back].
+ *)
let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_lvalue list
=
let ctx, values =