reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 03 08:52:32 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 03 14:23:40 2011 +0200
@@ -11,6 +11,8 @@
sig
type mode = Metis_Translate.mode
+ exception METIS of string * string
+
val trace : bool Config.T
val trace_msg : Proof.context -> (unit -> string) -> unit
val verbose : bool Config.T
@@ -30,12 +32,14 @@
open Metis_Translate
+exception METIS of string * string
+
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
fun verbose_warning ctxt msg =
- if Config.get ctxt verbose then warning msg else ()
+ if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
datatype term_or_type = SomeTerm of term | SomeType of typ
@@ -305,8 +309,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, _, _) =>
- error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
+ handle THM (msg, _, _) => raise METIS ("inst_inf", msg)
+ | ERROR msg => raise METIS ("inst_inf", msg)
(* INFERENCE RULE: RESOLVE *)
@@ -423,8 +427,7 @@
val _ = trace_msg ctxt (fn () => " index_th2: " ^ string_of_int index_th2)
in
resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
- handle TERM (s, _) => error ("Cannot replay Metis proof in Isabelle:\n" ^
- "resolve_inf: " ^ s)
+ handle TERM (s, _) => raise METIS ("resolve_inf", s)
end
end;
@@ -467,10 +470,10 @@
val p' = if adjustment > p then p else p-adjustment
val tm_p = nth args p'
handle Subscript =>
- error ("Cannot replay Metis proof in Isabelle:\n" ^
- "equality_inf: " ^ string_of_int p ^ " adj " ^
- string_of_int adjustment ^ " term " ^
- Syntax.string_of_term ctxt tm)
+ raise METIS ("equality_inf",
+ string_of_int p ^ " adj " ^
+ string_of_int adjustment ^ " term " ^
+ Syntax.string_of_term ctxt tm)
val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
" " ^ Syntax.string_of_term ctxt tm_p)
val (r,t) = path_finder_FO tm_p ps
@@ -585,7 +588,7 @@
val goal = Logic.list_implies (prems, concl)
in
if length prems = length prems0 then
- error "Cannot replay Metis proof in Isabelle: Out of sync."
+ raise METIS ("resynchronize", "Out of sync")
else
Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1
THEN ALLGOALS assume_tac))
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 03 08:52:32 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 03 14:23:40 2011 +0200
@@ -101,12 +101,11 @@
if have_common_thm used cls then NONE else SOME name)
in
if not (null cls) andalso not (have_common_thm used cls) then
- verbose_warning ctxt "Metis: The assumptions are inconsistent"
+ verbose_warning ctxt "The assumptions are inconsistent"
else
();
if not (null unused) then
- verbose_warning ctxt ("Metis: Unused theorems: " ^
- commas_quote unused)
+ verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused)
else
();
case result of
@@ -117,6 +116,11 @@
end
| Metis_Resolution.Satisfiable _ =>
(trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
+ if mode <> FT then
+ raise METIS ("FOL_SOLVE",
+ "No first-order proof with the lemmas supplied")
+ else
+ ();
[])
end;
@@ -153,16 +157,21 @@
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type type_has_top_sort (prop_of st0) then
- (verbose_warning ctxt "Metis: Proof state contains the universal sort {}";
+ (verbose_warning ctxt "Proof state contains the universal sort {}";
Seq.empty)
else
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
- handle ERROR message =>
- error (message |> mode <> FT
- ? suffix "\nHint: You might want to try out \
- \\"metisFT\".")
+ handle METIS (loc, msg) =>
+ if mode <> FT then
+ (verbose_warning ctxt ("Falling back on \"metisFT\".");
+ generic_metis_tac FT ctxt ths i st0)
+ else
+ error ("Failed to replay Metis proof in Isabelle." ^
+ (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
+ else ""))
+
end
val metis_tac = generic_metis_tac HO
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 03 08:52:32 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 03 14:23:40 2011 +0200
@@ -10,6 +10,7 @@
signature METIS_TRANSLATE =
sig
type name = string * string
+
datatype type_literal =
TyLitVar of name * name |
TyLitFree of name * name
@@ -199,7 +200,7 @@
(*Remove the initial ' character from a type variable, if it is present*)
fun trim_type_var s =
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
- else error ("trim_type: Malformed type variable encountered: " ^ s);
+ else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
fun ascii_of_indexname (v,0) = ascii_of v
| ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i;