|
1 (* ========================================================================= *) |
|
2 (* RANDOM FINITE MODELS *) |
|
3 (* Copyright (c) 2003 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure Model :> Model = |
|
7 struct |
|
8 |
|
9 open Useful; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* Constants. *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 val maxSpace = 1000; |
|
16 |
|
17 (* ------------------------------------------------------------------------- *) |
|
18 (* Helper functions. *) |
|
19 (* ------------------------------------------------------------------------- *) |
|
20 |
|
21 val multInt = |
|
22 case Int.maxInt of |
|
23 NONE => (fn x => fn y => SOME (x * y)) |
|
24 | SOME m => |
|
25 let |
|
26 val m = Real.floor (Math.sqrt (Real.fromInt m)) |
|
27 in |
|
28 fn x => fn y => if x <= m andalso y <= m then SOME (x * y) else NONE |
|
29 end; |
|
30 |
|
31 local |
|
32 fun iexp x y acc = |
|
33 if y mod 2 = 0 then iexp' x y acc |
|
34 else |
|
35 case multInt acc x of |
|
36 SOME acc => iexp' x y acc |
|
37 | NONE => NONE |
|
38 |
|
39 and iexp' x y acc = |
|
40 if y = 1 then SOME acc |
|
41 else |
|
42 let |
|
43 val y = y div 2 |
|
44 in |
|
45 case multInt x x of |
|
46 SOME x => iexp x y acc |
|
47 | NONE => NONE |
|
48 end; |
|
49 in |
|
50 fun expInt x y = |
|
51 if y <= 1 then |
|
52 if y = 0 then SOME 1 |
|
53 else if y = 1 then SOME x |
|
54 else raise Bug "expInt: negative exponent" |
|
55 else if x <= 1 then |
|
56 if 0 <= x then SOME x |
|
57 else raise Bug "expInt: negative exponand" |
|
58 else iexp x y 1; |
|
59 end; |
|
60 |
|
61 fun boolToInt true = 1 |
|
62 | boolToInt false = 0; |
|
63 |
|
64 fun intToBool 1 = true |
|
65 | intToBool 0 = false |
|
66 | intToBool _ = raise Bug "Model.intToBool"; |
|
67 |
|
68 fun minMaxInterval i j = interval i (1 + j - i); |
|
69 |
|
70 (* ------------------------------------------------------------------------- *) |
|
71 (* Model size. *) |
|
72 (* ------------------------------------------------------------------------- *) |
|
73 |
|
74 type size = {size : int}; |
|
75 |
|
76 (* ------------------------------------------------------------------------- *) |
|
77 (* A model of size N has integer elements 0...N-1. *) |
|
78 (* ------------------------------------------------------------------------- *) |
|
79 |
|
80 type element = int; |
|
81 |
|
82 val zeroElement = 0; |
|
83 |
|
84 fun incrementElement {size = N} i = |
|
85 let |
|
86 val i = i + 1 |
|
87 in |
|
88 if i = N then NONE else SOME i |
|
89 end; |
|
90 |
|
91 fun elementListSpace {size = N} arity = |
|
92 case expInt N arity of |
|
93 NONE => NONE |
|
94 | s as SOME m => if m <= maxSpace then s else NONE; |
|
95 |
|
96 fun elementListIndex {size = N} = |
|
97 let |
|
98 fun f acc elts = |
|
99 case elts of |
|
100 [] => acc |
|
101 | elt :: elts => f (N * acc + elt) elts |
|
102 in |
|
103 f 0 |
|
104 end; |
|
105 |
|
106 (* ------------------------------------------------------------------------- *) |
|
107 (* The parts of the model that are fixed. *) |
|
108 (* ------------------------------------------------------------------------- *) |
|
109 |
|
110 type fixedFunction = size -> element list -> element option; |
|
111 |
|
112 type fixedRelation = size -> element list -> bool option; |
|
113 |
|
114 datatype fixed = |
|
115 Fixed of |
|
116 {functions : fixedFunction NameArityMap.map, |
|
117 relations : fixedRelation NameArityMap.map}; |
|
118 |
|
119 val uselessFixedFunction : fixedFunction = K (K NONE); |
|
120 |
|
121 val uselessFixedRelation : fixedRelation = K (K NONE); |
|
122 |
|
123 val emptyFunctions : fixedFunction NameArityMap.map = NameArityMap.new (); |
|
124 |
|
125 val emptyRelations : fixedRelation NameArityMap.map = NameArityMap.new (); |
|
126 |
|
127 fun fixed0 f sz elts = |
|
128 case elts of |
|
129 [] => f sz |
|
130 | _ => raise Bug "Model.fixed0: wrong arity"; |
|
131 |
|
132 fun fixed1 f sz elts = |
|
133 case elts of |
|
134 [x] => f sz x |
|
135 | _ => raise Bug "Model.fixed1: wrong arity"; |
|
136 |
|
137 fun fixed2 f sz elts = |
|
138 case elts of |
|
139 [x,y] => f sz x y |
|
140 | _ => raise Bug "Model.fixed2: wrong arity"; |
|
141 |
|
142 val emptyFixed = |
|
143 let |
|
144 val fns = emptyFunctions |
|
145 and rels = emptyRelations |
|
146 in |
|
147 Fixed |
|
148 {functions = fns, |
|
149 relations = rels} |
|
150 end; |
|
151 |
|
152 fun peekFunctionFixed fix name_arity = |
|
153 let |
|
154 val Fixed {functions = fns, ...} = fix |
|
155 in |
|
156 NameArityMap.peek fns name_arity |
|
157 end; |
|
158 |
|
159 fun peekRelationFixed fix name_arity = |
|
160 let |
|
161 val Fixed {relations = rels, ...} = fix |
|
162 in |
|
163 NameArityMap.peek rels name_arity |
|
164 end; |
|
165 |
|
166 fun getFunctionFixed fix name_arity = |
|
167 case peekFunctionFixed fix name_arity of |
|
168 SOME f => f |
|
169 | NONE => uselessFixedFunction; |
|
170 |
|
171 fun getRelationFixed fix name_arity = |
|
172 case peekRelationFixed fix name_arity of |
|
173 SOME rel => rel |
|
174 | NONE => uselessFixedRelation; |
|
175 |
|
176 fun insertFunctionFixed fix name_arity_fn = |
|
177 let |
|
178 val Fixed {functions = fns, relations = rels} = fix |
|
179 |
|
180 val fns = NameArityMap.insert fns name_arity_fn |
|
181 in |
|
182 Fixed |
|
183 {functions = fns, |
|
184 relations = rels} |
|
185 end; |
|
186 |
|
187 fun insertRelationFixed fix name_arity_rel = |
|
188 let |
|
189 val Fixed {functions = fns, relations = rels} = fix |
|
190 |
|
191 val rels = NameArityMap.insert rels name_arity_rel |
|
192 in |
|
193 Fixed |
|
194 {functions = fns, |
|
195 relations = rels} |
|
196 end; |
|
197 |
|
198 local |
|
199 fun union _ = raise Bug "Model.unionFixed: nameArity clash"; |
|
200 in |
|
201 fun unionFixed fix1 fix2 = |
|
202 let |
|
203 val Fixed {functions = fns1, relations = rels1} = fix1 |
|
204 and Fixed {functions = fns2, relations = rels2} = fix2 |
|
205 |
|
206 val fns = NameArityMap.union union fns1 fns2 |
|
207 |
|
208 val rels = NameArityMap.union union rels1 rels2 |
|
209 in |
|
210 Fixed |
|
211 {functions = fns, |
|
212 relations = rels} |
|
213 end; |
|
214 end; |
|
215 |
|
216 val unionListFixed = |
|
217 let |
|
218 fun union (fix,acc) = unionFixed acc fix |
|
219 in |
|
220 List.foldl union emptyFixed |
|
221 end; |
|
222 |
|
223 local |
|
224 fun hasTypeFn _ elts = |
|
225 case elts of |
|
226 [x,_] => SOME x |
|
227 | _ => raise Bug "Model.hasTypeFn: wrong arity"; |
|
228 |
|
229 fun eqRel _ elts = |
|
230 case elts of |
|
231 [x,y] => SOME (x = y) |
|
232 | _ => raise Bug "Model.eqRel: wrong arity"; |
|
233 in |
|
234 val basicFixed = |
|
235 let |
|
236 val fns = NameArityMap.singleton (Term.hasTypeFunction,hasTypeFn) |
|
237 |
|
238 val rels = NameArityMap.singleton (Atom.eqRelation,eqRel) |
|
239 in |
|
240 Fixed |
|
241 {functions = fns, |
|
242 relations = rels} |
|
243 end; |
|
244 end; |
|
245 |
|
246 (* ------------------------------------------------------------------------- *) |
|
247 (* Renaming fixed model parts. *) |
|
248 (* ------------------------------------------------------------------------- *) |
|
249 |
|
250 type fixedMap = |
|
251 {functionMap : Name.name NameArityMap.map, |
|
252 relationMap : Name.name NameArityMap.map}; |
|
253 |
|
254 fun mapFixed fixMap fix = |
|
255 let |
|
256 val {functionMap = fnMap, relationMap = relMap} = fixMap |
|
257 and Fixed {functions = fns, relations = rels} = fix |
|
258 |
|
259 val fns = NameArityMap.compose fnMap fns |
|
260 |
|
261 val rels = NameArityMap.compose relMap rels |
|
262 in |
|
263 Fixed |
|
264 {functions = fns, |
|
265 relations = rels} |
|
266 end; |
|
267 |
|
268 local |
|
269 fun mkEntry tag (na,n) = (tag,na,n); |
|
270 |
|
271 fun mkList tag m = map (mkEntry tag) (NameArityMap.toList m); |
|
272 |
|
273 fun ppEntry (tag,source_arity,target) = |
|
274 Print.blockProgram Print.Inconsistent 2 |
|
275 [Print.addString tag, |
|
276 Print.addBreak 1, |
|
277 NameArity.pp source_arity, |
|
278 Print.addString " ->", |
|
279 Print.addBreak 1, |
|
280 Name.pp target]; |
|
281 in |
|
282 fun ppFixedMap fixMap = |
|
283 let |
|
284 val {functionMap = fnMap, relationMap = relMap} = fixMap |
|
285 in |
|
286 case mkList "function" fnMap @ mkList "relation" relMap of |
|
287 [] => Print.skip |
|
288 | entry :: entries => |
|
289 Print.blockProgram Print.Consistent 0 |
|
290 (ppEntry entry :: |
|
291 map (Print.sequence Print.addNewline o ppEntry) entries) |
|
292 end; |
|
293 end; |
|
294 |
|
295 (* ------------------------------------------------------------------------- *) |
|
296 (* Standard fixed model parts. *) |
|
297 (* ------------------------------------------------------------------------- *) |
|
298 |
|
299 (* Projections *) |
|
300 |
|
301 val projectionMin = 1 |
|
302 and projectionMax = 9; |
|
303 |
|
304 val projectionList = minMaxInterval projectionMin projectionMax; |
|
305 |
|
306 fun projectionName i = |
|
307 let |
|
308 val _ = projectionMin <= i orelse |
|
309 raise Bug "Model.projectionName: less than projectionMin" |
|
310 |
|
311 val _ = i <= projectionMax orelse |
|
312 raise Bug "Model.projectionName: greater than projectionMax" |
|
313 in |
|
314 Name.fromString ("project" ^ Int.toString i) |
|
315 end; |
|
316 |
|
317 fun projectionFn i _ elts = SOME (List.nth (elts, i - 1)); |
|
318 |
|
319 fun arityProjectionFixed arity = |
|
320 let |
|
321 fun mkProj i = ((projectionName i, arity), projectionFn i) |
|
322 |
|
323 fun addProj i acc = |
|
324 if i > arity then acc |
|
325 else addProj (i + 1) (NameArityMap.insert acc (mkProj i)) |
|
326 |
|
327 val fns = addProj projectionMin emptyFunctions |
|
328 |
|
329 val rels = emptyRelations |
|
330 in |
|
331 Fixed |
|
332 {functions = fns, |
|
333 relations = rels} |
|
334 end; |
|
335 |
|
336 val projectionFixed = |
|
337 unionListFixed (map arityProjectionFixed projectionList); |
|
338 |
|
339 (* Arithmetic *) |
|
340 |
|
341 val numeralMin = ~100 |
|
342 and numeralMax = 100; |
|
343 |
|
344 val numeralList = minMaxInterval numeralMin numeralMax; |
|
345 |
|
346 fun numeralName i = |
|
347 let |
|
348 val _ = numeralMin <= i orelse |
|
349 raise Bug "Model.numeralName: less than numeralMin" |
|
350 |
|
351 val _ = i <= numeralMax orelse |
|
352 raise Bug "Model.numeralName: greater than numeralMax" |
|
353 |
|
354 val s = if i < 0 then "negative" ^ Int.toString (~i) else Int.toString i |
|
355 in |
|
356 Name.fromString s |
|
357 end; |
|
358 |
|
359 val addName = Name.fromString "+" |
|
360 and divName = Name.fromString "div" |
|
361 and dividesName = Name.fromString "divides" |
|
362 and evenName = Name.fromString "even" |
|
363 and expName = Name.fromString "exp" |
|
364 and geName = Name.fromString ">=" |
|
365 and gtName = Name.fromString ">" |
|
366 and isZeroName = Name.fromString "isZero" |
|
367 and leName = Name.fromString "<=" |
|
368 and ltName = Name.fromString "<" |
|
369 and modName = Name.fromString "mod" |
|
370 and multName = Name.fromString "*" |
|
371 and negName = Name.fromString "~" |
|
372 and oddName = Name.fromString "odd" |
|
373 and preName = Name.fromString "pre" |
|
374 and subName = Name.fromString "-" |
|
375 and sucName = Name.fromString "suc"; |
|
376 |
|
377 local |
|
378 (* Support *) |
|
379 |
|
380 fun modN {size = N} x = x mod N; |
|
381 |
|
382 fun oneN sz = modN sz 1; |
|
383 |
|
384 fun multN sz (x,y) = modN sz (x * y); |
|
385 |
|
386 (* Functions *) |
|
387 |
|
388 fun numeralFn i sz = SOME (modN sz i); |
|
389 |
|
390 fun addFn sz x y = SOME (modN sz (x + y)); |
|
391 |
|
392 fun divFn {size = N} x y = |
|
393 let |
|
394 val y = if y = 0 then N else y |
|
395 in |
|
396 SOME (x div y) |
|
397 end; |
|
398 |
|
399 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz)); |
|
400 |
|
401 fun modFn {size = N} x y = |
|
402 let |
|
403 val y = if y = 0 then N else y |
|
404 in |
|
405 SOME (x mod y) |
|
406 end; |
|
407 |
|
408 fun multFn sz x y = SOME (multN sz (x,y)); |
|
409 |
|
410 fun negFn {size = N} x = SOME (if x = 0 then 0 else N - x); |
|
411 |
|
412 fun preFn {size = N} x = SOME (if x = 0 then N - 1 else x - 1); |
|
413 |
|
414 fun subFn {size = N} x y = SOME (if x < y then N + x - y else x - y); |
|
415 |
|
416 fun sucFn {size = N} x = SOME (if x = N - 1 then 0 else x + 1); |
|
417 |
|
418 (* Relations *) |
|
419 |
|
420 fun dividesRel _ x y = SOME (divides x y); |
|
421 |
|
422 fun evenRel _ x = SOME (x mod 2 = 0); |
|
423 |
|
424 fun geRel _ x y = SOME (x >= y); |
|
425 |
|
426 fun gtRel _ x y = SOME (x > y); |
|
427 |
|
428 fun isZeroRel _ x = SOME (x = 0); |
|
429 |
|
430 fun leRel _ x y = SOME (x <= y); |
|
431 |
|
432 fun ltRel _ x y = SOME (x < y); |
|
433 |
|
434 fun oddRel _ x = SOME (x mod 2 = 1); |
|
435 in |
|
436 val modularFixed = |
|
437 let |
|
438 val fns = |
|
439 NameArityMap.fromList |
|
440 (map (fn i => ((numeralName i,0), fixed0 (numeralFn i))) |
|
441 numeralList @ |
|
442 [((addName,2), fixed2 addFn), |
|
443 ((divName,2), fixed2 divFn), |
|
444 ((expName,2), fixed2 expFn), |
|
445 ((modName,2), fixed2 modFn), |
|
446 ((multName,2), fixed2 multFn), |
|
447 ((negName,1), fixed1 negFn), |
|
448 ((preName,1), fixed1 preFn), |
|
449 ((subName,2), fixed2 subFn), |
|
450 ((sucName,1), fixed1 sucFn)]) |
|
451 |
|
452 val rels = |
|
453 NameArityMap.fromList |
|
454 [((dividesName,2), fixed2 dividesRel), |
|
455 ((evenName,1), fixed1 evenRel), |
|
456 ((geName,2), fixed2 geRel), |
|
457 ((gtName,2), fixed2 gtRel), |
|
458 ((isZeroName,1), fixed1 isZeroRel), |
|
459 ((leName,2), fixed2 leRel), |
|
460 ((ltName,2), fixed2 ltRel), |
|
461 ((oddName,1), fixed1 oddRel)] |
|
462 in |
|
463 Fixed |
|
464 {functions = fns, |
|
465 relations = rels} |
|
466 end; |
|
467 end; |
|
468 |
|
469 local |
|
470 (* Support *) |
|
471 |
|
472 fun cutN {size = N} x = if x >= N then N - 1 else x; |
|
473 |
|
474 fun oneN sz = cutN sz 1; |
|
475 |
|
476 fun multN sz (x,y) = cutN sz (x * y); |
|
477 |
|
478 (* Functions *) |
|
479 |
|
480 fun numeralFn i sz = if i < 0 then NONE else SOME (cutN sz i); |
|
481 |
|
482 fun addFn sz x y = SOME (cutN sz (x + y)); |
|
483 |
|
484 fun divFn _ x y = if y = 0 then NONE else SOME (x div y); |
|
485 |
|
486 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz)); |
|
487 |
|
488 fun modFn {size = N} x y = |
|
489 if y = 0 orelse x = N - 1 then NONE else SOME (x mod y); |
|
490 |
|
491 fun multFn sz x y = SOME (multN sz (x,y)); |
|
492 |
|
493 fun negFn _ x = if x = 0 then SOME 0 else NONE; |
|
494 |
|
495 fun preFn _ x = if x = 0 then NONE else SOME (x - 1); |
|
496 |
|
497 fun subFn {size = N} x y = |
|
498 if y = 0 then SOME x |
|
499 else if x = N - 1 orelse x < y then NONE |
|
500 else SOME (x - y); |
|
501 |
|
502 fun sucFn sz x = SOME (cutN sz (x + 1)); |
|
503 |
|
504 (* Relations *) |
|
505 |
|
506 fun dividesRel {size = N} x y = |
|
507 if x = 1 orelse y = 0 then SOME true |
|
508 else if x = 0 then SOME false |
|
509 else if y = N - 1 then NONE |
|
510 else SOME (divides x y); |
|
511 |
|
512 fun evenRel {size = N} x = |
|
513 if x = N - 1 then NONE else SOME (x mod 2 = 0); |
|
514 |
|
515 fun geRel {size = N} y x = |
|
516 if x = N - 1 then if y = N - 1 then NONE else SOME false |
|
517 else if y = N - 1 then SOME true else SOME (x <= y); |
|
518 |
|
519 fun gtRel {size = N} y x = |
|
520 if x = N - 1 then if y = N - 1 then NONE else SOME false |
|
521 else if y = N - 1 then SOME true else SOME (x < y); |
|
522 |
|
523 fun isZeroRel _ x = SOME (x = 0); |
|
524 |
|
525 fun leRel {size = N} x y = |
|
526 if x = N - 1 then if y = N - 1 then NONE else SOME false |
|
527 else if y = N - 1 then SOME true else SOME (x <= y); |
|
528 |
|
529 fun ltRel {size = N} x y = |
|
530 if x = N - 1 then if y = N - 1 then NONE else SOME false |
|
531 else if y = N - 1 then SOME true else SOME (x < y); |
|
532 |
|
533 fun oddRel {size = N} x = |
|
534 if x = N - 1 then NONE else SOME (x mod 2 = 1); |
|
535 in |
|
536 val overflowFixed = |
|
537 let |
|
538 val fns = |
|
539 NameArityMap.fromList |
|
540 (map (fn i => ((numeralName i,0), fixed0 (numeralFn i))) |
|
541 numeralList @ |
|
542 [((addName,2), fixed2 addFn), |
|
543 ((divName,2), fixed2 divFn), |
|
544 ((expName,2), fixed2 expFn), |
|
545 ((modName,2), fixed2 modFn), |
|
546 ((multName,2), fixed2 multFn), |
|
547 ((negName,1), fixed1 negFn), |
|
548 ((preName,1), fixed1 preFn), |
|
549 ((subName,2), fixed2 subFn), |
|
550 ((sucName,1), fixed1 sucFn)]) |
|
551 |
|
552 val rels = |
|
553 NameArityMap.fromList |
|
554 [((dividesName,2), fixed2 dividesRel), |
|
555 ((evenName,1), fixed1 evenRel), |
|
556 ((geName,2), fixed2 geRel), |
|
557 ((gtName,2), fixed2 gtRel), |
|
558 ((isZeroName,1), fixed1 isZeroRel), |
|
559 ((leName,2), fixed2 leRel), |
|
560 ((ltName,2), fixed2 ltRel), |
|
561 ((oddName,1), fixed1 oddRel)] |
|
562 in |
|
563 Fixed |
|
564 {functions = fns, |
|
565 relations = rels} |
|
566 end; |
|
567 end; |
|
568 |
|
569 (* Sets *) |
|
570 |
|
571 val cardName = Name.fromString "card" |
|
572 and complementName = Name.fromString "complement" |
|
573 and differenceName = Name.fromString "difference" |
|
574 and emptyName = Name.fromString "empty" |
|
575 and memberName = Name.fromString "member" |
|
576 and insertName = Name.fromString "insert" |
|
577 and intersectName = Name.fromString "intersect" |
|
578 and singletonName = Name.fromString "singleton" |
|
579 and subsetName = Name.fromString "subset" |
|
580 and symmetricDifferenceName = Name.fromString "symmetricDifference" |
|
581 and unionName = Name.fromString "union" |
|
582 and universeName = Name.fromString "universe"; |
|
583 |
|
584 local |
|
585 (* Support *) |
|
586 |
|
587 fun eltN {size = N} = |
|
588 let |
|
589 fun f 0 acc = acc |
|
590 | f x acc = f (x div 2) (acc + 1) |
|
591 in |
|
592 f N ~1 |
|
593 end; |
|
594 |
|
595 fun posN i = Word.<< (0w1, Word.fromInt i); |
|
596 |
|
597 fun univN sz = Word.- (posN (eltN sz), 0w1); |
|
598 |
|
599 fun setN sz x = Word.andb (Word.fromInt x, univN sz); |
|
600 |
|
601 (* Functions *) |
|
602 |
|
603 fun cardFn sz x = |
|
604 let |
|
605 fun f 0w0 acc = acc |
|
606 | f s acc = |
|
607 let |
|
608 val acc = if Word.andb (s,0w1) = 0w0 then acc else acc + 1 |
|
609 in |
|
610 f (Word.>> (s,0w1)) acc |
|
611 end |
|
612 in |
|
613 SOME (f (setN sz x) 0) |
|
614 end; |
|
615 |
|
616 fun complementFn sz x = SOME (Word.toInt (Word.xorb (univN sz, setN sz x))); |
|
617 |
|
618 fun differenceFn sz x y = |
|
619 let |
|
620 val x = setN sz x |
|
621 and y = setN sz y |
|
622 in |
|
623 SOME (Word.toInt (Word.andb (x, Word.notb y))) |
|
624 end; |
|
625 |
|
626 fun emptyFn _ = SOME 0; |
|
627 |
|
628 fun insertFn sz x y = |
|
629 let |
|
630 val x = x mod eltN sz |
|
631 and y = setN sz y |
|
632 in |
|
633 SOME (Word.toInt (Word.orb (posN x, y))) |
|
634 end; |
|
635 |
|
636 fun intersectFn sz x y = |
|
637 SOME (Word.toInt (Word.andb (setN sz x, setN sz y))); |
|
638 |
|
639 fun singletonFn sz x = |
|
640 let |
|
641 val x = x mod eltN sz |
|
642 in |
|
643 SOME (Word.toInt (posN x)) |
|
644 end; |
|
645 |
|
646 fun symmetricDifferenceFn sz x y = |
|
647 let |
|
648 val x = setN sz x |
|
649 and y = setN sz y |
|
650 in |
|
651 SOME (Word.toInt (Word.xorb (x,y))) |
|
652 end; |
|
653 |
|
654 fun unionFn sz x y = |
|
655 SOME (Word.toInt (Word.orb (setN sz x, setN sz y))); |
|
656 |
|
657 fun universeFn sz = SOME (Word.toInt (univN sz)); |
|
658 |
|
659 (* Relations *) |
|
660 |
|
661 fun memberRel sz x y = |
|
662 let |
|
663 val x = x mod eltN sz |
|
664 and y = setN sz y |
|
665 in |
|
666 SOME (Word.andb (posN x, y) <> 0w0) |
|
667 end; |
|
668 |
|
669 fun subsetRel sz x y = |
|
670 let |
|
671 val x = setN sz x |
|
672 and y = setN sz y |
|
673 in |
|
674 SOME (Word.andb (x, Word.notb y) = 0w0) |
|
675 end; |
|
676 in |
|
677 val setFixed = |
|
678 let |
|
679 val fns = |
|
680 NameArityMap.fromList |
|
681 [((cardName,1), fixed1 cardFn), |
|
682 ((complementName,1), fixed1 complementFn), |
|
683 ((differenceName,2), fixed2 differenceFn), |
|
684 ((emptyName,0), fixed0 emptyFn), |
|
685 ((insertName,2), fixed2 insertFn), |
|
686 ((intersectName,2), fixed2 intersectFn), |
|
687 ((singletonName,1), fixed1 singletonFn), |
|
688 ((symmetricDifferenceName,2), fixed2 symmetricDifferenceFn), |
|
689 ((unionName,2), fixed2 unionFn), |
|
690 ((universeName,0), fixed0 universeFn)] |
|
691 |
|
692 val rels = |
|
693 NameArityMap.fromList |
|
694 [((memberName,2), fixed2 memberRel), |
|
695 ((subsetName,2), fixed2 subsetRel)] |
|
696 in |
|
697 Fixed |
|
698 {functions = fns, |
|
699 relations = rels} |
|
700 end; |
|
701 end; |
|
702 |
|
703 (* Lists *) |
|
704 |
|
705 val appendName = Name.fromString "@" |
|
706 and consName = Name.fromString "::" |
|
707 and lengthName = Name.fromString "length" |
|
708 and nilName = Name.fromString "nil" |
|
709 and nullName = Name.fromString "null" |
|
710 and tailName = Name.fromString "tail"; |
|
711 |
|
712 local |
|
713 val baseFix = |
|
714 let |
|
715 val fix = unionFixed projectionFixed overflowFixed |
|
716 |
|
717 val sucFn = getFunctionFixed fix (sucName,1) |
|
718 |
|
719 fun suc2Fn sz _ x = sucFn sz [x] |
|
720 in |
|
721 insertFunctionFixed fix ((sucName,2), fixed2 suc2Fn) |
|
722 end; |
|
723 |
|
724 val fixMap = |
|
725 {functionMap = NameArityMap.fromList |
|
726 [((appendName,2),addName), |
|
727 ((consName,2),sucName), |
|
728 ((lengthName,1), projectionName 1), |
|
729 ((nilName,0), numeralName 0), |
|
730 ((tailName,1),preName)], |
|
731 relationMap = NameArityMap.fromList |
|
732 [((nullName,1),isZeroName)]}; |
|
733 |
|
734 in |
|
735 val listFixed = mapFixed fixMap baseFix; |
|
736 end; |
|
737 |
|
738 (* ------------------------------------------------------------------------- *) |
|
739 (* Valuations. *) |
|
740 (* ------------------------------------------------------------------------- *) |
|
741 |
|
742 datatype valuation = Valuation of element NameMap.map; |
|
743 |
|
744 val emptyValuation = Valuation (NameMap.new ()); |
|
745 |
|
746 fun insertValuation (Valuation m) v_i = Valuation (NameMap.insert m v_i); |
|
747 |
|
748 fun peekValuation (Valuation m) v = NameMap.peek m v; |
|
749 |
|
750 fun constantValuation i = |
|
751 let |
|
752 fun add (v,V) = insertValuation V (v,i) |
|
753 in |
|
754 NameSet.foldl add emptyValuation |
|
755 end; |
|
756 |
|
757 val zeroValuation = constantValuation zeroElement; |
|
758 |
|
759 fun getValuation V v = |
|
760 case peekValuation V v of |
|
761 SOME i => i |
|
762 | NONE => raise Error "Model.getValuation: incomplete valuation"; |
|
763 |
|
764 fun randomValuation {size = N} vs = |
|
765 let |
|
766 fun f (v,V) = insertValuation V (v, Portable.randomInt N) |
|
767 in |
|
768 NameSet.foldl f emptyValuation vs |
|
769 end; |
|
770 |
|
771 fun incrementValuation N vars = |
|
772 let |
|
773 fun inc vs V = |
|
774 case vs of |
|
775 [] => NONE |
|
776 | v :: vs => |
|
777 let |
|
778 val (carry,i) = |
|
779 case incrementElement N (getValuation V v) of |
|
780 SOME i => (false,i) |
|
781 | NONE => (true,zeroElement) |
|
782 |
|
783 val V = insertValuation V (v,i) |
|
784 in |
|
785 if carry then inc vs V else SOME V |
|
786 end |
|
787 in |
|
788 inc (NameSet.toList vars) |
|
789 end; |
|
790 |
|
791 fun foldValuation N vars f = |
|
792 let |
|
793 val inc = incrementValuation N vars |
|
794 |
|
795 fun fold V acc = |
|
796 let |
|
797 val acc = f (V,acc) |
|
798 in |
|
799 case inc V of |
|
800 NONE => acc |
|
801 | SOME V => fold V acc |
|
802 end |
|
803 |
|
804 val zero = zeroValuation vars |
|
805 in |
|
806 fold zero |
|
807 end; |
|
808 |
|
809 (* ------------------------------------------------------------------------- *) |
|
810 (* A type of random finite mapping Z^n -> Z. *) |
|
811 (* ------------------------------------------------------------------------- *) |
|
812 |
|
813 val UNKNOWN = ~1; |
|
814 |
|
815 datatype table = |
|
816 ForgetfulTable |
|
817 | ArrayTable of int Array.array; |
|
818 |
|
819 fun newTable N arity = |
|
820 case elementListSpace {size = N} arity of |
|
821 NONE => ForgetfulTable |
|
822 | SOME space => ArrayTable (Array.array (space,UNKNOWN)); |
|
823 |
|
824 local |
|
825 fun randomResult R = Portable.randomInt R; |
|
826 in |
|
827 fun lookupTable N R table elts = |
|
828 case table of |
|
829 ForgetfulTable => randomResult R |
|
830 | ArrayTable a => |
|
831 let |
|
832 val i = elementListIndex {size = N} elts |
|
833 |
|
834 val r = Array.sub (a,i) |
|
835 in |
|
836 if r <> UNKNOWN then r |
|
837 else |
|
838 let |
|
839 val r = randomResult R |
|
840 |
|
841 val () = Array.update (a,i,r) |
|
842 in |
|
843 r |
|
844 end |
|
845 end; |
|
846 end; |
|
847 |
|
848 fun updateTable N table (elts,r) = |
|
849 case table of |
|
850 ForgetfulTable => () |
|
851 | ArrayTable a => |
|
852 let |
|
853 val i = elementListIndex {size = N} elts |
|
854 |
|
855 val () = Array.update (a,i,r) |
|
856 in |
|
857 () |
|
858 end; |
|
859 |
|
860 (* ------------------------------------------------------------------------- *) |
|
861 (* A type of random finite mappings name * arity -> Z^arity -> Z. *) |
|
862 (* ------------------------------------------------------------------------- *) |
|
863 |
|
864 datatype tables = |
|
865 Tables of |
|
866 {domainSize : int, |
|
867 rangeSize : int, |
|
868 tableMap : table NameArityMap.map ref}; |
|
869 |
|
870 fun newTables N R = |
|
871 Tables |
|
872 {domainSize = N, |
|
873 rangeSize = R, |
|
874 tableMap = ref (NameArityMap.new ())}; |
|
875 |
|
876 fun getTables tables n_a = |
|
877 let |
|
878 val Tables {domainSize = N, rangeSize = _, tableMap = tm} = tables |
|
879 |
|
880 val ref m = tm |
|
881 in |
|
882 case NameArityMap.peek m n_a of |
|
883 SOME t => t |
|
884 | NONE => |
|
885 let |
|
886 val (_,a) = n_a |
|
887 |
|
888 val t = newTable N a |
|
889 |
|
890 val m = NameArityMap.insert m (n_a,t) |
|
891 |
|
892 val () = tm := m |
|
893 in |
|
894 t |
|
895 end |
|
896 end; |
|
897 |
|
898 fun lookupTables tables (n,elts) = |
|
899 let |
|
900 val Tables {domainSize = N, rangeSize = R, ...} = tables |
|
901 |
|
902 val a = length elts |
|
903 |
|
904 val table = getTables tables (n,a) |
|
905 in |
|
906 lookupTable N R table elts |
|
907 end; |
|
908 |
|
909 fun updateTables tables ((n,elts),r) = |
|
910 let |
|
911 val Tables {domainSize = N, ...} = tables |
|
912 |
|
913 val a = length elts |
|
914 |
|
915 val table = getTables tables (n,a) |
|
916 in |
|
917 updateTable N table (elts,r) |
|
918 end; |
|
919 |
|
920 (* ------------------------------------------------------------------------- *) |
|
921 (* A type of random finite models. *) |
|
922 (* ------------------------------------------------------------------------- *) |
|
923 |
|
924 type parameters = {size : int, fixed : fixed}; |
|
925 |
|
926 datatype model = |
|
927 Model of |
|
928 {size : int, |
|
929 fixedFunctions : (element list -> element option) NameArityMap.map, |
|
930 fixedRelations : (element list -> bool option) NameArityMap.map, |
|
931 randomFunctions : tables, |
|
932 randomRelations : tables}; |
|
933 |
|
934 fun new {size = N, fixed} = |
|
935 let |
|
936 val Fixed {functions = fns, relations = rels} = fixed |
|
937 |
|
938 val fixFns = NameArityMap.transform (fn f => f {size = N}) fns |
|
939 and fixRels = NameArityMap.transform (fn r => r {size = N}) rels |
|
940 |
|
941 val rndFns = newTables N N |
|
942 and rndRels = newTables N 2 |
|
943 in |
|
944 Model |
|
945 {size = N, |
|
946 fixedFunctions = fixFns, |
|
947 fixedRelations = fixRels, |
|
948 randomFunctions = rndFns, |
|
949 randomRelations = rndRels} |
|
950 end; |
|
951 |
|
952 fun size (Model {size = N, ...}) = N; |
|
953 |
|
954 fun peekFixedFunction M (n,elts) = |
|
955 let |
|
956 val Model {fixedFunctions = fixFns, ...} = M |
|
957 in |
|
958 case NameArityMap.peek fixFns (n, length elts) of |
|
959 NONE => NONE |
|
960 | SOME fixFn => fixFn elts |
|
961 end; |
|
962 |
|
963 fun isFixedFunction M n_elts = Option.isSome (peekFixedFunction M n_elts); |
|
964 |
|
965 fun peekFixedRelation M (n,elts) = |
|
966 let |
|
967 val Model {fixedRelations = fixRels, ...} = M |
|
968 in |
|
969 case NameArityMap.peek fixRels (n, length elts) of |
|
970 NONE => NONE |
|
971 | SOME fixRel => fixRel elts |
|
972 end; |
|
973 |
|
974 fun isFixedRelation M n_elts = Option.isSome (peekFixedRelation M n_elts); |
|
975 |
|
976 (* A default model *) |
|
977 |
|
978 val defaultSize = 8; |
|
979 |
|
980 val defaultFixed = |
|
981 unionListFixed |
|
982 [basicFixed, |
|
983 projectionFixed, |
|
984 modularFixed, |
|
985 setFixed, |
|
986 listFixed]; |
|
987 |
|
988 val default = {size = defaultSize, fixed = defaultFixed}; |
|
989 |
|
990 (* ------------------------------------------------------------------------- *) |
|
991 (* Taking apart terms to interpret them. *) |
|
992 (* ------------------------------------------------------------------------- *) |
|
993 |
|
994 fun destTerm tm = |
|
995 case tm of |
|
996 Term.Var _ => tm |
|
997 | Term.Fn f_tms => |
|
998 case Term.stripApp tm of |
|
999 (_,[]) => tm |
|
1000 | (v as Term.Var _, tms) => Term.Fn (Term.appName, v :: tms) |
|
1001 | (Term.Fn (f,tms), tms') => Term.Fn (f, tms @ tms'); |
|
1002 |
|
1003 (* ------------------------------------------------------------------------- *) |
|
1004 (* Interpreting terms and formulas in the model. *) |
|
1005 (* ------------------------------------------------------------------------- *) |
|
1006 |
|
1007 fun interpretFunction M n_elts = |
|
1008 case peekFixedFunction M n_elts of |
|
1009 SOME r => r |
|
1010 | NONE => |
|
1011 let |
|
1012 val Model {randomFunctions = rndFns, ...} = M |
|
1013 in |
|
1014 lookupTables rndFns n_elts |
|
1015 end; |
|
1016 |
|
1017 fun interpretRelation M n_elts = |
|
1018 case peekFixedRelation M n_elts of |
|
1019 SOME r => r |
|
1020 | NONE => |
|
1021 let |
|
1022 val Model {randomRelations = rndRels, ...} = M |
|
1023 in |
|
1024 intToBool (lookupTables rndRels n_elts) |
|
1025 end; |
|
1026 |
|
1027 fun interpretTerm M V = |
|
1028 let |
|
1029 fun interpret tm = |
|
1030 case destTerm tm of |
|
1031 Term.Var v => getValuation V v |
|
1032 | Term.Fn (f,tms) => interpretFunction M (f, map interpret tms) |
|
1033 in |
|
1034 interpret |
|
1035 end; |
|
1036 |
|
1037 fun interpretAtom M V (r,tms) = |
|
1038 interpretRelation M (r, map (interpretTerm M V) tms); |
|
1039 |
|
1040 fun interpretFormula M = |
|
1041 let |
|
1042 val N = size M |
|
1043 |
|
1044 fun interpret V fm = |
|
1045 case fm of |
|
1046 Formula.True => true |
|
1047 | Formula.False => false |
|
1048 | Formula.Atom atm => interpretAtom M V atm |
|
1049 | Formula.Not p => not (interpret V p) |
|
1050 | Formula.Or (p,q) => interpret V p orelse interpret V q |
|
1051 | Formula.And (p,q) => interpret V p andalso interpret V q |
|
1052 | Formula.Imp (p,q) => interpret V (Formula.Or (Formula.Not p, q)) |
|
1053 | Formula.Iff (p,q) => interpret V p = interpret V q |
|
1054 | Formula.Forall (v,p) => interpret' V p v N |
|
1055 | Formula.Exists (v,p) => |
|
1056 interpret V (Formula.Not (Formula.Forall (v, Formula.Not p))) |
|
1057 |
|
1058 and interpret' V fm v i = |
|
1059 i = 0 orelse |
|
1060 let |
|
1061 val i = i - 1 |
|
1062 val V' = insertValuation V (v,i) |
|
1063 in |
|
1064 interpret V' fm andalso interpret' V fm v i |
|
1065 end |
|
1066 in |
|
1067 interpret |
|
1068 end; |
|
1069 |
|
1070 fun interpretLiteral M V (pol,atm) = |
|
1071 let |
|
1072 val b = interpretAtom M V atm |
|
1073 in |
|
1074 if pol then b else not b |
|
1075 end; |
|
1076 |
|
1077 fun interpretClause M V cl = LiteralSet.exists (interpretLiteral M V) cl; |
|
1078 |
|
1079 (* ------------------------------------------------------------------------- *) |
|
1080 (* Check whether random groundings of a formula are true in the model. *) |
|
1081 (* Note: if it's cheaper, a systematic check will be performed instead. *) |
|
1082 (* ------------------------------------------------------------------------- *) |
|
1083 |
|
1084 fun check interpret {maxChecks} M fv x = |
|
1085 let |
|
1086 val N = size M |
|
1087 |
|
1088 fun score (V,{T,F}) = |
|
1089 if interpret M V x then {T = T + 1, F = F} else {T = T, F = F + 1} |
|
1090 |
|
1091 fun randomCheck acc = score (randomValuation {size = N} fv, acc) |
|
1092 |
|
1093 val maxChecks = |
|
1094 case maxChecks of |
|
1095 NONE => maxChecks |
|
1096 | SOME m => |
|
1097 case expInt N (NameSet.size fv) of |
|
1098 SOME n => if n <= m then NONE else maxChecks |
|
1099 | NONE => maxChecks |
|
1100 in |
|
1101 case maxChecks of |
|
1102 SOME m => funpow m randomCheck {T = 0, F = 0} |
|
1103 | NONE => foldValuation {size = N} fv score {T = 0, F = 0} |
|
1104 end; |
|
1105 |
|
1106 fun checkAtom maxChecks M atm = |
|
1107 check interpretAtom maxChecks M (Atom.freeVars atm) atm; |
|
1108 |
|
1109 fun checkFormula maxChecks M fm = |
|
1110 check interpretFormula maxChecks M (Formula.freeVars fm) fm; |
|
1111 |
|
1112 fun checkLiteral maxChecks M lit = |
|
1113 check interpretLiteral maxChecks M (Literal.freeVars lit) lit; |
|
1114 |
|
1115 fun checkClause maxChecks M cl = |
|
1116 check interpretClause maxChecks M (LiteralSet.freeVars cl) cl; |
|
1117 |
|
1118 (* ------------------------------------------------------------------------- *) |
|
1119 (* Updating the model. *) |
|
1120 (* ------------------------------------------------------------------------- *) |
|
1121 |
|
1122 fun updateFunction M func_elts_elt = |
|
1123 let |
|
1124 val Model {randomFunctions = rndFns, ...} = M |
|
1125 |
|
1126 val () = updateTables rndFns func_elts_elt |
|
1127 in |
|
1128 () |
|
1129 end; |
|
1130 |
|
1131 fun updateRelation M (rel_elts,pol) = |
|
1132 let |
|
1133 val Model {randomRelations = rndRels, ...} = M |
|
1134 |
|
1135 val () = updateTables rndRels (rel_elts, boolToInt pol) |
|
1136 in |
|
1137 () |
|
1138 end; |
|
1139 |
|
1140 (* ------------------------------------------------------------------------- *) |
|
1141 (* A type of terms with interpretations embedded in the subterms. *) |
|
1142 (* ------------------------------------------------------------------------- *) |
|
1143 |
|
1144 datatype modelTerm = |
|
1145 ModelVar |
|
1146 | ModelFn of Term.functionName * modelTerm list * int list; |
|
1147 |
|
1148 fun modelTerm M V = |
|
1149 let |
|
1150 fun modelTm tm = |
|
1151 case destTerm tm of |
|
1152 Term.Var v => (ModelVar, getValuation V v) |
|
1153 | Term.Fn (f,tms) => |
|
1154 let |
|
1155 val (tms,xs) = unzip (map modelTm tms) |
|
1156 in |
|
1157 (ModelFn (f,tms,xs), interpretFunction M (f,xs)) |
|
1158 end |
|
1159 in |
|
1160 modelTm |
|
1161 end; |
|
1162 |
|
1163 (* ------------------------------------------------------------------------- *) |
|
1164 (* Perturbing the model. *) |
|
1165 (* ------------------------------------------------------------------------- *) |
|
1166 |
|
1167 datatype perturbation = |
|
1168 FunctionPerturbation of (Term.functionName * element list) * element |
|
1169 | RelationPerturbation of (Atom.relationName * element list) * bool; |
|
1170 |
|
1171 fun perturb M pert = |
|
1172 case pert of |
|
1173 FunctionPerturbation func_elts_elt => updateFunction M func_elts_elt |
|
1174 | RelationPerturbation rel_elts_pol => updateRelation M rel_elts_pol; |
|
1175 |
|
1176 local |
|
1177 fun pertTerm _ [] _ acc = acc |
|
1178 | pertTerm M target tm acc = |
|
1179 case tm of |
|
1180 ModelVar => acc |
|
1181 | ModelFn (func,tms,xs) => |
|
1182 let |
|
1183 fun onTarget ys = mem (interpretFunction M (func,ys)) target |
|
1184 |
|
1185 val func_xs = (func,xs) |
|
1186 |
|
1187 val acc = |
|
1188 if isFixedFunction M func_xs then acc |
|
1189 else |
|
1190 let |
|
1191 fun add (y,acc) = FunctionPerturbation (func_xs,y) :: acc |
|
1192 in |
|
1193 foldl add acc target |
|
1194 end |
|
1195 in |
|
1196 pertTerms M onTarget tms xs acc |
|
1197 end |
|
1198 |
|
1199 and pertTerms M onTarget = |
|
1200 let |
|
1201 val N = size M |
|
1202 |
|
1203 fun filterElements pred = |
|
1204 let |
|
1205 fun filt 0 acc = acc |
|
1206 | filt i acc = |
|
1207 let |
|
1208 val i = i - 1 |
|
1209 val acc = if pred i then i :: acc else acc |
|
1210 in |
|
1211 filt i acc |
|
1212 end |
|
1213 in |
|
1214 filt N [] |
|
1215 end |
|
1216 |
|
1217 fun pert _ [] [] acc = acc |
|
1218 | pert ys (tm :: tms) (x :: xs) acc = |
|
1219 let |
|
1220 fun pred y = |
|
1221 y <> x andalso onTarget (List.revAppend (ys, y :: xs)) |
|
1222 |
|
1223 val target = filterElements pred |
|
1224 |
|
1225 val acc = pertTerm M target tm acc |
|
1226 in |
|
1227 pert (x :: ys) tms xs acc |
|
1228 end |
|
1229 | pert _ _ _ _ = raise Bug "Model.pertTerms.pert" |
|
1230 in |
|
1231 pert [] |
|
1232 end; |
|
1233 |
|
1234 fun pertAtom M V target (rel,tms) acc = |
|
1235 let |
|
1236 fun onTarget ys = interpretRelation M (rel,ys) = target |
|
1237 |
|
1238 val (tms,xs) = unzip (map (modelTerm M V) tms) |
|
1239 |
|
1240 val rel_xs = (rel,xs) |
|
1241 |
|
1242 val acc = |
|
1243 if isFixedRelation M rel_xs then acc |
|
1244 else RelationPerturbation (rel_xs,target) :: acc |
|
1245 in |
|
1246 pertTerms M onTarget tms xs acc |
|
1247 end; |
|
1248 |
|
1249 fun pertLiteral M V ((pol,atm),acc) = pertAtom M V pol atm acc; |
|
1250 |
|
1251 fun pertClause M V cl acc = LiteralSet.foldl (pertLiteral M V) acc cl; |
|
1252 |
|
1253 fun pickPerturb M perts = |
|
1254 if null perts then () |
|
1255 else perturb M (List.nth (perts, Portable.randomInt (length perts))); |
|
1256 in |
|
1257 fun perturbTerm M V (tm,target) = |
|
1258 pickPerturb M (pertTerm M target (fst (modelTerm M V tm)) []); |
|
1259 |
|
1260 fun perturbAtom M V (atm,target) = |
|
1261 pickPerturb M (pertAtom M V target atm []); |
|
1262 |
|
1263 fun perturbLiteral M V lit = pickPerturb M (pertLiteral M V (lit,[])); |
|
1264 |
|
1265 fun perturbClause M V cl = pickPerturb M (pertClause M V cl []); |
|
1266 end; |
|
1267 |
|
1268 (* ------------------------------------------------------------------------- *) |
|
1269 (* Pretty printing. *) |
|
1270 (* ------------------------------------------------------------------------- *) |
|
1271 |
|
1272 fun pp M = |
|
1273 Print.program |
|
1274 [Print.addString "Model{", |
|
1275 Print.ppInt (size M), |
|
1276 Print.addString "}"]; |
|
1277 |
|
1278 end |