summaryrefslogtreecommitdiff
path: root/compiler/InterpreterPaths.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterPaths.ml')
-rw-r--r--compiler/InterpreterPaths.ml66
1 files changed, 25 insertions, 41 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 04dc8892..2a277c91 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -3,6 +3,7 @@ module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
+module Assoc = AssociatedTypes
module L = Logging
open Cps
open ValuesUtils
@@ -95,16 +96,14 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
| pe :: p' -> (
(* Match on the projection element and the value *)
match (pe, v.V.value, v.V.ty) with
- | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id),
+ | ( Field ((ProjAdt (_, _) 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' ->
assert (def_id = def_id');
assert (opt_variant_id = adt.variant_id)
- | ProjOption variant_id, T.Assumed T.Option ->
- assert (Some variant_id = adt.variant_id)
| _ -> raise (Failure "Unreachable"));
(* Actually project *)
let fv = T.FieldId.nth adt.field_values field_id in
@@ -119,8 +118,7 @@ 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 *)
@@ -136,7 +134,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
Ok (ctx, { res with updated })
(* If we reach Bottom, it may mean we need to expand an uninitialized
* enumeration value *))
- | Field ((ProjAdt (_, _) | ProjTuple _ | ProjOption _), _), V.Bottom, _ ->
+ | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ ->
Error (FailBottom (1 + List.length p', pe, v.ty))
(* Symbolic value: needs to be expanded *)
| _, Symbolic sp, _ ->
@@ -145,9 +143,9 @@ 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, _, _, _) ) -> (
- (* We allow moving inside of boxes. In practice, this kind of
- * manipulations should happen only inside unsage code, so
+ T.Adt (T.Assumed T.Box, _) ) -> (
+ (* We allow moving outside of boxes. In practice, this kind of
+ * manipulations should happen only inside unsafe code, so
* it shouldn't happen due to user code, and we leverage it
* when implementing box dereferencement for the concrete
* interpreter *)
@@ -357,45 +355,32 @@ let write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
| Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
| Ok ctx -> ctx
-let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
+let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
(def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
- (regions : T.erased_region list) (types : T.ety list)
- (cgs : T.const_generic list) : V.typed_value =
+ (generics : T.egeneric_args) : 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
of fields at the same time. *)
- let def = T.TypeDeclId.Map.find def_id tyctx in
- assert (List.length regions = List.length def.T.region_params);
+ let def = C.ctx_lookup_type_decl ctx def_id in
+ assert (List.length generics.regions = List.length def.T.generics.regions);
(* Compute the field types *)
let field_types =
- Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types cgs
+ Assoc.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id generics
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, cgs) in
+ let ty = T.Adt (T.AdtId def_id, generics) in
{ V.value = av; V.ty }
-let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
- (param_ty : T.ety) : V.typed_value =
- (* Note that the variant can be [Some] or [None]: we expand bottom values
- * when writing to fields or setting discriminants *)
- let field_values =
- if variant_id = T.option_some_id then [ mk_bottom param_ty ]
- else if variant_id = T.option_none_id then []
- 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
- { V.value = av; ty }
-
let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
V.typed_value =
(* 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 generics = TypesUtils.mk_generic_args [] field_types [] [] in
+ let ty = T.Adt (T.Tuple, generics) in
{ V.value = v; V.ty }
(** Auxiliary helper to expand {!V.Bottom} values.
@@ -447,19 +432,18 @@ 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, cgs) ) ->
+ T.Adt (T.AdtId def_id', generics) ) ->
assert (def_id = def_id');
- compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id
- opt_variant_id regions types cgs
- (* Option *)
- | ( Field (ProjOption variant_id, _),
- T.Adt (T.Assumed T.Option, [], [ ty ], []) ) ->
- compute_expanded_bottom_option_value variant_id ty
+ compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
(* Tuples *)
- | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys, []) ->
- assert (arity = List.length tys);
+ | ( Field (ProjTuple arity, _),
+ T.Adt
+ ( T.Tuple,
+ { T.regions = []; types; const_generics = []; trait_refs = [] } ) )
+ ->
+ assert (arity = List.length types);
(* Generate the field values *)
- compute_expanded_bottom_tuple_value tys
+ compute_expanded_bottom_tuple_value types
| _ ->
raise
(Failure
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 03:45:47 +0000