src/Tools/Metis/src/ElementSet.sig

The Metis prover (slightly modified version from Larry);

(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
(* ========================================================================= *)

signature ElementSet =
sig

type element

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

type set

val empty : set

val singleton : element -> set

val null : set -> bool

val size : set -> int

val member : element -> set -> bool

val add : set -> element -> set

val addList : set -> element list -> set

val delete : set -> element -> set  (* raises Error *)

(* Union and intersect prefer elements in the second set *)

val union : set -> set -> set

val unionList : set list -> set

val intersect : set -> set -> set

val intersectList : set list -> set

val difference : set -> set -> set

val symmetricDifference : set -> set -> set

val disjoint : set -> set -> bool

val subset : set -> set -> bool

val equal : set -> set -> bool

val filter : (element -> bool) -> set -> set

val partition : (element -> bool) -> set -> set * set

val count : (element -> bool) -> set -> int

val foldl : (element * 's -> 's) -> 's -> set -> 's

val foldr : (element * 's -> 's) -> 's -> set -> 's

val findl : (element -> bool) -> set -> element option

val findr : (element -> bool) -> set -> element option

val firstl : (element -> 'a option) -> set -> 'a option

val firstr : (element -> 'a option) -> set -> 'a option

val exists : (element -> bool) -> set -> bool

val all : (element -> bool) -> set -> bool

val map : (element -> 'a) -> set -> (element * 'a) list

val transform : (element -> 'a) -> set -> 'a list

val app : (element -> unit) -> set -> unit

val toList : set -> element list

val fromList : element list -> set

val pick : set -> element  (* raises Empty *)

val random : set -> element  (* raises Empty *)

val deletePick : set -> element * set  (* raises Empty *)

val deleteRandom : set -> element * set  (* raises Empty *)

val compare : set * set -> order

val close : (set -> set) -> set -> set

val toString : set -> string

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

type iterator

val mkIterator : set -> iterator option

val mkRevIterator : set -> iterator option

val readIterator : iterator -> element

val advanceIterator : iterator -> iterator option

end