# HG changeset patch
# User blanchet
# Date 1271940472 -7200
# Node ID 96f45c5ffb3683effe0677ce67754d2b1e9c973c
# Parent  fa6d03d42aab3c96a329b376d7397dc105a725c3
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing

diff -r fa6d03d42aab -r 96f45c5ffb36 src/HOL/Tools/ATP_Manager/SystemOnTPTP
--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Thu Apr 22 13:50:58 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Thu Apr 22 14:47:52 2010 +0200
@@ -123,7 +123,7 @@
   $extract =~ s/\)\.cnf/\)\.\ncnf/g;
 
   print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
-  # orientation for res_reconstruct.ML
+  # orientation for "sledgehammer_proof_reconstruct.ML"
   print "# SZS output start CNFRefutation.\n";
   print "$extract\n";
   print "# SZS output end CNFRefutation.\n";
diff -r fa6d03d42aab -r 96f45c5ffb36 src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Apr 22 13:50:58 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Apr 22 14:47:52 2010 +0200
@@ -122,8 +122,8 @@
             ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
         in
           (SOME min_thms,
-           proof_text isar_proof debug modulus sorts ctxt (K "") proof
-                      internal_thm_names goal i |> fst)
+           proof_text true isar_proof debug modulus sorts ctxt
+                      (K "", proof, internal_thm_names, goal, i) |> fst)
         end
     | (Timeout, _) =>
         (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
diff -r fa6d03d42aab -r 96f45c5ffb36 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 22 13:50:58 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 22 14:47:52 2010 +0200
@@ -72,8 +72,9 @@
   | (message :: _) => message
 
 fun generic_prover overlord get_facts prepare write_file cmd args known_failures
-        proof_text name ({debug, full_types, explicit_apply, ...} : params)
-        minimize_command
+        supports_isar_proofs name
+        ({debug, full_types, explicit_apply, isar_proof, modulus, sorts, ...}
+         : params) minimize_command
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -167,7 +168,8 @@
     val success = rc = 0 andalso failure = "";
     val (message, relevant_thm_names) =
       if success then
-        proof_text ctxt minimize_command proof internal_thm_names th subgoal
+        proof_text supports_isar_proofs isar_proof debug modulus sorts ctxt
+                   (minimize_command, proof, internal_thm_names, th, subgoal)
       else if failure <> "" then
         (failure ^ "\n", [])
       else
@@ -188,7 +190,7 @@
                 prefers_theory_relevant, supports_isar_proofs})
         (params as {debug, overlord, respect_no_atp, relevance_threshold,
                     convergence, theory_relevant, higher_order, follow_defs,
-                    isar_proof, modulus, sorts, ...})
+                    isar_proof, ...})
         minimize_command timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
@@ -196,8 +198,7 @@
                           (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order false)
       (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
-      (arguments timeout) known_failures
-      (proof_text (supports_isar_proofs andalso isar_proof) debug modulus sorts)
+      (arguments timeout) known_failures supports_isar_proofs
       name params minimize_command
 
 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
@@ -249,8 +250,8 @@
 (* SPASS *)
 
 fun generic_dfg_prover
-        (name, ({command, arguments, known_failures, max_new_clauses,
-                 prefers_theory_relevant, ...} : prover_config))
+        (name, {command, arguments, known_failures, max_new_clauses,
+                prefers_theory_relevant, supports_isar_proofs})
         (params as {overlord, respect_no_atp, relevance_threshold, convergence,
                     theory_relevant, higher_order, follow_defs, ...})
         minimize_command timeout =
@@ -259,8 +260,8 @@
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order true) write_dfg_file command
-      (arguments timeout) known_failures (K metis_proof_text)
-      name params minimize_command
+      (arguments timeout) known_failures supports_isar_proofs name params
+      minimize_command
 
 fun dfg_prover name p = (name, generic_dfg_prover (name, p))
 
diff -r fa6d03d42aab -r 96f45c5ffb36 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 22 13:50:58 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 22 14:47:52 2010 +0200
@@ -17,14 +17,16 @@
   val is_proof_well_formed: string -> bool
   val metis_line: int -> int -> string list -> string
   val metis_proof_text:
-    minimize_command -> string -> string vector -> thm -> int
+    minimize_command * string * string vector * thm * int
     -> string * string list
   val isar_proof_text:
-    bool -> int -> bool -> Proof.context -> minimize_command -> string
-    -> string vector -> thm -> int -> string * string list
+    bool -> int -> bool -> Proof.context
+    -> minimize_command * string * string vector * thm * int
+    -> string * string list
   val proof_text:
-    bool -> bool -> int -> bool -> Proof.context -> minimize_command -> string
-    -> string vector -> thm -> int -> string * string list
+    bool -> bool -> bool -> int -> bool -> Proof.context
+    -> minimize_command * string * string vector * thm * int
+    -> string * string list
 end;
 
 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -541,7 +543,7 @@
       "To minimize the number of lemmas, try this command: " ^
       Markup.markup Markup.sendback command ^ ".\n"
 
-fun metis_proof_text minimize_command proof thm_names goal i =
+fun metis_proof_text (minimize_command, proof, thm_names, goal, i) =
   let
     val lemmas =
       proof |> get_proof_extract
@@ -556,8 +558,8 @@
     (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas)
   end
 
-fun isar_proof_text debug modulus sorts ctxt minimize_command proof thm_names
-                    goal i =
+fun isar_proof_text debug modulus sorts ctxt
+                    (minimize_command, proof, thm_names, goal, i) =
   let
     (* We could use "split_lines", but it can return blank lines. *)
     val lines = String.tokens (equal #"\n");
@@ -566,7 +568,7 @@
     val extract = get_proof_extract proof
     val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
     val (one_line_proof, lemma_names) =
-      metis_proof_text minimize_command proof thm_names goal i
+      metis_proof_text (minimize_command, proof, thm_names, goal, i)
     val tokens = String.tokens (fn c => c = #" ") one_line_proof
     fun isar_proof_for () =
       case isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names of
@@ -580,11 +582,17 @@
         isar_proof_for ()
       else
         try isar_proof_for ()
-        |> the_default "Error: The Isar proof reconstruction failed."
+        |> the_default "Warning: The Isar proof construction failed.\n"
   in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof debug modulus sorts ctxt =
-  if isar_proof then isar_proof_text debug modulus sorts ctxt
-  else metis_proof_text
+fun proof_text supports_isar_proofs isar_proof debug modulus sorts ctxt params =
+  if isar_proof then
+    if supports_isar_proofs then
+      isar_proof_text debug modulus sorts ctxt params
+    else
+      metis_proof_text params
+      |>> suffix "(Isar proof output is not supported for this ATP.)\n"
+  else
+    metis_proof_text params
 
 end;