1(* ========================================================================= *) 2(* RANDOM FINITE MODELS *) 3(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Model :> Model = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* Constants. *) 13(* ------------------------------------------------------------------------- *) 14 15val maxSpace = 1000; 16 17(* ------------------------------------------------------------------------- *) 18(* Helper functions. *) 19(* ------------------------------------------------------------------------- *) 20 21val 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 31local 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; 49in 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; 59end; 60 61fun boolToInt true = 1 62 | boolToInt false = 0; 63 64fun intToBool 1 = true 65 | intToBool 0 = false 66 | intToBool _ = raise Bug "Model.intToBool"; 67 68fun minMaxInterval i j = interval i (1 + j - i); 69 70(* ------------------------------------------------------------------------- *) 71(* Model size. *) 72(* ------------------------------------------------------------------------- *) 73 74type size = {size : int}; 75 76(* ------------------------------------------------------------------------- *) 77(* A model of size N has integer elements 0...N-1. *) 78(* ------------------------------------------------------------------------- *) 79 80type element = int; 81 82val zeroElement = 0; 83 84fun 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 91fun 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 96fun 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 110type fixedFunction = size -> element list -> element option; 111 112type fixedRelation = size -> element list -> bool option; 113 114datatype fixed = 115 Fixed of 116 {functions : fixedFunction NameArityMap.map, 117 relations : fixedRelation NameArityMap.map}; 118 119val uselessFixedFunction : fixedFunction = K (K NONE); 120 121val uselessFixedRelation : fixedRelation = K (K NONE); 122 123val emptyFunctions : fixedFunction NameArityMap.map = NameArityMap.new (); 124 125val emptyRelations : fixedRelation NameArityMap.map = NameArityMap.new (); 126 127fun fixed0 f sz elts = 128 case elts of 129 [] => f sz 130 | _ => raise Bug "Model.fixed0: wrong arity"; 131 132fun fixed1 f sz elts = 133 case elts of 134 [x] => f sz x 135 | _ => raise Bug "Model.fixed1: wrong arity"; 136 137fun fixed2 f sz elts = 138 case elts of 139 [x,y] => f sz x y 140 | _ => raise Bug "Model.fixed2: wrong arity"; 141 142val emptyFixed = 143 let 144 val fns = emptyFunctions 145 and rels = emptyRelations 146 in 147 Fixed 148 {functions = fns, 149 relations = rels} 150 end; 151 152fun peekFunctionFixed fix name_arity = 153 let 154 val Fixed {functions = fns, ...} = fix 155 in 156 NameArityMap.peek fns name_arity 157 end; 158 159fun peekRelationFixed fix name_arity = 160 let 161 val Fixed {relations = rels, ...} = fix 162 in 163 NameArityMap.peek rels name_arity 164 end; 165 166fun getFunctionFixed fix name_arity = 167 case peekFunctionFixed fix name_arity of 168 SOME f => f 169 | NONE => uselessFixedFunction; 170 171fun getRelationFixed fix name_arity = 172 case peekRelationFixed fix name_arity of 173 SOME rel => rel 174 | NONE => uselessFixedRelation; 175 176fun 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 187fun 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 198local 199 fun union _ = raise Bug "Model.unionFixed: nameArity clash"; 200in 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; 214end; 215 216val unionListFixed = 217 let 218 fun union (fix,acc) = unionFixed acc fix 219 in 220 List.foldl union emptyFixed 221 end; 222 223local 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"; 233in 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; 244end; 245 246(* ------------------------------------------------------------------------- *) 247(* Renaming fixed model parts. *) 248(* ------------------------------------------------------------------------- *) 249 250type fixedMap = 251 {functionMap : Name.name NameArityMap.map, 252 relationMap : Name.name NameArityMap.map}; 253 254fun 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 268local 269 fun mkEntry tag (na,n) = (tag,na,n); 270 271 fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m); 272 273 fun ppEntry (tag,source_arity,target) = 274 Print.inconsistentBlock 2 275 [Print.ppString tag, 276 Print.break, 277 NameArity.pp source_arity, 278 Print.ppString " ->", 279 Print.break, 280 Name.pp target]; 281in 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.consistentBlock 0 290 (ppEntry entry :: 291 List.map (Print.sequence Print.newline o ppEntry) entries) 292 end; 293end; 294 295(* ------------------------------------------------------------------------- *) 296(* Standard fixed model parts. *) 297(* ------------------------------------------------------------------------- *) 298 299(* Projections *) 300 301val projectionMin = 1 302and projectionMax = 9; 303 304val projectionList = minMaxInterval projectionMin projectionMax; 305 306fun 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 317fun projectionFn i _ elts = SOME (List.nth (elts, i - 1)); 318 319fun 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 336val projectionFixed = 337 unionListFixed (List.map arityProjectionFixed projectionList); 338 339(* Arithmetic *) 340 341val numeralMin = ~100 342and numeralMax = 100; 343 344val numeralList = minMaxInterval numeralMin numeralMax; 345 346fun 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 359val addName = Name.fromString "+" 360and divName = Name.fromString "div" 361and dividesName = Name.fromString "divides" 362and evenName = Name.fromString "even" 363and expName = Name.fromString "exp" 364and geName = Name.fromString ">=" 365and gtName = Name.fromString ">" 366and isZeroName = Name.fromString "isZero" 367and leName = Name.fromString "<=" 368and ltName = Name.fromString "<" 369and modName = Name.fromString "mod" 370and multName = Name.fromString "*" 371and negName = Name.fromString "~" 372and oddName = Name.fromString "odd" 373and preName = Name.fromString "pre" 374and subName = Name.fromString "-" 375and sucName = Name.fromString "suc"; 376 377local 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); 435in 436 val modularFixed = 437 let 438 val fns = 439 NameArityMap.fromList 440 (List.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; 467end; 468 469local 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); 535in 536 val overflowFixed = 537 let 538 val fns = 539 NameArityMap.fromList 540 (List.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; 567end; 568 569(* Sets *) 570 571val cardName = Name.fromString "card" 572and complementName = Name.fromString "complement" 573and differenceName = Name.fromString "difference" 574and emptyName = Name.fromString "empty" 575and memberName = Name.fromString "member" 576and insertName = Name.fromString "insert" 577and intersectName = Name.fromString "intersect" 578and singletonName = Name.fromString "singleton" 579and subsetName = Name.fromString "subset" 580and symmetricDifferenceName = Name.fromString "symmetricDifference" 581and unionName = Name.fromString "union" 582and universeName = Name.fromString "universe"; 583 584local 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; 676in 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; 701end; 702 703(* Lists *) 704 705val appendName = Name.fromString "@" 706and consName = Name.fromString "::" 707and lengthName = Name.fromString "length" 708and nilName = Name.fromString "nil" 709and nullName = Name.fromString "null" 710and tailName = Name.fromString "tail"; 711 712local 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 734in 735 val listFixed = mapFixed fixMap baseFix; 736end; 737 738(* ------------------------------------------------------------------------- *) 739(* Valuations. *) 740(* ------------------------------------------------------------------------- *) 741 742datatype valuation = Valuation of element NameMap.map; 743 744val emptyValuation = Valuation (NameMap.new ()); 745 746fun insertValuation (Valuation m) v_i = Valuation (NameMap.insert m v_i); 747 748fun peekValuation (Valuation m) v = NameMap.peek m v; 749 750fun constantValuation i = 751 let 752 fun add (v,V) = insertValuation V (v,i) 753 in 754 NameSet.foldl add emptyValuation 755 end; 756 757val zeroValuation = constantValuation zeroElement; 758 759fun getValuation V v = 760 case peekValuation V v of 761 SOME i => i 762 | NONE => raise Error "Model.getValuation: incomplete valuation"; 763 764fun 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 771fun 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 791fun 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 813val UNKNOWN = ~1; 814 815datatype table = 816 ForgetfulTable 817 | ArrayTable of int Array.array; 818 819fun newTable N arity = 820 case elementListSpace {size = N} arity of 821 NONE => ForgetfulTable 822 | SOME space => ArrayTable (Array.array (space,UNKNOWN)); 823 824local 825 fun randomResult R = Portable.randomInt R; 826in 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; 846end; 847 848fun 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 864datatype tables = 865 Tables of 866 {domainSize : int, 867 rangeSize : int, 868 tableMap : table NameArityMap.map ref}; 869 870fun newTables N R = 871 Tables 872 {domainSize = N, 873 rangeSize = R, 874 tableMap = ref (NameArityMap.new ())}; 875 876fun 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 898fun 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 909fun 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 924type parameters = {size : int, fixed : fixed}; 925 926datatype 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 934fun 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 952fun size (Model {size = N, ...}) = N; 953 954fun 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 963fun isFixedFunction M n_elts = Option.isSome (peekFixedFunction M n_elts); 964 965fun 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 974fun isFixedRelation M n_elts = Option.isSome (peekFixedRelation M n_elts); 975 976(* A default model *) 977 978val defaultSize = 8; 979 980val defaultFixed = 981 unionListFixed 982 [basicFixed, 983 projectionFixed, 984 modularFixed, 985 setFixed, 986 listFixed]; 987 988val default = {size = defaultSize, fixed = defaultFixed}; 989 990(* ------------------------------------------------------------------------- *) 991(* Taking apart terms to interpret them. *) 992(* ------------------------------------------------------------------------- *) 993 994fun 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 1007fun 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 1017fun 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 1027fun 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, List.map interpret tms) 1033 in 1034 interpret 1035 end; 1036 1037fun interpretAtom M V (r,tms) = 1038 interpretRelation M (r, List.map (interpretTerm M V) tms); 1039 1040fun 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 1070fun 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 1077fun 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 1084fun 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 1106fun checkAtom maxChecks M atm = 1107 check interpretAtom maxChecks M (Atom.freeVars atm) atm; 1108 1109fun checkFormula maxChecks M fm = 1110 check interpretFormula maxChecks M (Formula.freeVars fm) fm; 1111 1112fun checkLiteral maxChecks M lit = 1113 check interpretLiteral maxChecks M (Literal.freeVars lit) lit; 1114 1115fun checkClause maxChecks M cl = 1116 check interpretClause maxChecks M (LiteralSet.freeVars cl) cl; 1117 1118(* ------------------------------------------------------------------------- *) 1119(* Updating the model. *) 1120(* ------------------------------------------------------------------------- *) 1121 1122fun 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 1131fun 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 1144datatype modelTerm = 1145 ModelVar 1146 | ModelFn of Term.functionName * modelTerm list * int list; 1147 1148fun 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 (List.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 1167datatype perturbation = 1168 FunctionPerturbation of (Term.functionName * element list) * element 1169 | RelationPerturbation of (Atom.relationName * element list) * bool; 1170 1171fun 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 1176local 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 List.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 (List.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 List.null perts then () 1255 else perturb M (List.nth (perts, Portable.randomInt (length perts))); 1256in 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 []); 1266end; 1267 1268(* ------------------------------------------------------------------------- *) 1269(* Pretty printing. *) 1270(* ------------------------------------------------------------------------- *) 1271 1272fun pp M = 1273 Print.program 1274 [Print.ppString "Model{", 1275 Print.ppInt (size M), 1276 Print.ppString "}"]; 1277 1278end 1279