src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Fri, 27 May 2011 10:30:08 +0200
changeset 43013 3a95b1ae796d
parent 43011 5f8d74d3b297
child 43015 21b6baec55b1
permissions -rw-r--r--
shorten minimizer command further, exploiting until-now-undocumented syntax
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
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40941
diff changeset
     9
  type params = Sledgehammer_Provers.params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    10
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    11
  val auto : bool Unsynchronized.ref
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    12
  val provers : string Unsynchronized.ref
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    13
  val timeout : int Unsynchronized.ref
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    14
  val full_types : bool Unsynchronized.ref
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
    15
  val default_params : Proof.context -> (string * string) list -> params
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    16
  val setup : theory -> theory
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    17
end;
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    18
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    19
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    20
struct
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    21
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38021
diff changeset
    22
open ATP_Systems
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    23
open Sledgehammer_Util
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41136
diff changeset
    24
open Sledgehammer_ATP_Translate
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40941
diff changeset
    25
open Sledgehammer_Provers
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    26
open Sledgehammer_Minimize
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40941
diff changeset
    27
open Sledgehammer_Run
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    28
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    29
val auto = Unsynchronized.ref false
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    30
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    31
val _ =
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    32
  ProofGeneralPgip.add_preference Preferences.category_tracing
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    33
      (Preferences.bool_pref auto "auto-sledgehammer"
39327
blanchet
parents: 39324
diff changeset
    34
           "Run Sledgehammer automatically.")
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    35
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    36
(** Sledgehammer commands **)
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    37
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    38
val no_relevance_override = {add = [], del = [], only = false}
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    39
fun add_relevance_override ns : relevance_override =
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    40
  {add = ns, del = [], only = false}
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    41
fun del_relevance_override ns : relevance_override =
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    42
  {add = [], del = ns, only = false}
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    43
fun only_relevance_override ns : relevance_override =
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    44
  {add = ns, del = [], only = true}
36003
eb44a5d40b9e make SML/NJ happy
blanchet
parents: 35971
diff changeset
    45
