author  desharna 
Tue, 28 Sep 2021 10:38:36 +0200  
changeset 74369  3301c0d8b560 
parent 74352  fb8ce6090437 
child 74370  d8dc8fdc46fc 
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 
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
72400
diff
changeset

13 
val parse_params: (string * string) list parser 
35963  14 
end; 
15 

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

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

18 

44784  19 
open ATP_Util 
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 
72400  25 
open Sledgehammer_ATP_Systems 
55201  26 
open Sledgehammer_Prover 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

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

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

30 

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

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

33 
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

34 

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

37 
val refresh_tptpN = "refresh_tptp" 
48301  38 

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

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

40 

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

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

44 
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

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

46 
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

47 

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

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

49 

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

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

51 

35963  52 
type raw_param = string * string list 
53 

54 
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

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

57 
("overlord", "false"), 
53800  58 
("spy", "false"), 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

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

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

64 
("fact_filter", "smart"), 
73940
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset

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

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

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

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

70 
("isar_proofs", "smart"), 
57783  71 
("compress", "smart"), 
57245  72 
("try0", "true"), 
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
70934
diff
changeset

73 
("smt_proofs", "true"), 
45706  74 
("slice", "true"), 
57721  75 
("minimize", "true"), 
57719  76 
("preplay_timeout", "1")] 
35963  77 

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

78 
val alias_params = 
51138  79 
[("prover", ("provers", [])), (* undocumented *) 
51189  80 
("dont_preplay", ("preplay_timeout", ["0"])), 
57783  81 
("dont_compress", ("compress", ["1"])), 
52093  82 
("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

83 
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

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

86 
("no_overlord", "overlord"), 
53800  87 
("dont_spy", "spy"), 
46301  88 
("non_strict", "strict"), 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

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

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

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

95 
("no_smt_proofs", "smt_proofs")] 
35963  96 

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

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

98 

35963  99 
fun is_known_raw_param s = 
100 
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

101 
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

102 
AList.defined (op =) negated_alias_params s orelse 
67405
e9ab4ad7bd15
uniform use of Standard ML opinfix  eliminated warnings;
wenzelm
parents:
67399
diff
changeset

103 
member (op =) property_dependent_params s orelse s = "expect" 
35963  104 

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

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

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

109 

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

110 
fun unalias_raw_param (name, value) = 
55286  111 
(case AList.lookup (op =) alias_params name of 
47037  112 
SOME (name', []) => (name', value) 
113 
 SOME (param' as (name', _)) => 

114 
if value <> ["false"] then 

115 
param' 

116 
else 

63692  117 
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

118 
 NONE => 
55286  119 
(case AList.lookup (op =) negated_alias_params name of 
120 
SOME name' => (name', 

121 
(case value of 

122 
["false"] => ["true"] 

123 
 ["true"] => ["false"] 

124 
 [] => ["false"] 

125 
 _ => value)) 

126 
 NONE => (name, value))) 

35963  127 

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

128 
val any_type_enc = type_enc_of_string Strict "erased" 
45514  129 

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

132 
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

133 
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

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

135 
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

136 
(name, value) 
48533  137 
else if null value then 
138 
if is_prover_list ctxt name then 

139 
("provers", [name]) 

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

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

142 
else if can (trans_lams_of_string ctxt any_type_enc) name then 
48533  143 
("lam_trans", [name]) 
144 
else if member (op =) fact_filters name then 

145 
("fact_filter", [name]) 

146 
else if is_some (Int.fromString name) then 

147 
("max_facts", [name]) 

148 
else 

63692  149 
error ("Unknown parameter: " ^ quote name) 
48400  150 
else 
63692  151 
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

152 

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

156 

