src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Tue Mar 23 11:39:21 2010 +0100 (2010-03-23 ago)
changeset 35963 943e2582dc87
parent 35962 0e2d57686b3c
child 35965 0fce6db7babd
permissions -rw-r--r--
added options to Sledgehammer;
syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional
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@35963
     7
signature SLEDGEHAMMER_ISAR =
blanchet@35963
     8
sig
blanchet@35963
     9
  type params = ATP_Manager.params
blanchet@35963
    10
blanchet@35963
    11
  val default_params : theory -> (string * string) list -> params
blanchet@35963
    12
end;
blanchet@35963
    13
blanchet@35866
    14
structure Sledgehammer_Isar : sig end =
blanchet@35866
    15
struct
blanchet@35866
    16
blanchet@35866
    17
open ATP_Manager
blanchet@35866
    18
open ATP_Minimal
blanchet@35963
    19
open Sledgehammer_Util
blanchet@35866
    20
blanchet@35866
    21
structure K = OuterKeyword and P = OuterParse
blanchet@35866
    22
blanchet@35963
    23
type raw_param = string * string list
blanchet@35963
    24
blanchet@35963
    25
val default_default_params =
blanchet@35963
    26
  [("debug", "false"),
blanchet@35963
    27
   ("verbose", "false"),
blanchet@35963
    28
   ("relevance_threshold", "0.5"),
blanchet@35963
    29
   ("higher_order", "smart"),
blanchet@35963
    30
   ("respect_no_atp", "true"),
blanchet@35963
    31
   ("follow_defs", "false"),
blanchet@35963
    32
   ("isar_proof", "false"),
blanchet@35963
    33
   ("minimize_timeout", "5 s")]
blanchet@35963
    34
blanchet@35963
    35
val negated_params =
blanchet@35963
    36
  [("no_debug", "debug"),
blanchet@35963
    37
   ("quiet", "verbose"),
blanchet@35963
    38
   ("partial_types", "full_types"),
blanchet@35963
    39
   ("first_order", "higher_order"),
blanchet@35963
    40
   ("ignore_no_atp", "respect_no_atp"),
blanchet@35963
    41
   ("dont_follow_defs", "follow_defs"),
blanchet@35963
    42
   ("metis_proof", "isar_proof")]
blanchet@35963
    43
blanchet@35963
    44
val property_affected_params = ["atps", "full_types", "timeout"]
blanchet@35866
    45
blanchet@35963
    46
fun is_known_raw_param s =
blanchet@35963
    47
  AList.defined (op =) default_default_params s orelse
blanchet@35963
    48
  AList.defined (op =) negated_params s orelse
blanchet@35963
    49
  member (op =) property_affected_params s
blanchet@35963
    50
blanchet@35963
    51
fun check_raw_param (s, _) =
blanchet@35963
    52
  if is_known_raw_param s then ()
blanchet@35963
    53
  else error ("Unknown parameter: " ^ quote s ^ ".")
blanchet@35866
    54
blanchet@35963
    55
fun unnegate_raw_param (name, value) =
blanchet@35963
    56
  case AList.lookup (op =) negated_params name of
blanchet@35963
    57
    SOME name' => (name', case value of
blanchet@35963
    58
                            ["false"] => ["true"]
blanchet@35963
    59
                          | ["true"] => ["false"]
blanchet@35963
    60
                          | [] => ["false"]
blanchet@35963
    61
                          | _ => value)
blanchet@35963
    62
  | NONE => (name, value)
blanchet@35963
    63
blanchet@35963
    64
structure Data = Theory_Data(
blanchet@35963
    65
  type T = raw_param list
blanchet@35963
    66
  val empty = default_default_params |> map (apsnd single)
blanchet@35963
    67
  val extend = I
blanchet@35963
    68
  fun merge p : T = AList.merge (op =) (K true) p)
blanchet@35866
    69
blanchet@35963
    70
val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
blanchet@35963
    71
fun default_raw_params thy =
blanchet@35963
    72
  [("atps", [!atps]),
blanchet@35963
    73
   ("full_types", [if !full_types then "true" else "false"]),
blanchet@35963
    74
   ("timeout", [string_of_int (!timeout) ^ " s"])] @
blanchet@35963
    75
  Data.get thy
blanchet@35963
    76
blanchet@35963
    77
val infinity_time_in_secs = 60 * 60 * 24 * 365
blanchet@35963
    78
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
blanchet@35866
    79
blanchet@35963
    80
fun extract_params thy default_params override_params =
blanchet@35963
    81
  let
blanchet@35963
    82
    val override_params = map unnegate_raw_param override_params
blanchet@35963
    83
    val raw_params = rev override_params @ rev default_params
blanchet@35963
    84
    val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
