From: Claudio Sacerdoti Coen Date: Mon, 23 Oct 2006 20:23:24 +0000 (+0000) Subject: CicUniv.UniverseInconsistency is no handled correcly. X-Git-Tag: 0.4.95@7852~862 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b7387d913f7dddf52d1e73173bca3fc8729723ba;p=helm.git CicUniv.UniverseInconsistency is no handled correcly. --- diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml index 0d75caf89..d48772c27 100644 --- 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 eb3c50866..288efe616 100644 --- 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 b636c2a72..f4880e426 100644 --- 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 0c0646d05..8f36b9e17 100644 --- 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 dee8ba5f3..21af1f9c7 100644 --- 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 8ba0ae917..c9981bb11 100644 --- 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 b016eb85f..c9d68d9de 100644 --- 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 =