54059  157 
(* 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

158 
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

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

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

163 
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

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

165 

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

166 
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

167 
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

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

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

170 
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

171 
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

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

173 

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

174 
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

175 
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

176 
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

177 

57677  178 
(* 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

179 
fun default_provers_param_value mode ctxt = 
74369
3301c0d8b560
added Zipperposition to sledgehammer's default provers
desharna
parents:
74352
diff
changeset

180 
[cvc4N, vampireN, z3N, eN, spassN, veritN, zipperpositionN] 
55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

181 
> map_filter (remotify_prover_if_not_installed ctxt) 
54059  182 
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) 
62925  183 
> take (Multithreading.max_threads ()  (if mode = Try then 1 else 0)) 
42776  184 
> implode_param 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

185 

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

186 
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

187 
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

188 
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

189 
end 
54059  190 

55205  191 
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

192 
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

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

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

195 
[("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

196 
("timeout", 
69593  197 
let val timeout = Options.default_int \<^system_option>\<open>sledgehammer_timeout\<close> in 
55475
b8ebbcc5e49a
restored old 'remotify' logic  too many bugs were introduced when refactoring the code
blanchet
parents:
55458
diff
changeset

198 
[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

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

200 
end 
35963  201 

43021  202 
fun extract_params mode default_params override_params = 
35963  203 
let 
204 
val raw_params = rev override_params @ rev default_params 

42776  205 
val lookup = Option.map implode_param o AList.lookup (op =) raw_params 
35963  206 
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

207 

35963  208 
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

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

210 
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

211 
 NONE => default_value) 
35963  212 
val lookup_bool = the o general_lookup_bool false (SOME false) 
213 
fun lookup_time name = 

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

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

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

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

217 
fun lookup_int 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 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

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

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

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

222 
SOME n => n 
63692  223 
 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

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

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

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

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

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

229 
SOME n => n 
63692  230 
 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

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

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

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

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

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

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

237 
 _ => 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

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

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

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

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

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

245 
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

246 
val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57274
diff
changeset

247 
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

248 
val type_enc = 
43021  249 
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

250 
NONE 
55286  251 
else 
252 
(case lookup_string "type_enc" of 

253 
"smart" => NONE 

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

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

257 
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" 
48321  258 
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

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

260 
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

261 
> mode = Auto_Try ? (fn NONE => SOME mepoN  sf => sf) 
73940
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset

262 
val induction_rules = 
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset

263 
lookup_option (the o induction_rules_of_string o lookup_string) "induction_rules" 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

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

266 
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

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

268 
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

269 
val isar_proofs = lookup_option lookup_bool "isar_proofs" 
57783  270 
val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") 
57245  271 
val try0 = lookup_bool "try0" 
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
70934
diff
changeset

272 
val smt_proofs = lookup_bool "smt_proofs" 
45706  273 
val slice = mode <> Auto_Try andalso lookup_bool "slice" 
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60277
diff
changeset

274 
val minimize = lookup_bool "minimize" 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54546
diff
changeset

275 
val timeout = lookup_time "timeout" 
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60277
diff
changeset

276 
val preplay_timeout = lookup_time "preplay_timeout" 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

277 
val expect = lookup_string "expect" 
35963  278 
in 
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset

279 
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, 
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset

280 
type_enc = type_enc, strict = strict, lam_trans = lam_trans, 
53800  281 
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, 
73939
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
73691
diff
changeset

282 
induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, 
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
73691
diff
changeset

283 
max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, 
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
73691
diff
changeset

284 
isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, 
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
73691
diff
changeset

285 
slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, 
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
73691
diff
changeset

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

288 

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

291 

60564  292 
val silence_state = 
293 
Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) 

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 

61223  299 
fun hammer_away override_params writeln_result 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) 
60564  317 
> silence_state 
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) 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

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

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

325 
let val i = the_default 1 opt_i in 
60564  326 
ignore (run_sledgehammer 
61223  327 
(get_params Normal thy override_params) Normal writeln_result i fact_override state) 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

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

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

330 
supported_provers ctxt 
48383  331 
else if subcommand = unlearnN then 
64522
b66f8caf86b6
made MaSh faster and less likely to hang seemingly forever
blanchet
parents:
63692
diff
changeset

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

333 
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

334 
subcommand = relearn_isarN orelse subcommand = relearn_proverN then 
64522
b66f8caf86b6
made MaSh faster and less likely to hang seemingly forever
blanchet
parents:
63692
diff
changeset

335 
(if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt 
57433  336 
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

337 
mash_learn ctxt 
54129  338 
(* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) 
55205  339 
(get_params Normal thy 
340 
([("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

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

342 
override_params @ 
57721  343 
[("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

344 
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

345 
(subcommand = learn_proverN orelse subcommand = relearn_proverN)) 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

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

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

348 
else 
63692  349 
error ("Unknown subcommand: " ^ quote subcommand) 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

350 
end 
35963  351 

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

352 
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

353 
key ^ (case implode_param values of "" => ""  value => " = " ^ value) 
35963  354 

69593  355 
val parse_query_bang = \<^keyword>\<open>?\<close>  \<^keyword>\<open>!\<close>  \<^keyword>\<open>!!\<close> 
63136  356 
val parse_key = Scan.repeat1 (Parse.embedded  parse_query_bang) >> implode_param 
62969  357 
val parse_value = Scan.repeat1 (Parse.name  Parse.float_number  parse_query_bang) 
69593  358 
val parse_param = parse_key  Scan.optional (\<^keyword>\<open>=\<close>  parse_value) [] 
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
72400
diff
changeset

359 
val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] 
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
72400
diff
changeset

360 
val parse_params = parse_raw_params >> map (apsnd implode_param) 
62969  361 
val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name  Args.colon) Parse.thm) 
48293  362 
val parse_fact_override_chunk = 
48292  363 
(Args.add  Args.colon  parse_fact_refs >> add_fact_override) 
364 
 (Args.del  Args.colon  parse_fact_refs >> del_fact_override) 

365 
 (parse_fact_refs >> only_fact_override) 

366 
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

367 
Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) 
57433  368 
no_fact_override 
35963  369 

370 
val _ = 

69593  371 
Outer_Syntax.command \<^command_keyword>\<open>sledgehammer\<close> 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

372 
"search for firstorder proof using automatic theorem provers" 
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
72400
diff
changeset

373 
(Scan.optional Parse.name runN  parse_raw_params 
60277
bcd9a70342be
sledgehammer panel operation reuses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
wenzelm
parents:
60276
diff
changeset

374 
 parse_fact_override  Scan.option Parse.nat >> 
60276  375 
(fn (((subcommand, params), fact_override), opt_i) => 
60277
bcd9a70342be
sledgehammer panel operation reuses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
wenzelm
parents:
60276
diff
changeset

376 
Toplevel.keep_proof 
bcd9a70342be
sledgehammer panel operation reuses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
wenzelm
parents:
60276
diff
changeset

377 
(hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) 
35963  378 
val _ = 
69593  379 
Outer_Syntax.command \<^command_keyword>\<open>sledgehammer_params\<close> 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

380 
"set and display the default parameters for Sledgehammer" 
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
72400
diff
changeset

381 
(parse_raw_params >> (fn params => 
60276  382 
Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => 
383 
writeln ("Default parameters for Sledgehammer:\n" ^ 

384 
(case rev (default_raw_params Normal thy) of 

385 
[] => "none" 

386 
 params => params > map string_of_raw_param > sort_strings > cat_lines)))))) 

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

387 

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

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

389 
let 
55205  390 
val thy = Proof.theory_of state 
43021  391 
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

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

393 
in 
60564  394 
run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) 
40931  395 
end 
39318  396 

69593  397 
val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\<open>auto_sledgehammer\<close>, try_sledgehammer)) 
39318  398 

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

399 
val _ = 
61223  400 
Query_Operation.register {name = sledgehammerN, pri = 0} 
401 
(fn {state = st, args, writeln_result, ...} => 

402 
(case try Toplevel.proof_of st of 

403 
SOME state => 

404 
let 

405 
val [provers_arg, isar_proofs_arg, try0_arg] = args 

406 
val override_params = 

407 
((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ 

408 
[("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), 

409 
("try0", [try0_arg]), 

410 
("debug", ["false"]), 

411 
("verbose", ["false"]), 

412 
("overlord", ["false"])]); 

413 
in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end 

414 
 NONE => error "Unknown proof context")) 

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

415 

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

416 
end; 