author  blanchet 
Thu, 01 Dec 2011 13:34:13 +0100  
changeset 45706  418846ea4f99 
parent 45520  2b1dde0b1c30 
child 45707  6bf7eec9b153 
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 

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

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

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

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

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

21 

44784  22 
open ATP_Util 
38028  23 
open ATP_Systems 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

25 
open ATP_Reconstruct 
35971  26 
open Sledgehammer_Util 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44397
diff
changeset

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

28 
open Sledgehammer_Provers 
38988  29 
open Sledgehammer_Minimize 
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 sledgehammerN = "sledgehammer" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

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

34 

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

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

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

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

38 
val supported_proversN = "supported_provers" 
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" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

40 
val kill_proversN = "kill_provers" 
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" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

42 

39318  43 
val auto = Unsynchronized.ref false 
44 

45 
val _ = 

46 
ProofGeneralPgip.add_preference Preferences.category_tracing 

47 
(Preferences.bool_pref auto "autosledgehammer" 

39327  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 

39318  52 
fun add_relevance_override ns : relevance_override = 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

53 
{add = ns, del = [], only = false} 
39318  54 
fun del_relevance_override ns : relevance_override = 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

55 
{add = [], del = ns, only = false} 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

56 
fun only_relevance_override ns : relevance_override = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

57 
{add = ns, del = [], only = true} 
36003  58 
fun merge_relevance_override_pairwise (r1 : relevance_override) 
59 
(r2 : relevance_override) = 

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

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

61 
only = #only r1 andalso #only r2} 
36188  62 
fun merge_relevance_overrides rs = 
63 
fold merge_relevance_override_pairwise rs (only_relevance_override []) 

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

64 

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

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

66 

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

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

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

69 

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

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

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

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

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

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

75 

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

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

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

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

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

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

81 

35963  82 
type raw_param = string * string list 
83 

84 
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

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

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

88 
("blocking", "false"), 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

89 
("type_enc", "smart"), 
43572
ae612a423dad
added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents:
43569
diff
changeset

90 
("sound", "false"), 
45514  91 
("lam_trans", "smart"), 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41727
diff
changeset

92 
("relevance_thresholds", "0.45 0.85"), 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41727
diff
changeset

93 
("max_relevant", "smart"), 
42783
226962b6a6d1
reduce the number of mono iterations to prevent the mono code from going berserk
blanchet
parents:
42776
diff
changeset

94 
("max_mono_iters", "3"), 
43352
597f31069e18
fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer  backed up by Judgment Day
blanchet
parents:
43259
diff
changeset

95 
("max_new_mono_instances", "200"), 
35963  96 
("isar_proof", "false"), 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

97 
("isar_shrink_factor", "1"), 
45706  98 
("slice", "true"), 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43024
diff
changeset

99 
("preplay_timeout", "4")] 
35963  100 

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

101 
val alias_params = 
43353
6c008d3efb0a
removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them
blanchet
parents:
43352
diff
changeset

102 
[("prover", "provers")] 
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

103 
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

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

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

107 
("non_blocking", "blocking"), 
43572
ae612a423dad
added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents:
43569
diff
changeset

108 
("unsound", "sound"), 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

109 
("no_isar_proof", "isar_proof"), 
45706  110 
("dont_slice", "slice")] 
35963  111 

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

112 
val params_for_minimize = 
45514  113 
["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans", 
114 
"max_mono_iters", "max_new_mono_instances", "isar_proof", 

115 
"isar_shrink_factor", "timeout", "preplay_timeout"] 

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

116 

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

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

118 

35963  119 
fun is_known_raw_param s = 
120 
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

121 
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

122 
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

123 
member (op =) property_dependent_params s orelse s = "expect" 
35963  124 

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

125 
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

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

127 
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

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

129 

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

130 
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

131 
case AList.lookup (op =) alias_params name of 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

132 
SOME name' => (name', value) 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

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

134 
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

135 
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

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

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

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

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

140 
 NONE => (name, value) 
35963  141 

45514  142 
val any_type_enc = type_enc_from_string Sound "erased" 
143 

