123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361(* Copyright (c) 2016 David Kaloper Meršinjak. All rights reserved.
See LICENSE.md *)type'afmt=Format.formatter->'a->unitletpf=Format.fprintfmoduletypeOrdered=sigtypetvalcompare:t->t->intendmoduletypeS=sigtypettypektypepvalempty:tvalsg:k->p->tval(++):t->t->tvalis_empty:t->boolvalsize:t->intvalmem:k->t->boolvalfind:k->t->poptionvaladd:k->p->t->tvalremove:k->t->tvaladjust:k->(p->p)->t->tvalupdate:k->(poption->poption)->t->tvalmin:t->(k*p)optionvalrest:t->toptionvalpop:t->((k*p)*t)optionvalfold_at_most:p->(k->p->'a->'a)->'a->t->'avaliter_at_most:p->(k->p->unit)->t->unitvalto_seq_at_most:p->t->(k*p)Seq.tvalof_list:(k*p)list->tvalof_sorted_list:(k*p)list->tvalof_seq:(k*p)Seq.t->tvaladd_seq:(k*p)Seq.t->t->tvalto_list:t->(k*p)listvalto_seq:t->(k*p)Seq.tvalfold:(k->p->'a->'a)->'a->t->'avaliter:(k->p->unit)->t->unitvalto_priority_list:t->(k*p)listvalto_priority_seq:t->(k*p)Seq.tvalfilter:(k->p->bool)->t->tvalpartition:(k->p->bool)->t->t*tvalpp:?sep:(unitfmt)->(k*p)fmt->tfmtvalpp_dump:kfmt->pfmt->tfmtvaldepth:t->intendmoduleL=structincludeListletrectaken=functionx::xswhenn>0->x::take(predn)xs|_->[]letrecdropn=function_::xswhenn>0->drop(predn)xs|xs->xsendmoduleMake(K:Ordered)(P:Ordered):Swithtypek=K.tandtypep=P.t=structtypek=K.ttypep=P.ttypet=(* SEARCH PENNANTS *)N|Tof(k*p)*k*treeandtree=(* LOSER TREES, OH MY *)Lf|NdLof(k*p)*tree*k*tree*int|NdRof(k*p)*tree*k*tree*intletempty=Nletsg(k,_askp)=T(kp,k,Lf)letis_empty=functionN->true|_->falseletsize_t=functionLf->0|NdL(_,_,_,_,w)|NdR(_,_,_,_,w)->wletsize=functionN->0|T(_,_,t)->size_tt+1letnd_lkpt1skt2=NdL(kp,t1,sk,t2,size_tt1+size_tt2+1)letnd_rkpt1skt2=NdR(kp,t1,sk,t2,size_tt1+size_tt2+1)letnd(k,_askp)t1skt2=ifK.compareksk<=0thennd_lkpt1skt2elsend_rkpt1skt2letoutweighss1s2=s1*100>s2*375let(@<=@)(k1,p1)(k2,p2)=matchP.comparep1p2with0->K.comparek1k2<=0|c->c<0[@@inline]letrot_lkp1t1sk1=functionNdL(kp2,t2,sk2,t3,_)whenkp1@<=@kp2->ndkp1(ndkp2t1sk1t2)sk2t3|NdL(kp2,t2,sk2,t3,_)|NdR(kp2,t2,sk2,t3,_)->ndkp2(ndkp1t1sk1t2)sk2t3|Lf->assertfalseletrot_rkp1ttsk2t3=matchttwithNdR(kp2,t1,sk1,t2,_)whenkp1@<=@kp2->ndkp1t1sk1(ndkp2t2sk2t3)|NdL(kp2,t1,sk1,t2,_)|NdR(kp2,t1,sk1,t2,_)->ndkp2t1sk1(ndkp1t2sk2t3)|Lf->assertfalseletrot_llkp1t1sk1=functionNdL(kp2,t2,sk2,t3,_)|NdR(kp2,t2,sk2,t3,_)->rot_lkp1t1sk1(rot_rkp2t2sk2t3)|Lf->assertfalseletrot_rrkp1ttsk2t3=matchttwithNdL(kp2,t1,sk1,t2,_)|NdR(kp2,t1,sk1,t2,_)->rot_rkp1(rot_lkp2t1sk1t2)sk2t3|Lf->assertfalse(* Precond: at most one of t1, t2 is at most 1 away from a balanced
configuration. *)letnd_balkpt1skt2=lets1=size_tt1ands2=size_tt2inmatch(t1,t2)with((NdL(_,t11,_,t12,_)|NdR(_,t11,_,t12,_)),_)whens1>1&&outweighss1s2->ifsize_tt11>size_tt12thenrot_rkpt1skt2elserot_rrkpt1skt2|(_,(NdL(_,t21,_,t22,_)|NdR(_,t21,_,t22,_)))whens2>1&&outweighss2s1->ifsize_tt21<size_tt22thenrot_lkpt1skt2elserot_llkpt1skt2|_->ndkpt1skt2let(><)t1t2=match(t1,t2)with(N,t)|(t,N)->t|(T(kp1,sk1,t1),T(kp2,sk2,t2))->ifkp1@<=@kp2thenT(kp1,sk2,nd_balkp2t1sk1t2)elseT(kp2,sk2,nd_balkp1t1sk1t2)[@@inline]let(>|<)(k1,_askp1)(k2,_askp2)=ifkp1@<=@kp2thenT(kp1,k2,NdR(kp2,Lf,k1,Lf,1))elseT(kp2,k2,NdL(kp1,Lf,k1,Lf,1))[@@inline]letrecpromotesk0=functionLf->N|NdL(kp,t1,sk,t2,_)->T(kp,sk,t1)><promotesk0t2|NdR(kp,t1,sk,t2,_)->promoteskt1><T(kp,sk0,t2)letmin=functionN->None|T(kp,_,_)->Somekpletrest=functionN->None|T(_,sk,t)->Some(promoteskt)letpop=functionN->None|T(kp,sk,t)->Some(kp,promoteskt)letfindk0t=letrecgok0=functionLf->None|NdL((k,p),t1,sk,t2,_)|NdR((k,p),t1,sk,t2,_)->ifK.comparek0k=0thenSomepelseifK.comparek0sk<=0thengok0t1elsegok0t2inmatchtwithN->None|T((k,p),_,t)->ifK.comparek0k=0thenSomepelsegok0tletmemk0t=letrecgok0=functionLf->false|NdL((k,_),t1,sk,t2,_)|NdR((k,_),t1,sk,t2,_)->K.comparek0k=0||ifK.comparek0sk<=0thengok0t1elsegok0t2inmatchtwithN->false|T((k,_),_,t)->K.comparek0k=0||gok0tletfoldr_at_mostp0ftz=letrecf1p0(_,paskp)fzt=ifP.comparepp0<=0thenf2p0kpfztelsez()andf2p0kp0fz=functionLf->fkp0z|NdL(kp,t1,_,t2,_)->f1p0kpf(fun()->f2p0kp0fzt2)t1|NdR(kp,t1,_,t2,_)->f2p0kp0f(fun()->f1p0kpfzt2)t1inmatchtwithT(kp0,_,t)->f1p0kp0fzt|_->z()letfold_at_mostp0fzt=foldr_at_mostp0(fun(k,p)a->fkp(a()))t(fun()->z)letiter_at_mostp0ft=foldr_at_mostp0(fun(k,p)i->fkp;i())tignoreletto_seq_at_mostp0t()=foldr_at_mostp0(funkpseq->Seq.Cons(kp,seq))tSeq.empty(* type view = Nv | Sgv of (k * p) | Binv of t * K.t * t *)(* let view = function *)(* N -> Nv *)(* | T (kp, _, Lf) -> Sgv kp *)(* | T (kp1, sk1, NdL (kp2, t1, sk2, t2, _)) -> *)(* Binv (T (kp2, sk2, t1), sk2, T (kp1, sk1, t2)) *)(* | T (kp1, sk1, NdR (kp2, t1, sk2, t2, _)) -> *)(* Binv (T (kp1, sk2, t1), sk2, T (kp2, sk1, t2)) *)(* let rec add (k0, _ as kp0) t = match view t with *)(* | Nv -> sg kp0 *)(* | Sgv (k, _) -> *)(* let c = K.compare k0 k and t' = sg kp0 in *)(* if c < 0 then t' >< t else if c > 0 then t >< t' else t' *)(* | Binv (t1, sk, t2) -> *)(* if K.compare k0 sk <= 0 then add kp0 t1 >< t2 else t1 >< add kp0 t2 *)(* let remove k0 t = *)(* let rec go k0 t = match view t with *)(* Binv (t1, sk, t2) -> *)(* if K.compare k0 sk <= 0 then go k0 t1 >< t2 else t1 >< go k0 t2 *)(* | Sgv (k, _) when K.compare k k0 = 0 -> N *)(* | Sgv _ | Nv -> raise_notrace Exit in *)(* try go k0 t with Exit -> t *)(* let adjust k0 f t = *)(* let rec go f k0 t = match view t with *)(* Binv (t1, sk, t2) -> *)(* if K.compare k0 sk <= 0 then go f k0 t1 >|< t2 else t1 >|< go f k0 t2 *)(* | Sgv (k, p) when K.compare k k0 = 0 -> sg (k, f p) *)(* | Sgv _ | Nv -> raise_notrace Exit in *)(* try go f k0 t with Exit -> t *)(* let rec filter pf t = match view t with *)(* Nv -> N *)(* | Sgv (k, p as kp) -> if pf k p then sg kp else N *)(* | Binv (t1, _, t2) -> filter pf t1 >< filter pf t2 *)letupdatek0ft=letnodefk0p=matchfpwithSomep->sg(k0,p)|None->N[@@inline]inletrecgok0f(k1,p1askp1)sk1=functionLf->letc=K.comparek0k1inifc=0thennodefk0(Somep1)else(matchfNonewithSomep->ifc<0then(k0,p)>|<kp1elsekp1>|<(k0,p)|None->raise_notraceExit)|NdL(kp2,t1,sk2,t2,_)->ifK.comparek0sk2<=0thengok0fkp2sk2t1><T(kp1,sk1,t2)elseT(kp2,sk2,t1)><gok0fkp1sk1t2|NdR(kp2,t1,sk2,t2,_)->ifK.comparek0sk2<=0thengok0fkp1sk2t1><T(kp2,sk1,t2)elseT(kp1,sk2,t1)><gok0fkp2sk1t2inmatchtwithN->nodefk0None|T(kp,sk,t1)->trygok0fkpskt1withExit->tletaddkpt=updatek(fun_->Somep)tletremovekt=updatek(fun_->None)tletadjustkft=updatek(functionSomep->Some(fp)|_->None)tletfilterpft=letrecgopfkp1sk1=functionLf->ifpf(fstkp1)(sndkp1)thensgkp1elseN|NdL(kp2,t1,sk2,t2,_)->gopfkp2sk2t1><gopfkp1sk1t2|NdR(kp2,t1,sk2,t2,_)->gopfkp1sk2t1><gopfkp2sk1t2inmatchtwithN->N|T(kp,sk,t)->gopfkpsktletpartitionpft=(filterpft,filter(funkp->not(pfkp))t)letof_sorted_listxs=letrecgon=function[]->N|[x]->sgx|[x;y]->x>|<y|[x;y;z]->(x>|<y)><sgz|[x;y;z;w]->(x>|<y)><(z>|<w)|xs->letm=n/2ingomL.(takemxs)><go(n-m)L.(dropmxs)ingo(L.lengthxs)xsletcmp_k(k1,_)(k2,_)=K.comparek1k2letof_listxs=Psq_list.sort_uniqcmp_kxs|>of_sorted_listletof_seqxs=Seq.fold_left(funxsa->a::xs)[]xs|>of_listletadd_seqxsq=Seq.fold_left(funq(k,p)->addkpq)qxsletiterft=letrecgo(p0,k0aspk0)f=functionLf->fp0k0|NdL(pk,t1,_,t2,_)->gopkft1;gopk0ft2|NdR(pk,t1,_,t2,_)->gopk0ft1;gopkft2inmatchtwithN->()|T(pk,_,t)->gopkftletfoldrfzt=letrecgokp0fz=functionLf->fkp0z|NdL(kp,t1,_,t2,_)->gokpf(gokp0fzt2)t1|NdR(kp,t1,_,t2,_)->gokp0f(gokpfzt2)t1inmatchtwithN->z|T(kp,_,t)->gokpfztletlfoldrftz=letrecgokp0fz=functionLf->fkp0z|NdL(kp,t1,_,t2,_)->gokpf(fun()->gokp0fzt2)t1|NdR(kp,t1,_,t2,_)->gokp0f(fun()->gokpfzt2)t1inmatchtwithT(kp,_,t)->gokpfzt|N->z()let(++)q1q2=foldr(fun(k,p)q->addkpq)q1q2letfoldfzt=foldr(fun(k,p)z->fkpz)ztletto_listt=foldr(funkpxs->kp::xs)[]tletto_seqt()=lfoldr(funkpxs->Seq.Cons(kp,xs))tSeq.emptyletto_priority_listt=letrec(--)xsys=matchxs,yswith[],l|l,[]->l|x::xt,y::yt->ifx@<=@ythenx::(xt--ys)elsey::(xs--yt)inletrecgo=functionLf->[]|NdL(kp2,t1,_,t2,_)->(kp2::got1)--got2|NdR(kp2,t1,_,t2,_)->got1--(kp2::got2)inmatchtwithN->[]|T(kp,_,t)->kp::gotletto_priority_seqt()=letopenSeqinletrec(--)n1n2=matchn1,n2withNil,n|n,Nil->n|Cons(x,xt),Cons(y,yt)->ifx@<=@ythenCons(x,fun_->xt()--n2)elseCons(y,fun_->n1--yt())inletrecgo=functionLf->Nil|NdL(kp2,t1,_,t2,_)->Cons(kp2,fun_->got1)--got2|NdR(kp2,t1,_,t2,_)->got1--Cons(kp2,fun_->got2)inmatchtwithN->Nil|T(kp,_,t)->Cons(kp,fun_->got)letsgkp=sg(k,p)letdeptht=letrecgo=functionLf->0|NdL(_,t1,_,t2,_)|NdR(_,t1,_,t2,_)->max(got1)(got2)+1inmatchtwithN->0|T(_,_,t)->got+1letpp?(sep=Format.pp_print_space)ppppft=letfirst=reftrueinletkppf=iter@@funkp->(match!firstwithtrue->first:=false|_->sepppf());ppppf(k,p)inpfppf"@[%a@]"ktletpp_dumpppkpppppf=letsepppf()=pfppf";@ "andppkpppf(k,p)=pfppf"(@[%a,@ %a@])"ppkkppppinpfppf"of_sorted_list [%a]"(pp~sepppkp)end