12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388138913901391139213931394139513961397139813991400140114021403140414051406140714081409141014111412141314141415141614171418141914201421142214231424142514261427142814291430143114321433143414351436143714381439144014411442144314441445144614471448144914501451(******************************************************************************)(* *)(* Sek *)(* *)(* Arthur Charguéraud, Émilie Guermeur and François Pottier *)(* *)(* Copyright Inria. All rights reserved. This file is distributed under the *)(* terms of the GNU Lesser General Public License as published by the Free *)(* Software Foundation, either version 3 of the License, or (at your *)(* option) any later version, as described in the file LICENSE. *)(* *)(******************************************************************************)(* This module constructs an implementation of ephemeral sequences, based on
an implementation [SSeq] of shareable sequences. *)(* One could define an ephemeral sequence directly as a uniquely-owned
shareable sequence, and thereby, write almost no code in this module.
However, we prefer to write specialized code for the outermost level of
this data structure, at depth 0. Indeed, this allows us to save a possibly
large constant factor in time and memory:
* Here, [front] and [back] are raw chunks, not shareable chunks.
* No measure [m] is required; the weight of an element is 1.
* No case distinction between [Empty] and [Level] is required.
Furthermore, we introduce a mechanism which (for simplicity) does not exist
in shareable sequences, namely a free list where we keep a number of empty
chunks, ready to be re-used. This is important because initializing a newly
allocated array is costly. *)openPublicSettingsopenPrivateSignaturesmodule[@inline]Make(SChunk:SCHUNK)(C:CAPACITY)(SSeq:SSEQwithtype'aschunk='aSChunk.tandtype'ameasure='aSChunk.measure)=structmoduleEChunk=SChunk.EChunkmoduleSegment=EChunk.Segmenttype'achunk='aEChunk.ttype'aschunk='aSChunk.ttype'ameasure='aSChunk.measure=|MeasureUnit:'ameasure|MeasureSchunkWeight:'aschunkmeasure(* -------------------------------------------------------------------------- *)(* Depth zero. *)letdepth0=0(* Only the capacity at depth zero is of interest to us here. *)letcapacity=C.capacitydepth0(* -------------------------------------------------------------------------- *)(* The structure of an ephemeral sequence is analogous to the structure of a
level in a shareable sequence; see the comments there. Here, we also have a
front chunk, a middle sequence, and a back chunk. The front and back chunks
are just chunks, not shareable chunks; we own them. The middle sequence is
a shareable sequence of shareable chunks. The [owner] field contains the
identity that we must use when accessing [middle]; this identity is
distinct from [Owner.none].
In addition, a sequence features "inner front" and "inner back" chunks,
These chunks are either empty chunks, full chunks, or dummy chunks. The
order of elements is: [front], [ifront], [middle], [iback], [back]. The
motivation for maintaining these inner chunks is to avoid allocations and
operations on the middle sequence in worst-case scenarios, such as pushing
[capacity] items (thereby filling the front chunk), then pushing one item,
popping one item, pushing again, popping again, and so on. The use of dummy
inner chunks allows reducing the cost of initialization.
In addition to the empty chunks that may be stored in the inner fields, the
structure keeps a bounded number of empty chunks in a free list, stored in
the field [free]. This reduces pressure on the GC and saves the cost of
initializing a newly-allocated chunk. This seems especially useful when a
sequence is used as a FIFO queue.
In order to avoid the cost of allocating a new dummy chunk and a new empty
middle sequence during some operations, such as [clear] and [carve], we
keep an empty middle sequence at hand in the field [empty]. This empty
middle sequence is immutable and can be shared among several instances of
the data structure. From this empty middle sequence, we can recover a dummy
chunk, which is also immutable. (An alternative approach would be to store
a dummy chunk in another record field.)
An important invariant is the "populated-sides invariant", which asserts
that if the front or back chunk is empty, then so are the middle sequence
and the inner chunks. *)(* Some operations on ephemeral sequences destroy their argument. In order to
avoid exposing the concept of an invalidated data structure, we
reinitialize them to an empty sequence. In order to avoid the cost of
reinitialization when possible, we perform lazy reinitialization. We adopt
the convention that an empty sequence is allowed to have *dummy* front and
back chunks, instead of *empty* front and back chunks. Such a sequence must
be reinitialized before use. We refer to such a sequence as a fubar
sequence. It is technically a valid sequence (e.g., [check] succeeds), but
has special status. *)type'at={mutableowner:owner;mutablefront:'achunk;mutableifront:'achunk;mutablemiddle:'aschunkSSeq.t;mutableiback:'achunk;mutableback:'achunk;mutablefree:'afree_list;empty:'aschunkSSeq.t;}(* The free list is a list of empty chunks. Every [Cons] constructor carries
the length of the list. *)and'afree_list=|Nil|Consofint*'achunk*'afree_list(* -------------------------------------------------------------------------- *)(* Basic accessors. *)let[@inline]is_fubars=EChunk.is_dummys.frontlet[@inline]defaults=(* A subtle point is that [default s] continues to work, and must continue
to work, even if [s] is fubar. Indeed, it is called by [reinit]. *)EChunk.defaults.frontletlengths=(* A fubar sequence looks very much like an empty sequence; the only
difference is that the front and back chunks are dummy chunks. Because a
dummy chunk has length 0, we do not need to make a special case for fubar
sequences; the general case works. *)EChunk.lengths.front+EChunk.lengths.ifront+SSeq.weights.middle+EChunk.lengths.iback+EChunk.lengths.backletis_emptys=(* A fubar sequence has dummy front and back chunks. *)EChunk.is_empty_or_dummys.front&&EChunk.is_empty_or_dummys.back(* The populated-sides invariant guarantees that if the front or back
chunk is empty, then so are the middle sequence and the inner chunks. *)(* By construction, the default element of every middle sequence is a dummy
schunk, out of which we can recover a dummy chunk. This is a bit contrived,
but works. *)let[@inline]dummy_(s:'aschunkSSeq.t):'achunk=letp=SSeq.defaultsinassert(SChunk.is_dummyp);SChunk.supportplet[@inline]dummys=(* Here, we can use either [s.middle] or [s.empty]. *)dummy_s.empty(* -------------------------------------------------------------------------- *)(* Allocation and disposal of chunks, via the free list. *)letallocates=assert(not(is_fubars));matchs.freewith|Cons(_,c,tail)->s.free<-tail;EChunk.checkc;assert(EChunk.is_emptyc);c|Nil->EChunk.create(defaults)capacityletmax_length_of_free_list=0letfree_list_lengthfree=matchfreewith|Nil->0|Cons(n,_,_)->nletdisposesc=assert(not(is_fubars));ifnot(EChunk.is_dummyc)thenbegin(* If the current length of the free list is less than its maximum permitted
length, insert this chunk into the free list; otherwise drop it. *)letn=free_list_lengths.freeinifn<max_length_of_free_listthens.free<-Cons(n+1,c,s.free)endletrecfree_list_concatfree1free2=matchfree1with|Nil->free2|Cons(_,c1,free1)->letn=free_list_lengthfree2in(* If the current length of the free list is less than its maximum
permitted length, insert this chunk into the free list; otherwise
stop concatenating. *)ifn<max_length_of_free_listthenfree_list_concatfree1(Cons(n+1,c1,free2))elsefree2(* -------------------------------------------------------------------------- *)(* Validity. *)(* An inner chunk must be either a dummy chunk or a valid chunk, which must
be either empty or full. *)letcheck_innerc=ifnot(EChunk.is_dummyc)thenbeginEChunk.checkc;assert(EChunk.is_emptyc||EChunk.is_fullc)endletreccheck_free_listfree=matchfreewith|Nil->()|Cons(n,c,free)->assert(n=free_list_lengthfree+1);EChunk.checkc;(* This implies [c] is not a dummy chunk. *)assert(EChunk.is_emptyc);check_free_listfreeletchecks=ifis_fubarsthenbegin(* [s.owner] is unconstrained. *)assert(EChunk.is_dummys.front);assert(EChunk.is_dummys.ifront);assert(SSeq.is_emptys.middle);assert(EChunk.is_dummys.back);assert(EChunk.is_dummys.iback);assert(s.free==Nil)endelsebegin(* Check the populated-sides invariant. *)ifEChunk.is_emptys.front||EChunk.is_emptys.backthenbeginassert(SSeq.is_emptys.middle);assert(EChunk.is_empty_or_dummys.ifront);assert(EChunk.is_empty_or_dummys.iback);end;(* Check that the front and back chunks are well-formed. *)EChunk.checks.front;EChunk.checks.back;(* Check that the inner chunks are well-formed. *)check_inners.ifront;check_inners.iback;(* Check that the middle sequence is well-formed. *)SSeq.check_middles.middleMeasureUnits.ownerdepth0;(* Check the free list. *)check_free_lists.free;(* Check the empty sequence. *)assert(SSeq.is_emptys.empty);(* Check that our mechanism for obtaining a dummy chunk works. *)ignore(dummys)end(* Ensure [check] has zero cost in release mode. *)let[@inline]checks=assert(checks;true)(* -------------------------------------------------------------------------- *)(* Getters and setters, parameterized by a point of view. *)(* We use the words [this] and [that] to refer to this side -- the one
closest to us, from our point of view -- and that side -- the other
side. *)(* We use the words [inner] and [other] to refer to the inner chunk on
this side and the other side. *)let[@inline]get_thispovs=matchpovwith|Front->s.front|Back->s.backlet[@inline]set_thispovsthis=matchpovwith|Front->s.front<-this|Back->s.back<-thislet[@inline]get_innerpovs=matchpovwith|Front->s.ifront|Back->s.ibacklet[@inline]set_innerpovsc=matchpovwith|Front->s.ifront<-c|Back->s.iback<-clet[@inline]inner_is_fullc=assert(EChunk.is_empty_or_dummyc||EChunk.is_fullc);not(EChunk.is_empty_or_dummyc)(* We cannot just use [EChunk.is_full c] here, as we wish to return
[false] when [c] is a dummy chunk. *)let[@inline]get_bothpovs=matchpovwith|Front->s.front,s.back|Back->s.back,s.frontlet[@inline]set_bothpovsthisthat=matchpovwith|Front->s.front<-this;s.back<-that|Back->s.front<-that;s.back<-this(* -------------------------------------------------------------------------- *)(* Construction. *)(* [create_empty_middle default] creates an empty middle sequence. *)let[@inline]create_empty_middledefault=SSeq.create_middledefaultdepth0(* [seq owner front middle back] is a basic constructor. It takes care of
initializing the free list (to an empty list) and the inner chunks (to
dummy chunks). The caller must supply an existing empty middle sequence, so
there is no need to allocate a new one. *)letseqownerfrontmiddlebackempty=letdummy=dummy_emptyinletifront=dummyandiback=dummyandfree=Nilin{owner;front;ifront;middle;iback;back;free;empty}(* [seq_of_chunk c o empty] creates a new sequence with owner [o] out of the
chunk [c]. The caller must supply an existing [empty] middle sequence. *)(* [c] becomes the front chunk, but could just as well be the back chunk. *)letseq_of_chunkcoempty=letdefault=EChunk.defaultcinletowner=oandfront=candmiddle=emptyandback=EChunk.createdefaultcapacityinseqownerfrontmiddlebackemptyletcreatedefault=letc=EChunk.createdefaultcapacityinletempty=create_empty_middledefaultinseq_of_chunkcOwner.zeroempty(* -------------------------------------------------------------------------- *)(** [push_into_middle pov s c] pushes the chunk [c] into the middle sequence
of the sequence [s], on the side determined by [pov]. *)let[@inline]push_into_middlepovsc=letp=SChunk.of_chunk_destructivecs.ownerins.middle<-SSeq.pushpovs.middlepMeasureSchunkWeights.owner(* [inner_chunks_are_empty s] returns [true] if both inner chunks are empty.
This includes the case where they are dummy chunks. *)let[@inline]inner_chunks_are_emptys=EChunk.is_empty_or_dummys.ifront&&EChunk.is_empty_or_dummys.iback(* [flush_inner_chunks] flushes both inner chunks into the middle sequence.
If an inner chunk is nonempty, it is pushed into the middle sequence and
replaced with a dummy chunk. Thus, [flush_inner_chunks] guarantees that
both inner chunks are empty or dummy. *)let[@inline]flush_inner_chunkpovs=letinner=get_innerpovsinifinner_is_fullinnerthenbeginpush_into_middlepovsinner;set_innerpovs(dummys);end;assert(EChunk.is_empty_or_dummy(get_innerpovs))let[@inline]flush_inner_chunkss=flush_inner_chunkFronts;flush_inner_chunkBacks(* -------------------------------------------------------------------------- *)(* [fubar s] makes the sequence [s] fubar. This sequence then logically
represents an empty sequence, but its front and back chunks are not
reinitialized until it is actually used. *)(* One may be tempted to perform fewer writes here and let [reinit]
perform more work, thus relaxing the invariant on fubar sequences.
Unfortunately, allowing garbage to remain stored in the fields can
cause memory leaks. *)letfubars=letdummy=dummysins.front<-dummy;s.ifront<-dummy;s.iback<-dummy;s.back<-dummy;s.middle<-s.empty;s.free<-Nil(* [clear s] is equivalent to [assign s (create (default s))]. *)(* There are two reasonable ways of implementing [clear]:
- Keep and clear the front and back chunks. If [overwrite_empty_slots] is
[false], this can be significantly faster than allocating fresh chunks.
- Replace the front and back chunks with dummy chunks, making [s] fubar.
The front and back chunks are then lost.
The first approach seems preferable if the sequence [s] is used again in
the future, whereas the second approach seems preferable if [s] is never
used again.
Similarly, there is a question whether the free list should be kept or
emptied. For now, we empty it, but could keep it.
One may imagine that if the user does not intend to use [s] in the future,
then she should just let [s] become unreachable, without bothering to call
[clear]. So, it seems reasonable to assume that the user does intend to use
[s] again. For this reason, we choose the first approach. *)(* If [s] is fubar, we do nothing. It already represents an empty sequence. *)letclears=ifnot(is_fubars)thenbegins.owner<-Owner.zero;EChunk.clears.front;s.middle<-s.empty;letdummy=dummysins.ifront<-dummy;s.iback<-dummy;EChunk.clears.back;s.free<-Nilend(* [reinit s] is analogous to [clear s], but allocates new front and back
chunks. This is useful when parts of [s] (such as the front and back chunks
and the inner chunks) have been stolen, which means that [s] is not a valid
sequence. *)letreinits=assert(is_fubars);s.owner<-Owner.zero;letdefault=defaultsins.front<-EChunk.createdefaultcapacity;s.back<-EChunk.createdefaultcapacity(* [lazy_reinit s] tests whether the sequence [s] has been fubar'ed,
and if so, reinitializes it to an empty sequence. This test must be
applied to every argument of every public operation. *)let[@inline]lazy_reinits=ifis_fubarsthenreinits(* -------------------------------------------------------------------------- *)(* [copy s] creates a copy of the sequence [s]. The front and back chunk are
copied. For efficiency reasons, the middle sequence is not copied: it is
shared. For this reason, both [s] and [s'] must be given a new owner
identity, which is strictly above the current identity. This causes the
middle sequence to be regarded as shared. *)letcopys=lazy_reinits;flush_inner_chunkss;letowner=Owner.aboves.ownerins.owner<-owner;letfront=EChunk.copys.frontandback=EChunk.copys.backinseqownerfronts.middlebacks.empty(* -------------------------------------------------------------------------- *)(* Conversion of an ephemeral sequence to a shareable sequence. *)letsnapshot_and_clears:'aSSeq.t*owner=(* The case where [s] is fubar or empty can be treated quickly
and easily. We save time and memory by not going through the
general case, and we lose nothing, as testing whether [s] is
fubar is mandatory anyway. *)(* This discussion is kind of moot anyway, as [snapshot_and_clear]
should never be applied to a short sequence anyway; see the
wrapper function [snapshot_and_clear] in module [Sek]. *)leto=s.ownerinifis_emptysthenSSeq.create(defaults)depth0,oelsebeginassert(not(is_fubars));flush_inner_chunkss;letfront=SChunk.of_chunk_destructives.frontoandmiddle=s.middleandback=SChunk.of_chunk_destructives.backoandweight=lengthsin(* Fubar [s], as we are stealing its data. *)fubars;(* Build a new shareable sequence. Return a pair of this sequence
and the identity with which it must be accessed. *)SSeq.nonempty_levelFrontweightfrontmiddlebackdepth0,oend(* -------------------------------------------------------------------------- *)(* Conversion of shareable data (front, middle, back) to ephemeral sequence. *)letedit(s,owners)=(* This may be the only place where we exploit the fact that ['a SSeq.t]
is a private type, that is, a semi-abstract type. This allows us to
get read access to its fields without any overhead. *)matchswith|SSeq.Zero{default;_}->createdefault|SSeq.Level{front;middle;back;_}->(* The [owners] field is an upper bound on the creator of every schunk
in the shareable sequence [s]. We select an owner identity that lies
strictly above [owners]. As a result, the newly-created ephemeral
sequence does *not* uniquely own any of the schunks. *)letowner=Owner.aboveownersinletfront=SChunk.to_chunkfrontownerandback=SChunk.to_chunkbackownerinletdefault=EChunk.defaultfrontinletempty=create_empty_middledefaultinseqownerfrontmiddlebackempty(* -------------------------------------------------------------------------- *)(* If [s1] and [s2] are distinct, then [assign s1 s2] copies of all [s2]'s
fields into [s1] and clears [s2]. [assign s s] does nothing. *)letassigns1s2=ifs1!=s2thenbegins1.owner<-s2.owner;s1.ifront<-s2.ifront;s1.front<-s2.front;s1.middle<-s2.middle;s1.back<-s2.back;s1.iback<-s2.iback;s1.free<-s2.free;fubars2end(* [move_out_of s] returns a fresh sequence, a copy of [s], and
fubars [s]. *)letmove_out_ofs=lets'={owner=s.owner;front=s.front;ifront=s.ifront;middle=s.middle;iback=s.iback;back=s.back;free=s.free;empty=s.empty}infubars;s'(* [swap s1 s2] copies of all [s2]'s fields into [s1] and vice-versa. *)(* [swap] accepts fubar sequences. *)letswaps1s2=letowner1,front1,ifront1,middle1,iback1,back1,free1=s1.owner,s1.front,s1.ifront,s1.middle,s1.iback,s1.back,s1.freeins1.owner<-s2.owner;s1.front<-s2.front;s1.ifront<-s2.ifront;s1.middle<-s2.middle;s1.back<-s2.back;s1.iback<-s2.iback;s1.free<-s2.free;s2.owner<-owner1;s2.front<-front1;s2.ifront<-ifront1;s2.middle<-middle1;s2.iback<-iback1;s2.back<-back1;s2.free<-free1(* -------------------------------------------------------------------------- *)(* Restoring the populated-sides invariant. *)let[@inline]populatepovs=letthis=get_thispovsinifEChunk.is_emptythisthenbeginletinner=get_innerpovsinifinner_is_fullinnerthenbegin(* The front chunk is empty, and the inner chunk is full. Swap them. *)set_thispovsinner;set_innerpovsthis;endelseifnot(SSeq.is_emptys.middle)thenbegin(* The front chunk is empty and the inner front chunk is empty (or dummy),
yet the middle sequence is nonempty. *)(* Dispose of the front chunk, either by moving it to the free list or by
storing it into the inner front field. (Both are permitted, but storing
in the field [inner], if possible, is more efficient, as it does not
require allocating a free list cell. *)ifEChunk.is_dummyinnerthenset_innerpovsthiselsedisposesthis;(* Replace the front chunk with a chunk that is popped off the middle
sequence. *)letthis,middle=SSeq.poppovs.middleMeasureSchunkWeights.ownerins.middle<-middle;set_thispovs(SChunk.to_chunkthiss.owner)endelsebegin(* The front chunk is empty and the inner front chunk is empty (or dummy),
and the middle sequence is empty as well. *)(* If the inner chunk on the opposite side is full, swap it with the
front chunk. *)letother=get_inner(dualpov)sinifinner_is_fullotherthenbeginset_thispovsother;set_inner(dualpov)sthis;endendend;(* At this point, if the front chunk is still empty, then this implies
that the inner front chunk, middle sequence, and inner back chunk
are empty as well. *)assert(not(EChunk.is_emptys.front)||EChunk.is_empty_or_dummys.ifront&&SSeq.is_emptys.middle&&EChunk.is_empty_or_dummys.iback)let[@inline]populate_boths=populateFronts;populateBacks;(* At this point, the populated-sides invariant must hold. *)checks(* -------------------------------------------------------------------------- *)(* Peek. *)let[@specialise]peekpovs=ifis_emptysthenraiseEmptyelsebeginlazy_reinits;letthis,that=get_bothpovsinifnot(EChunk.is_emptythis)thenEChunk.peekpovthiselsebeginassert(inner_chunks_are_emptys);assert(SSeq.is_emptys.middle);EChunk.peekpovthatendend(* -------------------------------------------------------------------------- *)(* Push. *)let[@specialise]pushpovsx=lazy_reinits;letthis,that=get_bothpovsin(* If the front chunk is full, take action so as to come back to
a situation where it is not full. *)ifEChunk.is_fullthisthenbeginifEChunk.is_emptythatthenbeginassert(SSeq.is_emptys.middle);assert(inner_chunks_are_emptys);(* The full front chunk moves to the back.
The empty back chunk moves to the front. *)set_bothpovsthatthisendelsebeginletinner=get_innerpovsin(* It the inner front chunk is full, take action to empty it. *)ifinner_is_fullinnerthenbegin(* Push the front chunk into the middle sequence. *)push_into_middlepovsinner;(* Allocate a new empty inner chunk. *)set_innerpovs(allocates)end;letinner=get_innerpovsinassert(EChunk.is_empty_or_dummyinner);(* Set the [front] field to an empty chunk, and let the former front
chunk [this] become the inner front chunk. *)set_thispovs(ifEChunk.is_dummyinnerthenallocateselseinner);set_innerpovsthisend;end;(* The front chunk is not full. Push [x] into it. *)letthis=get_thispovsinassert(not(EChunk.is_fullthis));EChunk.pushpovthisx(* -------------------------------------------------------------------------- *)(* Pop. *)let[@specialise]poppovs=lazy_reinits;letthis,that=get_bothpovsinifEChunk.is_emptythisthenbeginassert(SSeq.is_emptys.middle);assert(inner_chunks_are_emptys);(* The front chunk and middle sequence are empty: pop an element
off the back chunk. *)ifEChunk.is_emptythatthenraiseEmptyelseEChunk.poppovthatendelsebegin(* The front chunk is nonempty: pop an element off it. *)letx=EChunk.poppovthisin(* Restore the populated-sides invariant, if necessary. *)populatepovs;xend(* -------------------------------------------------------------------------- *)(* Iteration. *)let[@specialise]iterpovgs=lazy_reinits;letthis,that=get_bothpovsinEChunk.iterpovgthis;letinner,other=get_innerpovs,get_inner(dualpov)sinEChunk.iterpovginner;SSeq.iterpov(funp->SChunk.iterpovgp)s.middle;EChunk.iterpovgother;EChunk.iterpovgthatletto_lists=Adapters.to_list(iterBack)sletiter_rangessf=assert(not(is_fubars));EChunk.iter_rangess.frontf;EChunk.iter_rangess.ifrontf;SSeq.iterFront(funs->SChunk.iter_rangessf)s.middle;EChunk.iter_rangess.ibackf;EChunk.iter_rangess.backfletto_arrays=lazy_reinits;ArrayExtra.concat_segments(defaults)(lengths)(iter_rangess)(* -------------------------------------------------------------------------- *)(* Printing. *)letprintelements=letopenPPrintinletopenPPrint.OCamlinletechunk=EChunk.printelementinletschunk=SChunk.printelementinifis_fubarsthen!^"<fubar>"elserecord"seq"["owner",!^(Owner.shows.owner);"front",echunks.front;"ifront",echunks.ifront;"middle",SSeq.printschunks.middle;"iback",echunks.iback;"back",echunks.back;"model",flowing_listelement(to_lists);]letformatelementchannels=PPrint.ToFormatter.pretty0.876channel(printelements)letformatchannel(s:intt)=formatPPrint.OCaml.intchannels(* -------------------------------------------------------------------------- *)(* Constructors for sequences of a known size [size]. *)(* See the comments in [ShareableSequence]. *)letcreate_by_segmentsdefaultsizecreate_chunk=ifsize=0thencreatedefaultelsebeginletn=capacityinleto=Owner.zeroinlet[@inline]create_chunk(i,k)=create_chunknikinletfront,foreach_middle_segment,back=ArrayExtra.cutnnsizeinletfront=create_chunkfrontinletempty=create_empty_middledefaultinletmiddle=refemptyinforeach_middle_segment(funik->letschunk=SChunk.of_chunk_destructive(create_chunk(i,k))oinmiddle:=SSeq.pushBack!middleschunkMeasureSchunkWeighto);letmiddle=!middleinletback=create_chunkbackin(* The empty middle sequence that was created above is re-used here. *)seqofrontmiddlebackemptyendletof_array_segmentdefaultaheadsize=assert(ArrayExtra.is_valid_segmentaheadsize);create_by_segmentsdefaultsize(funnik->EChunk.of_array_segmentdefaultna(head+i)k)letmakedefaultsizev=assert(0<=size);create_by_segmentsdefaultsize(funn_ik->EChunk.makedefaultnkv)letinitdefaultsizef=assert(0<=size);create_by_segmentsdefaultsize(funnik->EChunk.initdefaultnkif)(* -------------------------------------------------------------------------- *)(* Concatenation. *)(* [concat_nonempty t1 t2 s1 s2] performs the parallel assignment
[t1, t2 := s1 ++ s2, empty]. The sequences [s1] and [s2] must be
nonempty, therefore cannot be fubar. *)letconcat_nonemptyt1t2s1s2=assert(not(is_emptys1));assert(not(is_emptys2));assert(not(is_fubars1));assert(not(is_fubars2));(* For simplicity, ensure that all four inner chunks are empty (or dummy). *)flush_inner_chunkss1;flush_inner_chunkss2;(* We won't be needing these empty inner chunks, but don't want them to be
wasted, so we return them to the free list, which will be saved below. *)disposes1s1.ifront;disposes1s1.iback;disposes1s2.ifront;disposes1s2.iback;(* Exchange the front and back chunks of [s1], if necessary, to ensure
that its front chunk is nonempty. *)ifEChunk.is_emptys1.frontthenbeginassert(SSeq.is_emptys1.middle);letback1=s1.backins1.back<-s1.front;s1.front<-back1end;assert(not(EChunk.is_emptys1.front));(* Similarly, ensure that the back chunk of [s2] is nonempty. *)ifEChunk.is_emptys2.backthenbeginassert(SSeq.is_emptys2.middle);letfront2=s2.frontins2.front<-s2.back;s2.back<-front2end;assert(not(EChunk.is_emptys2.back));(* Compute a new owner identity for the concatenated sequence. Because
we inherit schunks from [s1] and [s2], we must use an identity that
is at least as high as [s1.owner] and [s2.owner]. *)leto=Owner.joins1.owners2.ownerint1.owner<-o;(* Get rid of [s1.back] and [s2.front] by pushing them into [middle1]. *)letmiddle1,middle2=s1.middle,s2.middleinletmiddle1=SSeq.fuse_backmiddle1(SChunk.of_chunk_destructives1.backo)oinletmiddle1=SSeq.fuse_backmiddle1(SChunk.of_chunk_destructives2.fronto)oin(* There remains to concatenate the two middles, *)t1.middle<-SSeq.fusemiddle1middle2o;(* and build a new sequence out of [s1.front], [s1.middle], [s2.back]. *)t1.front<-s1.front;t1.back<-s2.back;letdummy=dummys1int1.ifront<-dummy;t1.iback<-dummy;populate_botht1;(* We can give all of the free list blocks to [t1]. Any blocks that we
give to [t2] would be destroyed by [reinit] below. *)t1.free<-free_list_concats2.frees1.free;(* Fubar [t2], so it will be reinitialized to an empty sequence
if and when it is used again. *)fubart2(* [concat s1 s2] returns a new sequence and fubars [s1] and [s2].
It is less efficient than [append_back] and [append_front], but its
specification is simpler. *)letconcats1s2=assert(s1!=s2);ifis_emptys1thenmove_out_ofs2elseifis_emptys2thenmove_out_ofs1elsebegin(* Create an empty sequence [t]. *)lett=create(defaults1)in(* Compute the concatenation in [t] and clear [s2]. *)concat_nonemptyts2s1s2;(* Clear [s1]. *)fubars1;tend(* [append Back s1 s2] performs the parallel assignment
[s1, s2 := s1 ++ s2, empty]. *)(* It is therefore equivalent to [assign s1 (concat s1 s2)]. *)(* [append Front s1 s2] performs the parallel assignment
[s1, s2 := s2 ++ s1, empty]. *)(* It is therefore equivalent to [assign s1 (concat s2 s1)]. *)(* This code works even if [s1] or [s2] is fubar. *)let[@specialise]appendpovs1s2=assert(s1!=s2);ifis_emptys1thenswaps1s2elseifis_emptys2then()elsematchpovwith|Front->concat_nonemptys1s2s2s1|Back->concat_nonemptys1s2s1s2(* -------------------------------------------------------------------------- *)(* Split. *)(* [carve_back s i] performs the parallel assignment
[s, result := take i s, drop i s]. *)(* It is therefore equivalent to
[let s1, s2 = split s i in assign s s1; s2]. *)letcarve_back_nonemptysi=(* [s] is nonempty, therefore is not fubar. Thus, no call to
[lazy_reinit] is required. *)assert(not(is_emptys));assert(not(is_fubars));(* For simplicity, ensure that all the inner chunks are empty (or dummy).
We won't touch them at all, so they remain associated with [s]. *)flush_inner_chunkss;letlength_front=EChunk.lengths.frontinifi<=length_frontthenbegin(* The line falls in the front chunk. Split it. *)letfront2=EChunk.carve_backs.frontiin(* Build a fresh sequence out of [front2], [middle], [back]. *)lets2=seqs.ownerfront2s.middles.backs.emptyinpopulateFronts2;(* Deprive [s] of its middle and back. *)s.middle<-s.empty;s.back<-EChunk.create(defaults)capacity;s2endelseleti=i-length_frontinletweight_middle=SSeq.weights.middleinifweight_middle<=ithenbeginleti=i-weight_middlein(* The line falls in the back chunk. Split it. *)letback2=EChunk.carve_backs.backiin(* Build a fresh sequence out of just [back2]. *)lets2=seq_of_chunkback2s.owners.emptyin(* Restore the populated-sides invariant in [s],
which can be broken if [i] is [weight_middle]. *)populateBacks;s2endelsebegin(* The line falls strictly in the middle. *)assert(weight_middle>0);assert(not(SSeq.is_emptys.middle));assert(0<i&&i<weight_middle);(* Split the middle sequence. *)letmiddle1,p,middle2=SSeq.three_way_splits.middleiMeasureSchunkWeights.ownerin(* We now know that the line falls in the schunk [p]. *)leti=i-SSeq.weightmiddle1inassert(0<=i&&i<SChunk.weightp);(* Downgrade this schunk to a chunk [c]. *)letc=SChunk.to_chunkps.ownerin(* Split this chunk. *)letc2=EChunk.carve_backciin(* Build a fresh sequence out of [c2], [middle2], [back]. *)lets2=seqs.ownerc2middle2s.backs.emptyinpopulateFronts2;(* In the sequence [s], keep only [front], [middle1], [c]. *)s.middle<-middle1;s.back<-c;populateBacks;s2endletcarve_backsi=assert(0<=i&&i<=lengths);ifi=lengthsthencreate(defaults)else(* If [s] is empty, then [i] must be zero, so [i = length s] must hold.
This case has already been taken care of above. Therefore, [s] is
nonempty. *)carve_back_nonemptysi(* [carve_front s i] performs the parallel assignment
[s, result := drop i s, take i s]. *)(* It is therefore equivalent to
[let s1, s2 = split s i in assign s s2; s1]. *)letcarve_frontsi=assert(0<=i&&i<=lengths);ifi=0thencreate(defaults)elsebegin(* Extract [s2], the last part of [s]. *)lets2=carve_back_nonemptysiin(* Steal what remains in [s] to initialize a fresh sequence [s1]. *)lets1=seqs.owners.fronts.middles.backs.emptyin(* At this point, [s] is invalid. Restore it by assigning [s := s2].
There is no need to copy the [owner] and [free] fields, as [s] has
retained them through the call to [carve_back] above. *)s.front<-s2.front;s.middle<-s2.middle;s.back<-s2.back;s1endlet[@specialise]carvepovsi=matchpovwith|Front->carve_frontsi|Back->carve_backsi(* [split s i] returns the pair [take s i, drop s i] and clears [s]. *)letsplitsi=assert(0<=i&&i<=lengths);lets2=carve_backsiinlets1=move_out_ofsins1,s2(* -------------------------------------------------------------------------- *)(* Get. *)letgetsi=assert(0<=i&&i<lengths);(* No need to call [lazy_reinit s], as [s] is nonempty. *)flush_inner_chunkss;letweight_front=EChunk.lengths.frontinifi<weight_frontthen(* The desired element lies in the front chunk. *)EChunk.gets.frontielseleti=i-weight_frontinletweight_middle=SSeq.weights.middleinifweight_middle<=ithenleti=i-weight_middlein(* The desired element lies in the back chunk. *)EChunk.gets.backielse(* The desired element lies in the middle. *)leti,p=SSeq.gets.middleiMeasureSchunkWeightinSChunk.getpi(* -------------------------------------------------------------------------- *)(* Set. *)letsetsix=assert(0<=i&&i<lengths);(* No need to call [lazy_reinit s], as [s] is nonempty. *)flush_inner_chunkss;leto=s.ownerinletweight_front=EChunk.lengths.frontinifi<weight_frontthen(* The desired element lies in the front chunk. *)EChunk.sets.frontixelseleti=i-weight_frontinletweight_middle=SSeq.weights.middleinifweight_middle<=ithenleti=i-weight_middlein(* The desired element lies in the back chunk. *)EChunk.sets.backixelse(* The desired element lies in the middle sequence. *)letf_xi=assert(i=0);xins.middle<-SSeq.updateMeasureSchunkWeighto(SChunk.update_by_weightMeasureUnitof)s.middlei(* -------------------------------------------------------------------------- *)moduleIter=structmoduleMIter=SSeq.Itertype'aiter={seq:'at;(* sequence being iterated *)mutablepath:'apath;(* iterator pointing at the schunk that contains the current item *)mutablesegtype:segtype;(* which contiguous fragment contains the current item *)mutablesupport:'aarray;(* direct pointer to the array that contains the items *)mutablesupport_uniquely_owned:bool;(* whether support is uniquely owned *)mutablehead:int;(* first index to consider in the current segment *)mutabletail:int;(* last index to consider in the current segment *)mutableindex:int;(* index of current item in the current segment *)mutablenb_items_before_segment:int;(* nb items in the sequence before the current segment *)}and'apath=|PathFront(* iterator in the front chunk *)|PathMiddleof'aSChunk.tMIter.iter(* iterator in a schunk from middle *)|PathBack(* iterator in the back chunk *)andsegtype=|SegUnknown|SegUnique|SegFront|SegBackletsequenceit=it.seq(* returns the absolute index of the current item in the sequence *)letindexit=it.nb_items_before_segment+it.index-it.headletcurrent_segment_lengthit=it.tail-it.head+1letgetit=it.support.(it.index)letcurrent_schunkit=matchit.pathwith|PathFront->SChunk.of_chunk_destructiveit.seq.frontit.seq.owner|PathMiddleit_middle->MIter.getit_middle|PathBack->SChunk.of_chunk_destructiveit.seq.backit.seq.owner(* TODO BUG? calling [of_chunk_destructive] does not seem OK! *)typereach=ReachFront|ReachBack|ReachIndexofint(* [reach_in_current_schunk] takes as argument a [segtype], indicating
whether one should reach the first or second consecutive segment,
or if it unconstrained (use [SegUnknown] for that); and takes as
argument a [reach] which indicates whether targetting the front
or back side of the segment, or a particular index.
This function sets the fields: segtype, support, head, tail, index *)letreach_in_current_schunkitsegtypereach=letp=current_schunkitinit.support<-SChunk.datap;it.support_uniquely_owned<-SChunk.is_uniquely_ownedpit.seq.owner;letauxsegsegtypenb_before=letsize=Segment.sizeseginassert(size>0);lethead=Segment.headseginlettail=head+size-1inletindex=(matchreachwith|ReachFront->head|ReachBack->tail|ReachIndexi->head+(i-nb_before))inassert(0<=head&&head<SChunk.capacityp);assert(0<=tail&&tail<SChunk.capacityp);assert(head<=index&&index<=tail);it.segtype<-segtype;it.head<-head;it.tail<-tail;it.index<-index;inmatchSChunk.contiguous_segmentspwith|[seg]->auxsegSegUnique0|[segf;segb]->beginmatchsegtypewith|SegUnique->assertfalse(* illegal argument *)|SegFront->auxsegfSegFront0|SegBack->auxsegbSegBack0|SegUnknown->beginmatchreachwith|ReachIndexi->assert(0<=i&&i<SChunk.lengthp);letnbf=Segment.sizesegfinifi<nbfthenauxsegfSegFront0elseauxsegbSegBacknbf|(ReachFront|ReachBack)->assertfalse(* illegal argument *)endend|_->assertfalse(* can be only one or two contiguous segments in a chunk *)letreach_index_in_current_schunkiti=reach_in_current_schunkitSegUnknown(ReachIndexi)letcreate_commons=lazy_reinits;(* TODO if we treat the empty sequence specially, then we do not need this *)flush_inner_chunkss;{seq=s;(* dummy fields: *)path=PathFront;segtype=SegUnknown;support=EChunk.datas.front;support_uniquely_owned=true;head=0;tail=0;index=0;nb_items_before_segment=0;}letreach_frontit=it.path<-(if(not(EChunk.is_emptyit.seq.front))thenPathFrontelsePathBack);(* using populated sides invariant to know that middle is empty if front is *)reach_in_current_schunkitSegFrontReachFront;it.nb_items_before_segment<-0letcreate_at_fronts=letit=create_commonsinreach_frontit;itletreach_backit=it.path<-(if(not(EChunk.is_emptyit.seq.back))thenPathBackelsePathFront);(* using populated sides invariant to know that middle is empty if front is *)reach_in_current_schunkitSegBackReachBack;it.nb_items_before_segment<-lengthit.seq-(current_segment_lengthit)letcreate_at_backs=letit=create_commonsinreach_backit;it(* returns a triple [Some (array, head, tail)] describing next segment
reached by the iterator; or [None] if it was the last segment. *)letnext_segmentit=letnb_cur=current_segment_lengthitinletreturn()=it.nb_items_before_segment<-it.nb_items_before_segment+nb_cur;Some(it.support,it.head,it.tail)inifit.segtype=SegFrontthenbeginreach_in_current_schunkitSegBackReachFront;return()endelsebeginletreach_front_and_return()=reach_in_current_schunkitSegFrontReachFront;return()inletnext_in_back()=(* factorizes two cases *)ifnot(EChunk.is_emptyit.seq.back)thenbeginit.path<-PathBack;reach_front_and_return()endelseNoneinmatchit.pathwith|PathFront->ifnot(SSeq.is_emptyit.seq.middle)thenbeginletit_middle=MIter.createFrontit.seq.middleMeasureSchunkWeightinlet_p=MIter.moveFrontit_middleMeasureSchunkWeightin(* the move above succeeds because the middle sequence is nonempty *)(* TODO: alternative is to call "create_at 0" *)it.path<-PathMiddleit_middle;reach_front_and_return()endelsenext_in_back()|PathMiddleit_middle->beginmatchMIter.move_optFrontit_middleMeasureSchunkWeightwith|Some_p->reach_front_and_return()|None->next_in_back()end|PathBack->Noneend(* returns [Some item] or [None] *)letnextit=ifit.index<it.tailthenbeginit.index<-it.index+1;Some(getit)endelsebeginmatchnext_segmentitwith|None->None|Some_->Some(getit)end(* returns [item] or [Not_found] *)letnext_exnit=ifit.index<it.tailthenit.index<-it.index+1elseignore(next_segmentit);getit(* returns a triple [Some (array, head, tail)] describing prev segment
reached by the iterator; or [None] if it was the last segment. *)letprev_segmentit=letreturn()=letnb_cur=current_segment_lengthitinit.nb_items_before_segment<-it.nb_items_before_segment-nb_cur;Some(it.support,it.head,it.tail)inifit.segtype=SegBackthenbeginreach_in_current_schunkitSegFrontReachBack;return()endelsebeginletreach_back_and_return()=reach_in_current_schunkitSegBackReachBack;return()inletprev_in_front()=(* factorizes two cases *)ifnot(EChunk.is_emptyit.seq.front)thenbeginit.path<-PathFront;reach_back_and_return()endelseNoneinmatchit.pathwith|PathFront->None|PathMiddleit_middle->beginmatchMIter.move_optBackit_middleMeasureSchunkWeightwith|Some_p->reach_back_and_return()|None->prev_in_front()end|PathBack->ifnot(SSeq.is_emptyit.seq.middle)thenbeginletit_middle=MIter.createBackit.seq.middleMeasureSchunkWeightinlet_p=MIter.moveBackit_middleMeasureSchunkWeightinit.path<-PathMiddleit_middle;reach_back_and_return()endelseprev_in_front()end(* returns [Some item] or [None] *)letprevit=ifit.index>it.headthenbeginit.index<-it.index-1;Some(getit)endelsebeginmatchprev_segmentitwith|None->None|Some_->Some(getit)end(* returns [item] or [Not_found] *)letprev_exnit=ifit.index>it.headthenit.index<-it.index-1elseignore(prev_segmentit);getit(* shifts the iterator to a given position; returns nothing;
may safely be called after abitrary modification to the sequence. *)letreach_positi=lets=it.seqinifnot(0<=i&&i<=lengths)theninvalid_arg"reach_pos: invalid index";(* TODO: ultimately, move [invalid_arg] into Sek and use an assertion here *)ifi<EChunk.lengths.frontthenbegin(* element is in front *)it.path<-PathFront;reach_index_in_current_schunkiti;endelsebeginletib=i-EChunk.lengths.front-SSeq.weights.middleinifib>=0thenbegin(* element is in back *)it.path<-PathBack;reach_index_in_current_schunkitib;endelsebegin(* element is in middle *)assert(not(SSeq.is_emptys.middle));letim=i-EChunk.lengths.frontinletit_middle=MIter.create_ats.middleimMeasureSchunkWeightinit.path<-PathMiddleit_middle;letip=im-MIter.windexit_middleinreach_index_in_current_schunkitip;endendletfreshen_supportit=matchit.pathwith|PathFront|PathBack->()|PathMiddle_->lets=it.seqinletv=s.ownerinletp=current_schunkitinifnot(SChunk.is_uniquely_ownedpv)thenbeginletp2=SChunk.copypvin(* Note: beware that [it.index] is not the index in the middle
sequence, but is a weight that corresponds to the weight of
the subsequence that reaches the chunk that contains the
element focused by the iterator. *)s.middle<-SSeq.sets.middleit.indexMeasureSchunkWeightvp2endletensure_support_uniquely_ownedit=leti=indexitinfreshen_supportit;reach_positiletsetitx=ifnotit.support_uniquely_ownedthenensure_support_uniquely_ownedit;it.support.(it.index)<-xletcreate_atsi=letit=create_commonsinreach_positi;itend(* Iter *)end(* Make *)