move the Sledgehammer Isar commands together into one file;
authorblanchet
Fri Mar 19 15:07:44 2010 +0100 (2010-03-19)
changeset 35866513074557e06
parent 35865 2f8fb5242799
child 35867 16279c4c7a33
move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Mar 19 13:02:18 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Mar 19 15:07:44 2010 +0100
     1.3 @@ -320,6 +320,7 @@
     1.4    Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
     1.5    Tools/Sledgehammer/sledgehammer_fol_clause.ML \
     1.6    Tools/Sledgehammer/sledgehammer_hol_clause.ML \
     1.7 +  Tools/Sledgehammer/sledgehammer_isar.ML \
     1.8    Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
     1.9    Tools/string_code.ML \
    1.10    Tools/string_syntax.ML \
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 13:02:18 2010 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 15:07:44 2010 +0100
     2.3 @@ -42,8 +42,7 @@
     2.4  
     2.5  datatype min_data = MinData of {
     2.6    succs: int,
     2.7 -  ab_ratios: int,
     2.8 -  it_ratios: int
     2.9 +  ab_ratios: int
    2.10    }
    2.11  
    2.12  fun make_sh_data
    2.13 @@ -51,8 +50,8 @@
    2.14    ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
    2.15           time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
    2.16  
    2.17 -fun make_min_data (succs, ab_ratios, it_ratios) =
    2.18 -  MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
    2.19 +fun make_min_data (succs, ab_ratios) =
    2.20 +  MinData{succs=succs, ab_ratios=ab_ratios}
    2.21  
    2.22  fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
    2.23    MeData{calls=calls, success=success, proofs=proofs, time=time,
    2.24 @@ -66,8 +65,7 @@
    2.25    time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
    2.26    time_atp, time_atp_fail)
    2.27  
    2.28 -fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
    2.29 -  (succs, ab_ratios, it_ratios)
    2.30 +fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
    2.31  
    2.32  fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
    2.33    posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
    2.34 @@ -147,13 +145,10 @@
    2.35      => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
    2.36  
    2.37  val inc_min_succs = map_min_data
    2.38 -  (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
    2.39 +  (fn (succs,ab_ratios) => (succs+1, ab_ratios))
    2.40  
    2.41  fun inc_min_ab_ratios r = map_min_data
    2.42 -  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
    2.43 -
    2.44 -fun inc_min_it_ratios r = map_min_data
    2.45 -  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
    2.46 +  (fn (succs, ab_ratios) => (succs, ab_ratios+r))
    2.47  
    2.48  val inc_metis_calls = map_me_data
    2.49    (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.50 @@ -234,10 +229,9 @@
    2.51    else ()
    2.52   )
    2.53  
    2.54 -fun log_min_data log (succs, ab_ratios, it_ratios) =
    2.55 +fun log_min_data log (succs, ab_ratios) =
    2.56    (log ("Number of successful minimizations: " ^ string_of_int succs);
    2.57 -   log ("After/before ratios: " ^ string_of_int ab_ratios);
    2.58 -   log ("Iterations ratios: " ^ string_of_int it_ratios)
    2.59 +   log ("After/before ratios: " ^ string_of_int ab_ratios)
    2.60    )
    2.61  
    2.62  in
    2.63 @@ -380,9 +374,10 @@
    2.64  
    2.65  fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
    2.66    let
    2.67 +    open ATP_Minimal
    2.68      val n0 = length (these (!named_thms))
    2.69      val (prover_name, prover) = get_atp (Proof.theory_of st) args
    2.70 -    val minimize = ATP_Minimal.minimalize prover prover_name
    2.71 +    val minimize = minimize_theorems linear_minimize prover prover_name
    2.72      val timeout =
    2.73        AList.lookup (op =) args minimize_timeoutK
    2.74        |> Option.map (fst o read_int o explode)
    2.75 @@ -393,7 +388,6 @@
    2.76        (SOME (named_thms',its), msg) =>
    2.77          (change_data id inc_min_succs;
    2.78           change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
    2.79 -         change_data id (inc_min_it_ratios ((100*its) div n0));
    2.80           if length named_thms' = n0
    2.81           then log (minimize_tag id ^ "already minimal")
    2.82           else (named_thms := SOME named_thms';
     3.1 --- a/src/HOL/Sledgehammer.thy	Fri Mar 19 13:02:18 2010 +0100
     3.2 +++ b/src/HOL/Sledgehammer.thy	Fri Mar 19 15:07:44 2010 +0100
     3.3 @@ -20,6 +20,7 @@
     3.4    ("Tools/ATP_Manager/atp_manager.ML")
     3.5    ("Tools/ATP_Manager/atp_wrapper.ML")
     3.6    ("Tools/ATP_Manager/atp_minimal.ML")
     3.7 +  ("Tools/Sledgehammer/sledgehammer_isar.ML")
     3.8    ("Tools/Sledgehammer/meson_tactic.ML")
     3.9    ("Tools/Sledgehammer/metis_tactics.ML")
    3.10  begin
    3.11 @@ -90,6 +91,7 @@
    3.12  apply (simp add: COMBC_def) 
    3.13  done
    3.14  
    3.15 +
    3.16  subsection {* Setup of external ATPs *}
    3.17  
    3.18  use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    3.19 @@ -122,6 +124,8 @@
    3.20  setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
    3.21  setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
    3.22  
    3.23 +use "Tools/Sledgehammer/sledgehammer_isar.ML"
    3.24 +
    3.25  
    3.26  subsection {* The MESON prover *}
    3.27  
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 13:02:18 2010 +0100
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 15:07:44 2010 +0100
     4.3 @@ -282,36 +282,4 @@
     4.4      val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
     4.5    in () end;
     4.6  
     4.7 -
     4.8 -
     4.9 -(** Isar command syntax **)
    4.10 -
    4.11 -local structure K = OuterKeyword and P = OuterParse in
    4.12 -
    4.13 -val _ =
    4.14 -  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
    4.15 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
    4.16 -
    4.17 -val _ =
    4.18 -  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
    4.19 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
    4.20 -
    4.21 -val _ =
    4.22 -  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
    4.23 -    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
    4.24 -      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
    4.25 -
    4.26 -val _ =
    4.27 -  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
    4.28 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    4.29 -      Toplevel.keep (print_provers o Toplevel.theory_of)));
    4.30 -
    4.31 -val _ =
    4.32 -  OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
    4.33 -    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
    4.34 -      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
    4.35 -
    4.36  end;
    4.37 -
    4.38 -end;
    4.39 -
     5.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 19 13:02:18 2010 +0100
     5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 19 15:07:44 2010 +0100
     5.3 @@ -6,27 +6,31 @@
     5.4  
     5.5  signature ATP_MINIMAL =
     5.6  sig
     5.7 -  val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
     5.8 -    (string * thm list) list -> ((string * thm list) list * int) option * string
     5.9 -  (* To be removed once TN has finished his measurements;
    5.10 -     the int component of the result should then be removed: *)
    5.11 -  val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
    5.12 -    (string * thm list) list -> ((string * thm list) list * int) option * string
    5.13 -end
    5.14 +  type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    5.15 +  val linear_minimize : 'a minimize_fun
    5.16 +  val binary_minimize : 'a minimize_fun
    5.17 +  val minimize_theorems :
    5.18 +    (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int
    5.19 +    -> Proof.state -> (string * thm list) list
    5.20 +    -> (string * thm list) list option * string
    5.21 +end;
    5.22  
    5.23  structure ATP_Minimal : ATP_MINIMAL =
    5.24  struct
    5.25  
    5.26 -(* Linear minimization *)
    5.27 +open Sledgehammer_Fact_Preprocessor
    5.28 +
    5.29 +type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    5.30 +
    5.31 +(* Linear minimization algorithm *)
    5.32  
    5.33 -fun lin_gen_minimize p s =
    5.34 -let
    5.35 -  fun min [] needed = needed
    5.36 -    | min (x::xs) needed =
    5.37 -        if p(xs @ needed) then min xs needed else min xs (x::needed)
    5.38 -in (min s [], length s) end;
    5.39 +fun linear_minimize p s =
    5.40 +  let
    5.41 +    fun aux [] needed = needed
    5.42 +      | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
    5.43 +  in aux s [] end;
    5.44  
    5.45 -(* Clever minimalization algorithm *)
    5.46 +(* Binary minimalization *)
    5.47  
    5.48  local
    5.49    fun isplit (l, r) [] = (l, r)
    5.50 @@ -37,24 +41,21 @@
    5.51  end
    5.52  
    5.53  local
    5.54 -  fun min p sup [] = raise Empty
    5.55 -    | min p sup [s0] = [s0]
    5.56 +  fun min _ _ [] = raise Empty
    5.57 +    | min _ _ [s0] = [s0]
    5.58      | min p sup s =
    5.59        let
    5.60          val (l0, r0) = split s
    5.61        in
    5.62 -        if p (sup @ l0)
    5.63 -        then min p sup l0
    5.64 +        if p (sup @ l0) then
    5.65 +          min p sup l0
    5.66 +        else if p (sup @ r0) then
    5.67 +          min p sup r0
    5.68          else
    5.69 -          if p (sup @ r0)
    5.70 -          then min p sup r0
    5.71 -          else
    5.72 -            let
    5.73 -              val l = min p (sup @ r0) l0
    5.74 -              val r = min p (sup @ l) r0
    5.75 -            in
    5.76 -              l @ r
    5.77 -            end
    5.78 +          let
    5.79 +            val l = min p (sup @ r0) l0
    5.80 +            val r = min p (sup @ l) r0
    5.81 +          in l @ r end
    5.82        end
    5.83  in
    5.84    (* return a minimal subset v of s that satisfies p
    5.85 @@ -62,15 +63,10 @@
    5.86     @post v subset s & p(v) &
    5.87           forall e in v. ~p(v \ e)
    5.88     *)
    5.89 -  fun minimal p s =
    5.90 -    let
    5.91 -      val count = Unsynchronized.ref 0
    5.92 -      fun p_count xs = (Unsynchronized.inc count; p xs)
    5.93 -      val v =
    5.94 -        (case min p_count [] s of
    5.95 -          [x] => if p_count [] then [] else [x]
    5.96 -        | m => m);
    5.97 -    in (v, ! count) end
    5.98 +  fun binary_minimize p s =
    5.99 +    case min p [] s of
   5.100 +      [x] => if p [] then [] else [x]
   5.101 +    | m => m
   5.102  end
   5.103  
   5.104  
   5.105 @@ -91,7 +87,7 @@
   5.106     ("# Cannot determine problem status within resource limit", Timeout),
   5.107     ("Error", Error)]
   5.108  
   5.109 -fun produce_answer (result: ATP_Wrapper.prover_result) =
   5.110 +fun produce_answer (result : ATP_Wrapper.prover_result) =
   5.111    let
   5.112      val {success, proof = result_string, internal_thm_names = thm_name_vec,
   5.113        filtered_clauses = filtered, ...} = result
   5.114 @@ -116,7 +112,7 @@
   5.115    let
   5.116      val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
   5.117      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
   5.118 -    val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
   5.119 +    val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
   5.120      val {context = ctxt, facts, goal} = Proof.goal state
   5.121      val problem =
   5.122       {with_full_types = ! ATP_Manager.full_types,
   5.123 @@ -133,7 +129,8 @@
   5.124  
   5.125  (* minimalization of thms *)
   5.126  
   5.127 -fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
   5.128 +fun minimize_theorems gen_min prover prover_name time_limit state
   5.129 +                      name_thms_pairs =
   5.130    let
   5.131      val _ =
   5.132        priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
   5.133 @@ -152,15 +149,14 @@
   5.134              if length ordered_used < length name_thms_pairs then
   5.135                filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
   5.136              else name_thms_pairs
   5.137 -          val (min_thms, n) =
   5.138 -            if null to_use then ([], 0)
   5.139 +          val min_thms =
   5.140 +            if null to_use then []
   5.141              else gen_min (test_thms (SOME filtered)) to_use
   5.142            val min_names = sort_distinct string_ord (map fst min_thms)
   5.143            val _ = priority (cat_lines
   5.144 -            ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
   5.145 -             "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
   5.146 +            ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
   5.147          in
   5.148 -          (SOME (min_thms, n), "Try this command: " ^
   5.149 +          (SOME min_thms, "Try this command: " ^
   5.150              Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
   5.151          end
   5.152      | (Timeout, _) =>
   5.153 @@ -171,67 +167,8 @@
   5.154      | (Failure, _) =>
   5.155          (NONE, "Failure: No proof with the theorems supplied"))
   5.156      handle Sledgehammer_HOL_Clause.TRIVIAL =>
   5.157 -        (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
   5.158 +        (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
   5.159        | ERROR msg => (NONE, "Error: " ^ msg)
   5.160    end
   5.161  
   5.162 -
   5.163 -(* Isar command and parsing input *)
   5.164 -
   5.165 -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
   5.166 -
   5.167 -fun get_thms context =
   5.168 -  map (fn (name, interval) =>
   5.169 -    let
   5.170 -      val thmref = Facts.Named ((name, Position.none), interval)
   5.171 -      val ths = ProofContext.get_fact context thmref
   5.172 -      val name' = Facts.string_of_ref thmref
   5.173 -    in
   5.174 -      (name', ths)
   5.175 -    end)
   5.176 -
   5.177 -val default_prover = "remote_vampire"
   5.178 -val default_time_limit = 5
   5.179 -
   5.180 -fun get_time_limit_arg time_string =
   5.181 -  (case Int.fromString time_string of
   5.182 -    SOME t => t
   5.183 -  | NONE => error ("Invalid time limit: " ^ quote time_string))
   5.184 -
   5.185 -fun get_opt (name, a) (p, t) =
   5.186 -  (case name of
   5.187 -    "time" => (p, get_time_limit_arg a)
   5.188 -  | "atp" => (a, t)
   5.189 -  | n => error ("Invalid argument: " ^ n))
   5.190 -
   5.191 -fun get_options args = fold get_opt args (default_prover, default_time_limit)
   5.192 -
   5.193 -val minimize = gen_minimalize lin_gen_minimize
   5.194 -
   5.195 -val minimalize = gen_minimalize minimal
   5.196 -
   5.197 -fun sh_min_command args thm_names state =
   5.198 -  let
   5.199 -    val (prover_name, time_limit) = get_options args
   5.200 -    val prover =
   5.201 -      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
   5.202 -        SOME prover => prover
   5.203 -      | NONE => error ("Unknown prover: " ^ quote prover_name))
   5.204 -    val name_thms_pairs = get_thms (Proof.context_of state) thm_names
   5.205 -  in
   5.206 -    writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
   5.207 -  end
   5.208 -
   5.209 -val parse_args =
   5.210 -  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
   5.211 -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
   5.212 -
   5.213 -val _ =
   5.214 -  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
   5.215 -    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
   5.216 -      Toplevel.no_timing o Toplevel.unknown_proof o
   5.217 -        Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
   5.218 -
   5.219 -end
   5.220 -
   5.221 -end
   5.222 +end;
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Mar 19 13:02:18 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Mar 19 15:07:44 2010 +0100
     6.3 @@ -13,7 +13,7 @@
     6.4    val auto: bool Unsynchronized.ref
     6.5    val default_params : theory -> (string * string) list -> params
     6.6    val setup : theory -> theory
     6.7 -end
     6.8 +end;
     6.9  
    6.10  structure Nitpick_Isar : NITPICK_ISAR =
    6.11  struct
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 19 13:02:18 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 19 15:07:44 2010 +0100
     7.3 @@ -12,7 +12,7 @@
     7.4      hol_context -> (typ option * bool option) list
     7.5      -> (typ option * bool option) list -> term
     7.6      -> term list * term list * bool * bool * bool
     7.7 -end
     7.8 +end;
     7.9  
    7.10  structure Nitpick_Preproc : NITPICK_PREPROC =
    7.11  struct
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Mar 19 13:02:18 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Mar 19 15:07:44 2010 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  signature NITPICK_TESTS =
     8.5  sig
     8.6    val run_all_tests : unit -> unit
     8.7 -end
     8.8 +end;
     8.9  
    8.10  structure Nitpick_Tests =
    8.11  struct
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Mar 19 13:02:18 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Mar 19 15:07:44 2010 +0100
     9.3 @@ -62,7 +62,7 @@
     9.4    val pstrs : string -> Pretty.T list
     9.5    val unyxml : string -> string
     9.6    val maybe_quote : string -> string
     9.7 -end
     9.8 +end;
     9.9  
    9.10  structure Nitpick_Util : NITPICK_UTIL =
    9.11  struct
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 19 15:07:44 2010 +0100
    10.3 @@ -0,0 +1,87 @@
    10.4 +(*  Title:      HOL/Sledgehammer/sledgehammer_isar.ML
    10.5 +    Author:     Jasmin Blanchette, TU Muenchen
    10.6 +
    10.7 +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
    10.8 +*)
    10.9 +
   10.10 +structure Sledgehammer_Isar : sig end =
   10.11 +struct
   10.12 +
   10.13 +open ATP_Manager
   10.14 +open ATP_Minimal
   10.15 +
   10.16 +structure K = OuterKeyword and P = OuterParse
   10.17 +
   10.18 +val _ =
   10.19 +  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
   10.20 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   10.21 +
   10.22 +val _ =
   10.23 +  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
   10.24 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
   10.25 +
   10.26 +val _ =
   10.27 +  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
   10.28 +    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
   10.29 +      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
   10.30 +
   10.31 +val _ =
   10.32 +  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
   10.33 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   10.34 +      Toplevel.keep (print_provers o Toplevel.theory_of)));
   10.35 +
   10.36 +val _ =
   10.37 +  OuterSyntax.command "sledgehammer"
   10.38 +    "search for first-order proof using automatic theorem provers" K.diag
   10.39 +    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
   10.40 +      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
   10.41 +
   10.42 +val default_minimize_prover = "remote_vampire"
   10.43 +val default_minimize_time_limit = 5
   10.44 +
   10.45 +fun atp_minimize_command args thm_names state =
   10.46 +  let
   10.47 +    fun theorems_from_names ctxt =
   10.48 +      map (fn (name, interval) =>
   10.49 +              let
   10.50 +                val thmref = Facts.Named ((name, Position.none), interval)
   10.51 +                val ths = ProofContext.get_fact ctxt thmref
   10.52 +                val name' = Facts.string_of_ref thmref
   10.53 +              in (name', ths) end)
   10.54 +    fun get_time_limit_arg time_string =
   10.55 +      (case Int.fromString time_string of
   10.56 +        SOME t => t
   10.57 +      | NONE => error ("Invalid time limit: " ^ quote time_string))
   10.58 +    fun get_opt (name, a) (p, t) =
   10.59 +      (case name of
   10.60 +        "time" => (p, get_time_limit_arg a)
   10.61 +      | "atp" => (a, t)
   10.62 +      | n => error ("Invalid argument: " ^ n))
   10.63 +    fun get_options args =
   10.64 +      fold get_opt args (default_minimize_prover, default_minimize_time_limit)
   10.65 +    val (prover_name, time_limit) = get_options args
   10.66 +    val prover =
   10.67 +      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
   10.68 +        SOME prover => prover
   10.69 +      | NONE => error ("Unknown prover: " ^ quote prover_name))
   10.70 +    val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
   10.71 +  in
   10.72 +    writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
   10.73 +                                   state name_thms_pairs))
   10.74 +  end
   10.75 +
   10.76 +local structure K = OuterKeyword and P = OuterParse in
   10.77 +
   10.78 +val parse_args =
   10.79 +  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
   10.80 +val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
   10.81 +
   10.82 +val _ =
   10.83 +  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
   10.84 +    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
   10.85 +      Toplevel.no_timing o Toplevel.unknown_proof o
   10.86 +        Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
   10.87 +
   10.88 +end
   10.89 +
   10.90 +end;