Missing check implemented: the sort of each constructors should be constrained

by the sort of its inductive type.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 88219ee37d2e9a95a05894db3fce055db3c156af..6cbb44f8044432db90ae2cd361d2831cb132be8d 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -557,25 +557,35 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
   (* constructors using Prods                                *)
   let len = List.length itl in
   let tys =
-    List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
+    List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
   let _,ugraph2 =
     List.fold_right
-      (fun (_,_,_,cl) (i,ugraph) ->
+      (fun (_,_,ty,cl) (i,ugraph) ->
+        let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in
        let ugraph'' = 
           List.fold_left
             (fun ugraph (name,te) -> 
-              let debrujinedte = debrujin_constructor uri len [] te in
-              let augmented_term =
-               List.fold_right
-                 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-                 itl debrujinedte
-              in
-              let _,ugraph' = type_of ~logger augmented_term ugraph in
+              let te = debrujin_constructor uri len [] te in
+              let context,te = split_prods ~subst:[] tys indparamsno te in
+              let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in
+              let ugraph =
+               match
+                CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
+               with
+                  Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) ->
+                   CicUniv.add_ge u2 u1 ugraph
+                | Cic.Sort _, Cic.Sort Cic.Prop
+                | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
+                | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
+                | _, _ ->
+                   raise
+                    (TypeCheckerFailure
+                      (lazy ("Wrong constructor or inductive arity shape"))) in
               (* let's check also the positivity conditions *)
               if
                not
-                 (are_all_occurrences_positive tys uri indparamsno i 0 len
-                     debrujinedte)
+                 (are_all_occurrences_positive context uri indparamsno
+                    (i+indparamsno) indparamsno (len+indparamsno) te)
               then
                 begin
                 prerr_endline (UriManager.string_of_uri uri);
@@ -584,7 +594,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
                  (TypeCheckerFailure
                     (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
               else
-               ugraph'
+               ugraph
             ) ugraph cl in
        (i + 1),ugraph''
       ) itl (1,ugrap1)
@@ -708,7 +718,8 @@ and split_prods ~subst context n te =
  let module R = CicReduction in
   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 ((Some (name,(C.Decl so)))::context) (n - 1) ta
    | (_, _) -> raise (AssertFailure (lazy "8"))