Metis/src/KeyMap.sml

43 type priority = Word.word;
60        priority : priority,
68       val Node {priority = p1, ...} = node1
69       and Node {priority = p2, ...} = node2
126                 else raise Bug "left child has greater priority"
133                 else raise Bug "right child has greater priority"
165 fun mkNode priority left key value right =
171          priority = priority,
178 fun mkTree priority left key value right =
180       val node = mkNode priority left key value right
217 fun mkNodeSingleton priority key value =
225          priority = priority,
234       val priority = randomPriority ()
236       mkNodeSingleton priority key value
260             val Node {priority,left,key,value,right,...} = node2
264             mkTree priority left key value right
268             val Node {priority,left,key,value,right,...} = node1
272             mkTree priority left key value right
332       val Node {priority,left,key,value,right,...} = node
334       if wentLeft then (leftTree, mkTree priority rightTree key value right)
335       else (mkTree priority left key value leftTree, rightTree)
347         val Node {priority,left,key,value,right,...} = node
349         if wentLeft then mkTree priority tree key value right
350         else mkTree priority left key value tree
452           val Node {size,priority,left,right,...} = node
457                  priority = priority,
479       val Node {size,priority,left,key,value,right} = node
490                  priority = priority,
507                  priority = priority,
527 and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
535       | SOME value => mkTree priority left key value right
549       val Node {size,priority,left,key,value,right} = node
557          priority = priority,
579       val Node {priority,left,key,value,right,...} = node2
595           val node = mkNodeSingleton priority key value
617         val Node {priority,left,key,value,right,...} = node2
633             val node = mkNodeSingleton priority key value
653       val Node {priority,left,key,value,right,...} = n2
667       | SOME value => mkTree priority left key value right
686       val Node {priority,left,key,value,right,...} = node2
693       val node = mkNodeSingleton priority key value
714       val Node {priority,left,key,value,right,...} = node2
721       if Option.isSome kvo then mkTree priority left key value right
741         val Node {priority,left,key,value,right,...} = n1
749         else mkTree priority left key value right
842       val Node {size,priority,left,key,value,right} = node
856                  priority = priority,
875                  priority = priority,