123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287(**************************************************************************)(* *)(* OCaml *)(* *)(* Jean-Christophe Filliâtre *)(* *)(* Copyright 2023 CNRS *)(* *)(* All rights reserved. This file is distributed under the terms of *)(* the GNU Lesser General Public License version 2.1, with the *)(* special exception on linking described in the file LICENSE. *)(* *)(**************************************************************************)(* Priority queues over ordered elements.
We choose to have polymorphic elements here, so that we can later
derive both polymorphic and monomorphic priority queues from it.
*)moduletypeOrderedPolyType=sigtype'atvalcompare:'at->'bt->intendmoduleMakeMinPoly(E:OrderedPolyType)=structtype'aelt='aE.t(* Our priority queues are implemented using the standard "min heap"
data structure, a dynamic array representing a binary tree. *)type'at='aE.tDynarray.tletcreate=Dynarray.createletlength=Dynarray.lengthletis_empty=Dynarray.is_emptyletclear=Dynarray.clear(* The node at index [i] has children nodes at indices [2 * i + 1]
and [2 * i + 2] -- if they are valid indices in the dynarray. *)letleft_childi=2*i+1letright_childi=2*i+2letparent_nodei=(i-1)/2(* We say that a heap respects the "heap ordering" if the value of
each node is no greater than the value of its children. The
algorithm manipulates arrays that respect the heap ordering,
except for one node whose value may be too small or too large.
The auxiliary functions [sift_up] and [sift_down] take
such a misplaced value, and move it "up" (respectively: "down")
until the heap ordering is restored.
Functions [sift_up] and [sift_down] do not perform swaps, but
rather expect the value to be assigned in the heap as an
additional parameter [x], resulting in twice less assignments. *)(* store [x] at index [i], moving it up if necessary *)letrecsift_uphix=ifi=0thenDynarray.seth0xelseletp=parent_nodeiinlety=Dynarray.gethpinifE.comparexy<0then(Dynarray.sethiy;sift_uphpx)elseDynarray.sethixletaddhx=leti=Dynarray.lengthhinDynarray.add_lasthx;ifi>0thensift_uphixletadd_iterhiterx=iter(addh)xletmin_elth=ifDynarray.is_emptyhthenNoneelseSome(Dynarray.geth0)letget_min_elth=ifDynarray.is_emptyhtheninvalid_arg"empty priority queue";Dynarray.geth0letlthij=E.compare(Dynarray.gethi)(Dynarray.gethj)<0(* store [x] at index [i], moving it down if necessary *)letrecsift_downh~lenix=letleft=left_childiinifleft>=lenthenDynarray.sethix(* no child, stop *)elseletsmallest=letright=right_childiinifright>=lenthenleft(* no right child *)elseiflthleftrightthenleftelserightinlety=Dynarray.gethsmallestinifE.compareyx<0then(Dynarray.sethiy;sift_downh~lensmallestx)elseDynarray.sethixletpop_minh=letn=Dynarray.lengthhinifn=0thenNoneelseletx=Dynarray.pop_lasthinifn=1thenSomexelse(letr=Dynarray.geth0insift_downh~len:(n-1)0x;Somer)letremove_minh=letn=Dynarray.lengthhinifn>0then(letx=Dynarray.pop_lasthinifn>1thensift_downh~len:(n-1)0x)letcopy=Dynarray.copy(* array to heap in linear time (Floyd, 1964)
many elements travel a short distance, few travel longer distances
and we can show that it totals to O(N) *)letheapifyh=letn=Dynarray.lengthhinfori=n/2-1downto0dosift_downh~len:ni(Dynarray.gethi)done;hletof_arraya=Dynarray.of_arraya|>heapifyletof_listl=Dynarray.of_listl|>heapifyletof_iteriterx=leta=Dynarray.create()initer(Dynarray.add_lasta)x;heapifyaletiter_unordered=Dynarray.iterletfold_unordered=Dynarray.fold_leftendmoduletypeMinPoly=sigtype'attype'aeltvalcreate:unit->'atvallength:'at->intvalis_empty:'at->boolvaladd:'at->'aelt->unitvaladd_iter:'at->(('aelt->unit)->'x->unit)->'x->unitvalmin_elt:'at->'aeltoptionvalget_min_elt:'at->'aeltvalpop_min:'at->'aeltoptionvalremove_min:'at->unitvalclear:'at->unitvalcopy:'at->'atvalof_array:'aeltarray->'atvalof_list:'aeltlist->'atvalof_iter:(('aelt->unit)->'x->unit)->'x->'atvaliter_unordered:('aelt->unit)->'at->unitvalfold_unordered:('acc->'aelt->'acc)->'acc->'at->'accendmoduletypeMaxPoly=sigtype'attype'aeltvalcreate:unit->'atvallength:'at->intvalis_empty:'at->boolvaladd:'at->'aelt->unitvaladd_iter:'at->(('aelt->unit)->'x->unit)->'x->unitvalmax_elt:'at->'aeltoptionvalget_max_elt:'at->'aeltvalpop_max:'at->'aeltoptionvalremove_max:'at->unitvalclear:'at->unitvalcopy:'at->'atvalof_array:'aeltarray->'atvalof_list:'aeltlist->'atvalof_iter:(('aelt->unit)->'x->unit)->'x->'atvaliter_unordered:('aelt->unit)->'at->unitvalfold_unordered:('acc->'aelt->'acc)->'acc->'at->'accendmoduleMakeMaxPoly(E:OrderedPolyType):MaxPolywithtype'aelt='aE.t=structincludeMakeMinPoly(structtype'at='aE.tletcomparexy=E.compareyxend)(* renaming a few functions... *)letmax_elt=min_eltletget_max_elt=get_min_eltletpop_max=pop_minletremove_max=remove_minend(* Monomorphic priority queues *)moduletypeOrderedType=sigtypetvalcompare:t->t->intendmoduletypeMin=sigtypettypeeltvalcreate:unit->tvallength:t->intvalis_empty:t->boolvaladd:t->elt->unitvaladd_iter:t->((elt->unit)->'x->unit)->'x->unitvalmin_elt:t->eltoptionvalget_min_elt:t->eltvalpop_min:t->eltoptionvalremove_min:t->unitvalclear:t->unitvalcopy:t->tvalof_array:eltarray->tvalof_list:eltlist->tvalof_iter:((elt->unit)->'x->unit)->'x->tvaliter_unordered:(elt->unit)->t->unitvalfold_unordered:('acc->elt->'acc)->'acc->t->'accendmoduleMakeMin(E:OrderedType)=structincludeMakeMinPoly(structtype'at=E.tletcompare=E.compareend)typet=E.tDynarray.tendmoduletypeMax=sigtypettypeeltvalcreate:unit->tvallength:t->intvalis_empty:t->boolvaladd:t->elt->unitvaladd_iter:t->((elt->unit)->'x->unit)->'x->unitvalmax_elt:t->eltoptionvalget_max_elt:t->eltvalpop_max:t->eltoptionvalremove_max:t->unitvalclear:t->unitvalcopy:t->tvalof_array:eltarray->tvalof_list:eltlist->tvalof_iter:((elt->unit)->'x->unit)->'x->tvaliter_unordered:(elt->unit)->t->unitvalfold_unordered:('acc->elt->'acc)->'acc->t->'accendmoduleMakeMax(E:OrderedType)=structincludeMakeMinPoly(structtype'at=E.tletcomparexy=E.compareyxend)typet=E.tDynarray.tletmax_elt=min_eltletget_max_elt=get_min_eltletpop_max=pop_minletremove_max=remove_minend