diff options
| author | Son Ho | 2023-10-23 13:47:39 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-23 13:47:39 +0200 |
| commit | 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 (patch) | |
| tree | 26f8d2064020861bd821a15b50f84f2e95ae21af /compiler/Invariants.ml | |
| parent | f11d5186b467df318f7c09eedf8b5629c165b453 (diff) | |
Remove some assumed types and add more support for builtin definitions
Diffstat (limited to 'compiler/Invariants.ml')
| -rw-r--r-- | compiler/Invariants.ml | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 9ac5ce13..5c8ec7af 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -447,7 +447,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = fields_with_types (* Assumed type case *) | V.Adt av, T.Adt (T.Assumed aty_id, generics) -> ( - assert (av.V.variant_id = None || aty_id = T.Option); + assert (av.V.variant_id = None); match ( aty_id, av.V.field_values, @@ -456,19 +456,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = 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 ( |