author  wenzelm 
Sat, 17 Aug 2013 19:54:16 +0200  
changeset 53053  6a3320758f0d 
parent 53052  a0db255af8c5 
child 53055  0fe8a9972eda 
permissions  rwrr 
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  7 
signature SLEDGEHAMMER_ISAR = 
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  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  12 
val timeout : int Unsynchronized.ref 
40069  13 
val default_params : Proof.context > (string * string) list > params 
35963  14 
end; 
15 

35971  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  19 
open ATP_Util 
38028  20 
open ATP_Systems 
46320  21 
open ATP_Problem_Generate 
22 
open ATP_Proof_Reconstruct 

35971  23 
open Sledgehammer_Util 
48250
1065c307fafe
further ML structure split to permit finergrained 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  26 
open Sledgehammer_Minimize 
48381  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  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  42 

39318  43 
val _ = 
52639  44 
ProofGeneral.preference_option ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset

45 
NONE 
52639  46 
@{option auto_sledgehammer} 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset

47 
"autosledgehammer" 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset

48 
"Run Sledgehammer automatically" 
39318  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  52 
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} 
53 
fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} 

54 
fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} 

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  58 
fun merge_fact_overrides rs = 
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" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck 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" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck 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  80 
type raw_param = string * string list 
81 

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  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  88 
("strict", "false"), 
45514  89 
("lam_trans", "smart"), 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

90 
("uncurried_aliases", "smart"), 
48321  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  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 3way 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  103 
("slice", "true"), 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

104 
("minimize", "smart"), 
51879  105 
("preplay_timeout", "3"), 
106 
("preplay_trace", "false")] (* TODO: document *) 

35963  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  109 
[("prover", ("provers", [])), (* undocumented *) 
51189  110 
("dont_preplay", ("preplay_timeout", ["0"])), 
52093  111 
("dont_compress_isar", ("isar_compress", ["0"])), 
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  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  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  120 
("dont_learn", "learn"), 
49918
cf441f4a358b
renamed Isarproof 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  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  126 
("no_preplay_trace", "preplay_trace")] (* TODO: document *) 
35963  127 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

128 
val params_for_minimize = 
46301  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  137 
fun is_known_raw_param s = 
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  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  150 
SOME (name', []) => (name', value) 
151 
 SOME (param' as (name', _)) => 

152 
if value <> ["false"] then 

153 
param' 

154 
else 

155 
error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \ 

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  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  167 

48397  168 
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" 
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  175 
else if null value then 
176 
if is_prover_list ctxt name then 

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  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  181 
("lam_trans", [name]) 
182 
else if member (op =) fact_filters name then 

183 
("fact_filter", [name]) 

184 
else if is_some (Int.fromString name) then 

185 
("max_facts", [name]) 

186 
else 

187 
error ("Unknown parameter: " ^ quote name ^ ".") 

48400  188 
else 
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  191 
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are 
44785  192 
read correctly. *) 
44784  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  197 
type T = raw_param list 
198 
val empty = default_default_params > map (apsnd single) 

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  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  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  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  236 
fun default_raw_params ctxt = 
42361  237 
let val thy = Proof_Context.theory_of ctxt in 
40069  238 
Data.get thy 
239 
> fold (AList.default (op =)) 

240 
[("provers", [case !provers of 

241 
"" => default_provers_param_value ctxt 

242 
 s => s]), 

243 
("timeout", let val timeout = !timeout in 

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  246 
end)] 
247 
end 

35963  248 

43021  249 
fun extract_params mode default_params override_params = 
35963  250 
let 
251 
val raw_params = rev override_params @ rev default_params 

42776  252 
val lookup = Option.map implode_param o AList.lookup (op =) raw_params 
35963  253 
val lookup_string = the_default "" o lookup 
254 
fun general_lookup_bool option default_value name = 

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  257 
 NONE => default_value 
258 
val lookup_bool = the o general_lookup_bool false (SOME false) 

259 
fun lookup_time name = 

39318  260 
case lookup name of 
261 
SOME s => parse_time_option name s 

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  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 Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

270 
fun lookup_real name = 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

271 
case lookup name of 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

272 
NONE => 0.0 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

