1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071(* elpi: embedded lambda prolog interpreter *)(* license: GNU Lesser General Public License Version 2.1 or later *)(* ------------------------------------------------------------------------- *)moduletypeS=sigincludeUtil.ShowincludeUtil.ShowKeymoduleKeySet:Util.Set.Swithtypeelt=keyvalempty:tvalis_empty:t->boolvalfind:t->key->keyvalfind_class:t->key->key*KeySet.tvalunion:t->key->canon:key->keyoption*tvalmerge:t->t->tvalroots:t->KeySet.tvalmapi:(key->key)->t->tendmoduleMake(O:Util.Map.OrderedType):Swithtypekey=O.t=structmoduleM=Util.Map.Make(O)moduleKeySet=Util.Set.Make(O)typekey=M.key[@@derivingshow]typet=(key*KeySet.t)M.t[@@derivingshow]letempty=M.emptyletis_empty=(=)M.emptyletrecfindmv=matchM.find_optvmwith|None->v|Some(e,_)->findmeletrecfind_classmvs=matchM.find_optvmwith|None->v,KeySet.addvs|Some(e,s1)->find_classme(KeySet.adde(KeySet.unions1s))letfind_classmv=find_classmvKeySet.emptyletunionmi~canon:j=(* assert ( i <> j ); *)letri,si=find_classmiinletrj,sj=find_classmjin(* ri is put in the same disjoint set of rj and can be removed from other
data structures *)ifO.comparerirj!=0then(Someri,M.addri(rj,KeySet.unionsisj)m)else(None,m)letmergeu1u2=(* all disjoint-set in u1 and u2 should be pairwise disjoint *)M.union(fun_(a,sa)(_,sb)->Some(a,KeySet.unionsasb))u1u2(* M.fold (fun k father acc ->
let acc = if M.mem father acc then assert false else add acc father in
union acc k father
) u1 u2 *)letmapift=M.fold(funk(v,s)acc->M.add(fk)(fv,KeySet.mapfs)acc)M.emptytletrootsd=letroots=refKeySet.emptyinletadde=ifnot(KeySet.meme!roots)thenroots:=KeySet.adde!rootsinM.iter(funkv->add(finddk))d;!rootsletppfmtv=Format.fprintffmt"{{\n";M.iter(funk(v,cl)->ifO.comparekv!=0thenFormat.fprintffmt"@[%a -> %a@]\n"M.pp_keykM.pp_keyv)v;Format.fprintffmt"}}@."letpp_key=M.pp_keyend