author  wenzelm 
Thu, 16 Apr 2015 14:18:32 +0200  
changeset 60094  96a4765ba7d1 
parent 59962  b622365f181c 
child 60190  906de96ba68a 
permissions  rwrr 
55198  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

3 

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

4 
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

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

6 

55198  7 
signature SLEDGEHAMMER_COMMANDS = 
35963  8 
sig 
55201  9 
type params = Sledgehammer_Prover.params 
35963  10 

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

11 
val provers : string Unsynchronized.ref 
55205  12 
val default_params : theory > (string * string) list > params 
35963  13 
end; 
14 

55198  15 
structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

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

17 

44784  18 
open ATP_Util 
38028  19 
open ATP_Systems 
46320  20 
open ATP_Problem_Generate 
57154  21 
open ATP_Proof 
46320  22 
open ATP_Proof_Reconstruct 
35971  23 
open Sledgehammer_Util 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
47962
diff
changeset

24 
open Sledgehammer_Fact 
55201  25 
open Sledgehammer_Prover 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

26 
open Sledgehammer_Prover_Minimize 
48381  27 
open Sledgehammer_MaSh 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

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

29 

59508  30 
val cvc4N = "cvc4" 
31 
val veritN = "verit" 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57208
diff
changeset

32 
val z3N = "z3" 
48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48400
diff
changeset

33 

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

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

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

36 
val supported_proversN = "supported_provers" 
50719
58b0b44da54a
renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
blanchet
parents:
50604
diff
changeset

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

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

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

40 
val refresh_tptpN = "refresh_tptp" 
48301  41 

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

42 
(** Sledgehammer commands **) 
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

43 

48292  44 
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} 
45 
fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} 

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

47 
fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = 

57273
01b68f625550
automatically learn MaSh facts also in 'blocking' mode
blanchet
parents:
57245
diff
changeset

48 
{add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} 
01b68f625550
automatically learn MaSh facts also in 'blocking' mode
blanchet
parents:
57245
diff
changeset

49 
fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

50 

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

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

52 

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

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

54 

35963  55 
type raw_param = string * string list 
56 

57 
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

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

60 
("overlord", "false"), 
53800  61 
("spy", "false"), 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

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

63 
("type_enc", "smart"), 
46301  64 
("strict", "false"), 
45514  65 
("lam_trans", "smart"), 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

66 
("uncurried_aliases", "smart"), 
48321  67 
("learn", "true"), 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

68 
("fact_filter", "smart"), 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

69 
("max_facts", "smart"), 
48293  70 
("fact_thresholds", "0.45 0.85"), 
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

71 
("max_mono_iters", "smart"), 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

72 
("max_new_mono_instances", "smart"), 
51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51189
diff
changeset

73 
("isar_proofs", "smart"), 
57783  74 
("compress", "smart"), 
57245  75 
("try0", "true"), 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset

76 
("smt_proofs", "smart"), 
45706  77 
("slice", "true"), 
57721  78 
("minimize", "true"), 
57719  79 
("preplay_timeout", "1")] 
35963  80 

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

81 
val alias_params = 
51138  82 
[("prover", ("provers", [])), (* undocumented *) 
51189  83 
("dont_preplay", ("preplay_timeout", ["0"])), 
57783  84 
("dont_compress", ("compress", ["1"])), 
52093  85 
("isar_proof", ("isar_proofs", [])) (* legacy *)] 
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

86 
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

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

89 
("no_overlord", "overlord"), 
53800  90 
("dont_spy", "spy"), 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

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

93 
("no_uncurried_aliases", "uncurried_aliases"), 
48321  94 
("dont_learn", "learn"), 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

95 
("no_isar_proofs", "isar_proofs"), 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

96 
("dont_slice", "slice"), 
51879  97 
("dont_minimize", "minimize"), 
57245  98 
("dont_try0", "try0"), 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset

99 
("no_smt_proofs", "smt_proofs")] 
35963  100 

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

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

102 

35963  103 
fun is_known_raw_param s = 
104 
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

105 
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

106 
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

107 
member (op =) property_dependent_params s orelse s = "expect" 
35963  108 

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

109 
fun is_prover_list ctxt s = 
55286  110 
(case space_explode " " s of 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

111 
ss as _ :: _ => forall (is_prover_supported ctxt) ss 
55286  112 
 _ => false) 
41258
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

113 

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

114 
fun unalias_raw_param (name, value) = 
55286  115 
(case AList.lookup (op =) alias_params name of 
47037  116 
SOME (name', []) => (name', value) 
117 
 SOME (param' as (name', _)) => 

