src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37617 f73cd4069f69
child 37926 e6ff246c0cdb
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36375
2482446a604c move the minimizer to the Sledgehammer directory
blanchet
parents: 36373
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     3
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     4
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     5
*)
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     6
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
     7
signature SLEDGEHAMMER_ISAR =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
     8
sig
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
     9
  type params = ATP_Manager.params
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    10
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    11
  val atps: string Unsynchronized.ref
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    12
  val timeout: int Unsynchronized.ref
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    13
  val full_types: bool Unsynchronized.ref
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    14
  val default_params : theory -> (string * string) list -> params
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    15
end;
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    16
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    17
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    18
struct
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    19
37574
b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents: 37567
diff changeset
    20
open Clausifier
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    21
open Sledgehammer_Util
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37584
diff changeset
    22
open Sledgehammer_Fact_Filter
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    23
open ATP_Manager
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36375
diff changeset
    24
open ATP_Systems
36375
2482446a604c move the minimizer to the Sledgehammer directory
blanchet
parents: 36373
diff changeset
    25
open Sledgehammer_Fact_Minimizer
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    26
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    27
(** Sledgehammer commands **)
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    28
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    29
fun add_to_relevance_override ns : relevance_override =
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    30
  {add = ns, del = [], only = false}
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    31
fun del_from_relevance_override ns : relevance_override =
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    32
  {add = [], del = ns, only = false}
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    33
fun only_relevance_override ns : relevance_override =
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    34
  {add = ns, del = [], only = true}
36003
eb44a5d40b9e make SML/NJ happy
blanchet
parents: 35971
diff changeset
    35
