# HG changeset patch
# User blanchet
# Date 1287765105 -7200
# Node ID acb75271cdcefeccb9a08afab8f9ff625f83674c
# Parent  1f61f0826e8a85ddb43750acb855091c0caf8010
tuning

diff -r 1f61f0826e8a -r acb75271cdce src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 18:24:10 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 18:31:45 2010 +0200
@@ -364,7 +364,7 @@
     val problem =
       {state = st', goal = goal, subgoal = i,
        subgoal_count = Sledgehammer_Util.subgoal_count st,
-       axioms = axioms |> map Sledgehammer.Unprepared, only = true}
+       axioms = axioms |> map Sledgehammer.Untranslated, only = true}
     val time_limit =
       (case hard_timeout of
         NONE => I
diff -r 1f61f0826e8a -r acb75271cdce src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 18:24:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 18:31:45 2010 +0200
@@ -12,7 +12,7 @@
   type locality = Sledgehammer_Filter.locality
   type relevance_fudge = Sledgehammer_Filter.relevance_fudge
   type relevance_override = Sledgehammer_Filter.relevance_override
-  type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula
+  type translated_formula = Sledgehammer_ATP_Translate.translated_formula
   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
 
   type params =
@@ -31,8 +31,8 @@
      expect: string}
 
   datatype axiom =
-    Unprepared of (string * locality) * thm |
-    Prepared of term * ((string * locality) * prepared_formula) option
+    Untranslated of (string * locality) * thm |
+    Translated of term * ((string * locality) * translated_formula) option
 
   type prover_problem =
     {state: Proof.state,
@@ -195,8 +195,8 @@
    expect: string}
 
 datatype axiom =
