Lines Matching refs:priority
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,