1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 19 15:07:44 2010 +0100
     1.3 @@ -0,0 +1,87 @@
     1.4 +(*  Title:      HOL/Sledgehammer/sledgehammer_isar.ML
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +
     1.7 +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
     1.8 +*)
     1.9 +
    1.10 +structure Sledgehammer_Isar : sig end =
    1.11 +struct
    1.12 +
    1.13 +open ATP_Manager
    1.14 +open ATP_Minimal
    1.15 +
    1.16 +structure K = OuterKeyword and P = OuterParse
    1.17 +
    1.18 +val _ =
    1.19 +  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
    1.20 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
    1.21 +
    1.22 +val _ =
    1.23 +  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
    1.24 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
    1.25 +
    1.26 +val _ =
    1.27 +  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
    1.28 +    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
    1.29 +      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
    1.30 +
    1.31 +val _ =
    1.32 +  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
    1.33 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    1.34 +      Toplevel.keep (print_provers o Toplevel.theory_of)));
    1.35 +
    1.36 +val _ =
    1.37 +  OuterSyntax.command "sledgehammer"
    1.38 +    "search for first-order proof using automatic theorem provers" K.diag
    1.39 +    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
    1.40 +      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
    1.41 +
    1.42 +val default_minimize_prover = "remote_vampire"
    1.43 +val default_minimize_time_limit = 5
    1.44 +
    1.45 +fun atp_minimize_command args thm_names state =
    1.46 +  let
    1.47 +    fun theorems_from_names ctxt =
    1.48 +      map (fn (name, interval) =>
    1.49 +              let
    1.50 +                val thmref = Facts.Named ((name, Position.none), interval)
    1.51 +                val ths = ProofContext.get_fact ctxt thmref
    1.52 +                val name' = Facts.string_of_ref thmref
    1.53 +              in (name', ths) end)
    1.54 +    fun get_time_limit_arg time_string =
    1.55 +      (case Int.fromString time_string of
    1.56 +        SOME t => t
    1.57 +      | NONE => error ("Invalid time limit: " ^ quote time_string))
    1.58 +    fun get_opt (name, a) (p, t) =
    1.59 +      (case name of
    1.60 +        "time" => (p, get_time_limit_arg a)
    1.61 +      | "atp" => (a, t)
    1.62 +      | n => error ("Invalid argument: " ^ n))
    1.63 +    fun get_options args =
    1.64 +      fold get_opt args (default_minimize_prover, default_minimize_time_limit)
    1.65 +    val (prover_name, time_limit) = get_options args
    1.66 +    val prover =
    1.67 +      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
    1.68 +        SOME prover => prover
    1.69 +      | NONE => error ("Unknown prover: " ^ quote prover_name))
    1.70 +    val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
    1.71 +  in
    1.72 +    writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
    1.73 +                                   state name_thms_pairs))
    1.74 +  end
    1.75 +
    1.76 +local structure K = OuterKeyword and P = OuterParse in
    1.77 +
    1.78 +val parse_args =
    1.79 +  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
    1.80 +val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
    1.81 +
    1.82 +val _ =
    1.83 +  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
    1.84 +    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
    1.85 +      Toplevel.no_timing o Toplevel.unknown_proof o
    1.86 +        Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
    1.87 +
    1.88 +end
    1.89 +
    1.90 +end;