CicUniv.UniverseInconsistency is no handled correcly.

diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml
index 0d75caf898cec408590e0f82a59aaf22bfa4b085..d48772c27a40a0bea41d14eeb0e55de644fb1976 100644 (file)
--- a/components/cic/cicUniv.ml
+++ b/components/cic/cicUniv.ml
@@ -397,20 +397,22 @@ let add_gt fast u v b =
 (** Other real code                                                         **)
 (*****************************************************************************)
 
-exception UniverseInconsistency of string 
+exception UniverseInconsistency of string Lazy.t
 
 let error arc node1 closure_type node2 closure =
-  let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
-   "   Unable to add\n" ^ 
-   "\t" ^ (string_of_arc arc) ^ "\n" ^
-   "   cause\n" ^ 
-   "\t" ^ (string_of_universe node1) ^ "\n" ^
-   "   is in the " ^ closure_type ^ " closure\n" ^
-   "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
-   "   of\n" ^ 
-   "\t" ^ (string_of_universe node2) ^ "\n\n" ^
-   "  ===== Universe Inconsistency detected =====\n" in
-  prerr_endline s;
+  let s =
+   lazy
+    ("\n  ===== Universe Inconsistency detected =====\n\n" ^
+     "   Unable to add\n" ^ 
+     "\t" ^ (string_of_arc arc) ^ "\n" ^
+     "   cause\n" ^ 
+     "\t" ^ (string_of_universe node1) ^ "\n" ^
+     "   is in the " ^ closure_type ^ " closure\n" ^
+     "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
+     "   of\n" ^ 
+     "\t" ^ (string_of_universe node2) ^ "\n\n" ^
+     "  ===== Universe Inconsistency detected =====\n") in
+  prerr_endline (Lazy.force s);
   raise (UniverseInconsistency s)
 
 
@@ -947,7 +949,8 @@ let recons_graph (graph,uriset) =
 
 let assert_univ u =
     match u with 
-    | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
+    | (_,None) ->
+       raise (UniverseInconsistency (lazy "This universe graph has a hole"))
     | _ -> ()
     
 let assert_univs_have_uri (graph,_) univlist =

diff --git a/components/cic/cicUniv.mli b/components/cic/cicUniv.mli
index eb3c50866f73482a578f0f8376bd376c8e124236..288efe616885b833ceedb5984af376fda2f8b2ae 100644 (file)
--- a/components/cic/cicUniv.mli
+++ b/components/cic/cicUniv.mli
@@ -27,7 +27,7 @@
 (*
   The strings contains an unreadable message
 *)
-exception UniverseInconsistency of string
+exception UniverseInconsistency of string Lazy.t
 
 (*
   Cic.Type of universe 
@@ -136,7 +136,7 @@ val recons_graph: universe_graph -> universe_graph
   (** re-hash-cons a single universe *)
 val recons_univ: universe -> universe
 
-  (** consistency chek that should be done before committin the graph to the
+  (** consistency check that should be done before committin the graph to the
    * cache *)
 val assert_univs_have_uri: universe_graph -> universe list-> unit
 

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index b636c2a729aa2ef688d99a8c8a42e0c173b795f5..f4880e426de66ffd74b78808eea763cb4b761a71 100644 (file)
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -856,10 +856,14 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             with  CicUtil.Subst_not_found _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-            true,(CicUniv.add_eq t2 t1 ugraph)
+            (try
+              true,(CicUniv.add_eq t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-            true,(CicUniv.add_ge t2 t1 ugraph)
+            (try
+              true,(CicUniv.add_ge t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
           (* TASSI: CONSTRAINTS *)

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index 0c0646d05a559dfc745c044d7fa1b2ced6a9e01a..8f36b9e1780e1d562c99939f7b791d181b615aec 100644 (file)
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/components/cic_proof_checking/cicTypeChecker.ml
@@ -1543,8 +1543,11 @@ 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
+       (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 "Implicit found"))
     | C.Cast (te,ty) as t ->
@@ -1962,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? *)

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index dee8ba5f3a451d7e8470f738fbabf618397314d9..21af1f9c74533cb640311e630c61fac70ffa0f96 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -395,8 +395,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    subst', metasenv',ugraph1)
         | C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
-            let ugraph1 = CicUniv.add_gt tno' tno ugraph in
-              t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+             (try
+               let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+                 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | C.Sort _ -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
         | C.Implicit infos ->
@@ -1145,9 +1148,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               C.Sort s2,subst,metasenv,ugraph
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
             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'),subst,metasenv,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'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | (C.Sort _,C.Sort (C.Type t1)) -> 
             C.Sort (C.Type t1),subst,metasenv,ugraph
         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index 8ba0ae917c828e807d85980acdb0a6a560a77718..c9981bb1114ead6d8b5fd8262162a1066a4f94db 100644 (file)
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -431,10 +431,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                C.Sort (C.Type u) when not test_equality_only ->
                  let u' = CicUniv.fresh () in
                  let s = C.Sort (C.Type u') in
-                 let ugraph2 =   
-                   CicUniv.add_ge (upper u u') (lower u u') ugraph1
-                 in
-                   s,ugraph2
+                  (try
+                    let ugraph2 =   
+                     CicUniv.add_ge (upper u u') (lower u u') ugraph1
+                    in
+                     s,ugraph2
+                   with
+                    CicUniv.UniverseInconsistency msg ->
+                     raise (UnificationFailure msg))
              | _ -> t',ugraph1
          in
          (* Unifying the types may have already instantiated n. Let's check *)

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index b016eb85f6141cc7445bb75dcdcc306d5657c4c3..c9d68d9deccfe96770cf888097cfcc1797ec6a20 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -298,8 +298,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
      try
       new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
         termty n
-     with (CicUnification.UnificationFailure _ 
-     | CicUniv.UniverseInconsistency _ ) when n > 0 ->
+     with CicUnification.UnificationFailure _ when n > 0 ->
       add_one_argument (n - 1)
     in
      add_one_argument goal_arity
@@ -337,7 +336,6 @@ let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
   with 
   | CicUnification.UnificationFailure msg
   | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
-  | CicUniv.UniverseInconsistency msg  -> raise (Fail (lazy msg))
 
 (* ALB *)
 let apply_tac_verbose ~term status =