118 
if value <> ["false"] then 

119 
param' 

120 
else 

57433  121 
error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ").") 
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

122 
 NONE => 
55286  123 
(case AList.lookup (op =) negated_alias_params name of 
124 
SOME name' => (name', 

125 
(case value of 

126 
["false"] => ["true"] 

127 
 ["true"] => ["false"] 

128 
 [] => ["false"] 

129 
 _ => value)) 

130 
 NONE => (name, value))) 

35963  131 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
52018
diff
changeset

132 
val any_type_enc = type_enc_of_string Strict "erased" 
45514  133 

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

136 
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

137 
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

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

139 
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

140 
(name, value) 
48533  141 
else if null value then 
142 
if is_prover_list ctxt name then 

143 
("provers", [name]) 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
52018
diff
changeset

144 
else if can (type_enc_of_string Strict) name then 
48533  145 
("type_enc", [name]) 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
52018
diff
changeset

146 
else if can (trans_lams_of_string ctxt any_type_enc) name then 
48533  147 
("lam_trans", [name]) 
148 
else if member (op =) fact_filters name then 

149 
("fact_filter", [name]) 

150 
else if is_some (Int.fromString name) then 

151 
("max_facts", [name]) 

152 
else 

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

48400  154 
else 
155 
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

156 

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

160 

54059  161 
(* FIXME: use "Generic_Data" *) 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41258
diff
changeset

162 
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

163 
( 
35963  164 
type T = raw_param list 
54546
8b403a7a8c44
fixed spying so that the envirnoment variables are queried at runtime not at buildtime
blanchet
parents:
54503
diff
changeset

165 
val empty = default_default_params > map (apsnd single) 
35963  166 
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

167 
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

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

169 

55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

170 
fun remotify_prover_if_supported_and_not_already_remote ctxt name = 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

171 
if String.isPrefix remote_prefix name then 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

172 
SOME name 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

173 
else 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

174 
let val remote_name = remote_prefix ^ name in 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

175 
if is_prover_supported ctxt remote_name then SOME remote_name else NONE 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

176 
end 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

177 

b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

178 
fun remotify_prover_if_not_installed ctxt name = 
57237
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57209
diff
changeset

179 
if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name 
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57209
diff
changeset

180 
else remotify_prover_if_supported_and_not_already_remote ctxt name 
55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

181 

57677  182 
(* The first ATP of the list is used by Auto Sledgehammer. *) 
55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

183 
fun default_provers_param_value mode ctxt = 
59962  184 
[cvc4N, vampireN, z3N, spassN, eN, veritN, e_sineN] 
55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

185 
> map_filter (remotify_prover_if_not_installed ctxt) 
54059  186 
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) 
187 
> take (Multithreading.max_threads_value ()  (if mode = Try then 1 else 0)) 

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

189 

44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

190 
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

191 
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

192 
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

193 
end 
54059  194 

55205  195 
fun default_raw_params mode thy = 
55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

196 
let val ctxt = Proof_Context.init_global thy in 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

197 
Data.get thy 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

198 
> fold (AList.default (op =)) 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

199 
[("provers", [(case !provers of "" => default_provers_param_value mode ctxt  s => s)]), 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

200 
("timeout", 
56467  201 
let val timeout = Options.default_int @{system_option sledgehammer_timeout} in 
55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

202 
[if timeout <= 0 then "none" else string_of_int timeout] 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

203 
end)] 
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

204 
end 
35963  205 

43021  206 
fun extract_params mode default_params override_params = 
35963  207 
let 
208 
val raw_params = rev override_params @ rev default_params 

42776  209 
val lookup = Option.map implode_param o AList.lookup (op =) raw_params 
35963  210 
val lookup_string = the_default "" o lookup 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

211 

35963  212 
fun general_lookup_bool option default_value name = 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

213 
(case lookup name of 
35970
3d41a2a490f0
revert debugging output that shouldn't have been submitted in the first place
blanchet
parents:
35966
diff
changeset

214 
SOME s => parse_bool_option option name s 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

215 
 NONE => default_value) 
35963  216 
val lookup_bool = the o general_lookup_bool false (SOME false) 
217 
fun lookup_time name = 

54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

218 
(case lookup name of 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

219 
SOME s => parse_time name s 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

220 
 NONE => Time.zeroTime) 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

221 
fun lookup_int name = 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

