diff options
Diffstat (limited to 'compiler/Invariants.ml')
| -rw-r--r-- | compiler/Invariants.ml | 82 |
1 files changed, 46 insertions, 36 deletions
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index f29c7f88..5c8ec7af 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -7,6 +7,7 @@ module V = Values module E = Expressions module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module A = LlbcAst module L = Logging open Cps @@ -406,13 +407,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (match (tv.V.value, tv.V.ty) with | V.Literal cv, T.Literal ty -> check_literal_type cv ty (* ADT case *) - | V.Adt av, T.Adt (T.AdtId def_id, regions, tys, cgs) -> + | V.Adt av, T.Adt (T.AdtId def_id, generics) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) let def = C.ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - assert (List.length regions = List.length def.region_params); - assert (List.length tys = List.length def.type_params); + assert ( + List.length generics.regions = List.length def.generics.regions); + assert (List.length generics.types = List.length def.generics.types); (* Check that the variant id is consistent *) (match (av.V.variant_id, def.T.kind) with | Some variant_id, T.Enum variants -> @@ -421,8 +423,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> raise (Failure "Erroneous typing")); (* Check that the field types are correct *) let field_types = - Subst.type_decl_get_instantiated_field_etypes def av.V.variant_id - tys cgs + Assoc.type_decl_get_inst_norm_field_etypes ctx def av.V.variant_id + generics in let fields_with_types = List.combine av.V.field_values field_types @@ -431,34 +433,31 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty)) fields_with_types (* Tuple case *) - | V.Adt av, T.Adt (T.Tuple, regions, tys, cgs) -> - assert (regions = []); - assert (cgs = []); + | V.Adt av, T.Adt (T.Tuple, generics) -> + assert (generics.regions = []); + assert (generics.const_generics = []); assert (av.V.variant_id = None); (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) - let fields_with_types = List.combine av.V.field_values tys in + let fields_with_types = + List.combine av.V.field_values generics.types + in List.iter (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty)) fields_with_types (* Assumed type case *) - | V.Adt av, T.Adt (T.Assumed aty_id, regions, tys, cgs) -> ( - assert (av.V.variant_id = None || aty_id = T.Option); - match (aty_id, av.V.field_values, regions, tys, cgs) with + | V.Adt av, T.Adt (T.Assumed aty_id, generics) -> ( + assert (av.V.variant_id = None); + match + ( aty_id, + av.V.field_values, + generics.regions, + generics.types, + generics.const_generics ) + with (* Box *) - | T.Box, [ inner_value ], [], [ inner_ty ], [] - | T.Option, [ inner_value ], [], [ inner_ty ], [] -> + | T.Box, [ inner_value ], [], [ inner_ty ], [] -> assert (inner_value.V.ty = inner_ty) - | T.Option, _, [], [ _ ], [] -> - (* Option::None: nothing to check *) - () - | T.Vec, fvs, [], [ vec_ty ], [] -> - List.iter - (fun (v : V.typed_value) -> assert (v.ty = vec_ty)) - fvs - | T.Range, [ v0; v1 ], [], [ inner_ty ], [] -> - assert (v0.V.ty = inner_ty); - assert (v1.V.ty = inner_ty) | T.Array, inner_values, _, [ inner_ty ], [ cg ] -> (* *) assert ( @@ -520,14 +519,17 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Check the current pair (value, type) *) (match (atv.V.value, atv.V.ty) with (* ADT case *) - | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys, cgs) -> + | V.AAdt av, T.Adt (T.AdtId def_id, generics) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) let def = C.ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - assert (List.length regions = List.length def.region_params); - assert (List.length tys = List.length def.type_params); - assert (List.length cgs = List.length def.const_generic_params); + assert ( + List.length generics.regions = List.length def.generics.regions); + assert (List.length generics.types = List.length def.generics.types); + assert ( + List.length generics.const_generics + = List.length def.generics.const_generics); (* Check that the variant id is consistent *) (match (av.V.variant_id, def.T.kind) with | Some variant_id, T.Enum variants -> @@ -536,8 +538,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> raise (Failure "Erroneous typing")); (* Check that the field types are correct *) let field_types = - Subst.type_decl_get_instantiated_field_rtypes def av.V.variant_id - regions tys cgs + Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.V.variant_id + generics in let fields_with_types = List.combine av.V.field_values field_types @@ -546,20 +548,28 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty)) fields_with_types (* Tuple case *) - | V.AAdt av, T.Adt (T.Tuple, regions, tys, cgs) -> - assert (regions = []); - assert (cgs = []); + | V.AAdt av, T.Adt (T.Tuple, generics) -> + assert (generics.regions = []); + assert (generics.const_generics = []); assert (av.V.variant_id = None); (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) - let fields_with_types = List.combine av.V.field_values tys in + let fields_with_types = + List.combine av.V.field_values generics.types + in List.iter (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty)) fields_with_types (* Assumed type case *) - | V.AAdt av, T.Adt (T.Assumed aty_id, regions, tys, cgs) -> ( + | V.AAdt av, T.Adt (T.Assumed aty_id, generics) -> ( assert (av.V.variant_id = None); - match (aty_id, av.V.field_values, regions, tys, cgs) with + match + ( aty_id, + av.V.field_values, + generics.regions, + generics.types, + generics.const_generics ) + with (* Box *) | T.Box, [ boxed_value ], [], [ boxed_ty ], [] -> assert (boxed_value.V.ty = boxed_ty) |