Implement the Aggregate branch of eval_rvalue

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