fun merge_relevance_override_pairwise (r1 : relevance_override)
eb44a5d40b9e make SML/NJ happy
blanchet
parents: 35971
diff changeset
    36
                                      (r2 : relevance_override) =
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    37
  {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
36183
f723348b2231 Sledgehammer: the empty set of fact () should mean nothing, not unchanged
blanchet
parents: 36143
diff changeset
    38
   only = #only r1 andalso #only r2}
36188
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
    39
fun merge_relevance_overrides rs =
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
    40
  fold merge_relevance_override_pairwise rs (only_relevance_override [])
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
    41
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    42
(*** parameters ***)
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    43
36908
fb18db78be80 delect installed ATPs dynamically, _not_ at image built time
blanchet
parents: 36607
diff changeset
    44
val atps = Unsynchronized.ref ""
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    45
val timeout = Unsynchronized.ref 60
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    46
val full_types = Unsynchronized.ref false
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    47
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    48
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    49
  ProofGeneralPgip.add_preference Preferences.category_proof
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    50
      (Preferences.string_pref atps
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    51
          "Sledgehammer: ATPs"
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    52
          "Default automatic provers (separated by whitespace)")
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    53
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    54
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    55
  ProofGeneralPgip.add_preference Preferences.category_proof
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    56
      (Preferences.int_pref timeout
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
    57
          "Sledgehammer: Time Limit"
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    58
          "ATPs will be interrupted after this time (in seconds)")
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    59
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    60
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    61
  ProofGeneralPgip.add_preference Preferences.category_proof
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    62
      (Preferences.bool_pref full_types
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
    63
          "Sledgehammer: Full Types" "ATPs will use full type information")
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    64
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    65
type raw_param = string * string list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    66
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    67
val default_default_params =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    68
  [("debug", "false"),
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    69
   ("verbose", "false"),
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36142
diff changeset
    70
   ("overlord", "false"),
36235
61159615a0c5 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents: 36223
diff changeset
    71
   ("explicit_apply", "false"),
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    72
   ("relevance_threshold", "50"),
36922
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
    73
   ("relevance_convergence", "320"),
36220
f3655a3ae1ab rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents: 36189
diff changeset
    74
   ("theory_relevant", "smart"),
36922
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
    75
   ("defs_relevant", "false"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    76
   ("isar_proof", "false"),
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
    77
   ("isar_shrink_factor", "1"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    78
   ("minimize_timeout", "5 s")]
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    79
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
    80
val alias_params =
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
    81
  [("atp", "atps")]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
    82
val negated_alias_params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    83
  [("no_debug", "debug"),
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    84
   ("quiet", "verbose"),
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36142
diff changeset
    85
   ("no_overlord", "overlord"),
36399
f2d83794333c rename options
blanchet
parents: 36395
diff changeset
    86
   ("partial_types", "full_types"),
36235
61159615a0c5 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents: 36223
diff changeset
    87
   ("implicit_apply", "explicit_apply"),
36220
f3655a3ae1ab rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents: 36189
diff changeset
    88
   ("theory_irrelevant", "theory_relevant"),
36922
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
    89
   ("defs_irrelevant", "defs_relevant"),
36908
fb18db78be80 delect installed ATPs dynamically, _not_ at image built time
blanchet
parents: 36607
diff changeset
    90
   ("no_isar_proof", "isar_proof")]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    91
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
    92
val params_for_minimize =
36399
f2d83794333c rename options
blanchet
parents: 36395
diff changeset
    93
  ["debug", "verbose", "overlord", "full_types", "explicit_apply",
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
    94
   "isar_proof", "isar_shrink_factor", "minimize_timeout"]
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
    95
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    96
val property_dependent_params = ["atps", "full_types", "timeout"]
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    97
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    98
fun is_known_raw_param s =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    99
  AList.defined (op =) default_default_params s orelse
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   100
  AList.defined (op =) alias_params s orelse
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   101
  AList.defined (op =) negated_alias_params s orelse
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
   102
  member (op =) property_dependent_params s
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   103
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   104
fun check_raw_param (s, _) =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   105
  if is_known_raw_param s then ()
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   106
  else error ("Unknown parameter: " ^ quote s ^ ".")
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   107
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   108
fun unalias_raw_param (name, value) =
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   109
  case AList.lookup (op =) alias_params name of
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   110
    SOME name' => (name', value)
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   111
  | NONE =>
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   112
    case AList.lookup (op =) negated_alias_params name of
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   113
      SOME name' => (name', case value of
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   114
                              ["false"] => ["true"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   115
                            | ["true"] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   116
                            | [] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   117
                            | _ => value)
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   118
    | NONE => (name, value)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   119
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   120
structure Data = Theory_Data(
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   121
  type T = raw_param list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   122
  val empty = default_default_params |> map (apsnd single)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   123
  val extend = I
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   124
  fun merge p : T = AList.merge (op =) (K true) p)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   125
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   126
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   127
fun default_raw_params thy =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   128
  Data.get thy
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   129
  |> fold (AList.default (op =))
36908
fb18db78be80 delect installed ATPs dynamically, _not_ at image built time
blanchet
parents: 36607
diff changeset
   130
          [("atps", [case !atps of "" => default_atps_param_value () | s => s]),
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   131
           ("full_types", [if !full_types then "true" else "false"]),
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36141
diff changeset
   132
           ("timeout", let val timeout = !timeout in
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36141
diff changeset
   133
                         [if timeout <= 0 then "none"
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36141
diff changeset
   134
                          else string_of_int timeout ^ " s"]
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36141
diff changeset
   135
                       end)]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   136
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   137
val infinity_time_in_secs = 60 * 60 * 24 * 365
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   138
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   139
37498
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37399
diff changeset
   140
fun extract_params default_params override_params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   141
  let
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   142
    val override_params = map unalias_raw_param override_params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   143
    val raw_params = rev override_params @ rev default_params
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   144
    val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   145
    val lookup_string = the_default "" o lookup
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   146
    fun general_lookup_bool option default_value name =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   147
      case lookup name of
35970
3d41a2a490f0 revert debugging output that shouldn't have been submitted in the first place
blanchet
parents: 35966
diff changeset
   148
        SOME s => parse_bool_option option name s
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   149
      | NONE => default_value
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   150
    val lookup_bool = the o general_lookup_bool false (SOME false)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   151
    val lookup_bool_option = general_lookup_bool true NONE
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   152
    fun lookup_time name =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   153
      the_timeout (case lookup name of
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   154
                     NONE => NONE
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   155
                   | SOME s => parse_time_option name s)
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   156
    fun lookup_int name =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   157
      case lookup name of
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   158
        NONE => 0
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   159
      | SOME s => case Int.fromString s of
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   160
                    SOME n => n
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   161
                  | NONE => error ("Parameter " ^ quote name ^
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   162
                                   " must be assigned an integer value.")
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   163
    val debug = lookup_bool "debug"
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   164
    val verbose = debug orelse lookup_bool "verbose"
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36142
diff changeset
   165
    val overlord = lookup_bool "overlord"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   166
    val atps = lookup_string "atps" |> space_explode " "
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   167
    val full_types = lookup_bool "full_types"
36235
61159615a0c5 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents: 36223
diff changeset
   168
    val explicit_apply = lookup_bool "explicit_apply"
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   169
    val relevance_threshold =
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   170
      0.01 * Real.fromInt (lookup_int "relevance_threshold")
36922
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
   171
    val relevance_convergence =
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
   172
      0.01 * Real.fromInt (lookup_int "relevance_convergence")
36220
f3655a3ae1ab rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents: 36189
diff changeset
   173
    val theory_relevant = lookup_bool_option "theory_relevant"
36922
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
   174
    val defs_relevant = lookup_bool "defs_relevant"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   175
    val isar_proof = lookup_bool "isar_proof"
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   176
    val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   177
    val timeout = lookup_time "timeout"
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   178
    val minimize_timeout = lookup_time "minimize_timeout"
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   179
  in
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36142
diff changeset
   180
    {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
36235
61159615a0c5 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents: 36223
diff changeset
   181
     full_types = full_types, explicit_apply = explicit_apply,
37580
c2c1caff5dea got rid of "respect_no_atp" option, which even I don't use
blanchet
parents: 37574
diff changeset
   182
     relevance_threshold = relevance_threshold,
36922
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
   183
     relevance_convergence = relevance_convergence,
12f87df9c1a5 renamed two Sledgehammer options
blanchet
parents: 36908
diff changeset
   184
     theory_relevant = theory_relevant, defs_relevant = defs_relevant,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   185
     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   186
     timeout = timeout, minimize_timeout = minimize_timeout}
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   187
  end
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   188
37498
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37399
diff changeset
   189
fun get_params thy = extract_params (default_raw_params thy)
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   190
fun default_params thy = get_params thy o map (apsnd single)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   191
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   192
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   193
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   194
(* Sledgehammer the given subgoal *)
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   195
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   196
fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   197
  | run (params as {atps, ...}) i relevance_override minimize_command state =
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   198
    case subgoal_count state of
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   199
      0 => priority "No subgoal!"
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   200
    | n =>
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   201
      let
37326
bf5d936bb985 kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
blanchet
parents: 37171
diff changeset
   202
        val _ = kill_atps ()
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   203
        val _ = priority "Sledgehammering..."
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37580
diff changeset
   204
        val _ = app (start_prover_thread params i n relevance_override
2e289dc13615 factor out thread creation
blanchet
parents: 37580
diff changeset
   205
                                         minimize_command state) atps
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   206
      in () end
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   207
37344
40f379944c1e totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents: 37328
diff changeset
   208
fun minimize override_params i refs state =
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   209
  let
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   210
    val thy = Proof.theory_of state
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   211
    val ctxt = Proof.context_of state
37171
fc1e20373e6a make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
blanchet
parents: 36960
diff changeset
   212
    val chained_ths = #facts (Proof.goal state)
37344
40f379944c1e totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents: 37328
diff changeset
   213
    val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   214
  in
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   215
    case subgoal_count state of
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   216
      0 => priority "No subgoal!"
37326
bf5d936bb985 kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
blanchet
parents: 37171
diff changeset
   217
    | n =>
bf5d936bb985 kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
blanchet
parents: 37171
diff changeset
   218
      (kill_atps ();
bf5d936bb985 kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
blanchet
parents: 37171
diff changeset
   219
       priority (#2 (minimize_theorems (get_params thy override_params) i n
bf5d936bb985 kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
blanchet
parents: 37171
diff changeset
   220
                                       state name_thms_pairs)))
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   221
  end
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   222
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   223
val sledgehammerN = "sledgehammer"
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   224
val sledgehammer_paramsN = "sledgehammer_params"
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   225
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   226
val runN = "run"
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   227
val minimizeN = "minimize"
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   228
val messagesN = "messages"
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   229
val available_atpsN = "available_atps"
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   230
val running_atpsN = "running_atps"
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   231
val kill_atpsN = "kill_atps"
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   232
val refresh_tptpN = "refresh_tptp"
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   233
36141
c31602d268be make Sledgehammer's "timeout" option work for "minimize"
blanchet
parents: 36140
diff changeset
   234
fun minimizize_raw_param_name "timeout" = "minimize_timeout"
c31602d268be make Sledgehammer's "timeout" option work for "minimize"
blanchet
parents: 36140
diff changeset
   235
  | minimizize_raw_param_name name = name
c31602d268be make Sledgehammer's "timeout" option work for "minimize"
blanchet
parents: 36140
diff changeset
   236
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   237
val is_raw_param_relevant_for_minimize =
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   238
  member (op =) params_for_minimize o fst o unalias_raw_param
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   239
fun string_for_raw_param (key, values) =
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   240
  key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   241
37171
fc1e20373e6a make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
blanchet
parents: 36960
diff changeset
   242
fun minimize_command override_params i atp_name fact_names =
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   243
  sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   244
  (override_params |> filter is_raw_param_relevant_for_minimize
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   245
                   |> implode o map (prefix ", " o string_for_raw_param)) ^
37171
fc1e20373e6a make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
blanchet
parents: 36960
diff changeset
   246
  "] (" ^ space_implode " " fact_names ^ ")" ^
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   247
  (if i = 1 then "" else " " ^ string_of_int i)
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   248
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   249
fun hammer_away override_params subcommand opt_i relevance_override state =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   250
  let
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   251
    val thy = Proof.theory_of state
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36473
diff changeset
   252
    val _ = app check_raw_param override_params
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   253
  in
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   254
    if subcommand = runN then
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   255
      let val i = the_default 1 opt_i in
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   256
        run (get_params thy override_params) i relevance_override
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   257
            (minimize_command override_params i) state
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   258
      end
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   259
    else if subcommand = minimizeN then
36378
f32c567dbcaa remove some bloat
blanchet
parents: 36376
diff changeset
   260
      minimize (map (apfst minimizize_raw_param_name) override_params)
36141
c31602d268be make Sledgehammer's "timeout" option work for "minimize"
blanchet
parents: 36140
diff changeset
   261
               (the_default 1 opt_i) (#add relevance_override) state
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   262
    else if subcommand = messagesN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   263
      messages opt_i
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   264
    else if subcommand = available_atpsN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   265
      available_atps thy
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   266
    else if subcommand = running_atpsN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   267
      running_atps ()
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   268
    else if subcommand = kill_atpsN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   269
      kill_atps ()
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   270
    else if subcommand = refresh_tptpN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   271
      refresh_systems_on_tptp ()
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   272
    else
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   273
      error ("Unknown subcommand: " ^ quote subcommand ^ ".")
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   274
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   275
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   276
fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   277
  Toplevel.keep (hammer_away params subcommand opt_i relevance_override
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   278
                 o Toplevel.proof_of)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   279
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   280
fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   281
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   282
fun sledgehammer_params_trans params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   283
  Toplevel.theory
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   284
      (fold set_default_raw_param params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   285
       #> tap (fn thy => 
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   286
                  writeln ("Default parameters for Sledgehammer:\n" ^
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   287
                           (case rev (default_raw_params thy) of
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   288
                              [] => "none"
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   289
                            | params =>
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   290
                              (map check_raw_param params;
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   291
                               params |> map string_for_raw_param
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   292
                                      |> sort_strings |> cat_lines)))))
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   293
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   294
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   295
val parse_value = Scan.repeat1 Parse.xname
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   296
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   297
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   298
val parse_fact_refs =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   299
  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   300
                            (Parse.xname -- Scan.option Attrib.thm_sel)
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   301
                >> (fn (name, interval) =>
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   302
                       Facts.Named ((name, Position.none), interval)))
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   303
val parse_relevance_chunk =
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   304
  (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   305
  || (Args.del |-- Args.colon |-- parse_fact_refs
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   306
      >> del_from_relevance_override)
36188
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
   307
  || (parse_fact_refs >> only_relevance_override)
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   308
val parse_relevance_override =
36188
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
   309
  Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
   310
                              >> merge_relevance_overrides))
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
   311
                (add_to_relevance_override [])
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   312
val parse_sledgehammer_command =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37344
diff changeset
   313
  (Scan.optional Parse.short_ident runN -- parse_params
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37344
diff changeset
   314
   -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   315
val parse_sledgehammer_params_command =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   316
  parse_params #>> sledgehammer_params_trans
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   317
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   318
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   319
  Outer_Syntax.improper_command sledgehammerN
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   320
      "search for first-order proof using automatic theorem provers" Keyword.diag
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
   321
      parse_sledgehammer_command
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   322
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   323
  Outer_Syntax.command sledgehammer_paramsN
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   324
      "set and display the default parameters for Sledgehammer" Keyword.thy_decl
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
   325
      parse_sledgehammer_params_command
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
   326
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   327
end;