| author | huffman | 
| Mon, 20 Aug 2007 17:34:04 +0200 | |
| changeset 24339 | d929e9b2e598 | 
| parent 23510 | 4521fead5609 | 
| child 25430 | 372d6749f00e | 
| permissions | -rw-r--r-- | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 1 | (* ========================================================================= *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 2 | (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *) | 
| 23510 | 3 | (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 4 | (* ========================================================================= *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 5 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 6 | structure RandomSet :> Set = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 7 | struct | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 8 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 9 | exception Bug = Useful.Bug; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 10 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 11 | exception Error = Useful.Error; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 12 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 13 | val pointerEqual = Portable.pointerEqual; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 14 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 15 | val K = Useful.K; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 16 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 17 | val snd = Useful.snd; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 18 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 19 | val randomInt = Useful.random; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 20 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 21 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 22 | (* Random search trees. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 23 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 24 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 25 | datatype 'a tree = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 26 | E | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 27 | | T of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 28 |     {size : int,
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 29 | priority : real, | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 30 | left : 'a tree, | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 31 | key : 'a, | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 32 | right : 'a tree}; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 33 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 34 | type 'a node = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 35 |      {size : int,
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 36 | priority : real, | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 37 | left : 'a tree, | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 38 | key : 'a, | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 39 | right : 'a tree}; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 40 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 41 | datatype 'a set = Set of ('a * 'a -> order) * 'a tree;
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 42 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 43 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 44 | (* Random priorities. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 45 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 46 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 47 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 48 | val randomPriority = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 49 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 50 | val gen = Random.newgenseed 2.0 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 51 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 52 | fn () => Random.random gen | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 53 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 54 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 55 | val priorityOrder = Real.compare; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 56 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 57 | fun treeSingleton key = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 58 |       T {size = 1, priority = randomPriority (),
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 59 | left = E, key = key, right = E}; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 60 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 61 | fun nodePriorityOrder cmp (x1 : 'a node, x2 : 'a node) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 62 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 63 |         val {priority = p1, key = k1, ...} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 64 |         and {priority = p2, key = k2, ...} = x2
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 65 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 66 | case priorityOrder (p1,p2) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 67 | LESS => LESS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 68 | | EQUAL => cmp (k1,k2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 69 | | GREATER => GREATER | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 70 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 71 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 72 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 73 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 74 | (* Debugging functions. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 75 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 76 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 77 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 78 | fun checkSizes E = 0 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 79 |     | checkSizes (T {size,left,right,...}) =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 80 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 81 | val l = checkSizes left | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 82 | and r = checkSizes right | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 83 | val () = if l + 1 + r = size then () else raise Error "wrong size" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 84 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 85 | size | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 86 | end | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 87 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 88 | fun checkSorted _ x E = x | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 89 |     | checkSorted cmp x (T {left,key,right,...}) =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 90 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 91 | val x = checkSorted cmp x left | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 92 | val () = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 93 | case x of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 94 | NONE => () | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 95 | | SOME k => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 96 | case cmp (k,key) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 97 | LESS => () | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 98 | | EQUAL => raise Error "duplicate keys" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 99 | | GREATER => raise Error "unsorted" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 100 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 101 | checkSorted cmp (SOME key) right | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 102 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 103 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 104 | fun checkPriorities _ E = NONE | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 105 |     | checkPriorities cmp (T (x as {left,right,...})) =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 106 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 107 | val () = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 108 | case checkPriorities cmp left of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 109 | NONE => () | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 110 | | SOME l => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 111 | case nodePriorityOrder cmp (l,x) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 112 | LESS => () | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 113 | | EQUAL => raise Error "left child has equal key" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 114 | | GREATER => raise Error "left child has greater priority" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 115 | val () = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 116 | case checkPriorities cmp right of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 117 | NONE => () | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 118 | | SOME r => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 119 | case nodePriorityOrder cmp (r,x) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 120 | LESS => () | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 121 | | EQUAL => raise Error "right child has equal key" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 122 | | GREATER => raise Error "right child has greater priority" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 123 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 124 | SOME x | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 125 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 126 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 127 | fun checkWellformed s (set as Set (cmp,tree)) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 128 | (let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 129 | val _ = checkSizes tree | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 130 | val _ = checkSorted cmp NONE tree | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 131 | val _ = checkPriorities cmp tree | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 132 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 133 | set | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 134 | end | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 135 | handle Error err => raise Bug err) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 136 | handle Bug bug => raise Bug (s ^ "\nRandomSet.checkWellformed: " ^ bug); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 137 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 138 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 139 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 140 | (* Basic operations. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 141 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 142 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 143 | fun comparison (Set (cmp,_)) = cmp; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 144 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 145 | fun empty cmp = Set (cmp,E); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 146 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 147 | fun treeSize E = 0 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 148 |   | treeSize (T {size = s, ...}) = s;
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 149 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 150 | fun size (Set (_,tree)) = treeSize tree; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 151 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 152 | fun mkT p l k r = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 153 |     T {size = treeSize l + 1 + treeSize r, priority = p,
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 154 | left = l, key = k, right = r}; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 155 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 156 | fun singleton cmp key = Set (cmp, treeSingleton key); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 157 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 158 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 159 | fun treePeek cmp E pkey = NONE | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 160 |     | treePeek cmp (T {left,key,right,...}) pkey =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 161 | case cmp (pkey,key) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 162 | LESS => treePeek cmp left pkey | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 163 | | EQUAL => SOME key | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 164 | | GREATER => treePeek cmp right pkey | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 165 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 166 | fun peek (Set (cmp,tree)) key = treePeek cmp tree key; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 167 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 168 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 169 | (* treeAppend assumes that every element of the first tree is less than *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 170 | (* every element of the second tree. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 171 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 172 | fun treeAppend _ t1 E = t1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 173 | | treeAppend _ E t2 = t2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 174 | | treeAppend cmp (t1 as T x1) (t2 as T x2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 175 | case nodePriorityOrder cmp (x1,x2) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 176 | LESS => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 177 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 178 |         val {priority = p2, left = l2, key = k2, right = r2, ...} = x2
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 179 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 180 | mkT p2 (treeAppend cmp t1 l2) k2 r2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 181 | end | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 182 | | EQUAL => raise Bug "RandomSet.treeAppend: equal keys" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 183 | | GREATER => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 184 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 185 |         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 186 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 187 | mkT p1 l1 k1 (treeAppend cmp r1 t2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 188 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 189 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 190 | (* nodePartition splits the node into three parts: the keys comparing less *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 191 | (* than the supplied key, an optional equal key, and the keys comparing *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 192 | (* greater. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 193 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 194 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 195 | fun mkLeft [] t = t | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 196 |     | mkLeft (({priority,left,key,...} : 'a node) :: xs) t =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 197 | mkLeft xs (mkT priority left key t); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 198 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 199 | fun mkRight [] t = t | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 200 |     | mkRight (({priority,key,right,...} : 'a node) :: xs) t =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 201 | mkRight xs (mkT priority t key right); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 202 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 203 | fun treePart _ _ lefts rights E = (mkLeft lefts E, NONE, mkRight rights E) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 204 | | treePart cmp pkey lefts rights (T x) = nodePart cmp pkey lefts rights x | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 205 |   and nodePart cmp pkey lefts rights (x as {left,key,right,...}) =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 206 | case cmp (pkey,key) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 207 | LESS => treePart cmp pkey lefts (x :: rights) left | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 208 | | EQUAL => (mkLeft lefts left, SOME key, mkRight rights right) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 209 | | GREATER => treePart cmp pkey (x :: lefts) rights right; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 210 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 211 | fun nodePartition cmp x pkey = nodePart cmp pkey [] [] x; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 212 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 213 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 214 | (* union first calls treeCombineRemove, to combine the values *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 215 | (* for equal keys into the first map and remove them from the second map. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 216 | (* Note that the combined key is always the one from the second map. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 217 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 218 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 219 | fun treeCombineRemove _ t1 E = (t1,E) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 220 | | treeCombineRemove _ E t2 = (E,t2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 221 | | treeCombineRemove cmp (t1 as T x1) (t2 as T x2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 222 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 223 |         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 224 | val (l2,k2,r2) = nodePartition cmp x2 k1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 225 | val (l1,l2) = treeCombineRemove cmp l1 l2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 226 | and (r1,r2) = treeCombineRemove cmp r1 r2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 227 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 228 | case k2 of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 229 | NONE => if treeSize l2 + treeSize r2 = #size x2 then (t1,t2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 230 | else (mkT p1 l1 k1 r1, treeAppend cmp l2 r2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 231 | | SOME k2 => (mkT p1 l1 k2 r1, treeAppend cmp l2 r2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 232 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 233 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 234 | fun treeUnionDisjoint _ t1 E = t1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 235 | | treeUnionDisjoint _ E t2 = t2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 236 | | treeUnionDisjoint cmp (T x1) (T x2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 237 | case nodePriorityOrder cmp (x1,x2) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 238 | LESS => nodeUnionDisjoint cmp x2 x1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 239 | | EQUAL => raise Bug "RandomSet.unionDisjoint: equal keys" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 240 | | GREATER => nodeUnionDisjoint cmp x1 x2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 241 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 242 | and nodeUnionDisjoint cmp x1 x2 = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 243 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 244 |         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 245 | val (l2,_,r2) = nodePartition cmp x2 k1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 246 | val l = treeUnionDisjoint cmp l1 l2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 247 | and r = treeUnionDisjoint cmp r1 r2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 248 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 249 | mkT p1 l k1 r | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 250 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 251 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 252 | fun union (s1 as Set (cmp,t1)) (Set (_,t2)) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 253 | if pointerEqual (t1,t2) then s1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 254 | else | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 255 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 256 | val (t1,t2) = treeCombineRemove cmp t1 t2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 257 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 258 | Set (cmp, treeUnionDisjoint cmp t1 t2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 259 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 260 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 261 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 262 | (*DEBUG | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 263 | val union = fn t1 => fn t2 => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 264 | checkWellformed "RandomSet.union: result" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 265 | (union (checkWellformed "RandomSet.union: input 1" t1) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 266 | (checkWellformed "RandomSet.union: input 2" t2)); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 267 | *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 268 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 269 | (* intersect is a simple case of the union algorithm. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 270 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 271 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 272 | fun treeIntersect _ _ E = E | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 273 | | treeIntersect _ E _ = E | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 274 | | treeIntersect cmp (t1 as T x1) (t2 as T x2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 275 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 276 |         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 277 | val (l2,k2,r2) = nodePartition cmp x2 k1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 278 | val l = treeIntersect cmp l1 l2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 279 | and r = treeIntersect cmp r1 r2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 280 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 281 | case k2 of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 282 | NONE => treeAppend cmp l r | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 283 | | SOME k2 => mkT p1 l k2 r | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 284 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 285 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 286 | fun intersect (s1 as Set (cmp,t1)) (Set (_,t2)) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 287 | if pointerEqual (t1,t2) then s1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 288 | else Set (cmp, treeIntersect cmp t1 t2); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 289 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 290 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 291 | (*DEBUG | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 292 | val intersect = fn t1 => fn t2 => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 293 | checkWellformed "RandomSet.intersect: result" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 294 | (intersect (checkWellformed "RandomSet.intersect: input 1" t1) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 295 | (checkWellformed "RandomSet.intersect: input 2" t2)); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 296 | *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 297 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 298 | (* delete raises an exception if the supplied key is not found, which *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 299 | (* makes it simpler to maximize sharing. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 300 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 301 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 302 | fun treeDelete _ E _ = raise Error "RandomSet.delete: element not found" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 303 |     | treeDelete cmp (T {priority,left,key,right,...}) dkey =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 304 | case cmp (dkey,key) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 305 | LESS => mkT priority (treeDelete cmp left dkey) key right | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 306 | | EQUAL => treeAppend cmp left right | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 307 | | GREATER => mkT priority left key (treeDelete cmp right dkey); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 308 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 309 | fun delete (Set (cmp,tree)) key = Set (cmp, treeDelete cmp tree key); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 310 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 311 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 312 | (*DEBUG | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 313 | val delete = fn t => fn x => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 314 | checkWellformed "RandomSet.delete: result" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 315 | (delete (checkWellformed "RandomSet.delete: input" t) x); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 316 | *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 317 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 318 | (* Set difference *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 319 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 320 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 321 | fun treeDifference _ t1 E = t1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 322 | | treeDifference _ E _ = E | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 323 | | treeDifference cmp (t1 as T x1) (T x2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 324 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 325 |         val {size = s1, priority = p1, left = l1, key = k1, right = r1} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 326 | val (l2,k2,r2) = nodePartition cmp x2 k1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 327 | val l = treeDifference cmp l1 l2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 328 | and r = treeDifference cmp r1 r2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 329 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 330 | if Option.isSome k2 then treeAppend cmp l r | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 331 | else if treeSize l + treeSize r + 1 = s1 then t1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 332 | else mkT p1 l k1 r | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 333 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 334 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 335 | fun difference (Set (cmp,tree1)) (Set (_,tree2)) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 336 | if pointerEqual (tree1,tree2) then Set (cmp,E) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 337 | else Set (cmp, treeDifference cmp tree1 tree2); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 338 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 339 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 340 | (*DEBUG | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 341 | val difference = fn t1 => fn t2 => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 342 | checkWellformed "RandomSet.difference: result" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 343 | (difference (checkWellformed "RandomSet.difference: input 1" t1) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 344 | (checkWellformed "RandomSet.difference: input 2" t2)); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 345 | *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 346 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 347 | (* Subsets *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 348 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 349 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 350 | fun treeSubset _ E _ = true | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 351 | | treeSubset _ _ E = false | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 352 | | treeSubset cmp (t1 as T x1) (T x2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 353 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 354 |         val {size = s1, left = l1, key = k1, right = r1, ...} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 355 |         and {size = s2, ...} = x2
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 356 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 357 | s1 <= s2 andalso | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 358 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 359 | val (l2,k2,r2) = nodePartition cmp x2 k1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 360 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 361 | Option.isSome k2 andalso | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 362 | treeSubset cmp l1 l2 andalso | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 363 | treeSubset cmp r1 r2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 364 | end | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 365 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 366 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 367 | fun subset (Set (cmp,tree1)) (Set (_,tree2)) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 368 | pointerEqual (tree1,tree2) orelse | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 369 | treeSubset cmp tree1 tree2; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 370 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 371 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 372 | (* Set equality *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 373 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 374 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 375 | fun treeEqual _ E E = true | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 376 | | treeEqual _ E _ = false | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 377 | | treeEqual _ _ E = false | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 378 | | treeEqual cmp (t1 as T x1) (T x2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 379 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 380 |         val {size = s1, left = l1, key = k1, right = r1, ...} = x1
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 381 |         and {size = s2, ...} = x2
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 382 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 383 | s1 = s2 andalso | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 384 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 385 | val (l2,k2,r2) = nodePartition cmp x2 k1 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 386 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 387 | Option.isSome k2 andalso | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 388 | treeEqual cmp l1 l2 andalso | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 389 | treeEqual cmp r1 r2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 390 | end | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 391 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 392 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 393 | fun equal (Set (cmp,tree1)) (Set (_,tree2)) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 394 | pointerEqual (tree1,tree2) orelse | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 395 | treeEqual cmp tree1 tree2; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 396 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 397 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 398 | (* filter is the basic function for preserving the tree structure. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 399 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 400 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 401 | fun treeFilter _ _ E = E | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 402 |     | treeFilter cmp pred (T {priority,left,key,right,...}) =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 403 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 404 | val left = treeFilter cmp pred left | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 405 | and right = treeFilter cmp pred right | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 406 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 407 | if pred key then mkT priority left key right | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 408 | else treeAppend cmp left right | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 409 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 410 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 411 | fun filter pred (Set (cmp,tree)) = Set (cmp, treeFilter cmp pred tree); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 412 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 413 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 414 | (* nth picks the nth smallest key (counting from 0). *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 415 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 416 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 417 | fun treeNth E _ = raise Subscript | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 418 |     | treeNth (T {left,key,right,...}) n =
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 419 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 420 | val k = treeSize left | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 421 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 422 | if n = k then key | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 423 | else if n < k then treeNth left n | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 424 | else treeNth right (n - (k + 1)) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 425 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 426 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 427 | fun nth (Set (_,tree)) n = treeNth tree n; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 428 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 429 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 430 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 431 | (* Iterators. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 432 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 433 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 434 | fun leftSpine E acc = acc | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 435 |   | leftSpine (t as T {left,...}) acc = leftSpine left (t :: acc);
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 436 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 437 | fun rightSpine E acc = acc | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 438 |   | rightSpine (t as T {right,...}) acc = rightSpine right (t :: acc);
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 439 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 440 | datatype 'a iterator = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 441 | LR of 'a * 'a tree * 'a tree list | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 442 | | RL of 'a * 'a tree * 'a tree list; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 443 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 444 | fun mkLR [] = NONE | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 445 |   | mkLR (T {key,right,...} :: l) = SOME (LR (key,right,l))
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 446 | | mkLR (E :: _) = raise Bug "RandomSet.mkLR"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 447 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 448 | fun mkRL [] = NONE | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 449 |   | mkRL (T {key,left,...} :: l) = SOME (RL (key,left,l))
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 450 | | mkRL (E :: _) = raise Bug "RandomSet.mkRL"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 451 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 452 | fun mkIterator (Set (_,tree)) = mkLR (leftSpine tree []); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 453 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 454 | fun mkRevIterator (Set (_,tree)) = mkRL (rightSpine tree []); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 455 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 456 | fun readIterator (LR (key,_,_)) = key | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 457 | | readIterator (RL (key,_,_)) = key; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 458 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 459 | fun advanceIterator (LR (_,next,l)) = mkLR (leftSpine next l) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 460 | | advanceIterator (RL (_,next,l)) = mkRL (rightSpine next l); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 461 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 462 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 463 | (* Derived operations. *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 464 | (* ------------------------------------------------------------------------- *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 465 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 466 | fun null s = size s = 0; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 467 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 468 | fun member x s = Option.isSome (peek s x); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 469 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 470 | (* add must be primitive to get hold of the comparison function *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 471 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 472 | fun add s x = union s (singleton (comparison s) x); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 473 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 474 | (*DEBUG | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 475 | val add = fn s => fn x => | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 476 | checkWellformed "RandomSet.add: result" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 477 | (add (checkWellformed "RandomSet.add: input" s) x); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 478 | *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 479 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 480 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 481 | fun unionPairs ys [] = rev ys | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 482 | | unionPairs ys (xs as [_]) = List.revAppend (ys,xs) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 483 | | unionPairs ys (x1 :: x2 :: xs) = unionPairs (union x1 x2 :: ys) xs; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 484 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 485 | fun unionList [] = raise Error "Set.unionList: no sets" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 486 | | unionList [s] = s | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 487 | | unionList l = unionList (unionPairs [] l); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 488 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 489 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 490 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 491 | fun intersectPairs ys [] = rev ys | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 492 | | intersectPairs ys (xs as [_]) = List.revAppend (ys,xs) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 493 | | intersectPairs ys (x1 :: x2 :: xs) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 494 | intersectPairs (intersect x1 x2 :: ys) xs; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 495 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 496 | fun intersectList [] = raise Error "Set.intersectList: no sets" | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 497 | | intersectList [s] = s | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 498 | | intersectList l = intersectList (intersectPairs [] l); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 499 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 500 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 501 | fun symmetricDifference s1 s2 = union (difference s1 s2) (difference s2 s1); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 502 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 503 | fun disjoint s1 s2 = null (intersect s1 s2); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 504 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 505 | fun partition pred set = (filter pred set, filter (not o pred) set); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 506 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 507 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 508 | fun fold _ NONE acc = acc | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 509 | | fold f (SOME iter) acc = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 510 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 511 | val key = readIterator iter | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 512 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 513 | fold f (advanceIterator iter) (f (key,acc)) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 514 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 515 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 516 | fun foldl f b m = fold f (mkIterator m) b; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 517 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 518 | fun foldr f b m = fold f (mkRevIterator m) b; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 519 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 520 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 521 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 522 | fun find _ NONE = NONE | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 523 | | find pred (SOME iter) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 524 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 525 | val key = readIterator iter | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 526 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 527 | if pred key then SOME key | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 528 | else find pred (advanceIterator iter) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 529 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 530 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 531 | fun findl p m = find p (mkIterator m); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 532 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 533 | fun findr p m = find p (mkRevIterator m); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 534 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 535 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 536 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 537 | fun first _ NONE = NONE | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 538 | | first f (SOME iter) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 539 | let | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 540 | val key = readIterator iter | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 541 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 542 | case f key of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 543 | NONE => first f (advanceIterator iter) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 544 | | s => s | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 545 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 546 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 547 | fun firstl f m = first f (mkIterator m); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 548 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 549 | fun firstr f m = first f (mkRevIterator m); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 550 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 551 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 552 | fun count p = foldl (fn (x,n) => if p x then n + 1 else n) 0; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 553 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 554 | fun fromList cmp l = List.foldl (fn (k,s) => add s k) (empty cmp) l; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 555 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 556 | fun addList s l = union s (fromList (comparison s) l); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 557 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 558 | fun toList s = foldr op:: [] s; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 559 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 560 | fun map f s = rev (foldl (fn (x,l) => (x, f x) :: l) [] s); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 561 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 562 | fun transform f s = rev (foldl (fn (x,l) => f x :: l) [] s); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 563 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 564 | fun app f s = foldl (fn (x,()) => f x) () s; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 565 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 566 | fun exists p s = Option.isSome (findl p s); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 567 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 568 | fun all p s = not (exists (not o p) s); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 569 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 570 | local | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 571 | fun iterCompare _ NONE NONE = EQUAL | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 572 | | iterCompare _ NONE (SOME _) = LESS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 573 | | iterCompare _ (SOME _) NONE = GREATER | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 574 | | iterCompare cmp (SOME i1) (SOME i2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 575 | keyIterCompare cmp (readIterator i1) (readIterator i2) i1 i2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 576 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 577 | and keyIterCompare cmp k1 k2 i1 i2 = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 578 | case cmp (k1,k2) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 579 | LESS => LESS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 580 | | EQUAL => iterCompare cmp (advanceIterator i1) (advanceIterator i2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 581 | | GREATER => GREATER; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 582 | in | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 583 | fun compare (s1,s2) = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 584 | if pointerEqual (s1,s2) then EQUAL | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 585 | else | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 586 | case Int.compare (size s1, size s2) of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 587 | LESS => LESS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 588 | | EQUAL => iterCompare (comparison s1) (mkIterator s1) (mkIterator s2) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 589 | | GREATER => GREATER; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 590 | end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 591 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 592 | fun pick s = | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 593 | case findl (K true) s of | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 594 | SOME p => p | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 595 | | NONE => raise Error "RandomSet.pick: empty"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 596 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 597 | fun random s = case size s of 0 => raise Empty | n => nth s (randomInt n); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 598 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 599 | fun deletePick s = let val x = pick s in (x, delete s x) end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 600 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 601 | fun deleteRandom s = let val x = random s in (x, delete s x) end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 602 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 603 | fun close f s = let val s' = f s in if equal s s' then s else close f s' end; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 604 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 605 | fun toString s = "{" ^ (if null s then "" else Int.toString (size s)) ^ "}";
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 606 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 607 | end |