--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 31 23:50:59 2010 +0200
@@ -290,7 +290,7 @@
| NONE => get_prover (default_atp_name ()))
end
-type locality = Sledgehammer_Fact_Filter.locality
+type locality = Sledgehammer_Filter.locality
local
@@ -357,7 +357,7 @@
case result of
SH_OK (time_isa, time_atp, names) =>
let
- fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE
+ fun get_thms (name, Sledgehammer_Filter.Chained) = NONE
| get_thms (name, loc) =
SOME ((name, loc), thms_of_name (Proof.context_of st) name)
in
@@ -396,7 +396,7 @@
val params = Sledgehammer_Isar.default_params thy
[("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
val minimize =
- Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
+ Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 31 23:50:59 2010 +0200
@@ -6,21 +6,20 @@
struct
val relevance_filter_args =
- [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
- ("higher_order_irrel_weight",
- Sledgehammer_Fact_Filter.higher_order_irrel_weight),
- ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
- ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
- ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
- ("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus),
- ("elim_bonus", Sledgehammer_Fact_Filter.elim_bonus),
- ("simp_bonus", Sledgehammer_Fact_Filter.simp_bonus),
- ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
- ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
- ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
- ("max_imperfect_exp", Sledgehammer_Fact_Filter.max_imperfect_exp),
- ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor),
- ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold)]
+ [("worse_irrel_freq", Sledgehammer_Filter.worse_irrel_freq),
+ ("higher_order_irrel_weight", Sledgehammer_Filter.higher_order_irrel_weight),
+ ("abs_rel_weight", Sledgehammer_Filter.abs_rel_weight),
+ ("abs_irrel_weight", Sledgehammer_Filter.abs_irrel_weight),
+ ("skolem_irrel_weight", Sledgehammer_Filter.skolem_irrel_weight),
+ ("intro_bonus", Sledgehammer_Filter.intro_bonus),
+ ("elim_bonus", Sledgehammer_Filter.elim_bonus),
+ ("simp_bonus", Sledgehammer_Filter.simp_bonus),
+ ("local_bonus", Sledgehammer_Filter.local_bonus),
+ ("chained_bonus", Sledgehammer_Filter.chained_bonus),
+ ("max_imperfect", Sledgehammer_Filter.max_imperfect),
+ ("max_imperfect_exp", Sledgehammer_Filter.max_imperfect_exp),
+ ("threshold_divisor", Sledgehammer_Filter.threshold_divisor),
+ ("ridiculous_threshold", Sledgehammer_Filter.ridiculous_threshold)]
structure Prooftab =
Table(type key = int * int val ord = prod_ord int_ord int_ord);
@@ -104,7 +103,7 @@
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
- Sledgehammer_Fact_Filter.relevant_facts ctxt full_types
+ Sledgehammer_Filter.relevant_facts ctxt full_types
relevance_thresholds
(the_default default_max_relevant max_relevant)
(the_default false theory_relevant)
--- a/src/HOL/Sledgehammer.thy Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Aug 31 23:50:59 2010 +0200
@@ -19,11 +19,11 @@
("Tools/Sledgehammer/metis_clauses.ML")
("Tools/Sledgehammer/metis_tactics.ML")
("Tools/Sledgehammer/sledgehammer_util.ML")
- ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+ ("Tools/Sledgehammer/sledgehammer_filter.ML")
("Tools/Sledgehammer/sledgehammer_translate.ML")
- ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
+ ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
("Tools/Sledgehammer/sledgehammer.ML")
- ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
+ ("Tools/Sledgehammer/sledgehammer_minimize.ML")
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
@@ -103,12 +103,12 @@
use "Tools/Sledgehammer/metis_tactics.ML"
use "Tools/Sledgehammer/sledgehammer_util.ML"
-use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+use "Tools/Sledgehammer/sledgehammer_filter.ML"
use "Tools/Sledgehammer/sledgehammer_translate.ML"
-use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
+use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
use "Tools/Sledgehammer/sledgehammer.ML"
setup Sledgehammer.setup
-use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
+use "Tools/Sledgehammer/sledgehammer_minimize.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
setup Metis_Tactics.setup
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 31 23:50:59 2010 +0200
@@ -9,9 +9,9 @@
signature SLEDGEHAMMER =
sig
type failure = ATP_Systems.failure
- type locality = Sledgehammer_Fact_Filter.locality
- type relevance_override = Sledgehammer_Fact_Filter.relevance_override
- type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
+ type locality = Sledgehammer_Filter.locality
+ type relevance_override = Sledgehammer_Filter.relevance_override
+ type minimize_command = Sledgehammer_Reconstruct.minimize_command
type params =
{blocking: bool,
debug: bool,
@@ -64,9 +64,9 @@
open ATP_Systems
open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
+open Sledgehammer_Filter
open Sledgehammer_Translate
-open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_Reconstruct
(** The Sledgehammer **)
@@ -179,7 +179,7 @@
#> snd #> Substring.string #> strip_spaces_except_between_ident_chars
#> explode #> parse_clause_formula_relation #> fst
-(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *)
+(* TODO: move to "Sledgehammer_Reconstruct" *)
fun repair_conjecture_shape_and_theorem_names output conjecture_shape
axiom_names =
if String.isSubstring set_ClauseFormulaRelationN output then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 31 23:50:59 2010 +0200
@@ -1,9 +1,9 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
*)
-signature SLEDGEHAMMER_FACT_FILTER =
+signature SLEDGEHAMMER_FILTER =
sig
datatype locality = General | Intro | Elim | Simp | Local | Chained
@@ -35,7 +35,7 @@
-> thm list -> term list -> term -> ((string * locality) * thm) list
end;
-structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
+structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
struct
open Sledgehammer_Util
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 23:50:59 2010 +0200
@@ -20,7 +20,7 @@
open ATP_Systems
open Sledgehammer_Util
open Sledgehammer
-open Sledgehammer_Fact_Minimize
+open Sledgehammer_Minimize
(** Sledgehammer commands **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 31 23:50:59 2010 +0200
@@ -1,13 +1,13 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
Author: Philipp Meyer, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Minimization of theorem list for Metis using automatic theorem provers.
*)
-signature SLEDGEHAMMER_FACT_MINIMIZE =
+signature SLEDGEHAMMER_MINIMIZE =
sig
- type locality = Sledgehammer_Fact_Filter.locality
+ type locality = Sledgehammer_Filter.locality
type params = Sledgehammer.params
val minimize_theorems :
@@ -16,13 +16,13 @@
val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
end;
-structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
+structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
struct
open ATP_Systems
open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_Filter
+open Sledgehammer_Reconstruct
open Sledgehammer
(* wrapper for calling external prover *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Aug 31 23:50:59 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Claire Quigley, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
@@ -6,9 +6,9 @@
Transfer of proofs from external provers.
*)
-signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
+signature SLEDGEHAMMER_RECONSTRUCT =
sig
- type locality = Sledgehammer_Fact_Filter.locality
+ type locality = Sledgehammer_Filter.locality
type minimize_command = string list -> string
type metis_params =
bool * minimize_command * string * (string * locality) list vector * thm
@@ -22,13 +22,13 @@
val proof_text : bool -> isar_params -> metis_params -> text_result
end;
-structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
+structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
struct
open ATP_Problem
open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
+open Sledgehammer_Filter
open Sledgehammer_Translate
type minimize_command = string list -> string