X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=fd2819738af77561725d77067926a694b90b9480;hb=063523ae5f8da7e6458232f4afb6744ec86dc8bd;hp=88219ee37d2e9a95a05894db3fce055db3c156af;hpb=d344d41028275b6d1451dca8e40a88e33e588389;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 88219ee37..fd2819738 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -557,25 +557,37 @@ 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.Sort Cic.Set
+                | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
+                | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
+                | a,b ->
+                   raise
+                    (TypeCheckerFailure
+                      (lazy ("Wrong constructor or inductive arity shape: "^
+                        CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) 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 +596,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 +720,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"))