123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180(* (c) 2017, 2018 Hannes Mehnert, all rights reserved *)(* this code wouldn't exist without Justus Matthiesen, thanks for the help! *)moduleOrder=structtype(_,_)t=|Lt:('a,'b)t|Eq:('a,'a)t|Gt:('a,'b)tendmoduletypeKEY=sigtype_tvalcompare:'at->'bt->('a,'b)Order.tendmoduletypeS=sigtype'akeytypetvalempty:tvalsingleton:'akey->'a->tvalis_empty:t->boolvalcardinal:t->intvalmem:'akey->t->boolvalfind:'akey->t->'aoptionvalget:'akey->t->'avaladd_unless_bound:'akey->'a->t->toptionvaladd:'akey->'a->t->tvalremove:'akey->t->tvalupdate:'akey->('aoption->'aoption)->t->ttypeb=B:'akey*'a->bvalmin_binding:t->boptionvalmax_binding:t->boptionvalany_binding:t->boptionvalbindings:t->blisttypeeq={f:'a.'akey->'a->'a->bool}valequal:eq->t->t->booltypemapper={f:'a.'akey->'a->'a}valmap:mapper->t->tvaliter:(b->unit)->t->unitvalfold:(b->'a->'a)->t->'a->'avalfor_all:(b->bool)->t->boolvalexists:(b->bool)->t->boolvalfilter:(b->bool)->t->ttypemerger={f:'a.'akey->'aoption->'aoption->'aoption}valmerge:merger->t->t->ttypeunionee={f:'a.'akey->'a->'a->'aoption}valunion:unionee->t->t->tendmoduleMake(Key:KEY):Swithtype'akey='aKey.t=structtype'akey='aKey.ttypek=K:'akey->ktypeb=B:'akey*'a->bmoduleM=Map.Make(structtypet=kletcompare(Ka)(Kb)=matchKey.compareabwith|Order.Lt->-1|Order.Eq->0|Order.Gt->1end)typet=bM.tletempty=M.emptyletsingletonkv=M.singleton(Kk)(B(k,v))letis_empty=M.is_emptyletmemkm=M.mem(Kk)mletaddkvm=M.add(Kk)(B(k,v))mletadd_unless_boundkvm=ifmemkmthenNoneelseSome(addkvm)letremovekm=M.remove(Kk)mletget:typea.akey->t->a=funkm->matchM.find(Kk)mwith|B(k',v)->(* TODO this compare (and further below similar ones) is only needed for
the type checker (to get the k = k' proof), because the invariant
foreach k . t [K k] = B (k', v) -> k = k' is preserved by this library
it could be replaced by:
- Obj.magic
- vendor and slight modification of Stdlib.Map
- using integers as key -> compare can be a single instruction
Stay better safe than sorry (at least for now) *)matchKey.comparekk'with|Order.Eq->v|_->assertfalseletfind:typea.akey->t->aoption=funkm->trySome(getkm)withNot_found->Noneletupdatekfm=matchf(findkm)with|None->removekm|Somev->addkvmletany_bindingm=trySome(snd(M.choosem))withNot_found->Noneletmin_bindingm=trySome(snd(M.min_bindingm))withNot_found->Noneletmax_bindingm=trySome(snd(M.max_bindingm))withNot_found->Noneletbindingsm=snd(List.split(M.bindingsm))letcardinalm=M.cardinalmletfor_allpm=M.for_all(fun_b->pb)mletexistspm=M.exists(fun_b->pb)mletiterfm=M.iter(fun_b->fb)mletfoldfmacc=M.fold(fun_bacc->fbacc)maccletfilterpm=M.filter(fun_b->pb)mtypemapper={f:'a.'akey->'a->'a}letmapfm=M.map(fun(B(k,v))->B(k,f.fkv))mtypemerger={f:'a.'akey->'aoption->'aoption->'aoption}letmergefmm'=M.merge(fun(Kk)bb'->matchb,b'with|None,None->beginmatchf.fkNoneNonewith|None->None|Somev->Some(B(k,v))end|None,Some(B(k',v))->(* see above comment about compare *)beginmatchKey.comparekk'with|Order.Eq->(matchf.fkNone(Somev)with|None->None|Somev->Some(B(k,v)))|_->assertfalseend|Some(B(k',v)),None->(* see above comment about compare *)beginmatchKey.comparekk'with|Order.Eq->(matchf.fk(Somev)Nonewith|None->None|Somev->Some(B(k,v)))|_->assertfalseend|Some(B(k',v)),Some(B(k'',v'))->(* see above comment about compare *)beginmatchKey.comparekk',Key.comparekk''with|Order.Eq,Order.Eq->(matchf.fk(Somev)(Somev')with|None->None|Somev->Some(B(k,v)))|_->assertfalseend)mm'typeunionee={f:'a.'akey->'a->'a->'aoption}letunionfmm'=M.union(fun(Kk)(B(k',v))(B(k'',v'))->(* see above comment about compare *)matchKey.comparekk',Key.comparekk''with|Order.Eq,Order.Eq->(matchf.fkvv'withNone->None|Somev''->Some(B(k,v'')))|_->assertfalse)mm'typeeq={f:'a.'akey->'a->'a->bool}letequalcmpmm'=M.equal(fun(B(k,v))(B(k',v'))->(* see above comment about compare *)matchKey.comparekk'with|Order.Eq->cmp.fkvv'|_->assertfalse)mm'end