equal
deleted
inserted
replaced
63 |
63 |
64 val weight_ord = prod_ord int_ord int_ord |
64 val weight_ord = prod_ord int_ord int_ord |
65 |
65 |
66 fun weight_of vals t = fst (value_of vals t) |
66 fun weight_of vals t = fst (value_of vals t) |
67 |
67 |
68 fun less_than vals t1 t2 = weight_ord (weight_of vals t1, weight_of vals t2) = LESS |
68 fun less_than vals t1 t2 = is_less (weight_ord (weight_of vals t1, weight_of vals t2)) |
69 |
69 |
70 fun rescale activity = activity div activity_rescale |
70 fun rescale activity = activity div activity_rescale |
71 |
71 |
72 fun incr_activity incr t = map_value t (apfst (apfst (Integer.add incr))) |
72 fun incr_activity incr t = map_value t (apfst (apfst (Integer.add incr))) |
73 fun incr_count t = map_value t (apfst (apsnd (Integer.add 1))) |
73 fun incr_count t = map_value t (apfst (apsnd (Integer.add 1))) |
161 If the changed weight violates the heap property, the corresponding tree |
161 If the changed weight violates the heap property, the corresponding tree |
162 is extracted and merged with the root. |
162 is extracted and merged with the root. |
163 *) |
163 *) |
164 |
164 |
165 fun fix t (w, Some parent) (incr, vals) tree = |
165 fun fix t (w, Some parent) (incr, vals) tree = |
166 if weight_ord (weight_of vals parent, w) = LESS then |
166 if is_less (weight_ord (weight_of vals parent, w)) then |
167 let val (tree1, tree2) = cut t (path_to vals parent []) tree |
167 let val (tree1, tree2) = cut t (path_to vals parent []) tree |
168 in mk_heap' incr (merge tree1 tree2 (root t vals)) end |
168 in mk_heap' incr (merge tree1 tree2 (root t vals)) end |
169 else mk_heap incr vals tree |
169 else mk_heap incr vals tree |
170 | fix _ _ (incr, vals) tree = mk_heap incr vals tree |
170 | fix _ _ (incr, vals) tree = mk_heap incr vals tree |
171 |
171 |