144 
(* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two, 

145 
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

146 
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

147 
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

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

149 
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

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

151 
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

152 
("provers", [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

153 
else if can (type_enc_from_string Sound) 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

154 
("type_enc", [name]) 
45514  155 
else if can (trans_lams_from_string ctxt any_type_enc) name andalso 
156 
null value then 

157 
("lam_trans", [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

158 
else 
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 
error ("Unknown parameter: " ^ quote 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

160 

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 

44785  162 
(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are 
163 
read correctly. *) 

44784  164 
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

165 

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

166 
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

167 
( 
35963  168 
type T = raw_param list 
169 
val empty = default_default_params > map (apsnd single) 

170 
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

171 
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

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

173 

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

174 
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

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

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

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

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

179 
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

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

181 

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

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

183 
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

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

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

186 
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

187 

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

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

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

190 
 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

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

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

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

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

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

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

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

198 
 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

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

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

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

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

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

204 
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

205 

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

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

207 

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

208 
(* 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

209 
timeout, it makes sense to put SPASS first. *) 
40069  210 
fun default_provers_param_value ctxt = 
45063
b3b50d8b535a
reintroduced ESInE now that it's unexpectedly working again (thanks to Geoff)
blanchet
parents:
45048
diff
changeset

211 
[spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN] 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40931
diff
changeset

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

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

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

216 

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

217 
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

218 
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

219 
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

220 
end 
40069  221 
fun default_raw_params ctxt = 
42361  222 
let val thy = Proof_Context.theory_of ctxt in 
40069  223 
Data.get thy 
224 
> fold (AList.default (op =)) 

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

226 
"" => default_provers_param_value ctxt 

227 
 s => s]), 

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

229 
[if timeout <= 0 then "none" 

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

230 
else string_of_int timeout] 
40069  231 
end)] 
232 
end 

35963  233 

234 
val infinity_time_in_secs = 60 * 60 * 24 * 365 

235 
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) 

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

236 

43021  237 
fun extract_params mode default_params override_params = 
35963  238 
let 
239 
val raw_params = rev override_params @ rev default_params 

42776  240 
val lookup = Option.map implode_param o AList.lookup (op =) raw_params 
35963  241 
val lookup_string = the_default "" o lookup 
242 
fun general_lookup_bool option default_value name = 

243 
case lookup name of 

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

244 
SOME s => parse_bool_option option name s 
35963  245 
 NONE => default_value 
246 
val lookup_bool = the o general_lookup_bool false (SOME false) 

247 
fun lookup_time name = 

39318  248 
case lookup name of 
249 
SOME s => parse_time_option name s 

250 
 NONE => NONE 

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

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

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

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

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

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

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

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

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

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

261 
 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

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

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

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

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

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

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

268 
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

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

272 
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

273 
val blocking = 
43021  274 
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

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

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

278 
val type_enc = 
43021  279 
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

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

281 
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

282 
"smart" => NONE 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44092
diff
changeset

283 
 s => (type_enc_from_string Sound s; SOME s) 
43572
ae612a423dad
added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents:
43569
diff
changeset

284 
val sound = mode = Auto_Try orelse lookup_bool "sound" 
45520  285 
val lam_trans = lookup_option lookup_string "lam_trans" 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41727
diff
changeset

286 
val relevance_thresholds = lookup_real_pair "relevance_thresholds" 
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

287 
val max_relevant = lookup_option lookup_int "max_relevant" 
42724
4d6bcf846759
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents:
42688
diff
changeset

288 
val max_mono_iters = lookup_int "max_mono_iters" 
42740
31334a7b109d
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents:
42736
diff
changeset

289 
val max_new_mono_instances = lookup_int "max_new_mono_instances" 
35963  290 
val isar_proof = lookup_bool "isar_proof" 
36924  291 
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") 
45706  292 
val slice = mode <> Auto_Try andalso lookup_bool "slice" 
43021  293 
val timeout = 
294 
(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

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

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

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

300 
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, 
45514  301 
provers = provers, type_enc = type_enc, sound = sound, 
302 
lam_trans = lam_trans, relevance_thresholds = relevance_thresholds, 

42724
4d6bcf846759
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents:
42688
diff
changeset

303 
max_relevant = max_relevant, max_mono_iters = max_mono_iters, 
45514  304 
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, 
45706  305 
isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout, 
306 
preplay_timeout = preplay_timeout, expect = expect} 

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

308 

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

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

311 

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

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

313 

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

314 
val default_minimize_prover = metisN 
43051  315 

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

316 
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

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

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

320 

45520  321 
fun minimize_command override_params i more_override_params prover_name 
322 
fact_names = 

43057  323 
let 
324 
val params = 

45520  325 
(override_params 
326 
> filter_out (AList.defined (op =) more_override_params o fst)) @ 

327 
more_override_params 

43057  328 
> filter is_raw_param_relevant_for_minimize 
329 
> map string_for_raw_param 

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

331 
> space_implode ", " 

332 
in 

333 
sledgehammerN ^ " " ^ minN ^ 

334 
(if params = "" then "" else enclose " [" "]" params) ^ 

335 
" (" ^ space_implode " " fact_names ^ ")" ^ 

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

337 
end 

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

338 

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

339 
fun hammer_away override_params subcommand opt_i relevance_override state = 
35963  340 
let 
40069  341 
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

342 
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

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

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

345 
let val i = the_default 1 opt_i in 
43021  346 
run_sledgehammer (get_params Normal ctxt override_params) Normal i 
39318  347 
relevance_override (minimize_command override_params i) 
348 
state 

349 
> K () 

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

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

351 
else if subcommand = minN then 
43051  352 
run_minimize (get_params Minimize ctxt 
353 
(("provers", [default_minimize_prover]) :: 

354 
override_params)) 

43021  355 
(the_default 1 opt_i) (#add relevance_override) state 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

368 
end 
35963  369 

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

370 
fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

371 
Toplevel.keep (hammer_away params subcommand opt_i relevance_override 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

372 
o Toplevel.proof_of) 
35963  373 

42776  374 
fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value 
35963  375 

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

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

378 
(fold set_default_raw_param params 
39318  379 
#> tap (fn thy => 
42361  380 
let val ctxt = Proof_Context.init_global thy in 
40069  381 
writeln ("Default parameters for Sledgehammer:\n" ^ 
382 
(case default_raw_params ctxt > rev of 

383 
[] => "none" 

384 
 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

385 
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

386 
> sort_strings > cat_lines)) 
40069  387 
end)) 
35963  388 

44768  389 
val parse_query_bang = Parse.$$$ "?"  Parse.$$$ "!"  Parse.$$$ "!!" 
42776  390 
val parse_key = 
44768  391 
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

392 
val parse_value = 
44768  393 
Scan.repeat1 (Parse.xname  Parse.float_number  parse_query_bang) 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36924
diff
changeset

394 
val parse_param = parse_key  Scan.optional (Parse.$$$ "="  parse_value) [] 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36924
diff
changeset

395 
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

396 
val parse_fact_refs = 
38996  397 
Scan.repeat1 (Scan.unless (Parse.name  Args.colon) Parse_Spec.xthm) 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

398 
val parse_relevance_chunk = 
39318  399 
(Args.add  Args.colon  parse_fact_refs >> add_relevance_override) 
400 
 (Args.del  Args.colon  parse_fact_refs >> del_relevance_override) 

36188  401 
 (parse_fact_refs >> only_relevance_override) 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

402 
val parse_relevance_override = 
36188  403 
Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk 
404 
>> merge_relevance_overrides)) 

39318  405 
no_relevance_override 
35963  406 
val parse_sledgehammer_command = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37344
diff
changeset

407 
(Scan.optional Parse.short_ident runN  parse_params 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37344
diff
changeset

408 
 parse_relevance_override  Scan.option Parse.nat) #>> sledgehammer_trans 
35963  409 
val parse_sledgehammer_params_command = 
410 
parse_params #>> sledgehammer_params_trans 

411 

412 
val _ = 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36924
diff
changeset

413 
Outer_Syntax.improper_command sledgehammerN 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36924
diff
changeset

414 
"search for firstorder proof using automatic theorem provers" Keyword.diag 
36394
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

415 
parse_sledgehammer_command 
35963  416 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36924
diff
changeset

417 
Outer_Syntax.command sledgehammer_paramsN 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36924
diff
changeset

418 
"set and display the default parameters for Sledgehammer" Keyword.thy_decl 
36394
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

419 
parse_sledgehammer_params_command 
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

420 

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

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

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

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

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

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

428 
(minimize_command [] i) state 
40931  429 
end 
39318  430 

43024
58150aa44941
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents:
43021
diff
changeset

431 
val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer)) 
39318  432 

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

433 
end; 