Metis/src/Map.sml

35 type priority = Word.word;
52        priority : priority,
60       val Node {priority = p1, ...} = node1
61       and Node {priority = p2, ...} = node2
118                 else raise Bug "left child has greater priority"
125                 else raise Bug "right child has greater priority"
157 fun mkNode priority left key value right =
163          priority = priority,
170 fun mkTree priority left key value right =
172       val node = mkNode priority left key value right
209 fun mkNodeSingleton priority key value =
217          priority = priority,
226       val priority = randomPriority ()
228       mkNodeSingleton priority key value
252             val Node {priority,left,key,value,right,...} = node2
256             mkTree priority left key value right
260             val Node {priority,left,key,value,right,...} = node1
264             mkTree priority left key value right
324       val Node {priority,left,key,value,right,...} = node
326       if wentLeft then (leftTree, mkTree priority rightTree key value right)
327       else (mkTree priority left key value leftTree, rightTree)
339         val Node {priority,left,key,value,right,...} = node
341         if wentLeft then mkTree priority tree key value right
342         else mkTree priority left key value tree
444           val Node {size,priority,left,right,...} = node
449                  priority = priority,
471       val Node {size,priority,left,key,value,right} = node
482                  priority = priority,
499                  priority = priority,
519 and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
527       | SOME value => mkTree priority left key value right
541       val Node {size,priority,left,key,value,right} = node
549          priority = priority,
571       val Node {priority,left,key,value,right,...} = node2
587           val node = mkNodeSingleton priority key value
609         val Node {priority,left,key,value,right,...} = node2
625             val node = mkNodeSingleton priority key value
645       val Node {priority,left,key,value,right,...} = n2
659       | SOME value => mkTree priority left key value right
678       val Node {priority,left,key,value,right,...} = node2
685       val node = mkNodeSingleton priority key value
706       val Node {priority,left,key,value,right,...} = node2
713       if Option.isSome kvo then mkTree priority left key value right
733         val Node {priority,left,key,value,right,...} = n1
741         else mkTree priority left key value right
834       val Node {size,priority,left,key,value,right} = node
848                  priority = priority,
867                  priority = priority,