33192
|
1 |
(* Title: HOL/Nitpick/Tools/nitpick_isar.ML
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Copyright 2008, 2009
|
|
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 |
|
|
13 |
val default_params : theory -> (string * string) list -> params
|
|
14 |
end
|
|
15 |
|
|
16 |
structure NitpickIsar : NITPICK_ISAR =
|
|
17 |
struct
|
|
18 |
|
|
19 |
open NitpickUtil
|
|
20 |
open NitpickHOL
|
|
21 |
open NitpickRep
|
|
22 |
open NitpickNut
|
|
23 |
open Nitpick
|
|
24 |
|
|
25 |
type raw_param = string * string list
|
|
26 |
|
|
27 |
val default_default_params =
|
|
28 |
[("card", ["1\<midarrow>8"]),
|
|
29 |
("iter", ["0,1,2,4,8,12,16,24"]),
|
|
30 |
("bisim_depth", ["7"]),
|
|
31 |
("box", ["smart"]),
|
|
32 |
("mono", ["smart"]),
|
|
33 |
("wf", ["smart"]),
|
|
34 |
("sat_solver", ["smart"]),
|
|
35 |
("batch_size", ["smart"]),
|
|
36 |
("auto", ["false"]),
|
|
37 |
("blocking", ["true"]),
|
|
38 |
("falsify", ["true"]),
|
|
39 |
("user_axioms", ["smart"]),
|
|
40 |
("assms", ["true"]),
|
|
41 |
("coalesce_type_vars", ["false"]),
|
|
42 |
("destroy_constrs", ["true"]),
|
|
43 |
("specialize", ["true"]),
|
|
44 |
("skolemize", ["true"]),
|
|
45 |
("star_linear_preds", ["true"]),
|
|
46 |
("uncurry", ["true"]),
|
|
47 |
("fast_descrs", ["true"]),
|
|
48 |
("peephole_optim", ["true"]),
|
|
49 |
("timeout", ["30 s"]),
|
|
50 |
("auto_timeout", ["5 s"]),
|
|
51 |
("tac_timeout", ["500 ms"]),
|
|
52 |
("sym_break", ["20"]),
|
|
53 |
("sharing_depth", ["3"]),
|
|
54 |
("flatten_props", ["false"]),
|
|
55 |
("max_threads", ["0"]),
|
|
56 |
("verbose", ["false"]),
|
|
57 |
("debug", ["false"]),
|
|
58 |
("overlord", [if exists (fn s => String.isSuffix s (getenv "HOME"))
|
|
59 |
["blanchet", "blanchette"] then
|
|
60 |
"true"
|
|
61 |
else
|
|
62 |
"false"]),
|
|
63 |
("show_all", ["false"]),
|
|
64 |
("show_skolems", ["true"]),
|
|
65 |
("show_datatypes", ["false"]),
|
|
66 |
("show_consts", ["false"]),
|
|
67 |
("format", ["1"]),
|
|
68 |
("max_potential", ["1"]),
|
|
69 |
("max_genuine", ["1"]),
|
|
70 |
("check_potential", ["false"]),
|
|
71 |
("check_genuine", ["false"])]
|
|
72 |
|
|
73 |
val negated_params =
|
|
74 |
[("dont_box", "box"),
|
|
75 |
("non_mono", "mono"),
|
|
76 |
("non_wf", "wf"),
|
|
77 |
("no_auto", "auto"),
|
|
78 |
("non_blocking", "blocking"),
|
|
79 |
("satisfy", "falsify"),
|
|
80 |
("no_user_axioms", "user_axioms"),
|
|
81 |
("no_assms", "assms"),
|
|
82 |
("dont_coalesce_type_vars", "coalesce_type_vars"),
|
|
83 |
("dont_destroy_constrs", "destroy_constrs"),
|
|
84 |
("dont_specialize", "specialize"),
|
|
85 |
("dont_skolemize", "skolemize"),
|
|
86 |
("dont_star_linear_preds", "star_linear_preds"),
|
|
87 |
("dont_uncurry", "uncurry"),
|
|
88 |
("full_descrs", "fast_descrs"),
|
|
89 |
("no_peephole_optim", "peephole_optim"),
|
|
90 |
("dont_flatten_props", "flatten_props"),
|
|
91 |
("quiet", "verbose"),
|
|
92 |
("no_debug", "debug"),
|
|
93 |
("no_overlord", "overlord"),
|
|
94 |
("dont_show_all", "show_all"),
|
|
95 |
("hide_skolems", "show_skolems"),
|
|
96 |
("hide_datatypes", "show_datatypes"),
|
|
97 |
("hide_consts", "show_consts"),
|
|
98 |
("trust_potential", "check_potential"),
|
|
99 |
("trust_genuine", "check_genuine")]
|
|
100 |
|
|
101 |
(* string -> bool *)
|
|
102 |
fun is_known_raw_param s =
|
|
103 |
AList.defined (op =) default_default_params s
|
|
104 |
orelse AList.defined (op =) negated_params s
|
|
105 |
orelse s mem ["max", "eval", "expect"]
|
|
106 |
orelse exists (fn p => String.isPrefix (p ^ " ") s)
|
|
107 |
["card", "max", "iter", "box", "dont_box", "mono", "non_mono",
|
|
108 |
"wf", "non_wf", "format"]
|
|
109 |
|
|
110 |
(* string * 'a -> unit *)
|
|
111 |
fun check_raw_param (s, _) =
|
|
112 |
if is_known_raw_param s then ()
|
|
113 |
else error ("Unknown parameter " ^ quote s ^ ".")
|
|
114 |
|
|
115 |
(* string -> string option *)
|
|
116 |
fun unnegate_param_name name =
|
|
117 |
case AList.lookup (op =) negated_params name of
|
|
118 |
NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
|
|
119 |
else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
|
|
120 |
else NONE
|
|
121 |
| some_name => some_name
|
|
122 |
(* raw_param -> raw_param *)
|
|
123 |
fun unnegate_raw_param (name, value) =
|
|
124 |
case unnegate_param_name name of
|
|
125 |
SOME name' => (name', case value of
|
|
126 |
["false"] => ["true"]
|
|
127 |
| ["true"] => ["false"]
|
|
128 |
| [] => ["false"]
|
|
129 |
| _ => value)
|
|
130 |
| NONE => (name, value)
|
|
131 |
|
|
132 |
structure TheoryData = TheoryDataFun(
|
|
133 |
type T = {params: raw_param list, registered_auto: bool}
|
|
134 |
val empty = {params = rev default_default_params, registered_auto = false}
|
|
135 |
val copy = I
|
|
136 |
val extend = I
|
|
137 |
fun merge _ ({params = ps1, registered_auto = a1},
|
|
138 |
{params = ps2, registered_auto = a2}) =
|
|
139 |
{params = AList.merge (op =) (op =) (ps1, ps2),
|
|
140 |
registered_auto = a1 orelse a2})
|
|
141 |
|
|
142 |
(* raw_param -> theory -> theory *)
|
|
143 |
fun set_default_raw_param param thy =
|
|
144 |
let val {params, registered_auto} = TheoryData.get thy in
|
|
145 |
TheoryData.put
|
|
146 |
{params = AList.update (op =) (unnegate_raw_param param) params,
|
|
147 |
registered_auto = registered_auto} thy
|
|
148 |
end
|
|
149 |
(* theory -> raw_param list *)
|
|
150 |
val default_raw_params = #params o TheoryData.get
|
|
151 |
|
|
152 |
(* theory -> theory *)
|
|
153 |
fun set_registered_auto thy =
|
|
154 |
TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
|
|
155 |
(* theory -> bool *)
|
|
156 |
val is_registered_auto = #registered_auto o TheoryData.get
|
|
157 |
|
|
158 |
(* string -> bool *)
|
|
159 |
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
|
|
160 |
|
|
161 |
(* string list -> string *)
|
|
162 |
fun stringify_raw_param_value [] = ""
|
|
163 |
| stringify_raw_param_value [s] = s
|
|
164 |
| stringify_raw_param_value (s1 :: s2 :: ss) =
|
|
165 |
s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
|
|
166 |
stringify_raw_param_value (s2 :: ss)
|
|
167 |
|
|
168 |
(* bool -> string -> string -> bool option *)
|
|
169 |
fun bool_option_from_string option name s =
|
|
170 |
(case s of
|
|
171 |
"smart" => if option then NONE else raise Option
|
|
172 |
| "false" => SOME false
|
|
173 |
| "true" => SOME true
|
|
174 |
| "" => SOME true
|
|
175 |
| s => raise Option)
|
|
176 |
handle Option.Option =>
|
|
177 |
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
|
|
178 |
error ("Parameter " ^ quote name ^ " must be assigned " ^
|
|
179 |
space_implode " " (serial_commas "or" ss) ^ ".")
|
|
180 |
end
|
|
181 |
(* bool -> raw_param list -> bool option -> string -> bool option *)
|
|
182 |
fun general_lookup_bool option raw_params default_value name =
|
|
183 |
case AList.lookup (op =) raw_params name of
|
|
184 |
SOME s => s |> stringify_raw_param_value
|
|
185 |
|> bool_option_from_string option name
|
|
186 |
| NONE => default_value
|
|
187 |
|
|
188 |
(* int -> string -> int *)
|
|
189 |
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
|
|
190 |
|
|
191 |
(* Proof.context -> bool -> raw_param list -> raw_param list -> params *)
|
|
192 |
fun extract_params ctxt auto default_params override_params =
|
|
193 |
let
|
|
194 |
val override_params = map unnegate_raw_param override_params
|
|
195 |
val raw_params = rev override_params @ rev default_params
|
|
196 |
val lookup =
|
|
197 |
Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
|
|
198 |
(* string -> string *)
|
|
199 |
fun lookup_string name = the_default "" (lookup name)
|
|
200 |
(* string -> bool *)
|
|
201 |
val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
|
|
202 |
(* string -> bool option *)
|
|
203 |
val lookup_bool_option = general_lookup_bool true raw_params NONE
|
|
204 |
(* string -> string option -> int *)
|
|
205 |
fun do_int name value =
|
|
206 |
case value of
|
|
207 |
SOME s => (case Int.fromString s of
|
|
208 |
SOME i => i
|
|
209 |
| NONE => error ("Parameter " ^ quote name ^
|
|
210 |
" must be assigned an integer value."))
|
|
211 |
| NONE => 0
|
|
212 |
(* string -> int *)
|
|
213 |
fun lookup_int name = do_int name (lookup name)
|
|
214 |
(* string -> int option *)
|
|
215 |
fun lookup_int_option name =
|
|
216 |
case lookup name of
|
|
217 |
SOME "smart" => NONE
|
|
218 |
| value => SOME (do_int name value)
|
|
219 |
(* string -> int -> string -> int list *)
|
|
220 |
fun int_range_from_string name min_int s =
|
|
221 |
let
|
|
222 |
val (k1, k2) =
|
|
223 |
(case space_explode "-" s of
|
|
224 |
[s] => the_default (s, s) (first_field "\<midarrow>" s)
|
|
225 |
| ["", s2] => ("-" ^ s2, "-" ^ s2)
|
|
226 |
| [s1, s2] => (s1, s2)
|
|
227 |
| _ => raise Option)
|
|
228 |
|> pairself (maxed_int_from_string min_int)
|
|
229 |
in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
|
|
230 |
handle Option.Option =>
|
|
231 |
error ("Parameter " ^ quote name ^
|
|
232 |
" must be assigned a sequence of integers.")
|
|
233 |
(* string -> int -> string -> int list *)
|
|
234 |
fun int_seq_from_string name min_int s =
|
|
235 |
maps (int_range_from_string name min_int) (space_explode "," s)
|
|
236 |
(* string -> int -> int list *)
|
|
237 |
fun lookup_int_seq name min_int =
|
|
238 |
case lookup name of
|
|
239 |
SOME s => (case int_seq_from_string name min_int s of
|
|
240 |
[] => [min_int]
|
|
241 |
| value => value)
|
|
242 |
| NONE => [min_int]
|
|
243 |
(* (string -> 'a) -> int -> string -> ('a option * int list) list *)
|
|
244 |
fun lookup_ints_assigns read prefix min_int =
|
|
245 |
(NONE, lookup_int_seq prefix min_int)
|
|
246 |
:: map (fn (name, value) =>
|
|
247 |
(SOME (read (String.extract (name, size prefix + 1, NONE))),
|
|
248 |
value |> stringify_raw_param_value
|
|
249 |
|> int_seq_from_string name min_int))
|
|
250 |
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
|
|
251 |
(* (string -> 'a) -> string -> ('a option * bool option) list *)
|
|
252 |
fun lookup_bool_option_assigns read prefix =
|
|
253 |
(NONE, lookup_bool_option prefix)
|
|
254 |
:: map (fn (name, value) =>
|
|
255 |
(SOME (read (String.extract (name, size prefix + 1, NONE))),
|
|
256 |
value |> stringify_raw_param_value
|
|
257 |
|> bool_option_from_string true name))
|
|
258 |
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
|
|
259 |
(* string -> Time.time option *)
|
|
260 |
fun lookup_time name =
|
|
261 |
case lookup name of
|
|
262 |
NONE => NONE
|
|
263 |
| SOME "none" => NONE
|
|
264 |
| SOME s =>
|
|
265 |
let
|
|
266 |
val msecs =
|
|
267 |
case space_explode " " s of
|
|
268 |
[s1, "min"] => 60000 * the (Int.fromString s1)
|
|
269 |
| [s1, "s"] => 1000 * the (Int.fromString s1)
|
|
270 |
| [s1, "ms"] => the (Int.fromString s1)
|
|
271 |
| _ => 0
|
|
272 |
in
|
|
273 |
if msecs <= 0 then
|
|
274 |
error ("Parameter " ^ quote name ^ " must be assigned a positive \
|
|
275 |
\time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
|
|
276 |
else
|
|
277 |
SOME (Time.fromMilliseconds msecs)
|
|
278 |
end
|
|
279 |
(* string -> term list *)
|
|
280 |
val lookup_term_list =
|
|
281 |
AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
|
|
282 |
val read_type_polymorphic =
|
|
283 |
Syntax.read_typ ctxt #> Logic.mk_type
|
|
284 |
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
|
|
285 |
(* string -> term *)
|
|
286 |
val read_term_polymorphic =
|
|
287 |
Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
|
|
288 |
(* string -> styp *)
|
|
289 |
val read_const_polymorphic = read_term_polymorphic #> dest_Const
|
|
290 |
val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
|
|
291 |
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
|
|
292 |
val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
|
|
293 |
val bisim_depths = lookup_int_seq "bisim_depth" ~1
|
|
294 |
val boxes =
|
|
295 |
lookup_bool_option_assigns read_type_polymorphic "box" @
|
|
296 |
map_filter (fn (SOME T, _) =>
|
|
297 |
if is_fun_type T orelse is_pair_type T then
|
|
298 |
SOME (SOME T, SOME true)
|
|
299 |
else
|
|
300 |
NONE
|
|
301 |
| (NONE, _) => NONE) cards_assigns
|
|
302 |
val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
|
|
303 |
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
|
|
304 |
val sat_solver = lookup_string "sat_solver"
|
|
305 |
val blocking = not auto andalso lookup_bool "blocking"
|
|
306 |
val falsify = lookup_bool "falsify"
|
|
307 |
val debug = not auto andalso lookup_bool "debug"
|
|
308 |
val verbose = debug orelse (not auto andalso lookup_bool "verbose")
|
|
309 |
val overlord = lookup_bool "overlord"
|
|
310 |
val user_axioms = lookup_bool_option "user_axioms"
|
|
311 |
val assms = lookup_bool "assms"
|
|
312 |
val coalesce_type_vars = lookup_bool "coalesce_type_vars"
|
|
313 |
val destroy_constrs = lookup_bool "destroy_constrs"
|
|
314 |
val specialize = lookup_bool "specialize"
|
|
315 |
val skolemize = lookup_bool "skolemize"
|
|
316 |
val star_linear_preds = lookup_bool "star_linear_preds"
|
|
317 |
val uncurry = lookup_bool "uncurry"
|
|
318 |
val fast_descrs = lookup_bool "fast_descrs"
|
|
319 |
val peephole_optim = lookup_bool "peephole_optim"
|
|
320 |
val timeout = if auto then lookup_time "auto_timeout"
|
|
321 |
else lookup_time "timeout"
|
|
322 |
val tac_timeout = lookup_time "tac_timeout"
|
|
323 |
val sym_break = Int.max (0, lookup_int "sym_break")
|
|
324 |
val sharing_depth = Int.max (1, lookup_int "sharing_depth")
|
|
325 |
val flatten_props = lookup_bool "flatten_props"
|
|
326 |
val max_threads = Int.max (0, lookup_int "max_threads")
|
|
327 |
val show_all = debug orelse lookup_bool "show_all"
|
|
328 |
val show_skolems = show_all orelse lookup_bool "show_skolems"
|
|
329 |
val show_datatypes = show_all orelse lookup_bool "show_datatypes"
|
|
330 |
val show_consts = show_all orelse lookup_bool "show_consts"
|
|
331 |
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
|
|
332 |
val evals = lookup_term_list "eval"
|
|
333 |
val max_potential = if auto then 0
|
|
334 |
else Int.max (0, lookup_int "max_potential")
|
|
335 |
val max_genuine = Int.max (0, lookup_int "max_genuine")
|
|
336 |
val check_potential = lookup_bool "check_potential"
|
|
337 |
val check_genuine = lookup_bool "check_genuine"
|
|
338 |
val batch_size = case lookup_int_option "batch_size" of
|
|
339 |
SOME n => Int.max (1, n)
|
|
340 |
| NONE => if debug then 1 else 64
|
|
341 |
val expect = lookup_string "expect"
|
|
342 |
in
|
|
343 |
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
|
|
344 |
iters_assigns = iters_assigns, bisim_depths = bisim_depths, boxes = boxes,
|
|
345 |
monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
|
|
346 |
falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
|
|
347 |
user_axioms = user_axioms, assms = assms,
|
|
348 |
coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
|
|
349 |
specialize = specialize, skolemize = skolemize,
|
|
350 |
star_linear_preds = star_linear_preds, uncurry = uncurry,
|
|
351 |
fast_descrs = fast_descrs, peephole_optim = peephole_optim,
|
|
352 |
timeout = timeout, tac_timeout = tac_timeout, sym_break = sym_break,
|
|
353 |
sharing_depth = sharing_depth, flatten_props = flatten_props,
|
|
354 |
max_threads = max_threads, show_skolems = show_skolems,
|
|
355 |
show_datatypes = show_datatypes, show_consts = show_consts,
|
|
356 |
formats = formats, evals = evals, max_potential = max_potential,
|
|
357 |
max_genuine = max_genuine, check_potential = check_potential,
|
|
358 |
check_genuine = check_genuine, batch_size = batch_size, expect = expect}
|
|
359 |
end
|
|
360 |
|
|
361 |
(* theory -> (string * string) list -> params *)
|
|
362 |
fun default_params thy =
|
|
363 |
extract_params (ProofContext.init thy) false (default_raw_params thy)
|
|
364 |
o map (apsnd single)
|
|
365 |
|
|
366 |
(* OuterParse.token list -> string * OuterParse.token list *)
|
|
367 |
val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
|
|
368 |
|
|
369 |
(* OuterParse.token list -> string list * OuterParse.token list *)
|
|
370 |
val scan_value =
|
|
371 |
Scan.repeat1 (OuterParse.minus >> single
|
|
372 |
|| Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
|
|
373 |
|| OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
|
|
374 |
>> single) >> flat
|
|
375 |
|
|
376 |
(* OuterParse.token list -> raw_param * OuterParse.token list *)
|
|
377 |
val scan_param =
|
|
378 |
scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
|
|
379 |
(* OuterParse.token list -> raw_param list option * OuterParse.token list *)
|
|
380 |
val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
|
|
381 |
--| OuterParse.$$$ "]")
|
|
382 |
|
|
383 |
(* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
|
|
384 |
fun handle_exceptions ctxt f x =
|
|
385 |
f x
|
|
386 |
handle ARG (loc, details) =>
|
|
387 |
error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
|
|
388 |
| BAD (loc, details) =>
|
|
389 |
error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
|
|
390 |
| LIMIT (_, details) =>
|
|
391 |
(warning ("Limit reached: " ^ details ^ "."); x)
|
|
392 |
| NOT_SUPPORTED details =>
|
|
393 |
(warning ("Unsupported case: " ^ details ^ "."); x)
|
|
394 |
| NUT (loc, us) =>
|
|
395 |
error ("Invalid intermediate term" ^ plural_s_for_list us ^
|
|
396 |
" (" ^ quote loc ^ "): " ^
|
|
397 |
commas (map (string_for_nut ctxt) us) ^ ".")
|
|
398 |
| REP (loc, Rs) =>
|
|
399 |
error ("Invalid representation" ^ plural_s_for_list Rs ^
|
|
400 |
" (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
|
|
401 |
| TERM (loc, ts) =>
|
|
402 |
error ("Invalid term" ^ plural_s_for_list ts ^
|
|
403 |
" (" ^ quote loc ^ "): " ^
|
|
404 |
commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
|
|
405 |
| TYPE (loc, Ts, ts) =>
|
|
406 |
error ("Invalid type" ^ plural_s_for_list Ts ^
|
|
407 |
(if null ts then
|
|
408 |
""
|
|
409 |
else
|
|
410 |
" for term" ^ plural_s_for_list ts ^ " " ^
|
|
411 |
commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
|
|
412 |
" (" ^ quote loc ^ "): " ^
|
|
413 |
commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
|
|
414 |
| Kodkod.SYNTAX (_, details) =>
|
|
415 |
(warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
|
|
416 |
| Refute.REFUTE (loc, details) =>
|
|
417 |
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
|
|
418 |
|
|
419 |
(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
|
|
420 |
fun pick_nits override_params auto subgoal state =
|
|
421 |
let
|
|
422 |
val thy = Proof.theory_of state
|
|
423 |
val ctxt = Proof.context_of state
|
|
424 |
val thm = snd (snd (Proof.get_goal state))
|
|
425 |
val _ = List.app check_raw_param override_params
|
|
426 |
val params as {blocking, debug, ...} =
|
|
427 |
extract_params ctxt auto (default_raw_params thy) override_params
|
|
428 |
(* unit -> Proof.state *)
|
|
429 |
fun go () =
|
|
430 |
(if auto then perhaps o try
|
|
431 |
else if debug then fn f => fn x => f x
|
|
432 |
else handle_exceptions ctxt)
|
|
433 |
(fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
|
|
434 |
state
|
|
435 |
in
|
|
436 |
if auto orelse blocking then
|
|
437 |
go ()
|
|
438 |
else
|
|
439 |
(SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());
|
|
440 |
state)
|
|
441 |
end
|
|
442 |
|
|
443 |
(* (TableFun().key * string list) list option * int option
|
|
444 |
-> Toplevel.transition -> Toplevel.transition *)
|
|
445 |
fun nitpick_trans (opt_params, opt_subgoal) =
|
|
446 |
Toplevel.keep (K ()
|
|
447 |
o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
|
|
448 |
o Toplevel.proof_of)
|
|
449 |
|
|
450 |
(* raw_param -> string *)
|
|
451 |
fun string_for_raw_param (name, value) =
|
|
452 |
name ^ " = " ^ stringify_raw_param_value value
|
|
453 |
|
|
454 |
(* bool -> Proof.state -> Proof.state *)
|
|
455 |
fun pick_nits_auto interactive state =
|
|
456 |
let val thy = Proof.theory_of state in
|
|
457 |
((interactive andalso not (!Toplevel.quiet)
|
|
458 |
andalso the (general_lookup_bool false (default_raw_params thy)
|
|
459 |
(SOME false) "auto"))
|
|
460 |
? pick_nits [] true 0) state
|
|
461 |
end
|
|
462 |
|
|
463 |
(* theory -> theory *)
|
|
464 |
fun register_auto thy =
|
|
465 |
(not (is_registered_auto thy)
|
|
466 |
? (set_registered_auto
|
|
467 |
#> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
|
|
468 |
thy
|
|
469 |
|
|
470 |
(* (TableFun().key * string) list option -> Toplevel.transition
|
|
471 |
-> Toplevel.transition *)
|
|
472 |
fun nitpick_params_trans opt_params =
|
|
473 |
Toplevel.theory
|
|
474 |
(fn thy =>
|
|
475 |
let val thy = fold set_default_raw_param (these opt_params) thy in
|
|
476 |
writeln ("Default parameters for Nitpick:\n" ^
|
|
477 |
(case rev (default_raw_params thy) of
|
|
478 |
[] => "none"
|
|
479 |
| params =>
|
|
480 |
(map check_raw_param params;
|
|
481 |
params |> map string_for_raw_param |> sort_strings
|
|
482 |
|> cat_lines)));
|
|
483 |
register_auto thy
|
|
484 |
end)
|
|
485 |
|
|
486 |
(* OuterParse.token list
|
|
487 |
-> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
|
|
488 |
fun scan_nitpick_command tokens =
|
|
489 |
(scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
|
|
490 |
fun scan_nitpick_params_command tokens =
|
|
491 |
scan_params tokens |>> nitpick_params_trans
|
|
492 |
|
|
493 |
val _ = OuterSyntax.improper_command "nitpick"
|
|
494 |
"try to find a counterexample for a given subgoal using Kodkod"
|
|
495 |
OuterKeyword.diag scan_nitpick_command
|
|
496 |
val _ = OuterSyntax.command "nitpick_params"
|
|
497 |
"set and display the default parameters for Nitpick"
|
|
498 |
OuterKeyword.thy_decl scan_nitpick_params_command
|
|
499 |
|
|
500 |
end;
|