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