diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterPaths.ml | 30 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.mli | 1 |
2 files changed, 17 insertions, 14 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 619815b3..04dc8892 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -97,7 +97,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) match (pe, v.V.value, v.V.ty) with | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id), V.Adt adt, - T.Adt (type_id, _, _) ) -> ( + T.Adt (type_id, _, _, _) ) -> ( (* Check consistency *) (match (proj_kind, type_id) with | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' -> @@ -119,7 +119,8 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) let updated = { v with value = nadt } in Ok (ctx, { res with updated })) (* Tuples *) - | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> ( + | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _, _) + -> ( assert (arity = List.length adt.field_values); let fv = T.FieldId.nth adt.field_values field_id in (* Project *) @@ -144,7 +145,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Box dereferencement *) | ( DerefBox, Adt { variant_id = None; field_values = [ bv ] }, - T.Adt (T.Assumed T.Box, _, _) ) -> ( + T.Adt (T.Assumed T.Box, _, _, _) ) -> ( (* We allow moving inside of boxes. In practice, this kind of * manipulations should happen only inside unsage code, so * it shouldn't happen due to user code, and we leverage it @@ -249,7 +250,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) in Ok (ctx, { res with updated = nv }) else Error (FailSharedLoan bids)) - | (_, (V.Primitive _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> + | (_, (V.Literal _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> let pe, v, ty = r in let pe = "- pe: " ^ E.show_projection_elem pe in let v = "- v:\n" ^ V.show_value v in @@ -358,7 +359,8 @@ let write_place (access : access_kind) (p : E.place) (nv : V.typed_value) let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t) (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) - (regions : T.erased_region list) (types : T.ety list) : V.typed_value = + (regions : T.erased_region list) (types : T.ety list) + (cgs : T.const_generic list) : V.typed_value = (* Lookup the definition and check if it is an enumeration - it should be an enumeration if and only if the projection element is a field projection with *some* variant id. Retrieve the list @@ -367,12 +369,12 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t) assert (List.length regions = List.length def.T.region_params); (* Compute the field types *) let field_types = - Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types + Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types cgs in (* Initialize the expanded value *) let fields = List.map mk_bottom field_types in let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in - let ty = T.Adt (T.AdtId def_id, regions, types) in + let ty = T.Adt (T.AdtId def_id, regions, types, cgs) in { V.value = av; V.ty } let compute_expanded_bottom_option_value (variant_id : T.VariantId.id) @@ -385,7 +387,7 @@ let compute_expanded_bottom_option_value (variant_id : T.VariantId.id) else raise (Failure "Unreachable") in let av = V.Adt { variant_id = Some variant_id; field_values } in - let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ]) in + let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ], []) in { V.value = av; ty } let compute_expanded_bottom_tuple_value (field_types : T.ety list) : @@ -393,7 +395,7 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) : (* Generate the field values *) let fields = List.map mk_bottom field_types in let v = V.Adt { variant_id = None; field_values = fields } in - let ty = T.Adt (T.Tuple, [], field_types) in + let ty = T.Adt (T.Tuple, [], field_types, []) in { V.value = v; V.ty } (** Auxiliary helper to expand {!V.Bottom} values. @@ -445,16 +447,16 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place) match (pe, ty) with (* "Regular" ADTs *) | ( Field (ProjAdt (def_id, opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types) ) -> + T.Adt (T.AdtId def_id', regions, types, cgs) ) -> assert (def_id = def_id'); compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id - opt_variant_id regions types + opt_variant_id regions types cgs (* Option *) - | Field (ProjOption variant_id, _), T.Adt (T.Assumed T.Option, [], [ ty ]) - -> + | ( Field (ProjOption variant_id, _), + T.Adt (T.Assumed T.Option, [], [ ty ], []) ) -> compute_expanded_bottom_option_value variant_id ty (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> + | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys, []) -> assert (arity = List.length tys); (* Generate the field values *) compute_expanded_bottom_tuple_value tys diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 6e9286cd..4a9f3b41 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -61,6 +61,7 @@ val compute_expanded_bottom_adt_value : T.VariantId.id option -> T.erased_region list -> T.ety list -> + T.const_generic list -> V.typed_value (** Compute an expanded [Option] ⊥ value *) |