Changeset 1023

Show
Ignore:
Timestamp:
11/24/07 10:18:34 (1 year ago)
Author:
mspiegel
Message:

Strengthened the trait declarations in the Skiplist implementation.

Files:

Legend:

Unmodified
Added
Removed
Modified
Copied
Moved

  • trunk/ProjectFortress/test_library/SkipList.fsi

    r1022 r1023  
    1818api SkipList 
    1919 
     20(* A SkipList type consists of a root node and pInverse = 1/p, where the fraction 
     21   p is used in the negative binomial distribution to select random levels for insertion. 
     22*) 
    2023object SkipList[\Key,Val,nat pInverse\](root:Node[\Key,Val\]) end 
    2124 
     25(* Construct an empty skip list *) 
    2226NewList[\Key,Val,nat pInverse\]():SkipList[\Key,Val,pInverse\] 
    2327 
     28 
     29(* A Node is the basic type for the Skip List data structure. 
     30   There are four types of Nodes: 
     31    i)   Empty Nodes - represents an empty tree. 
     32    ii)  Leaf Nodes - stores a (key,val) pair. Lives at the bottom of the tree. 
     33    iii) Internal Nodes - stores N keys and N+1 children for N > 0. 
     34    iv)  White Nodes - stores exactly zero keys and one child. 
     35*) 
    2436trait Node[\Key,Val\] comprises {EmptyNode[\Key,Val\], LeafNode[\Key,Val\], 
    25   InternalNode[\Key,Val\], WhiteNode[\Key,Val\]} 
     37  WhiteNode[\Key,Val\], InternalNode[\Key,Val\]} 
    2638 
    27   getHeight():ZZ32 
    28   getSize():ZZ32 
     39  (* The height of the current node.  Height = 0 must be a leaf *) 
     40  getter height():ZZ32 
    2941 
    30   isLeaf():Boolean 
    31   isTreeEmpty():Boolean 
    32   isNodeEmpty():Boolean 
     42  (* The number of values stores in this subtree.  The number of  
     43     values is greater than or equal to the number of keys, 
     44     as duplicates are allowed in this implementation. *)   
     45  getter size():ZZ32 
    3346 
     47  (* given a search key, try to return a value that matches that key *) 
    3448  search(k:Key):Maybe[\Val\] 
    3549 
    3650  toString():String 
     51  (* toGraphViz():String   wait until hashCode() is implemented*) 
    3752 
     53  (* the add method will grow the tree if level > root height *) 
    3854  add(leaf:LeafNode[\Key,Val\], level:ZZ32):Node[\Key,Val\] 
     55 
     56  (* the add_helper method is only invoked if level <= root height *) 
     57  (* returns the new node and whether a new key was inserted *) 
    3958  add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\], Boolean) 
    4059 
     60  (* perform a search operation, and remove a value if it is found *) 
    4161  remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) 
    4262 
    4363  (* merge must always be invoked with at least one element in the merge list *) 
    4464  merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] 
    45  
     65   
    4666  (* return the list of leaves that are under the current subtree *) 
    4767  getLeaves():List[\LeafNode[\Key,Val\]\] 
    4868 
    49   (* splits the new child in half and sucks the split key up to this level *) 
    50   split(index:ZZ32, heir:Node[\Key,Val\]):InternalNode[\Key,Val\] 
     69end 
    5170 
    52   (* breaks the keys of this node into two new nodes *) 
    53   break():(Node[\Key,Val\],Node[\Key,Val\],Key) 
     71(* There are two types of white nodes: 
     72    a) WhiteLevel1 are white nodes that live at level 1 of the tree.  Their children are leaves. 
     73    b) WhiteLevelN are white nodes that live at level > 1 of the tree. Their children are non-leaves. *) 
     74trait WhiteNode[\Key,Val\] extends Node[\Key,Val\] excludes InternalNode[\Key,Val\] comprises {WhiteLevel1[\Key,Val\], WhiteLevelN[\Key,Val\]} end 
     75 
     76 
     77(* There are two types of internal nodes: 
     78    a) InternalLevel1 are internal nodes that live at level 1 of the tree.  Their children are leaves. 
     79    b) InternalLevelN are internal nodes that live at level > 1 of the tree. Their children are non-leaves. *)     
     80trait InternalNode[\Key,Val\] extends Node[\Key,Val\] excludes WhiteNode[\Key,Val\] comprises {InternalLevel1[\Key,Val\], InternalLevelN[\Key, Val\]} end 
     81 
     82(* There are four types of NonLeafNodes and they are the union of the WhiteNode types and InternalNode types *) 
     83trait NonLeafNode[\Key,Val\] extends Node[\Key,Val\] comprises {WhiteLevel1[\Key,Val\], WhiteLevelN[\Key,Val\], InternalLevel1[\Key,Val\], InternalLevelN[\Key, Val\]} end 
     84 
     85(* WhiteNodeHelper is the trait that is used to distinguish between WhiteLevel1 and WhiteLevelN *) 
     86trait WhiteNodeHelper[\Key,Val,ChildType extends Node[\Key,Val\]\] extends Node[\Key,Val\]  
     87  comprises {WhiteLevel1[\Key,Val\], WhiteLevelN[\Key,Val\]} 
     88 
     89  getter child():ChildType 
     90   
     91end 
     92 
     93(* InternalNodeHelper is the trait that is used to distinguish between InternalLevel1 and InternalLevelN *) 
     94trait InternalNodeHelper[\SelfType extends InternalNodeHelper[\SelfType,Key,Val,ChildType\],Key,Val,ChildType extends Node\] 
     95  extends Node[\Key,Val\] comprises {InternalLevel1[\Key,Val\], InternalLevelN[\Key,Val\]} 
     96 
     97  getter keys():Array[\Key,ZZ32\] 
     98  getter children():Array[\ChildType,ZZ32\] 
     99 
     100  (* given an instance of SelfType, generate a singleton SelfType *) 
     101  singleton(keys':Array[\Key,ZZ32\], children':Array[\ChildType,ZZ32\]) : SelfType 
     102   
     103  (* given a key k, return the largest offset with a value less than or equal to k *) 
     104  find_index(k:Key):ZZ32 
     105 
     106  (* break this internal node in half.  Returns the two halves along with the key used for breaking *) 
     107  break():(NonLeafNode[\Key,Val\],NonLeafNode[\Key,Val\],Key) 
     108   
     109  (* return a new internal node that has children[index] and keys[index - 1] missing *) 
     110  index_remove(index:ZZ32): SelfType 
    54111 
    55112end 
    56113 
    57 generate_tail[\Key,Val\](node:Node[\Key,Val\], length:ZZ32):Node[\Key,Val\] 
     114(* Given a length > 0 and a node, generate that many white nodes that  
     115   connect "as a tail" to the node. *) 
     116generate_tail[\Key,Val\](node:LeafNode[\Key,Val\], length:ZZ32):Node[\Key,Val\] 
     117generate_tail[\Key,Val\](node:NonLeafNode[\Key,Val\], length:ZZ32):Node[\Key,Val\] 
    58118 
    59 (* The four types of nodes: EmptyNode, WhiteNode, LeafNode, and InternalNode *) 
     119(* Represents an empty tree *) 
    60120object EmptyNode[\Key,Val\]() extends Node[\Key,Val\] end 
    61 object WhiteNode[\Key,Val\](child:Node[\Key,Val\]) extends Node[\Key,Val\] end 
    62 object LeafNode[\Key,Val\](pair: (Key, Val)) extends Node[\Key,Val\] end 
    63 object InternalNode[\Key,Val\](keys:Array[\Key,ZZ32\], children:Array[\Node[\Key,Val\],ZZ32\]) extends Node[\Key,Val\] end 
     121 
     122(* A leaf node.  For a given unique key, stores an array of values *) 
     123object LeafNode[\Key,Val\](key: Key, values: Array[\Val,ZZ32\]) extends Node[\Key,Val\] end 
     124 
     125(* A white node with one leaf child *) 
     126object WhiteLevel1[\Key,Val\](child:LeafNode[\Key,Val\]) extends {WhiteNode[\Key,Val\],  
     127  WhiteNodeHelper[\Key,Val,LeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} end 
     128 
     129(* A white node with one nonleaf child *) 
     130object WhiteLevelN[\Key,Val\](child:NonLeafNode[\Key,Val\]) extends {WhiteNode[\Key,Val\],  
     131  WhiteNodeHelper[\Key,Val,NonLeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} end 
     132 
     133(* An internal node with k keys and k + 1 leaf children *) 
     134object InternalLevel1[\Key,Val\](keys:Array[\Key,ZZ32\], 
     135  children:Array[\LeafNode[\Key,Val\],ZZ32\]) extends {InternalNode[\Key,Val\],  
     136  InternalNodeHelper[\InternalLevel1[\Key,Val\],Key,Val,LeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} end 
     137 
     138(* An internal node with k keys and k + 1 nonleaf children *) 
     139object InternalLevelN[\Key,Val\](keys:Array[\Key,ZZ32\], 
     140  children:Array[\NonLeafNode[\Key,Val\],ZZ32\]) extends {InternalNode[\Key,Val\],  
     141  InternalNodeHelper[\InternalLevelN[\Key,Val\],Key,Val,NonLeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} end 
    64142 
    65143end 

  • trunk/ProjectFortress/test_library/SkipList.fss

    r1022 r1023  
    3434   All leaves live in level 0 of the tree, and values are stored only in the leaf 
    3535   nodes. 
     36    
     37   This implementation of skip trees supports multiple values for a unique key. 
     38   If a key contains multiple values, then an arbitrary value is returned on 
     39   a search for that key. 
    3640 
    3741***************************************************************************) 
    …… 
    4650  toString():String = root.toString() 
    4751 
    48   getSize():ZZ32 = root.getSize() 
    49   getRoot():Node[\Key,Val\] = root 
    50  
     52  (* The number of values stores in this tree. *) 
     53  size():ZZ32 = root.size() 
     54 
     55  (* given a search key, try to return a value that matches that key *) 
    5156  search(k:Key):Maybe[\Val\] = root.search(k) 
    5257 
     58  (* add a (key, value) pair to this tree *) 
    5359  add(k:Key, v:Val):SkipList[\Key,Val,pInverse\] = do 
    5460    level:ZZ32 = randomLevel() 
    …… 
    5965  end 
    6066 
     67  (* remove one (key, value) pair from this tree *) 
    6168  remove(k:Key):SkipList[\Key,Val,pInverse\] = do 
    6269    (root', maybe) = root.remove(k) 
    …… 
    6471  end 
    6572 
     73  (* merge two skip trees *) 
    6674  merge(other:SkipList[\Key,Val,pInverse\]):SkipList[\Key,Val,pInverse\] = do 
    67     (larger, smaller) = if self.getSize() > other.getSize() then (self, other) else (other, self) end 
    68     smallList = singleton[\Node[\Key,Val\]\](smaller.getRoot()) 
    69     SkipList[\Key,Val,pInverse\](larger.getRoot().merge(smallList)) 
     75    (larger, smaller) = if self.size() > other.size() then (self, other) else (other, self) end 
     76    smallList = singleton[\Node[\Key,Val\]\](smaller.root) 
     77    SkipList[\Key,Val,pInverse\](larger.root.merge(smallList)) 
    7078  end 
    7179 
    …… 
    8492NewList[\Key,Val,nat pInverse\]():SkipList[\Key,Val,pInverse\] = 
    8593  SkipList[\Key,Val,pInverse\](EmptyNode[\Key,Val\]()) 
    86    
    8794 
    8895 
    …… 
    95102*) 
    96103trait Node[\Key,Val\] comprises {EmptyNode[\Key,Val\], LeafNode[\Key,Val\], 
    97   InternalNode[\Key,Val\], WhiteNode[\Key,Val\]} 
    98  
    99   getHeight():ZZ32 
    100   getSize():ZZ32 
    101    
    102    
    103   isLeaf():Boolean 
    104   isTreeEmpty():Boolean 
    105   isNodeEmpty():Boolean 
    106  
     104  WhiteNode[\Key,Val\], InternalNode[\Key,Val\]} 
     105 
     106  (* The height of the current node.  Height = 0 must be a leaf *) 
     107  getter height():ZZ32 
     108 
     109  (* The number of values stores in this subtree.  The number of  
     110     values is greater than or equal to the number of keys, 
     111     as duplicates are allowed in this implementation. *)   
     112  getter size():ZZ32 
     113 
     114  (* given a search key, try to return a value that matches that key *) 
    107115  search(k:Key):Maybe[\Val\] 
    108116 
    …… 
    117125  add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\], Boolean) 
    118126 
     127  (* perform a search operation, and remove a value if it is found *) 
    119128  remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) 
    120129 
    …… 
    125134  getLeaves():List[\LeafNode[\Key,Val\]\] 
    126135 
    127   (* splits the new child in half and sucks the split key up to this level *) 
    128   split(index:ZZ32, heir:Node[\Key,Val\]):InternalNode[\Key,Val\] 
    129  
    130   (* breaks the keys of this node into two new nodes *) 
    131   break():(Node[\Key,Val\],Node[\Key,Val\],Key) 
    132  
    133 end 
    134  
    135  
    136 generate_tail[\Key,Val\](node:Node[\Key,Val\], length:ZZ32):Node[\Key,Val\] = 
     136end 
     137 
     138 
     139(* There are two types of white nodes: 
     140    a) WhiteLevel1 are white nodes that live at level 1 of the tree.  Their children are leaves. 
     141    b) WhiteLevelN are white nodes that live at level > 1 of the tree. Their children are non-leaves. *) 
     142trait WhiteNode[\Key,Val\] extends Node[\Key,Val\] excludes InternalNode[\Key,Val\] comprises {WhiteLevel1[\Key,Val\], WhiteLevelN[\Key,Val\]} end 
     143 
     144(* There are two types of internal nodes: 
     145    a) InternalLevel1 are internal nodes that live at level 1 of the tree.  Their children are leaves. 
     146    b) InternalLevelN are internal nodes that live at level > 1 of the tree. Their children are non-leaves. *)     
     147trait InternalNode[\Key,Val\] extends Node[\Key,Val\] excludes WhiteNode[\Key,Val\] comprises {InternalLevel1[\Key,Val\], InternalLevelN[\Key, Val\]} end 
     148 
     149(* There are four types of NonLeafNodes and they are the union of the WhiteNode types and InternalNode types *) 
     150trait NonLeafNode[\Key,Val\] extends Node[\Key,Val\] comprises {WhiteLevel1[\Key,Val\], WhiteLevelN[\Key,Val\], InternalLevel1[\Key,Val\], InternalLevelN[\Key, Val\]} end 
     151 
     152(* WhiteNodeHelper is the trait that is used to distinguish between WhiteLevel1 and WhiteLevelN *) 
     153trait WhiteNodeHelper[\Key,Val,ChildType extends Node[\Key,Val\]\] extends Node[\Key,Val\]  
     154  comprises {WhiteLevel1[\Key,Val\], WhiteLevelN[\Key,Val\]} 
     155 
     156  getter child():ChildType 
     157  getter size():ZZ32 = child.size() 
     158  getter height():ZZ32 = child.height() + 1 
     159 
     160  search(k:Key):Maybe[\Val\] = child.search(k) 
     161 
     162  toString():String = "{ [], [" child.toString() "] }" 
     163 
     164  add(leaf:LeafNode[\Key,Val\], level:ZZ32):Node[\Key,Val\] = do 
     165    tail:Node[\Key,Val\] = generate_tail[\Key,Val\](self, level - height()) 
     166    (newNode, newKey) = tail.add_helper(leaf, level) 
     167    newNode 
     168  end 
     169 
     170  getLeaves():List[\LeafNode[\Key,Val\]\] = child.getLeaves() 
     171   
     172end 
     173 
     174(* InternalNodeHelper is the trait that is used to distinguish between InternalLevel1 and InternalLevelN *) 
     175trait InternalNodeHelper[\SelfType extends InternalNodeHelper[\SelfType,Key,Val,ChildType\],Key,Val,ChildType extends Node\] 
     176  extends Node[\Key,Val\] comprises {InternalLevel1[\Key,Val\], InternalLevelN[\Key,Val\]} 
     177   
     178  getter keys():Array[\Key,ZZ32\] 
     179  getter children():Array[\ChildType,ZZ32\] 
     180 
     181  getter size():ZZ32 = children.generate[\ZZ32\](SumReduction[\ZZ32\](), 
     182                                        fn (node:Node[\Key,Val\]):ZZ32 => node.size()) 
     183                                         
     184  getter height():ZZ32 = children[0].height() + 1 
     185 
     186  (* given an instance of SelfType, generate a singleton SelfType *) 
     187  singleton(keys':Array[\Key,ZZ32\], children':Array[\ChildType,ZZ32\]) : SelfType 
     188 
     189  (* given a key k, return the largest offset with a value less than or equal to k *) 
     190  find_index(k:Key):ZZ32 = do 
     191    index:ZZ32 := 0 
     192    while (index < keys.size() AND: k >= keys[index]) do 
     193      index += 1 
     194    end 
     195    index 
     196  end 
     197 
     198  search(k:Key):Maybe[\Val\] = do 
     199    index:ZZ32 = find_index(k) 
     200    children[index].search(k) 
     201  end 
     202 
     203  toString():String = "{" keys.toString() ", " children.toString() "}" 
     204 
     205  add(leaf:LeafNode[\Key,Val\], level:ZZ32):Node[\Key,Val\] = do 
     206    tail:Node[\Key,Val\] = generate_tail[\Key,Val\](self, level - height()) 
     207    (newNode, newKey) = tail.add_helper(leaf, level) 
     208    newNode 
     209  end 
     210 
     211  getLeaves():List[\LeafNode[\Key,Val\]\] = children.generate[\List[\LeafNode[\Key,Val\]\]\]( 
     212    Concat[\LeafNode[\Key,Val\]\](), 
     213    fn (node:Node[\Key,Val\]): List[\LeafNode[\Key,Val\]\] => node.getLeaves()) 
     214 
     215  (* break this internal node in half.  Returns the two halves along with the key used for breaking *) 
     216  break():(NonLeafNode[\Key,Val\],NonLeafNode[\Key,Val\],Key) = 
     217  if keys.size() = 1 then 
     218    onekey_break() 
     219  elif keys.size() = 2 then 
     220    twokeys_break() 
     221  else 
     222    nkeys_break() 
     223  end 
     224 
     225  (* perform the break operation when we have exactly one key *) 
     226  onekey_break():(NonLeafNode[\Key,Val\],NonLeafNode[\Key,Val\],Key) = do 
     227    smaller:Node[\Key,Val\] = children[0] 
     228    larger:Node[\Key,Val\] = children[1] 
     229    key':Key = keys[0] 
     230    left:NonLeafNode[\Key,Val\] = generate_tail[\Key,Val\](smaller, 1) 
     231    right:NonLeafNode[\Key,Val\] = generate_tail[\Key,Val\](larger, 1) 
     232    (left, right, key') 
     233  end 
     234 
     235  (* perform the break operation when we have exactly two keys *) 
     236  twokeys_break():(NonLeafNode[\Key,Val\],NonLeafNode[\Key,Val\],Key) = do 
     237    smaller:Node[\Key,Val\] = children[0] 
     238    rkeys:Array[\Key,ZZ32\] = array[\Key\](1) 
     239    rchildren:Array[\ChildType,ZZ32\] = array[\ChildType\](2) 
     240    key':Key = keys[0] 
     241    rkeys[0] := keys[1] 
     242    rchildren[0#2] := children[1#2] 
     243    left:NonLeafNode[\Key,Val\] = generate_tail[\Key,Val\](smaller, 1) 
     244    right:NonLeafNode[\Key,Val\] = singleton(rkeys,rchildren) 
     245    (left, right, key') 
     246  end 
     247 
     248  (* perform the break operation when we have three or more keys *) 
     249  nkeys_break():(NonLeafNode[\Key,Val\],NonLeafNode[\Key,Val\],Key) = do 
     250    half:ZZ32 = keys.size() DIV 2 
     251    rsize:ZZ32 = keys.size() - half - 1 
     252    lsize:ZZ32 = keys.size() - rsize - 1 
     253    key':Key = keys[half] 
     254    lkeys:Array[\Key,ZZ32\] = array[\Key\](lsize) 
     255    lchildren:Array[\ChildType,ZZ32\] = array[\ChildType\](lsize + 1) 
     256    rkeys:Array[\Key,ZZ32\] = array[\Key\](rsize) 
     257    rchildren:Array[\ChildType,ZZ32\] = array[\ChildType\](rsize + 1) 
     258    lkeys[0 # lsize] := keys[0 # lsize] 
     259    lchildren[0 # (lsize + 1)] := children[0 # (lsize + 1)] 
     260    rkeys[0 # rsize] := keys[(half + 1) # rsize] 
     261    rchildren[0 # (rsize + 1)] := children[(half + 1) # (rsize + 1)] 
     262    left:NonLeafNode[\Key,Val\] = singleton(lkeys,lchildren) 
     263    right:NonLeafNode[\Key,Val\] = singleton(rkeys,rchildren) 
     264    (left, right, key') 
     265  end 
     266   
     267  (* return a new internal node that has children[index] and keys[index - 1] missing *) 
     268  index_remove(index:ZZ32): SelfType = do 
     269    keys':Array[\Key,ZZ32\] = array[\Key\](keys.size() - 1) 
     270    children':Array[\ChildType,ZZ32\] = array[\ChildType\](children.size() - 1) 
     271    replace:ZZ32 = MAX(0, index - 1) 
     272    keys'[0 # replace] := keys[0 # replace] 
     273    keys'[replace # (keys'.size() - replace)] := keys[(replace + 1) # (keys'.size() - replace)] 
     274    children'[0 # index] := children[0 # index] 
     275    children'[index # (children'.size() - index)] := children[(index + 1) # (children'.size() - index)] 
     276    singleton(keys', children') 
     277  end   
     278   
     279end 
     280 
     281(* Helper function to generate a tail of white nodes coming off a leaf node *) 
     282generate_tail[\Key,Val\](node:LeafNode[\Key,Val\], length:ZZ32):Node[\Key,Val\] = 
    137283if length > 0 then 
    138   generate_tail[\Key,Val\](WhiteNode[\Key,Val\](node), length - 1) 
     284  generate_tail[\Key,Val\](WhiteLevel1[\Key,Val\](node), length - 1) 
    139285else 
    140286  node 
    141287end 
    142288 
     289(* Helper function to generate a tail of white nodes coming off a non leaf node *) 
     290generate_tail[\Key,Val\](node:NonLeafNode[\Key,Val\], length:ZZ32):Node[\Key,Val\] = 
     291if length > 0 then 
     292  generate_tail[\Key,Val\](WhiteLevelN[\Key,Val\](node), length - 1) 
     293else 
     294  node 
     295end 
    143296 
    144297(* A white node stores exactly zero keys and contains one child. White nodes are 
    145298   used as placeholders to keep the height of all branches identical. A white node 
    146299   has a height > 0 *) 
    147 object WhiteNode[\Key,Val\](child:Node[\Key,Val\]) extends Node[\Key,Val\] 
    148  
    149   size:ZZ32 = child.getSize() 
    150   height:ZZ32 = child.getHeight() + 1 
    151   getHeight():ZZ32 = height 
    152   getSize():ZZ32 = size 
    153  
    154   isLeaf():Boolean = false 
    155   isTreeEmpty():Boolean = false 
    156   isNodeEmpty():Boolean = true 
    157  
    158   search(k:Key):Maybe[\Val\] = child.search(k) 
    159  
    160   toString():String = "{ [], [" child.toString() "] }" 
    161  
    162   add(leaf:LeafNode[\Key,Val\], level:ZZ32):Node[\Key,Val\] = do 
    163     tail:Node[\Key,Val\] = generate_tail[\Key,Val\](self, level - getHeight()) 
    164     (newNode, newKey) = tail.add_helper(leaf, level) 
    165     newNode 
    166   end 
    167  
    168   add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\], Boolean) = 
    169   if height = 1 then 
    170     height1_add(leaf) 
    171   else 
    172     heightn_add(leaf, level) 
    173   end 
    174  
    175   remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) = do 
    176     if height = 1 then 
    177       height1_remove(k) 
    178     else 
    179       heightn_remove(k) 
    180     end 
    181   end 
    182  
    183   (* splits the new child in half and sucks the split key up to this level *) 
    184   split(index:ZZ32, heir:Node[\Key,Val\]):InternalNode[\Key,Val\] = do 
    185     keys:Array[\Key,ZZ32\] = array[\Key\](1) 
    186     children:Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](2) 
    187     (left,right,key') = heir.break() 
    188     keys[0] := key' 
    189     children[0] := left 
    190     children[1] := right 
    191     InternalNode[\Key,Val\](keys,children) 
    192   end 
    193  
    194   break():(Node[\Key,Val\],Node[\Key,Val\],Key) = fail("Cannot break a white node") 
    195  
    196  
    197   merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] =  
    198   if height = 1 then   
    199     height1_merge(nodes) 
    200   else 
    201     heightn_merge(nodes) 
    202   end 
    203  
    204   (* perform the add operation when the height is one *) 
    205   height1_add(leaf:LeafNode[\Key,Val\]):(Node[\Key,Val\], Boolean) = do 
     300object WhiteLevel1[\Key,Val\](child:LeafNode[\Key,Val\]) extends {WhiteNode[\Key,Val\], WhiteNodeHelper[\Key,Val,LeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} 
     301 
     302  getter child():LeafNode[\Key,Val\] = child 
     303 
     304  add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\], Boolean) = do 
    206305    k:Key = leaf.key 
    207306    k':Key = child.key 
    …… 
    211310      values[leaf.values.size() # child.values.size()] := child.values[0 # child.values.size()] 
    212311      newleaf:LeafNode[\Key,Val\] = LeafNode[\Key,Val\](k, values) 
    213       (WhiteNode[\Key,Val\](newleaf), false) 
     312      (WhiteLevel1[\Key,Val\](newleaf), false) 
    214313    else 
    215314      keys:Array[\Key,ZZ32\] = array[\Key\](1) 
    216       children:Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](2) 
     315      children:Array[\LeafNode[\Key,Val\],ZZ32\] = array[\LeafNode[\Key,Val\]\](2) 
    217316      (smaller,larger,lkey) = if k > k' then (child,leaf,k) else (leaf,child,k') end 
    218317      keys[0] := lkey 
    219318      children[0] := smaller 
    220319      children[1] := larger 
    221       (InternalNode[\Key,Val\](keys,children), true) 
    222     end 
    223   end 
    224  
    225   (* perform the add operation when the height is greater than one *) 
    226   heightn_add(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\], Boolean) = do 
    227     (child':Node[\Key,Val\], newKey:Boolean) = child.add_helper(leaf,level) 
    228     if level < height OR newKey = false then 
    229       (WhiteNode[\Key,Val\](child'), newKey) 
    230     else 
    231       (split(0, child'), newKey) 
    232     end 
    233   end 
    234  
    235   (* perform the remove operation when the height is one *) 
    236   height1_remove(k:Key):(Node[\Key,Val\], Maybe[\Val\])  = do 
     320      (InternalLevel1[\Key,Val\](keys,children), true) 
     321    end 
     322  end 
     323 
     324  remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) = do 
    237325    if child.getKey() = k then 
    238326      if child.values.size() = 1 then 
    …… 
    242330        values[0 # values.size()] := child.values[0 # values.size()] 
    243331        newLeaf = LeafNode[\Key,Val\](k, values) 
    244         (WhiteNode[\Key,Val\](newLeaf), Just[\Val\](child.values[values.size()])) 
     332        (WhiteLevel1[\Key,Val\](newLeaf), Just[\Val\](child.values[values.size()])) 
    245333      end 
    246334    else 
    247335      (self, Nothing[\Val\]()) 
    248     end 
    249   end 
    250  
    251   (* perform the remove operation when the height is greater than one *) 
    252   heightn_remove(k:Key):(Node[\Key,Val\], Maybe[\Val\])  = do 
    253     (child':Node[\Key,Val\], maybe:Maybe[\Val\]) = child.remove(k) 
    254     if instanceOf[\EmptyNode[\Key,Val\]\](child') then 
    255       (child', maybe) 
    256     else 
    257       (WhiteNode[\Key,Val\](child'), maybe) 
    258     end 
    259   end 
    260   
    261   (* perform the merge operation when the height is equal to one *) 
    262   height1_merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = do 
     336    end   
     337  end 
     338 
     339  merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] =  
    263340    height1_merge_leaves(nodes.generate[\List[\LeafNode[\Key,Val\]\]\]( 
    264341      Concat[\LeafNode[\Key,Val\]\](), 
    265342      fn (node:Node[\Key,Val\]): List[\LeafNode[\Key,Val\]\] => node.getLeaves())) 
    266   end 
    267343 
    268344  (* helper function for height1_merge where nodes is a list of all leaves *)   
    …… 
    277353  end 
    278354 
    279   (* perform the merge operation when the height is greater than one *)  
    280   heightn_merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = WhiteNode[\Key,Val\](child.merge(nodes)) 
    281  
    282   getLeaves():List[\LeafNode[\Key,Val\]\] = child.getLeaves() 
     355end 
     356 
     357 
     358(* A white node stores exactly zero keys and contains one child. White nodes are 
     359   used as placeholders to keep the height of all branches identical. A white node 
     360   has a height > 0 *) 
     361object WhiteLevelN[\Key,Val\](child:NonLeafNode[\Key,Val\]) extends {WhiteNode[\Key,Val\], WhiteNodeHelper[\Key,Val,NonLeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} 
     362 
     363  getter child():NonLeafNode[\Key,Val\] = child 
     364 
     365  add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\], Boolean) = do 
     366    (child':Node[\Key,Val\], newKey:Boolean) = child.add_helper(leaf,level) 
     367    if level < height() OR newKey = false then 
     368      (WhiteLevelN[\Key,Val\](child'), newKey) 
     369    else 
     370      (split(0, child'), newKey) 
     371    end 
     372  end 
     373 
     374  remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) = do 
     375    (child':Node[\Key,Val\], maybe:Maybe[\Val\]) = child.remove(k) 
     376    if instanceOf[\EmptyNode[\Key,Val\]\](child') then 
     377      (child', maybe) 
     378    else 
     379      (WhiteLevelN[\Key,Val\](child'), maybe) 
     380    end 
     381  end 
     382 
     383  merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = WhiteLevelN[\Key,Val\](child.merge(nodes)) 
     384 
     385  (* splits the new child in half and sucks the split key up to this level *) 
     386  split(index:ZZ32, heir:InternalNode[\Key,Val\]):InternalLevelN[\Key,Val\] = do 
     387    keys:Array[\Key,ZZ32\] = array[\Key\](1) 
     388    children:Array[\NonLeafNode[\Key,Val\],ZZ32\] = array[\NonLeafNode[\Key,Val\]\](2) 
     389    (left,right,key') = heir.break() 
     390    keys[0] := key' 
     391    children[0] := left 
     392    children[1] := right 
     393    InternalLevelN[\Key,Val\](keys,children) 
     394  end 
    283395 
    284396end 
    …… 
    286398(* An internal node stores N keys and N + 1 children where N > 0. 
    287399   An internal nodes has a height > 0. *) 
    288 object InternalNode[\Key,Val\](keys:Array[\Key,ZZ32\], 
    289   children:Array[\Node[\Key,Val\],ZZ32\]) extends Node[\Key,Val\] 
    290  
    291   size:ZZ32 = children.generate[\ZZ32\](SumReduction[\ZZ32\](), 
    292                                         fn (node:Node[\Key,Val\]):ZZ32 => node.getSize()) 
    293                                          
    294   height:ZZ32 = children[0].getHeight() + 1 
    295    
    296   getHeight():ZZ32 = height 
    297   getSize():ZZ32 = size 
    298  
    299   isLeaf():Boolean = false 
    300   isTreeEmpty():Boolean = false 
    301   isNodeEmpty():Boolean = false 
    302  
    303   find_index(k:Key):ZZ32 = do 
    304     index:ZZ32 := 0 
    305     while (index < keys.size() AND: k >= keys[index]) do 
    306       index += 1 
    307     end 
    308     index 
    309   end 
    310  
    311   search(k:Key):Maybe[\Val\] = do 
    312     index:ZZ32 = find_index(k) 
    313     children[index].search(k) 
    314   end 
    315  
    316   toString():String = "{" keys.toString() ", " children.toString() "}" 
    317  
    318   add(leaf:LeafNode[\Key,Val\], level:ZZ32):Node[\Key,Val\] = do 
    319     tail:Node[\Key,Val\] = generate_tail[\Key,Val\](self, level - getHeight()) 
    320     (newNode, newKey) = tail.add_helper(leaf, level) 
    321     newNode 
    322   end 
     400object InternalLevel1[\Key,Val\](keys:Array[\Key,ZZ32\], 
     401  children:Array[\LeafNode[\Key,Val\],ZZ32\]) extends {InternalNode[\Key,Val\],  
     402  InternalNodeHelper[\InternalLevel1[\Key,Val\],Key,Val,LeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} 
     403 
     404  getter keys():Array[\Key,ZZ32\] = keys 
     405  getter children():Array[\LeafNode,ZZ32\] = children 
     406 
     407  singleton(keys':Array[\Key,ZZ32\], children':Array[\LeafNode[\Key,Val\],ZZ32\]) : InternalLevel1[\Key,Val\] = InternalLevel1[\Key,Val\](keys',children') 
    323408 
    324409  add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\],Boolean) = do 
    325410    index:ZZ32 = find_index(leaf.getKey()) 
    326     if height = 1 then 
    327       height1_add(leaf, index) 
    328     else 
    329       heightn_add(leaf, index, level) 
    330     end 
    331   end 
    332  
    333   remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) = do 
    334     index:ZZ32 = find_index(k) 
    335     if height = 1 then 
    336       height1_remove(k,index) 
    337     else 
    338       heightn_remove(k,index) 
    339     end 
    340   end 
    341  
    342   (* splits the new child in half and sucks the split key up to this level *) 
    343   split(index:ZZ32, heir:Node[\Key,Val\]):InternalNode[\Key,Val\] = do 
    344     keysplit:ZZ32 = keys.size() - index 
    345     keys':Array[\Key,ZZ32\] = array[\Key\](keys.size() + 1) 
    346     children':Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](children.size() + 1) 
    347     (left,right,key') = heir.break() 
    348     keys'[0 # index] := keys[0 # index] 
    349     children'[0 # index] := children[0 # index] 
    350     keys'[index] := key' 
    351     children'[index] := left 
    352     children'[index + 1] := right 
    353     keys'[(index + 1) # keysplit] := keys[index # keysplit] 
    354     children'[(index + 2) # keysplit] := children[(index + 1) # keysplit] 
    355     InternalNode[\Key,Val\](keys',children') 
    356   end 
    357  
    358   break():(Node[\Key,Val\],Node[\Key,Val\],Key) = 
    359   if keys.size() = 1 then 
    360     onekey_break() 
    361   elif keys.size() = 2 then 
    362     twokeys_break() 
    363   else 
    364     nkeys_break() 
    365   end 
    366  
    367   merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] =  
    368   if height = 1 then   
    369     height1_merge(nodes) 
    370   else 
    371     heightn_merge(nodes) 
    372   end 
    373  
    374   (* perform the add operation when the height is one *) 
    375   height1_add(leaf:LeafNode[\Key,Val\], index:ZZ32):(Node[\Key,Val\], Boolean) = do 
    376411    if children[index].getKey() = leaf.getKey() then 
    377412      values:Array[\Val,ZZ32\] = array[\Val\](leaf.values.size() + children[index].values.size()) 
    …… 
    379414      values[leaf.values.size() # children[index].values.size()] := children[index].values[0 # children[index].values.size()] 
    380415      newleaf:LeafNode[\Key,Val\] = LeafNode[\Key,Val\](leaf.getKey(), values) 
    381       children':Array[\Node[\Key,Val\],ZZ32\] = children.copy() 
     416      children':Array[\LeafNode[\Key,Val\],ZZ32\] = children.copy() 
    382417      children'[index] := newleaf 
    383       (InternalNode[\Key,Val\](keys,children'), false) 
     418      (InternalLevel1[\Key,Val\](keys,children'), false) 
    384419    else 
    385420      keys':Array[\Key,ZZ32\] = array[\Key\](keys.size() + 1) 
    386       children':Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](children.size() + 1) 
     421      children':Array[\LeafNode[\Key,Val\],ZZ32\] = array[\LeafNode[\Key,Val\]\](children.size() + 1) 
    387422      keysplit:ZZ32 = keys.size() - index 
    388423      (smaller,larger) = if leaf.getKey() > children[index].getKey() then (children[index], leaf) else (leaf, children[index]) end 
    …… 
    394429      keys'[0 # index] := keys[0 # index] 
    395430      keys'[(index + 1) # keysplit] := keys[index # keysplit] 
    396       (InternalNode[\Key,Val\](keys',children'), true) 
    397     end 
    398   end 
    399  
    400   (* perform the add operation when the height is greater than one *) 
    401   heightn_add(leaf:LeafNode[\Key,Val\], index:ZZ32, level:ZZ32):(Node[\Key,Val\], Boolean) = do 
    402     (child':Node[\Key,Val\], newKey:Boolean) = children[index].add_helper(leaf, level) 
    403     if level < height OR newKey = false then 
    404       children':Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](children.size()) 
    405       children'[0 # (children.size())] := children[0 # (children.size())] 
    406       children'[index] := child' 
    407       (InternalNode[\Key,Val\](keys,children'), newKey) 
    408     else 
    409       (split(index, child'), newKey) 
    410     end 
    411   end 
    412  
    413   (* perform the remove operation when the height is one *) 
    414   height1_remove(k:Key, index:ZZ32):(Node[\Key,Val\],Maybe[\Val\]) = do 
     431      (InternalLevel1[\Key,Val\](keys',children'), true) 
     432    end              
     433  end 
     434 
     435  remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) = do 
     436    index:ZZ32 = find_index(k) 
    415437    if children[index].getKey() = k then 
    416438      height1_remove_helper(k, index) 
    …… 
    427449      values'[0 # values'.size()] := values[0 # values'.size()] 
    428450      newleaf:LeafNode[\Key,Val\] = LeafNode[\Key,Val\](k, values') 
    429       children':Array[\Node[\Key,Val\],ZZ32\] = children.copy() 
     451      children':Array[\LeafNode[\Key,Val\],ZZ32\] = children.copy() 
    430452      children'[index] := newleaf 
    431       InternalNode[\Key,Val\](keys,children') 
     453      InternalLevel1[\Key,Val\](keys,children') 
    432454    elif keys.size() = 1 then 
    433       (WhiteNode[\Key,Val\](children[(index + 1) MOD 2]), Just[\Val\](val)) 
     455      (WhiteLevel1[\Key,Val\](children[(index + 1) MOD 2]), Just[\Val\](val)) 
    434456    else 
    435457      (index_remove(index), Just[\Val\](val)) 
    …… 
    437459  end 
    438460 
    439   (* perform the remove operation when the height is greater than one *) 
    440   heightn_remove(k:Key, index:ZZ32):(Node[\Key,Val\],Maybe[\Val\]) = do 
    441     (child':Node[\Key,Val\], maybe:Maybe[\Val\]) = children[index].remove(k) 
    442     if keys.size() = 1 then 
    443       (heightn_remove_1key(index,child'), maybe) 
    444     else 
    445       (heightn_remove_nkeys(index,child'), maybe) 
    446     end 
    447   end 
    448  
    449   (* perform the remove operation when height > 1 and keys = 1 *) 
    450   heightn_remove_1key(index:ZZ32, child':Node[\Key,Val\]):Node[\Key,Val\] = do 
    451     other:ZZ32 = (index + 1) MOD 2 
    452     if instanceOf[\EmptyNode[\Key,Val\]\](child') then 
    453       WhiteNode[\Key,Val\](children[other]) 
    454     else 
    455       keys':Array[\Key,ZZ32\] = array[\Key\](1) 
    456       children':Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](2) 
    457       keys'[0] := keys[0] 
    458       children'[index] := child' 
    459       children'[other] := children[other] 
    460       InternalNode[\Key,Val\](keys', children') 
    461     end 
    462   end 
    463  
    464   (* perform the remove operation when height > 1 and keys > 1 *) 
    465   heightn_remove_nkeys(index:ZZ32, child':Node[\Key,Val\]):Node[\Key,Val\] = do 
    466     if instanceOf[\EmptyNode[\Key,Val\]\](child') then 
    467       index_remove(index) 
    468     else 
    469       keys':Array[\Key,ZZ32\] = array[\Key\](keys.size()) 
    470       children':Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](children.size()) 
    471       keys'[0 # keys.size()] := keys[0 # keys.size()] 
    472       children'[0 # children.size()] := children[0 # children.size()] 
    473       children'[index] := child' 
    474       InternalNode[\Key,Val\](keys', children') 
    475     end 
    476   end 
    477  
    478   (* return a new internal node that has children[index] and keys[index - 1] missing *) 
    479   index_remove(index:ZZ32):Node[\Key,Val\] = do 
    480     keys':Array[\Key,ZZ32\] = array[\Key\](keys.size() - 1) 
    481     children':Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](children.size() - 1) 
    482     replace:ZZ32 = MAX(0, index - 1) 
    483     keys'[0 # replace] := keys[0 # replace] 
    484     keys'[replace # (keys'.size() - replace)] := keys[(replace + 1) # (keys'.size() - replace)] 
    485     children'[0 # index] := children[0 # index] 
    486     children'[index # (children'.size() - index)] := children[(index + 1) # (children'.size() - index)] 
    487     InternalNode[\Key,Val\](keys', children') 
    488   end 
    489  
    490   (* perform the break operation when we have exactly one key *) 
    491   onekey_break():(Node[\Key,Val\],Node[\Key,Val\],Key) = do 
    492     smaller:Node[\Key,Val\] = children[0] 
    493     larger:Node[\Key,Val\] = children[1] 
    494     key':Key = keys[0] 
    495     left:Node[\Key,Val\] = generate_tail[\Key,Val\](smaller, 1) 
    496     right:Node[\Key,Val\] = generate_tail[\Key,Val\](larger, 1) 
    497     (left, right, key') 
    498   end 
    499  
    500   (* perform the break operation when we have exactly two keys *) 
    501   twokeys_break():(Node[\Key,Val\],Node[\Key,Val\],Key) = do 
    502     smaller:Node[\Key,Val\] = children[0] 
    503     rkeys:Array[\Key,ZZ32\] = array[\Key\](1) 
    504     rchildren:Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](2) 
    505     key':Key = keys[0] 
    506     rkeys[0] := keys[1] 
    507     rchildren[0#2] := children[1#2] 
    508     left:Node[\Key,Val\] = generate_tail[\Key,Val\](smaller, 1) 
    509     right:Node[\Key,Val\] = InternalNode[\Key,Val\](rkeys,rchildren) 
    510     (left, right, key') 
    511   end 
    512  
    513   (* perform the break operation when we have three or more keys *) 
    514   nkeys_break():(Node[\Key,Val\],Node[\Key,Val\],Key) = do 
    515     half:ZZ32 = keys.size() DIV 2 
    516     rsize:ZZ32 = keys.size() - half - 1 
    517     lsize:ZZ32 = keys.size() - rsize - 1 
    518     key':Key = keys[half] 
    519     lkeys:Array[\Key,ZZ32\] = array[\Key\](lsize) 
    520     lchildren:Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](lsize + 1) 
    521     rkeys:Array[\Key,ZZ32\] = array[\Key\](rsize) 
    522     rchildren:Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](rsize + 1) 
    523     lkeys[0 # lsize] := keys[0 # lsize] 
    524     lchildren[0 # (lsize + 1)] := children[0 # (lsize + 1)] 
    525     rkeys[0 # rsize] := keys[(half + 1) # rsize] 
    526     rchildren[0 # (rsize + 1)] := children[(half + 1) # (rsize + 1)] 
    527     left:Node[\Key,Val\] = InternalNode[\Key,Val\](lkeys,lchildren) 
    528     right:Node[\Key,Val\] = InternalNode[\Key,Val\](rkeys,rchildren) 
    529     (left, right, key') 
    530   end 
    531  
    532   (* perform the merge operation when the height is equal to one *) 
    533   height1_merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = do 
     461  merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] =  
    534462    height1_merge_leaves(nodes.generate[\List[\LeafNode[\Key,Val\]\]\]( 
    535463      Concat[\LeafNode[\Key,Val\]\](), 
    536464      fn (node:Node[\Key,Val\]): List[\LeafNode[\Key,Val\]\] => node.getLeaves())) 
    537   end 
    538465 
    539466  (* helper function for height1_merge where nodes is a list of all leaves *)   
    …… 
    548475  end 
    549476 
     477 
     478end 
     479 
     480(* An internal node stores N keys and N + 1 children where N > 0. 
     481   An internal nodes has a height > 0. *) 
     482object InternalLevelN[\Key,Val\](keys:Array[\Key,ZZ32\], 
     483  children:Array[\NonLeafNode[\Key,Val\],ZZ32\]) extends {InternalNode[\Key,Val\], InternalNodeHelper[\InternalLevelN[\Key,Val\],Key,Val,NonLeafNode[\Key,Val\]\], NonLeafNode[\Key,Val\]} 
     484 
     485  getter keys():Array[\Key,ZZ32\] = keys 
     486  getter children():Array[\NonLeafNode[\Key,Val\],ZZ32\] = children 
     487 
     488  singleton(keys':Array[\Key,ZZ32\], children':Array[\NonLeafNode[\Key,Val\],ZZ32\]) : InternalLevelN[\Key,Val\] = InternalLevelN[\Key,Val\](keys',children') 
     489 
     490  add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\],Boolean) = do 
     491    index:ZZ32 = find_index(leaf.getKey()) 
     492    (child':Node[\Key,Val\], newKey:Boolean) = children[index].add_helper(leaf, level) 
     493    if level < height() OR newKey = false then 
     494      children':Array[\NonLeafNode[\Key,Val\],ZZ32\] = array[\NonLeafNode[\Key,Val\]\](children.size()) 
     495      children'[0 # (children.size())] := children[0 # (children.size())] 
     496      children'[index] := child' 
     497      (InternalLevelN[\Key,Val\](keys,children'), newKey) 
     498    else 
     499      (split(index, child'), newKey) 
     500    end 
     501  end 
     502 
     503  remove(k:Key):(Node[\Key,Val\],Maybe[\Val\]) = do 
     504    index:ZZ32 = find_index(k) 
     505    (child':Node[\Key,Val\], maybe:Maybe[\Val\]) = children[index].remove(k) 
     506    if keys.size() = 1 then 
     507      (heightn_remove_1key(index,child'), maybe) 
     508    else 
     509      (heightn_remove_nkeys(index,child'), maybe) 
     510    end 
     511  end 
     512 
     513  (* splits the new child in half and sucks the split key up to this level *) 
     514  split(index:ZZ32, heir:InternalNode[\Key,Val\]):InternalLevelN[\Key,Val\] = do 
     515    keysplit:ZZ32 = keys.size() - index 
     516    keys':Array[\Key,ZZ32\] = array[\Key\](keys.size() + 1) 
     517    children':Array[\NonLeafNode[\Key,Val\],ZZ32\] = array[\NonLeafNode[\Key,Val\]\](children.size() + 1) 
     518    (left,right,key') = heir.break() 
     519    keys'[0 # index] := keys[0 # index] 
     520    children'[0 # index] := children[0 # index] 
     521    keys'[index] := key' 
     522    children'[index] := left 
     523    children'[index + 1] := right 
     524    keys'[(index + 1) # keysplit] := keys[index # keysplit] 
     525    children'[(index + 2) # keysplit] := children[(index + 1) # keysplit] 
     526    InternalLevelN[\Key,Val\](keys',children') 
     527  end 
     528 
     529  merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = heightn_merge(nodes) 
     530 
     531  (* perform the remove operation when height > 1 and keys = 1 *) 
     532  heightn_remove_1key(index:ZZ32, child':Node[\Key,Val\]):Node[\Key,Val\] = do 
     533    other:ZZ32 = (index + 1) MOD 2 
     534    if instanceOf[\EmptyNode[\Key,Val\]\](child') then 
     535      WhiteLevelN[\Key,Val\](children[other]) 
     536    else 
     537      keys':Array[\Key,ZZ32\] = array[\Key\](1) 
     538      children':Array[\NonLeafNode[\Key,Val\],ZZ32\] = array[\NonLeafNode[\Key,Val\]\](2) 
     539      keys'[0] := keys[0] 
     540      children'[index] := child' 
     541      children'[other] := children[other] 
     542      InternalLevelN[\Key,Val\](keys', children') 
     543    end 
     544  end 
     545 
     546  (* perform the remove operation when height > 1 and keys > 1 *) 
     547  heightn_remove_nkeys(index:ZZ32, child':Node[\Key,Val\]):Node[\Key,Val\] = do 
     548    if instanceOf[\EmptyNode[\Key,Val\]\](child') then 
     549      index_remove(index) 
     550    else 
     551      keys':Array[\Key,ZZ32\] = array[\Key\](keys.size()) 
     552      children':Array[\NonLeafNode[\Key,Val\],ZZ32\] = array[\NonLeafNode[\Key,Val\]\](children.size()) 
     553      keys'[0 # keys.size()] := keys[0 # keys.size()] 
     554      children'[0 # children.size()] := children[0 # children.size()] 
     555      children'[index] := child' 
     556      InternalLevelN[\Key,Val\](keys', children') 
     557    end 
     558  end 
     559 
    550560  (* perform the merge operation when the height is greater than one *) 
    551561  heightn_merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = do 
    …… 
    557567    end 
    558568    keys':Array[\Key,ZZ32\] = keys.copy() 
    559     children':Array[\Node[\Key,Val\],ZZ32\] = array[\Node[\Key,Val\]\](children.size()) 
     569    children':Array[\NonLeafNode[\Key,Val\],ZZ32\] = array[\NonLeafNode[\Key,Val\]\](children.size()) 
    560570    for index <- 0 # children.size() do 
    561571      if destinations[index].isEmpty() then 
    …… 
    565575      end 
    566576    end 
    567     InternalNode[\Key,Val\](keys',children') 
     577    InternalLevelN[\Key,Val\](keys',children') 
    568578  end 
    569579 
    …… 
    586596  (* helper function for heightn_merge on WhiteNodes *) 
    587597  merge_destination_insert(node:WhiteNode[\Key,Val\], destinations:Array[\List[\Node[\Key,Val\]\],ZZ32\]):() = do 
    588     merge_destination_insert(node.child, destinations)     
     598    merge_destination_insert(node.child, destinations)   
    589599  end 
    590600   
    …… 
    651661  end 
    652662 
    653   getLeaves():List[\LeafNode[\Key,Val\]\] = children.generate[\List[\LeafNode[\Key,Val\]\]\]( 
    654     Concat[\LeafNode[\Key,Val\]\](), 
    655     fn (node:Node[\Key,Val\]): List[\LeafNode[\Key,Val\]\] => node.getLeaves()) 
    656  
    657663end 
    658664 
    …… 
    661667object EmptyNode[\Key,Val\]() extends Node[\Key,Val\] 
    662668 
    663   getHeight():ZZ32 = fail("Cannot get height of an empty tree") 
    664   getSize():ZZ32 = 0 
    665  
    666   isLeaf():Boolean = fail("Empty node is neither a leaf nor an internal node") 
    667   isTreeEmpty():Boolean = true 
    668   isNodeEmpty():Boolean = fail("Empty node cannot check for emptiness on keys") 
    669  
     669  getter height():ZZ32 = fail("Cannot get height of an empty tree") 
     670  getter size():ZZ32 = 0 
     671   
    670672  search(k:Key):Maybe[\Val\] = Nothing[\Val\]() 
    671673 
    …… 
    680682 
    681683  add_helper(leaf:LeafNode[\Key,Val\], level:ZZ32):(Node[\Key,Val\], Boolean) = do 
    682     parent:WhiteNode[\Key,Val\] = WhiteNode[\Key,Val\](leaf) 
     684    parent:WhiteLevel1[\Key,Val\] = WhiteLevel1[\Key,Val\](leaf) 
    683685    (parent, true) 
    684686  end 
    685  
    686   split(index:ZZ32, heir:Node[\Key,Val\]):InternalNode[\Key,Val\] = fail("Cannot split an empty node.") 
    687   break():(Node[\Key,Val\],Node[\Key,Val\],Key) = fail("Cannot break an empty node.") 
    688687 
    689688  merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = nodes[0] 
    …… 
    699698  getKey():Key = key 
    700699  getValues():Array[\Val,ZZ32\] = values 
    701   getHeight():ZZ32 = 0 
    702   getSize():ZZ32 = values.size()   
    703  
    704   isLeaf():Boolean = true 
    705   isTreeEmpty():Boolean = false 
    706   isNodeEmpty():Boolean = false 
     700  height():ZZ32 = 0 
     701  size():ZZ32 = values.size() 
    707702 
    708703  search(k:Key):Maybe[\Val\] = if k = key then Just[\Val\](values[0]) else Nothing[\Val\]() end 
    …… 
    712707  remove(k:Key):Node[\Key,Val\] = fail("Cannot remove a key from a leaf node.") 
    713708 
    714   split(index:ZZ32, heir:Node[\Key,Val\]):InternalNode[\Key,Val\] = fail("Cannot split a leaf node.") 
    715   break():(Node[\Key,Val\],Node[\Key,Val\],Key) = fail("Cannot break a leaf node.") 
    716  
    717709  merge(nodes:List[\Node[\Key,Val\]\]):Node[\Key,Val\] = fail("Cannot merge into a leaf node.") 
    718710 

  • trunk/ProjectFortress/tests/SkipListTest.fss

    r1011 r1023  
    2626add(database:SkipList[\String,ZZ32,2\], name:String, ranking: ZZ32) = database.add(name, ranking) 
    2727 
    28 remove(database:SkipList[\String,ZZ32,2\], name:String) = database := database.remove(name) 
     28remove(database:SkipList[\String,ZZ32,2\], name:String) = database.remove(name) 
    2929 
    3030run(args:String...):() = do 
    …… 
    3838 
    3939  println(database1.toString()) 
    40   println(database1.getSize()) 
     40  println(database1.size()) 
    4141     
    4242  database2 := add(database2, "Michael", 0) 
    …… 
    4848   
    4949  println(database2.toString()) 
    50   println(database2.getSize()) 
     50  println(database2.size()) 
    5151 
    5252  println(database1.merge(database2).toString()) 
    …… 
    5454  println(database1.toString()) 
    5555 
    56   (* 
    57   remove("Emily") 
    58   println(database.toString()) 
    59   remove("David") 
    60   println(database.toString()) 
    61   remove("Nathi") 
    62   println(database.toString()) 
    63   remove("Michael") 
    64   println(database.toString()) 
    65   remove("Jacob") 
    66   println(database.toString()) 
    67   remove("Aaron") 
    68   println(database.toStrin