author paulson Wed, 19 Mar 2008 18:10:23 +0100 changeset 26333 68e5eee47a45 parent 26332 aa54cd3ddc9f child 26334 80ec6cf82d95
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts Sledgehammer no longer produces structured proofs by default.
 NEWS file | annotate | diff | comparison | revisions src/HOL/MetisExamples/BigO.thy file | annotate | diff | comparison | revisions src/HOL/MetisExamples/set.thy file | annotate | diff | comparison | revisions src/HOL/Tools/res_reconstruct.ML file | annotate | diff | comparison | revisions
```--- a/NEWS	Wed Mar 19 14:25:59 2008 +0100
+++ b/NEWS	Wed Mar 19 18:10:23 2008 +0100
@@ -132,6 +132,10 @@
* Metis prover is now an order of magnitude faster, and also works

+* Sledgehammer no longer produces structured proofs by default. To enable,
+declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus,
+reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts.
+INCOMPATIBILITY.

*** ZF ***
```
```--- a/src/HOL/MetisExamples/BigO.thy	Wed Mar 19 14:25:59 2008 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Wed Mar 19 18:10:23 2008 +0100
@@ -31,7 +31,7 @@

(*** Now various verions with an increasing modulus ***)

-declare [[reconstruction_modulus = 1]]
+declare [[sledgehammer_modulus = 1]]

lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -100,7 +100,7 @@
by (metis abs_le_iff 5 18 14)
qed

-declare [[reconstruction_modulus = 2]]
+declare [[sledgehammer_modulus = 2]]

lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -141,7 +141,7 @@
by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
qed

-declare [[reconstruction_modulus = 3]]
+declare [[sledgehammer_modulus = 3]]

lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -173,7 +173,7 @@
qed

-declare [[reconstruction_modulus = 1]]
+declare [[sledgehammer_modulus = 1]]

lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -209,7 +209,7 @@
qed

-declare [[reconstruction_sorts = true]]
+declare [[sledgehammer_sorts = true]]

lemma bigo_alt_def: "O(f) =
{h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"```
```--- a/src/HOL/MetisExamples/set.thy	Wed Mar 19 14:25:59 2008 +0100
+++ b/src/HOL/MetisExamples/set.thy	Wed Mar 19 18:10:23 2008 +0100
@@ -20,7 +20,8 @@
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis

-declare [[reconstruction_modulus = 1]]
+declare [[sledgehammer_full = true]]
+declare [[sledgehammer_modulus = 1]]

(*multiple versions of this example*)
lemma (*equal_union: *)
@@ -90,7 +91,7 @@
by (metis 31 29)
qed

-declare [[reconstruction_modulus = 2]]
+declare [[sledgehammer_modulus = 2]]

lemma (*equal_union: *)
"(X = Y \<union> Z) =
@@ -133,7 +134,7 @@
by (metis 18 17)
qed

-declare [[reconstruction_modulus = 3]]
+declare [[sledgehammer_modulus = 3]]

lemma (*equal_union: *)
"(X = Y \<union> Z) =
@@ -168,7 +169,7 @@

(*Example included in TPHOLs paper*)

-declare [[reconstruction_modulus = 4]]
+declare [[sledgehammer_modulus = 4]]

lemma (*equal_union: *)
"(X = Y \<union> Z) =```
```--- a/src/HOL/Tools/res_reconstruct.ML	Wed Mar 19 14:25:59 2008 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Mar 19 18:10:23 2008 +0100
@@ -38,13 +38,18 @@
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
else ();

+val string_of_thm = PrintMode.setmp [] string_of_thm;
+
(*For generating structured proofs: keep every nth proof line*)
-val (modulus, modulus_setup) = Attrib.config_int "reconstruction_modulus" 1;
+val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;

(*Indicates whether to include sort information in generated proofs*)
-val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "reconstruction_sorts" true;
+val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;

-val setup = modulus_setup #> recon_sorts_setup;
+(*Indicates whether to generate full proofs or just lemma lists*)
+val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false;
+
+val setup = modulus_setup #> recon_sorts_setup #> full_proofs_setup;

datatype atp = E | SPASS | Vampire;

@@ -352,6 +357,7 @@
ATP may have their literals reordered.*)
fun isar_lines ctxt ctms =
let val string_of = Syntax.string_of_term ctxt
+      val _ = trace ("\n\nisar_lines: start\n")
fun doline have (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
(case permuted_clause t ctms of
SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
@@ -440,22 +446,29 @@
| isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";

fun decode_tstp_file cnfs ctxt th sgno thm_names =
-  let val tuples = map (dest_tstp o tstp_line o explode) cnfs
+  let val _ = trace "\ndecode_tstp_file: start\n"
+      val tuples = map (dest_tstp o tstp_line o explode) cnfs
+      val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n")
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
-      val nonnull_lines =
-                    (foldr add_prfline [] (decode_tstp_list ctxt tuples))
+      val raw_lines = foldr add_prfline [] (decode_tstp_list ctxt tuples)
+      val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n")
+      val nonnull_lines = foldr add_nonnull_prfline [] raw_lines
+      val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
val (_,lines) = foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
+      val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
+      val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
+      val _ = if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm th)) ccls
+              else ()
+      val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
+      val _ = trace "\ndecode_tstp_file: finishing\n"
in
-    app (fn th => Output.debug (fn () => string_of_thm th)) ccls;
-    isar_header (map #1 fixes) ^
-    String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)) ^
-    "qed\n"
+    isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
end
handle e => (*FIXME: exn handler is too general!*)
-    "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e;
+    let val msg = "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e
+    in  trace msg; msg  end;

(*Could use split_lines, but it can return blank lines...*)
val lines = String.tokens (equal #"\n");
@@ -552,15 +565,20 @@

(*The signal handler in watcher.ML must be able to read the output of this.*)
fun lemma_list atp proofextract thm_names probfile toParent ppid =
+ (trace "\nlemma_list: ready to signal success";
signal_success probfile toParent ppid
-                 (metis_line (nochained (get_axiom_names_for atp proofextract thm_names)));
+                 (metis_line (nochained (get_axiom_names_for atp proofextract thm_names))));

fun tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno =
-  let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
+  let val _ = trace "\nAttempting to extract structured proof from TSTP\n"
+      val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
+      val _ = trace (Int.toString (length cnfs) ^ " cnfs found")
val names = get_axiom_names_tstp proofextract thm_names
val line1 = metis_line (nochained names)
+      val _ = trace ("\nExtracted one-line proof: " ^ line1)
val line2 = if chained_hint mem_string names then ""
else decode_tstp_file cnfs ctxt th sgno thm_names
+      val _ = trace "\ntstp_extract: ready to signal success"
in
signal_success probfile toParent ppid (line1 ^ "\n" ^ line2)
end;
@@ -599,7 +617,7 @@
if any_substring [endS,end_TSTP] thisLine
then
(trace ("\nExtracted proof:\n" ^ proofextract);
-	       if String.isPrefix "cnf(" proofextract
+	       if Config.get ctxt full_proofs andalso String.isPrefix "cnf(" proofextract
then tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno
else lemma_list atp proofextract thm_names probfile toParent ppid;
true)```