(* set.sig *)

(* Copyright (C) 2006 Alley Stoughton

   This file is part of crypto, a cryptogram encoder/decoder.  See the
   file COPYING.txt for copying and usage restrictions *)

(* a set over a linear ordering *)

signature SET =
sig

structure LinOrd : LIN_ORD

type elem = LinOrd.elem

(* finite set of elem's *)

type set

(* the following functions always terminate, have no side-effects,
   and always return the same values when called with the same
   arguments *)

(* informally, memb(x, ys) tests whether x is a member of ys

   formally, memb's meaning is determined in relationship to the
   remaining functions *)

val memb : elem * set -> bool

(* subset(ys, zs) iff
   for all x : elem, if memb(x, ys), then memb(x, zs) *)

val subset : set * set -> bool

(* equal(ys, zs) iff
   for all x : elem,  memb(x, ys) iff memb(x, zs) *)

val equal : set * set -> bool

(* memb(y, fromList xs) iff
   List.exists (fn z => LinOrd.compare(z, y) = EQUAL) xs *)

val fromList : elem list -> set

(* List.exists (fn z => LinOrd.compare(z, y) = EQUAL) (toList xs) iff
   memb(y, xs)

   and

   isAscending(toList xs)

   where isAscending : elem list -> bool is defined by

   fun isAscending (x :: y :: zs) =
         LinOrd.compare(x, y) = LESS andalso isAscending(y :: zs)
     | isAscending _              = true *)

val toList : set -> elem list

(* size xs = length(toList xs) *)

val size : set -> int

(* memb(x, union(ys, zs)) iff memb(x, ys) or memb(x, zs) *)

val union : set * set -> set

(* memb(x, inter(ys, zs)) iff memb(x, ys) and memb(x, zs) *)

val inter : set * set -> set

(* memb(x, minus(ys, zs)) iff memb(x, ys) and not(memb(x, zs)) *)

val minus : set * set -> set

end;