HELP STACK                                       Robert Duncan, Nov 1989

Simple push-down lists.


    CONTENTS - (Use <ENTER> g to access required sections)

 -- The Stack Module
 -- Summary of Definitions


-- The Stack Module ---------------------------------------------------

signature Stack
structure Stack : Stack
    The structure -Stack-  is an  autoloadable library  module with  the
    following signature:

        signature Stack = sig

            datatype 'a stack =
                NIL
            |   PUSH of 'a * 'a stack

            exception Pop
            exception Top

            val nilstack    : 'a stack
            val push        : 'a * 'a stack -> 'a stack
            val pop         : 'a stack -> 'a * 'a stack
            val top         : 'a stack -> 'a
            val isempty     : 'a stack -> bool

        end;    (* signature Stack *)


-- Summary of Definitions ---------------------------------------------

datatype 'a stack
con NIL
con PUSH (x : 'a, s : 'a stack)
    The type of  stacks. Stacks  are constructed from  the empty  stack,
    -NIL-, and the constructor -PUSH- which pushes the item -x- onto the
    stack -s-.


val nilstack : 'a stack
val push (x : 'a, s : 'a stack) : 'a stack
    Synonyms for the constructors -NIL- and -PUSH-.


exception Pop
val pop (s : 'a stack) : 'a * 'a stack
    Pops the top item from  the stack -s-. The result  is a pair of  the
    item and the rest of the stack. The exception -Pop- is raised if -s-
    is the empty stack.

    The functions -push- and -pop- obey the identities:

        push(pop(s))   = s,     for all non-empty s
        pop(push(x,s)) = (x,s), for all x,s


exception Top
val top (s : 'a stack) : 'a
    Returns the top  item from  the stack  -s-. The  exception -Top-  is
    raised if -s- is the empty stack.

    The functions -push- and -top- obey the identity:

        top(push(x,s)) = x,     for all x,s


val isempty (s : 'a stack) : bool
    Returns -true- if -s-  is the empty stack.  Use of this function  is
    recommended rather than comparing -s-  directly against -NIL- as  it
    does not constrain the type of items on the stack to be an  equality
    type.


--- C.all/pml/help/stack
--- Copyright University of Sussex 1991. All rights reserved. ----------