123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116(**************************************************************************)(* *)(* 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). *)(* *)(**************************************************************************)moduletypeS=sigtypeelttypetvalempty:tvalis_empty:t->boolvalmem:elt->t->boolvalfind:elt->t->eltvaladd:elt->t->tvalsingleton:elt->tvalremove:elt->t->tvalunion:t->t->tvalinter:t->t->tvaldiff:t->t->tvalcompare:t->t->intvalequal:t->t->boolvalsubset:t->t->boolvaliter:(elt->unit)->t->unitvalfold:(elt->'a->'a)->t->'a->'avalfor_all:(elt->bool)->t->boolvalexists:(elt->bool)->t->boolvalfilter:(elt->bool)->t->tvalpartition:(elt->bool)->t->t*tvalcardinal:t->intvalelements:t->eltlistvalmap:(elt->elt)->t->tvalmapf:(elt->eltoption)->t->tvalintersect:t->t->boolendmoduletypeIndexedElements=sigtypetvalid:t->int(* unique per t *)endmoduleMake(E:IndexedElements)=structtypet=E.tIntmap.ttypeelt=E.tletempty=Intmap.emptyletsingletonx=Intmap.singleton(E.idx)x(* good sharing *)letaddx=Intmap.add(E.idx)x(* good sharing *)letremovex=Intmap.remove(E.idx)letis_empty=Intmap.is_emptyletmemxm=Intmap.mem(E.idx)mletfindxm=Intmap.find(E.idx)mletcardinal=Intmap.sizeletcomparem1m2=Intmap.compare(fun__->0)m1m2letequalm1m2=Intmap.equal(fun__->true)m1m2let_keep_x_=xlet_keepq_x_=Somexlet_same___=true(* good sharing *)letunionm1m2=Intmap.union_keepm1m2(* good sharing *)letinterm1m2=Intmap.interq_keepqm1m2(* good sharing *)letdiffm1m2=Intmap.diffq_keepqm1m2letsubsetm1m2=Intmap.subset_samem1m2letintersectm1m2=Intmap.intersectf_samem1m2(* increasing order on id *)letiterfm=Intmap.iteri(fun_ix->fx)m(* increasing order on id *)letfoldfmi=Intmap.foldi(fun_ixe->fxe)mi(* good sharing *)letfilterfm=Intmap.filter(fun_ix->fx)m(* good sharing *)letpartitionfm=Intmap.partition(fun_ix->fx)mletfor_allfm=Intmap.for_all(fun_ix->fx)mletexistsfm=Intmap.exists(fun_ix->fx)m(* increasing order on id *)letelementsm=Intmap.mapl(fun_ix->x)m(* good sharing *)letmapffm=Intmap.mapq(fun_ix->fx)m(* good sharing *)letmapfm=Intmap.mapq(fun_ix->Some(fx))mend