diff options
| -rw-r--r-- | src/Contexts.ml | 3 | ||||
| -rw-r--r-- | src/Interpreter.ml | 41 | ||||
| -rw-r--r-- | src/Substitute.ml | 10 |
3 files changed, 41 insertions, 13 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index afa68272..dd7ca016 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -46,6 +46,9 @@ let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = VarId.Map.find vid ctx.vars +let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def = + TypeDefId.nth ctx.type_context tid + (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = let check_ev (ev : env_value) : typed_value option = diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 7e956d0e..55045cf5 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1724,17 +1724,34 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : Ok (ctx1, { value = Concrete (Scalar sv); ty = Integer Isize }) )) | _ -> failwith "Invalid input for `discriminant`") - | Aggregate (aggregate_kind, ops) -> + | Aggregate (aggregate_kind, ops) -> ( (* Evaluate the operands *) let ctx1, values = eval_operands config ctx ops in - raise Unimplemented -(* (* Match on the aggregate kind *) - match aggregate_kind with - | AggregatedTuple -> - let tys = List.map (fun v -> v.ty) values in - let values = FieldId.vector_of_list values in - Ok (ctx1, { value = Tuple values; ty = Types.Tuple tys }) - | AggregatedAdt (def_id, opt_variant_id) -> raise Unimplemented - begin match - let expected_types = ctx_get_adt_field_types def_id opt_variant_id - let fields = ctx_get_adt_fields def_id opt_variant_id in*) + let values = FieldId.vector_of_list values in + (* Match on the aggregate kind *) + match aggregate_kind with + | AggregatedTuple -> + let tys = List.map (fun v -> v.ty) (FieldId.vector_to_list values) in + Ok (ctx1, { value = Tuple values; ty = Types.Tuple tys }) + | AggregatedAdt (def_id, opt_variant_id, regions, types) -> + (* Sanity checks *) + let type_def = ctx_lookup_type_def ctx def_id in + assert ( + RegionVarId.length type_def.region_params = List.length regions); + let expected_field_types = + Subst.ctx_adt_get_instantiated_field_types ctx1 def_id + opt_variant_id types + in + assert (expected_field_types = FieldId.map (fun v -> v.ty) values); + (* Construct the value *) + let av = + { + def_id; + variant_id = opt_variant_id; + regions; + types; + field_values = values; + } + in + let aty = Types.Adt (def_id, regions, types) in + Ok (ctx1, { value = Adt av; ty = aty })) diff --git a/src/Substitute.ml b/src/Substitute.ml index 1957dc24..917275af 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -4,6 +4,7 @@ module T = Types module V = Values +module C = Contexts (** Substitute types variables and regions in a type *) let rec ty_subst (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty) @@ -70,7 +71,6 @@ let type_def_get_fields (def : T.type_def) let type_def_get_instantiated_field_type (def : T.type_def) (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety T.FieldId.vector = - (* let indices = List.mapi (fun i _ -> TypeVarId.of_int i) def.type_params in*) let ty_subst = make_type_subst (List.map @@ -82,3 +82,11 @@ let type_def_get_instantiated_field_type (def : T.type_def) T.FieldId.map (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty) fields + +(** Return the types of the properly instantiated ADT's variant, provided a + context *) +let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx) + (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) + (types : T.ety list) : T.ety T.FieldId.vector = + let def = C.ctx_lookup_type_def ctx def_id in + type_def_get_instantiated_field_type def opt_variant_id types |