123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150(************************************************************************)(* * The Coq Proof Assistant / The Coq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)moduletypeS=sigtypenodemoduleNodeSet:Set.Swithtypeelt=nodetype('edge,'info,'cdata)tvalempty:('e,'i,'d)tvaladd_edge:('e,'i,'d)t->node->'e->node->('e,'i,'d)tvalfrom_node:('e,'i,'d)t->node->(node*'e)listvalmem:('e,'i,'d)t->node->boolvaldel_edge:('e,'i,'d)t->node->node->('e,'i,'d)tvaldel_nodes:('e,'i,'d)t->NodeSet.t->('e,'i,'d)tvalall_nodes:('e,'i,'d)t->NodeSet.tvalget_info:('e,'i,'d)t->node->'ioptionvalset_info:('e,'i,'d)t->node->'i->('e,'i,'d)tvalclear_info:('e,'i,'d)t->node->('e,'i,'d)tmoduleProperty:sigtype'dtvalequal:'dt->'dt->boolvalcompare:'dt->'dt->intvalto_string:'dt->stringvaldata:'dt->'dvalhaving_it:'dt->NodeSet.tendvalcreate_property:('e,'i,'d)t->nodelist->'d->('e,'i,'d)tvalproperty_of:('e,'i,'d)t->node->'dProperty.tlistvaldel_property:('e,'i,'d)t->'dProperty.t->('e,'i,'d)tvaliter:('e,'i,'d)t->(node->'dProperty.tlist->'ioption->(node*'e)list->unit)->unitendmoduleMake(OT:Map.OrderedType)=structmoduleNodeSet=Set.Make(OT)moduleProperty=structtype'dt={data:'d;uid:int;having_it:NodeSet.t}letequal{uid=i1}{uid=i2}=Int.equali1i2letcompare{uid=i1}{uid=i2}=Int.comparei1i2letto_string{uid=i}=string_of_intiletdata{data=d}=dlethaving_it{having_it}=having_itendtypenode=OT.tmoduleNodeMap=CMap.Make(OT)type('edge,'info,'data)t={graph:(node*'edge)listNodeMap.t;properties:'dataProperty.tlistNodeMap.t;infos:'infoNodeMap.t;}letempty={graph=NodeMap.empty;properties=NodeMap.empty;infos=NodeMap.empty;}letmem{graph}id=NodeMap.memidgraphletadd_edgedagfromtransdest={dagwithgraph=tryNodeMap.modifyfrom(fun_arcs->(dest,trans)::arcs)dag.graphwithNot_found->NodeMap.addfrom[dest,trans]dag.graph}letfrom_node{graph}id=NodeMap.findidgraphletdel_edgedagidtgt={dagwithgraph=tryletmodify_arcs=letfilter(d,_)=OT.comparedtgt<>0inList.filterfilterarcsinNodeMap.modifyidmodifydag.graphwithNot_found->dag.graph}letdel_nodesdags={infos=NodeMap.filter(funn_->not(NodeSet.memns))dag.infos;properties=NodeMap.filter(funn_->not(NodeSet.memns))dag.properties;graph=NodeMap.filter(funnl->letdrop=NodeSet.memnsinifnotdropthenassert(List.for_all(fun(n',_)->not(NodeSet.memn's))l);notdrop)dag.graph}letmap_add_listkvm=tryletl=NodeMap.findkminNodeMap.addk(v::l)mwithNot_found->NodeMap.addk[v]mletclid=ref1letcreate_propertydagldata=incrclid;lethaving_it=List.fold_rightNodeSet.addlNodeSet.emptyinletproperty={Property.data;uid=!clid;having_it}in{dagwithproperties=List.fold_right(funxps->map_add_listxpropertyps)ldag.properties}letproperty_ofdagid=tryNodeMap.findiddag.propertieswithNot_found->[]letdel_propertydagc={dagwithproperties=NodeMap.filter(fun_cl->cl<>[])(NodeMap.map(funcl->List.filter(func'->not(Property.equalc'c))cl)dag.properties)}letget_infodagid=trySome(NodeMap.findiddag.infos)withNot_found->Noneletset_infodagidinfo={dagwithinfos=NodeMap.addidinfodag.infos}letclear_infodagid={dagwithinfos=NodeMap.removeiddag.infos}letiterdagf=NodeMap.iter(funkv->fk(property_ofdagk)(get_infodagk)v)dag.graphletall_nodesdag=NodeMap.domaindag.graphend