src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Fri Mar 19 15:07:44 2010 +0100 (2010-03-19 ago)
changeset 35866 513074557e06
child 35962 0e2d57686b3c
permissions -rw-r--r--
move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later
blanchet@35866
     1
(*  Title:      HOL/Sledgehammer/sledgehammer_isar.ML
blanchet@35866
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35866
     3
blanchet@35866
     4
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
blanchet@35866
     5
*)
blanchet@35866
     6
blanchet@35866
     7
structure Sledgehammer_Isar : sig end =
blanchet@35866
     8
struct
blanchet@35866
     9
blanchet@35866
    10
open ATP_Manager
blanchet@35866
    11
open ATP_Minimal
blanchet@35866
    12
blanchet@35866
    13
structure K = OuterKeyword and P = OuterParse
blanchet@35866
    14
blanchet@35866
    15
val _ =
blanchet@35866
    16
  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
blanchet@35866
    17
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
blanchet@35866
    18
blanchet@35866
    19
val _ =
blanchet@35866
    20
  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
blanchet@35866
    21
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
blanchet@35866
    22
blanchet@35866
    23
val _ =
blanchet@35866
    24
  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
blanchet@35866
    25
    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
blanchet@35866
    26
      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
blanchet@35866
    27
blanchet@35866
    28
val _ =
blanchet@35866
    29
  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
blanchet@35866
    30
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
blanchet@35866
    31
      Toplevel.keep (print_provers o Toplevel.theory_of)));
blanchet@35866
    32
blanchet@35866
    33
val _ =
blanchet@35866
    34
  OuterSyntax.command "sledgehammer"
blanchet@35866
    35
    "search for first-order proof using automatic theorem provers" K.diag
blanchet@35866
    36
    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
blanchet@35866
    37
      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
blanchet@35866
    38
blanchet@35866
    39
val default_minimize_prover = "remote_vampire"
blanchet@35866
    40
val default_minimize_time_limit = 5
blanchet@35866
    41
blanchet@35866
    42
fun atp_minimize_command args thm_names state =
blanchet@35866
    43
  let
blanchet@35866
    44
    fun theorems_from_names ctxt =
blanchet@35866
    45
      map (fn (name, interval) =>
blanchet@35866
    46
              let
blanchet@35866
    47
                val thmref = Facts.Named ((name, Position.none), interval)
blanchet@35866
    48
                val ths = ProofContext.get_fact ctxt thmref
blanchet@35866
    49
                val name' = Facts.string_of_ref thmref
blanchet@35866
    50
              in (name', ths) end)
blanchet@35866
    51
    fun get_time_limit_arg time_string =
blanchet@35866
    52
      (case Int.fromString time_string of
blanchet@35866
    53
        SOME t => t
blanchet@35866
    54
      | NONE => error ("Invalid time limit: " ^ quote time_string))
blanchet@35866
    55
    fun get_opt (name, a) (p, t) =
blanchet@35866
    56
      (case name of
blanchet@35866
    57
        "time" => (p, get_time_limit_arg a)
blanchet@35866
    58
      | "atp" => (a, t)
blanchet@35866
    59
      | n => error ("Invalid argument: " ^ n))
blanchet@35866
    60
    fun get_options args =
blanchet@35866
    61
      fold get_opt args (default_minimize_prover, default_minimize_time_limit)
blanchet@35866
    62
    val (prover_name, time_limit) = get_options args
blanchet@35866
    63
    val prover =
blanchet@35866
    64
      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
blanchet@35866
    65
        SOME prover => prover
blanchet@35866
    66
      | NONE => error ("Unknown prover: " ^ quote prover_name))
blanchet@35866
    67
    val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
blanchet@35866
    68
  in
blanchet@35866
    69
    writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
blanchet@35866
    70
                                   state name_thms_pairs))
blanchet@35866
    71
  end
blanchet@35866
    72
blanchet@35866
    73
local structure K = OuterKeyword and P = OuterParse in
blanchet@35866
    74
blanchet@35866
    75
val parse_args =
blanchet@35866
    76
  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
blanchet@35866
    77
val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
blanchet@35866
    78
blanchet@35866
    79
val _ =
blanchet@35866
    80
  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
blanchet@35866
    81
    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
blanchet@35866
    82
      Toplevel.no_timing o Toplevel.unknown_proof o
blanchet@35866
    83
        Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
blanchet@35866
    84
blanchet@35866
    85
end
blanchet@35866
    86
blanchet@35866
    87
end;