author  blanchet 
Fri, 20 Jul 2012 22:19:46 +0200  
changeset 48397  9fe826095a02 
parent 48395  85a7fb65507a 
child 48399  4bacc8983b3d 
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 

39318  11 
val auto : bool Unsynchronized.ref 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

12 
val provers : string Unsynchronized.ref 
39318  13 
val timeout : int Unsynchronized.ref 
40069  14 
val default_params : Proof.context > (string * string) list > params 
39318  15 
val setup : theory > theory 
35963  16 
end; 
17 

35971  18 
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

19 
struct 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

20 

44784  21 
open ATP_Util 
38028  22 
open ATP_Systems 
46320  23 
open ATP_Problem_Generate 
24 
open ATP_Proof_Reconstruct 

35971  25 
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

26 
open Sledgehammer_Fact 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40941
diff
changeset

27 
open Sledgehammer_Provers 
38988  28 
open Sledgehammer_Minimize 
48381  29 
open Sledgehammer_MaSh 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40941
diff
changeset

30 
open Sledgehammer_Run 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

31 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

32 
val runN = "run" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

33 
val minN = "min" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

34 
val messagesN = "messages" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

35 
val supported_proversN = "supported_provers" 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

36 
val kill_proversN = "kill_provers" 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

37 
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

38 
val kill_learnersN = "kill_learners" 
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 auto = Unsynchronized.ref false 
43 

44 
val _ = 

45 
ProofGeneralPgip.add_preference Preferences.category_tracing 

46 
(Preferences.bool_pref auto "autosledgehammer" 

39327  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) = 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

