New check implemented: the sort of each constructor should be constrained by

the sort of its inductive type.

Note: I just realized that nobody implements the check that the left
abstractions of each constructors/inductive type must be exactly the same.
To be implemented.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c74ae2206f48b825d2490847b4ebbd8c87f5a42e..00a1b6120ce3fd4f70380030a709fb7655a3ba02 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -94,10 +94,12 @@ let fixed_args bos j n nn =
    (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos
 ;;
 
+(* if n < 0, then splits all prods from an arity, returning a sort *)
 let rec split_prods ~subst context n te =
   match (n, R.whd ~subst context te) with
    | (0, _) -> context,te
-   | (n, C.Prod (name,so,ta)) when n > 0 ->
+   | (n, C.Sort _) when n <= 0 -> context,te
+   | (n, C.Prod (name,so,ta)) ->
        split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
    | (_, _) -> raise (AssertFailure (lazy "split_prods"))
 ;;
@@ -364,6 +366,7 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
        are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
         uri indparamsno (i+1) (n + 1) (nn + 1) dest
    | _ ->
+prerr_endline ("MM: " ^ NCicPp.ppterm ~subst ~metasenv:[] ~context te);
      raise
       (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
         (NUri.string_of_uri uri))))
@@ -705,19 +708,36 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
   (* let's check if the types of the inductive constructors are well formed. *)
   let len = List.length tyl in
-  let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in
+  let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
   ignore
    (List.fold_right
-    (fun (_,_,_,cl) i ->
+    (fun (_,_,ty,cl) i ->
+       let _,ty_sort = split_prods ~subst [] ~-1 ty in
        List.iter
          (fun (_,name,te) -> 
-           let debruijnedte = debruijn uri len [] te in
-           ignore (typeof ~subst ~metasenv tys debruijnedte);
+(*CSC: assicurarmi che i sx siano esattamente gli stessi! *)
+           let te = debruijn uri len [] te in
+           let context,te = split_prods ~subst tys leftno te in
+           let con_sort = typeof ~subst ~metasenv context te in
+           (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
+               C.Sort (C.Type u1), C.Sort (C.Type u2) ->
+                if not (E.universe_leq u1 u2) then
+                 raise
+                  (TypeCheckerFailure
+                    (lazy ("The type of the constructor is not included in " ^
+                      "the inductive type sort")))
+             | C.Sort _, C.Sort C.Prop
+             | C.Sort C.CProp, C.Sort C.CProp
+             | C.Sort _, C.Sort C.Type _ -> ()
+             | _, _ ->
+                raise
+                 (TypeCheckerFailure
+                   (lazy ("Wrong constructor or inductive arity shape"))));
            (* let's check also the positivity conditions *)
            if 
              not
-               (are_all_occurrences_positive ~subst tys uri leftno i 0 len
-                  debruijnedte) 
+               (are_all_occurrences_positive ~subst context uri leftno
+                 (i+leftno) leftno (len+leftno) te) 
            then
              raise
                (TypeCheckerFailure