renamed module "ATP_Wrapper" to "ATP_Systems"
authorblanchet
Fri Apr 23 18:06:41 2010 +0200 (2010-04-23)
changeset 36376e83d52a52449
parent 36375 2482446a604c
child 36377 b3dce4c715d0
renamed module "ATP_Wrapper" to "ATP_Systems"
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Apr 23 17:38:25 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Apr 23 18:06:41 2010 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
     1.5  use "Tools/ATP_Manager/atp_manager.ML"
     1.6  use "Tools/ATP_Manager/atp_wrapper.ML"
     1.7 -setup ATP_Wrapper.setup
     1.8 +setup ATP_Systems.setup
     1.9  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    1.10  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.11  
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 23 17:38:25 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 23 18:06:41 2010 +0200
     2.3 @@ -1,16 +1,16 @@
     2.4 -(*  Title:      HOL/Tools/ATP_Manager/atp_wrapper.ML
     2.5 +(*  Title:      HOL/Tools/ATP_Manager/atp_systems.ML
     2.6      Author:     Fabian Immler, TU Muenchen
     2.7      Author:     Jasmin Blanchette, TU Muenchen
     2.8  
     2.9 -Wrapper functions for external ATPs.
    2.10 +Setup for supported ATPs.
    2.11  *)
    2.12  
    2.13 -signature ATP_WRAPPER =
    2.14 +signature ATP_SYSTEMS =
    2.15  sig
    2.16    type prover = ATP_Manager.prover
    2.17  
    2.18    (* hooks for problem files *)
    2.19 -  val destdir : string Config.T
    2.20 +  val dest_dir : string Config.T
    2.21    val problem_prefix : string Config.T
    2.22    val measure_runtime : bool Config.T
    2.23  
    2.24 @@ -19,7 +19,7 @@
    2.25    val setup : theory -> theory
    2.26  end;
    2.27  
    2.28 -structure ATP_Wrapper : ATP_WRAPPER =
    2.29 +structure ATP_Systems : ATP_SYSTEMS =
    2.30  struct
    2.31  
    2.32  open Sledgehammer_Util
    2.33 @@ -29,11 +29,11 @@
    2.34  open Sledgehammer_Proof_Reconstruct
    2.35  open ATP_Manager
    2.36  
    2.37 -(** generic ATP wrapper **)
    2.38 +(** generic ATP **)
    2.39  
    2.40  (* external problem files *)
    2.41  
    2.42 -val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" (K "");
    2.43 +val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
    2.44    (*Empty string means create files in Isabelle's temporary files directory.*)
    2.45  
    2.46  val (problem_prefix, problem_prefix_setup) =
    2.47 @@ -123,20 +123,20 @@
    2.48        prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
    2.49  
    2.50      (* path to unique problem file *)
    2.51 -    val destdir' = if overlord then getenv "ISABELLE_HOME_USER"
    2.52 -                   else Config.get ctxt destdir;
    2.53 -    val problem_prefix' = Config.get ctxt problem_prefix;
    2.54 +    val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    2.55 +                       else Config.get ctxt dest_dir;
    2.56 +    val the_problem_prefix = Config.get ctxt problem_prefix;
    2.57      fun prob_pathname nr =
    2.58        let
    2.59          val probfile =
    2.60 -          Path.basic (problem_prefix' ^
    2.61 +          Path.basic (the_problem_prefix ^
    2.62                        (if overlord then "_" ^ name else serial_string ())
    2.63                        ^ "_" ^ string_of_int nr)
    2.64        in
    2.65 -        if destdir' = "" then File.tmp_path probfile
    2.66 -        else if File.exists (Path.explode destdir')
    2.67 -        then Path.append (Path.explode destdir') probfile
    2.68 -        else error ("No such directory: " ^ destdir' ^ ".")
    2.69 +        if the_dest_dir = "" then File.tmp_path probfile
    2.70 +        else if File.exists (Path.explode the_dest_dir)
    2.71 +        then Path.append (Path.explode the_dest_dir) probfile
    2.72 +        else error ("No such directory: " ^ the_dest_dir ^ ".")
    2.73        end;
    2.74  
    2.75      val command = Path.explode (home ^ "/" ^ executable)
    2.76 @@ -179,9 +179,10 @@
    2.77  
    2.78      (* If the problem file has not been exported, remove it; otherwise, export
    2.79         the proof file too. *)
    2.80 -    fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE;
    2.81 +    fun cleanup probfile =
    2.82 +      if the_dest_dir = "" then try File.rm probfile else NONE
    2.83      fun export probfile (((output, _), _), _) =
    2.84 -      if destdir' = "" then
    2.85 +      if the_dest_dir = "" then
    2.86          ()
    2.87        else
    2.88          File.write (Path.explode (Path.implode probfile ^ "_proof"))
    2.89 @@ -341,7 +342,7 @@
    2.90  
    2.91  (* remote prover invocation via SystemOnTPTP *)
    2.92  
    2.93 -val systems = Synchronized.var "atp_wrapper_systems" ([]: string list);
    2.94 +val systems = Synchronized.var "atp_systems" ([]: string list);
    2.95  
    2.96  fun get_systems () =
    2.97    case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
    2.98 @@ -403,7 +404,7 @@
    2.99  val prover_setup = fold add_prover provers
   2.100  
   2.101  val setup =
   2.102 -  destdir_setup
   2.103 +  dest_dir_setup
   2.104    #> problem_prefix_setup
   2.105    #> measure_runtime_setup
   2.106    #> prover_setup
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 17:38:25 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 18:06:41 2010 +0200
     3.3 @@ -19,7 +19,7 @@
     3.4  
     3.5  open Sledgehammer_Util
     3.6  open ATP_Manager
     3.7 -open ATP_Wrapper
     3.8 +open ATP_Systems
     3.9  open Sledgehammer_Fact_Minimizer
    3.10  
    3.11  structure K = OuterKeyword and P = OuterParse