Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file EphemeralChunk.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757(******************************************************************************)(* *)(* 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. *)(* *)(******************************************************************************)openPublicSettingsopenPrivateSignatures(* -------------------------------------------------------------------------- *)(* A circular view of a chunk is represented as a pair of a [head] index
and a [size]. *)(* We have [head < max_capacity] and [size <= max_capacity]. We know that
[max_capacity] is less than [2^bits], so both [head] and [size] fit in
[bits] bits. Provided [bits] is small enough, we can pack [2 * bits]
bits of information in a single OCaml integer value. This allows us to
avoid allocating a pair. *)letmin_capacity=2letmax_capacity=32767letbits=15let()=assert(max_capacity<1lslbits)let()=assert(2*bits<=Sys.word_size-1)typeview=int(* view_head : high [bits] bits *)(* view_size : low [bits] bits *)let[@inline]viewheadsize=assert(0<=head&&head<max_capacity);assert(0<=size&&size<=max_capacity);(headlslbits)lorsizelet[@inline]unchecked_view_headv=vlsrbitslet[@inline]view_headv=lethead=unchecked_view_headvinassert(0<=head&&head<max_capacity);headlet[@inline]unchecked_view_sizev=vland(1lslbits-1)let[@inline]view_sizev=letsize=unchecked_view_sizevinassert(0<=size&&size<=max_capacity);size(* [view_update_size v size] is equivalent to [view (view_head v) size].
This formulation saves two shifts. *)let[@inline]view_update_sizevsize=assert(0<=size&&size<=max_capacity);letv=vland(lnot(1lslbits-1))invlorsize(* [empty] is equivalent to [view 0 0]. *)letempty:view=0let[@inline]resizevdelta=(* Changing the size of a view without moving its head can be done
with one addition, without going through shifting and masking. *)assert(v+delta=view(view_headv)(view_sizev+delta));v+delta(* -------------------------------------------------------------------------- *)module[@inline]Make(O:OVERWRITE_EMPTY_SLOTS)=structopenO(* -------------------------------------------------------------------------- *)(* A chunk is represented as an array [data], where only the circular
view [view] actually contains data. The [default] element is used
to overwrite a slot that becomes empty. *)type'at={mutableview:view;data:'aarray;default:'a;}(* -------------------------------------------------------------------------- *)(* Accessors. *)let[@inline]unchecked_headc=unchecked_view_headc.viewlet[@inline]unchecked_sizec=unchecked_view_sizec.viewlet[@inline]headc=view_headc.viewlet[@inline]sizec=view_sizec.viewlet[@inline]set_headch=c.view<-viewh(sizec)let[@inline]set_sizeci=c.view<-view_update_sizec.viewi(* or: [view (head c) i] *)let[@inline]set_head_sizechi=c.view<-viewhilet[@inline]capacityc=Array.lengthc.data(* -------------------------------------------------------------------------- *)(* A chunk satisfies the following invariant. *)letcheckc=letn=capacitycinassert(min_capacity<=n&&n<=max_capacity);assert(0<=headc&&headc<n);assert(sizec<=n);(* If [overwrite_empty_slots] is [true], then every empty slot must
contain the value [default]. *)ifoverwrite_empty_slotsthenfori=sizecton-1doassert(Array.getc.data((headc+i)modn)==c.default)done(* Ensure [check] has zero cost in release mode. *)let[@inline]checkc=assert(checkc;true)let[@inline]validatec=checkc;c(* -------------------------------------------------------------------------- *)(* Chunk creation functions. *)letcreatedn=assert(min_capacity<=n&&n<=max_capacity);validate{view=empty;data=Array.makend;default=d;}letdummyd={view=empty;data=[||];default=d;}let[@inline]is_dummyc=Array.lengthc.data=0(* [of_array_destructive d k data] creates a chunk whose default element is
[d] and whose size is [k] by taking ownership of the array [data]. The
array segment that extends from index [0] included to index [k] excluded
must contain valid elements. The rest of the array must be filled with
[default]. *)letof_array_destructivedkdata=assert(0<=k&&k<=Array.lengthdata);validate{view=view0k;data;default=d;}letmakednkv=assert(min_capacity<=n&&n<=max_capacity);assert(0<=k&&k<=n);letdata=ifk=nthenArray.makenvelseifk<n/2thenbegin(* Majority of [d]: initialize with [d], fill front with [v]. *)letdata=Array.makendinArray.filldata0kv;dataendelsebegin(* Majority of [v]: initialize with [v], fill back with [d]. *)letdata=Array.makenvinArray.filldatak(n-k)d;dataendinof_array_destructivedkdataletinitdnkif=assert(min_capacity<=n&&n<=max_capacity);assert(0<=k&&k<=n);letdata=Array.makendinforj=0tok-1doArray.setdataj(f(i+j));done;of_array_destructivedkdataletof_array_segmentdnaheadsize=(* [head] and [size] must represent a valid segment of the array [a]. *)assert(Segment.is_valid(a,head,size));(* [size] must be less than the desired capacity [n] of the chunk. *)assert(size<=n);(* Allocate an array of length [n], and copy a segment of size [size]
of the array [a] into it. *)letdata=ifsize=nthenArray.subaheadsizeelseletdata=Array.makendinArray.blitaheaddata0size;datainvalidate{view=view0size;data;default=d}(* -------------------------------------------------------------------------- *)(* Basic accessors. *)let[@inline]datac=c.datalet[@inline]defaultc=(* It is permitted to apply [default] to a dummy chunk. *)c.defaultlet[@inline]lengthc=(* It is permitted to apply [length] to a dummy chunk.
The result is zero. *)sizeclet[@inline]is_empty_or_dummyc=sizec=0let[@inline]is_full_or_dummyc=sizec=capacityclet[@inline]is_emptyc=assert(not(is_dummyc));sizec=0let[@inline]is_fullc=assert(not(is_dummyc));sizec=capacityc(* -------------------------------------------------------------------------- *)(* Internal index calculations. *)(* [wrap_up c i] adjusts the index [i], by wrapping around, in case
it exceeds the capacity of the chunk [c]. *)let[@inline]wrap_upci=letn=capacitycinassert(0<=i&&i<2*n);ifi<nthenielsei-n(* OR: [i mod n] *)(* [wrap_down c i] adjusts the index [i], by wrapping around, in case
it is negative. *)let[@inline]wrap_downci=letn=capacitycinassert(-n<=i&&i<n);ifi<0theni+nelsei(* OR: [i mod n] *)(* A benchmark (with flambda, with inlining and specialisation) suggests
that using a branch is significantly faster than using [mod]. *)(* -------------------------------------------------------------------------- *)(* Random access to a single element in a chunk. *)(* [index c i] converts the index [i], an index into the sequence of
elements represented by the chunk [c], to an index into the array
[c.data]. *)let[@inline]indexci=assert(0<=i&&i<lengthc);wrap_upc(headc+i)let[@inline]getci=Array.getc.data(indexci)let[@inline]setciy=Array.setc.data(indexci)y(* [xchg c i y] combines [get] and [set], saving one call to [index]. *)let[@inline]xchgciy=leti=indexciinletx=Array.getc.dataiinArray.setc.dataiy;x(* -------------------------------------------------------------------------- *)(* Stack operations: [peek], [push], [pop]. *)let[@inline]peek_indexpovc=matchpovwith|Front->0|Back->lengthc-1let[@inline]peekpovc=assert(0<lengthc);getc(peek_indexpovc)let[@inline]allocate_frontc=leti=wrap_downc(headc-1)inset_headci;ilet[@inline]allocate_backc=wrap_upc(headc+sizec)let[@inline]allocatepovc=assert(lengthc<capacityc);matchpovwith|Front->allocate_frontc|Back->allocate_backclet[@inline]pushpovcx=Array.setc.data(allocatepovc)x;c.view<-resizec.view(+1);checkclet[@inline]poppovc=assert(0<lengthc);letx=ifoverwrite_empty_slotsthenxchgc(peek_indexpovc)c.defaultelsegetc(peek_indexpovc)inbeginmatchpovwith|Front->set_head_sizec(wrap_upc(headc+1))(sizec-1)|Back->c.view<-resizec.view(-1)end;checkc;x(* -------------------------------------------------------------------------- *)(* Copying and clearing. *)letcopyc=validate{cwithdata=Array.copyc.data}letclearc=ifoverwrite_empty_slotsthenArrayExtra.fill_circularlyc.data(headc)(sizec)c.default;c.view<-empty;checkc;()(* -------------------------------------------------------------------------- *)(* Views. *)moduleView=structtypenonrecview=viewletcheck_viewcv=letn=capacitycin(* The view head must be within bounds. *)assert(0<=view_headv&&view_headv<n);(* The view size must be comprised between 0 and [size c], included. *)assert(0<=view_sizev);letslack=sizec-view_sizevinassert(slack>=0);(* The live area of the view must be included in the live area of
the chunk. This is expressed by computing the relative advance of
the view head over the chunk head, a nonnegative number, and
requiring this number to be at most [slack]. *)assert(wrap_downc(view_headv-headc)<=slack)(* Ensure [check_view] has zero cost in release mode. *)let[@inline]check_viewcv=assert(check_viewcv;true)letdummy=0let[@specialise]iter_segmentspov(c,v)yield=(* This function can be applied to a dummy chunk, in which case
the view size [s] is zero. *)lets=view_sizevinifs>0thenbeginletn=capacitycinleth=view_headvinleti=h+sinifi<=nthenyield(datac,h,s)elsematchpovwith|Front->yield(datac,h,n-h);yield(datac,0,i-n)|Back->yield(datac,0,i-n);yield(datac,h,n-h)endlet[@inline]iterpovfcv=ArrayExtra.iteriter_segmentspovfcvletfold_leftfcv=Adapters.fold_left(iterFront)fcvlet[@inline]peekpovcv=check_viewcv;assert(view_sizev>0);matchpovwith|Front->Array.getc.data(view_headv)|Back->Array.getc.data(wrap_upc(view_headv+view_sizev-1))let[@inline]indexcvi=check_viewcv;assert(0<=i&&i<view_sizev);wrap_upc(view_headv+i)let[@inline]getcvi=Array.getc.data(indexcvi)let[@inline]setcvix=Array.setc.data(indexcvi)xletthree_way_splitcvi=check_viewcv;assert(0<=i&&i<view_sizev);letfront=view_update_sizeviinletx=getcviinleti=i+1inletback=view(wrap_upc(view_headv+i))(view_sizev-i)infront,x,backlettakecvi=check_viewcv;assert(0<=i&&i<view_sizev);letfront=view_update_sizeviinletx=getcviinfront,xletdropcvi=check_viewcv;assert(0<=i&&i<view_sizev);letx=getcviinleti=i+1inletback=view(wrap_upc(view_headv+i))(view_sizev-i)inx,back(* We use the following terminology: a view is "flush" if it is flush with
one side (front or back) of a chunk. A view is "aligned" if it is flush
with both sides. *)let[@inline]is_flush_frontcv=headc=view_headvlet[@inline]is_flush_backcv=letslack=sizec-view_sizevinwrap_downc(view_headv-headc)=slacklet[@inline]is_flushpovcv=check_viewcv;matchpovwith|Front->is_flush_frontcv|Back->is_flush_backcvlet[@inline]is_alignedcv=check_viewcv;is_flush_frontcv&&sizec=view_sizev(* This is equivalent to [is_flush_front c v && is_flush_back c v]. *)let[@inline]push_frontcv=view(wrap_downc(view_headv-1))(view_sizev+1)let[@inline]push_back_cv=resizev(+1)let[@inline]pushpovcv=assert(view_sizev<capacityc);matchpovwith|Front->push_frontcv|Back->push_backcvlet[@inline]restrictcvik=assert(0<=i&&i<=view_sizev);assert(0<=k&&i+k<=view_sizev);view(wrap_upc(view_headv+i))klet[@inline]pop_frontcv=restrictcv1(view_sizev-1)let[@inline]pop_back_cv=resizev(-1)(* equivalent to: [restrict c v 0 (view_size v - 1)] *)let[@inline]poppovcv=assert(0<view_sizev);matchpovwith|Front->pop_frontcv|Back->pop_backcvlet[@inline]copy_frontc1v1c2v2=lettarget=wrap_downc2(view_headv2-view_sizev1)inArrayExtra.blit_circularlyc1.data(view_headv1)c2.datatarget(view_sizev1);set_head_sizec2target(sizec2+view_sizev1);checkc2;viewtarget(view_sizev1+view_sizev2)let[@inline]copy_backc1v1c2v2=lettarget=wrap_upc2(view_headv2+view_sizev2)inArrayExtra.blit_circularlyc1.data(view_headv1)c2.datatarget(view_sizev1);(* No change to [head c2] is required. *)c2.view<-resizec2.view(view_sizev1);resizev2(view_sizev1)let[@inline]copypovc1v1c2v2=check_viewc1v1;check_viewc2v2;assert(view_sizev1+view_sizev2<=capacityc2);matchpovwith|Front->copy_frontc1v1c2v2|Back->copy_backc1v1c2v2letsubcv=check_viewcv;letdefault=defaultcin(* We have a choice between 1- copying all of the data from the old
chunk to the new chunk; or 2- first initialize the new chunk with
a default element everywhere, then copy only the data in view
[v] from the old chunk to the new chunk. Approach 1- seems more
efficient, as every slot in the new chunk is written just once,
instead of possibly twice. However, approach 2- is always safe,
whereas approach 1- fails to overwrite empty slots with a default
value, so it is safe only if [overwrite_empty_slots] is [false]
or the view [v] covers all of the chunk [c]. *)letdata=ifnotoverwrite_empty_slots||is_alignedcvthen(* Approach 1: *)Array.copyc.dataelsebegin(* Approach 2: *)letdata=Array.make(capacityc)defaultinlethead,size=view_headv,view_sizevinArrayExtra.blit_circularlyc.dataheaddataheadsize;dataendinletview=vinvalidate{view;data;default}let[@inline]segmentpovikcv=letn=capacitycandh=view_headvands=view_sizevinassert(0<=i&&i<s);assert(0<=k);assert(k<=matchpovwithFront->s-i|Back->i+1);(* [j] is the absolute index of the first element of the view
in iteration order. *)letj=wrap_upc(h+i)inletj,m=matchpovwith|Front->(* The segment begins at index [j] and includes [m] elements,
where [m] is:
- at most [k] (thus no more than the number of elements
that exist in the chunk between index [j] and the end
of the chunk at index [wrap_up c (h + s)] excluded),
- at most the number of elements between index [j] and
index [n] excluded, because the segment must stop at
the physical end of the chunk and cannot wrap around. *)letm=mink(n-j)inassert(m<=k&&k<=s-i);assert(m<=s-i);j,m|Back->(* The segment ends at index [j] (included) and includes [m] elements,
where [m] is:
- at most [k] (thus no more than the number of elements
that exist in the chunk beweeen index [j] included and
the beginning of the chunk at index [h] included),
- at most the number of elements beweeen index [j] (included)
and index [0], because the segment must stop at the
physical beginning of the chunk and cannot wrap around. *)letm=mink(j+1)inassert(m<=k&&k<=i+1);assert(m<=i+1);assert(0<=j+1-m);j+1-m,minassert(Segment.is_valid(c.data,j,m));(* If [k > 0] then [m > 0]. *)assert(k=0||m>0);c.data,j,mletcheck=check_viewletprintv=letopenPPrint.OCamlinrecord"view"["head",int(unchecked_view_headv);"size",int(unchecked_view_sizev);]lethead=view_headletsize=view_sizeend(* View *)(* -------------------------------------------------------------------------- *)(* The following functions are relegated here because they use some of the
facilities offered by the submodule [View]. *)letcarve_backci=assert(0<=i&&i<=sizec);(* Compute the head and size of the back view. *)lethead=wrap_upc(headc+i)andsize=sizec-iinletv=viewheadsizeinletback=View.subcvinifoverwrite_empty_slotsthenArrayExtra.fill_circularlyc.dataheadsizec.default;set_sizeci;back(* [take] is a specialized version of [carve_back], where we construct
and keep only the front part of the chunk. *)lettakeci=assert(0<=i&&i<=sizec);ifoverwrite_empty_slotsthenbeginlethead=wrap_upc(headc+i)andsize=sizec-iinArrayExtra.fill_circularlyc.dataheadsizec.defaultend;set_sizeci(* [drop] is a specialized version of [carve_back], where we construct
and keep only the last part of the chunk. The code differs. *)letdropci=assert(0<=i&&i<=sizec);leth=headcinlethead=wrap_upc(h+i)andsize=sizec-iinifoverwrite_empty_slotsthenArrayExtra.fill_circularlyc.datahic.default;set_head_sizecheadsizelet[@inline]viewc=c.viewlet[@inline]iter_segmentspovcyield=(* [iter_segments] can be applied to a dummy chunk. *)View.iter_segmentspov(c,viewc)yield(* -------------------------------------------------------------------------- *)(* Printing. *)letiterpovfc=ArrayExtra.iteriter_segmentspovfcletto_listc=Adapters.to_list(iterBack)cletprintprintc=letopenPPrintinletopenPPrint.OCamlinifis_dummycthen!^"<dummy>"elseletmodel=(* The function [to_list] invokes [iter], which can fail if
the chunk is ill-formed. Catch these exceptions. *)tryflowing_listprint(to_listc)with|Assert_failure(s,i,j)->utf8format"<cannot print: Assert_failure (%S, %d, %d)>"sij|Invalid_arguments->utf8format"<cannot print: Invalid_argument %S>"sinrecord"chunk"["head",int(unchecked_headc);"size",int(unchecked_sizec);"model",model;]end(* Make *)