fun merge_relevance_override_pairwise (r1 : relevance_override)
eb44a5d40b9e make SML/NJ happy
blanchet
parents: 35971
diff changeset
    46
                                      (r2 : relevance_override) =
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    47
  {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
    48
   only = #only r1 andalso #only r2}
36188
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
    49
fun merge_relevance_overrides rs =
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
    50
  fold merge_relevance_override_pairwise rs (only_relevance_override [])
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
    51
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    52
(*** parameters ***)
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    53
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    54
val provers = Unsynchronized.ref ""
39335
87a9ff4d5817 use 30 s instead of 60 s as the default Sledgehammer timeout;
blanchet
parents: 39327
diff changeset
    55
val timeout = Unsynchronized.ref 30
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    56
val full_types = Unsynchronized.ref false
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    57
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    58
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    59
  ProofGeneralPgip.add_preference Preferences.category_proof
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    60
      (Preferences.string_pref provers
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    61
          "Sledgehammer: Provers"
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    62
          "Default automatic provers (separated by whitespace)")
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    63
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    64
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    65
  ProofGeneralPgip.add_preference Preferences.category_proof
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    66
      (Preferences.int_pref timeout
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
    67
          "Sledgehammer: Time Limit"
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    68
          "ATPs will be interrupted after this time (in seconds)")
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    69
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    70
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    71
  ProofGeneralPgip.add_preference Preferences.category_proof
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    72
      (Preferences.bool_pref full_types
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
    73
          "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
    74
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    75
type raw_param = string * string list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    76
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    77
val default_default_params =
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
    78
  [("debug", "false"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    79
   ("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
    80
   ("overlord", "false"),
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
    81
   ("blocking", "false"),
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42447
diff changeset
    82
   ("type_sys", "smart"),
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41727
diff changeset
    83
   ("relevance_thresholds", "0.45 0.85"),
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41727
diff changeset
    84
   ("max_relevant", "smart"),
42783
226962b6a6d1 reduce the number of mono iterations to prevent the mono code from going berserk
blanchet
parents: 42776
diff changeset
    85
   ("max_mono_iters", "3"),
226962b6a6d1 reduce the number of mono iterations to prevent the mono code from going berserk
blanchet
parents: 42776
diff changeset
    86
   ("max_new_mono_instances", "400"),
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
   ("explicit_apply", "false"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    88
   ("isar_proof", "false"),
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
    89
   ("isar_shrink_factor", "1"),
43011
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43009
diff changeset
    90
   ("slicing", "true"),
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43009
diff changeset
    91
   ("metis_timeout", "5")]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    92
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
    93
val alias_params =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    94
  [("prover", "provers"),
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    95
   ("atps", "provers"), (* FIXME: legacy *)
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    96
   ("atp", "provers")]  (* FIXME: legacy *)
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
    97
val negated_alias_params =
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
    98
  [("no_debug", "debug"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    99
   ("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
   100
   ("no_overlord", "overlord"),
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
   101
   ("non_blocking", "blocking"),
36399
f2d83794333c rename options
blanchet
parents: 36395
diff changeset
   102
   ("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
   103
   ("implicit_apply", "explicit_apply"),
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   104
   ("no_isar_proof", "isar_proof"),
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   105
   ("no_slicing", "slicing")]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   106
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   107
val params_for_minimize =
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42688
diff changeset
   108
  ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
43011
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43009
diff changeset
   109
   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43009
diff changeset
   110
   "metis_timeout"]
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   111
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   112
val property_dependent_params = ["provers", "full_types", "timeout"]
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   113
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   114
fun is_known_raw_param s =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   115
  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
   116
  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
   117
  AList.defined (op =) negated_alias_params s orelse
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   118
  member (op =) property_dependent_params s orelse s = "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   119
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   120
fun is_prover_list ctxt s =
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   121
  case space_explode " " s of
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   122
    ss as _ :: _ => forall (is_prover_supported ctxt) ss
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   123
  | _ => false
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   124
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   125
(* Secret feature: "provers =" and "type_sys =" can be left out. *)
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   126
fun check_and_repair_raw_param ctxt (name, value) =
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   127
  if is_known_raw_param name then
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   128
    (name, value)
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   129
  else if is_prover_list ctxt name andalso null value then
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   130
    ("provers", [name])
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   131
  else if can type_sys_from_string name andalso null value then
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   132
    ("type_sys", [name])
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   133
  else
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   134
    error ("Unknown parameter: " ^ quote name ^ ".")
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   135
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   136
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
   137
  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
   138
    SOME name' => (name', value)
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   139
  | NONE =>
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   140
    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
   141
      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
   142
                              ["false"] => ["true"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   143
                            | ["true"] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   144
                            | [] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   145
                            | _ => value)
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   146
    | NONE => (name, value)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   147
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   148
(* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   149
   correctly. *)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   150
fun implode_param [s, "?"] = s ^ "?"
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   151
  | implode_param [s, "!"] = s ^ "!"
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   152
  | implode_param ss = space_implode " " ss
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   153
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   154
structure Data = Theory_Data
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   155
(
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   156
  type T = raw_param list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   157
  val empty = default_default_params |> map (apsnd single)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   158
  val extend = I
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   159
  fun merge data : T = AList.merge (op =) (K true) data
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   160
)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   161
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   162
fun remotify_prover_if_supported_and_not_already_remote ctxt name =
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   163
  if String.isPrefix remote_prefix name then
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   164
    SOME name
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   165
  else
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   166
    let val remote_name = remote_prefix ^ name in
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   167
      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   168
    end
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   169
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   170
fun remotify_prover_if_not_installed ctxt name =
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   171
  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40931
diff changeset
   172
    SOME name
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40931
diff changeset
   173
  else
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   174
    remotify_prover_if_supported_and_not_already_remote ctxt name
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   175
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   176
fun avoid_too_many_threads _ _ [] = []
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   177
  | avoid_too_many_threads _ (0, 0) _ = []
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   178
  | avoid_too_many_threads ctxt (0, max_remote) provers =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   179
    provers
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   180
    |> map_filter (remotify_prover_if_supported_and_not_already_remote ctxt)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   181
    |> take max_remote
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   182
  | avoid_too_many_threads _ (max_local, 0) provers =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   183
    provers
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   184
    |> filter_out (String.isPrefix remote_prefix)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   185
    |> take max_local
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   186
  | avoid_too_many_threads ctxt max_local_and_remote (prover :: provers) =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   187
    let
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   188
      val max_local_and_remote =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   189
        max_local_and_remote
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   190
        |> (if String.isPrefix remote_prefix prover then apsnd else apfst)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   191
              (Integer.add ~1)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   192
    in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   193
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   194
val max_default_remote_threads = 4
42688
097a61baeca9 smoother handling of ! and ? in type system names
blanchet
parents: 42613
diff changeset
   195
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   196
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   197
   timeout, it makes sense to put SPASS first. *)
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   198
fun default_provers_param_value ctxt =
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   199
  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN]
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40931
diff changeset
   200
  |> map_filter (remotify_prover_if_not_installed ctxt)
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   201
  |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   202
                                  max_default_remote_threads)
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   203
  |> implode_param
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   204
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   205
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   206
fun default_raw_params ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42237
diff changeset
   207
  let val thy = Proof_Context.theory_of ctxt in
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   208
    Data.get thy
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   209
    |> fold (AList.default (op =))
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   210
            [("provers", [case !provers of
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   211
                            "" => default_provers_param_value ctxt
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   212
                          | s => s]),
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   213
             ("full_types", [if !full_types then "true" else "false"]),
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   214
             ("timeout", let val timeout = !timeout in
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   215
                           [if timeout <= 0 then "none"
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40181
diff changeset
   216
                            else string_of_int timeout]
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   217
                         end)]
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   218
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   219
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   220
val infinity_time_in_secs = 60 * 60 * 24 * 365
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   221
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
   222
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   223
fun extract_params auto default_params override_params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   224
  let
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   225
    val override_params = map unalias_raw_param override_params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   226
    val raw_params = rev override_params @ rev default_params
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   227
    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   228
    val lookup_string = the_default "" o lookup
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   229
    fun general_lookup_bool option default_value name =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   230
      case lookup name of
35970
3d41a2a490f0 revert debugging output that shouldn't have been submitted in the first place
blanchet
parents: 35966
diff changeset
   231
        SOME s => parse_bool_option option name s
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   232
      | NONE => default_value
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   233
    val lookup_bool = the o general_lookup_bool false (SOME false)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   234
    fun lookup_time name =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   235
      case lookup name of
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   236
        SOME s => parse_time_option name s
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   237
      | NONE => NONE
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   238
    fun lookup_int name =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   239
      case lookup name of
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   240
        NONE => 0
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   241
      | SOME s => case Int.fromString s of
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   242
                    SOME n => n
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   243
                  | NONE => error ("Parameter " ^ quote name ^
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   244
                                   " must be assigned an integer value.")
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   245
    fun lookup_real_pair name =
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   246
      case lookup name of
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   247
        NONE => (0.0, 0.0)
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   248
      | SOME s => case s |> space_explode " " |> map Real.fromString of
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   249
                    [SOME r1, SOME r2] => (r1, r2)
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   250
                  | _ => error ("Parameter " ^ quote name ^
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   251
                                "must be assigned a pair of floating-point \
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   252
                                \values (e.g., \"0.6 0.95\")")
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   253
    fun lookup_int_option name =
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   254
      case lookup name of
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   255
        SOME "smart" => NONE
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   256
      | _ => SOME (lookup_int name)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   257
    val debug = not auto andalso lookup_bool "debug"
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   258
    val verbose = debug orelse (not auto andalso 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
   259
    val overlord = lookup_bool "overlord"
42995
e23f61546cf0 always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents: 42944
diff changeset
   260
    val blocking =
e23f61546cf0 always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents: 42944
diff changeset
   261
      Isabelle_Process.is_active () orelse auto orelse debug orelse
e23f61546cf0 always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents: 42944
diff changeset
   262
      lookup_bool "blocking"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   263
    val provers = lookup_string "provers" |> space_explode " "
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   264
                  |> auto ? single o hd
42548
ea2a28b1938f make sure the minimizer monomorphizes when it should
blanchet
parents: 42523
diff changeset
   265
    val type_sys =
42736
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   266
      if auto then
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   267
        Smart_Type_Sys true
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   268
      else case lookup_string "type_sys" of
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42589
diff changeset
   269
        "smart" => Smart_Type_Sys (lookup_bool "full_types")
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42589
diff changeset
   270
      | s => Dumb_Type_Sys (type_sys_from_string s)
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41727
diff changeset
   271
    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41727
diff changeset
   272
    val max_relevant = lookup_int_option "max_relevant"
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42688
diff changeset
   273
    val max_mono_iters = lookup_int "max_mono_iters"
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42736
diff changeset
   274
    val max_new_mono_instances = lookup_int "max_new_mono_instances"
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
   275
    val explicit_apply = lookup_bool "explicit_apply"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   276
    val isar_proof = lookup_bool "isar_proof"
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   277
    val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   278
    val slicing = not auto andalso lookup_bool "slicing"
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   279
    val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
43011
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43009
diff changeset
   280
    val metis_timeout =
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43009
diff changeset
   281
      if auto then Time.zeroTime else lookup_time "metis_timeout" |> the_timeout
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   282
    val expect = lookup_string "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   283
  in
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
   284
    {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41727
diff changeset
   285
     provers = provers, relevance_thresholds = relevance_thresholds,
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42688
diff changeset
   286
     max_relevant = max_relevant, max_mono_iters = max_mono_iters,
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42736
diff changeset
   287
     max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42688
diff changeset
   288
     explicit_apply = explicit_apply, isar_proof = isar_proof,
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42688
diff changeset
   289
     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
43011
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43009
diff changeset
   290
     timeout = timeout, metis_timeout = metis_timeout, expect = expect}
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   291
  end
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   292
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   293
fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   294
fun default_params thy = get_params false thy o map (apsnd single)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   295
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   296
(* Sledgehammer the given subgoal *)
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   297
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   298
val sledgehammerN = "sledgehammer"
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   299
val sledgehammer_paramsN = "sledgehammer_params"
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   300
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   301
val runN = "run"
43008
bb212c2ad238 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents: 42997
diff changeset
   302
val minN = "min"
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   303
val messagesN = "messages"
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   304
val supported_proversN = "supported_provers"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   305
val running_proversN = "running_provers"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   306
val kill_proversN = "kill_provers"
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   307
val refresh_tptpN = "refresh_tptp"
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   308
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   309
val is_raw_param_relevant_for_minimize =
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   310
  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
   311
fun string_for_raw_param (key, values) =
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   312
  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   313
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   314
fun minimize_command override_params i prover_name fact_names =
43013
3a95b1ae796d shorten minimizer command further, exploiting until-now-undocumented syntax
blanchet
parents: 43011
diff changeset
   315
  sledgehammerN ^ " " ^ minN ^ " [" ^ prover_name ^
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   316
  (override_params |> filter is_raw_param_relevant_for_minimize
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   317
                   |> 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
   318
  "] (" ^ space_implode " " fact_names ^ ")" ^
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   319
  (if i = 1 then "" else " " ^ string_of_int i)
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   320
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   321
fun hammer_away override_params subcommand opt_i relevance_override state =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   322
  let
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   323
    val ctxt = Proof.context_of state
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   324
    val override_params =
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   325
      override_params |> map (check_and_repair_raw_param ctxt)
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   326
  in
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   327
    if subcommand = runN then
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   328
      let val i = the_default 1 opt_i in
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   329
        run_sledgehammer (get_params false ctxt override_params) false i
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   330
                         relevance_override (minimize_command override_params i)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   331
                         state
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   332
        |> K ()
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   333
      end
43008
bb212c2ad238 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents: 42997
diff changeset
   334
    else if subcommand = minN then
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   335
      run_minimize (get_params false ctxt override_params) (the_default 1 opt_i)
38590
bd443b426d56 get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
blanchet
parents: 38589
diff changeset
   336
                   (#add relevance_override) state
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   337
    else if subcommand = messagesN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   338
      messages opt_i
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   339
    else if subcommand = supported_proversN then
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   340
      supported_provers ctxt
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   341
    else if subcommand = running_proversN then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   342
      running_provers ()
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   343
    else if subcommand = kill_proversN then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   344
      kill_provers ()
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   345
    else if subcommand = refresh_tptpN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   346
      refresh_systems_on_tptp ()
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   347
    else
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   348
      error ("Unknown subcommand: " ^ quote subcommand ^ ".")
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   349
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   350
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   351
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
   352
  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
   353
                 o Toplevel.proof_of)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   354
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   355
fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   356
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   357
fun sledgehammer_params_trans params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   358
  Toplevel.theory
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   359
      (fold set_default_raw_param params
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   360
       #> tap (fn thy =>
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42237
diff changeset
   361
                  let val ctxt = Proof_Context.init_global thy in
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   362
                    writeln ("Default parameters for Sledgehammer:\n" ^
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   363
                             (case default_raw_params ctxt |> rev of
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   364
                                [] => "none"
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   365
                              | params =>
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   366
                                params |> map (check_and_repair_raw_param ctxt)
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   367
                                       |> map string_for_raw_param
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   368
                                       |> sort_strings |> cat_lines))
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   369
                  end))
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   370
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   371
val parse_key =
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   372
  Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!")
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   373
               >> implode_param
42581
398fff2c6b8f use ! for mildly unsound and !! for very unsound encodings
blanchet
parents: 42579
diff changeset
   374
val parse_value =
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42581
diff changeset
   375
  Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
42581
398fff2c6b8f use ! for mildly unsound and !! for very unsound encodings
blanchet
parents: 42579
diff changeset
   376
                || Parse.$$$ "!")
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   377
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   378
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
   379
val parse_fact_refs =
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38988
diff changeset
   380
  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   381
val parse_relevance_chunk =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   382
  (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   383
  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_relevance_override)
36188
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
   384
  || (parse_fact_refs >> only_relevance_override)
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   385
val parse_relevance_override =
36188
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
   386
  Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
35b9f0db49a0 fiddle with Sledgehammer option syntax
blanchet
parents: 36183
diff changeset
   387
                              >> merge_relevance_overrides))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   388
                no_relevance_override
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   389
val parse_sledgehammer_command =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37344
diff changeset
   390
  (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
   391
   -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   392
val parse_sledgehammer_params_command =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   393
  parse_params #>> sledgehammer_params_trans
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   394
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   395
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   396
  Outer_Syntax.improper_command sledgehammerN
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   397
      "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
   398
      parse_sledgehammer_command
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   399
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   400
  Outer_Syntax.command sledgehammer_paramsN
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   401
      "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
   402
      parse_sledgehammer_params_command
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
   403
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   404
fun auto_sledgehammer state =
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40599
diff changeset
   405
  let val ctxt = Proof.context_of state in
42447
blanchet
parents: 42444
diff changeset
   406
    run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
blanchet
parents: 42444
diff changeset
   407
                     (minimize_command [] 1) state
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40599
diff changeset
   408
  end
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   409
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40599
diff changeset
   410
val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   411
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   412
end;