summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-17 16:31:07 +0100
committerSon Ho2021-12-17 16:31:07 +0100
commit46fd662af66ef9b536a3a06cb38a18468f1f33d2 (patch)
tree9e7abfe997442b058edf8513a41ca736ab01540d /src
parent88558dcbb12bde11af6fba9eb36e1f4841b8e7d1 (diff)
Add more field type instantiation functions for the ADTs
Diffstat (limited to 'src')
-rw-r--r--src/Substitute.ml41
1 files changed, 40 insertions, 1 deletions
diff --git a/src/Substitute.ml b/src/Substitute.ml
index b3a8fcf5..c1903c71 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -41,8 +41,23 @@ let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in
ty_substitute rsubst tsubst ty
+(** Create a region substitution from a list of region variable ids and a list of
+ regions (with which to substitute the region variable ids *)
+let make_region_subst (var_ids : T.RegionVarId.id list)
+ (regions : 'r T.region list) : T.RegionVarId.id T.region -> 'r T.region =
+ let ls = List.combine var_ids regions in
+ let mp =
+ List.fold_left
+ (fun mp (k, v) -> T.RegionVarId.Map.add k v mp)
+ T.RegionVarId.Map.empty ls
+ in
+ fun r ->
+ match r with
+ | T.Static -> T.Static
+ | T.Var id -> T.RegionVarId.Map.find id mp
+
(** Create a type substitution from a list of type variable ids and a list of
- types (with which to substitute the type variable ids *)
+ types (with which to substitute the type variable ids) *)
let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
T.TypeVarId.id -> 'r T.ty =
let ls = List.combine var_ids tys in
@@ -55,6 +70,30 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
(** Instantiate the type variables in an ADT definition, and return the list
of types of the fields for the chosen variant *)
+let type_def_get_instantiated_field_rtype (def : T.type_def)
+ (opt_variant_id : T.VariantId.id option)
+ (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
+ let r_subst =
+ make_region_subst
+ (List.map (fun x -> x.T.index) def.T.region_params)
+ regions
+ in
+ let ty_subst =
+ make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
+ in
+ let fields = TU.type_def_get_fields def opt_variant_id in
+ List.map (fun f -> ty_substitute r_subst 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_rtypes (ctx : C.eval_ctx)
+ (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
+ (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
+ let def = C.ctx_lookup_type_def ctx def_id in
+ type_def_get_instantiated_field_rtype def opt_variant_id regions types
+
+(** Instantiate the type variables in an ADT definition, and return the list
+ of types of the fields for the chosen variant *)
let type_def_get_instantiated_field_etype (def : T.type_def)
(opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list =
let ty_subst =