blanchet@33982
|
1 |
(* Title: HOL/Tools/Nitpick/nitpick_isar.ML
|
blanchet@33192
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@34969
|
3 |
Copyright 2008, 2009, 2010
|
blanchet@33192
|
4 |
|
blanchet@33192
|
5 |
Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
|
blanchet@33192
|
6 |
syntax.
|
blanchet@33192
|
7 |
*)
|
blanchet@33192
|
8 |
|
blanchet@33192
|
9 |
signature NITPICK_ISAR =
|
blanchet@33192
|
10 |
sig
|
blanchet@33192
|
11 |
type params = Nitpick.params
|
blanchet@33192
|
12 |
|
blanchet@43861
|
13 |
val nitpickN : string
|
blanchet@43861
|
14 |
val nitpick_paramsN : string
|
blanchet@39562
|
15 |
val auto : bool Unsynchronized.ref
|
blanchet@33192
|
16 |
val default_params : theory -> (string * string) list -> params
|
blanchet@33552
|
17 |
val setup : theory -> theory
|
blanchet@35866
|
18 |
end;
|
blanchet@33192
|
19 |
|
blanchet@33224
|
20 |
structure Nitpick_Isar : NITPICK_ISAR =
|
blanchet@33192
|
21 |
struct
|
blanchet@33192
|
22 |
|
blanchet@33224
|
23 |
open Nitpick_Util
|
blanchet@33224
|
24 |
open Nitpick_HOL
|
blanchet@33224
|
25 |
open Nitpick_Rep
|
blanchet@33224
|
26 |
open Nitpick_Nut
|
blanchet@33192
|
27 |
open Nitpick
|
blanchet@33192
|
28 |
|
blanchet@43861
|
29 |
val nitpickN = "nitpick"
|
blanchet@43861
|
30 |
val nitpick_paramsN = "nitpick_params"
|
blanchet@43861
|
31 |
|
blanchet@39562
|
32 |
val auto = Unsynchronized.ref false
|
blanchet@33552
|
33 |
|
blanchet@39590
|
34 |
(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
|
blanchet@39590
|
35 |
its time slot with several other automatic tools. *)
|
blanchet@43863
|
36 |
val auto_try_max_scopes = 6
|
blanchet@39590
|
37 |
|
wenzelm@33601
|
38 |
val _ =
|
wenzelm@33601
|
39 |
ProofGeneralPgip.add_preference Preferences.category_tracing
|
blanchet@43863
|
40 |
(Preferences.bool_pref auto "auto-nitpick" "Run Nitpick automatically.")
|
blanchet@33552
|
41 |
|
blanchet@33192
|
42 |
type raw_param = string * string list
|
blanchet@33192
|
43 |
|
blanchet@33192
|
44 |
val default_default_params =
|
blanchet@43800
|
45 |
[("card", "1\<emdash>10"),
|
blanchet@38407
|
46 |
("iter", "0,1,2,4,8,12,16,20,24,28"),
|
blanchet@38407
|
47 |
("bits", "1,2,3,4,6,8,10,12,14,16"),
|
blanchet@38407
|
48 |
("bisim_depth", "9"),
|
blanchet@35962
|
49 |
("box", "smart"),
|
blanchet@35962
|
50 |
("finitize", "smart"),
|
blanchet@35962
|
51 |
("mono", "smart"),
|
blanchet@35962
|
52 |
("std", "true"),
|
blanchet@35962
|
53 |
("wf", "smart"),
|
blanchet@35962
|
54 |
("sat_solver", "smart"),
|
blanchet@35962
|
55 |
("batch_size", "smart"),
|
blanchet@35962
|
56 |
("blocking", "true"),
|
blanchet@35962
|
57 |
("falsify", "true"),
|
blanchet@35962
|
58 |
("user_axioms", "smart"),
|
blanchet@35962
|
59 |
("assms", "true"),
|
blanchet@35962
|
60 |
("merge_type_vars", "false"),
|
blanchet@35962
|
61 |
("binary_ints", "smart"),
|
blanchet@35962
|
62 |
("destroy_constrs", "true"),
|
blanchet@35962
|
63 |
("specialize", "true"),
|
blanchet@35962
|
64 |
("star_linear_preds", "true"),
|
blanchet@42727
|
65 |
("total_consts", "smart"),
|
blanchet@35962
|
66 |
("peephole_optim", "true"),
|
blanchet@38373
|
67 |
("datatype_sym_break", "5"),
|
blanchet@38373
|
68 |
("kodkod_sym_break", "15"),
|
blanchet@40582
|
69 |
("timeout", "30"),
|
blanchet@40582
|
70 |
("tac_timeout", "0.5"),
|
blanchet@35962
|
71 |
("max_threads", "0"),
|
blanchet@35962
|
72 |
("debug", "false"),
|
blanchet@35962
|
73 |
("verbose", "false"),
|
blanchet@35962
|
74 |
("overlord", "false"),
|
blanchet@35962
|
75 |
("show_datatypes", "false"),
|
blanchet@42864
|
76 |
("show_skolems", "true"),
|
blanchet@35962
|
77 |
("show_consts", "false"),
|
blanchet@35962
|
78 |
("format", "1"),
|
blanchet@35962
|
79 |
("max_potential", "1"),
|
blanchet@35962
|
80 |
("max_genuine", "1"),
|
blanchet@35962
|
81 |
("check_potential", "false"),
|
blanchet@35962
|
82 |
("check_genuine", "false")]
|
blanchet@33192
|
83 |
|
blanchet@33192
|
84 |
val negated_params =
|
blanchet@33192
|
85 |
[("dont_box", "box"),
|
blanchet@35665
|
86 |
("dont_finitize", "finitize"),
|
blanchet@33192
|
87 |
("non_mono", "mono"),
|
blanchet@34969
|
88 |
("non_std", "std"),
|
blanchet@33192
|
89 |
("non_wf", "wf"),
|
blanchet@33192
|
90 |
("non_blocking", "blocking"),
|
blanchet@33192
|
91 |
("satisfy", "falsify"),
|
blanchet@33192
|
92 |
("no_user_axioms", "user_axioms"),
|
blanchet@33192
|
93 |
("no_assms", "assms"),
|
blanchet@33547
|
94 |
("dont_merge_type_vars", "merge_type_vars"),
|
blanchet@34121
|
95 |
("unary_ints", "binary_ints"),
|
blanchet@33192
|
96 |
("dont_destroy_constrs", "destroy_constrs"),
|
blanchet@33192
|
97 |
("dont_specialize", "specialize"),
|
blanchet@33192
|
98 |
("dont_star_linear_preds", "star_linear_preds"),
|
blanchet@42727
|
99 |
("partial_consts", "total_consts"),
|
blanchet@33192
|
100 |
("no_peephole_optim", "peephole_optim"),
|
blanchet@35962
|
101 |
("no_debug", "debug"),
|
blanchet@33192
|
102 |
("quiet", "verbose"),
|
blanchet@33192
|
103 |
("no_overlord", "overlord"),
|
blanchet@33192
|
104 |
("hide_datatypes", "show_datatypes"),
|
blanchet@42864
|
105 |
("hide_skolems", "show_skolems"),
|
blanchet@33192
|
106 |
("hide_consts", "show_consts"),
|
blanchet@33192
|
107 |
("trust_potential", "check_potential"),
|
blanchet@33192
|
108 |
("trust_genuine", "check_genuine")]
|
blanchet@33192
|
109 |
|
blanchet@33192
|
110 |
fun is_known_raw_param s =
|
blanchet@34923
|
111 |
AList.defined (op =) default_default_params s orelse
|
blanchet@34923
|
112 |
AList.defined (op =) negated_params s orelse
|
blanchet@42747
|
113 |
member (op =) ["max", "show_all", "whack", "eval", "need", "atoms",
|
blanchet@42747
|
114 |
"expect"] s orelse
|
blanchet@34923
|
115 |
exists (fn p => String.isPrefix (p ^ " ") s)
|
blanchet@35665
|
116 |
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
|
blanchet@42747
|
117 |
"mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
|
blanchet@42747
|
118 |
"atoms"]
|
blanchet@33192
|
119 |
|
blanchet@33192
|
120 |
fun check_raw_param (s, _) =
|
blanchet@33192
|
121 |
if is_known_raw_param s then ()
|
blanchet@39562
|
122 |
else error ("Unknown parameter: " ^ quote s ^ ".")
|
blanchet@33192
|
123 |
|
blanchet@33192
|
124 |
fun unnegate_param_name name =
|
blanchet@33192
|
125 |
case AList.lookup (op =) negated_params name of
|
blanchet@33192
|
126 |
NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
|
blanchet@33192
|
127 |
else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
|
blanchet@33192
|
128 |
else NONE
|
blanchet@33192
|
129 |
| some_name => some_name
|
blanchet@37163
|
130 |
fun normalize_raw_param (name, value) =
|
blanchet@33192
|
131 |
case unnegate_param_name name of
|
blanchet@37163
|
132 |
SOME name' => [(name', case value of
|
blanchet@37163
|
133 |
["false"] => ["true"]
|
blanchet@37163
|
134 |
| ["true"] => ["false"]
|
blanchet@37163
|
135 |
| [] => ["false"]
|
blanchet@37163
|
136 |
| _ => value)]
|
blanchet@37163
|
137 |
| NONE => if name = "show_all" then
|
blanchet@42864
|
138 |
[("show_datatypes", value), ("show_skolems", value),
|
blanchet@42864
|
139 |
("show_consts", value)]
|
blanchet@37163
|
140 |
else
|
blanchet@37163
|
141 |
[(name, value)]
|
blanchet@33192
|
142 |
|
wenzelm@41720
|
143 |
structure Data = Theory_Data
|
wenzelm@41720
|
144 |
(
|
blanchet@35962
|
145 |
type T = raw_param list
|
blanchet@36391
|
146 |
val empty = map (apsnd single) default_default_params
|
blanchet@33192
|
147 |
val extend = I
|
wenzelm@41720
|
148 |
fun merge data = AList.merge (op =) (K true) data
|
wenzelm@41720
|
149 |
)
|
blanchet@33192
|
150 |
|
blanchet@37163
|
151 |
val set_default_raw_param =
|
blanchet@37163
|
152 |
Data.map o fold (AList.update (op =)) o normalize_raw_param
|
blanchet@35962
|
153 |
val default_raw_params = Data.get
|
blanchet@33192
|
154 |
|
blanchet@43800
|
155 |
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")
|
blanchet@33192
|
156 |
|
blanchet@33192
|
157 |
fun stringify_raw_param_value [] = ""
|
blanchet@33192
|
158 |
| stringify_raw_param_value [s] = s
|
blanchet@33192
|
159 |
| stringify_raw_param_value (s1 :: s2 :: ss) =
|
blanchet@33192
|
160 |
s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
|
blanchet@33192
|
161 |
stringify_raw_param_value (s2 :: ss)
|
blanchet@33192
|
162 |
|
blanchet@33192
|
163 |
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
|
blanchet@33192
|
164 |
|
blanchet@43863
|
165 |
fun extract_params ctxt mode default_params override_params =
|
blanchet@33192
|
166 |
let
|
blanchet@37163
|
167 |
val override_params = maps normalize_raw_param override_params
|
blanchet@33192
|
168 |
val raw_params = rev override_params @ rev default_params
|
blanchet@37259
|
169 |
val raw_lookup = AList.lookup (op =) raw_params
|
blanchet@37259
|
170 |
val lookup = Option.map stringify_raw_param_value o raw_lookup
|
blanchet@35962
|
171 |
val lookup_string = the_default "" o lookup
|
blanchet@35962
|
172 |
fun general_lookup_bool option default_value name =
|
blanchet@35962
|
173 |
case lookup name of
|
blanchet@36380
|
174 |
SOME s => parse_bool_option option name s
|
blanchet@35962
|
175 |
| NONE => default_value
|
blanchet@35962
|
176 |
val lookup_bool = the o general_lookup_bool false (SOME false)
|
blanchet@35962
|
177 |
val lookup_bool_option = general_lookup_bool true NONE
|
blanchet@33192
|
178 |
fun do_int name value =
|
blanchet@33192
|
179 |
case value of
|
blanchet@33192
|
180 |
SOME s => (case Int.fromString s of
|
blanchet@33192
|
181 |
SOME i => i
|
blanchet@33192
|
182 |
| NONE => error ("Parameter " ^ quote name ^
|
blanchet@33192
|
183 |
" must be assigned an integer value."))
|
blanchet@33192
|
184 |
| NONE => 0
|
blanchet@33192
|
185 |
fun lookup_int name = do_int name (lookup name)
|
blanchet@33192
|
186 |
fun lookup_int_option name =
|
blanchet@33192
|
187 |
case lookup name of
|
blanchet@33192
|
188 |
SOME "smart" => NONE
|
blanchet@33192
|
189 |
| value => SOME (do_int name value)
|
blanchet@33192
|
190 |
fun int_range_from_string name min_int s =
|
blanchet@33192
|
191 |
let
|
blanchet@33192
|
192 |
val (k1, k2) =
|
blanchet@33192
|
193 |
(case space_explode "-" s of
|
blanchet@43800
|
194 |
[s] => the_default (s, s) (first_field "\<emdash>" s)
|
blanchet@33192
|
195 |
| ["", s2] => ("-" ^ s2, "-" ^ s2)
|
blanchet@33192
|
196 |
| [s1, s2] => (s1, s2)
|
blanchet@33192
|
197 |
| _ => raise Option)
|
blanchet@33192
|
198 |
|> pairself (maxed_int_from_string min_int)
|
blanchet@33192
|
199 |
in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
|
blanchet@33192
|
200 |
handle Option.Option =>
|
blanchet@33192
|
201 |
error ("Parameter " ^ quote name ^
|
blanchet@33192
|
202 |
" must be assigned a sequence of integers.")
|
blanchet@33192
|
203 |
fun int_seq_from_string name min_int s =
|
blanchet@33192
|
204 |
maps (int_range_from_string name min_int) (space_explode "," s)
|
blanchet@33192
|
205 |
fun lookup_int_seq name min_int =
|
blanchet@33192
|
206 |
case lookup name of
|
blanchet@33192
|
207 |
SOME s => (case int_seq_from_string name min_int s of
|
blanchet@33192
|
208 |
[] => [min_int]
|
blanchet@33192
|
209 |
| value => value)
|
blanchet@33192
|
210 |
| NONE => [min_int]
|
blanchet@37259
|
211 |
fun lookup_assigns read prefix default convert =
|
blanchet@37259
|
212 |
(NONE, convert (the_default default (lookup prefix)))
|
blanchet@33192
|
213 |
:: map (fn (name, value) =>
|
blanchet@33192
|
214 |
(SOME (read (String.extract (name, size prefix + 1, NONE))),
|
blanchet@37259
|
215 |
convert (stringify_raw_param_value value)))
|
blanchet@33192
|
216 |
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
|
blanchet@37259
|
217 |
fun lookup_ints_assigns read prefix min_int =
|
blanchet@37259
|
218 |
lookup_assigns read prefix (signed_string_of_int min_int)
|
blanchet@37259
|
219 |
(int_seq_from_string prefix min_int)
|
blanchet@34969
|
220 |
fun lookup_bool_assigns read prefix =
|
blanchet@37259
|
221 |
lookup_assigns read prefix "" (the o parse_bool_option false prefix)
|
blanchet@33192
|
222 |
fun lookup_bool_option_assigns read prefix =
|
blanchet@37259
|
223 |
lookup_assigns read prefix "" (parse_bool_option true prefix)
|
blanchet@37259
|
224 |
fun lookup_strings_assigns read prefix =
|
blanchet@37259
|
225 |
lookup_assigns read prefix "" (space_explode " ")
|
blanchet@33192
|
226 |
fun lookup_time name =
|
blanchet@33192
|
227 |
case lookup name of
|
blanchet@39562
|
228 |
SOME s => parse_time_option name s
|
blanchet@39562
|
229 |
| NONE => NONE
|
blanchet@33192
|
230 |
val read_type_polymorphic =
|
blanchet@33192
|
231 |
Syntax.read_typ ctxt #> Logic.mk_type
|
blanchet@33192
|
232 |
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
|
blanchet@33192
|
233 |
val read_term_polymorphic =
|
blanchet@33192
|
234 |
Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
|
blanchet@42747
|
235 |
val lookup_term_list_option_polymorphic =
|
blanchet@42747
|
236 |
AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)
|
blanchet@33192
|
237 |
val read_const_polymorphic = read_term_polymorphic #> dest_Const
|
blanchet@43863
|
238 |
val cards_assigns =
|
blanchet@43863
|
239 |
lookup_ints_assigns read_type_polymorphic "card" 1
|
blanchet@43863
|
240 |
|> mode = Auto_Try ? map (apsnd (take auto_try_max_scopes))
|
blanchet@33192
|
241 |
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
|
blanchet@33192
|
242 |
val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
|
blanchet@34121
|
243 |
val bitss = lookup_int_seq "bits" 1
|
blanchet@33192
|
244 |
val bisim_depths = lookup_int_seq "bisim_depth" ~1
|
blanchet@35665
|
245 |
val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
|
blanchet@35665
|
246 |
val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
|
blanchet@43863
|
247 |
val monos = if mode = Auto_Try then [(NONE, SOME true)]
|
blanchet@39562
|
248 |
else lookup_bool_option_assigns read_type_polymorphic "mono"
|
blanchet@34969
|
249 |
val stds = lookup_bool_assigns read_type_polymorphic "std"
|
blanchet@33192
|
250 |
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
|
blanchet@33192
|
251 |
val sat_solver = lookup_string "sat_solver"
|
blanchet@43863
|
252 |
val blocking = mode <> Normal orelse lookup_bool "blocking"
|
blanchet@33192
|
253 |
val falsify = lookup_bool "falsify"
|
blanchet@43863
|
254 |
val debug = (mode <> Auto_Try andalso lookup_bool "debug")
|
blanchet@43863
|
255 |
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
|
blanchet@33192
|
256 |
val overlord = lookup_bool "overlord"
|
blanchet@33192
|
257 |
val user_axioms = lookup_bool_option "user_axioms"
|
blanchet@33192
|
258 |
val assms = lookup_bool "assms"
|
blanchet@42747
|
259 |
val whacks = lookup_term_list_option_polymorphic "whack" |> these
|
blanchet@33547
|
260 |
val merge_type_vars = lookup_bool "merge_type_vars"
|
blanchet@34121
|
261 |
val binary_ints = lookup_bool_option "binary_ints"
|
blanchet@33192
|
262 |
val destroy_constrs = lookup_bool "destroy_constrs"
|
blanchet@33192
|
263 |
val specialize = lookup_bool "specialize"
|
blanchet@33192
|
264 |
val star_linear_preds = lookup_bool "star_linear_preds"
|
blanchet@42727
|
265 |
val total_consts = lookup_bool_option "total_consts"
|
blanchet@42747
|
266 |
val needs = lookup_term_list_option_polymorphic "need"
|
blanchet@33192
|
267 |
val peephole_optim = lookup_bool "peephole_optim"
|
blanchet@38370
|
268 |
val datatype_sym_break = lookup_int "datatype_sym_break"
|
blanchet@38370
|
269 |
val kodkod_sym_break = lookup_int "kodkod_sym_break"
|
blanchet@43863
|
270 |
val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
|
blanchet@33192
|
271 |
val tac_timeout = lookup_time "tac_timeout"
|
blanchet@43863
|
272 |
val max_threads =
|
blanchet@43863
|
273 |
if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
|
blanchet@37163
|
274 |
val show_datatypes = debug orelse lookup_bool "show_datatypes"
|
blanchet@42864
|
275 |
val show_skolems = debug orelse lookup_bool "show_skolems"
|
blanchet@37163
|
276 |
val show_consts = debug orelse lookup_bool "show_consts"
|
blanchet@42747
|
277 |
val evals = lookup_term_list_option_polymorphic "eval" |> these
|
blanchet@33192
|
278 |
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
|
blanchet@37259
|
279 |
val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
|
blanchet@33552
|
280 |
val max_potential =
|
blanchet@43873
|
281 |
if mode = Normal then Int.max (0, lookup_int "max_potential") else 0
|
blanchet@33192
|
282 |
val max_genuine = Int.max (0, lookup_int "max_genuine")
|
blanchet@33192
|
283 |
val check_potential = lookup_bool "check_potential"
|
blanchet@33192
|
284 |
val check_genuine = lookup_bool "check_genuine"
|
blanchet@36390
|
285 |
val batch_size =
|
blanchet@36390
|
286 |
case lookup_int_option "batch_size" of
|
blanchet@36390
|
287 |
SOME n => Int.max (1, n)
|
blanchet@38407
|
288 |
| NONE => if debug then 1 else 50
|
blanchet@33192
|
289 |
val expect = lookup_string "expect"
|
blanchet@33192
|
290 |
in
|
blanchet@33192
|
291 |
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
|
blanchet@34121
|
292 |
iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
|
blanchet@35665
|
293 |
boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
|
blanchet@35665
|
294 |
wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
|
blanchet@34969
|
295 |
debug = debug, verbose = verbose, overlord = overlord,
|
blanchet@38436
|
296 |
user_axioms = user_axioms, assms = assms, whacks = whacks,
|
blanchet@34121
|
297 |
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
|
blanchet@34121
|
298 |
destroy_constrs = destroy_constrs, specialize = specialize,
|
blanchet@42727
|
299 |
star_linear_preds = star_linear_preds, total_consts = total_consts,
|
blanchet@42746
|
300 |
needs = needs, peephole_optim = peephole_optim,
|
blanchet@42727
|
301 |
datatype_sym_break = datatype_sym_break,
|
blanchet@38370
|
302 |
kodkod_sym_break = kodkod_sym_break, timeout = timeout,
|
blanchet@36389
|
303 |
tac_timeout = tac_timeout, max_threads = max_threads,
|
blanchet@42864
|
304 |
show_datatypes = show_datatypes, show_skolems = show_skolems,
|
blanchet@42864
|
305 |
show_consts = show_consts, evals = evals, formats = formats,
|
blanchet@42864
|
306 |
atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
|
blanchet@37259
|
307 |
check_potential = check_potential, check_genuine = check_genuine,
|
blanchet@37259
|
308 |
batch_size = batch_size, expect = expect}
|
blanchet@33192
|
309 |
end
|
blanchet@33192
|
310 |
|
blanchet@33192
|
311 |
fun default_params thy =
|
blanchet@43863
|
312 |
extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
|
blanchet@33192
|
313 |
o map (apsnd single)
|
blanchet@33192
|
314 |
|
wenzelm@36970
|
315 |
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
|
blanchet@35962
|
316 |
val parse_value =
|
wenzelm@36970
|
317 |
Scan.repeat1 (Parse.minus >> single
|
blanchet@40582
|
318 |
|| Scan.repeat1 (Scan.unless Parse.minus
|
blanchet@40582
|
319 |
(Parse.name || Parse.float_number))
|
blanchet@40582
|
320 |
|| Parse.$$$ "," |-- Parse.number >> prefix "," >> single)
|
blanchet@40582
|
321 |
>> flat
|
wenzelm@36970
|
322 |
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
|
blanchet@35966
|
323 |
val parse_params =
|
wenzelm@36970
|
324 |
Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
|
blanchet@33192
|
325 |
|
blanchet@33192
|
326 |
fun handle_exceptions ctxt f x =
|
blanchet@33192
|
327 |
f x
|
blanchet@33192
|
328 |
handle ARG (loc, details) =>
|
blanchet@33192
|
329 |
error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
|
blanchet@33192
|
330 |
| BAD (loc, details) =>
|
blanchet@33192
|
331 |
error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
|
blanchet@33192
|
332 |
| NOT_SUPPORTED details =>
|
blanchet@33192
|
333 |
(warning ("Unsupported case: " ^ details ^ "."); x)
|
blanchet@33192
|
334 |
| NUT (loc, us) =>
|
blanchet@33192
|
335 |
error ("Invalid intermediate term" ^ plural_s_for_list us ^
|
blanchet@33192
|
336 |
" (" ^ quote loc ^ "): " ^
|
blanchet@33192
|
337 |
commas (map (string_for_nut ctxt) us) ^ ".")
|
blanchet@33192
|
338 |
| REP (loc, Rs) =>
|
blanchet@33192
|
339 |
error ("Invalid representation" ^ plural_s_for_list Rs ^
|
blanchet@33192
|
340 |
" (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
|
blanchet@33192
|
341 |
| TERM (loc, ts) =>
|
blanchet@33192
|
342 |
error ("Invalid term" ^ plural_s_for_list ts ^
|
blanchet@33192
|
343 |
" (" ^ quote loc ^ "): " ^
|
blanchet@33192
|
344 |
commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
|
blanchet@33192
|
345 |
| TYPE (loc, Ts, ts) =>
|
blanchet@33192
|
346 |
error ("Invalid type" ^ plural_s_for_list Ts ^
|
blanchet@33192
|
347 |
(if null ts then
|
blanchet@33192
|
348 |
""
|
blanchet@33192
|
349 |
else
|
blanchet@33192
|
350 |
" for term" ^ plural_s_for_list ts ^ " " ^
|
blanchet@33192
|
351 |
commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
|
blanchet@33192
|
352 |
" (" ^ quote loc ^ "): " ^
|
blanchet@33192
|
353 |
commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
|
blanchet@33192
|
354 |
| Refute.REFUTE (loc, details) =>
|
blanchet@33192
|
355 |
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
|
blanchet@33192
|
356 |
|
blanchet@43863
|
357 |
fun pick_nits override_params mode i step state =
|
blanchet@33192
|
358 |
let
|
blanchet@33192
|
359 |
val thy = Proof.theory_of state
|
blanchet@33192
|
360 |
val ctxt = Proof.context_of state
|
blanchet@33192
|
361 |
val _ = List.app check_raw_param override_params
|
blanchet@33192
|
362 |
val params as {blocking, debug, ...} =
|
blanchet@43863
|
363 |
extract_params ctxt mode (default_raw_params thy) override_params
|
blanchet@33192
|
364 |
fun go () =
|
blanchet@43861
|
365 |
(unknownN, state)
|
blanchet@43863
|
366 |
|> (if mode = Auto_Try then perhaps o try
|
blanchet@33552
|
367 |
else if debug then fn f => fn x => f x
|
blanchet@33552
|
368 |
else handle_exceptions ctxt)
|
blanchet@43863
|
369 |
(fn (_, state) => pick_nits_in_subgoal state params mode i step)
|
blanchet@43861
|
370 |
in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
|
blanchet@43861
|
371 |
|> `(fn (outcome_code, _) => outcome_code = genuineN)
|
blanchet@33192
|
372 |
|
blanchet@35966
|
373 |
fun nitpick_trans (params, i) =
|
blanchet@43861
|
374 |
Toplevel.keep (fn state =>
|
blanchet@43863
|
375 |
pick_nits params Normal i (Toplevel.proof_position_of state)
|
blanchet@43861
|
376 |
(Toplevel.proof_of state) |> K ())
|
blanchet@33192
|
377 |
|
blanchet@33192
|
378 |
fun string_for_raw_param (name, value) =
|
blanchet@33192
|
379 |
name ^ " = " ^ stringify_raw_param_value value
|
blanchet@33192
|
380 |
|
blanchet@35966
|
381 |
fun nitpick_params_trans params =
|
blanchet@33192
|
382 |
Toplevel.theory
|
blanchet@35966
|
383 |
(fold set_default_raw_param params
|
blanchet@39562
|
384 |
#> tap (fn thy =>
|
blanchet@33552
|
385 |
writeln ("Default parameters for Nitpick:\n" ^
|
blanchet@33552
|
386 |
(case rev (default_raw_params thy) of
|
blanchet@33552
|
387 |
[] => "none"
|
blanchet@33552
|
388 |
| params =>
|
blanchet@33552
|
389 |
(map check_raw_param params;
|
blanchet@33552
|
390 |
params |> map string_for_raw_param
|
blanchet@33552
|
391 |
|> sort_strings |> cat_lines)))))
|
blanchet@33192
|
392 |
|
blanchet@35962
|
393 |
val parse_nitpick_command =
|
wenzelm@36970
|
394 |
(parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
|
blanchet@35962
|
395 |
val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
|
blanchet@33192
|
396 |
|
blanchet@43861
|
397 |
val _ = Outer_Syntax.improper_command nitpickN
|
blanchet@36390
|
398 |
"try to find a counterexample for a given subgoal using Nitpick"
|
wenzelm@36970
|
399 |
Keyword.diag parse_nitpick_command
|
blanchet@43861
|
400 |
val _ = Outer_Syntax.command nitpick_paramsN
|
blanchet@33192
|
401 |
"set and display the default parameters for Nitpick"
|
wenzelm@36970
|
402 |
Keyword.thy_decl parse_nitpick_params_command
|
blanchet@33192
|
403 |
|
blanchet@43863
|
404 |
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
|
blanchet@33552
|
405 |
|
blanchet@43865
|
406 |
val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
|
blanchet@33552
|
407 |
|
blanchet@33192
|
408 |
end;
|