src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author wenzelm
Sat, 17 Aug 2013 19:54:16 +0200
changeset 53053 6a3320758f0d
parent 53052 a0db255af8c5
child 53055 0fe8a9972eda
permissions -rw-r--r--
always enable "minimize" to simplify interaction model; override params more directly -- they are no longer echoed in minimize command;
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
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    11
  val provers : string Unsynchronized.ref
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    12
  val timeout : int Unsynchronized.ref
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
    13
  val default_params : Proof.context -> (string * string) list -> params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    14
end;
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    15
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    16
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    17
struct
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    18
44784
blanchet
parents: 44768
diff changeset
    19
open ATP_Util
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38021
diff changeset
    20
open ATP_Systems
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    21
open ATP_Problem_Generate
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    22
open ATP_Proof_Reconstruct
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    23
open Sledgehammer_Util
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 47962
diff changeset
    24
open Sledgehammer_Fact
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
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48332
diff changeset
    27
open Sledgehammer_MaSh
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40941
diff changeset
    28
open Sledgehammer_Run
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    29
48433
9e9b6e363859 don't relearn old facts in Isar mode
blanchet
parents: 48432
diff changeset
    30
(* val cvc3N = "cvc3" *)
48405
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
    31
val yicesN = "yices"
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
    32
val z3N = "z3"
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
    33
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    34
val runN = "run"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    35
val minN = "min"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    36
val messagesN = "messages"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    37
val supported_proversN = "supported_provers"
50719
58b0b44da54a renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
blanchet
parents: 50604
diff changeset
    38
val kill_allN = "kill_all"
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    39
val running_proversN = "running_provers"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
    40
val running_learnersN = "running_learners"
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    41
val refresh_tptpN = "refresh_tptp"
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48293
diff changeset
    42
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    43
val _ =
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents: 52556
diff changeset
    44
  ProofGeneral.preference_option ProofGeneral.category_tracing
52017
bc0238c1f73a clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents: 52007
diff changeset
    45
    NONE
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents: 52556
diff changeset
    46
    @{option auto_sledgehammer}
52017
bc0238c1f73a clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents: 52007
diff changeset
    47
    "auto-sledgehammer"
