diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 20 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.mli | 11 |
2 files changed, 20 insertions, 11 deletions
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 9487df84..faed066b 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -23,12 +23,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) if not (ty_has_regions_in_set regions ty) then [] else match (v.V.value, ty) with - | V.Primitive _, (T.Bool | T.Char | T.Integer _ | T.Str) -> [] - | V.Adt adt, T.Adt (id, region_params, tys) -> + | V.Literal _, T.Literal _ -> [] + | V.Adt adt, T.Adt (id, region_params, tys, cgs) -> (* Retrieve the types of the fields *) let field_types = Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id - region_params tys + region_params tys cgs in (* Project over the field values *) let fields_types = List.combine adt.V.field_values field_types in @@ -102,12 +102,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) else let value : V.avalue = match (v.V.value, ty) with - | V.Primitive _, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AIgnored - | V.Adt adt, T.Adt (id, region_params, tys) -> + | V.Literal _, T.Literal _ -> V.AIgnored + | V.Adt adt, T.Adt (id, region_params, tys, cgs) -> (* Retrieve the types of the fields *) let field_types = Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id - region_params tys + region_params tys cgs in (* Project over the field values *) let fields_types = List.combine adt.V.field_values field_types in @@ -231,7 +231,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) let ty = Subst.erase_regions sv.V.sv_ty in let value = match see with - | SePrimitive cv -> V.Primitive cv + | SeLiteral cv -> V.Literal cv | SeAdt (variant_id, field_values) -> let field_values = List.map mk_typed_value_from_symbolic_value field_values @@ -267,9 +267,9 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) (* Match *) let (value, ty) : V.avalue * T.rty = match (see, original_sv_ty) with - | SePrimitive _, (T.Bool | T.Char | T.Integer _ | T.Str) -> - (V.AIgnored, original_sv_ty) - | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) -> + | SeLiteral _, T.Literal _ -> (V.AIgnored, original_sv_ty) + | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys, _cgs) + -> (* Project over the field values *) let field_values = List.map diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli index 1afb9d53..bcc3dee2 100644 --- a/compiler/InterpreterProjectors.mli +++ b/compiler/InterpreterProjectors.mli @@ -55,7 +55,16 @@ val prepare_reborrows : bool -> (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) -(** Apply (and reduce) a projector over borrows to a value. +(** Apply (and reduce) a projector over borrows to an avalue. + We use this for instance to spread the borrows present in the inputs + of a function into the regions introduced for this function. For instance: + {[ + fn f<'a, 'b, T>(x: &'a T, y: &'b T) + ]} + If we call `f` with `x -> shared_borrow l0` and `y -> shared_borrow l1`, then + for the region introduced for `'a` we need to project the value for `x` to + a shared aborrow, and we need to ignore the borrow in `y`, because it belongs + to the other region. Parameters: - [check_symbolic_no_ended]: controls whether we check or not whether |