author | blanchet |
Tue, 24 Jun 2014 08:19:55 +0200 | |
changeset 57290 | bc06471cb7b7 |
parent 57274 | 0acfdb151e52 |
child 57433 | 7e55bd4f9b0e |
permissions | -rw-r--r-- |
55198 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.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 |
|
55198 | 7 |
signature SLEDGEHAMMER_COMMANDS = |
35963 | 8 |
sig |
55201 | 9 |
type params = Sledgehammer_Prover.params |
35963 | 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 |
55205 | 12 |
val default_params : theory -> (string * string) list -> params |
35963 | 13 |
end; |
14 |
||
55198 | 15 |
structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset
|
16 |
struct |
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset
|
17 |
|
44784 | 18 |
open ATP_Util |
38028 | 19 |
open ATP_Systems |
46320 | 20 |
open ATP_Problem_Generate |
57154 | 21 |
open ATP_Proof |
46320 | 22 |
open ATP_Proof_Reconstruct |
35971 | 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 |
55201 | 25 |
open Sledgehammer_Prover |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
26 |
open Sledgehammer_Prover_Minimize |
48381 | 27 |
open Sledgehammer_MaSh |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
28 |
open Sledgehammer |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset
|
29 |
|
48433 | 30 |
(* val cvc3N = "cvc3" *) |
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57208
diff
changeset
|
31 |
val z3N = "z3" |
48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48400
diff
changeset
|
32 |
|
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
33 |
val runN = "run" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
34 |
val minN = "min" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
35 |
val messagesN = "messages" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
val refresh_tptpN = "refresh_tptp" |
48301 | 41 |
|
39318 | 42 |
val _ = |
52639 | 43 |
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
|
44 |
NONE |
56467 | 45 |
@{system_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
|
46 |
"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
|
47 |
"Run Sledgehammer automatically" |
39318 | 48 |
|
36394
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset
|
49 |
(** Sledgehammer commands **) |
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset
|
50 |
|
48292 | 51 |
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} |
52 |
fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} |
|
53 |
fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} |
|
54 |
fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = |
|
57273
01b68f625550
automatically learn MaSh facts also in 'blocking' mode
blanchet
parents:
57245
diff
changeset
|
55 |
{add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} |
01b68f625550
automatically learn MaSh facts also in 'blocking' mode
blanchet
parents:
57245
diff
changeset
|
56 |
fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) |
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
57 |
|
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset
|
58 |
(*** parameters ***) |
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset
|
59 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
60 |
val provers = Unsynchronized.ref "" |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset
|
61 |
|
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset
|
62 |
val _ = |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset
|
63 |
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
|
64 |
NONE |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset
|
65 |
provers |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset
|
66 |
"Sledgehammer: Provers" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset
|
67 |
"Default automatic provers (separated by whitespace)" |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset
|
68 |
|
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset
|
69 |
val _ = |
53057
e18a028b345c
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
wenzelm
parents:
53055
diff
changeset
|
70 |
ProofGeneral.preference_option 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
|
71 |
NONE |
56467 | 72 |
@{system_option sledgehammer_timeout} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset
|
73 |
"Sledgehammer: Time Limit" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset
|
74 |
"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
|
75 |
|
35963 | 76 |
type raw_param = string * string list |
77 |
||
78 |
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
|
79 |
[("debug", "false"), |
35963 | 80 |
("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
|
81 |
("overlord", "false"), |
53800 | 82 |
("spy", "false"), |
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset
|
83 |
("blocking", "false"), |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset
|
84 |
("type_enc", "smart"), |
46301 | 85 |
("strict", "false"), |
45514 | 86 |
("lam_trans", "smart"), |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset
|
87 |
("uncurried_aliases", "smart"), |
48321 | 88 |
("learn", "true"), |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset
|
89 |
("fact_filter", "smart"), |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset
|
90 |
("max_facts", "smart"), |
48293 | 91 |
("fact_thresholds", "0.45 0.85"), |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset
|
92 |
("max_mono_iters", "smart"), |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset
|
93 |
("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
|
94 |
("isar_proofs", "smart"), |
57245 | 95 |
("compress", "10"), |
96 |
("try0", "true"), |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
97 |
("smt_proofs", "smart"), |
45706 | 98 |
("slice", "true"), |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
99 |
("minimize", "smart"), |
55277
93c7fcfbe6f5
reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
blanchet
parents:
55205
diff
changeset
|
100 |
("preplay_timeout", "2")] |
35963 | 101 |
|
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset
|
102 |
val alias_params = |
51138 | 103 |
[("prover", ("provers", [])), (* undocumented *) |
51189 | 104 |
("dont_preplay", ("preplay_timeout", ["0"])), |
57245 | 105 |
("dont_compress", ("compress", ["0"])), |
52093 | 106 |
("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
|
107 |
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
|
108 |
[("no_debug", "debug"), |
35963 | 109 |
("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
|
110 |
("no_overlord", "overlord"), |
53800 | 111 |
("dont_spy", "spy"), |
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset
|
112 |
("non_blocking", "blocking"), |
46301 | 113 |
("non_strict", "strict"), |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset
|
114 |
("no_uncurried_aliases", "uncurried_aliases"), |
48321 | 115 |
("dont_learn", "learn"), |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset
|
116 |
("no_isar_proofs", "isar_proofs"), |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
117 |
("dont_slice", "slice"), |
51879 | 118 |
("dont_minimize", "minimize"), |
57245 | 119 |
("dont_try0", "try0"), |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
120 |
("no_smt_proofs", "smt_proofs")] |
35963 | 121 |
|
53758 | 122 |
val params_not_for_minimize = |
56847 | 123 |
["provers", "blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"]; |
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset
|
124 |
|
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43353
diff
changeset
|
125 |
val property_dependent_params = ["provers", "timeout"] |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset
|
126 |
|
35963 | 127 |
fun is_known_raw_param s = |
128 |
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
|
129 |
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
|
130 |
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
|
131 |
member (op =) property_dependent_params s orelse s = "expect" |
35963 | 132 |
|
41258
73401632a80c
convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset
|
133 |
fun is_prover_list ctxt s = |
55286 | 134 |
(case space_explode " " s of |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset
|
135 |
ss as _ :: _ => forall (is_prover_supported ctxt) ss |
55286 | 136 |
| _ => false) |
41258
73401632a80c
convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset
|
137 |
|
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset
|
138 |
fun unalias_raw_param (name, value) = |
55286 | 139 |
(case AList.lookup (op =) alias_params name of |
47037 | 140 |
SOME (name', []) => (name', value) |
141 |
| SOME (param' as (name', _)) => |
|
142 |
if value <> ["false"] then |
|
143 |
param' |
|
144 |
else |
|
145 |
error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \ |
|
146 |
\(cf. " ^ quote name' ^ ").") |
|
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset
|
147 |
| NONE => |
55286 | 148 |
(case AList.lookup (op =) negated_alias_params name of |
149 |
SOME name' => (name', |
|
150 |
(case value of |
|
151 |
["false"] => ["true"] |
|
152 |
| ["true"] => ["false"] |
|
153 |
| [] => ["false"] |
|
154 |
| _ => value)) |
|
155 |
| NONE => (name, value))) |
|
35963 | 156 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
52018
diff
changeset
|
157 |
val any_type_enc = type_enc_of_string Strict "erased" |
45514 | 158 |
|
48397 | 159 |
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" |
160 |
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
|
161 |
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
|
162 |
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
|
163 |
#> (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
|
164 |
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
|
165 |
(name, value) |
48533 | 166 |
else if null value then |
167 |
if is_prover_list ctxt name then |
|
168 |
("provers", [name]) |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
52018
diff
changeset
|
169 |
else if can (type_enc_of_string Strict) name then |
48533 | 170 |
("type_enc", [name]) |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
52018
diff
changeset
|
171 |
else if can (trans_lams_of_string ctxt any_type_enc) name then |
48533 | 172 |
("lam_trans", [name]) |
173 |
else if member (op =) fact_filters name then |
|
174 |
("fact_filter", [name]) |
|
175 |
else if is_some (Int.fromString name) then |
|
176 |
("max_facts", [name]) |
|
177 |
else |
|
178 |
error ("Unknown parameter: " ^ quote name ^ ".") |
|
48400 | 179 |
else |
180 |
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
|
181 |
|
46435 | 182 |
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are |
44785 | 183 |
read correctly. *) |
44784 | 184 |
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
|
185 |
|
54059 | 186 |
(* FIXME: use "Generic_Data" *) |
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41258
diff
changeset
|
187 |
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
|
188 |
( |
35963 | 189 |
type T = raw_param list |
54546
8b403a7a8c44
fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet
parents:
54503
diff
changeset
|
190 |
val empty = default_default_params |> map (apsnd single) |
35963 | 191 |
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
|
192 |
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
|
193 |
) |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset
|
194 |
|
55475
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
195 |
fun remotify_prover_if_supported_and_not_already_remote ctxt name = |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
196 |
if String.isPrefix remote_prefix name then |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
197 |
SOME name |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
198 |
else |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
199 |
let val remote_name = remote_prefix ^ name in |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
200 |
if is_prover_supported ctxt remote_name then SOME remote_name else NONE |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
201 |
end |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
202 |
|
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
203 |
fun remotify_prover_if_not_installed ctxt name = |
57237
bc51864c2ac4
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents:
57209
diff
changeset
|
204 |
if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name |
bc51864c2ac4
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents:
57209
diff
changeset
|
205 |
else remotify_prover_if_supported_and_not_already_remote ctxt name |
55475
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
206 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
207 |
(* 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
|
208 |
timeout, it makes sense to put E first. *) |
55475
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
209 |
fun default_provers_param_value mode ctxt = |
57237
bc51864c2ac4
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents:
57209
diff
changeset
|
210 |
[eN, spassN, z3N, e_sineN, vampireN] |
55475
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
211 |
|> map_filter (remotify_prover_if_not_installed ctxt) |
54059 | 212 |
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |
213 |
|> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0)) |
|
42776 | 214 |
|> implode_param |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
215 |
|
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
|
216 |
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
|
217 |
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
|
218 |
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
|
219 |
end |
54059 | 220 |
|
55205 | 221 |
fun default_raw_params mode thy = |
55475
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
222 |
let val ctxt = Proof_Context.init_global thy in |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
223 |
Data.get thy |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
224 |
|> fold (AList.default (op =)) |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
225 |
[("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]), |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
226 |
("timeout", |
56467 | 227 |
let val timeout = Options.default_int @{system_option sledgehammer_timeout} in |
55475
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
228 |
[if timeout <= 0 then "none" else string_of_int timeout] |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
229 |
end)] |
b8ebbcc5e49a
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset
|
230 |
end |
35963 | 231 |
|
43021 | 232 |
fun extract_params mode default_params override_params = |
35963 | 233 |
let |
234 |
val raw_params = rev override_params @ rev default_params |
|
42776 | 235 |
val lookup = Option.map implode_param o AList.lookup (op =) raw_params |
35963 | 236 |
val lookup_string = the_default "" o lookup |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
237 |
|
35963 | 238 |
fun general_lookup_bool option default_value name = |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
239 |
(case lookup name of |
35970
3d41a2a490f0
revert debugging output that shouldn't have been submitted in the first place
blanchet
parents:
35966
diff
changeset
|
240 |
SOME s => parse_bool_option option name s |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
241 |
| NONE => default_value) |
35963 | 242 |
val lookup_bool = the o general_lookup_bool false (SOME false) |
243 |
fun lookup_time name = |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
244 |
(case lookup name of |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
245 |
SOME s => parse_time name s |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
246 |
| NONE => Time.zeroTime) |
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset
|
247 |
fun lookup_int name = |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
248 |
(case lookup name of |
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset
|
249 |
NONE => 0 |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
250 |
| SOME s => |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
251 |
(case Int.fromString s of |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
252 |
SOME n => n |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
253 |
| NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value."))) |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset
|
254 |
fun lookup_real name = |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
255 |
(case lookup name of |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset
|
256 |
NONE => 0.0 |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
257 |
| SOME s => |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
258 |
(case Real.fromString s of |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
259 |
SOME n => n |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
260 |
| NONE => error ("Parameter " ^ quote name ^ " 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
|
261 |
fun lookup_real_pair name = |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
262 |
(case lookup name of |
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
263 |
NONE => (0.0, 0.0) |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
264 |
| SOME s => |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
265 |
(case s |> space_explode " " |> map Real.fromString of |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
266 |
[SOME r1, SOME r2] => (r1, r2) |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
267 |
| _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
268 |
\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
|
269 |
fun lookup_option lookup' name = |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
270 |
(case lookup name of |
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38282
diff
changeset
|
271 |
SOME "smart" => NONE |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
272 |
| _ => SOME (lookup' name)) |
43021 | 273 |
val debug = mode <> Auto_Try andalso lookup_bool "debug" |
274 |
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
|
275 |
val overlord = lookup_bool "overlord" |
54546
8b403a7a8c44
fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet
parents:
54503
diff
changeset
|
276 |
val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" |
42995
e23f61546cf0
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents:
42944
diff
changeset
|
277 |
val blocking = |
56982 | 278 |
Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking" |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
279 |
val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset
|
280 |
val type_enc = |
43021 | 281 |
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
|
282 |
NONE |
55286 | 283 |
else |
284 |
(case lookup_string "type_enc" of |
|
285 |
"smart" => NONE |
|
286 |
| s => (type_enc_of_string Strict s; SOME s)) |
|
46301 | 287 |
val strict = mode = Auto_Try orelse lookup_bool "strict" |
45520 | 288 |
val lam_trans = lookup_option lookup_string "lam_trans" |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset
|
289 |
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" |
48321 | 290 |
val learn = lookup_bool "learn" |
54113
df080dfefddc
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents:
54059
diff
changeset
|
291 |
val fact_filter = |
df080dfefddc
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents:
54059
diff
changeset
|
292 |
lookup_option lookup_string "fact_filter" |
df080dfefddc
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents:
54059
diff
changeset
|
293 |
|> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset
|
294 |
val max_facts = lookup_option lookup_int "max_facts" |
48293 | 295 |
val fact_thresholds = lookup_real_pair "fact_thresholds" |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset
|
296 |
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
|
297 |
val max_new_mono_instances = |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset
|
298 |
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
|
299 |
val isar_proofs = lookup_option lookup_bool "isar_proofs" |
57245 | 300 |
val compress = Real.max (1.0, lookup_real "compress") |
301 |
val try0 = lookup_bool "try0" |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
302 |
val smt_proofs = lookup_option lookup_bool "smt_proofs" |
45706 | 303 |
val slice = mode <> Auto_Try andalso lookup_bool "slice" |
54113
df080dfefddc
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents:
54059
diff
changeset
|
304 |
val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
305 |
val timeout = lookup_time "timeout" |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
306 |
val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout" |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
307 |
val expect = lookup_string "expect" |
35963 | 308 |
in |
53800 | 309 |
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, |
310 |
provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
|
311 |
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, |
|
312 |
max_facts = max_facts, 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
|
313 |
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
57245 | 314 |
compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, |
315 |
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} |
|
35963 | 316 |
end |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset
|
317 |
|
54059 | 318 |
fun get_params mode = extract_params mode o default_raw_params mode |
43021 | 319 |
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
|
320 |
|
36373
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36371
diff
changeset
|
321 |
(* Sledgehammer the given subgoal *) |
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36371
diff
changeset
|
322 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
323 |
val default_minimize_prover = metisN |
43051 | 324 |
|
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
325 |
fun is_raw_param_relevant_for_minimize (name, _) = not (member (op =) params_not_for_minimize name) |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
326 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
327 |
fun string_of_raw_param (key, values) = |
42776 | 328 |
key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
329 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
330 |
fun nice_string_of_raw_param (p as (key, ["false"])) = |
50748 | 331 |
(case AList.find (op =) negated_alias_params key of |
332 |
[neg] => neg |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
333 |
| _ => string_of_raw_param p) |
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
334 |
| 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
|
335 |
|
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
336 |
fun minimize_command override_params i more_override_params prover_name fact_names = |
43057 | 337 |
let |
338 |
val params = |
|
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
339 |
(override_params |> filter_out (AList.defined (op =) more_override_params o fst)) @ |
45520 | 340 |
more_override_params |
43057 | 341 |
|> filter is_raw_param_relevant_for_minimize |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
342 |
|> map nice_string_of_raw_param |
43057 | 343 |
|> (if prover_name = default_minimize_prover then I else cons prover_name) |
344 |
|> space_implode ", " |
|
345 |
in |
|
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
346 |
sledgehammerN ^ " " ^ minN ^ (if params = "" then "" else enclose " [" "]" params) ^ |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
347 |
" (" ^ space_implode " " fact_names ^ ")" ^ (if i = 1 then "" else " " ^ string_of_int i) |
43057 | 348 |
end |
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset
|
349 |
|
50604 | 350 |
val default_learn_prover_timeout = 2.0 |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset
|
351 |
|
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
352 |
fun hammer_away override_params subcommand opt_i fact_override state = |
35963 | 353 |
let |
55205 | 354 |
val thy = Proof.theory_of state |
40069 | 355 |
val ctxt = Proof.context_of state |
55205 | 356 |
|
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
|
357 |
val override_params = override_params |> map (normalize_raw_param ctxt) |
50052 | 358 |
val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP")) |
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
359 |
in |
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
360 |
if subcommand = runN then |
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset
|
361 |
let val i = the_default 1 opt_i in |
55205 | 362 |
run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override |
363 |
(minimize_command override_params i) state |
|
39318 | 364 |
|> K () |
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset
|
365 |
end |
43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
42997
diff
changeset
|
366 |
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
|
367 |
let |
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset
|
368 |
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
|
369 |
val i = the_default 1 opt_i |
48400 | 370 |
val params = |
55205 | 371 |
get_params Minimize thy (("provers", [default_minimize_prover]) :: override_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
|
372 |
val goal = prop_of (#goal (Proof.goal state)) |
57274
0acfdb151e52
more generous formula -- there are lots of duplicates out there
blanchet
parents:
57273
diff
changeset
|
373 |
val facts = nearly_all_facts ctxt false fact_override Symtab.empty Termtab.empty [] [] goal |
54503 | 374 |
val learn = mash_learn_proof ctxt params goal facts |
48399
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48397
diff
changeset
|
375 |
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
|
376 |
else if subcommand = messagesN then |
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
377 |
messages opt_i |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset
|
378 |
else if subcommand = supported_proversN then |
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset
|
379 |
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
|
380 |
else if subcommand = kill_allN then |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
381 |
(kill_provers (); |
55205 | 382 |
kill_learners ctxt (get_params Normal thy override_params)) |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset
|
383 |
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
|
384 |
running_provers () |
48383 | 385 |
else if subcommand = unlearnN then |
55205 | 386 |
mash_unlearn ctxt (get_params Normal thy override_params) |
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
|
387 |
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
|
388 |
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
|
389 |
(if subcommand = relearn_isarN orelse subcommand = relearn_proverN then |
55205 | 390 |
mash_unlearn ctxt (get_params Normal thy override_params) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset
|
391 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset
|
392 |
(); |
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
|
393 |
mash_learn ctxt |
54129 | 394 |
(* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) |
55205 | 395 |
(get_params Normal thy |
396 |
([("timeout", [string_of_real default_learn_prover_timeout]), |
|
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
|
397 |
("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
|
398 |
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
|
399 |
[("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
|
400 |
("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
|
401 |
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
|
402 |
(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
|
403 |
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
|
404 |
running_learners () |
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
405 |
else if subcommand = refresh_tptpN then |
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
406 |
refresh_systems_on_tptp () |
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
407 |
else |
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
408 |
error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
409 |
end |
35963 | 410 |
|
48292 | 411 |
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
|
412 |
Toplevel.unknown_proof o |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
413 |
Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) |
35963 | 414 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset
|
415 |
fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value |
35963 | 416 |
|
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset
|
417 |
fun sledgehammer_params_trans params = |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
418 |
Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
419 |
writeln ("Default parameters for Sledgehammer:\n" ^ |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
420 |
(case rev (default_raw_params Normal thy) of |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
421 |
[] => "none" |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
422 |
| params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))) |
35963 | 423 |
|
46949 | 424 |
val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"} |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
425 |
val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
426 |
val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang) |
46949 | 427 |
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
|
428 |
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
|
429 |
val parse_fact_refs = |
38996 | 430 |
Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm) |
48293 | 431 |
val parse_fact_override_chunk = |
48292 | 432 |
(Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) |
433 |
|| (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) |
|
434 |
|| (parse_fact_refs >> only_fact_override) |
|
435 |
val parse_fact_override = |
|
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57274
diff
changeset
|
436 |
Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) |
48292 | 437 |
no_fact_override |
35963 | 438 |
|
439 |
val _ = |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
440 |
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
|
441 |
"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
|
442 |
((Scan.optional Parse.short_ident runN -- parse_params |
48292 | 443 |
-- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans) |
35963 | 444 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
445 |
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
|
446 |
"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
|
447 |
(parse_params #>> sledgehammer_params_trans) |
36394
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset
|
448 |
|
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
449 |
fun try_sledgehammer auto state = |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
450 |
let |
55205 | 451 |
val thy = Proof.theory_of state |
43021 | 452 |
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
|
453 |
val i = 1 |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
454 |
in |
55205 | 455 |
run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (minimize_command [] i) |
456 |
state |
|
40931 | 457 |
end |
39318 | 458 |
|
56467 | 459 |
val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer)) |
39318 | 460 |
|
52908
3461985dcbc3
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
52653
diff
changeset
|
461 |
val _ = |
52982
8e78bd316a53
clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents:
52908
diff
changeset
|
462 |
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
|
463 |
(case try Toplevel.proof_of st of |
8e78bd316a53
clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents:
52908
diff
changeset
|
464 |
SOME state => |
8e78bd316a53
clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents:
52908
diff
changeset
|
465 |
let |
55205 | 466 |
val thy = Proof.theory_of state |
52982
8e78bd316a53
clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents:
52908
diff
changeset
|
467 |
val ctxt = Proof.context_of state |
55205 | 468 |
val [provers_arg, isar_proofs_arg] = args |
52908
3461985dcbc3
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
52653
diff
changeset
|
469 |
|
52982
8e78bd316a53
clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents:
52908
diff
changeset
|
470 |
val override_params = |
53053
6a3320758f0d
always enable "minimize" to simplify interaction model;
wenzelm
parents:
53052
diff
changeset
|
471 |
((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ |
53057
e18a028b345c
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
wenzelm
parents:
53055
diff
changeset
|
472 |
[("isar_proofs", [isar_proofs_arg]), |
53053
6a3320758f0d
always enable "minimize" to simplify interaction model;
wenzelm
parents:
53052
diff
changeset
|
473 |
("blocking", ["true"]), |
6a3320758f0d
always enable "minimize" to simplify interaction model;
wenzelm
parents:
53052
diff
changeset
|
474 |
("minimize", ["true"]), |
6a3320758f0d
always enable "minimize" to simplify interaction model;
wenzelm
parents:
53052
diff
changeset
|
475 |
("debug", ["false"]), |
6a3320758f0d
always enable "minimize" to simplify interaction model;
wenzelm
parents:
53052
diff
changeset
|
476 |
("verbose", ["false"]), |
6a3320758f0d
always enable "minimize" to simplify interaction model;
wenzelm
parents:
53052
diff
changeset
|
477 |
("overlord", ["false"])]) |
52982
8e78bd316a53
clarified Query_Operation.register: avoid hard-wired parallel policy;
wenzelm
parents:
52908
diff
changeset
|
478 |
|> map (normalize_raw_param ctxt) |
55205 | 479 |
|
480 |
val _ = run_sledgehammer (get_params Normal thy override_params) Normal |
|
481 |
(SOME output_result) 1 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
|
482 |
in () end |
53055
0fe8a9972eda
some protocol to determine provers according to ML;
wenzelm
parents:
53053
diff
changeset
|
483 |
| NONE => error "Unknown proof context")) |
0fe8a9972eda
some protocol to determine provers according to ML;
wenzelm
parents:
53053
diff
changeset
|
484 |
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset
|
485 |
end; |