summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-25 21:55:19 +0100
committerSon Ho2022-01-25 21:55:19 +0100
commit11c1991d81e3ecdf3fb348416cb1650b02d8efe3 (patch)
tree4d8648543976ca8883c2720ac9fa8fab4430a369
parent4789a0c1762dd8358b8c2f2b88653d0f9bf16059 (diff)
Finish implementing SymbolicToPure.translate_end_abstraction
Diffstat (limited to '')
-rw-r--r--src/Pure.ml4
-rw-r--r--src/SymbolicToPure.ml28
2 files changed, 26 insertions, 6 deletions
diff --git a/src/Pure.ml b/src/Pure.ml
index 504f2c11..45907610 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -126,8 +126,8 @@ type left_value = unit
type let_bindings =
| Call of typed_lvalue list * call
(** The called function and the tuple of returned values. *)
- | Assignment of var * typed_rvalue
- (** Variable assignment: the introduced variable and the place we read *)
+ | Assign of typed_lvalue * typed_rvalue
+ (** Variable assignment: the introduced pattern and the place we read *)
| Deconstruct of
var_or_dummy list * (TypeDefId.id * VariantId.id) option * typed_rvalue
(** This is used in two cases.
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 06ccf7bf..7cae951b 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -105,6 +105,11 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
let ty = v.ty in
{ value; ty }
+let mk_typed_lvalue_from_var (v : var) : typed_lvalue =
+ let value = LvVar (Var v) in
+ let ty = v.ty in
+ { value; ty }
+
(* TODO: move *)
let type_def_is_enum (def : T.type_def) : bool =
match def.kind with T.Struct _ -> false | Enum _ -> true
@@ -670,7 +675,22 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
(* First, retrieve the list of variables used for the inputs for the
* backward function *)
let inputs = T.RegionGroupId.Map.find abs.back_id ctx.backward_inputs in
- raise Unimplemented
+ (* Retrieve the values consumed upon ending the loans inside this
+ * abstraction: as there are no nested borrows, there should be none. *)
+ let consumed = abs_to_consumed ctx abs in
+ assert (consumed = []);
+ (* Retrieve the values given back upon ending this abstraction *)
+ let ctx, given_back = abs_to_given_back abs ctx in
+ (* Link the inputs to those given back values - note that we must
+ * have the same number of values *)
+ let given_back_inputs = List.combine given_back inputs in
+ (* Translate the next expression *)
+ let e = translate_expression e ctx in
+ (* Generate the assignments *)
+ List.fold_right
+ (fun (given_back, input_var) e ->
+ Let (Assign (given_back, mk_typed_rvalue_from_var input_var), e))
+ given_back_inputs e
and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
(ctx : bs_ctx) : expression =
@@ -690,7 +710,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
* introduce an reassignment *)
let ctx, var = fresh_var_for_symbolic_value sv ctx in
let e = translate_expression e ctx in
- Let (Assignment (var, scrutinee), e)
+ Let (Assign (mk_typed_lvalue_from_var var, scrutinee), e)
| SeAdt _ ->
(* Should be in the [ExpandAdt] case *)
failwith "Unreachable")
@@ -733,7 +753,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
List.fold_right
(fun (fid, var) e ->
let field_proj = gen_field_proj fid var in
- Let (Assignment (var, field_proj), e))
+ Let (Assign (mk_typed_lvalue_from_var var, field_proj), e))
id_var_pairs branch
| T.Tuple ->
let vars = List.map (fun x -> Var x) vars in
@@ -745,7 +765,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
in
(* We simply introduce an assignment - the box type is the
* identity when extracted (`box a == a`) *)
- Let (Assignment (var, scrutinee), branch))
+ Let (Assign (mk_typed_lvalue_from_var var, scrutinee), branch))
| branches ->
let translate_branch (variant_id : T.VariantId.id option)
(svl : V.symbolic_value list) (branch : S.expression) :