author | blanchet |
Fri, 02 Oct 2015 21:24:37 +0200 | |
changeset 61315 | a48388351990 |
parent 60310 | 932221b62e89 |
child 61476 | 1884c40f1539 |
permissions | -rw-r--r-- |
55199 | 1 |
(* Title: HOL/Tools/Nitpick/nitpick_commands.ML |
33192 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
3 |
Copyright 2008, 2009, 2010 |
33192 | 4 |
|
5 |
Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer |
|
6 |
syntax. |
|
7 |
*) |
|
8 |
||
55199 | 9 |
signature NITPICK_COMMANDS = |
33192 | 10 |
sig |
11 |
type params = Nitpick.params |
|
12 |
||
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
13 |
val nitpickN : string |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
14 |
val nitpick_paramsN : string |
33192 | 15 |
val default_params : theory -> (string * string) list -> params |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35665
diff
changeset
|
16 |
end; |
33192 | 17 |
|
55203 | 18 |
structure Nitpick_Commands : NITPICK_COMMANDS = |
33192 | 19 |
struct |
20 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33220
diff
changeset
|
21 |
open Nitpick_Util |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33220
diff
changeset
|
22 |
open Nitpick_HOL |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33220
diff
changeset
|
23 |
open Nitpick_Rep |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33220
diff
changeset
|
24 |
open Nitpick_Nut |
33192 | 25 |
open Nitpick |
26 |
||
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
27 |
val nitpickN = "nitpick" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
28 |
val nitpick_paramsN = "nitpick_params" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
29 |
|
39344 | 30 |
(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share |
31 |
its time slot with several other automatic tools. *) |
|
43022 | 32 |
val auto_try_max_scopes = 6 |
39344 | 33 |
|
33192 | 34 |
type raw_param = string * string list |
35 |
||
36 |
val default_default_params = |
|
42959 | 37 |
[("card", "1\<emdash>10"), |
38180
7a88032f9265
bump up the max cardinalities, to use up more of the time given to us by the user
blanchet
parents:
38127
diff
changeset
|
38 |
("iter", "0,1,2,4,8,12,16,20,24,28"), |
49618
29be73b789f9
lower the defaults for the number of bits, based on an example by Lukas Bulwahn
blanchet
parents:
46961
diff
changeset
|
39 |
("bits", "1\<emdash>10"), |
38180
7a88032f9265
bump up the max cardinalities, to use up more of the time given to us by the user
blanchet
parents:
38127
diff
changeset
|
40 |
("bisim_depth", "9"), |
35964 | 41 |
("box", "smart"), |
42 |
("finitize", "smart"), |
|
43 |
("mono", "smart"), |
|
44 |
("wf", "smart"), |
|
45 |
("sat_solver", "smart"), |
|
46 |
("batch_size", "smart"), |
|
47 |
("falsify", "true"), |
|
48 |
("user_axioms", "smart"), |
|
49 |
("assms", "true"), |
|
50 |
("merge_type_vars", "false"), |
|
51 |
("binary_ints", "smart"), |
|
52 |
("destroy_constrs", "true"), |
|
53 |
("specialize", "true"), |
|
54 |
("star_linear_preds", "true"), |
|
41856 | 55 |
("total_consts", "smart"), |
35964 | 56 |
("peephole_optim", "true"), |
38127 | 57 |
("datatype_sym_break", "5"), |
58 |
("kodkod_sym_break", "15"), |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39359
diff
changeset
|
59 |
("timeout", "30"), |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39359
diff
changeset
|
60 |
("tac_timeout", "0.5"), |
35964 | 61 |
("max_threads", "0"), |
62 |
("debug", "false"), |
|
63 |
("verbose", "false"), |
|
64 |
("overlord", "false"), |
|
53802 | 65 |
("spy", "false"), |
55889 | 66 |
("show_types", "false"), |
41993
bd6296de1432
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents:
41876
diff
changeset
|
67 |
("show_skolems", "true"), |
35964 | 68 |
("show_consts", "false"), |
69 |
("format", "1"), |
|
70 |
("max_potential", "1"), |
|
60310 | 71 |
("max_genuine", "1")] |
33192 | 72 |
|
73 |
val negated_params = |
|
74 |
[("dont_box", "box"), |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
75 |
("dont_finitize", "finitize"), |
33192 | 76 |
("non_mono", "mono"), |
77 |
("non_wf", "wf"), |
|
78 |
("satisfy", "falsify"), |
|
79 |
("no_user_axioms", "user_axioms"), |
|
80 |
("no_assms", "assms"), |
|
33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33232
diff
changeset
|
81 |
("dont_merge_type_vars", "merge_type_vars"), |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
82 |
("unary_ints", "binary_ints"), |
33192 | 83 |
("dont_destroy_constrs", "destroy_constrs"), |
84 |
("dont_specialize", "specialize"), |
|
85 |
("dont_star_linear_preds", "star_linear_preds"), |
|
41856 | 86 |
("partial_consts", "total_consts"), |
33192 | 87 |
("no_peephole_optim", "peephole_optim"), |
35964 | 88 |
("no_debug", "debug"), |
33192 | 89 |
("quiet", "verbose"), |
90 |
("no_overlord", "overlord"), |
|
53802 | 91 |
("dont_spy", "spy"), |
55889 | 92 |
("hide_types", "show_types"), |
41993
bd6296de1432
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents:
41876
diff
changeset
|
93 |
("hide_skolems", "show_skolems"), |
60310 | 94 |
("hide_consts", "show_consts")] |
33192 | 95 |
|
96 |
fun is_known_raw_param s = |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
97 |
AList.defined (op =) default_default_params s orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
98 |
AList.defined (op =) negated_params s orelse |
41876 | 99 |
member (op =) ["max", "show_all", "whack", "eval", "need", "atoms", |
100 |
"expect"] s orelse |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
101 |
exists (fn p => String.isPrefix (p ^ " ") s) |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
102 |
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", |
55888 | 103 |
"mono", "non_mono", "wf", "non_wf", "format", "atoms"] |
33192 | 104 |
|
105 |
fun check_raw_param (s, _) = |
|
106 |
if is_known_raw_param s then () |
|
39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
39155
diff
changeset
|
107 |
else error ("Unknown parameter: " ^ quote s ^ ".") |
33192 | 108 |
|
109 |
fun unnegate_param_name name = |
|
110 |
case AList.lookup (op =) negated_params name of |
|
111 |
NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name) |
|
112 |
else if String.isPrefix "non_" name then SOME (unprefix "non_" name) |
|
113 |
else NONE |
|
114 |
| some_name => some_name |
|
55889 | 115 |
|
37169
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
116 |
fun normalize_raw_param (name, value) = |
33192 | 117 |
case unnegate_param_name name of |
37169
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
118 |
SOME name' => [(name', case value of |
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
119 |
["false"] => ["true"] |
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
120 |
| ["true"] => ["false"] |
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
121 |
| [] => ["false"] |
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
122 |
| _ => value)] |
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
123 |
| NONE => if name = "show_all" then |
55889 | 124 |
[("show_types", value), ("show_skolems", value), |
41993
bd6296de1432
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents:
41876
diff
changeset
|
125 |
("show_consts", value)] |
37169
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
126 |
else |
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
127 |
[(name, value)] |
33192 | 128 |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40931
diff
changeset
|
129 |
structure Data = Theory_Data |
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40931
diff
changeset
|
130 |
( |
35964 | 131 |
type T = raw_param list |
54546
8b403a7a8c44
fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet
parents:
53802
diff
changeset
|
132 |
val empty = default_default_params |> map (apsnd single) |
33192 | 133 |
val extend = I |
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40931
diff
changeset
|
134 |
fun merge data = AList.merge (op =) (K true) data |
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40931
diff
changeset
|
135 |
) |
33192 | 136 |
|
37169
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
137 |
val set_default_raw_param = |
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
138 |
Data.map o fold (AList.update (op =)) o normalize_raw_param |
35964 | 139 |
val default_raw_params = Data.get |
33192 | 140 |
|
42959 | 141 |
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>") |
33192 | 142 |
|
143 |
fun stringify_raw_param_value [] = "" |
|
144 |
| stringify_raw_param_value [s] = s |
|
145 |
| stringify_raw_param_value (s1 :: s2 :: ss) = |
|
146 |
s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^ |
|
147 |
stringify_raw_param_value (s2 :: ss) |
|
148 |
||
149 |
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s)) |
|
150 |
||
43022 | 151 |
fun extract_params ctxt mode default_params override_params = |
33192 | 152 |
let |
37169
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
153 |
val override_params = maps normalize_raw_param override_params |
33192 | 154 |
val raw_params = rev override_params @ rev default_params |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
155 |
val raw_lookup = AList.lookup (op =) raw_params |
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
156 |
val lookup = Option.map stringify_raw_param_value o raw_lookup |
35964 | 157 |
val lookup_string = the_default "" o lookup |
158 |
fun general_lookup_bool option default_value name = |
|
159 |
case lookup name of |
|
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35968
diff
changeset
|
160 |
SOME s => parse_bool_option option name s |
35964 | 161 |
| NONE => default_value |
162 |
val lookup_bool = the o general_lookup_bool false (SOME false) |
|
163 |
val lookup_bool_option = general_lookup_bool true NONE |
|
33192 | 164 |
fun do_int name value = |
165 |
case value of |
|
166 |
SOME s => (case Int.fromString s of |
|
167 |
SOME i => i |
|
168 |
| NONE => error ("Parameter " ^ quote name ^ |
|
169 |
" must be assigned an integer value.")) |
|
170 |
| NONE => 0 |
|
171 |
fun lookup_int name = do_int name (lookup name) |
|
172 |
fun lookup_int_option name = |
|
173 |
case lookup name of |
|
174 |
SOME "smart" => NONE |
|
175 |
| value => SOME (do_int name value) |
|
176 |
fun int_range_from_string name min_int s = |
|
177 |
let |
|
178 |
val (k1, k2) = |
|
179 |
(case space_explode "-" s of |
|
42959 | 180 |
[s] => the_default (s, s) (first_field "\<emdash>" s) |
33192 | 181 |
| ["", s2] => ("-" ^ s2, "-" ^ s2) |
182 |
| [s1, s2] => (s1, s2) |
|
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51557
diff
changeset
|
183 |
| _ => raise Option.Option) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
184 |
|> apply2 (maxed_int_from_string min_int) |
33192 | 185 |
in if k1 <= k2 then k1 upto k2 else k1 downto k2 end |
186 |
handle Option.Option => |
|
187 |
error ("Parameter " ^ quote name ^ |
|
188 |
" must be assigned a sequence of integers.") |
|
189 |
fun int_seq_from_string name min_int s = |
|
190 |
maps (int_range_from_string name min_int) (space_explode "," s) |
|
191 |
fun lookup_int_seq name min_int = |
|
192 |
case lookup name of |
|
193 |
SOME s => (case int_seq_from_string name min_int s of |
|
194 |
[] => [min_int] |
|
195 |
| value => value) |
|
196 |
| NONE => [min_int] |
|
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
197 |
fun lookup_assigns read prefix default convert = |
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
198 |
(NONE, convert (the_default default (lookup prefix))) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
199 |
:: map (fn (name, value) => |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
200 |
(SOME (read (String.extract (name, size prefix + 1, NONE))), |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
201 |
convert (stringify_raw_param_value value))) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
202 |
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params) |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
203 |
fun lookup_ints_assigns read prefix min_int = |
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
204 |
lookup_assigns read prefix (signed_string_of_int min_int) |
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
205 |
(int_seq_from_string prefix min_int) |
33192 | 206 |
fun lookup_bool_option_assigns read prefix = |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
207 |
lookup_assigns read prefix "" (parse_bool_option true prefix) |
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
208 |
fun lookup_strings_assigns read prefix = |
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
209 |
lookup_assigns read prefix "" (space_explode " ") |
33192 | 210 |
fun lookup_time name = |
211 |
case lookup name of |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
212 |
SOME s => parse_time name s |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
213 |
| NONE => Time.zeroTime |
33192 | 214 |
val read_type_polymorphic = |
215 |
Syntax.read_typ ctxt #> Logic.mk_type |
|
216 |
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type |
|
217 |
val read_term_polymorphic = |
|
218 |
Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt) |
|
41876 | 219 |
val lookup_term_list_option_polymorphic = |
220 |
AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic) |
|
33192 | 221 |
val read_const_polymorphic = read_term_polymorphic #> dest_Const |
43022 | 222 |
val cards_assigns = |
223 |
lookup_ints_assigns read_type_polymorphic "card" 1 |
|
224 |
|> mode = Auto_Try ? map (apsnd (take auto_try_max_scopes)) |
|
33192 | 225 |
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 |
226 |
val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0 |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
227 |
val bitss = lookup_int_seq "bits" 1 |
33192 | 228 |
val bisim_depths = lookup_int_seq "bisim_depth" ~1 |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
229 |
val boxes = lookup_bool_option_assigns read_type_polymorphic "box" |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
230 |
val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize" |
43022 | 231 |
val monos = if mode = Auto_Try then [(NONE, SOME true)] |
39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
39155
diff
changeset
|
232 |
else lookup_bool_option_assigns read_type_polymorphic "mono" |
33192 | 233 |
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf" |
234 |
val sat_solver = lookup_string "sat_solver" |
|
235 |
val falsify = lookup_bool "falsify" |
|
43022 | 236 |
val debug = (mode <> Auto_Try andalso lookup_bool "debug") |
237 |
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") |
|
33192 | 238 |
val overlord = lookup_bool "overlord" |
54546
8b403a7a8c44
fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet
parents:
53802
diff
changeset
|
239 |
val spy = getenv "NITPICK_SPY" = "yes" orelse lookup_bool "spy" |
33192 | 240 |
val user_axioms = lookup_bool_option "user_axioms" |
241 |
val assms = lookup_bool "assms" |
|
41876 | 242 |
val whacks = lookup_term_list_option_polymorphic "whack" |> these |
33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33232
diff
changeset
|
243 |
val merge_type_vars = lookup_bool "merge_type_vars" |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
244 |
val binary_ints = lookup_bool_option "binary_ints" |
33192 | 245 |
val destroy_constrs = lookup_bool "destroy_constrs" |
246 |
val specialize = lookup_bool "specialize" |
|
247 |
val star_linear_preds = lookup_bool "star_linear_preds" |
|
41856 | 248 |
val total_consts = lookup_bool_option "total_consts" |
41876 | 249 |
val needs = lookup_term_list_option_polymorphic "need" |
33192 | 250 |
val peephole_optim = lookup_bool "peephole_optim" |
38124 | 251 |
val datatype_sym_break = lookup_int "datatype_sym_break" |
252 |
val kodkod_sym_break = lookup_int "kodkod_sym_break" |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54546
diff
changeset
|
253 |
val timeout = lookup_time "timeout" |
33192 | 254 |
val tac_timeout = lookup_time "tac_timeout" |
43022 | 255 |
val max_threads = |
256 |
if mode = Normal then Int.max (0, lookup_int "max_threads") else 1 |
|
55889 | 257 |
val show_types = debug orelse lookup_bool "show_types" |
41993
bd6296de1432
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents:
41876
diff
changeset
|
258 |
val show_skolems = debug orelse lookup_bool "show_skolems" |
37169
f69efa106feb
make Nitpick "show_all" option behave less surprisingly
blanchet
parents:
36960
diff
changeset
|
259 |
val show_consts = debug orelse lookup_bool "show_consts" |
41876 | 260 |
val evals = lookup_term_list_option_polymorphic "eval" |> these |
33192 | 261 |
val formats = lookup_ints_assigns read_term_polymorphic "format" 0 |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37213
diff
changeset
|
262 |
val atomss = lookup_strings_assigns read_type_polymorphic "atoms" |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
263 |
val max_potential = |
43032 | 264 |
if mode = Normal then Int.max (0, lookup_int "max_potential") else 0 |
33192 | 265 |
val max_genuine = Int.max (0, lookup_int "max_genuine") |
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset
|
266 |
val batch_size = |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset
|
267 |
case lookup_int_option "batch_size" of |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset
|
268 |
SOME n => Int.max (1, n) |
38180
7a88032f9265
bump up the max cardinalities, to use up more of the time given to us by the user
blanchet
parents:
38127
diff
changeset
|
269 |
| NONE => if debug then 1 else 50 |
33192 | 270 |
val expect = lookup_string "expect" |
271 |
in |
|
55888 | 272 |
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, |
273 |
iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, |
|
274 |
boxes = boxes, finitizes = finitizes, monos = monos, wfs = wfs, |
|
61315
a48388351990
removed Nitpick nonblocking mode, that was never really used
blanchet
parents:
60310
diff
changeset
|
275 |
sat_solver = sat_solver, falsify = falsify, debug = debug, |
a48388351990
removed Nitpick nonblocking mode, that was never really used
blanchet
parents:
60310
diff
changeset
|
276 |
verbose = verbose, overlord = overlord, spy = spy, |
55888 | 277 |
user_axioms = user_axioms, assms = assms, whacks = whacks, |
278 |
merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
|
279 |
destroy_constrs = destroy_constrs, specialize = specialize, |
|
280 |
star_linear_preds = star_linear_preds, total_consts = total_consts, |
|
281 |
needs = needs, peephole_optim = peephole_optim, |
|
282 |
datatype_sym_break = datatype_sym_break, |
|
283 |
kodkod_sym_break = kodkod_sym_break, timeout = timeout, |
|
284 |
tac_timeout = tac_timeout, max_threads = max_threads, |
|
55889 | 285 |
show_types = show_types, show_skolems = show_skolems, |
55888 | 286 |
show_consts = show_consts, evals = evals, formats = formats, |
287 |
atomss = atomss, max_potential = max_potential, max_genuine = max_genuine, |
|
288 |
batch_size = batch_size, expect = expect} |
|
33192 | 289 |
end |
290 |
||
291 |
fun default_params thy = |
|
43022 | 292 |
extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy) |
33192 | 293 |
o map (apsnd single) |
294 |
||
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
295 |
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " |
35964 | 296 |
val parse_value = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
297 |
Scan.repeat1 (Parse.minus >> single |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39359
diff
changeset
|
298 |
|| Scan.repeat1 (Scan.unless Parse.minus |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39359
diff
changeset
|
299 |
(Parse.name || Parse.float_number)) |
46949 | 300 |
|| @{keyword ","} |-- Parse.number >> prefix "," >> single) |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39359
diff
changeset
|
301 |
>> flat |
46949 | 302 |
val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) [] |
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
303 |
val parse_params = |
46949 | 304 |
Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) [] |
33192 | 305 |
|
306 |
fun handle_exceptions ctxt f x = |
|
307 |
f x |
|
308 |
handle ARG (loc, details) => |
|
309 |
error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".") |
|
310 |
| BAD (loc, details) => |
|
311 |
error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".") |
|
312 |
| NOT_SUPPORTED details => |
|
313 |
(warning ("Unsupported case: " ^ details ^ "."); x) |
|
314 |
| NUT (loc, us) => |
|
315 |
error ("Invalid intermediate term" ^ plural_s_for_list us ^ |
|
316 |
" (" ^ quote loc ^ "): " ^ |
|
317 |
commas (map (string_for_nut ctxt) us) ^ ".") |
|
318 |
| REP (loc, Rs) => |
|
319 |
error ("Invalid representation" ^ plural_s_for_list Rs ^ |
|
320 |
" (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".") |
|
321 |
| TERM (loc, ts) => |
|
322 |
error ("Invalid term" ^ plural_s_for_list ts ^ |
|
323 |
" (" ^ quote loc ^ "): " ^ |
|
324 |
commas (map (Syntax.string_of_term ctxt) ts) ^ ".") |
|
325 |
| TYPE (loc, Ts, ts) => |
|
326 |
error ("Invalid type" ^ plural_s_for_list Ts ^ |
|
327 |
(if null ts then |
|
328 |
"" |
|
329 |
else |
|
330 |
" for term" ^ plural_s_for_list ts ^ " " ^ |
|
331 |
commas (map (quote o Syntax.string_of_term ctxt) ts)) ^ |
|
332 |
" (" ^ quote loc ^ "): " ^ |
|
333 |
commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".") |
|
334 |
||
43022 | 335 |
fun pick_nits override_params mode i step state = |
33192 | 336 |
let |
337 |
val thy = Proof.theory_of state |
|
338 |
val ctxt = Proof.context_of state |
|
339 |
val _ = List.app check_raw_param override_params |
|
61315
a48388351990
removed Nitpick nonblocking mode, that was never really used
blanchet
parents:
60310
diff
changeset
|
340 |
val params as {debug, ...} = |
43022 | 341 |
extract_params ctxt mode (default_raw_params thy) override_params |
33192 | 342 |
fun go () = |
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents:
58842
diff
changeset
|
343 |
(unknownN, []) |
43022 | 344 |
|> (if mode = Auto_Try then perhaps o try |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
345 |
else if debug then fn f => fn x => f x |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
346 |
else handle_exceptions ctxt) |
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents:
58842
diff
changeset
|
347 |
(fn _ => pick_nits_in_subgoal state params mode i step) |
61315
a48388351990
removed Nitpick nonblocking mode, that was never really used
blanchet
parents:
60310
diff
changeset
|
348 |
in go () end |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
349 |
|> `(fn (outcome_code, _) => outcome_code = genuineN) |
33192 | 350 |
|
351 |
fun string_for_raw_param (name, value) = |
|
352 |
name ^ " = " ^ stringify_raw_param_value value |
|
353 |
||
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
354 |
fun nitpick_params_trans params = |
33192 | 355 |
Toplevel.theory |
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
356 |
(fold set_default_raw_param params |
39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
39155
diff
changeset
|
357 |
#> tap (fn thy => |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
358 |
writeln ("Default parameters for Nitpick:\n" ^ |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
359 |
(case rev (default_raw_params thy) of |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
360 |
[] => "none" |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
361 |
| params => |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
362 |
(map check_raw_param params; |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
363 |
params |> map string_for_raw_param |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
364 |
|> sort_strings |> cat_lines))))) |
33192 | 365 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
366 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59058
diff
changeset
|
367 |
Outer_Syntax.command @{command_keyword nitpick} |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
368 |
"try to find a counterexample for a given subgoal using Nitpick" |
51557
4e4b56b7a3a5
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents:
49985
diff
changeset
|
369 |
(parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) => |
60190
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60094
diff
changeset
|
370 |
Toplevel.keep_proof (fn state => |
51557
4e4b56b7a3a5
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents:
49985
diff
changeset
|
371 |
ignore (pick_nits params Normal i (Toplevel.proof_position_of state) |
4e4b56b7a3a5
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents:
49985
diff
changeset
|
372 |
(Toplevel.proof_of state))))) |
33192 | 373 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
374 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59058
diff
changeset
|
375 |
Outer_Syntax.command @{command_keyword nitpick_params} |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
376 |
"set and display the default parameters for Nitpick" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
377 |
(parse_params #>> nitpick_params_trans) |
33192 | 378 |
|
43022 | 379 |
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0 |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
380 |
|
56467 | 381 |
val _ = Try.tool_setup (nitpickN, (50, @{system_option auto_nitpick}, try_nitpick)) |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
382 |
|
33192 | 383 |
end; |