(*

Class:      Set
Package:    com.waysysweb
Author:     W. Shaffer
Date:       27-Oct-2005
Description:

    This structure

Maintenance:

Date        Author  Description
----------- ------  -----------------------------------------------------------
27-Oct-2005 Shaffer File created

*)

structure SET = struct

    (*============  Exceptions ==============================================*)

    exception SetException of string;

    (*============  Imports     =============================================*)



    (*============  Types       =============================================*)

    type ''a Set = ''a list;

    (*============  Constants  ==============================================*)

    val empty = [];

    (*============  Properties ==============================================*)



    (*============  Attributes  =============================================*)



    (*============  Invariant   =============================================*)



    (*============  Initialization ==========================================*)



    (*============  Operations  =============================================*)

    (* return true if set is empty                                           *)
    (* Precondition: true                                                    *)
    (* Postcondition: set = empty                                            *)
    fun isEmpty(set : ''a Set) : bool =
        if set = empty then true
        else false;

    (* return true if item is in set                                         *)
    (* Precondition: true                                                    *)
    (* Postcondition: if set = empty then false                              *)
    (*                else if item = hd(set) then true                       *)
    (*                else item inset tl(set)                                *)
    infix inset;
    fun ((item : ''a) inset (set : ''a Set) ) : bool  =
        if      isEmpty(set) then false
        else if item = hd(set) then true
        else    item inset tl(set);

    (* turn true if an item is not in the set                                *)
    (* Precondition: item : 'a andalso set : 'a Set                          *)
    (* Postcondition: not (item inset set)                                   *)
    infix notinset;
    fun ((item : ''a) notinset (set : ''a Set)) : bool = not (item inset set);

    (* return a set with an item added to it                                 *)
    (* Precondition:  not (item inset set)                                   *)
    (* Postcondition: set' = add(set, item) andalso item inset set'          *)
    fun add(set : ''a Set, item : ''a) : ''a Set =
        if item inset set then raise SetException("add: item is already in set")
        else item::set;

    (* return a set with an item removed                                     *)
    (* Precondition:  item inset set                                         *)
    (* Postcondition: remove(set, item) = set' andalso                       *)
    (*                not (item inset set)                                   *)
    fun remove(set : ''a Set, item : ''a) : ''a Set =
        if item inset set then
            let
                val first = hd(set)
            in
                if item = first then tl(set)
                else first::remove(set, item)
            end
        else raise SetException("remove: item is not in set");

    (* return true if if each element in a set satisfies the predicate       *)
    (* Precondition: true                                                    *)
    (* Postcondition: for all x inset set | pred(x)                          *)
    fun forall(set : ''a Set, pred : ''a -> bool) : bool =
        if set = empty then true
        else pred(hd(set)) andalso forall(tl(set), pred);

    (* return true if there exists an element that satisfies the predicate   *)
    (* Precondition: true                                                    *)
    (* Postcondition: there exists x inset set | pred(x)                     *)
    fun exists(set : ''a Set, pred : ''a -> bool) : bool =
        if set = empty then false
        else if pred(hd(set)) then true
        else exists(tl(set), pred);

    (* return the cardinality of the set or the number of items in set       *)
    (* Precondition: true                                                    *)
    (* Postcondition: size(empty) andalso                                    *)
    (*                size(add(set, item)) = size(set) + 1                   *)
    fun card(set : '' Set) : int = length(set);

    (* return a set of the elements in a list                                *)
    (* Precondition: true                                                    *)
    (* Postcondition: set = toSet(list') andalso                             *)
    (*                forall x in list1 | x inset set andalso                *)
    (*                forall(set, fn x : x in list)                          *)
    fun toSet([]                    ) : ''a Set = empty
    |   toSet(item::list' : ''a list) : ''a Set =
        let
           val set = toSet(list')
        in
            if item inset set then set
            else                   add(set, item)
        end;

    (* return one element of a set                                           *)
    (* Precondition: card(set) > 0                                           *)
    (* Postcondition: item = fetch(set) andalso item inset set               *)
    fun fetch(set : ''a Set) : ''a = hd(set);

    (* return the union of two sets                                          *)
    (* Precondition: true                                                    *)
    (* Postcondition: set' = union(set1, set2) andalso                       *)
    (*                forall(set1, fn x => x inset set')                     *)
    (*                forall(set2, fn x => x inset set')                     *)
    (*                forall(set',                                           *)
    (*                   fn x => (x inset set1) orelse (x inset set2)        *)
    fun union(set1 : ''a Set, set2 : ''a Set) : ''a Set =
        if set1 = empty then set2
        else
            let
                val item  = fetch(set1);
                val set1' = remove(set1, item);
                val set'  = union(set1', set2)
            in
                if item inset set' then set'
                else                    add(set', item)
            end;

    (* return the intersection of two sets                                   *)
    (* Precondition: true                                                    *)
    (* Postcondition: set' = inter(set1, set2) andalso                       *)
    (*                forall(set',                                           *)
    (*                    fn x => (x inset set1) andalso (x inset set2)      *)
    (*                forall(set1, fn x => if x inset set2 then x inset set' *)
    (*                                     else true)                        *)
    fun inter(set1 : ''a Set, set2 : ''a Set) : ''a Set =
        if set1 = empty then empty
        else
            let
                val item  = fetch(set1);
                val set1' = remove(set1, item);
                val set'  = inter(set1', set2)
            in
                if   (item inset set2) andalso (not (item inset set'))
                then add(set', item)
                else set'
            end;

    (* return true if sub is a subset of superset                            *)
    (* Precondition: true                                                    *)
    (* Postcondition: forall(sub, fn x => x inset superset)                  *)
    fun subset(sub : ''a Set, superset : ''a Set) : bool =
        forall(sub, fn x => x inset superset);

    (* return true if a set equals another set                               *)
    (* Precondition: true                                                    *)
    (* Postcondition: subset(set1, set2) andalso subset(set2, set1)          *)
    fun equals(set1 : ''a Set, set2 : ''a Set) : bool =
        subset(set1, set2) andalso subset(set2, set1);

    (* return a set of items that satisfy a predicate                        *)
    (* Precondition: true                                                   *)
    (* Postcondition: set' = select(set, pred) andalso                       *)
    (*                subset(set', set) andalso forall(set', pred)           *)
    fun select(set : ''a Set, pred : ''a -> bool) : ''a Set =
        if isEmpty(set) then empty
        else
            let
                val item = fetch(set);
                val set' = remove(set, item);
                val sel  = select(set', pred)
            in
                if pred(item) then add(sel, item)
                else sel
            end;

    (* return the set after applying a function to each element              *)
    (* Precondition: true                                                    *)
    (* Postcondition: set' = project(set, func) andalso                      *)
    (*                forall(set, fn x => func(x) inset set') andalso        *)
    (*                forall(set', fn x => exists(set, fn y => func(y) = x)) *)
    fun project(set : ''a Set, func : ''a -> ''b) : ''b Set =
        toSet(map func set);

    (* return a set of sets where each inner set contains item.              *)
    (* Precondition: setofSet : 'a Set Set andalso item : 'a andalso         *)
    (*               forall(setofSet, fn set => item notinset set)           *)
    fun addItem(setofSet : ''a Set Set, item : ''a) : ''a Set Set =
        if isEmpty(setofSet) then empty
        else
            let
                val aSet        = fetch(setofSet);
                val restSet     = remove(setofSet, aSet);
                val newSet      = add(aSet, item);
                val newSetofSet = addItem(restSet, item)
            in
                add(newSetofSet, newSet)
            end;

    (* return the powerset of a set                                          *)
    (* Precondition: set : ''a Set andalso                                   *)
    (*               powerset' = powerset(set) andalso                       *)
    (*               POWERSET : ''a Set Set is the powerset of set           *)
    fun powerset(set : ''a Set) : ''a Set Set =
        if isEmpty(set) then add(empty, empty)
        else
            let
                val item = fetch(set);
                val restSet = remove(set, item);
                val restPower = powerset(restSet)
            in
                union(restPower, addItem(restPower, item))
            end;

    (* create a set of integers in a range                                   *)
    fun range(first : int, last : int) : int Set =
        if first > last then empty
        else add(range(first + 1, last), first);

    (* return the largest integer in a range that satisifies a predicate     *)
    fun max(first : int, last : int, pred : int -> bool) : int =
        if      last < first then raise SetException("max: predicate is never true")
        else if pred(last)   then last
        else                      max(first, last-1, pred);

end (* SET *)