123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517(*
* Copyright (C) 2016 David Scott <dave@recoil.org>
*
* Permission to use, copy, modify, and distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*
*)[@@@warning"-44"]moduletypeELT=sigtypetvalcompare:t->t->intvalzero:tvalpred:t->tvalsucc:t->tvalsub:t->t->tvaladd:t->t->tvalto_string:t->stringendmoduletypeINTERVAL_SET=sigtypeelttypeintervalmoduleInterval:sigvalmake:elt->elt->intervalvalx:interval->eltvaly:interval->eltendtypetvalequal:t->t->boolvalcompare:t->t->intvalpp:Format.formatter->t->unitvalempty:tvalis_empty:t->boolvalsingleton:elt->tvalcardinal:t->eltvalmem:elt->t->boolvalfold:(interval->'a->'a)->t->'a->'avalfold_individual:(elt->'a->'a)->t->'a->'avalfilter_map_individual:(elt->eltoption)->t->tvaliter:(interval->unit)->t->unitvaladd:interval->t->tvalremove:interval->t->tvalmin_elt:t->eltvalmax_elt:t->eltvalmin_interval:t->intervalvalmax_interval:t->intervalvalchoose:t->intervalvaltake:t->elt->(t*t)optionvalunion:t->t->tvalunions:tlist->tvaldiff:t->t->tvalinter:t->t->tvalsubset:t->t->boolvalcross_filter_map_individual:(elt->elt->eltoption)->t->t->tvalfind_next_gap:elt->t->eltvalelements:t->intervallistvalelements_individual:t->eltlistvalof_list:eltlist->tvalcheck_invariants:t->(unit,string)resultvalheight:t->intendmoduleMake(Elt:ELT)=structtypeelt=Elt.tmoduleElt=structincludeEltlet(-)=sublet(+)=addendtypeinterval=elt*eltmoduleInterval=structletmakexy=ifx>ytheninvalid_arg"Interval.make";(x,y)letx=fstlety=sndendlet(>)xy=Elt.comparexy>0let(>=)xy=Elt.comparexy>=0let(<)xy=Elt.comparexy<0let(<=)xy=Elt.comparexy<=0leteqxy=Elt.comparexy=0letsucc,pred=(Elt.succ,Elt.pred)typet=Empty|Node:node->tandnode={x:elt;y:elt;l:t;r:t;h:int;cardinal:elt}letreccons_enumtenum=matchtwith|Empty->enum|Node({l;_}asnode)->cons_enuml(node::enum)letcompare_with_invariant{x;y;_}{x=x';y=y';_}=ifeqxx'&&eqyy'then0elseify<x'then-1else1letreccompare_auxenumenum'=match(enum,enum')with|[],[]->0|[],_->-1|_,[]->1|node::enum,node'::enum'->(matchcompare_with_invariantnodenode'with|0->compare_aux(cons_enumnode.renum)(cons_enumnode'.renum')|c->c)letcomparett'=compare_aux(cons_enumt[])(cons_enumt'[])letequaltt'=comparett'=0letrecppfmt=function|Empty->Format.fprintffmt"Empty"|Noden->pp_nodefmtnandpp_nodefmt{x;y;l;r;h;cardinal}=Format.pp_open_vboxfmt0;Format.fprintffmt"x: %s@,"(Elt.to_stringx);Format.fprintffmt"y: %s@,"(Elt.to_stringy);Format.fprintffmt"l:@[@\n%a@]@,"ppl;Format.fprintffmt"r:@[@\n%a@]@,"ppr;Format.fprintffmt"h: %d@,"h;Format.fprintffmt"cardinal: %s"(Elt.to_stringcardinal);Format.pp_close_boxfmt()letheight=functionEmpty->0|Noden->n.hletcardinal=functionEmpty->Elt.zero|Noden->n.cardinalletcreatexylr=leth=max(heightl)(heightr)+1inletcardinal=Elt.(succ(y-x)+cardinall+cardinalr)inNode{x;y;l;r;h;cardinal}letrecnodexylr=lethl=heightlandhr=heightrinletopenStdlibinifhl>hr+2thenmatchlwith|Empty->assertfalse|Node{x=lx;y=ly;l=ll;r=lr;_}->(ifheightll>=heightlrthennodelxlyll(nodexylrr)elsematchlrwith|Empty->assertfalse|Node{x=lrx;y=lry;l=lrl;r=lrr;_}->nodelrxlry(nodelxlylllrl)(nodexylrrr))elseifhr>hl+2thenmatchrwith|Empty->assertfalse|Node{x=rx;y=ry;l=rl;r=rr;_}->(ifheightrr>=heightrlthennoderxry(nodexylrl)rrelsematchrlwith|Empty->assertfalse|Node{x=rlx;y=rly;l=rll;r=rlr;_}->noderlxrly(nodexylrll)(noderxryrlrrr))elsecreatexylrletdepthtree=letrecdepthtreek=matchtreewith|Empty->k0|Noden->depthn.l(fundl->depthn.r(fundr->k(1+maxdldr)))indepthtree(fund->d)moduleInvariant=structlet(>>=)xrf=matchxrwithOkx->fx|e->eletensurebmsgt=ifbthenOk()elseError(Format.asprintf"%s: %a"msgppt)letrecon_every_nodedf=matchdwith|Empty->Ok()|Noden->fnd>>=fun()->on_every_noden.lf>>=fun()->on_every_noden.rf(* The pairs (x, y) in each interval are ordered such that x <= y *)letordered{x;y;_}=ensure(x<=y)"Pairs within each interval should be ordered"(* The intervals don't overlap *)letno_overlap{x;y;l;r;_}n=leterror="Intervals should be ordered without overlap"in(matchlwithEmpty->Ok()|Nodeleft->ensure(left.y<x)errorn)>>=fun()->matchrwithEmpty->Ok()|Noderight->ensure(right.x>y)errornletno_adjacent{x;y;l;r;_}n=leterror="Intervals should not be adjacent"in(matchlwith|Empty->Ok()|Nodeleft->ensure(Elt.succleft.y<x)errorn)>>=fun()->matchrwith|Empty->Ok()|Noderight->ensure(Elt.predright.x>y)errornletnode_heightn=n.hletnode_depthn=depth(Noden)(* The height is being stored correctly *)letheight_equals_depthn=ensure(node_heightn=node_depthn)"The height is not being maintained correctly"letbalanced{l;r;_}=letdiff=heightl-heightrinletopenStdlibinensure(-2<=diff&&diff<=2)"The tree has become imbalanced"letcheck_cardinal{x;y;l;r;cardinal=c;_}=ensureElt.(c-cardinall-cardinalr-y+x=succzero)"The cardinal value stored in the node is wrong"letcheckt=on_every_nodetordered>>=fun()->on_every_nodetno_overlap>>=fun()->on_every_nodetheight_equals_depth>>=fun()->on_every_nodetbalanced>>=fun()->on_every_nodetcheck_cardinal>>=fun()->on_every_nodetno_adjacentendletempty=Emptyletis_empty=functionEmpty->true|_->falseletrecmemelt=function|Empty->false|Noden->(* consider this interval *)(elt>=n.x&&elt<=n.y)||(* or search left or search right *)ifelt<n.xthenmemeltn.lelsememeltn.rletrecmin_interval=function|Empty->raiseNot_found|Node{x;y;l=Empty;_}->(x,y)|Node{l;_}->min_intervallletrecmax_interval=function|Empty->raiseNot_found|Node{x;y;r=Empty;_}->(x,y)|Node{r;_}->max_intervalrletmin_eltt=min_intervalt|>Interval.xletmax_eltt=max_intervalt|>Interval.yletchoose=functionEmpty->raiseNot_found|Node{x;y;_}->(x,y)(* fold over the maximal contiguous intervals *)letrecfoldftacc=matchtwith|Empty->acc|Noden->letacc=foldfn.laccinletacc=f(n.x,n.y)accinfoldfn.racc(* fold over individual elements *)letfold_individualftacc=letrange(from,upto)acc=letrecloopaccx=ifeqx(succupto)thenaccelseloop(fxacc)(succx)inloopaccfrominfoldrangetaccletelementst=foldList.const[]letelements_individualt=fold_individualList.const[](* iterate over maximal contiguous intervals *)letiterft=letf'itl()=fitlinfoldf't()(* return (x, y, l) where (x, y) is the maximal interval and [l] is
the rest of the tree on the left (whose intervals are all smaller). *)letrecsplitMax=function|{x;y;l;r=Empty;_}->(x,y,l)|{r=Noder;_}asn->letu,v,r'=splitMaxrin(u,v,noden.xn.yn.lr')(* return (x, y, r) where (x, y) is the minimal interval and [r] is
the rest of the tree on the right (whose intervals are all larger) *)letrecsplitMin=function|{x;y;l=Empty;r;_}->(x,y,r)|{l=Nodel;_}asn->letu,v,l'=splitMinlin(u,v,noden.xn.yl'n.r)letaddL=function|{l=Empty;_}asn->n|{l=Nodel;_}asn->(* we might have to merge the new element with the maximal interval from
the left *)letx',y',l'=splitMaxlinifeq(succy')n.xthen{nwithx=x';l=l'}elsenletaddR=function|{r=Empty;_}asn->n|{r=Noder;_}asn->(* we might have to merge the new element with the minimal interval on
the right *)letx',y',r'=splitMinrinifeq(succn.y)x'then{nwithy=y';r=r'}elsenletrecadd(x,y)t=ify<xtheninvalid_arg"interval reversed";matchtwith|Empty->nodexyEmptyEmpty(* completely to the left *)|Nodenwheny<Elt.predn.x->letl=add(x,y)n.linnoden.xn.yln.r(* completely to the right *)|NodenwhenElt.succn.y<x->letr=add(x,y)n.rinnoden.xn.yn.lr(* overlap on the left only *)|Nodenwhenx<n.x&&y<=n.y->letl=add(x,predn.x)n.linletn=addL{nwithl}innoden.xn.yn.ln.r(* overlap on the right only *)|Nodenwheny>n.y&&x>=n.x->letr=add(succn.y,y)n.rinletn=addR{nwithr}innoden.xn.yn.ln.r(* overlap on both sides *)|Nodenwhenx<n.x&&y>n.y->letl=add(x,predn.x)n.linletr=add(succn.y,y)n.rinletn=addL{(addR{nwithr})withl}innoden.xn.yn.ln.r(* completely within *)|Noden->Nodenletunionab=leta'=cardinalaandb'=cardinalbinifa'>b'thenfoldaddbaelsefoldaddab(* Added by Hadrien Renaud *)letrecpairwise_unionsacc=function|[]->acc|x::[]->x::acc|x::y::li->pairwise_unions(unionxy::acc)liletrecunions=function|[]->empty|x::[]->x|li->pairwise_unions[]li|>unions(* End added by Hadrien Renaud *)letmergelr=match(l,r)with|l,Empty->l|Empty,r->r|Nodel,r->letx,y,l'=splitMaxlinnodexyl'rletrecremove(x,y)t=ify<xtheninvalid_arg"interval reversed";matchtwith|Empty->Empty(* completely to the left *)|Nodenwheny<n.x->letl=remove(x,y)n.linnoden.xn.yln.r(* completely to the right *)|Nodenwhenn.y<x->letr=remove(x,y)n.rinnoden.xn.yn.lr(* overlap on the left only *)|Nodenwhenx<n.x&&y<n.y->letn'=node(succy)n.yn.ln.rinremove(x,predn.x)n'(* overlap on the right only *)|Nodenwheny>n.y&&x>n.x->letn'=noden.x(predx)n.ln.rinremove(succn.y,y)n'(* overlap on both sides *)|Nodenwhenx<=n.x&&y>=n.y->letl=remove(x,n.x)n.linletr=remove(n.y,y)n.rinmergelr(* completely within *)|Nodenwheneqyn.y->noden.x(predx)n.ln.r|Nodenwheneqxn.x->node(succy)n.yn.ln.r|Noden->assert(n.x<=predx);assert(succy<=n.y);letr=node(succy)n.yEmptyn.rinnoden.x(predx)n.lrletdiffab=foldremovebaletinterab=diffa(diffab)letsubsetab=is_empty(diffab)letrecfind_next_gapfrom=function|Empty->from|Noden->(* consider this interval *)iffrom>=n.x&&from<=n.ythensuccn.y(* or search left *)elseiffrom<n.xthenfind_next_gapfromn.l(* or search right *)elsefind_next_gapfromn.rlettaketn=letrecloopaccfreen=ifn=Elt.zerothenSome(acc,free)elsematchtryleti=choosefreeinletx,y=Interval.(xi,yi)inletlen=Elt.(succ@@(y-x))inletwill_use=ifStdlib.(Elt.comparenlen<0)thennelseleninleti'=Interval.makexElt.(pred@@(x+will_use))inSome(addi'acc,removei'free,Elt.(n-will_use))withNot_found->Nonewith|Some(acc',free',n')->loopacc'free'n'|None->Noneinloopemptytnletof_sorted_list=letrecloopaccxy=function|[]->add(Interval.makexy)acc|z::t->lety'=Elt.succyinifeqy'zthenloopaccxy'telseloop(add(Interval.makexy)acc)zztinfunction[]->empty|x::t->loopemptyxxtletof_listli=List.sort_uniqElt.compareli|>of_sorted_listletfilter_map_individualft=fold_individual(funxacc->matchfxwithSomez->z::acc|None->acc)t[]|>of_listletcross_filter_map_individualft1t2=fold_individual(funx->fold_individual(funyacc->matchfxywithSomez->z::acc|None->acc)t2)t1[]|>of_listletcheck_invariants=Invariant.checkletsingletonx=add(Interval.makexx)emptyletpp_intervalfmti=letx,y=Interval.(xi,yi)inifeqxythenFormat.fprintffmt"{%s}"(Elt.to_stringx)elseFormat.fprintffmt"[%s, %s]"(Elt.to_stringx)(Elt.to_stringy)letppfmt=letopenFormatinfunction|Empty->fprintffmt"∅"|t->letm=min_intervaltinlett=removemtinpp_open_hovboxfmt0;pp_intervalfmtm;iter(funi->fprintffmt"@ \u{222a} ";pp_intervalfmti)t;pp_close_boxfmt()endmoduleInt_elt=structtypet=intletcompareab=compare(a:int)bletzero=0letpred=predletsucc=succletsub=(-)letadd=(+)letto_string=string_of_intendmoduleInt=Make(Int_elt)moduleInt64=Make(Int64)moduleZ=Make(Z)