finished renaming
authorblanchet
Tue Aug 31 23:50:59 2010 +0200 (2010-08-31)
changeset 38988483879af0643
parent 38987 96fae8916d8b
child 38989 e34b099e477e
finished renaming
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 31 23:50:40 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 31 23:50:59 2010 +0200
     1.3 @@ -290,7 +290,7 @@
     1.4      | NONE => get_prover (default_atp_name ()))
     1.5    end
     1.6  
     1.7 -type locality = Sledgehammer_Fact_Filter.locality
     1.8 +type locality = Sledgehammer_Filter.locality
     1.9  
    1.10  local
    1.11  
    1.12 @@ -357,7 +357,7 @@
    1.13      case result of
    1.14        SH_OK (time_isa, time_atp, names) =>
    1.15          let
    1.16 -          fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE
    1.17 +          fun get_thms (name, Sledgehammer_Filter.Chained) = NONE
    1.18              | get_thms (name, loc) =
    1.19                SOME ((name, loc), thms_of_name (Proof.context_of st) name)
    1.20          in
    1.21 @@ -396,7 +396,7 @@
    1.22      val params = Sledgehammer_Isar.default_params thy
    1.23        [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
    1.24      val minimize =
    1.25 -      Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
    1.26 +      Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st)
    1.27      val _ = log separator
    1.28    in
    1.29      case minimize st (these (!named_thms)) of
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 23:50:40 2010 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 23:50:59 2010 +0200
     2.3 @@ -6,21 +6,20 @@
     2.4  struct
     2.5  
     2.6  val relevance_filter_args =
     2.7 -  [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
     2.8 -   ("higher_order_irrel_weight",
     2.9 -    Sledgehammer_Fact_Filter.higher_order_irrel_weight),
    2.10 -   ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
    2.11 -   ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
    2.12 -   ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
    2.13 -   ("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus),
    2.14 -   ("elim_bonus", Sledgehammer_Fact_Filter.elim_bonus),
    2.15 -   ("simp_bonus", Sledgehammer_Fact_Filter.simp_bonus),
    2.16 -   ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
    2.17 -   ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
    2.18 -   ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
    2.19 -   ("max_imperfect_exp", Sledgehammer_Fact_Filter.max_imperfect_exp),
    2.20 -   ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor),
    2.21 -   ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold)]
    2.22 +  [("worse_irrel_freq", Sledgehammer_Filter.worse_irrel_freq),
    2.23 +   ("higher_order_irrel_weight", Sledgehammer_Filter.higher_order_irrel_weight),
    2.24 +   ("abs_rel_weight", Sledgehammer_Filter.abs_rel_weight),
    2.25 +   ("abs_irrel_weight", Sledgehammer_Filter.abs_irrel_weight),
    2.26 +   ("skolem_irrel_weight", Sledgehammer_Filter.skolem_irrel_weight),
    2.27 +   ("intro_bonus", Sledgehammer_Filter.intro_bonus),
    2.28 +   ("elim_bonus", Sledgehammer_Filter.elim_bonus),
    2.29 +   ("simp_bonus", Sledgehammer_Filter.simp_bonus),
    2.30 +   ("local_bonus", Sledgehammer_Filter.local_bonus),
    2.31 +   ("chained_bonus", Sledgehammer_Filter.chained_bonus),
    2.32 +   ("max_imperfect", Sledgehammer_Filter.max_imperfect),
    2.33 +   ("max_imperfect_exp", Sledgehammer_Filter.max_imperfect_exp),
    2.34 +   ("threshold_divisor", Sledgehammer_Filter.threshold_divisor),
    2.35 +   ("ridiculous_threshold", Sledgehammer_Filter.ridiculous_threshold)]
    2.36  
    2.37  structure Prooftab =
    2.38    Table(type key = int * int val ord = prod_ord int_ord int_ord);
    2.39 @@ -104,7 +103,7 @@
    2.40           val subgoal = 1
    2.41           val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
    2.42           val facts =
    2.43 -           Sledgehammer_Fact_Filter.relevant_facts ctxt full_types
    2.44 +           Sledgehammer_Filter.relevant_facts ctxt full_types
    2.45                 relevance_thresholds
    2.46                 (the_default default_max_relevant max_relevant)
    2.47                 (the_default false theory_relevant)
     3.1 --- a/src/HOL/Sledgehammer.thy	Tue Aug 31 23:50:40 2010 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Tue Aug 31 23:50:59 2010 +0200
     3.3 @@ -19,11 +19,11 @@
     3.4    ("Tools/Sledgehammer/metis_clauses.ML")
     3.5    ("Tools/Sledgehammer/metis_tactics.ML")
     3.6    ("Tools/Sledgehammer/sledgehammer_util.ML")
     3.7 -  ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     3.8 +  ("Tools/Sledgehammer/sledgehammer_filter.ML")
     3.9    ("Tools/Sledgehammer/sledgehammer_translate.ML")
    3.10 -  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    3.11 +  ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
    3.12    ("Tools/Sledgehammer/sledgehammer.ML")
    3.13 -  ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
    3.14 +  ("Tools/Sledgehammer/sledgehammer_minimize.ML")
    3.15    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    3.16  begin
    3.17  
    3.18 @@ -103,12 +103,12 @@
    3.19  use "Tools/Sledgehammer/metis_tactics.ML"
    3.20  
    3.21  use "Tools/Sledgehammer/sledgehammer_util.ML"
    3.22 -use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    3.23 +use "Tools/Sledgehammer/sledgehammer_filter.ML"
    3.24  use "Tools/Sledgehammer/sledgehammer_translate.ML"
    3.25 -use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    3.26 +use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    3.27  use "Tools/Sledgehammer/sledgehammer.ML"
    3.28  setup Sledgehammer.setup
    3.29 -use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
    3.30 +use "Tools/Sledgehammer/sledgehammer_minimize.ML"
    3.31  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    3.32  setup Metis_Tactics.setup
    3.33  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 23:50:40 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 23:50:59 2010 +0200
     4.3 @@ -9,9 +9,9 @@
     4.4  signature SLEDGEHAMMER =
     4.5  sig
     4.6    type failure = ATP_Systems.failure
     4.7 -  type locality = Sledgehammer_Fact_Filter.locality
     4.8 -  type relevance_override = Sledgehammer_Fact_Filter.relevance_override
     4.9 -  type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    4.10 +  type locality = Sledgehammer_Filter.locality
    4.11 +  type relevance_override = Sledgehammer_Filter.relevance_override
    4.12 +  type minimize_command = Sledgehammer_Reconstruct.minimize_command
    4.13    type params =
    4.14      {blocking: bool,
    4.15       debug: bool,
    4.16 @@ -64,9 +64,9 @@
    4.17  open ATP_Systems
    4.18  open Metis_Clauses
    4.19  open Sledgehammer_Util
    4.20 -open Sledgehammer_Fact_Filter
    4.21 +open Sledgehammer_Filter
    4.22  open Sledgehammer_Translate
    4.23 -open Sledgehammer_Proof_Reconstruct
    4.24 +open Sledgehammer_Reconstruct
    4.25  
    4.26  
    4.27  (** The Sledgehammer **)
    4.28 @@ -179,7 +179,7 @@
    4.29    #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
    4.30    #> explode #> parse_clause_formula_relation #> fst
    4.31  
    4.32 -(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *)
    4.33 +(* TODO: move to "Sledgehammer_Reconstruct" *)
    4.34  fun repair_conjecture_shape_and_theorem_names output conjecture_shape
    4.35                                                axiom_names =
    4.36    if String.isSubstring set_ClauseFormulaRelationN output then
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Aug 31 23:50:40 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Aug 31 23:50:59 2010 +0200
     5.3 @@ -1,9 +1,9 @@
     5.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     5.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     5.6      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     5.7      Author:     Jasmin Blanchette, TU Muenchen
     5.8  *)
     5.9  
    5.10 -signature SLEDGEHAMMER_FACT_FILTER =
    5.11 +signature SLEDGEHAMMER_FILTER =
    5.12  sig
    5.13    datatype locality = General | Intro | Elim | Simp | Local | Chained
    5.14  
    5.15 @@ -35,7 +35,7 @@
    5.16      -> thm list -> term list -> term -> ((string * locality) * thm) list
    5.17  end;
    5.18  
    5.19 -structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    5.20 +structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
    5.21  struct
    5.22  
    5.23  open Sledgehammer_Util
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 23:50:40 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 23:50:59 2010 +0200
     6.3 @@ -20,7 +20,7 @@
     6.4  open ATP_Systems
     6.5  open Sledgehammer_Util
     6.6  open Sledgehammer
     6.7 -open Sledgehammer_Fact_Minimize
     6.8 +open Sledgehammer_Minimize
     6.9  
    6.10  (** Sledgehammer commands **)
    6.11  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 31 23:50:40 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 31 23:50:59 2010 +0200
     7.3 @@ -1,13 +1,13 @@
     7.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
     7.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     7.6      Author:     Philipp Meyer, TU Muenchen
     7.7      Author:     Jasmin Blanchette, TU Muenchen
     7.8  
     7.9  Minimization of theorem list for Metis using automatic theorem provers.
    7.10  *)
    7.11  
    7.12 -signature SLEDGEHAMMER_FACT_MINIMIZE =
    7.13 +signature SLEDGEHAMMER_MINIMIZE =
    7.14  sig
    7.15 -  type locality = Sledgehammer_Fact_Filter.locality
    7.16 +  type locality = Sledgehammer_Filter.locality
    7.17    type params = Sledgehammer.params
    7.18  
    7.19    val minimize_theorems :
    7.20 @@ -16,13 +16,13 @@
    7.21    val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
    7.22  end;
    7.23  
    7.24 -structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
    7.25 +structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
    7.26  struct
    7.27  
    7.28  open ATP_Systems
    7.29  open Sledgehammer_Util
    7.30 -open Sledgehammer_Fact_Filter
    7.31 -open Sledgehammer_Proof_Reconstruct
    7.32 +open Sledgehammer_Filter
    7.33 +open Sledgehammer_Reconstruct
    7.34  open Sledgehammer
    7.35  
    7.36  (* wrapper for calling external prover *)
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Aug 31 23:50:40 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Aug 31 23:50:59 2010 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     8.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     8.6      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     8.7      Author:     Claire Quigley, Cambridge University Computer Laboratory
     8.8      Author:     Jasmin Blanchette, TU Muenchen
     8.9 @@ -6,9 +6,9 @@
    8.10  Transfer of proofs from external provers.
    8.11  *)
    8.12  
    8.13 -signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
    8.14 +signature SLEDGEHAMMER_RECONSTRUCT =
    8.15  sig
    8.16 -  type locality = Sledgehammer_Fact_Filter.locality
    8.17 +  type locality = Sledgehammer_Filter.locality
    8.18    type minimize_command = string list -> string
    8.19    type metis_params =
    8.20      bool * minimize_command * string * (string * locality) list vector * thm
    8.21 @@ -22,13 +22,13 @@
    8.22    val proof_text : bool -> isar_params -> metis_params -> text_result
    8.23  end;
    8.24  
    8.25 -structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    8.26 +structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
    8.27  struct
    8.28  
    8.29  open ATP_Problem
    8.30  open Metis_Clauses
    8.31  open Sledgehammer_Util
    8.32 -open Sledgehammer_Fact_Filter
    8.33 +open Sledgehammer_Filter
    8.34  open Sledgehammer_Translate
    8.35  
    8.36  type minimize_command = string list -> string