less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jan 14 09:59:50 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jan 14 09:59:50 2013 +0100
@@ -11,7 +11,7 @@
sig
type type_enc = ATP_Problem_Generate.type_enc
- exception METIS of string * string
+ exception METIS_RECONSTRUCT of string * string
val hol_clause_from_metis :
Proof.context -> type_enc -> int Symtab.table
@@ -34,7 +34,7 @@
open ATP_Proof_Reconstruct
open Metis_Generate
-exception METIS of string * string
+exception METIS_RECONSTRUCT of string * string
fun atp_name_from_metis type_enc s =
case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
@@ -166,8 +166,8 @@
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
Syntax.string_of_term ctxt (term_of y)))));
in cterm_instantiate substs' i_th end
- handle THM (msg, _, _) => raise METIS ("inst_inference", msg)
- | ERROR msg => raise METIS ("inst_inference", msg)
+ handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg)
+ | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg)
(* INFERENCE RULE: RESOLVE *)
@@ -293,7 +293,8 @@
| j2 =>
(trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2);
resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
- handle TERM (s, _) => raise METIS ("resolve_inference", s)))
+ handle TERM (s, _) =>
+ raise METIS_RECONSTRUCT ("resolve_inference", s)))
end
end
@@ -327,12 +328,12 @@
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
fun path_finder_fail tm ps t =
- raise METIS ("equality_inference (path_finder)",
- "path = " ^ space_implode " " (map string_of_int ps) ^
- " isa-term: " ^ Syntax.string_of_term ctxt tm ^
- (case t of
- SOME t => " fol-term: " ^ Metis_Term.toString t
- | NONE => ""))
+ raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
+ "path = " ^ space_implode " " (map string_of_int ps) ^
+ " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+ (case t of
+ SOME t => " fol-term: " ^ Metis_Term.toString t
+ | NONE => ""))
fun path_finder tm [] _ = (tm, Bound 0)
| path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
let
@@ -443,7 +444,7 @@
THEN ALLGOALS assume_tac
in
if length prems = length prems0 then
- raise METIS ("resynchronize", "Out of sync")
+ raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
else
Goal.prove ctxt [] [] goal (K tac)
|> resynchronize ctxt fol_th
--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Jan 14 09:59:50 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Jan 14 09:59:50 2013 +0100
@@ -134,6 +134,8 @@
| ord => ord
in {weight = weight, precedence = precedence} end
+exception METIS_UNPROVABLE of unit
+
(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
@@ -175,64 +177,68 @@
kbo_advisory_simp_ordering (ord_info ())
else
Metis_KnuthBendixOrder.default
+ fun fall_back () =
+ (verbose_warning ctxt
+ ("Falling back on " ^
+ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
+ FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0)
in
- case filter (fn t => prop_of t aconv @{prop False}) cls of
- false_th :: _ => [false_th RS @{thm FalseE}]
- | [] =>
- case Metis_Resolution.new (resolution_params ordering)
- {axioms = axioms |> map fst, conjecture = []}
- |> Metis_Resolution.loop of
- Metis_Resolution.Contradiction mth =>
- let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
- Metis_Thm.toString mth)
- val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
- (*add constraints arising from converting goal to clause form*)
- val proof = Metis_Proof.proof mth
- val result =
- axioms
- |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
- val used = proof |> map_filter (used_axioms axioms)
- val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
- val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
- val names = th_cls_pairs |> map fst
- val used_names =
- th_cls_pairs
- |> map_filter (fn (name, (_, cls)) =>
- if have_common_thm used cls then SOME name
- else NONE)
- val unused_names = names |> subtract (op =) used_names
- in
- if not (null cls) andalso not (have_common_thm used cls) then
- verbose_warning ctxt "The assumptions are inconsistent"
- else
- ();
- if not (null unused_names) then
- "Unused theorems: " ^ commas_quote unused_names
- |> verbose_warning ctxt
- else
- ();
- case result of
- (_,ith)::_ =>
- (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
- [discharge_skolem_premises ctxt dischargers ith])
- | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
- end
- | Metis_Resolution.Satisfiable _ =>
- (trace_msg ctxt (fn () =>
- "Metis: No first-order proof with the lemmas supplied");
- raise METIS ("FOL_SOLVE",
- "No first-order proof with the lemmas supplied"))
+ (case filter (fn t => prop_of t aconv @{prop False}) cls of
+ false_th :: _ => [false_th RS @{thm FalseE}]
+ | [] =>
+ case Metis_Resolution.new (resolution_params ordering)
+ {axioms = axioms |> map fst, conjecture = []}
+ |> Metis_Resolution.loop of
+ Metis_Resolution.Contradiction mth =>
+ let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
+ Metis_Thm.toString mth)
+ val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
+ (*add constraints arising from converting goal to clause form*)
+ val proof = Metis_Proof.proof mth
+ val result =
+ axioms
+ |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
+ val used = proof |> map_filter (used_axioms axioms)
+ val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
+ val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
+ val names = th_cls_pairs |> map fst
+ val used_names =
+ th_cls_pairs
+ |> map_filter (fn (name, (_, cls)) =>
+ if have_common_thm used cls then SOME name
+ else NONE)
+ val unused_names = names |> subtract (op =) used_names
+ in
+ if not (null cls) andalso not (have_common_thm used cls) then
+ verbose_warning ctxt "The assumptions are inconsistent"
+ else
+ ();
+ if not (null unused_names) then
+ "Unused theorems: " ^ commas_quote unused_names
+ |> verbose_warning ctxt
+ else
+ ();
+ case result of
+ (_,ith)::_ =>
+ (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
+ [discharge_skolem_premises ctxt dischargers ith])
+ | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
+ end
+ | Metis_Resolution.Satisfiable _ =>
+ (trace_msg ctxt (fn () =>
+ "Metis: No first-order proof with the supplied lemmas");
+ raise METIS_UNPROVABLE ()))
+ handle METIS_UNPROVABLE () =>
+ (case fallback_type_encs of
+ [] => []
+ | _ => fall_back ())
+ | METIS_RECONSTRUCT (loc, msg) =>
+ (case fallback_type_encs of
+ [] =>
+ (verbose_warning ctxt
+ ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); [])
+ | _ => fall_back ())
end
- handle METIS (loc, msg) =>
- case fallback_type_encs of
- [] => error ("Failed to replay Metis proof in Isabelle." ^
- (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
- else ""))
- | first_fallback :: _ =>
- (verbose_warning ctxt
- ("Falling back on " ^
- quote (metis_call first_fallback lam_trans) ^ "...");
- FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0)
fun neg_clausify ctxt combinators =
single