diff options
Diffstat (limited to 'compiler/InterpreterProjectors.ml')
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 20 |
1 files changed, 10 insertions, 10 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 |