# HG changeset patch
# User blanchet
# Date 1283375087 -7200
# Node ID f1b465f889b5d002642f1d477966fa41122b9f7a
# Parent  c2aebd79981f20527cc04743089fda4943ec2bf3
translate the axioms to FOF once and for all ATPs

diff -r c2aebd79981f -r f1b465f889b5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 01 22:33:31 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 01 23:04:47 2010 +0200
@@ -319,7 +319,10 @@
       Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
           (the_default default_max_relevant max_relevant)
           relevance_override chained_ths hyp_ts concl_t
-    val problem = {ctxt = ctxt', goal = goal, subgoal = i, axioms = axioms}
+    val problem =
+      {ctxt = ctxt', goal = goal, subgoal = i,
+       axiom_ts = map (prop_of o snd) axioms,
+       prepared_axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
     val time_limit =
       (case hard_timeout of
         NONE => I
diff -r c2aebd79981f -r f1b465f889b5 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 22:33:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:04:47 2010 +0200
@@ -11,6 +11,7 @@
   type failure = ATP_Systems.failure
   type locality = Sledgehammer_Filter.locality
   type relevance_override = Sledgehammer_Filter.relevance_override
+  type fol_formula = Sledgehammer_Translate.fol_formula
   type minimize_command = Sledgehammer_Reconstruct.minimize_command
   type params =
     {blocking: bool,
@@ -30,7 +31,8 @@
     {ctxt: Proof.context,
      goal: thm,
      subgoal: int,
-     axioms: ((string * locality) * thm) list}
+     axiom_ts: term list,
+     prepared_axioms: ((string * locality) * fol_formula) option list}
   type prover_result =
     {outcome: failure option,
      message: string,
@@ -99,7 +101,8 @@
   {ctxt: Proof.context,
    goal: thm,
    subgoal: int,
-   axioms: ((string * locality) * thm) list}
+   axiom_ts: term list,
+   prepared_axioms: ((string * locality) * fol_formula) option list}
 
 type prover_result =
   {outcome: failure option,
@@ -217,11 +220,13 @@
          use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
           max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
-        minimize_command ({ctxt, goal, subgoal, axioms} : problem) =
+        minimize_command
+        ({ctxt, goal, subgoal, axiom_ts, prepared_axioms} : problem) =
   let
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     val max_relevant = the_default default_max_relevant max_relevant
-    val axioms = take max_relevant axioms
+    val axiom_ts = take max_relevant axiom_ts
+    val prepared_axioms = take max_relevant prepared_axioms
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
                        else Config.get ctxt dest_dir
@@ -283,7 +288,8 @@
             val readable_names = debug andalso overlord
             val (problem, pool, conjecture_offset, axiom_names) =
               prepare_problem ctxt readable_names explicit_forall full_types
-                              explicit_apply hyp_ts concl_t axioms
+                              explicit_apply hyp_ts concl_t axiom_ts
+                              prepared_axioms
             val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
                                               problem
             val _ = File.write_list probfile ss
@@ -360,7 +366,10 @@
          "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
     fun run () =
       let
-        val problem = {ctxt = ctxt, goal = goal, subgoal = i, axioms = axioms}
+        val problem =
+          {ctxt = ctxt, goal = goal, subgoal = i,
+           axiom_ts = map (prop_of o snd) axioms,
+           prepared_axioms = map (prepare_axiom ctxt) axioms}
         val (outcome_code, message) =
           prover_fun atp_name prover params (minimize_command atp_name) problem
           |> (fn {outcome, message, ...} =>
diff -r c2aebd79981f -r f1b465f889b5 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 22:33:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 23:04:47 2010 +0200
@@ -23,6 +23,7 @@
 open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Filter
+open Sledgehammer_Translate
 open Sledgehammer_Reconstruct
 open Sledgehammer
 
@@ -57,7 +58,10 @@
        isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
     val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
     val {context = ctxt, goal, ...} = Proof.goal state
-    val problem = {ctxt = ctxt, goal = goal, subgoal = subgoal, axioms = axioms}
+    val problem =
+      {ctxt = ctxt, goal = goal, subgoal = subgoal,
+       axiom_ts = map (prop_of o snd) axioms,
+       prepared_axioms = map (prepare_axiom ctxt) axioms}
     val result as {outcome, used_thm_names, ...} = prover params (K "") problem
   in
     priority (case outcome of
diff -r c2aebd79981f -r f1b465f889b5 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Sep 01 22:33:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Sep 01 23:04:47 2010 +0200
@@ -9,6 +9,7 @@
 signature SLEDGEHAMMER_TRANSLATE =
 sig
   type 'a problem = 'a ATP_Problem.problem
+  type fol_formula
 
   val axiom_prefix : string
   val conjecture_prefix : string
@@ -16,9 +17,11 @@
   val class_rel_clause_prefix : string
   val arity_clause_prefix : string
   val tfrees_name : string
+  val prepare_axiom :
+    Proof.context -> (string * 'a) * thm -> ((string * 'a) * fol_formula) option
   val prepare_problem :
     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
-    -> ((string * 'a) * thm) list
+    -> term list -> ((string * 'a) * fol_formula) option list
     -> string problem * string Symtab.table * int * (string * 'a) list vector
 end;
 
@@ -246,10 +249,11 @@
     |> map_filter (Option.map snd o make_axiom ctxt false)
   end
 
-fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs =
+fun prepare_axiom ctxt = make_axiom ctxt true
+
+fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_axioms =
   let
     val thy = ProofContext.theory_of ctxt
-    val axiom_ts = map (prop_of o snd) axiom_pairs
     val hyp_ts =
       (* Remove existing axioms from the conjecture, as this can dramatically
          boost an ATP's performance (for some reason). *)
@@ -261,8 +265,7 @@
     val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
     (* TFrees in the conjecture; TVars in the axioms *)
     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
-    val (axiom_names, axioms) =
-      ListPair.unzip (map_filter (make_axiom ctxt true) axiom_pairs)
+    val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
@@ -495,12 +498,12 @@
       (const_table_for_problem explicit_apply problem) problem
 
 fun prepare_problem ctxt readable_names explicit_forall full_types
-                    explicit_apply hyp_ts concl_t axiom_pairs =
+                    explicit_apply hyp_ts concl_t axiom_ts prepared_axioms =
   let
     val thy = ProofContext.theory_of ctxt
     val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
                        arity_clauses)) =
-      prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs
+      prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_axioms
     val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
     val helper_lines =
       map (problem_line_for_fact helper_prefix full_types) helper_facts