273 
 SOME s => case Real.fromString s of 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

274 
SOME n => n 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

275 
 NONE => error ("Parameter " ^ quote name ^ 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

276 
" must be assigned a real value.") 
40343
4521d56aef63
use floatingpoint 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 floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

279 
NONE => (0.0, 0.0) 
4521d56aef63
use floatingpoint 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 floatingpoint 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  283 
" must be assigned a pair of floatingpoint \ 
40343
4521d56aef63
use floatingpoint 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  289 
val debug = mode <> Auto_Try andalso lookup_bool "debug" 
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  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  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  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  303 
val strict = mode = Auto_Try orelse lookup_bool "strict" 
45520  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  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  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 3way 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  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  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  324 
if mode = Auto_Try then SOME Time.zeroTime 
325 
else lookup_time "preplay_timeout" 

51879  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  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  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  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 Isarproof 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  339 
preplay_trace = preplay_trace, expect = expect} 
35963  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  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  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  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  354 
(case AList.find (op =) negated_alias_params key of 
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  359 
fun minimize_command override_params i more_override_params prover_name 
360 
fact_names = 

43057  361 
let 
362 
val params = 

45520  363 
(override_params 
364 
> filter_out (AList.defined (op =) more_override_params o fst)) @ 

365 
more_override_params 

43057  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  368 
> (if prover_name = default_minimize_prover then I else cons prover_name) 
369 
> space_implode ", " 

370 
in 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

371 
sledgehammerN ^ " " ^ minN ^ 
43057  372 
(if params = "" then "" else enclose " [" "]" params) ^ 
373 
" (" ^ space_implode " " fact_names ^ ")" ^ 

374 
(if i = 1 then "" else " " ^ string_of_int i) 

375 
end 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

376 

50604  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  379 
fun hammer_away override_params subcommand opt_i fact_override state = 
35963  380 
let 
40069  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  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  388 
fact_override (minimize_command override_params i) 
39318  389 
state 
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  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  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  412 
else if subcommand = unlearnN then 
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  437 

48292  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  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  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  444 

35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

445 
fun sledgehammer_params_trans params = 
35963  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  448 
#> tap (fn thy => 
42361  449 
let val ctxt = Proof_Context.init_global thy in 
40069  450 
writeln ("Default parameters for Sledgehammer:\n" ^ 
451 
(case default_raw_params ctxt > rev of 

452 
[] => "none" 

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  456 
end)) 
35963  457 

46949  458 
val parse_query_bang = @{keyword "?"}  @{keyword "!"}  @{keyword "!!"} 
42776  459 
val parse_key = 
44768  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  462 
Scan.repeat1 (Parse.xname  Parse.float_number  parse_query_bang) 
46949  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  466 
Scan.repeat1 (Scan.unless (Parse.name  Args.colon) Parse_Spec.xthm) 
48293  467 
val parse_fact_override_chunk = 
48292  468 
(Args.add  Args.colon  parse_fact_refs >> add_fact_override) 
469 
 (Args.del  Args.colon  parse_fact_refs >> del_fact_override) 

470 
 (parse_fact_refs >> only_fact_override) 

471 
val parse_fact_override = 

48293  472 
Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk 
48292  473 
>> merge_fact_overrides)) 
474 
no_fact_override 

35963  475 

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 firstorder 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  480 
 parse_fact_override  Scan.option Parse.nat) #>> sledgehammer_trans) 
35963  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  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  494 
end 
39318  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  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 hardwired parallel policy;
wenzelm
parents:
52908
diff
changeset

499 
Query_Operation.register sledgehammerN (fn {state = st, args, output_result} => 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52908
diff
changeset

500 
(case try Toplevel.proof_of st of 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52908
diff
changeset

501 
SOME state => 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52908
diff
changeset

502 
let 
53049  503 
val [provers_arg, timeout_arg, isar_proofs_arg] = args; 
52982
8e78bd316a53
clarified Query_Operation.register: avoid hardwired 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 hardwired 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 hardwired 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  oldstyle inline 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  518 
no_fact_override (minimize_command override_params 1) state 
52982
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52908
diff
changeset

519 
in () end 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired 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; 