# HG changeset patch
# User blanchet
# Date 1269249907 -3600
# Node ID cac366550624b7f6cd13b8c0208f3c3a73d9ad32
# Parent  491a97039ce150ed52ed9b5cd5b0330c914ef708
start work on direct proof reconstruction for Sledgehammer

diff -r 491a97039ce1 -r cac366550624 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 22 10:25:07 2010 +0100
@@ -174,14 +174,14 @@
 val vampire_max_new_clauses = 60;
 val vampire_insert_theory_const = false;
 
-fun vampire_prover_config full : prover_config =
+fun vampire_prover_config isar : prover_config =
  {command = Path.explode "$VAMPIRE_HOME/vampire",
   arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
     " -t " ^ string_of_int timeout),
   failure_strs = vampire_failure_strs,
   max_new_clauses = vampire_max_new_clauses,
   insert_theory_const = vampire_insert_theory_const,
-  emit_structured_proof = full};
+  emit_structured_proof = isar};
 
 val vampire = tptp_prover ("vampire", vampire_prover_config false);
 val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
@@ -196,14 +196,14 @@
 val eprover_max_new_clauses = 100;
 val eprover_insert_theory_const = false;
 
-fun eprover_config full : prover_config =
+fun eprover_config isar : prover_config =
  {command = Path.explode "$E_HOME/eproof",
   arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
     " --silent --cpu-limit=" ^ string_of_int timeout),
   failure_strs = eprover_failure_strs,
   max_new_clauses = eprover_max_new_clauses,
   insert_theory_const = eprover_insert_theory_const,
-  emit_structured_proof = full};
+  emit_structured_proof = isar};
 
 val eprover = tptp_prover ("e", eprover_config false);
 val eprover_isar = tptp_prover ("e_isar", eprover_config true);
diff -r 491a97039ce1 -r cac366550624 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Mar 22 10:25:07 2010 +0100
@@ -463,7 +463,8 @@
 fun neg_skolemize_tac ctxt =
   EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
 
-val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
+val neg_clausify =
+  Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf;
 
 fun neg_conjecture_clauses ctxt st0 n =
   let
diff -r 491a97039ce1 -r cac366550624 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 22 10:25:07 2010 +0100
@@ -333,26 +333,30 @@
             then SOME ctm else perm ctms
   in perm end;
 
-fun have_or_show "show " _ = "show \""
-  | have_or_show have lname = have ^ lname ^ ": \""
-
 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
   ATP may have their literals reordered.*)
-fun isar_lines ctxt ctms =
-  let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
-      val _ = trace_proof_msg (K "\n\nisar_lines: start\n")
-      fun doline _ (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"
-              | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
-        | doline have (lname, t, deps) =
-            have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
-            "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
-      fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
-        | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
-  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
+fun isar_proof_body ctxt ctms =
+  let
+    val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
+    val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
+    fun have_or_show "show" _ = "show \""
+      | have_or_show have lname = have ^ " " ^ lname ^ ": \""
+    fun do_line _ (lname, t, []) =
+       (* No deps: it's a conjecture clause, with no proof. *)
+       (case permuted_clause t ctms of
+          SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+        | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
+                              [t]))
+      | do_line have (lname, t, deps) =
+        have_or_show have lname ^
+        string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
+        "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
+    fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
+      | do_lines ((lname, t, deps) :: lines) =
+        do_line "have" (lname, t, deps) :: do_lines lines
+  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
 
-fun notequal t (_,t',_) = not (t aconv t');
+fun unequal t (_, t', _) = not (t aconv t');
 
 (*No "real" literals means only type information*)
 fun eq_types t = t aconv HOLogic.true_const;
@@ -368,7 +372,7 @@
       if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
       then map (replace_deps (lno, [])) lines
       else
-       (case take_prefix (notequal t) lines of
+       (case take_prefix (unequal t) lines of
            (_,[]) => lines                  (*no repetition of proof line*)
          | (pre, (lno', _, _) :: post) =>   (*repetition: replace later line by earlier one*)
              pre @ map (replace_deps (lno', [lno])) post)
@@ -378,7 +382,7 @@
       if eq_types t then (lno, t, deps) :: lines
       (*Type information will be deleted later; skip repetition test.*)
       else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
-      case take_prefix (notequal t) lines of
+      case take_prefix (unequal t) lines of
          (_,[]) => (lno, t, deps) :: lines  (*no repetition of proof line*)
        | (pre, (lno', t', _) :: post) =>
            (lno, t', deps) ::               (*repetition: replace later line by earlier one*)
@@ -450,10 +454,10 @@
     val ccls = map forall_intr_vars ccls
     val _ = app (fn th => trace_proof_msg
                               (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
-    val isar_lines = isar_lines ctxt (map prop_of ccls)
-                                (stringify_deps thm_names [] lines)
+    val body = isar_proof_body ctxt (map prop_of ccls)
+                               (stringify_deps thm_names [] lines)
     val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
-  in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end
+  in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
   handle STREE _ => error "Could not extract proof (ATP output malformed?)";
 
 
diff -r 491a97039ce1 -r cac366550624 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/meson.ML	Mon Mar 22 10:25:07 2010 +0100
@@ -18,6 +18,7 @@
   val make_nnf: Proof.context -> thm -> thm
   val skolemize: Proof.context -> thm -> thm
   val is_fol_term: theory -> term -> bool
+  val make_clauses_unsorted: thm list -> thm list
   val make_clauses: thm list -> thm list
   val make_horns: thm list -> thm list
   val best_prolog_tac: (thm -> int) -> thm list -> tactic
@@ -560,7 +561,8 @@
 
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
-fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
+fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
+val make_clauses = sort_clauses o make_clauses_unsorted;
 
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =