modernized structure names;
authorwenzelm
Wed Oct 14 23:44:37 2009 +0200 (2009-10-14)
changeset 329369491bec20595
parent 32935 2218b970325a
child 32937 34f66c9dd8a2
modernized structure names;
src/HOL/ATP_Linkup.thy
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Oct 14 23:13:38 2009 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Oct 14 23:44:37 2009 +0200
     1.3 @@ -96,26 +96,26 @@
     1.4  use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
     1.5  use "Tools/res_atp.ML"
     1.6  
     1.7 -use "Tools/ATP_Manager/atp_wrapper.ML" setup AtpWrapper.setup
     1.8 +use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup
     1.9  use "Tools/ATP_Manager/atp_manager.ML"
    1.10  use "Tools/ATP_Manager/atp_minimal.ML"
    1.11  
    1.12  text {* basic provers *}
    1.13 -setup {* AtpManager.add_prover AtpWrapper.spass *}
    1.14 -setup {* AtpManager.add_prover AtpWrapper.vampire *}
    1.15 -setup {* AtpManager.add_prover AtpWrapper.eprover *}
    1.16 +setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
    1.17 +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
    1.18 +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
    1.19  
    1.20  text {* provers with stuctured output *}
    1.21 -setup {* AtpManager.add_prover AtpWrapper.vampire_full *}
    1.22 -setup {* AtpManager.add_prover AtpWrapper.eprover_full *}
    1.23 +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
    1.24 +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
    1.25  
    1.26  text {* on some problems better results *}
    1.27 -setup {* AtpManager.add_prover AtpWrapper.spass_no_tc *}
    1.28 +setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
    1.29  
    1.30  text {* remote provers via SystemOnTPTP *}
    1.31 -setup {* AtpManager.add_prover AtpWrapper.remote_vampire *}
    1.32 -setup {* AtpManager.add_prover AtpWrapper.remote_spass *}
    1.33 -setup {* AtpManager.add_prover AtpWrapper.remote_eprover *}
    1.34 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
    1.35 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
    1.36 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
    1.37    
    1.38  
    1.39  
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 14 23:13:38 2009 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 14 23:44:37 2009 +0200
     2.3 @@ -286,8 +286,8 @@
     2.4  
     2.5  fun get_atp thy args =
     2.6    AList.lookup (op =) args proverK
     2.7 -  |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
     2.8 -  |> (fn name => (name, the (AtpManager.get_prover name thy)))
     2.9 +  |> the_default (hd (space_explode " " (ATP_Manager.get_atps ())))
    2.10 +  |> (fn name => (name, the (ATP_Manager.get_prover name thy)))
    2.11  
    2.12  local
    2.13  
    2.14 @@ -300,15 +300,15 @@
    2.15    let
    2.16      val (ctxt, goal) = Proof.get_goal st
    2.17      val ctxt' = if is_none dir then ctxt
    2.18 -      else Config.put AtpWrapper.destdir (the dir) ctxt
    2.19 -    val atp = prover (AtpWrapper.atp_problem_of_goal
    2.20 -      (AtpManager.get_full_types ()) 1 (ctxt', goal))
    2.21 +      else Config.put ATP_Wrapper.destdir (the dir) ctxt
    2.22 +    val atp = prover (ATP_Wrapper.atp_problem_of_goal
    2.23 +      (ATP_Manager.get_full_types ()) 1 (ctxt', goal))
    2.24  
    2.25      val time_limit =
    2.26        (case hard_timeout of
    2.27          NONE => I
    2.28        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
    2.29 -    val (AtpWrapper.Prover_Result {success, message, theorem_names,
    2.30 +    val (ATP_Wrapper.Prover_Result {success, message, theorem_names,
    2.31        runtime=time_atp, ...}, time_isa) =
    2.32        time_limit (Mirabelle.cpu_time atp) timeout
    2.33    in
    2.34 @@ -372,7 +372,7 @@
    2.35    let
    2.36      val n0 = length (these (!named_thms))
    2.37      val (prover_name, prover) = get_atp (Proof.theory_of st) args
    2.38 -    val minimize = AtpMinimal.minimalize prover prover_name
    2.39 +    val minimize = ATP_Minimal.minimalize prover prover_name
    2.40      val timeout =
    2.41        AList.lookup (op =) args minimize_timeoutK
    2.42        |> Option.map (fst o read_int o explode)
    2.43 @@ -448,7 +448,7 @@
    2.44  
    2.45  fun invoke args =
    2.46    let
    2.47 -    val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
    2.48 +    val _ = ATP_Manager.set_full_types (AList.defined (op =) args full_typesK)
    2.49    in Mirabelle.register (init, sledgehammer_action args, done) end
    2.50  
    2.51  end
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 14 23:13:38 2009 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 14 23:44:37 2009 +0200
     3.3 @@ -21,13 +21,13 @@
     3.4    val kill: unit -> unit
     3.5    val info: unit -> unit
     3.6    val messages: int option -> unit
     3.7 -  val add_prover: string * AtpWrapper.prover -> theory -> theory
     3.8 +  val add_prover: string * ATP_Wrapper.prover -> theory -> theory
     3.9    val print_provers: theory -> unit
    3.10 -  val get_prover: string -> theory -> AtpWrapper.prover option
    3.11 +  val get_prover: string -> theory -> ATP_Wrapper.prover option
    3.12    val sledgehammer: string list -> Proof.state -> unit
    3.13  end;
    3.14  
    3.15 -structure AtpManager: ATP_MANAGER =
    3.16 +structure ATP_Manager: ATP_MANAGER =
    3.17  struct
    3.18  
    3.19  (** preferences **)
    3.20 @@ -302,7 +302,7 @@
    3.21  
    3.22  structure Provers = TheoryDataFun
    3.23  (
    3.24 -  type T = (AtpWrapper.prover * stamp) Symtab.table
    3.25 +  type T = (ATP_Wrapper.prover * stamp) Symtab.table
    3.26    val empty = Symtab.empty
    3.27    val copy = I
    3.28    val extend = I
    3.29 @@ -337,10 +337,10 @@
    3.30          val _ = SimpleThread.fork true (fn () =>
    3.31            let
    3.32              val _ = register birthtime deadtime (Thread.self (), desc)
    3.33 -            val problem = AtpWrapper.atp_problem_of_goal (get_full_types ()) i
    3.34 +            val problem = ATP_Wrapper.atp_problem_of_goal (get_full_types ()) i
    3.35                (Proof.get_goal proof_state)
    3.36              val result =
    3.37 -              let val AtpWrapper.Prover_Result {success, message, ...} =
    3.38 +              let val ATP_Wrapper.Prover_Result {success, message, ...} =
    3.39                  prover problem (get_timeout ())
    3.40                in (success, message) end
    3.41                handle ResHolClause.TOO_TRIVIAL
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 14 23:13:38 2009 +0200
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 14 23:44:37 2009 +0200
     4.3 @@ -6,11 +6,11 @@
     4.4  
     4.5  signature ATP_MINIMAL =
     4.6  sig
     4.7 -  val minimalize: AtpWrapper.prover -> string -> int -> Proof.state ->
     4.8 +  val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
     4.9      (string * thm list) list -> ((string * thm list) list * int) option * string
    4.10  end
    4.11  
    4.12 -structure AtpMinimal: ATP_MINIMAL =
    4.13 +structure ATP_Minimal: ATP_MINIMAL =
    4.14  struct
    4.15  
    4.16  (* output control *)
    4.17 @@ -99,7 +99,7 @@
    4.18  
    4.19  fun produce_answer result =
    4.20    let
    4.21 -    val AtpWrapper.Prover_Result {success, message, proof=result_string,
    4.22 +    val ATP_Wrapper.Prover_Result {success, message, proof=result_string,
    4.23        internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result
    4.24    in
    4.25    if success then
    4.26 @@ -116,6 +116,7 @@
    4.27      end
    4.28    end
    4.29  
    4.30 +
    4.31  (* wrapper for calling external prover *)
    4.32  
    4.33  fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
    4.34 @@ -124,8 +125,8 @@
    4.35      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    4.36      val _ = debug_fn (fn () => print_names name_thm_pairs)
    4.37      val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    4.38 -    val problem = AtpWrapper.ATP_Problem {
    4.39 -      with_full_types = AtpManager.get_full_types (),
    4.40 +    val problem = ATP_Wrapper.ATP_Problem {
    4.41 +      with_full_types = ATP_Manager.get_full_types (),
    4.42        subgoal = subgoalno,
    4.43        goal = Proof.get_goal state,
    4.44        axiom_clauses = SOME axclauses,
    4.45 @@ -224,7 +225,7 @@
    4.46    let
    4.47      val (prover_name, time_limit) = get_options args
    4.48      val prover =
    4.49 -      case AtpManager.get_prover prover_name (Proof.theory_of state) of
    4.50 +      case ATP_Manager.get_prover prover_name (Proof.theory_of state) of
    4.51          SOME prover => prover
    4.52        | NONE => error ("Unknown prover: " ^ quote prover_name)
    4.53      val name_thms_pairs = get_thms (Proof.context_of state) thm_names
     5.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Oct 14 23:13:38 2009 +0200
     5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Oct 14 23:44:37 2009 +0200
     5.3 @@ -49,7 +49,7 @@
     5.4    val refresh_systems: unit -> unit
     5.5  end;
     5.6  
     5.7 -structure AtpWrapper: ATP_WRAPPER =
     5.8 +structure ATP_Wrapper: ATP_WRAPPER =
     5.9  struct
    5.10  
    5.11  (** generic ATP wrapper **)