222 
(case lookup name of 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

223 
NONE => 0 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

224 
 SOME s => 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

225 
(case Int.fromString s of 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

226 
SOME n => n 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

227 
 NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value."))) 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

228 
fun lookup_real name = 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

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

230 
NONE => 0.0 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

231 
 SOME s => 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

232 
(case Real.fromString s of 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

233 
SOME n => n 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

234 
 NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value."))) 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

235 
fun lookup_real_pair name = 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

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

237 
NONE => (0.0, 0.0) 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

238 
 SOME s => 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

239 
(case s > space_explode " " > map Real.fromString of 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

240 
[SOME r1, SOME r2] => (r1, r2) 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

241 
 _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floatingpoint \ 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

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

243 
fun lookup_option lookup' name = 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

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

245 
SOME "smart" => NONE 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

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

249 
val overlord = lookup_bool "overlord" 
54546
8b403a7a8c44
fixed spying so that the envirnoment variables are queried at runtime not at buildtime
blanchet
parents:
54503
diff
changeset

250 
val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" 
42995
e23f61546cf0
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents:
42944
diff
changeset

251 
val blocking = 
56982  252 
Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking" 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

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

254 
val type_enc = 
43021  255 
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

256 
NONE 
55286  257 
else 
258 
(case lookup_string "type_enc" of 

259 
"smart" => NONE 

260 
 s => (type_enc_of_string Strict s; SOME s)) 

46301  261 
val strict = mode = Auto_Try orelse lookup_bool "strict" 
45520  262 
val lam_trans = lookup_option lookup_string "lam_trans" 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

263 
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" 
48321  264 
val learn = lookup_bool "learn" 
54113
df080dfefddc
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents:
54059
diff
changeset

265 
val fact_filter = 
df080dfefddc
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents:
54059
diff
changeset

266 
lookup_option lookup_string "fact_filter" 
df080dfefddc
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents:
54059
diff
changeset

267 
> mode = Auto_Try ? (fn NONE => SOME mepoN  sf => sf) 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

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

270 
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

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

272 
lookup_option lookup_int "max_new_mono_instances" 
51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51189
diff
changeset

273 
val isar_proofs = lookup_option lookup_bool "isar_proofs" 
57783  274 
val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") 
57245  275 
val try0 = lookup_bool "try0" 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset

276 
val smt_proofs = lookup_option lookup_bool "smt_proofs" 
45706  277 
val slice = mode <> Auto_Try andalso lookup_bool "slice" 
57721  278 
val minimize = mode <> Auto_Try andalso lookup_bool "minimize" 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

279 
val timeout = lookup_time "timeout" 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

280 
val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout" 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

281 
val expect = lookup_string "expect" 
35963  282 
in 
53800  283 
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, 
284 
provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, 

285 
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, 

286 
max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49632
diff
changeset

287 
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, 
57245  288 
compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, 
289 
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} 

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

291 

54059  292 
fun get_params mode = extract_params mode o default_raw_params mode 
43021  293 
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

294 

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

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

296 

50604  297 
val default_learn_prover_timeout = 2.0 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

298 

58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58028
diff
changeset

299 
fun hammer_away override_params subcommand opt_i fact_override state0 = 
35963  300 
let 
58089
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

301 
(* We generally want chained facts to be picked up by the relevance filter, because it can then 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

302 
give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

303 
verbose output, machine learning). However, if the fact is available by no other means (not 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

304 
even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

305 
but to insert it into the state as an additional hypothesis. 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

306 
*) 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

307 
val {facts = chained0, ...} = Proof.goal state0 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

308 
val (inserts, keep_chained) = 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

309 
if null chained0 orelse #only fact_override then 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

310 
(chained0, []) 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

311 
else 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

312 
let val ctxt0 = Proof.context_of state0 in 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

313 
List.partition (is_useful_unnamed_local_fact ctxt0) chained0 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

314 
end 
58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58028
diff
changeset

315 
val state = state0 
58089
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

316 
> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) 
58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58028
diff
changeset

317 
> Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) 
58089
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58075
diff
changeset

318 

55205  319 
val thy = Proof.theory_of state 
40069  320 
val ctxt = Proof.context_of state 
55205  321 

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

322 
val override_params = override_params > map (normalize_raw_param ctxt) 
50052  323 
val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP")) 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

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

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

326 
let val i = the_default 1 opt_i in 
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

327 
ignore (run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

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

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

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

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

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

333 
supported_provers ctxt 
50719
58b0b44da54a
renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
blanchet
parents:
50604
diff
changeset

334 
else if subcommand = kill_allN then 
57433  335 
(kill_provers (); kill_learners ()) 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

336 
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

337 
running_provers () 
48383  338 
else if subcommand = unlearnN then 
57433  339 
mash_unlearn () 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50052
diff
changeset

340 
else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50052
diff
changeset

341 
subcommand = relearn_isarN orelse subcommand = relearn_proverN then 
57433  342 
(if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn () 
343 
else (); 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50052
diff
changeset

344 
mash_learn ctxt 
54129  345 
(* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) 
55205  346 
(get_params Normal thy 
347 
([("timeout", [string_of_real default_learn_prover_timeout]), 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50052
diff
changeset

348 
("slice", ["false"])] @ 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50052
diff
changeset

349 
override_params @ 
57721  350 
[("preplay_timeout", ["0"])])) 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50052
diff
changeset

351 
fact_override (#facts (Proof.goal state)) 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50052
diff
changeset

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

353 
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

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

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

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

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

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

359 
end 
35963  360 

48292  361 
fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

362 
Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) 
35963  363 

57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

364 
fun string_of_raw_param (key, values) = 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

365 
key ^ (case implode_param values of "" => ""  value => " = " ^ value) 
35963  366 

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

367 
fun sledgehammer_params_trans params = 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

368 
Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

369 
writeln ("Default parameters for Sledgehammer:\n" ^ 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

370 
(case rev (default_raw_params Normal thy) of 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

371 
[] => "none" 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

372 
 params => params > map string_of_raw_param > sort_strings > cat_lines)))) 
35963  373 

46949  374 
val parse_query_bang = @{keyword "?"}  @{keyword "!"}  @{keyword "!!"} 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

375 
val parse_key = Scan.repeat1 (Parse.typ_group  parse_query_bang) >> implode_param 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

376 
val parse_value = Scan.repeat1 (Parse.xname  Parse.float_number  parse_query_bang) 
46949  377 
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

378 
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] 
58028
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
57783
diff
changeset

