123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142(**************************************************************************)(* *)(* This file is part of WP plug-in of Frama-C. *)(* *)(* Copyright (C) 2007-2023 *)(* CEA (Commissariat a l'energie atomique et aux energies *)(* alternatives) *)(* *)(* you can redistribute it and/or modify it under the terms of the GNU *)(* Lesser General Public License as published by the Free Software *)(* Foundation, version 2.1. *)(* *)(* It is distributed in the hope that it will be useful, *)(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)(* GNU Lesser General Public License for more details. *)(* *)(* See the GNU Lesser General Public License version 2.1 *)(* for more details (enclosed in the file licenses/LGPLv2.1). *)(* *)(**************************************************************************)(* -------------------------------------------------------------------------- *)(* --- Merging Map Functor --- *)(* -------------------------------------------------------------------------- *)moduletypeKey=sigtypetvalhash:t->intvalequal:t->t->boolvalcompare:t->t->intendmoduleMake(K:Key)=structmoduleLmap=Listmap.Make(K)typekey=K.ttype'at='aLmap.tIntmap.t(* sorted collisions *)letis_emptym=tryIntmap.iteri(fun_m->ifm<>[]thenraiseExit)m;truewithExit->falseletempty=Intmap.emptylet_nonempty=function[]->None|l->Somellet_nonempty_inv=functionNone->[]|Somel->l(* good sharing *)letinsertfkvm=leth=K.hashkinIntmap.insert(fun_hkvold->matchkvwith|[k,v]->Lmap.insertfkvold|_->assertfalse)h[k,v]m(* good sharing *)(* val change : (key -> 'b -> 'a option -> 'a option) -> key -> 'b -> 'a t -> 'a t*)letchange(f:key->'b->'aoption->'aoption)(k:key)(v:'b)(m:'at)=leth=K.hashkinIntmap.change(fun_h(k,v)->function|None->(matchfkvNonewith|None->None|Somew->Some[k,w])|Someold->_nonempty(Lmap.changefkvold))h(k,v)m(* good sharing *)letaddkv=insert(fun_kx_old->x)kvletfindkm=Lmap.findk(Intmap.find(K.hashk)m)letfindkkm=Lmap.findkk(Intmap.find(K.hashk)m)letmemkm=tryignore(findkm);truewithNot_found->falseletmapfm=Intmap.map(Lmap.mapf)mletmapifm=Intmap.map(Lmap.mapif)mletmapff=Intmap.mapf(fun_hw->_nonempty(Lmap.mapffw))(* good sharing *)letmapqf=Intmap.mapq(fun_hw->_nonempty(Lmap.mapqfw))(* good sharing *)letfilterf=Intmap.mapq(fun_kw->_nonempty(Lmap.filterfw))(* good sharing *)letremovekm=leth=K.hashkinIntmap.change(fun_hk->function|None->None|Someold->_nonempty(Lmap.removekold))hkmletiterfm=Intmap.iter(Lmap.iterf)mletiter_sortedfm=letxs=Intmap.fold(List.merge(funab->K.compare(fsta)(fstb)))m[]inList.iter(fun(k,v)->fkv)xsletfoldfma=Intmap.fold(Lmap.foldf)maletfold_sortedfma=letxs=Intmap.fold(List.merge(funab->K.compare(fsta)(fstb)))m[]inList.fold_left(funacc(k,v)->fkvacc)axsletsizem=fold(fun__w->succw)m0(* good sharing *)letpartitionp=Intmap.partition_split(fun_kw->letu,v=Lmap.partitionpwin(_nonemptyu),(_nonemptyv))(* good sharing *)letunionf=Intmap.union(fun_h->Lmap.unionf)letinterf=Intmap.inter(fun_h->Lmap.interf)letinterff=Intmap.interf(fun_hab->_nonempty(Lmap.interffab))(* good sharing *)letinterqf=Intmap.interq(fun_hab->_nonempty(Lmap.interqfab))(* good sharing *)letdiffqf=Intmap.diffq(fun_hab->_nonempty(Lmap.diffqfab))letsubsetf=Intmap.subset(fun_h->Lmap.subsetf)letequaleqm1m2=Intmap.equal(Lmap.equaleq)m1m2letiterkf=Intmap.iterk(fun_h->Lmap.iterkf)letiter2f=Intmap.iter2(fun_hu1u2->Lmap.iter2f(_nonempty_invu1)(_nonempty_invu2))(* good sharing *)letmergef=Intmap.merge(fun_hu1u2->_nonempty(Lmap.mergef(_nonempty_invu1)(_nonempty_invu2)))end