-  Unprepared of (string * locality) * thm |
-  Prepared of term * ((string * locality) * prepared_formula) option
+  Untranslated of (string * locality) * thm |
+  Translated of term * ((string * locality) * translated_formula) option
 
 type prover_problem =
   {state: Proof.state,
@@ -250,10 +250,10 @@
 
 (* generic TPTP-based ATPs *)
 
-fun dest_Unprepared (Unprepared p) = p
-  | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared"
-fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
-  | prepared_axiom _ (Prepared p) = p
+fun dest_Untranslated (Untranslated p) = p
+  | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
+fun translated_axiom ctxt (Untranslated p) = translate_axiom ctxt p
+  | translated_axiom _ (Translated p) = p
 
 fun int_option_add (SOME m) (SOME n) = SOME (m + n)
   | int_option_add _ _ = NONE
@@ -275,7 +275,7 @@
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     val axioms =
       axioms |> not only ? take (the_default default_max_relevant max_relevant)
-             |> map (prepared_axiom ctxt)
+             |> map (translated_axiom ctxt)
     val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
                    else Config.get ctxt dest_dir
     val problem_prefix = Config.get ctxt problem_prefix
@@ -418,7 +418,7 @@
   let
     val {outcome, used_axioms, run_time_in_msecs} =
       saschas_run_smt_solver remote timeout state
-                             (map_filter (try dest_Unprepared) axioms) subgoal
+                             (map_filter (try dest_Untranslated) axioms) subgoal
     val message =
       if outcome = NONE then
         try_command_line (proof_banner false)
@@ -507,8 +507,8 @@
       val _ = () |> not blocking ? kill_provers
       val _ = if auto then () else priority "Sledgehammering..."
       val (smts, atps) = provers |> List.partition is_smt_prover
-      fun run_provers full_types irrelevant_consts relevance_fudge maybe_prepare
-                      provers (res as (success, state)) =
+      fun run_provers full_types irrelevant_consts relevance_fudge
+                      maybe_translate provers (res as (success, state)) =
         if success orelse null provers then
           res
         else
@@ -524,7 +524,7 @@
               relevant_facts ctxt full_types relevance_thresholds
                              max_max_relevant irrelevant_consts relevance_fudge
                              relevance_override chained_ths hyp_ts concl_t
-              |> map maybe_prepare
+              |> map maybe_translate
             val problem =
               {state = state, goal = goal, subgoal = i, subgoal_count = n,
                axioms = axioms, only = only}
@@ -541,9 +541,9 @@
           end
       val run_atps =
         run_provers full_types atp_irrelevant_consts atp_relevance_fudge
-                    (Prepared o prepare_axiom ctxt) atps
+                    (Translated o translate_axiom ctxt) atps
       val run_smts =
-        run_provers true smt_irrelevant_consts smt_relevance_fudge Unprepared
+        run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated
                     smts
       fun run_atps_and_smt_solvers () =
         [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
diff -r 1f61f0826e8a -r acb75271cdce src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 18:24:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 18:31:45 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Claire Quigley, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
diff -r 1f61f0826e8a -r acb75271cdce src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 18:24:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 18:31:45 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     Author:     Fabian Immler, TU Muenchen
     Author:     Makarius
     Author:     Jasmin Blanchette, TU Muenchen
@@ -9,16 +9,16 @@
 signature SLEDGEHAMMER_ATP_TRANSLATE =
 sig
   type 'a problem = 'a ATP_Problem.problem
-  type prepared_formula
+  type translated_formula
 
   val axiom_prefix : string
   val conjecture_prefix : string
-  val prepare_axiom :
+  val translate_axiom :
     Proof.context -> (string * 'a) * thm
-    -> term * ((string * 'a) * prepared_formula) option
+    -> term * ((string * 'a) * translated_formula) option
   val prepare_atp_problem :
     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
-    -> (term * ((string * 'a) * prepared_formula) option) list
+    -> (term * ((string * 'a) * translated_formula) option) list
     -> string problem * string Symtab.table * int * (string * 'a) list vector
 end;
 
@@ -39,7 +39,7 @@
 (* Freshness almost guaranteed! *)
 val sledgehammer_weak_prefix = "Sledgehammer:"
 
-type prepared_formula =
+type translated_formula =
   {name: string,
    kind: kind,
    combformula: (name, combterm) formula,
@@ -214,7 +214,7 @@
 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   | count_combformula (AConn (_, phis)) = fold count_combformula phis
   | count_combformula (AAtom tm) = count_combterm tm
-fun count_prepared_formula ({combformula, ...} : prepared_formula) =
+fun count_translated_formula ({combformula, ...} : translated_formula) =
   count_combformula combformula
 
 val optional_helpers =
@@ -235,7 +235,7 @@
 fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   let
     val ct =
-      fold (fold count_prepared_formula) [conjectures, axioms] init_counters
+      fold (fold count_translated_formula) [conjectures, axioms] init_counters
     fun is_needed c = the (Symtab.lookup ct c) > 0
     fun baptize th = ((Thm.get_name_hint th, false), th)
   in
@@ -247,12 +247,12 @@
     |> map_filter (Option.map snd o make_axiom ctxt false)
   end
 
-fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
+fun translate_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
 
-fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
+fun translate_formulas ctxt full_types hyp_ts concl_t axioms =
   let
     val thy = ProofContext.theory_of ctxt
-    val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
+    val (axiom_ts, translated_axioms) = ListPair.unzip axioms
     (* Remove existing axioms from the conjecture, as this can dramatically
        boost an ATP's performance (for some reason). *)
     val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
@@ -263,7 +263,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 I prepared_axioms)
+    val (axiom_names, axioms) = ListPair.unzip (map_filter I translated_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'
@@ -323,7 +323,7 @@
   in aux end
 
 fun formula_for_axiom full_types
-                      ({combformula, ctypes_sorts, ...} : prepared_formula) =
+                      ({combformula, ctypes_sorts, ...} : translated_formula) =
   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
                 (type_literals_for_types ctypes_sorts))
            (formula_for_combformula full_types combformula)
@@ -353,11 +353,12 @@
                      (fo_literal_for_arity_literal conclLit)))
 
 fun problem_line_for_conjecture full_types
-                           ({name, kind, combformula, ...} : prepared_formula) =
+        ({name, kind, combformula, ...} : translated_formula) =
   Fof (conjecture_prefix ^ name, kind,
        formula_for_combformula full_types combformula)
 
-fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : prepared_formula) =
+fun free_type_literals_for_conjecture
+        ({ctypes_sorts, ...} : translated_formula) =
   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_free_type j lit =
@@ -501,7 +502,7 @@
     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 axioms
+      translate_formulas ctxt full_types hyp_ts concl_t 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
diff -r 1f61f0826e8a -r acb75271cdce src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 18:24:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 18:31:45 2010 +0200
@@ -55,7 +55,7 @@
        max_relevant = NONE, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
     val axioms =
-      axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))
+      axioms |> maps (fn (n, ths) => ths |> map (Untranslated o pair n))
     val {goal, ...} = Proof.goal state
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,