added oblivion_universe and used it in paxck_coercions

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 81b33b0d198f7b6c958c9055c1dbedee84d7f29f..8f36b9e1780e1d562c99939f7b791d181b615aec 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -772,7 +772,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
           C.Rel m when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -784,9 +784,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -809,7 +814,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -818,7 +823,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -830,9 +835,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -857,7 +867,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -1533,11 +1543,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_gt t' t ugraph in
-         (C.Sort (C.Type t')),ugraph1
-      (* TASSI: CONSTRAINTS *)
+       (try
+         let ugraph1 = CicUniv.add_gt t' t ugraph in
+           (C.Sort (C.Type t')),ugraph1
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
-    | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+    | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Cast (te,ty) as t ->
        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
@@ -1953,9 +1965,12 @@ end;
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_ge t' t1 ugraph in
-       let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
-       C.Sort (C.Type t'),ugraph2
+        (try
+         let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+         let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+          C.Sort (C.Type t'),ugraph2
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | (C.Sort _,C.Sort (C.Type t1)) -> 
         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)