author | blanchet |
Tue, 23 Feb 2010 15:56:13 +0100 | |
changeset 35333 | f61de25f71f9 |
parent 35309 | 997aa3a3e4bb |
child 35336 | ef3eba82465f |
permissions | -rw-r--r-- |
33982 | 1 |
(* Title: HOL/Tools/Nitpick/kodkod.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 |
ML interface on top of Kodkod. |
|
6 |
*) |
|
7 |
||
8 |
signature KODKOD = |
|
9 |
sig |
|
10 |
type n_ary_index = int * int |
|
11 |
type setting = string * string |
|
12 |
||
13 |
datatype tuple = |
|
14 |
Tuple of int list | |
|
15 |
TupleIndex of n_ary_index | |
|
16 |
TupleReg of n_ary_index |
|
17 |
||
18 |
datatype tuple_set = |
|
19 |
TupleUnion of tuple_set * tuple_set | |
|
20 |
TupleDifference of tuple_set * tuple_set | |
|
21 |
TupleIntersect of tuple_set * tuple_set | |
|
22 |
TupleProduct of tuple_set * tuple_set | |
|
23 |
TupleProject of tuple_set * int | |
|
24 |
TupleSet of tuple list | |
|
25 |
TupleRange of tuple * tuple | |
|
26 |
TupleArea of tuple * tuple | |
|
27 |
TupleAtomSeq of int * int | |
|
28 |
TupleSetReg of n_ary_index |
|
29 |
||
30 |
datatype tuple_assign = |
|
31 |
AssignTuple of n_ary_index * tuple | |
|
32 |
AssignTupleSet of n_ary_index * tuple_set |
|
33 |
||
34 |
type bound = (n_ary_index * string) list * tuple_set list |
|
35 |
type int_bound = int option * tuple_set list |
|
36 |
||
37 |
datatype formula = |
|
38 |
All of decl list * formula | |
|
39 |
Exist of decl list * formula | |
|
40 |
FormulaLet of expr_assign list * formula | |
|
41 |
FormulaIf of formula * formula * formula | |
|
42 |
Or of formula * formula | |
|
43 |
Iff of formula * formula | |
|
44 |
Implies of formula * formula | |
|
45 |
And of formula * formula | |
|
46 |
Not of formula | |
|
47 |
Acyclic of n_ary_index | |
|
48 |
Function of n_ary_index * rel_expr * rel_expr | |
|
49 |
Functional of n_ary_index * rel_expr * rel_expr | |
|
50 |
TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index | |
|
51 |
Subset of rel_expr * rel_expr | |
|
52 |
RelEq of rel_expr * rel_expr | |
|
53 |
IntEq of int_expr * int_expr | |
|
54 |
LT of int_expr * int_expr | |
|
55 |
LE of int_expr * int_expr | |
|
56 |
No of rel_expr | |
|
57 |
Lone of rel_expr | |
|
58 |
One of rel_expr | |
|
59 |
Some of rel_expr | |
|
60 |
False | |
|
61 |
True | |
|
62 |
FormulaReg of int |
|
63 |
and rel_expr = |
|
64 |
RelLet of expr_assign list * rel_expr | |
|
65 |
RelIf of formula * rel_expr * rel_expr | |
|
66 |
Union of rel_expr * rel_expr | |
|
67 |
Difference of rel_expr * rel_expr | |
|
68 |
Override of rel_expr * rel_expr | |
|
69 |
Intersect of rel_expr * rel_expr | |
|
70 |
Product of rel_expr * rel_expr | |
|
71 |
IfNo of rel_expr * rel_expr | |
|
72 |
Project of rel_expr * int_expr list | |
|
73 |
Join of rel_expr * rel_expr | |
|
74 |
Closure of rel_expr | |
|
75 |
ReflexiveClosure of rel_expr | |
|
76 |
Transpose of rel_expr | |
|
77 |
Comprehension of decl list * formula | |
|
78 |
Bits of int_expr | |
|
79 |
Int of int_expr | |
|
80 |
Iden | |
|
81 |
Ints | |
|
82 |
None | |
|
83 |
Univ | |
|
84 |
Atom of int | |
|
85 |
AtomSeq of int * int | |
|
86 |
Rel of n_ary_index | |
|
87 |
Var of n_ary_index | |
|
88 |
RelReg of n_ary_index |
|
89 |
and int_expr = |
|
90 |
Sum of decl list * int_expr | |
|
91 |
IntLet of expr_assign list * int_expr | |
|
92 |
IntIf of formula * int_expr * int_expr | |
|
93 |
SHL of int_expr * int_expr | |
|
94 |
SHA of int_expr * int_expr | |
|
95 |
SHR of int_expr * int_expr | |
|
96 |
Add of int_expr * int_expr | |
|
97 |
Sub of int_expr * int_expr | |
|
98 |
Mult of int_expr * int_expr | |
|
99 |
Div of int_expr * int_expr | |
|
100 |
Mod of int_expr * int_expr | |
|
101 |
Cardinality of rel_expr | |
|
102 |
SetSum of rel_expr | |
|
103 |
BitOr of int_expr * int_expr | |
|
104 |
BitXor of int_expr * int_expr | |
|
105 |
BitAnd of int_expr * int_expr | |
|
106 |
BitNot of int_expr | |
|
107 |
Neg of int_expr | |
|
108 |
Absolute of int_expr | |
|
109 |
Signum of int_expr | |
|
110 |
Num of int | |
|
111 |
IntReg of int |
|
112 |
and decl = |
|
113 |
DeclNo of n_ary_index * rel_expr | |
|
114 |
DeclLone of n_ary_index * rel_expr | |
|
115 |
DeclOne of n_ary_index * rel_expr | |
|
116 |
DeclSome of n_ary_index * rel_expr | |
|
117 |
DeclSet of n_ary_index * rel_expr |
|
118 |
and expr_assign = |
|
119 |
AssignFormulaReg of int * formula | |
|
120 |
AssignRelReg of n_ary_index * rel_expr | |
|
121 |
AssignIntReg of int * int_expr |
|
122 |
||
123 |
type 'a fold_expr_funcs = { |
|
124 |
formula_func: formula -> 'a -> 'a, |
|
125 |
rel_expr_func: rel_expr -> 'a -> 'a, |
|
126 |
int_expr_func: int_expr -> 'a -> 'a |
|
127 |
} |
|
128 |
||
129 |
val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a |
|
130 |
val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a |
|
131 |
val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a |
|
132 |
val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a |
|
133 |
val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a |
|
134 |
||
135 |
type 'a fold_tuple_funcs = { |
|
136 |
tuple_func: tuple -> 'a -> 'a, |
|
137 |
tuple_set_func: tuple_set -> 'a -> 'a |
|
138 |
} |
|
139 |
||
140 |
val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a |
|
141 |
val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a |
|
142 |
val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a |
|
143 |
val fold_bound : |
|
144 |
'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a |
|
145 |
val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a |
|
146 |
||
147 |
type problem = { |
|
148 |
comment: string, |
|
149 |
settings: setting list, |
|
150 |
univ_card: int, |
|
151 |
tuple_assigns: tuple_assign list, |
|
152 |
bounds: bound list, |
|
153 |
int_bounds: int_bound list, |
|
154 |
expr_assigns: expr_assign list, |
|
155 |
formula: formula} |
|
156 |
||
157 |
type raw_bound = n_ary_index * int list list |
|
158 |
||
159 |
datatype outcome = |
|
33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset
|
160 |
NotInstalled | |
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
161 |
Normal of (int * raw_bound list) list * int list * string | |
33192 | 162 |
TimedOut of int list | |
163 |
Interrupted of int list option | |
|
164 |
Error of string * int list |
|
165 |
||
166 |
exception SYNTAX of string * string |
|
167 |
||
168 |
val max_arity : int -> int |
|
169 |
val arity_of_rel_expr : rel_expr -> int |
|
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
170 |
val is_problem_trivially_false : problem -> bool |
33192 | 171 |
val problems_equivalent : problem -> problem -> bool |
172 |
val solve_any_problem : |
|
173 |
bool -> Time.time option -> int -> int -> problem list -> outcome |
|
174 |
end; |
|
175 |
||
176 |
structure Kodkod : KODKOD = |
|
177 |
struct |
|
178 |
||
179 |
type n_ary_index = int * int |
|
180 |
||
181 |
type setting = string * string |
|
182 |
||
183 |
datatype tuple = |
|
184 |
Tuple of int list | |
|
185 |
TupleIndex of n_ary_index | |
|
186 |
TupleReg of n_ary_index |
|
187 |
||
188 |
datatype tuple_set = |
|
189 |
TupleUnion of tuple_set * tuple_set | |
|
190 |
TupleDifference of tuple_set * tuple_set | |
|
191 |
TupleIntersect of tuple_set * tuple_set | |
|
192 |
TupleProduct of tuple_set * tuple_set | |
|
193 |
TupleProject of tuple_set * int | |
|
194 |
TupleSet of tuple list | |
|
195 |
TupleRange of tuple * tuple | |
|
196 |
TupleArea of tuple * tuple | |
|
197 |
TupleAtomSeq of int * int | |
|
198 |
TupleSetReg of n_ary_index |
|
199 |
||
200 |
datatype tuple_assign = |
|
201 |
AssignTuple of n_ary_index * tuple | |
|
202 |
AssignTupleSet of n_ary_index * tuple_set |
|
203 |
||
204 |
type bound = (n_ary_index * string) list * tuple_set list |
|
205 |
type int_bound = int option * tuple_set list |
|
206 |
||
207 |
datatype formula = |
|
208 |
All of decl list * formula | |
|
209 |
Exist of decl list * formula | |
|
210 |
FormulaLet of expr_assign list * formula | |
|
211 |
FormulaIf of formula * formula * formula | |
|
212 |
Or of formula * formula | |
|
213 |
Iff of formula * formula | |
|
214 |
Implies of formula * formula | |
|
215 |
And of formula * formula | |
|
216 |
Not of formula | |
|
217 |
Acyclic of n_ary_index | |
|
218 |
Function of n_ary_index * rel_expr * rel_expr | |
|
219 |
Functional of n_ary_index * rel_expr * rel_expr | |
|
220 |
TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index | |
|
221 |
Subset of rel_expr * rel_expr | |
|
222 |
RelEq of rel_expr * rel_expr | |
|
223 |
IntEq of int_expr * int_expr | |
|
224 |
LT of int_expr * int_expr | |
|
225 |
LE of int_expr * int_expr | |
|
226 |
No of rel_expr | |
|
227 |
Lone of rel_expr | |
|
228 |
One of rel_expr | |
|
229 |
Some of rel_expr | |
|
230 |
False | |
|
231 |
True | |
|
232 |
FormulaReg of int |
|
233 |
and rel_expr = |
|
234 |
RelLet of expr_assign list * rel_expr | |
|
235 |
RelIf of formula * rel_expr * rel_expr | |
|
236 |
Union of rel_expr * rel_expr | |
|
237 |
Difference of rel_expr * rel_expr | |
|
238 |
Override of rel_expr * rel_expr | |
|
239 |
Intersect of rel_expr * rel_expr | |
|
240 |
Product of rel_expr * rel_expr | |
|
241 |
IfNo of rel_expr * rel_expr | |
|
242 |
Project of rel_expr * int_expr list | |
|
243 |
Join of rel_expr * rel_expr | |
|
244 |
Closure of rel_expr | |
|
245 |
ReflexiveClosure of rel_expr | |
|
246 |
Transpose of rel_expr | |
|
247 |
Comprehension of decl list * formula | |
|
248 |
Bits of int_expr | |
|
249 |
Int of int_expr | |
|
250 |
Iden | |
|
251 |
Ints | |
|
252 |
None | |
|
253 |
Univ | |
|
254 |
Atom of int | |
|
255 |
AtomSeq of int * int | |
|
256 |
Rel of n_ary_index | |
|
257 |
Var of n_ary_index | |
|
258 |
RelReg of n_ary_index |
|
259 |
and int_expr = |
|
260 |
Sum of decl list * int_expr | |
|
261 |
IntLet of expr_assign list * int_expr | |
|
262 |
IntIf of formula * int_expr * int_expr | |
|
263 |
SHL of int_expr * int_expr | |
|
264 |
SHA of int_expr * int_expr | |
|
265 |
SHR of int_expr * int_expr | |
|
266 |
Add of int_expr * int_expr | |
|
267 |
Sub of int_expr * int_expr | |
|
268 |
Mult of int_expr * int_expr | |
|
269 |
Div of int_expr * int_expr | |
|
270 |
Mod of int_expr * int_expr | |
|
271 |
Cardinality of rel_expr | |
|
272 |
SetSum of rel_expr | |
|
273 |
BitOr of int_expr * int_expr | |
|
274 |
BitXor of int_expr * int_expr | |
|
275 |
BitAnd of int_expr * int_expr | |
|
276 |
BitNot of int_expr | |
|
277 |
Neg of int_expr | |
|
278 |
Absolute of int_expr | |
|
279 |
Signum of int_expr | |
|
280 |
Num of int | |
|
281 |
IntReg of int |
|
282 |
and decl = |
|
283 |
DeclNo of n_ary_index * rel_expr | |
|
284 |
DeclLone of n_ary_index * rel_expr | |
|
285 |
DeclOne of n_ary_index * rel_expr | |
|
286 |
DeclSome of n_ary_index * rel_expr | |
|
287 |
DeclSet of n_ary_index * rel_expr |
|
288 |
and expr_assign = |
|
289 |
AssignFormulaReg of int * formula | |
|
290 |
AssignRelReg of n_ary_index * rel_expr | |
|
291 |
AssignIntReg of int * int_expr |
|
292 |
||
293 |
type problem = { |
|
294 |
comment: string, |
|
295 |
settings: setting list, |
|
296 |
univ_card: int, |
|
297 |
tuple_assigns: tuple_assign list, |
|
298 |
bounds: bound list, |
|
299 |
int_bounds: int_bound list, |
|
300 |
expr_assigns: expr_assign list, |
|
301 |
formula: formula} |
|
302 |
||
303 |
type raw_bound = n_ary_index * int list list |
|
304 |
||
305 |
datatype outcome = |
|
33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset
|
306 |
NotInstalled | |
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
307 |
Normal of (int * raw_bound list) list * int list * string | |
33192 | 308 |
TimedOut of int list | |
309 |
Interrupted of int list option | |
|
310 |
Error of string * int list |
|
311 |
||
312 |
exception SYNTAX of string * string |
|
313 |
||
314 |
type 'a fold_expr_funcs = { |
|
315 |
formula_func: formula -> 'a -> 'a, |
|
316 |
rel_expr_func: rel_expr -> 'a -> 'a, |
|
317 |
int_expr_func: int_expr -> 'a -> 'a |
|
318 |
} |
|
319 |
||
320 |
(* 'a fold_expr_funcs -> formula -> 'a -> 'a *) |
|
321 |
fun fold_formula (F : 'a fold_expr_funcs) formula = |
|
322 |
case formula of |
|
323 |
All (ds, f) => fold (fold_decl F) ds #> fold_formula F f |
|
324 |
| Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f |
|
325 |
| FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f |
|
326 |
| FormulaIf (f, f1, f2) => |
|
327 |
fold_formula F f #> fold_formula F f1 #> fold_formula F f2 |
|
328 |
| Or (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
329 |
| Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
330 |
| Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
331 |
| And (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
332 |
| Not f => fold_formula F f |
|
333 |
| Acyclic x => fold_rel_expr F (Rel x) |
|
334 |
| Function (x, r1, r2) => |
|
335 |
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
336 |
| Functional (x, r1, r2) => |
|
337 |
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
338 |
| TotalOrdering (x1, x2, x3, x4) => |
|
339 |
fold_rel_expr F (Rel x1) #> fold_rel_expr F (Rel x2) |
|
340 |
#> fold_rel_expr F (Rel x3) #> fold_rel_expr F (Rel x4) |
|
341 |
| Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
342 |
| RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
343 |
| IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
344 |
| LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
345 |
| LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
346 |
| No r => fold_rel_expr F r |
|
347 |
| Lone r => fold_rel_expr F r |
|
348 |
| One r => fold_rel_expr F r |
|
349 |
| Some r => fold_rel_expr F r |
|
350 |
| False => #formula_func F formula |
|
351 |
| True => #formula_func F formula |
|
352 |
| FormulaReg _ => #formula_func F formula |
|
353 |
(* 'a fold_expr_funcs -> rel_expr -> 'a -> 'a *) |
|
354 |
and fold_rel_expr F rel_expr = |
|
355 |
case rel_expr of |
|
356 |
RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r |
|
357 |
| RelIf (f, r1, r2) => |
|
358 |
fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
359 |
| Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
360 |
| Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
361 |
| Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
362 |
| Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
363 |
| Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
364 |
| IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
365 |
| Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is |
|
366 |
| Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
367 |
| Closure r => fold_rel_expr F r |
|
368 |
| ReflexiveClosure r => fold_rel_expr F r |
|
369 |
| Transpose r => fold_rel_expr F r |
|
370 |
| Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f |
|
371 |
| Bits i => fold_int_expr F i |
|
372 |
| Int i => fold_int_expr F i |
|
373 |
| Iden => #rel_expr_func F rel_expr |
|
374 |
| Ints => #rel_expr_func F rel_expr |
|
375 |
| None => #rel_expr_func F rel_expr |
|
376 |
| Univ => #rel_expr_func F rel_expr |
|
377 |
| Atom _ => #rel_expr_func F rel_expr |
|
378 |
| AtomSeq _ => #rel_expr_func F rel_expr |
|
379 |
| Rel _ => #rel_expr_func F rel_expr |
|
380 |
| Var _ => #rel_expr_func F rel_expr |
|
381 |
| RelReg _ => #rel_expr_func F rel_expr |
|
382 |
(* 'a fold_expr_funcs -> int_expr -> 'a -> 'a *) |
|
383 |
and fold_int_expr F int_expr = |
|
384 |
case int_expr of |
|
385 |
Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i |
|
386 |
| IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i |
|
387 |
| IntIf (f, i1, i2) => |
|
388 |
fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2 |
|
389 |
| SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
390 |
| SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
391 |
| SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
392 |
| Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
393 |
| Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
394 |
| Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
395 |
| Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
396 |
| Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
397 |
| Cardinality r => fold_rel_expr F r |
|
398 |
| SetSum r => fold_rel_expr F r |
|
399 |
| BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
400 |
| BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
401 |
| BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
402 |
| BitNot i => fold_int_expr F i |
|
403 |
| Neg i => fold_int_expr F i |
|
404 |
| Absolute i => fold_int_expr F i |
|
405 |
| Signum i => fold_int_expr F i |
|
406 |
| Num _ => #int_expr_func F int_expr |
|
407 |
| IntReg _ => #int_expr_func F int_expr |
|
408 |
(* 'a fold_expr_funcs -> decl -> 'a -> 'a *) |
|
409 |
and fold_decl F decl = |
|
410 |
case decl of |
|
411 |
DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
412 |
| DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
413 |
| DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
414 |
| DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
415 |
| DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
416 |
(* 'a fold_expr_funcs -> expr_assign -> 'a -> 'a *) |
|
417 |
and fold_expr_assign F assign = |
|
418 |
case assign of |
|
419 |
AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f |
|
420 |
| AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r |
|
421 |
| AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i |
|
422 |
||
423 |
type 'a fold_tuple_funcs = { |
|
424 |
tuple_func: tuple -> 'a -> 'a, |
|
425 |
tuple_set_func: tuple_set -> 'a -> 'a |
|
426 |
} |
|
427 |
||
428 |
(* 'a fold_tuple_funcs -> tuple -> 'a -> 'a *) |
|
429 |
fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F |
|
430 |
(* 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a *) |
|
431 |
fun fold_tuple_set F tuple_set = |
|
432 |
case tuple_set of |
|
433 |
TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
434 |
| TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
435 |
| TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
436 |
| TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
437 |
| TupleProject (ts, _) => fold_tuple_set F ts |
|
438 |
| TupleSet ts => fold (fold_tuple F) ts |
|
439 |
| TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 |
|
440 |
| TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 |
|
441 |
| TupleAtomSeq _ => #tuple_set_func F tuple_set |
|
442 |
| TupleSetReg _ => #tuple_set_func F tuple_set |
|
443 |
(* 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a *) |
|
444 |
fun fold_tuple_assign F assign = |
|
445 |
case assign of |
|
446 |
AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t |
|
447 |
| AssignTupleSet (x, ts) => |
|
448 |
fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts |
|
449 |
(* 'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a *) |
|
450 |
fun fold_bound expr_F tuple_F (zs, tss) = |
|
451 |
fold (fold_rel_expr expr_F) (map (Rel o fst) zs) |
|
452 |
#> fold (fold_tuple_set tuple_F) tss |
|
453 |
(* 'a fold_tuple_funcs -> int_bound -> 'a -> 'a *) |
|
454 |
fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss |
|
455 |
||
456 |
(* int -> int *) |
|
457 |
fun max_arity univ_card = floor (Math.ln 2147483647.0 |
|
458 |
/ Math.ln (Real.fromInt univ_card)) |
|
459 |
(* rel_expr -> int *) |
|
460 |
fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r |
|
461 |
| arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1 |
|
462 |
| arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1 |
|
463 |
| arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1 |
|
464 |
| arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1 |
|
465 |
| arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1 |
|
466 |
| arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2 |
|
467 |
| arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35187
diff
changeset
|
468 |
| arity_of_rel_expr (Project (_, is)) = length is |
33192 | 469 |
| arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2 |
470 |
| arity_of_rel_expr (Closure _) = 2 |
|
471 |
| arity_of_rel_expr (ReflexiveClosure _) = 2 |
|
472 |
| arity_of_rel_expr (Transpose _) = 2 |
|
473 |
| arity_of_rel_expr (Comprehension (ds, _)) = |
|
474 |
fold (curry op + o arity_of_decl) ds 0 |
|
475 |
| arity_of_rel_expr (Bits _) = 1 |
|
476 |
| arity_of_rel_expr (Int _) = 1 |
|
477 |
| arity_of_rel_expr Iden = 2 |
|
478 |
| arity_of_rel_expr Ints = 1 |
|
479 |
| arity_of_rel_expr None = 1 |
|
480 |
| arity_of_rel_expr Univ = 1 |
|
481 |
| arity_of_rel_expr (Atom _) = 1 |
|
482 |
| arity_of_rel_expr (AtomSeq _) = 1 |
|
483 |
| arity_of_rel_expr (Rel (n, _)) = n |
|
484 |
| arity_of_rel_expr (Var (n, _)) = n |
|
485 |
| arity_of_rel_expr (RelReg (n, _)) = n |
|
486 |
(* rel_expr -> rel_expr -> int *) |
|
487 |
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2 |
|
488 |
(* decl -> int *) |
|
489 |
and arity_of_decl (DeclNo ((n, _), _)) = n |
|
490 |
| arity_of_decl (DeclLone ((n, _), _)) = n |
|
491 |
| arity_of_decl (DeclOne ((n, _), _)) = n |
|
492 |
| arity_of_decl (DeclSome ((n, _), _)) = n |
|
493 |
| arity_of_decl (DeclSet ((n, _), _)) = n |
|
494 |
||
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
495 |
(* problem -> bool *) |
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
496 |
fun is_problem_trivially_false ({formula = False, ...} : problem) = true |
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
497 |
| is_problem_trivially_false _ = false |
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
498 |
|
33192 | 499 |
(* string -> bool *) |
500 |
val is_relevant_setting = not o member (op =) ["solver", "delay"] |
|
501 |
||
502 |
(* problem -> problem -> bool *) |
|
503 |
fun problems_equivalent (p1 : problem) (p2 : problem) = |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
504 |
#univ_card p1 = #univ_card p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
505 |
#formula p1 = #formula p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
506 |
#bounds p1 = #bounds p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
507 |
#expr_assigns p1 = #expr_assigns p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
508 |
#tuple_assigns p1 = #tuple_assigns p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
509 |
#int_bounds p1 = #int_bounds p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
510 |
filter (is_relevant_setting o fst) (#settings p1) |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
511 |
= filter (is_relevant_setting o fst) (#settings p2) |
33192 | 512 |
|
34998 | 513 |
val created_temp_dir = Unsynchronized.ref false |
514 |
||
515 |
(* bool -> string * string *) |
|
516 |
fun serial_string_and_temporary_dir_for_overlord overlord = |
|
517 |
if overlord then |
|
518 |
("", getenv "ISABELLE_HOME_USER") |
|
519 |
else |
|
520 |
let |
|
521 |
val dir = getenv "ISABELLE_TMP" |
|
522 |
val _ = if !created_temp_dir then () |
|
523 |
else (created_temp_dir := true; File.mkdir (Path.explode dir)) |
|
524 |
in (serial_string (), dir) end |
|
525 |
||
33192 | 526 |
(* int -> string *) |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
527 |
fun base_name j = |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
528 |
if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j |
33192 | 529 |
|
530 |
(* n_ary_index -> string -> string -> string -> string *) |
|
531 |
fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j |
|
532 |
| n_ary_name (2, j) _ prefix _ = prefix ^ base_name j |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
533 |
| n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j |
33192 | 534 |
|
535 |
(* int -> string *) |
|
536 |
fun atom_name j = "A" ^ base_name j |
|
537 |
fun atom_seq_name (k, 0) = "u" ^ base_name k |
|
538 |
| atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0 |
|
539 |
fun formula_reg_name j = "$f" ^ base_name j |
|
540 |
fun rel_reg_name j = "$e" ^ base_name j |
|
541 |
fun int_reg_name j = "$i" ^ base_name j |
|
542 |
||
543 |
(* n_ary_index -> string *) |
|
544 |
fun tuple_name x = n_ary_name x "A" "P" "T" |
|
545 |
fun rel_name x = n_ary_name x "s" "r" "m" |
|
546 |
fun var_name x = n_ary_name x "S" "R" "M" |
|
547 |
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T" |
|
548 |
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t" |
|
549 |
||
550 |
(* string -> string *) |
|
551 |
fun inline_comment "" = "" |
|
552 |
| inline_comment comment = |
|
553 |
" /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^ |
|
554 |
" */" |
|
555 |
fun block_comment "" = "" |
|
556 |
| block_comment comment = prefix_lines "// " comment ^ "\n" |
|
557 |
||
558 |
(* (n_ary_index * string) -> string *) |
|
559 |
fun commented_rel_name (x, s) = rel_name x ^ inline_comment s |
|
560 |
||
561 |
(* tuple -> string *) |
|
562 |
fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]" |
|
563 |
| string_for_tuple (TupleIndex x) = tuple_name x |
|
564 |
| string_for_tuple (TupleReg x) = tuple_reg_name x |
|
565 |
||
566 |
val no_prec = 100 |
|
567 |
val prec_TupleUnion = 1 |
|
568 |
val prec_TupleIntersect = 2 |
|
569 |
val prec_TupleProduct = 3 |
|
570 |
val prec_TupleProject = 4 |
|
571 |
||
572 |
(* tuple_set -> int *) |
|
573 |
fun precedence_ts (TupleUnion _) = prec_TupleUnion |
|
574 |
| precedence_ts (TupleDifference _) = prec_TupleUnion |
|
575 |
| precedence_ts (TupleIntersect _) = prec_TupleIntersect |
|
576 |
| precedence_ts (TupleProduct _) = prec_TupleProduct |
|
577 |
| precedence_ts (TupleProject _) = prec_TupleProject |
|
578 |
| precedence_ts _ = no_prec |
|
579 |
||
580 |
(* tuple_set -> string *) |
|
581 |
fun string_for_tuple_set tuple_set = |
|
582 |
let |
|
583 |
(* tuple_set -> int -> string *) |
|
584 |
fun sub tuple_set outer_prec = |
|
585 |
let |
|
586 |
val prec = precedence_ts tuple_set |
|
587 |
val need_parens = (prec < outer_prec) |
|
588 |
in |
|
589 |
(if need_parens then "(" else "") ^ |
|
590 |
(case tuple_set of |
|
591 |
TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1) |
|
592 |
| TupleDifference (ts1, ts2) => |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35187
diff
changeset
|
593 |
sub ts1 prec ^ " - " ^ sub ts2 (prec + 1) |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35187
diff
changeset
|
594 |
| TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec |
33192 | 595 |
| TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
596 |
| TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]" |
33192 | 597 |
| TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}" |
598 |
| TupleRange (t1, t2) => |
|
599 |
"{" ^ string_for_tuple t1 ^ |
|
600 |
(if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}" |
|
601 |
| TupleArea (t1, t2) => |
|
602 |
"{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}" |
|
603 |
| TupleAtomSeq x => atom_seq_name x |
|
604 |
| TupleSetReg x => tuple_set_reg_name x) ^ |
|
605 |
(if need_parens then ")" else "") |
|
606 |
end |
|
607 |
in sub tuple_set 0 end |
|
608 |
||
609 |
(* tuple_assign -> string *) |
|
610 |
fun string_for_tuple_assign (AssignTuple (x, t)) = |
|
611 |
tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n" |
|
612 |
| string_for_tuple_assign (AssignTupleSet (x, ts)) = |
|
613 |
tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n" |
|
614 |
||
615 |
(* bound -> string *) |
|
616 |
fun string_for_bound (zs, tss) = |
|
617 |
"bounds " ^ commas (map commented_rel_name zs) ^ ": " ^ |
|
618 |
(if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^ |
|
619 |
(if length tss = 1 then "" else "]") ^ "\n" |
|
620 |
||
621 |
(* int_bound -> string *) |
|
622 |
fun int_string_for_bound (opt_n, tss) = |
|
623 |
(case opt_n of |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
624 |
SOME n => signed_string_of_int n ^ ": " |
33192 | 625 |
| NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]" |
626 |
||
627 |
val prec_All = 1 |
|
628 |
val prec_Or = 2 |
|
629 |
val prec_Iff = 3 |
|
630 |
val prec_Implies = 4 |
|
631 |
val prec_And = 5 |
|
632 |
val prec_Not = 6 |
|
633 |
val prec_Eq = 7 |
|
634 |
val prec_Some = 8 |
|
635 |
val prec_SHL = 9 |
|
636 |
val prec_Add = 10 |
|
637 |
val prec_Mult = 11 |
|
638 |
val prec_Override = 12 |
|
639 |
val prec_Intersect = 13 |
|
640 |
val prec_Product = 14 |
|
641 |
val prec_IfNo = 15 |
|
642 |
val prec_Project = 17 |
|
643 |
val prec_Join = 18 |
|
644 |
val prec_BitNot = 19 |
|
645 |
||
646 |
(* formula -> int *) |
|
647 |
fun precedence_f (All _) = prec_All |
|
648 |
| precedence_f (Exist _) = prec_All |
|
649 |
| precedence_f (FormulaLet _) = prec_All |
|
650 |
| precedence_f (FormulaIf _) = prec_All |
|
651 |
| precedence_f (Or _) = prec_Or |
|
652 |
| precedence_f (Iff _) = prec_Iff |
|
653 |
| precedence_f (Implies _) = prec_Implies |
|
654 |
| precedence_f (And _) = prec_And |
|
655 |
| precedence_f (Not _) = prec_Not |
|
656 |
| precedence_f (Acyclic _) = no_prec |
|
657 |
| precedence_f (Function _) = no_prec |
|
658 |
| precedence_f (Functional _) = no_prec |
|
659 |
| precedence_f (TotalOrdering _) = no_prec |
|
660 |
| precedence_f (Subset _) = prec_Eq |
|
661 |
| precedence_f (RelEq _) = prec_Eq |
|
662 |
| precedence_f (IntEq _) = prec_Eq |
|
663 |
| precedence_f (LT _) = prec_Eq |
|
664 |
| precedence_f (LE _) = prec_Eq |
|
665 |
| precedence_f (No _) = prec_Some |
|
666 |
| precedence_f (Lone _) = prec_Some |
|
667 |
| precedence_f (One _) = prec_Some |
|
668 |
| precedence_f (Some _) = prec_Some |
|
669 |
| precedence_f False = no_prec |
|
670 |
| precedence_f True = no_prec |
|
671 |
| precedence_f (FormulaReg _) = no_prec |
|
672 |
(* rel_expr -> int *) |
|
673 |
and precedence_r (RelLet _) = prec_All |
|
674 |
| precedence_r (RelIf _) = prec_All |
|
675 |
| precedence_r (Union _) = prec_Add |
|
676 |
| precedence_r (Difference _) = prec_Add |
|
677 |
| precedence_r (Override _) = prec_Override |
|
678 |
| precedence_r (Intersect _) = prec_Intersect |
|
679 |
| precedence_r (Product _) = prec_Product |
|
680 |
| precedence_r (IfNo _) = prec_IfNo |
|
681 |
| precedence_r (Project _) = prec_Project |
|
682 |
| precedence_r (Join _) = prec_Join |
|
683 |
| precedence_r (Closure _) = prec_BitNot |
|
684 |
| precedence_r (ReflexiveClosure _) = prec_BitNot |
|
685 |
| precedence_r (Transpose _) = prec_BitNot |
|
686 |
| precedence_r (Comprehension _) = no_prec |
|
687 |
| precedence_r (Bits _) = no_prec |
|
688 |
| precedence_r (Int _) = no_prec |
|
689 |
| precedence_r Iden = no_prec |
|
690 |
| precedence_r Ints = no_prec |
|
691 |
| precedence_r None = no_prec |
|
692 |
| precedence_r Univ = no_prec |
|
693 |
| precedence_r (Atom _) = no_prec |
|
694 |
| precedence_r (AtomSeq _) = no_prec |
|
695 |
| precedence_r (Rel _) = no_prec |
|
696 |
| precedence_r (Var _) = no_prec |
|
697 |
| precedence_r (RelReg _) = no_prec |
|
698 |
(* int_expr -> int *) |
|
699 |
and precedence_i (Sum _) = prec_All |
|
700 |
| precedence_i (IntLet _) = prec_All |
|
701 |
| precedence_i (IntIf _) = prec_All |
|
702 |
| precedence_i (SHL _) = prec_SHL |
|
703 |
| precedence_i (SHA _) = prec_SHL |
|
704 |
| precedence_i (SHR _) = prec_SHL |
|
705 |
| precedence_i (Add _) = prec_Add |
|
706 |
| precedence_i (Sub _) = prec_Add |
|
707 |
| precedence_i (Mult _) = prec_Mult |
|
708 |
| precedence_i (Div _) = prec_Mult |
|
709 |
| precedence_i (Mod _) = prec_Mult |
|
710 |
| precedence_i (Cardinality _) = no_prec |
|
711 |
| precedence_i (SetSum _) = no_prec |
|
712 |
| precedence_i (BitOr _) = prec_Intersect |
|
713 |
| precedence_i (BitXor _) = prec_Intersect |
|
714 |
| precedence_i (BitAnd _) = prec_Intersect |
|
715 |
| precedence_i (BitNot _) = prec_BitNot |
|
716 |
| precedence_i (Neg _) = prec_BitNot |
|
717 |
| precedence_i (Absolute _) = prec_BitNot |
|
718 |
| precedence_i (Signum _) = prec_BitNot |
|
719 |
| precedence_i (Num _) = no_prec |
|
720 |
| precedence_i (IntReg _) = no_prec |
|
721 |
||
722 |
(* (string -> unit) -> problem list -> unit *) |
|
723 |
fun write_problem_file out problems = |
|
724 |
let |
|
725 |
(* formula -> unit *) |
|
726 |
fun out_outmost_f (And (f1, f2)) = |
|
727 |
(out_outmost_f f1; out "\n && "; out_outmost_f f2) |
|
728 |
| out_outmost_f f = out_f f prec_And |
|
729 |
(* formula -> int -> unit *) |
|
730 |
and out_f formula outer_prec = |
|
731 |
let |
|
732 |
val prec = precedence_f formula |
|
733 |
val need_parens = (prec < outer_prec) |
|
734 |
in |
|
735 |
(if need_parens then out "(" else ()); |
|
736 |
(case formula of |
|
737 |
All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec) |
|
738 |
| Exist (ds, f) => |
|
739 |
(out "some ["; out_decls ds; out "] | "; out_f f prec) |
|
740 |
| FormulaLet (bs, f) => |
|
741 |
(out "let ["; out_assigns bs; out "] | "; out_f f prec) |
|
742 |
| FormulaIf (f, f1, f2) => |
|
743 |
(out "if "; out_f f prec; out " then "; out_f f1 prec; out " else "; |
|
744 |
out_f f2 prec) |
|
745 |
| Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec) |
|
746 |
| Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec) |
|
747 |
| Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec) |
|
748 |
| And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec) |
|
749 |
| Not f => (out "! "; out_f f prec) |
|
750 |
| Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")") |
|
751 |
| Function (x, r1, r2) => |
|
752 |
(out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one "; |
|
753 |
out_r r2 0; out ")") |
|
754 |
| Functional (x, r1, r2) => |
|
755 |
(out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone "; |
|
756 |
out_r r2 0; out ")") |
|
757 |
| TotalOrdering (x1, x2, x3, x4) => |
|
758 |
out ("TOTAL_ORDERING(" ^ rel_name x1 ^ ", " ^ rel_name x2 ^ ", " |
|
759 |
^ rel_name x3 ^ ", " ^ rel_name x4 ^ ")") |
|
760 |
| Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec) |
|
761 |
| RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec) |
|
762 |
| IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec) |
|
763 |
| LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec) |
|
764 |
| LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec) |
|
765 |
| No r => (out "no "; out_r r prec) |
|
766 |
| Lone r => (out "lone "; out_r r prec) |
|
767 |
| One r => (out "one "; out_r r prec) |
|
768 |
| Some r => (out "some "; out_r r prec) |
|
769 |
| False => out "false" |
|
770 |
| True => out "true" |
|
771 |
| FormulaReg j => out (formula_reg_name j)); |
|
772 |
(if need_parens then out ")" else ()) |
|
773 |
end |
|
774 |
(* rel_expr -> int -> unit *) |
|
775 |
and out_r rel_expr outer_prec = |
|
776 |
let |
|
777 |
val prec = precedence_r rel_expr |
|
778 |
val need_parens = (prec < outer_prec) |
|
779 |
in |
|
780 |
(if need_parens then out "(" else ()); |
|
781 |
(case rel_expr of |
|
782 |
RelLet (bs, r) => |
|
783 |
(out "let ["; out_assigns bs; out "] | "; out_r r prec) |
|
784 |
| RelIf (f, r1, r2) => |
|
785 |
(out "if "; out_f f prec; out " then "; out_r r1 prec; |
|
786 |
out " else "; out_r r2 prec) |
|
787 |
| Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1)) |
|
788 |
| Difference (r1, r2) => |
|
789 |
(out_r r1 prec; out " - "; out_r r2 (prec + 1)) |
|
790 |
| Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec) |
|
791 |
| Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec) |
|
792 |
| Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec) |
|
793 |
| IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec) |
|
794 |
| Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]") |
|
795 |
| Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1)) |
|
796 |
| Closure r => (out "^"; out_r r prec) |
|
797 |
| ReflexiveClosure r => (out "*"; out_r r prec) |
|
798 |
| Transpose r => (out "~"; out_r r prec) |
|
799 |
| Comprehension (ds, f) => |
|
800 |
(out "{["; out_decls ds; out "] | "; out_f f 0; out "}") |
|
801 |
| Bits i => (out "Bits["; out_i i 0; out "]") |
|
802 |
| Int i => (out "Int["; out_i i 0; out "]") |
|
803 |
| Iden => out "iden" |
|
804 |
| Ints => out "ints" |
|
805 |
| None => out "none" |
|
806 |
| Univ => out "univ" |
|
807 |
| Atom j => out (atom_name j) |
|
808 |
| AtomSeq x => out (atom_seq_name x) |
|
809 |
| Rel x => out (rel_name x) |
|
810 |
| Var x => out (var_name x) |
|
811 |
| RelReg (_, j) => out (rel_reg_name j)); |
|
812 |
(if need_parens then out ")" else ()) |
|
813 |
end |
|
814 |
(* int_expr -> int -> unit *) |
|
815 |
and out_i int_expr outer_prec = |
|
816 |
let |
|
817 |
val prec = precedence_i int_expr |
|
818 |
val need_parens = (prec < outer_prec) |
|
819 |
in |
|
820 |
(if need_parens then out "(" else ()); |
|
821 |
(case int_expr of |
|
822 |
Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec) |
|
823 |
| IntLet (bs, i) => |
|
824 |
(out "let ["; out_assigns bs; out "] | "; out_i i prec) |
|
825 |
| IntIf (f, i1, i2) => |
|
826 |
(out "if "; out_f f prec; out " then "; out_i i1 prec; |
|
827 |
out " else "; out_i i2 prec) |
|
828 |
| SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1)) |
|
829 |
| SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1)) |
|
830 |
| SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1)) |
|
831 |
| Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1)) |
|
832 |
| Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1)) |
|
833 |
| Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1)) |
|
834 |
| Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1)) |
|
835 |
| Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1)) |
|
836 |
| Cardinality r => (out "#("; out_r r 0; out ")") |
|
837 |
| SetSum r => (out "sum("; out_r r 0; out ")") |
|
838 |
| BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec) |
|
839 |
| BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec) |
|
840 |
| BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec) |
|
841 |
| BitNot i => (out "~"; out_i i prec) |
|
842 |
| Neg i => (out "-"; out_i i prec) |
|
843 |
| Absolute i => (out "abs "; out_i i prec) |
|
844 |
| Signum i => (out "sgn "; out_i i prec) |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
845 |
| Num k => out (signed_string_of_int k) |
33192 | 846 |
| IntReg j => out (int_reg_name j)); |
847 |
(if need_parens then out ")" else ()) |
|
848 |
end |
|
849 |
(* decl list -> unit *) |
|
850 |
and out_decls [] = () |
|
851 |
| out_decls [d] = out_decl d |
|
852 |
| out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds) |
|
853 |
(* decl -> unit *) |
|
854 |
and out_decl (DeclNo (x, r)) = |
|
855 |
(out (var_name x); out " : no "; out_r r 0) |
|
856 |
| out_decl (DeclLone (x, r)) = |
|
857 |
(out (var_name x); out " : lone "; out_r r 0) |
|
858 |
| out_decl (DeclOne (x, r)) = |
|
859 |
(out (var_name x); out " : one "; out_r r 0) |
|
860 |
| out_decl (DeclSome (x, r)) = |
|
861 |
(out (var_name x); out " : some "; out_r r 0) |
|
862 |
| out_decl (DeclSet (x, r)) = |
|
863 |
(out (var_name x); out " : set "; out_r r 0) |
|
864 |
(* assign_expr list -> unit *) |
|
865 |
and out_assigns [] = () |
|
866 |
| out_assigns [b] = out_assign b |
|
867 |
| out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs) |
|
868 |
(* assign_expr -> unit *) |
|
869 |
and out_assign (AssignFormulaReg (j, f)) = |
|
870 |
(out (formula_reg_name j); out " := "; out_f f 0) |
|
871 |
| out_assign (AssignRelReg ((_, j), r)) = |
|
872 |
(out (rel_reg_name j); out " := "; out_r r 0) |
|
873 |
| out_assign (AssignIntReg (j, i)) = |
|
874 |
(out (int_reg_name j); out " := "; out_i i 0) |
|
875 |
(* int_expr list -> unit *) |
|
876 |
and out_columns [] = () |
|
877 |
| out_columns [i] = out_i i 0 |
|
878 |
| out_columns (i :: is) = (out_i i 0; out ", "; out_columns is) |
|
879 |
(* problem -> unit *) |
|
880 |
and out_problem {comment, settings, univ_card, tuple_assigns, bounds, |
|
881 |
int_bounds, expr_assigns, formula} = |
|
882 |
(out ("\n" ^ block_comment comment ^ |
|
883 |
implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n") |
|
884 |
settings) ^ |
|
885 |
"univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^ |
|
886 |
implode (map string_for_tuple_assign tuple_assigns) ^ |
|
887 |
implode (map string_for_bound bounds) ^ |
|
888 |
(if int_bounds = [] then |
|
889 |
"" |
|
890 |
else |
|
891 |
"int_bounds: " ^ |
|
892 |
commas (map int_string_for_bound int_bounds) ^ "\n")); |
|
893 |
map (fn b => (out_assign b; out ";")) expr_assigns; |
|
894 |
out "solve "; out_outmost_f formula; out ";\n") |
|
895 |
in |
|
896 |
out ("// This file was generated by Isabelle (probably Nitpick)\n" ^ |
|
897 |
"// " ^ Date.fmt "%Y-%m-%d %H:%M:%S" |
|
898 |
(Date.fromTimeLocal (Time.now ())) ^ "\n"); |
|
899 |
map out_problem problems |
|
900 |
end |
|
901 |
||
902 |
(* string -> bool *) |
|
903 |
fun is_ident_char s = |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
904 |
Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
905 |
s = "_" orelse s = "'" orelse s = "$" |
33192 | 906 |
|
907 |
(* string list -> string list *) |
|
908 |
fun strip_blanks [] = [] |
|
909 |
| strip_blanks (" " :: ss) = strip_blanks ss |
|
910 |
| strip_blanks [s1, " "] = [s1] |
|
911 |
| strip_blanks (s1 :: " " :: s2 :: ss) = |
|
912 |
if is_ident_char s1 andalso is_ident_char s2 then |
|
913 |
s1 :: " " :: strip_blanks (s2 :: ss) |
|
914 |
else |
|
915 |
strip_blanks (s1 :: s2 :: ss) |
|
916 |
| strip_blanks (s :: ss) = s :: strip_blanks ss |
|
917 |
||
918 |
(* (string list -> 'a * string list) -> string list -> 'a list * string list *) |
|
919 |
fun scan_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan) |
|
920 |
fun scan_list scan = scan_non_empty_list scan || Scan.succeed [] |
|
921 |
(* string list -> int * string list *) |
|
922 |
val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) |
|
923 |
>> (the o Int.fromString o space_implode "") |
|
924 |
(* string list -> (int * int) * string list *) |
|
925 |
val scan_rel_name = $$ "s" |-- scan_nat >> pair 1 |
|
926 |
|| $$ "r" |-- scan_nat >> pair 2 |
|
927 |
|| ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat |
|
928 |
(* string list -> int * string list *) |
|
929 |
val scan_atom = $$ "A" |-- scan_nat |
|
930 |
(* string list -> int list * string list *) |
|
931 |
val scan_tuple = $$ "[" |-- scan_list scan_atom --| $$ "]" |
|
932 |
(* string list -> int list list * string list *) |
|
933 |
val scan_tuple_set = $$ "[" |-- scan_list scan_tuple --| $$ "]" |
|
934 |
(* string list -> ((int * int) * int list list) * string list *) |
|
935 |
val scan_assignment = (scan_rel_name --| $$ "=") -- scan_tuple_set |
|
936 |
(* string list -> ((int * int) * int list list) list * string list *) |
|
937 |
val scan_instance = Scan.this_string "relations:" |-- |
|
938 |
$$ "{" |-- scan_list scan_assignment --| $$ "}" |
|
939 |
||
940 |
(* string -> raw_bound list *) |
|
941 |
fun parse_instance inst = |
|
942 |
Scan.finite Symbol.stopper |
|
943 |
(Scan.error (!! (fn _ => raise SYNTAX ("Kodkod.parse_instance", |
|
944 |
"ill-formed Kodkodi output")) |
|
945 |
scan_instance)) |
|
946 |
(strip_blanks (explode inst)) |
|
947 |
|> fst |
|
948 |
||
949 |
val problem_marker = "*** PROBLEM " |
|
950 |
val outcome_marker = "---OUTCOME---\n" |
|
951 |
val instance_marker = "---INSTANCE---\n" |
|
952 |
||
953 |
(* string -> substring -> string *) |
|
954 |
fun read_section_body marker = |
|
955 |
Substring.string o fst o Substring.position "\n\n" |
|
956 |
o Substring.triml (size marker) |
|
957 |
||
958 |
(* substring -> raw_bound list *) |
|
959 |
fun read_next_instance s = |
|
960 |
let val s = Substring.position instance_marker s |> snd in |
|
961 |
if Substring.isEmpty s then |
|
962 |
raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker") |
|
963 |
else |
|
964 |
read_section_body instance_marker s |> parse_instance |
|
965 |
end |
|
966 |
||
967 |
(* int -> substring * (int * raw_bound list) list * int list |
|
968 |
-> substring * (int * raw_bound list) list * int list *) |
|
969 |
fun read_next_outcomes j (s, ps, js) = |
|
970 |
let val (s1, s2) = Substring.position outcome_marker s in |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
971 |
if Substring.isEmpty s2 orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
972 |
not (Substring.isEmpty (Substring.position problem_marker s1 |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
973 |
|> snd)) then |
33192 | 974 |
(s, ps, js) |
975 |
else |
|
976 |
let |
|
977 |
val outcome = read_section_body outcome_marker s2 |
|
978 |
val s = Substring.triml (size outcome_marker) s2 |
|
979 |
in |
|
980 |
if String.isSuffix "UNSATISFIABLE" outcome then |
|
981 |
read_next_outcomes j (s, ps, j :: js) |
|
982 |
else if String.isSuffix "SATISFIABLE" outcome then |
|
983 |
read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js) |
|
984 |
else |
|
985 |
raise SYNTAX ("Kodkod.read_next_outcomes", |
|
986 |
"unknown outcome " ^ quote outcome) |
|
987 |
end |
|
988 |
end |
|
989 |
||
990 |
(* substring * (int * raw_bound list) list * int list |
|
991 |
-> (int * raw_bound list) list * int list *) |
|
992 |
fun read_next_problems (s, ps, js) = |
|
993 |
let val s = Substring.position problem_marker s |> snd in |
|
994 |
if Substring.isEmpty s then |
|
995 |
(ps, js) |
|
996 |
else |
|
997 |
let |
|
998 |
val s = Substring.triml (size problem_marker) s |
|
999 |
val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string |
|
1000 |
|> Int.fromString |> the |
|
1001 |
val j = j_plus_1 - 1 |
|
1002 |
in read_next_problems (read_next_outcomes j (s, ps, js)) end |
|
1003 |
end |
|
1004 |
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems", |
|
1005 |
"expected number after \"PROBLEM\"") |
|
1006 |
||
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1007 |
(* Path.T -> bool * ((int * raw_bound list) list * int list) *) |
33192 | 1008 |
fun read_output_file path = |
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1009 |
(false, read_next_problems (Substring.full (File.read path), [], []) |
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1010 |
|>> rev ||> rev) |
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1011 |
handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], [])) |
33192 | 1012 |
|
1013 |
(* The fudge term below is to account for Kodkodi's slow start-up time, which |
|
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
34998
diff
changeset
|
1014 |
is partly due to the JVM and partly due to the ML "bash" function. *) |
33192 | 1015 |
val fudge_ms = 250 |
1016 |
||
1017 |
(* bool -> Time.time option -> int -> int -> problem list -> outcome *) |
|
1018 |
fun solve_any_problem overlord deadline max_threads max_solutions problems = |
|
1019 |
let |
|
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
1020 |
val j = find_index (curry (op =) True o #formula) problems |
33192 | 1021 |
val indexed_problems = if j >= 0 then |
1022 |
[(j, nth problems j)] |
|
1023 |
else |
|
35187
3acab6c90d4a
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
blanchet
parents:
35185
diff
changeset
|
1024 |
filter_out (is_problem_trivially_false o snd) |
3acab6c90d4a
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
blanchet
parents:
35185
diff
changeset
|
1025 |
(0 upto length problems - 1 ~~ problems) |
33192 | 1026 |
val triv_js = filter_out (AList.defined (op =) indexed_problems) |
1027 |
(0 upto length problems - 1) |
|
1028 |
(* int -> int *) |
|
1029 |
val reindex = fst o nth indexed_problems |
|
1030 |
in |
|
1031 |
if null indexed_problems then |
|
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1032 |
Normal ([], triv_js, "") |
33192 | 1033 |
else |
1034 |
let |
|
34998 | 1035 |
val (serial_str, temp_dir) = |
1036 |
serial_string_and_temporary_dir_for_overlord overlord |
|
1037 |
(* string -> Path.T *) |
|
1038 |
fun path_for suf = |
|
1039 |
Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) |
|
1040 |
val in_path = path_for "kki" |
|
33192 | 1041 |
val in_buf = Unsynchronized.ref Buffer.empty |
1042 |
(* string -> unit *) |
|
1043 |
fun out s = Unsynchronized.change in_buf (Buffer.add s) |
|
34998 | 1044 |
val out_path = path_for "out" |
1045 |
val err_path = path_for "err" |
|
33192 | 1046 |
val _ = write_problem_file out (map snd indexed_problems) |
1047 |
val _ = File.write_buffer in_path (!in_buf) |
|
33575
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1048 |
(* unit -> unit *) |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1049 |
fun remove_temporary_files () = |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1050 |
if overlord then () |
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1051 |
else List.app (K () o try File.rm) [in_path, out_path, err_path] |
33192 | 1052 |
in |
1053 |
let |
|
1054 |
val ms = |
|
1055 |
case deadline of |
|
1056 |
NONE => ~1 |
|
1057 |
| SOME time => |
|
1058 |
Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) |
|
1059 |
- fudge_ms) |
|
1060 |
val outcome = |
|
1061 |
let |
|
1062 |
val code = |
|
35011
9e55e87434ff
proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
wenzelm
parents:
35010
diff
changeset
|
1063 |
bash ("cd " ^ File.shell_quote temp_dir ^ ";\n" ^ |
35079 | 1064 |
"env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \ |
1065 |
\JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ |
|
1066 |
\$JAVA_LIBRARY_PATH\" \ |
|
1067 |
\LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ |
|
1068 |
\$LD_LIBRARY_PATH\" \ |
|
1069 |
\\"$KODKODI\"/bin/kodkodi" ^ |
|
1070 |
(if ms >= 0 then " -max-msecs " ^ string_of_int ms |
|
1071 |
else "") ^ |
|
1072 |
(if max_solutions > 1 then " -solve-all" else "") ^ |
|
1073 |
" -max-solutions " ^ string_of_int max_solutions ^ |
|
1074 |
(if max_threads > 0 then |
|
1075 |
" -max-threads " ^ string_of_int max_threads |
|
1076 |
else |
|
1077 |
"") ^ |
|
1078 |
" < " ^ File.shell_path in_path ^ |
|
1079 |
" > " ^ File.shell_path out_path ^ |
|
1080 |
" 2> " ^ File.shell_path err_path) |
|
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1081 |
val (io_error, (ps, nontriv_js)) = |
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1082 |
read_output_file out_path |
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1083 |
||> apfst (map (apfst reindex)) ||> apsnd (map reindex) |
33192 | 1084 |
val js = triv_js @ nontriv_js |
1085 |
val first_error = |
|
1086 |
File.fold_lines (fn line => fn "" => line | s => s) err_path "" |
|
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1087 |
handle IO.Io _ => "" | OS.SysErr _ => "" |
33192 | 1088 |
in |
1089 |
if null ps then |
|
1090 |
if code = 2 then |
|
1091 |
TimedOut js |
|
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1092 |
else if code = 0 then |
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1093 |
Normal ([], js, first_error) |
33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset
|
1094 |
else if first_error |> Substring.full |
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset
|
1095 |
|> Substring.position "NoClassDefFoundError" |> snd |
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset
|
1096 |
|> Substring.isEmpty |> not then |
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset
|
1097 |
NotInstalled |
33192 | 1098 |
else if first_error <> "" then |
1099 |
Error (first_error |> perhaps (try (unsuffix ".")) |
|
1100 |
|> perhaps (try (unprefix "Error: ")), js) |
|
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1101 |
else if io_error then |
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1102 |
Error ("I/O error", js) |
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1103 |
else |
33192 | 1104 |
Error ("Unknown error", js) |
1105 |
else |
|
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1106 |
Normal (ps, js, first_error) |
33192 | 1107 |
end |
33575
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1108 |
in remove_temporary_files (); outcome end |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1109 |
handle Exn.Interrupt => |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1110 |
let |
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1111 |
val nontriv_js = |
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1112 |
read_output_file out_path |> snd |> snd |> map reindex |
33575
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1113 |
in |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1114 |
(remove_temporary_files (); |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1115 |
Interrupted (SOME (triv_js @ nontriv_js))) |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1116 |
handle Exn.Interrupt => |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1117 |
(remove_temporary_files (); Interrupted NONE) |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1118 |
end |
33192 | 1119 |
end |
1120 |
end |
|
1121 |
||
1122 |
end; |