rename "ATP_Manager" ML module to "Sledgehammer";
authorblanchet
Tue Jul 27 17:56:01 2010 +0200 (2010-07-27)
changeset 38021e024504943d1
parent 38020 badd89633f4c
child 38022 d9c4d87838f3
rename "ATP_Manager" ML module to "Sledgehammer";
more refactoring to come
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 27 17:49:16 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 27 17:56:01 2010 +0200
     1.3 @@ -269,7 +269,6 @@
     1.4    $(SRC)/Provers/Arith/extract_common_term.ML \
     1.5    $(SRC)/Tools/Metis/metis.ML \
     1.6    Tools/ATP_Manager/async_manager.ML \
     1.7 -  Tools/ATP_Manager/atp_manager.ML \
     1.8    Tools/ATP_Manager/atp_problem.ML \
     1.9    Tools/ATP_Manager/atp_systems.ML \
    1.10    Tools/choice_specification.ML \
    1.11 @@ -320,6 +319,7 @@
    1.12    Tools/Sledgehammer/meson_tactic.ML \
    1.13    Tools/Sledgehammer/metis_clauses.ML \
    1.14    Tools/Sledgehammer/metis_tactics.ML \
    1.15 +  Tools/Sledgehammer/sledgehammer.ML \
    1.16    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
    1.17    Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
    1.18    Tools/Sledgehammer/sledgehammer_isar.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Tue Jul 27 17:49:16 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 17:56:01 2010 +0200
     2.3 @@ -97,7 +97,7 @@
     2.4  use "Tools/ATP_Manager/atp_problem.ML"
     2.5  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
     2.6  use "Tools/ATP_Manager/async_manager.ML"
     2.7 -use "Tools/ATP_Manager/atp_manager.ML"
     2.8 +use "Tools/Sledgehammer/sledgehammer.ML"
     2.9  use "Tools/ATP_Manager/atp_systems.ML"
    2.10  setup ATP_Systems.setup
    2.11  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:49:16 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:56:01 2010 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4  open Sledgehammer_Fact_Filter
     3.5  open ATP_Problem
     3.6  open Sledgehammer_Proof_Reconstruct
     3.7 -open ATP_Manager
     3.8 +open Sledgehammer
     3.9  
    3.10  val trace = Unsynchronized.ref false
    3.11  fun trace_msg msg = if !trace then tracing (msg ()) else ()
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 17:49:16 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 17:56:01 2010 +0200
     4.3 @@ -1,12 +1,12 @@
     4.4 -(*  Title:      HOL/Tools/ATP_Manager/atp_manager.ML
     4.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
     4.6      Author:     Fabian Immler, TU Muenchen
     4.7      Author:     Makarius
     4.8      Author:     Jasmin Blanchette, TU Muenchen
     4.9  
    4.10 -Central manager component for ATP threads.
    4.11 +Sledgehammer's heart.
    4.12  *)
    4.13  
    4.14 -signature ATP_MANAGER =
    4.15 +signature SLEDGEHAMMER =
    4.16  sig
    4.17    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
    4.18    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    4.19 @@ -59,7 +59,7 @@
    4.20      -> Proof.state -> string -> unit
    4.21  end;
    4.22  
    4.23 -structure ATP_Manager : ATP_MANAGER =
    4.24 +structure Sledgehammer : SLEDGEHAMMER =
    4.25  struct
    4.26  
    4.27  open Metis_Clauses
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 17:49:16 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 17:56:01 2010 +0200
     5.3 @@ -7,8 +7,8 @@
     5.4  
     5.5  signature SLEDGEHAMMER_FACT_MINIMIZER =
     5.6  sig
     5.7 -  type params = ATP_Manager.params
     5.8 -  type prover_result = ATP_Manager.prover_result
     5.9 +  type params = Sledgehammer.params
    5.10 +  type prover_result = Sledgehammer.prover_result
    5.11  
    5.12    val minimize_theorems :
    5.13      params -> int -> int -> Proof.state -> (string * thm list) list
    5.14 @@ -21,7 +21,7 @@
    5.15  open Metis_Clauses
    5.16  open Sledgehammer_Util
    5.17  open Sledgehammer_Proof_Reconstruct
    5.18 -open ATP_Manager
    5.19 +open Sledgehammer
    5.20  
    5.21  (* wrapper for calling external prover *)
    5.22  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 17:49:16 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 17:56:01 2010 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  signature SLEDGEHAMMER_ISAR =
     6.6  sig
     6.7 -  type params = ATP_Manager.params
     6.8 +  type params = Sledgehammer.params
     6.9  
    6.10    val atps: string Unsynchronized.ref
    6.11    val timeout: int Unsynchronized.ref
    6.12 @@ -19,7 +19,7 @@
    6.13  
    6.14  open Sledgehammer_Util
    6.15  open Sledgehammer_Fact_Filter
    6.16 -open ATP_Manager
    6.17 +open Sledgehammer
    6.18  open ATP_Systems
    6.19  open Sledgehammer_Fact_Minimizer
    6.20