# HG changeset patch # User blanchet # Date 1304425420 -7200 # Node ID 552eae49f97d949dd23c41b413c865bb8275fe49 # Parent 1f45340b1e9197d9f739ff2beb83f03f6a45de76 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" diff -r 1f45340b1e91 -r 552eae49f97d src/HOL/Tools/Metis/metis_reconstruct.ML --- 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)) diff -r 1f45340b1e91 -r 552eae49f97d src/HOL/Tools/Metis/metis_tactics.ML --- 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 diff -r 1f45340b1e91 -r 552eae49f97d src/HOL/Tools/Metis/metis_translate.ML --- 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;