blanchet@35963
    85
    val lookup_string = the_default "" o lookup
blanchet@35963
    86
    fun general_lookup_bool option default_value name =
blanchet@35963
    87
      case lookup name of
blanchet@35963
    88
        SOME s => s |> parse_bool_option option name
blanchet@35963
    89
      | NONE => default_value
blanchet@35963
    90
    val lookup_bool = the o general_lookup_bool false (SOME false)
blanchet@35963
    91
    val lookup_bool_option = general_lookup_bool true NONE
blanchet@35963
    92
    fun lookup_time name =
blanchet@35963
    93
      the_timeout (case lookup name of
blanchet@35963
    94
                     NONE => NONE
blanchet@35963
    95
                   | SOME s => parse_time_option name s)
blanchet@35963
    96
    fun lookup_real name =
blanchet@35963
    97
      case lookup name of
blanchet@35963
    98
        NONE => 0.0
blanchet@35963
    99
      | SOME s => 0.0 (* FIXME ### *)
blanchet@35963
   100
    val debug = lookup_bool "debug"
blanchet@35963
   101
    val verbose = debug orelse lookup_bool "verbose"
blanchet@35963
   102
    val atps = lookup_string "atps" |> space_explode " "
blanchet@35963
   103
    val full_types = lookup_bool "full_types"
blanchet@35963
   104
    val relevance_threshold = lookup_real "relevance_threshold"
blanchet@35963
   105
    val higher_order = lookup_bool_option "higher_order"
blanchet@35963
   106
    val respect_no_atp = lookup_bool "respect_no_atp"
blanchet@35963
   107
    val follow_defs = lookup_bool "follow_defs"
blanchet@35963
   108
    val isar_proof = lookup_bool "isar_proof"
blanchet@35963
   109
    val timeout = lookup_time "timeout"
blanchet@35963
   110
    val minimize_timeout = lookup_time "minimize_timeout"
blanchet@35963
   111
  in
blanchet@35963
   112
    {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
blanchet@35963
   113
     relevance_threshold = relevance_threshold, higher_order = higher_order,
blanchet@35963
   114
     respect_no_atp = respect_no_atp, follow_defs = follow_defs,
blanchet@35963
   115
     isar_proof = isar_proof, timeout = timeout,
blanchet@35963
   116
     minimize_timeout = minimize_timeout}
blanchet@35963
   117
  end
blanchet@35866
   118
blanchet@35963
   119
fun default_params thy =
blanchet@35963
   120
  extract_params thy (default_raw_params thy) o map (apsnd single)
blanchet@35866
   121
blanchet@35866
   122
fun atp_minimize_command args thm_names state =
blanchet@35866
   123
  let
blanchet@35963
   124
    val thy = Proof.theory_of state
blanchet@35963
   125
    val ctxt = Proof.context_of state
blanchet@35866
   126
    fun theorems_from_names ctxt =
blanchet@35866
   127
      map (fn (name, interval) =>
blanchet@35866
   128
              let
blanchet@35866
   129
                val thmref = Facts.Named ((name, Position.none), interval)
blanchet@35866
   130
                val ths = ProofContext.get_fact ctxt thmref
blanchet@35866
   131
                val name' = Facts.string_of_ref thmref
blanchet@35866
   132
              in (name', ths) end)
blanchet@35963
   133
    fun get_time_limit_arg s =
blanchet@35963
   134
      (case Int.fromString s of
blanchet@35963
   135
        SOME t => Time.fromSeconds t
blanchet@35963
   136
      | NONE => error ("Invalid time limit: " ^ quote s))
blanchet@35866
   137
    fun get_opt (name, a) (p, t) =
blanchet@35866
   138
      (case name of
blanchet@35866
   139
        "time" => (p, get_time_limit_arg a)
blanchet@35866
   140
      | "atp" => (a, t)
blanchet@35866
   141
      | n => error ("Invalid argument: " ^ n))
blanchet@35963
   142
    val {atps, minimize_timeout, ...} = default_params thy []
blanchet@35963
   143
    fun get_options args = fold get_opt args (hd atps, minimize_timeout)
blanchet@35963
   144
    val (atp, timeout) = get_options args
blanchet@35963
   145
    val params =
blanchet@35963
   146
      default_params thy
blanchet@35963
   147
          [("atps", atp),
blanchet@35963
   148
           ("minimize_timeout", string_of_int (Time.toSeconds timeout) ^ " s")]
blanchet@35866
   149
    val prover =
blanchet@35963
   150
      (case get_prover thy atp of
blanchet@35866
   151
        SOME prover => prover
blanchet@35963
   152
      | NONE => error ("Unknown ATP: " ^ quote atp))
blanchet@35963
   153
    val name_thms_pairs = theorems_from_names ctxt thm_names
blanchet@35866
   154
  in
blanchet@35963
   155
    writeln (#2 (minimize_theorems params linear_minimize prover atp state
blanchet@35963
   156
                                   name_thms_pairs))
blanchet@35866
   157
  end
blanchet@35866
   158
blanchet@35866
   159
val parse_args =
blanchet@35866
   160
  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
blanchet@35866
   161
val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
blanchet@35866
   162
val _ =
blanchet@35963
   163
  OuterSyntax.improper_command "atp_minimize"
blanchet@35963
   164
    "minimize theorem list with external prover" K.diag
blanchet@35866
   165
    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
blanchet@35866
   166
      Toplevel.no_timing o Toplevel.unknown_proof o
blanchet@35866
   167
        Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
blanchet@35866
   168
blanchet@35963
   169
fun hammer_away override_params i state =
blanchet@35963
   170
  let
blanchet@35963
   171
    val thy = Proof.theory_of state
blanchet@35963
   172
    val _ = List.app check_raw_param override_params
blanchet@35963
   173
    val params = extract_params thy (default_raw_params thy) override_params
blanchet@35963
   174
  in sledgehammer params i state end
blanchet@35963
   175
blanchet@35963
   176
fun sledgehammer_trans (opt_params, opt_i) =
blanchet@35963
   177
  Toplevel.keep (hammer_away (these opt_params) (the_default 1 opt_i)
blanchet@35963
   178
                 o Toplevel.proof_of)
blanchet@35963
   179
blanchet@35963
   180
fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
blanchet@35963
   181
blanchet@35963
   182
fun sledgehammer_params_trans opt_params =
blanchet@35963
   183
  Toplevel.theory
blanchet@35963
   184
      (fold set_default_raw_param (these opt_params)
blanchet@35963
   185
       #> tap (fn thy => 
blanchet@35963
   186
                  writeln ("Default parameters for Sledgehammer:\n" ^
blanchet@35963
   187
                           (case rev (default_raw_params thy) of
blanchet@35963
   188
                              [] => "none"
blanchet@35963
   189
                            | params =>
blanchet@35963
   190
                              (map check_raw_param params;
blanchet@35963
   191
                               params |> map string_for_raw_param
blanchet@35963
   192
                                      |> sort_strings |> cat_lines)))))
blanchet@35963
   193
blanchet@35963
   194
val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
blanchet@35963
   195
val parse_value =
blanchet@35963
   196
  Scan.repeat1 (P.minus >> single
blanchet@35963
   197
                || Scan.repeat1 (Scan.unless P.minus P.name)) >> flat
blanchet@35963
   198
val parse_param =
blanchet@35963
   199
  parse_key -- (Scan.option (P.$$$ "=" |-- parse_value) >> these)
blanchet@35963
   200
val parse_params =
blanchet@35963
   201
  Scan.option (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]")
blanchet@35963
   202
val parse_sledgehammer_command =
blanchet@35963
   203
  (parse_params -- Scan.option P.nat) #>> sledgehammer_trans
blanchet@35963
   204
val parse_sledgehammer_params_command =
blanchet@35963
   205
  parse_params #>> sledgehammer_params_trans
blanchet@35963
   206
blanchet@35963
   207
val _ =
blanchet@35963
   208
  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
blanchet@35963
   209
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill))
blanchet@35963
   210