55 
{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

56 
only = #only r1 andalso #only r2} 
48292  57 
fun merge_fact_overrides rs = 
58 
fold merge_fact_override_pairwise rs (only_fact_override []) 

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

59 

36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

60 
(*** parameters ***) 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

61 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

62 
val provers = Unsynchronized.ref "" 
39335
87a9ff4d5817
use 30 s instead of 60 s as the default Sledgehammer timeout;
blanchet
parents:
39327
diff
changeset

63 
val timeout = Unsynchronized.ref 30 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

64 

8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

65 
val _ = 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

66 
ProofGeneralPgip.add_preference Preferences.category_proof 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

67 
(Preferences.string_pref provers 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

68 
"Sledgehammer: Provers" 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

69 
"Default automatic provers (separated by whitespace)") 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

70 

8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

71 
val _ = 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

72 
ProofGeneralPgip.add_preference Preferences.category_proof 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

73 
(Preferences.int_pref timeout 
36373
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36371
diff
changeset

74 
"Sledgehammer: Time Limit" 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

75 
"ATPs will be interrupted after this time (in seconds)") 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

76 

35963  77 
type raw_param = string * string list 
78 

79 
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

80 
[("debug", "false"), 
35963  81 
("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

82 
("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

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"), 
35963  94 
("isar_proof", "false"), 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

95 
("isar_shrink_factor", "1"), 
45706  96 
("slice", "true"), 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

97 
("minimize", "smart"), 
46297
0a4907baf9db
lower timeout for preplay, now that we have more preplay methods
blanchet
parents:
45707
diff
changeset

98 
("preplay_timeout", "3")] 
35963  99 

36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

100 
val alias_params = 
48293  101 
[("prover", ("provers", [])), (* legacy *) 
102 
("max_relevant", ("max_facts", [])), (* legacy *) 

47037  103 
("dont_preplay", ("preplay_timeout", ["0"]))] 
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

104 
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

105 
[("no_debug", "debug"), 
35963  106 
("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

107 
("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

108 
("non_blocking", "blocking"), 
46301  109 
("non_strict", "strict"), 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

110 
("no_uncurried_aliases", "uncurried_aliases"), 
48321  111 
("dont_learn", "learn"), 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

112 
("no_isar_proof", "isar_proof"), 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

113 
("dont_slice", "slice"), 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

114 
("dont_minimize", "minimize")] 
35963  115 

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

116 
val params_for_minimize = 
46301  117 
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans", 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

118 
"uncurried_aliases", "max_mono_iters", "max_new_mono_instances", 
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

119 
"isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"] 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

120 

43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43353
diff
changeset

121 
val property_dependent_params = ["provers", "timeout"] 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

122 

35963  123 
fun is_known_raw_param s = 
124 
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

125 
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

126 
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

127 
member (op =) property_dependent_params s orelse s = "expect" 
35963  128 

41258
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

129 
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

130 
case space_explode " " s of 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

131 
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

132 
 _ => false 
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

133 

36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

134 
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

135 
case AList.lookup (op =) alias_params name of 
47037  136 
SOME (name', []) => (name', value) 
137 
 SOME (param' as (name', _)) => 

138 
if value <> ["false"] then 

139 
param' 

140 
else 

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

142 
\(cf. " ^ quote name' ^ ").") 

36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

143 
 NONE => 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

144 
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

145 
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

146 
["false"] => ["true"] 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

147 
 ["true"] => ["false"] 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

148 
 [] => ["false"] 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

149 
 _ => value) 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

150 
 NONE => (name, value) 
35963  151 

46301  152 
val any_type_enc = type_enc_from_string Strict "erased" 
45514  153 

48397  154 
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" 
155 
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

156 
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

157 
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

158 
#> (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

159 
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

160 
(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

161 
else if is_prover_list ctxt name andalso null value 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

162 
("provers", [name]) 
46301  163 
else if can (type_enc_from_string Strict) name andalso null value then 
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

164 
("type_enc", [name]) 
45514  165 
else if can (trans_lams_from_string ctxt any_type_enc) name andalso 
166 
null value then 

167 
("lam_trans", [name]) 

48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

168 
else if member (op =) fact_filters name then 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

169 
("fact_filter", [name]) 
48397  170 
else case Int.fromString name of 
171 
SOME n => ("max_facts", [name]) 

172 
 NONE => 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

173 

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 

46435  175 
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are 
44785  176 
read correctly. *) 
44784  177 
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

178 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41258
diff
changeset

179 
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

180 
( 
35963  181 
type T = raw_param list 
182 
val empty = default_default_params > map (apsnd single) 

183 
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

184 
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

185 
) 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

186 

41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

187 
fun remotify_prover_if_supported_and_not_already_remote ctxt name = 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

188 
if String.isPrefix remote_prefix name then 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

189 
SOME name 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

190 
else 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

191 
let val remote_name = remote_prefix ^ name in 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

192 
if is_prover_supported ctxt remote_name then SOME remote_name else NONE 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

193 
end 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

194 

27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

195 
fun remotify_prover_if_not_installed ctxt name = 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

196 
if is_prover_supported ctxt name andalso is_prover_installed ctxt name then 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40931
diff
changeset

197 
SOME name 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40931
diff
changeset

198 
else 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

199 
remotify_prover_if_supported_and_not_already_remote ctxt name 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

200 

43009
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

201 
fun avoid_too_many_threads _ _ [] = [] 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

202 
 avoid_too_many_threads _ (0, 0) _ = [] 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

203 
 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

204 
provers 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

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

206 
> take max_remote 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

207 
 avoid_too_many_threads _ (max_local, 0) provers = 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

208 
provers 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

209 
> filter_out (String.isPrefix remote_prefix) 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

210 
> take max_local 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

211 
 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

212 
let 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

213 
val max_local_and_remote = 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

214 
max_local_and_remote 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

215 
> (if String.isPrefix remote_prefix prover then apsnd else apfst) 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

216 
(Integer.add ~1) 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

217 
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

218 

43009
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

219 
val max_default_remote_threads = 4 
42688
097a61baeca9
smoother handling of ! and ? in type system names
blanchet
parents:
42613
diff
changeset

220 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

221 
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

222 
timeout, it makes sense to put SPASS first. *) 
40069  223 
fun default_provers_param_value ctxt = 
47642
9a9218111085
swap out Satallax, pull in ESInE again  it's not clear yet how useful Satallax is after proof reconstruction, whereas ESInE performed surprisingly well on latest evaluations
blanchet
parents:
47074
diff
changeset

224 
[spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, 
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47055
diff
changeset

225 
waldmeisterN] 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40931
diff
changeset

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

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

228 
max_default_remote_threads) 
42776  229 
> implode_param 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

230 

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

231 
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

232 
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

233 
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

234 
end 
40069  235 
fun default_raw_params ctxt = 
42361  236 
let val thy = Proof_Context.theory_of ctxt in 
40069  237 
Data.get thy 
238 
> fold (AList.default (op =)) 

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

240 
"" => default_provers_param_value ctxt 

241 
 s => s]), 

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

243 
[if timeout <= 0 then "none" 

40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40181
diff
changeset

244 
else string_of_int timeout] 
40069  245 
end)] 
246 
end 

35963  247 

48383  248 
val the_timeout = the_default infinite_timeout 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

249 

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

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

256 
case lookup name of 

35970
3d41a2a490f0
revert debugging output that shouldn't have been submitted in the first place
blanchet
parents:
35966
diff
changeset

257 
SOME s => parse_bool_option option name s 
35963  258 
 NONE => default_value 