379 
val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name  Args.colon) Parse.xthm) 
48293  380 
val parse_fact_override_chunk = 
48292  381 
(Args.add  Args.colon  parse_fact_refs >> add_fact_override) 
382 
 (Args.del  Args.colon  parse_fact_refs >> del_fact_override) 

383 
 (parse_fact_refs >> only_fact_override) 

384 
val parse_fact_override = 

57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

385 
Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) 
57433  386 
no_fact_override 
35963  387 

388 
val _ = 

59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59508
diff
changeset

389 
Outer_Syntax.command @{command_keyword sledgehammer} 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

390 
"search for firstorder proof using automatic theorem provers" 
58831
aa8cf5eed06e
proper syntax categery "name"  as usual and as documented;
wenzelm
parents:
58089
diff
changeset

391 
((Scan.optional Parse.name runN  parse_params 
48292  392 
 parse_fact_override  Scan.option Parse.nat) #>> sledgehammer_trans) 
35963  393 
val _ = 
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59508
diff
changeset

394 
Outer_Syntax.command @{command_keyword sledgehammer_params} 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

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

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

397 

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

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

399 
let 
55205  400 
val thy = Proof.theory_of state 
43021  401 
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

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

403 
in 
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

404 
run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override state 
40931  405 
end 
39318  406 

56467  407 
val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer)) 
39318  408 

52908
3461985dcbc3
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
52653
diff
changeset

409 
val _ = 
52982
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52908
diff
changeset

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

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

412 
SOME state => 
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

413 
let 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

414 
val thy = Proof.theory_of state 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

415 
val ctxt = Proof.context_of state 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

416 
val [provers_arg, isar_proofs_arg] = args 
52908
3461985dcbc3
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
52653
diff
changeset

417 

57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

418 
val override_params = 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

419 
((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

420 
[("isar_proofs", [isar_proofs_arg]), 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

421 
("blocking", ["true"]), 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

422 
("debug", ["false"]), 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

423 
("verbose", ["false"]), 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

424 
("overlord", ["false"])]) 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

425 
> map (normalize_raw_param ctxt) 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

426 
in 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

427 
ignore (run_sledgehammer (get_params Normal thy override_params) Normal 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

428 
(SOME output_result) 1 no_fact_override state) 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57732
diff
changeset

429 
end 
53055
0fe8a9972eda
some protocol to determine provers according to ML;
wenzelm
parents:
53053
diff
changeset

430 
 NONE => error "Unknown proof context")) 
0fe8a9972eda
some protocol to determine provers according to ML;
wenzelm
parents:
53053
diff
changeset

431 

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

432 
end; 