val _ =
blanchet@35963
   211
  OuterSyntax.improper_command "atp_info"
blanchet@35963
   212
    "print information about managed provers" K.diag
blanchet@35963
   213
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info))
blanchet@35963
   214
val _ =
blanchet@35963
   215
  OuterSyntax.improper_command "atp_messages"
blanchet@35963
   216
    "print recent messages issued by managed provers" K.diag
blanchet@35963
   217
    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
blanchet@35963
   218
      (fn limit => Toplevel.no_timing
blanchet@35963
   219
                   o Toplevel.imperative (fn () => messages limit)))
blanchet@35963
   220
val _ =
blanchet@35963
   221
  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
blanchet@35963
   222
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
blanchet@35963
   223
      Toplevel.keep (print_provers o Toplevel.theory_of)))
blanchet@35963
   224
val _ =
blanchet@35963
   225
  OuterSyntax.improper_command "sledgehammer"
blanchet@35963
   226
    "search for first-order proof using automatic theorem provers" K.diag
blanchet@35963
   227
    parse_sledgehammer_command
blanchet@35963
   228
val _ =
blanchet@35963
   229
  OuterSyntax.command "sledgehammer_params"
blanchet@35963
   230
    "set and display the default parameters for Sledgehammer" K.thy_decl
blanchet@35963
   231
    parse_sledgehammer_params_command
blanchet@35866
   232
blanchet@35866
   233
end;