Merge pull request #44 from AeneasVerif/son_traits_types

Add support for traits

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)