259 
val lookup_bool = the o general_lookup_bool false (SOME false) 

260 
fun lookup_time name = 

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

263 
 NONE => NONE 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

264 
fun lookup_int name = 
35963  265 
case lookup name of 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

266 
NONE => 0 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

267 
 SOME s => case Int.fromString s of 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

268 
SOME n => n 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

269 
 NONE => error ("Parameter " ^ quote name ^ 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

270 
" must be assigned an integer value.") 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

271 
fun lookup_real_pair name = 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

272 
case lookup name of 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

273 
NONE => (0.0, 0.0) 
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

274 
 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

275 
[SOME r1, SOME r2] => (r1, r2) 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

276 
 _ => error ("Parameter " ^ quote name ^ 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

277 
"must be assigned a pair of floatingpoint \ 
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

278 
\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

279 
fun lookup_option lookup' name = 
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38282
diff
changeset

280 
case lookup name of 
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38282
diff
changeset

281 
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

282 
 _ => SOME (lookup' name) 
43021  283 
val debug = mode <> Auto_Try andalso lookup_bool "debug" 
284 
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

285 
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

286 
val blocking = 
43021  287 
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

288 
lookup_bool "blocking" 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

289 
val provers = lookup_string "provers" > space_explode " " 
43021  290 
> mode = Auto_Try ? single o hd 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

291 
val type_enc = 
43021  292 
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

293 
NONE 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

294 
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

295 
"smart" => NONE 
46301  296 
 s => (type_enc_from_string Strict s; SOME s) 
297 
val strict = mode = Auto_Try orelse lookup_bool "strict" 

45520  298 
val lam_trans = lookup_option lookup_string "lam_trans" 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

299 
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" 
48321  300 
val learn = lookup_bool "learn" 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

301 
val fact_filter = lookup_option lookup_string "fact_filter" 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

302 
val max_facts = lookup_option lookup_int "max_facts" 
48293  303 
val fact_thresholds = lookup_real_pair "fact_thresholds" 
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

304 
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

305 
val max_new_mono_instances = 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

306 
lookup_option lookup_int "max_new_mono_instances" 
35963  307 
val isar_proof = lookup_bool "isar_proof" 
36924  308 
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") 
45706  309 
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

310 
val minimize = 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

311 
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" 
43021  312 
val timeout = 
313 
(if mode = Auto_Try then NONE else lookup_time "timeout") > the_timeout 

43015
21b6baec55b1
renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents:
43013
diff
changeset

314 
val preplay_timeout = 
43021  315 
if mode = Auto_Try then Time.zeroTime 
43015
21b6baec55b1
renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents:
43013
diff
changeset

316 
else lookup_time "preplay_timeout" > the_timeout 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

317 
val expect = lookup_string "expect" 
35963  318 
in 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

319 
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, 
46301  320 
provers = provers, type_enc = type_enc, strict = strict, 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

321 
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, 
48321  322 
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

323 
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, 
48388  324 
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

325 
isar_shrink_factor = isar_shrink_factor, slice = slice, 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

326 
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

327 
expect = expect} 
35963  328 
end 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

329 

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

330 
fun get_params mode = extract_params mode o default_raw_params 
43021  331 
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

332 

36373
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36371
diff
changeset

333 
(* Sledgehammer the given subgoal *) 
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36371
diff
changeset

334 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

335 
val default_minimize_prover = metisN 
43051  336 

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

337 
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

338 
member (op =) params_for_minimize name 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

339 
fun string_for_raw_param (key, values) = 
42776  340 
key ^ (case implode_param values of "" => ""  value => " = " ^ value) 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

341 

45520  342 
fun minimize_command override_params i more_override_params prover_name 
343 
fact_names = 

43057  344 
let 
345 
val params = 

45520  346 
(override_params 
347 
> filter_out (AList.defined (op =) more_override_params o fst)) @ 

348 
more_override_params 

43057  349 
> filter is_raw_param_relevant_for_minimize 
350 
> map string_for_raw_param 

351 
> (if prover_name = default_minimize_prover then I else cons prover_name) 

352 
> space_implode ", " 

353 
in 

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

354 
sledgehammerN ^ " " ^ minN ^ 
43057  355 
(if params = "" then "" else enclose " [" "]" params) ^ 
356 
" (" ^ space_implode " " fact_names ^ ")" ^ 

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

358 
end 

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

359 

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

360 
val default_learn_atp_timeout = 0.5 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

361 

48292  362 
fun hammer_away override_params subcommand opt_i fact_override state = 
35963  363 
let 
40069  364 
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

365 
val override_params = override_params > map (normalize_raw_param ctxt) 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

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

367 
if subcommand = runN then 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

368 
let val i = the_default 1 opt_i in 
43021  369 
run_sledgehammer (get_params Normal ctxt override_params) Normal i 
48292  370 
fact_override (minimize_command override_params i) 
39318  371 
state 
372 
> K () 

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

373 
end 
43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
42997
diff
changeset

374 
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

375 
let 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

376 
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

377 
val i = the_default 1 opt_i 
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

378 
val params as {provers, ...} = 
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

379 
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

380 
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

381 
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

382 
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

383 
Termtab.empty [] [] goal 
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

384 
val do_learn = mash_learn_proof ctxt params (hd provers) goal facts 
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

385 
in run_minimize params do_learn i (#add fact_override) state end 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

386 
else if subcommand = messagesN then 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

387 
messages opt_i 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

388 
else if subcommand = supported_proversN then 
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

389 
supported_provers ctxt 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

390 
else if subcommand = kill_proversN then 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

391 
kill_provers () 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

392 
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

393 
running_provers () 
48383  394 
else if subcommand = unlearnN then 
395 
mash_unlearn ctxt 

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

396 
else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

397 
subcommand = relearn_isarN orelse subcommand = relearn_atpN then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

398 
(if subcommand = relearn_isarN orelse subcommand = relearn_atpN then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

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

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

401 
(); 
48383  402 
mash_learn ctxt (get_params Normal ctxt 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

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

404 
[string_of_real default_learn_atp_timeout]) :: 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

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

406 
[("slice", ["false"]), 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

407 
("minimize", ["true"]), 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

408 
("preplay_timeout", ["0"])])) 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

409 
fact_override (#facts (Proof.goal state)) 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

410 
(subcommand = learn_atpN orelse subcommand = relearn_atpN)) 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

411 
else if subcommand = kill_learnersN then 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

412 
kill_learners () 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

413 
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

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

415 
else if subcommand = refresh_tptpN then 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

416 
refresh_systems_on_tptp () 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

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

418 
error ("Unknown subcommand: " ^ quote subcommand ^ ".") 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

419 
end 
35963  420 

48292  421 
fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = 
422 
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

423 
o Toplevel.proof_of) 
35963  424 

