author | blanchet |
Fri, 23 Apr 2010 19:18:39 +0200 | |
changeset 36380 | 1e8fcaccb3e8 |
parent 35968 | b7f98ff9c7d9 |
child 36385 | ff5f88702590 |
permissions | -rw-r--r-- |
33982 | 1 |
(* Title: HOL/Tools/Nitpick/nitpick_isar.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 |
||
9 |
signature NITPICK_ISAR = |
|
10 |
sig |
|
11 |
type params = Nitpick.params |
|
12 |
||
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
13 |
val auto: bool Unsynchronized.ref |
33192 | 14 |
val default_params : theory -> (string * string) list -> params |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
15 |
val setup : theory -> theory |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35665
diff
changeset
|
16 |
end; |
33192 | 17 |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33220
diff
changeset
|
18 |
structure Nitpick_Isar : NITPICK_ISAR = |
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 |
||
35964 | 27 |
structure K = OuterKeyword and P = OuterParse |
28 |
||
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
29 |
val auto = Unsynchronized.ref false; |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
30 |
|
33601
4608243edcfc
plain add_preference, no setmp_CRITICAL required;
wenzelm
parents:
33599
diff
changeset
|
31 |
val _ = |
4608243edcfc
plain add_preference, no setmp_CRITICAL required;
wenzelm
parents:
33599
diff
changeset
|
32 |
ProofGeneralPgip.add_preference Preferences.category_tracing |
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
|
33 |
(Preferences.bool_pref auto "auto-nitpick" |
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
|
34 |
"Whether to run Nitpick automatically.") |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
35 |
|
33192 | 36 |
type raw_param = string * string list |
37 |
||
38 |
val default_default_params = |
|
35964 | 39 |
[("card", "1\<midarrow>8"), |
40 |
("iter", "0,1,2,4,8,12,16,24"), |
|
41 |
("bits", "1,2,3,4,6,8,10,12"), |
|
42 |
("bisim_depth", "7"), |
|
43 |
("box", "smart"), |
|
44 |
("finitize", "smart"), |
|
45 |
("mono", "smart"), |
|
46 |
("std", "true"), |
|
47 |
("wf", "smart"), |
|
48 |
("sat_solver", "smart"), |
|
49 |
("batch_size", "smart"), |
|
50 |
("blocking", "true"), |
|
51 |
("falsify", "true"), |
|
52 |
("user_axioms", "smart"), |
|
53 |
("assms", "true"), |
|
54 |
("merge_type_vars", "false"), |
|
55 |
("binary_ints", "smart"), |
|
56 |
("destroy_constrs", "true"), |
|
57 |
("specialize", "true"), |
|
58 |
("skolemize", "true"), |
|
59 |
("star_linear_preds", "true"), |
|
60 |
("uncurry", "true"), |
|
61 |
("fast_descrs", "true"), |
|
62 |
("peephole_optim", "true"), |
|
63 |
("timeout", "30 s"), |
|
64 |
("tac_timeout", "500 ms"), |
|
65 |
("sym_break", "20"), |
|
66 |
("sharing_depth", "3"), |
|
67 |
("flatten_props", "false"), |
|
68 |
("max_threads", "0"), |
|
69 |
("debug", "false"), |
|
70 |
("verbose", "false"), |
|
71 |
("overlord", "false"), |
|
72 |
("show_all", "false"), |
|
73 |
("show_skolems", "true"), |
|
74 |
("show_datatypes", "false"), |
|
75 |
("show_consts", "false"), |
|
76 |
("format", "1"), |
|
77 |
("max_potential", "1"), |
|
78 |
("max_genuine", "1"), |
|
79 |
("check_potential", "false"), |
|
80 |
("check_genuine", "false")] |
|
33192 | 81 |
|
82 |
val negated_params = |
|
83 |
[("dont_box", "box"), |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
84 |
("dont_finitize", "finitize"), |
33192 | 85 |
("non_mono", "mono"), |
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
|
86 |
("non_std", "std"), |
33192 | 87 |
("non_wf", "wf"), |
88 |
("non_blocking", "blocking"), |
|
89 |
("satisfy", "falsify"), |
|
90 |
("no_user_axioms", "user_axioms"), |
|
91 |
("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
|
92 |
("dont_merge_type_vars", "merge_type_vars"), |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
93 |
("unary_ints", "binary_ints"), |
33192 | 94 |
("dont_destroy_constrs", "destroy_constrs"), |
95 |
("dont_specialize", "specialize"), |
|
96 |
("dont_skolemize", "skolemize"), |
|
97 |
("dont_star_linear_preds", "star_linear_preds"), |
|
98 |
("dont_uncurry", "uncurry"), |
|
99 |
("full_descrs", "fast_descrs"), |
|
100 |
("no_peephole_optim", "peephole_optim"), |
|
101 |
("dont_flatten_props", "flatten_props"), |
|
35964 | 102 |
("no_debug", "debug"), |
33192 | 103 |
("quiet", "verbose"), |
104 |
("no_overlord", "overlord"), |
|
105 |
("dont_show_all", "show_all"), |
|
106 |
("hide_skolems", "show_skolems"), |
|
107 |
("hide_datatypes", "show_datatypes"), |
|
108 |
("hide_consts", "show_consts"), |
|
109 |
("trust_potential", "check_potential"), |
|
110 |
("trust_genuine", "check_genuine")] |
|
111 |
||
112 |
(* string -> bool *) |
|
113 |
fun is_known_raw_param s = |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
114 |
AList.defined (op =) default_default_params s orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
115 |
AList.defined (op =) negated_params s orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
116 |
s = "max" orelse s = "eval" orelse s = "expect" orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
117 |
exists (fn p => String.isPrefix (p ^ " ") s) |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
118 |
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
119 |
"mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"] |
33192 | 120 |
|
121 |
(* string * 'a -> unit *) |
|
122 |
fun check_raw_param (s, _) = |
|
123 |
if is_known_raw_param s then () |
|
35964 | 124 |
else error ("Unknown parameter: " ^ quote s ^ ".") |
33192 | 125 |
|
126 |
(* string -> string option *) |
|
127 |
fun unnegate_param_name name = |
|
128 |
case AList.lookup (op =) negated_params name of |
|
129 |
NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name) |
|
130 |
else if String.isPrefix "non_" name then SOME (unprefix "non_" name) |
|
131 |
else NONE |
|
132 |
| some_name => some_name |
|
133 |
(* raw_param -> raw_param *) |
|
134 |
fun unnegate_raw_param (name, value) = |
|
135 |
case unnegate_param_name name of |
|
136 |
SOME name' => (name', case value of |
|
137 |
["false"] => ["true"] |
|
138 |
| ["true"] => ["false"] |
|
139 |
| [] => ["false"] |
|
140 |
| _ => value) |
|
141 |
| NONE => (name, value) |
|
142 |
||
33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset
|
143 |
structure Data = Theory_Data( |
35964 | 144 |
type T = raw_param list |
145 |
val empty = default_default_params |> map (apsnd single) |
|
33192 | 146 |
val extend = I |
35964 | 147 |
fun merge p : T = AList.merge (op =) (K true) p) |
33192 | 148 |
|
149 |
(* raw_param -> theory -> theory *) |
|
35964 | 150 |
val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param |
33192 | 151 |
(* theory -> raw_param list *) |
35964 | 152 |
val default_raw_params = Data.get |
33192 | 153 |
|
154 |
(* string -> bool *) |
|
155 |
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>") |
|
156 |
||
157 |
(* string list -> string *) |
|
158 |
fun stringify_raw_param_value [] = "" |
|
159 |
| stringify_raw_param_value [s] = s |
|
160 |
| stringify_raw_param_value (s1 :: s2 :: ss) = |
|
161 |
s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^ |
|
162 |
stringify_raw_param_value (s2 :: ss) |
|
163 |
||
164 |
(* int -> string -> int *) |
|
165 |
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s)) |
|
166 |
||
167 |
(* Proof.context -> bool -> raw_param list -> raw_param list -> params *) |
|
168 |
fun extract_params ctxt auto default_params override_params = |
|
169 |
let |
|
170 |
val override_params = map unnegate_raw_param override_params |
|
171 |
val raw_params = rev override_params @ rev default_params |
|
35964 | 172 |
(* string -> string *) |
33192 | 173 |
val lookup = |
174 |
Option.map stringify_raw_param_value o AList.lookup (op =) raw_params |
|
35964 | 175 |
val lookup_string = the_default "" o lookup |
176 |
(* bool -> bool option -> string -> bool option *) |
|
177 |
fun general_lookup_bool option default_value name = |
|
178 |
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
|
179 |
SOME s => parse_bool_option option name s |
35964 | 180 |
| NONE => default_value |
33192 | 181 |
(* string -> bool *) |
35964 | 182 |
val lookup_bool = the o general_lookup_bool false (SOME false) |
33192 | 183 |
(* string -> bool option *) |
35964 | 184 |
val lookup_bool_option = general_lookup_bool true NONE |
33192 | 185 |
(* string -> string option -> int *) |
186 |
fun do_int name value = |
|
187 |
case value of |
|
188 |
SOME s => (case Int.fromString s of |
|
189 |
SOME i => i |
|
190 |
| NONE => error ("Parameter " ^ quote name ^ |
|
191 |
" must be assigned an integer value.")) |
|
192 |
| NONE => 0 |
|
193 |
(* string -> int *) |
|
194 |
fun lookup_int name = do_int name (lookup name) |
|
195 |
(* string -> int option *) |
|
196 |
fun lookup_int_option name = |
|
197 |
case lookup name of |
|
198 |
SOME "smart" => NONE |
|
199 |
| value => SOME (do_int name value) |
|
200 |
(* string -> int -> string -> int list *) |
|
201 |
fun int_range_from_string name min_int s = |
|
202 |
let |
|
203 |
val (k1, k2) = |
|
204 |
(case space_explode "-" s of |
|
205 |
[s] => the_default (s, s) (first_field "\<midarrow>" s) |
|
206 |
| ["", s2] => ("-" ^ s2, "-" ^ s2) |
|
207 |
| [s1, s2] => (s1, s2) |
|
208 |
| _ => raise Option) |
|
209 |
|> pairself (maxed_int_from_string min_int) |
|
210 |
in if k1 <= k2 then k1 upto k2 else k1 downto k2 end |
|
211 |
handle Option.Option => |
|
212 |
error ("Parameter " ^ quote name ^ |
|
213 |
" must be assigned a sequence of integers.") |
|
214 |
(* string -> int -> string -> int list *) |
|
215 |
fun int_seq_from_string name min_int s = |
|
216 |
maps (int_range_from_string name min_int) (space_explode "," s) |
|
217 |
(* string -> int -> int list *) |
|
218 |
fun lookup_int_seq name min_int = |
|
219 |
case lookup name of |
|
220 |
SOME s => (case int_seq_from_string name min_int s of |
|
221 |
[] => [min_int] |
|
222 |
| value => value) |
|
223 |
| NONE => [min_int] |
|
224 |
(* (string -> 'a) -> int -> string -> ('a option * int list) list *) |
|
225 |
fun lookup_ints_assigns read prefix min_int = |
|
226 |
(NONE, lookup_int_seq prefix min_int) |
|
227 |
:: map (fn (name, value) => |
|
228 |
(SOME (read (String.extract (name, size prefix + 1, NONE))), |
|
229 |
value |> stringify_raw_param_value |
|
230 |
|> int_seq_from_string name min_int)) |
|
231 |
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params) |
|
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
|
232 |
(* (string -> 'a) -> string -> ('a option * bool) list *) |
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
|
233 |
fun lookup_bool_assigns read prefix = |
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
|
234 |
(NONE, lookup_bool prefix) |
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
|
235 |
:: 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
|
236 |
(SOME (read (String.extract (name, size prefix + 1, NONE))), |
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
|
237 |
value |> stringify_raw_param_value |
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
|
238 |
|> parse_bool_option false name |> the)) |
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
|
239 |
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params) |
33192 | 240 |
(* (string -> 'a) -> string -> ('a option * bool option) list *) |
241 |
fun lookup_bool_option_assigns read prefix = |
|
242 |
(NONE, lookup_bool_option prefix) |
|
243 |
:: map (fn (name, value) => |
|
244 |
(SOME (read (String.extract (name, size prefix + 1, NONE))), |
|
245 |
value |> stringify_raw_param_value |
|
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
|
246 |
|> parse_bool_option true name)) |
33192 | 247 |
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params) |
248 |
(* string -> Time.time option *) |
|
249 |
fun lookup_time name = |
|
250 |
case lookup name of |
|
251 |
NONE => NONE |
|
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
|
252 |
| SOME s => parse_time_option name s |
33192 | 253 |
(* string -> term list *) |
254 |
val lookup_term_list = |
|
255 |
AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt |
|
256 |
val read_type_polymorphic = |
|
257 |
Syntax.read_typ ctxt #> Logic.mk_type |
|
258 |
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type |
|
259 |
(* string -> term *) |
|
260 |
val read_term_polymorphic = |
|
261 |
Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt) |
|
262 |
(* string -> styp *) |
|
263 |
val read_const_polymorphic = read_term_polymorphic #> dest_Const |
|
264 |
val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 |
|
265 |
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 |
|
266 |
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
|
267 |
val bitss = lookup_int_seq "bits" 1 |
33192 | 268 |
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
|
269 |
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
|
270 |
val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize" |
33192 | 271 |
val monos = lookup_bool_option_assigns read_type_polymorphic "mono" |
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
|
272 |
val stds = lookup_bool_assigns read_type_polymorphic "std" |
33192 | 273 |
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf" |
274 |
val sat_solver = lookup_string "sat_solver" |
|
275 |
val blocking = not auto andalso lookup_bool "blocking" |
|
276 |
val falsify = lookup_bool "falsify" |
|
277 |
val debug = not auto andalso lookup_bool "debug" |
|
278 |
val verbose = debug orelse (not auto andalso lookup_bool "verbose") |
|
279 |
val overlord = lookup_bool "overlord" |
|
280 |
val user_axioms = lookup_bool_option "user_axioms" |
|
281 |
val assms = lookup_bool "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
|
282 |
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
|
283 |
val binary_ints = lookup_bool_option "binary_ints" |
33192 | 284 |
val destroy_constrs = lookup_bool "destroy_constrs" |
285 |
val specialize = lookup_bool "specialize" |
|
286 |
val skolemize = lookup_bool "skolemize" |
|
287 |
val star_linear_preds = lookup_bool "star_linear_preds" |
|
288 |
val uncurry = lookup_bool "uncurry" |
|
289 |
val fast_descrs = lookup_bool "fast_descrs" |
|
290 |
val peephole_optim = lookup_bool "peephole_optim" |
|
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
291 |
val timeout = if auto then NONE else lookup_time "timeout" |
33192 | 292 |
val tac_timeout = lookup_time "tac_timeout" |
293 |
val sym_break = Int.max (0, lookup_int "sym_break") |
|
294 |
val sharing_depth = Int.max (1, lookup_int "sharing_depth") |
|
295 |
val flatten_props = lookup_bool "flatten_props" |
|
296 |
val max_threads = Int.max (0, lookup_int "max_threads") |
|
297 |
val show_all = debug orelse lookup_bool "show_all" |
|
298 |
val show_skolems = show_all orelse lookup_bool "show_skolems" |
|
299 |
val show_datatypes = show_all orelse lookup_bool "show_datatypes" |
|
300 |
val show_consts = show_all orelse lookup_bool "show_consts" |
|
301 |
val formats = lookup_ints_assigns read_term_polymorphic "format" 0 |
|
302 |
val evals = lookup_term_list "eval" |
|
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
303 |
val max_potential = |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
304 |
if auto then 0 else Int.max (0, lookup_int "max_potential") |
33192 | 305 |
val max_genuine = Int.max (0, lookup_int "max_genuine") |
306 |
val check_potential = lookup_bool "check_potential" |
|
307 |
val check_genuine = lookup_bool "check_genuine" |
|
308 |
val batch_size = case lookup_int_option "batch_size" of |
|
309 |
SOME n => Int.max (1, n) |
|
310 |
| NONE => if debug then 1 else 64 |
|
311 |
val expect = lookup_string "expect" |
|
312 |
in |
|
313 |
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
314 |
iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
315 |
boxes = boxes, finitizes = finitizes, monos = monos, stds = stds, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35280
diff
changeset
|
316 |
wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify, |
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
|
317 |
debug = debug, verbose = verbose, overlord = overlord, |
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
|
318 |
user_axioms = user_axioms, assms = assms, |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
319 |
merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
320 |
destroy_constrs = destroy_constrs, specialize = specialize, |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
321 |
skolemize = skolemize, star_linear_preds = star_linear_preds, |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
322 |
uncurry = uncurry, fast_descrs = fast_descrs, |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
323 |
peephole_optim = peephole_optim, timeout = timeout, |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
324 |
tac_timeout = tac_timeout, sym_break = sym_break, |
33192 | 325 |
sharing_depth = sharing_depth, flatten_props = flatten_props, |
326 |
max_threads = max_threads, show_skolems = show_skolems, |
|
327 |
show_datatypes = show_datatypes, show_consts = show_consts, |
|
328 |
formats = formats, evals = evals, max_potential = max_potential, |
|
329 |
max_genuine = max_genuine, check_potential = check_potential, |
|
330 |
check_genuine = check_genuine, batch_size = batch_size, expect = expect} |
|
331 |
end |
|
332 |
||
333 |
(* theory -> (string * string) list -> params *) |
|
334 |
fun default_params thy = |
|
335 |
extract_params (ProofContext.init thy) false (default_raw_params thy) |
|
336 |
o map (apsnd single) |
|
337 |
||
35964 | 338 |
(* P.token list -> string * P.token list *) |
339 |
val parse_key = Scan.repeat1 P.typ_group >> space_implode " " |
|
340 |
(* P.token list -> string list * P.token list *) |
|
341 |
val parse_value = |
|
342 |
Scan.repeat1 (P.minus >> single |
|
343 |
|| Scan.repeat1 (Scan.unless P.minus P.name) |
|
344 |
|| P.$$$ "," |-- P.number >> prefix "," >> single) >> flat |
|
345 |
(* P.token list -> raw_param * P.token list *) |
|
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
346 |
val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) [] |
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
347 |
(* P.token list -> raw_param list * P.token list *) |
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
348 |
val parse_params = |
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
349 |
Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") [] |
33192 | 350 |
|
351 |
(* Proof.context -> ('a -> 'a) -> 'a -> 'a *) |
|
352 |
fun handle_exceptions ctxt f x = |
|
353 |
f x |
|
354 |
handle ARG (loc, details) => |
|
355 |
error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".") |
|
356 |
| BAD (loc, details) => |
|
357 |
error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".") |
|
358 |
| NOT_SUPPORTED details => |
|
359 |
(warning ("Unsupported case: " ^ details ^ "."); x) |
|
360 |
| NUT (loc, us) => |
|
361 |
error ("Invalid intermediate term" ^ plural_s_for_list us ^ |
|
362 |
" (" ^ quote loc ^ "): " ^ |
|
363 |
commas (map (string_for_nut ctxt) us) ^ ".") |
|
364 |
| REP (loc, Rs) => |
|
365 |
error ("Invalid representation" ^ plural_s_for_list Rs ^ |
|
366 |
" (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".") |
|
367 |
| TERM (loc, ts) => |
|
368 |
error ("Invalid term" ^ plural_s_for_list ts ^ |
|
369 |
" (" ^ quote loc ^ "): " ^ |
|
370 |
commas (map (Syntax.string_of_term ctxt) ts) ^ ".") |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
371 |
| TOO_LARGE (_, details) => |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
372 |
(warning ("Limit reached: " ^ details ^ "."); x) |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
373 |
| TOO_SMALL (_, details) => |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
374 |
(warning ("Limit reached: " ^ details ^ "."); x) |
33192 | 375 |
| TYPE (loc, Ts, ts) => |
376 |
error ("Invalid type" ^ plural_s_for_list Ts ^ |
|
377 |
(if null ts then |
|
378 |
"" |
|
379 |
else |
|
380 |
" for term" ^ plural_s_for_list ts ^ " " ^ |
|
381 |
commas (map (quote o Syntax.string_of_term ctxt) ts)) ^ |
|
382 |
" (" ^ quote loc ^ "): " ^ |
|
383 |
commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".") |
|
384 |
| Kodkod.SYNTAX (_, details) => |
|
385 |
(warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x) |
|
386 |
| Refute.REFUTE (loc, details) => |
|
387 |
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".") |
|
388 |
||
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
|
389 |
(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *) |
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
|
390 |
fun pick_nits override_params auto i step state = |
33192 | 391 |
let |
392 |
val thy = Proof.theory_of state |
|
393 |
val ctxt = Proof.context_of state |
|
394 |
val _ = List.app check_raw_param override_params |
|
395 |
val params as {blocking, debug, ...} = |
|
396 |
extract_params ctxt auto (default_raw_params thy) override_params |
|
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
397 |
(* unit -> bool * Proof.state *) |
33192 | 398 |
fun go () = |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
399 |
(false, state) |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
400 |
|> (if auto then perhaps o try |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
401 |
else if debug then fn f => fn x => f x |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
402 |
else handle_exceptions ctxt) |
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
|
403 |
(fn (_, state) => pick_nits_in_subgoal state params auto i step |
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
404 |
|>> curry (op =) "genuine") |
33192 | 405 |
in |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
406 |
if auto orelse blocking then go () |
33604
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33601
diff
changeset
|
407 |
else (Toplevel.thread true (fn () => (go (); ())); (false, state)) |
33192 | 408 |
end |
409 |
||
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
410 |
(* raw_param list * int -> Toplevel.transition -> Toplevel.transition *) |
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
411 |
fun nitpick_trans (params, i) = |
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
|
412 |
Toplevel.keep (fn st => |
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
413 |
(pick_nits params false i (Toplevel.proof_position_of st) |
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
414 |
(Toplevel.proof_of st); ())) |
33192 | 415 |
|
416 |
(* raw_param -> string *) |
|
417 |
fun string_for_raw_param (name, value) = |
|
418 |
name ^ " = " ^ stringify_raw_param_value value |
|
419 |
||
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
420 |
(* raw_param list -> Toplevel.transition -> Toplevel.transition *) |
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
421 |
fun nitpick_params_trans params = |
33192 | 422 |
Toplevel.theory |
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
423 |
(fold set_default_raw_param params |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
424 |
#> tap (fn thy => |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
425 |
writeln ("Default parameters for Nitpick:\n" ^ |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
426 |
(case rev (default_raw_params thy) of |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
427 |
[] => "none" |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
428 |
| params => |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
429 |
(map check_raw_param params; |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
430 |
params |> map string_for_raw_param |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
431 |
|> sort_strings |> cat_lines))))) |
33192 | 432 |
|
35964 | 433 |
(* P.token list |
434 |
-> (Toplevel.transition -> Toplevel.transition) * P.token list *) |
|
435 |
val parse_nitpick_command = |
|
35968
b7f98ff9c7d9
simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents:
35964
diff
changeset
|
436 |
(parse_params -- Scan.optional P.nat 1) #>> nitpick_trans |
35964 | 437 |
val parse_nitpick_params_command = parse_params #>> nitpick_params_trans |
33192 | 438 |
|
439 |
val _ = OuterSyntax.improper_command "nitpick" |
|
440 |
"try to find a counterexample for a given subgoal using Kodkod" |
|
35964 | 441 |
K.diag parse_nitpick_command |
33192 | 442 |
val _ = OuterSyntax.command "nitpick_params" |
443 |
"set and display the default parameters for Nitpick" |
|
35964 | 444 |
K.thy_decl parse_nitpick_params_command |
33192 | 445 |
|
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
446 |
(* Proof.state -> bool * Proof.state *) |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
447 |
fun auto_nitpick state = |
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
|
448 |
if not (!auto) then (false, state) else pick_nits [] true 1 0 state |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
449 |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
450 |
val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick) |
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset
|
451 |
|
33192 | 452 |
end; |