src/Tools/Metis/src/ElementSet.sml

removed obsolete Markup_Tree.flatten/filter;

(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)

functor ElementSet (Key : Ordered) :> ElementSet where type element = Key.t =
struct

(*isabelle open Metis;*)

type element = Key.t;

(* ------------------------------------------------------------------------- *)
(* Finite sets                                                               *)
(* ------------------------------------------------------------------------- *)

type set = Key.t Set.set;

val empty = Set.empty Key.compare;

fun singleton key = Set.singleton Key.compare key;

val null = Set.null;

val size = Set.size;

val member = Set.member;

val add = Set.add;

val addList = Set.addList;

val delete = Set.delete;

val union = Set.union;

val unionList = Set.unionList;

val intersect = Set.intersect;

val intersectList = Set.intersectList;

val difference = Set.difference;

val symmetricDifference = Set.symmetricDifference;

val disjoint = Set.disjoint;

val subset = Set.subset;

val equal = Set.equal;

val filter = Set.filter;

val partition = Set.partition;

val count = Set.count;

val foldl = Set.foldl;

val foldr = Set.foldr;

val findl = Set.findl;

val findr = Set.findr;

val firstl = Set.firstl;

val firstr = Set.firstr;

val exists = Set.exists;

val all = Set.all;

val map = Set.map;

val transform = Set.transform;

val app = Set.app;

val toList = Set.toList;

fun fromList l = Set.fromList Key.compare l;

val pick = Set.pick;

val random = Set.random;

val deletePick = Set.deletePick;

val deleteRandom = Set.deleteRandom;

val compare = Set.compare;

val close = Set.close;

val toString = Set.toString;

(* ------------------------------------------------------------------------- *)
(* Iterators over sets                                                       *)
(* ------------------------------------------------------------------------- *)

type iterator = Key.t Set.iterator;

val mkIterator = Set.mkIterator;

val mkRevIterator = Set.mkRevIterator;

val readIterator = Set.readIterator;

val advanceIterator = Set.advanceIterator;

end

(*isabelle structure Metis = struct open Metis;*)

structure IntSet =
ElementSet (IntOrdered);

structure StringSet =
ElementSet (StringOrdered);

(*isabelle end;*)