42776  425 
fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value 
35963  426 

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

427 
fun sledgehammer_params_trans params = 
35963  428 
Toplevel.theory 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

429 
(fold set_default_raw_param params 
39318  430 
#> tap (fn thy => 
42361  431 
let val ctxt = Proof_Context.init_global thy in 
40069  432 
writeln ("Default parameters for Sledgehammer:\n" ^ 
433 
(case default_raw_params ctxt > rev of 

434 
[] => "none" 

435 
 params => 

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

436 
params > map string_for_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

437 
> sort_strings > cat_lines)) 
40069  438 
end)) 
35963  439 

46949  440 
val parse_query_bang = @{keyword "?"}  @{keyword "!"}  @{keyword "!!"} 
42776  441 
val parse_key = 
44768  442 
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

443 
val parse_value = 
44768  444 
Scan.repeat1 (Parse.xname  Parse.float_number  parse_query_bang) 
46949  445 
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

446 
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

447 
val parse_fact_refs = 
38996  448 
Scan.repeat1 (Scan.unless (Parse.name  Args.colon) Parse_Spec.xthm) 
48293  449 
val parse_fact_override_chunk = 
48292  450 
(Args.add  Args.colon  parse_fact_refs >> add_fact_override) 
451 
 (Args.del  Args.colon  parse_fact_refs >> del_fact_override) 

452 
 (parse_fact_refs >> only_fact_override) 

453 
val parse_fact_override = 

48293  454 
Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk 
48292  455 
>> merge_fact_overrides)) 
456 
no_fact_override 

35963  457 

458 
val _ = 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

459 
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

460 
"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

461 
((Scan.optional Parse.short_ident runN  parse_params 
48292  462 
 parse_fact_override  Scan.option Parse.nat) #>> sledgehammer_trans) 
35963  463 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

464 
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

465 
"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

466 
(parse_params #>> sledgehammer_params_trans) 
36394
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

467 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

468 
fun try_sledgehammer auto state = 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

469 
let 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

470 
val ctxt = Proof.context_of state 
43021  471 
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

472 
val i = 1 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

473 
in 
48292  474 
run_sledgehammer (get_params mode ctxt []) mode i no_fact_override 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

475 
(minimize_command [] i) state 
40931  476 
end 
39318  477 

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

478 
val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer)) 
39318  479 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

480 
end; 