bc0238c1f73a clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents: 52007
diff changeset
    48
    "Run Sledgehammer automatically"
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    49
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    50
(** Sledgehammer commands **)
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    51
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    52
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    53
fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    54
fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    55
fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    56
  {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
    57
   only = #only r1 andalso #only r2}
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    58
fun merge_fact_overrides rs =
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    59
  fold merge_fact_override_pairwise rs (only_fact_override [])
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
    60
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    61
(*** parameters ***)
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    62
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    63
val provers = Unsynchronized.ref ""
39335
87a9ff4d5817 use 30 s instead of 60 s as the default Sledgehammer timeout;
blanchet
parents: 39327
diff changeset
    64
val timeout = Unsynchronized.ref 30
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    65
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    66
val _ =
52007
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    67
  ProofGeneral.preference_string ProofGeneral.category_proof
52017
bc0238c1f73a clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents: 52007
diff changeset
    68
    NONE
52007
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    69
    provers
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    70
    "Sledgehammer: Provers"
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    71
    "Default automatic provers (separated by whitespace)"
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    72
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    73
val _ =
52007
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    74
  ProofGeneral.preference_int ProofGeneral.category_proof
52017
bc0238c1f73a clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents: 52007
diff changeset
    75
    NONE
52007
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    76
    timeout
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    77
    "Sledgehammer: Time Limit"
0b1183012a3c maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents: 52006
diff changeset
    78
    "ATPs will be interrupted after this time (in seconds)"
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    79
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    80
type raw_param = string * string list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    81
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    82
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
    83
  [("debug", "false"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    84
   ("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
    85
   ("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
    86
   ("blocking", "false"),
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
    87
   ("type_enc", "smart"),
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
    88
   ("strict", "false"),
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45063
diff changeset
    89
   ("lam_trans", "smart"),
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
    90
   ("uncurried_aliases", "smart"),
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    91
   ("learn", "true"),
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
    92
   ("fact_filter", "smart"),
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
    93
   ("max_facts", "smart"),
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    94
   ("fact_thresholds", "0.45 0.85"),
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
    95
   ("max_mono_iters", "smart"),
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
    96
   ("max_new_mono_instances", "smart"),
51190
2654b3965c8d made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents: 51189
diff changeset
    97
   ("isar_proofs", "smart"),
51130
76d68444cd59 renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents: 50824
diff changeset
    98
   ("isar_compress", "10"),
52556
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52366
diff changeset
    99
   ("isar_compress_degree", "2"), (* TODO: document; right value?? *)
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52366
diff changeset
   100
   ("merge_timeout_slack", "1.2"), (* TODO: document *)
52632
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   101
   ("isar_try0", "true"), (* TODO: document *)
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   102
   ("isar_minimize", "true"), (* TODO: document *)
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
   103
   ("slice", "true"),
45707
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   104
   ("minimize", "smart"),
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51557
diff changeset
   105
   ("preplay_timeout", "3"),
ee9562d31778 added preplay tracing
smolkas
parents: 51557
diff changeset
   106
   ("preplay_trace", "false")] (* TODO: document *)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   107
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   108
val alias_params =
51138
583a37b9512d killed legacy alias
blanchet
parents: 51130
diff changeset
   109
  [("prover", ("provers", [])), (* undocumented *)
51189
a55ef201b19d alias for people like me
blanchet
parents: 51138
diff changeset
   110
   ("dont_preplay", ("preplay_timeout", ["0"])),
52093
f5280907284d added compatibility alias
blanchet
parents: 52031
diff changeset
   111
   ("dont_compress_isar", ("isar_compress", ["0"])),
f5280907284d added compatibility alias
blanchet
parents: 52031
diff changeset
   112
   ("isar_proof", ("isar_proofs", [])) (* legacy *)]
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   113
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
   114
  [("no_debug", "debug"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   115
   ("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
   116
   ("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
   117
   ("non_blocking", "blocking"),
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   118
   ("non_strict", "strict"),
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   119
   ("no_uncurried_aliases", "uncurried_aliases"),
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   120
   ("dont_learn", "learn"),
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   121
   ("no_isar_proofs", "isar_proofs"),
45707
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   122
   ("dont_slice", "slice"),
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51557
diff changeset
   123
   ("dont_minimize", "minimize"),
52632
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   124
   ("dont_try0_isar", "isar_try0"),
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   125
   ("dont_minimize_isar", "isar_minimize"),
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51557
diff changeset
   126
   ("no_preplay_trace", "preplay_trace")] (* TODO: document *)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   127
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   128
val params_for_minimize =
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   129
  ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   130
   "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
51130
76d68444cd59 renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents: 50824
diff changeset
   131
   "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
52632
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   132
(* TODO: add isar_compress_degree, merge_timeout_slack,  preplay_trace,
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   133
   isar_try0, isar_minimize? *)
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   134
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43353
diff changeset
   135
val property_dependent_params = ["provers", "timeout"]
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   136
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   137
fun is_known_raw_param s =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   138
  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
   139
  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
   140
  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
   141
  member (op =) property_dependent_params s orelse s = "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   142
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   143
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
   144
  case space_explode " " s of
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   145
    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
   146
  | _ => false
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   147
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   148
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
   149
  case AList.lookup (op =) alias_params name of
47037
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   150
    SOME (name', []) => (name', value)
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   151
  | SOME (param' as (name', _)) =>
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   152
    if value <> ["false"] then
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   153
      param'
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   154
    else
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   155
      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   156
             \(cf. " ^ quote name' ^ ").")
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   157
  | NONE =>
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   158
    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
   159
      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
   160
                              ["false"] => ["true"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   161
                            | ["true"] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   162
                            | [] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   163
                            | _ => value)
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   164
    | NONE => (name, value)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   165
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 52018
diff changeset
   166
val any_type_enc = type_enc_of_string Strict "erased"
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45063
diff changeset
   167
48397
9fe826095a02 convenience
blanchet
parents: 48395
diff changeset
   168
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
9fe826095a02 convenience
blanchet
parents: 48395
diff changeset
   169
   can be omitted. For the last four, this is a secret feature. *)
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   170
fun normalize_raw_param ctxt =
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   171
  unalias_raw_param
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   172
  #> (fn (name, value) =>
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   173
         if is_known_raw_param name then
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   174
           (name, value)
48533
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   175
         else if null value then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   176
           if is_prover_list ctxt name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   177
             ("provers", [name])
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 52018
diff changeset
   178
           else if can (type_enc_of_string Strict) name then
48533
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   179
             ("type_enc", [name])
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 52018
diff changeset
   180
           else if can (trans_lams_of_string ctxt any_type_enc) name then
48533
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   181
             ("lam_trans", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   182
           else if member (op =) fact_filters name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   183
             ("fact_filter", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   184
           else if is_some (Int.fromString name) then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   185
             ("max_facts", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   186
           else
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   187
             error ("Unknown parameter: " ^ quote name ^ ".")
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   188
         else
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   189
           error ("Unknown parameter: " ^ quote name ^ "."))
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   190
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46409
diff changeset
   191
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44784
diff changeset
   192
   read correctly. *)
44784
blanchet
parents: 44768
diff changeset
   193
val implode_param = strip_spaces_except_between_idents o space_implode " "
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   194
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   195
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
   196
(
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   197
  type T = raw_param list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   198
  val empty = default_default_params |> map (apsnd single)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   199
  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
   200
  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
   201
)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   202
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   203
fun avoid_too_many_threads _ _ [] = []
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   204
  | avoid_too_many_threads _ (0, 0) _ = []
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   205
  | 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
   206
    provers
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   207
    |> 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
   208
    |> take max_remote
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   209
  | avoid_too_many_threads _ (max_local, 0) provers =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   210
    provers
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   211
    |> filter_out (String.isPrefix remote_prefix)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   212
    |> take max_local
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   213
  | 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
   214
    let
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   215
      val max_local_and_remote =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   216
        max_local_and_remote
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   217
        |> (if String.isPrefix remote_prefix prover then apsnd else apfst)
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48405
diff changeset
   218
               (Integer.add ~1)
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   219
    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
   220
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   221
val max_default_remote_threads = 4
42688
097a61baeca9 smoother handling of ! and ? in type system names
blanchet
parents: 42613
diff changeset
   222
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   223
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
48405
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
   224
   timeout, it makes sense to put E first. *)
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   225
fun default_provers_param_value ctxt =
48432
60759d07df24 took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents: 48406
diff changeset
   226
  [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40931
diff changeset
   227
  |> 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
   228
  |> 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
   229
                                  max_default_remote_threads)
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   230
  |> implode_param
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   231
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   232
fun set_default_raw_param param thy =
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   233
  let val ctxt = Proof_Context.init_global thy in
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   234
    thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   235
  end
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   236
fun default_raw_params ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42237
diff changeset
   237
  let val thy = Proof_Context.theory_of ctxt in
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   238
    Data.get thy
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   239
    |> fold (AList.default (op =))
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   240
            [("provers", [case !provers of
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   241
                            "" => default_provers_param_value ctxt
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   242
                          | s => s]),
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   243
             ("timeout", let val timeout = !timeout in
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   244
                           [if timeout <= 0 then "none"
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40181
diff changeset
   245
                            else string_of_int timeout]
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   246
                         end)]
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   247
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   248
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   249
fun extract_params mode default_params override_params =
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 raw_params = rev override_params @ rev default_params
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   252
    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   253
    val lookup_string = the_default "" o lookup
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   254
    fun general_lookup_bool option default_value name =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   255
      case lookup name of
35970
3d41a2a490f0 revert debugging output that shouldn't have been submitted in the first place
blanchet
parents: 35966
diff changeset
   256
        SOME s => parse_bool_option option name s
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   257
      | NONE => default_value
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   258
    val lookup_bool = the o general_lookup_bool false (SOME false)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   259
    fun lookup_time name =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   260
      case lookup name of
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   261
        SOME s => parse_time_option name s
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   262
      | NONE => NONE
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   263
    fun lookup_int name =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   264
      case lookup name of
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   265
        NONE => 0
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   266
      | SOME s => case Int.fromString s of
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   267
                    SOME n => n
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   268
                  | NONE => error ("Parameter " ^ quote name ^
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   269
                                   " must be assigned an integer value.")
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   270
    fun lookup_real name =
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   271
      case lookup name of
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   272
        NONE => 0.0
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   273
      | SOME s => case Real.fromString s of
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   274
                    SOME n => n
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   275
                  | NONE => error ("Parameter " ^ quote name ^
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   276
                                   " must be assigned a real value.")
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   277
    fun lookup_real_pair name =
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   278
      case lookup name of
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   279
        NONE => (0.0, 0.0)
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   280
      | 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
   281
                    [SOME r1, SOME r2] => (r1, r2)
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   282
                  | _ => error ("Parameter " ^ quote name ^
49632
c44b2a404687 tuned message
blanchet
parents: 49365
diff changeset
   283
                                " must be assigned a pair of floating-point \
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   284
                                \values (e.g., \"0.6 0.95\")")
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43057
diff changeset
   285
    fun lookup_option lookup' name =
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   286
      case lookup name of
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   287
        SOME "smart" => NONE
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43057
diff changeset
   288
      | _ => SOME (lookup' name)
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   289
    val debug = mode <> Auto_Try andalso lookup_bool "debug"
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   290
    val verbose = debug orelse (mode <> Auto_Try 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
   291
    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
   292
    val blocking =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   293
      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
42995
e23f61546cf0 always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents: 42944
diff changeset
   294
      lookup_bool "blocking"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   295
    val provers = lookup_string "provers" |> space_explode " "
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   296
                  |> mode = Auto_Try ? single o hd
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   297
    val type_enc =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   298
      if mode = Auto_Try then
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43353
diff changeset
   299
        NONE
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   300
      else case lookup_string "type_enc" of
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43353
diff changeset
   301
        "smart" => NONE
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 52018
diff changeset
   302
      | s => (type_enc_of_string Strict s; SOME s)
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   303
    val strict = mode = Auto_Try orelse lookup_bool "strict"
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   304
    val lam_trans = lookup_option lookup_string "lam_trans"
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   305
    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   306
    val learn = lookup_bool "learn"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
   307
    val fact_filter = lookup_option lookup_string "fact_filter"
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
   308
    val max_facts = lookup_option lookup_int "max_facts"
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   309
    val fact_thresholds = lookup_real_pair "fact_thresholds"
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   310
    val max_mono_iters = lookup_option lookup_int "max_mono_iters"
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   311
    val max_new_mono_instances =
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   312
      lookup_option lookup_int "max_new_mono_instances"
51190
2654b3965c8d made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents: 51189
diff changeset
   313
    val isar_proofs = lookup_option lookup_bool "isar_proofs"
51130
76d68444cd59 renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents: 50824
diff changeset
   314
    val isar_compress = Real.max (1.0, lookup_real "isar_compress")
52556
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52366
diff changeset
   315
    val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree")
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52366
diff changeset
   316
    val merge_timeout_slack = Real.max (1.0, lookup_real "merge_timeout_slack")
52632
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   317
    val isar_try0 = lookup_bool "isar_try0"
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   318
    val isar_minimize = lookup_bool "isar_minimize"
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
   319
    val slice = mode <> Auto_Try andalso lookup_bool "slice"
45707
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   320
    val minimize =
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   321
      if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50484
diff changeset
   322
    val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
43015
21b6baec55b1 renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents: 43013
diff changeset
   323
    val preplay_timeout =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50484
diff changeset
   324
      if mode = Auto_Try then SOME Time.zeroTime
31313171deb5 thread no timeout properly
blanchet
parents: 50484
diff changeset
   325
      else lookup_time "preplay_timeout"
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51557
diff changeset
   326
    val preplay_trace = lookup_bool "preplay_trace"
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   327
    val expect = lookup_string "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   328
  in
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
   329
    {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   330
     provers = provers, type_enc = type_enc, strict = strict,
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   331
     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   332
     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
   333
     fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   334
     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
52556
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52366
diff changeset
   335
     isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
52632
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   336
     merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0,
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   337
     isar_minimize = isar_minimize, slice = slice,
52556
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52366
diff changeset
   338
     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51557
diff changeset
   339
     preplay_trace = preplay_trace, expect = expect}
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   340
  end
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   341
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   342
fun get_params mode = extract_params mode o default_raw_params
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   343
fun default_params thy = get_params Normal thy o map (apsnd single)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   344
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   345
(* Sledgehammer the given subgoal *)
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   346
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   347
val default_minimize_prover = metisN
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43034
diff changeset
   348
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   349
fun is_raw_param_relevant_for_minimize (name, _) =
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   350
  member (op =) params_for_minimize name
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   351
fun string_of_raw_param (key, values) =
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   352
  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   353
fun nice_string_of_raw_param (p as (key, ["false"])) =
50748
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   354
    (case AList.find (op =) negated_alias_params key of
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   355
       [neg] => neg
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   356
     | _ => string_of_raw_param p)
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   357
  | nice_string_of_raw_param p = string_of_raw_param p
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   358
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   359
fun minimize_command override_params i more_override_params prover_name
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   360
                     fact_names =
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   361
  let
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   362
    val params =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   363
      (override_params
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   364
       |> filter_out (AList.defined (op =) more_override_params o fst)) @
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   365
      more_override_params
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   366
      |> filter is_raw_param_relevant_for_minimize
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   367
      |> map nice_string_of_raw_param
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   368
      |> (if prover_name = default_minimize_prover then I else cons prover_name)
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   369
      |> space_implode ", "
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   370
  in
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   371
    sledgehammerN ^ " " ^ minN ^
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   372
    (if params = "" then "" else enclose " [" "]" params) ^
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   373
    " (" ^ space_implode " " fact_names ^ ")" ^
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   374
    (if i = 1 then "" else " " ^ string_of_int i)
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   375
  end
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   376
50604
4f840e2e362e crank up default timeout for MaSh ATP learning
blanchet
parents: 50557
diff changeset
   377
val default_learn_prover_timeout = 2.0
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   378
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   379
fun hammer_away override_params subcommand opt_i fact_override state =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   380
  let
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   381
    val ctxt = Proof.context_of state
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   382
    val override_params = override_params |> map (normalize_raw_param ctxt)
50052
c8d141cce517 create temp directory if not already created
blanchet
parents: 50020
diff changeset
   383
    val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   384
  in
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   385
    if subcommand = runN then
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   386
      let val i = the_default 1 opt_i in
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52982
diff changeset
   387
        run_sledgehammer (get_params Normal ctxt override_params) Normal NONE i
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   388
                         fact_override (minimize_command override_params i)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   389
                         state
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   390
        |> K ()
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   391
      end
43008
bb212c2ad238 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents: 42997
diff changeset
   392
    else if subcommand = minN then
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   393
      let
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48392
diff changeset
   394
        val ctxt = ctxt |> Config.put instantiate_inducts false
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   395
        val i = the_default 1 opt_i
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   396
        val params =
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   397
          get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   398
                                    override_params)
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   399
        val goal = prop_of (#goal (Proof.goal state))
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   400
        val facts = nearly_all_facts ctxt false fact_override Symtab.empty
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   401
                                     Termtab.empty [] [] goal
48399
4bacc8983b3d learn from SMT proofs when they can be minimized by Metis
blanchet
parents: 48397
diff changeset
   402
        fun learn prover = mash_learn_proof ctxt params prover goal facts
4bacc8983b3d learn from SMT proofs when they can be minimized by Metis
blanchet
parents: 48397
diff changeset
   403
      in run_minimize params learn i (#add fact_override) state end
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   404
    else if subcommand = messagesN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   405
      messages opt_i
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   406
    else if subcommand = supported_proversN then
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   407
      supported_provers ctxt
50719
58b0b44da54a renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
blanchet
parents: 50604
diff changeset
   408
    else if subcommand = kill_allN then
49365
8aebe857aaaa merged two commands
blanchet
parents: 48533
diff changeset
   409
      (kill_provers (); kill_learners ())
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   410
    else if subcommand = running_proversN then
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   411
      running_provers ()
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48381
diff changeset
   412
    else if subcommand = unlearnN then
df75b2d7e26a learn command in MaSh
blanchet
parents: 48381
diff changeset
   413
      mash_unlearn ctxt
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   414
    else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   415
            subcommand = relearn_isarN orelse subcommand = relearn_proverN then
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   416
      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   417
         mash_unlearn ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   418
       else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   419
         ();
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   420
       mash_learn ctxt
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   421
           (get_params Normal ctxt
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   422
                ([("timeout",
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   423
                   [string_of_real default_learn_prover_timeout]),
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   424
                  ("slice", ["false"])] @
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   425
                 override_params @
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   426
                 [("minimize", ["true"]),
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   427
                  ("preplay_timeout", ["0"])]))
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   428
           fact_override (#facts (Proof.goal state))
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   429
           (subcommand = learn_proverN orelse subcommand = relearn_proverN))
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   430
    else if subcommand = running_learnersN then
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   431
      running_learners ()
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   432
    else if subcommand = refresh_tptpN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   433
      refresh_systems_on_tptp ()
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   434
    else
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   435
      error ("Unknown subcommand: " ^ quote subcommand ^ ".")
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   436
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   437
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   438
fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
51557
4e4b56b7a3a5 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents: 51200
diff changeset
   439
  Toplevel.unknown_proof o
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   440
  Toplevel.keep (hammer_away params subcommand opt_i fact_override
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   441
                 o Toplevel.proof_of)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   442
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   443
fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   444
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   445
fun sledgehammer_params_trans params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   446
  Toplevel.theory
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   447
      (fold set_default_raw_param params
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   448
       #> tap (fn thy =>
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42237
diff changeset
   449
                  let val ctxt = Proof_Context.init_global thy in
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   450
                    writeln ("Default parameters for Sledgehammer:\n" ^
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   451
                             (case default_raw_params ctxt |> rev of
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   452
                                [] => "none"
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   453
                              | params =>
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   454
                                params |> map string_of_raw_param
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   455
                                       |> sort_strings |> cat_lines))
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   456
                  end))
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   457
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46435
diff changeset
   458
val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   459
val parse_key =
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44720
diff changeset
   460
  Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
42581
398fff2c6b8f use ! for mildly unsound and !! for very unsound encodings
blanchet
parents: 42579
diff changeset
   461
val parse_value =
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44720
diff changeset
   462
  Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46435
diff changeset
   463
val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   464
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
   465
val parse_fact_refs =
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38988
diff changeset
   466
  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   467
val parse_fact_override_chunk =
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   468
  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   469
  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   470
  || (parse_fact_refs >> only_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   471
val parse_fact_override =
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   472
  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   473
                              >> merge_fact_overrides))
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   474
                no_fact_override
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   475
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   476
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   477
  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   478
    "search for first-order proof using automatic theorem provers"
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   479
    ((Scan.optional Parse.short_ident runN -- parse_params
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   480
      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   481
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   482
  Outer_Syntax.command @{command_spec "sledgehammer_params"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   483
    "set and display the default parameters for Sledgehammer"
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   484
    (parse_params #>> sledgehammer_params_trans)
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
   485
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   486
fun try_sledgehammer auto state =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   487
  let
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   488
    val ctxt = Proof.context_of state
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   489
    val mode = if auto then Auto_Try else Try
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   490
    val i = 1
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   491
  in
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52982
diff changeset
   492
    run_sledgehammer (get_params mode ctxt []) mode NONE i no_fact_override
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   493
                     (minimize_command [] i) state
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40599
diff changeset
   494
  end
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   495
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
   496
val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   497
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52653
diff changeset
   498
val _ =
52982
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   499
  Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   500
    (case try Toplevel.proof_of st of
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   501
      SOME state =>
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   502
        let
53049
f60f92e47290 eliminated pointless subgoal argument;
wenzelm
parents: 53048
diff changeset
   503
          val [provers_arg, timeout_arg, isar_proofs_arg] = args;
52982
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   504
          val ctxt = Proof.context_of state
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52653
diff changeset
   505
52982
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   506
          val override_params =
53053
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   507
            ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   508
              [("timeout", [timeout_arg]),
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   509
               ("isar_proofs", [isar_proofs_arg]),
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   510
               ("blocking", ["true"]),
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   511
               ("minimize", ["true"]),
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   512
               ("debug", ["false"]),
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   513
               ("verbose", ["false"]),
6a3320758f0d always enable "minimize" to simplify interaction model;
wenzelm
parents: 53052
diff changeset
   514
               ("overlord", ["false"])])
52982
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   515
            |> map (normalize_raw_param ctxt)
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52982
diff changeset
   516
          val _ =
53052
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53049
diff changeset
   517
            run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
53049
f60f92e47290 eliminated pointless subgoal argument;
wenzelm
parents: 53048
diff changeset
   518
              no_fact_override (minimize_command override_params 1) state
52982
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   519
        in () end
8e78bd316a53 clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents: 52908
diff changeset
   520
    | NONE => error "Unknown proof context"));
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52653
diff changeset
   521
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   522
end;