diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Substitute.ml | 39 |
1 files changed, 22 insertions, 17 deletions
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index dbd310b7..177d8c24 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -7,6 +7,7 @@ open Types open Values open LlbcAst open Contexts +open Errors (** Generate fresh regions for region variables. @@ -67,25 +68,27 @@ let ctx_adt_get_instantiated_field_types (ctx : eval_ctx) **IMPORTANT**: this function doesn't normalize the types, you may want to use the [AssociatedTypes] equivalent instead. *) -let ctx_adt_value_get_instantiated_field_types (ctx : eval_ctx) - (adt : adt_value) (id : type_id) (generics : generic_args) : ty list = +let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) + (ctx : eval_ctx) (adt : adt_value) (id : type_id) (generics : generic_args) + : ty list = match id with | TAdtId id -> (* Retrieve the types of the fields *) ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics | TTuple -> - assert (generics.regions = []); + cassert __FILE__ __LINE__ (generics.regions = []) meta + "Tuples don't have region parameters"; generics.types | TAssumed aty -> ( match aty with | TBox -> - assert (generics.regions = []); - assert (List.length generics.types = 1); - assert (generics.const_generics = []); + sanity_check __FILE__ __LINE__ (generics.regions = []) meta; + sanity_check __FILE__ __LINE__ (List.length generics.types = 1) meta; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; generics.types | TArray | TSlice | TStr -> (* Those types don't have fields *) - raise (Failure "Unreachable")) + craise __FILE__ __LINE__ meta "Unreachable") (** Substitute a function signature, together with the regions hierarchy associated to that signature. @@ -144,30 +147,32 @@ let subst_ids_visitor (r_subst : RegionId.id -> RegionId.id) method! visit_abstraction_id _ id = asubst id end -let typed_value_subst_ids (r_subst : RegionId.id -> RegionId.id) +let typed_value_subst_ids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> TypeVarId.id) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) (bsubst : BorrowId.id -> BorrowId.id) (v : typed_value) : typed_value = - let asubst _ = raise (Failure "Unreachable") in + let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_typed_value () v -let typed_value_subst_rids (r_subst : RegionId.id -> RegionId.id) - (v : typed_value) : typed_value = - typed_value_subst_ids r_subst +let typed_value_subst_rids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (v : typed_value) : typed_value = + typed_value_subst_ids meta r_subst (fun x -> x) (fun x -> x) (fun x -> x) (fun x -> x) v -let typed_avalue_subst_ids (r_subst : RegionId.id -> RegionId.id) +let typed_avalue_subst_ids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> TypeVarId.id) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) (bsubst : BorrowId.id -> BorrowId.id) (v : typed_avalue) : typed_avalue = - let asubst _ = raise (Failure "Unreachable") in + let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_typed_avalue () v @@ -189,9 +194,9 @@ let env_subst_ids (r_subst : RegionId.id -> RegionId.id) let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_env () x -let typed_avalue_subst_rids (r_subst : RegionId.id -> RegionId.id) - (x : typed_avalue) : typed_avalue = - let asubst _ = raise (Failure "Unreachable") in +let typed_avalue_subst_rids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (x : typed_avalue) : typed_avalue = + let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in let vis = subst_ids_visitor r_subst (fun x -> x) |