# HG changeset patch # User blanchet # Date 1358153990 -3600 # Node ID bfb626265782a3a57f722b3d578821cbb1074776 # Parent 2eae85887282b744166fbaca92262e0f2f74eb2d less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2 diff -r 2eae85887282 -r bfb626265782 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r 2eae85887282 -r bfb626265782 src/HOL/Tools/Metis/metis_tactic.ML --- 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