From b7387d913f7dddf52d1e73173bca3fc8729723ba Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 23 Oct 2006 20:23:24 +0000
Subject: [PATCH] CicUniv.UniverseInconsistency is no handled correcly.
---
components/cic/cicUniv.ml | 29 ++++++++++---------
components/cic/cicUniv.mli | 4 +--
components/cic_proof_checking/cicReduction.ml | 8 +++--
.../cic_proof_checking/cicTypeChecker.ml | 16 ++++++----
components/cic_unification/cicRefine.ml | 16 ++++++----
components/cic_unification/cicUnification.ml | 12 +++++---
components/tactics/primitiveTactics.ml | 4 +--
7 files changed, 55 insertions(+), 34 deletions(-)
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 =
--
2.39.5