src/Pure/General/stack.ML
author wenzelm
Tue, 13 Sep 2005 22:19:53 +0200
changeset 17368 e02adca07c31
child 17756 d4a35f82fbb4
permissions -rw-r--r--
Non-empty stacks.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17368
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/stack.ML
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     4
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     5
Non-empty stacks.
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     6
*)
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     7
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     8
signature STACK =
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
     9
sig
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    10
  type 'a T = 'a * 'a list
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    11
  val level: 'a T -> int
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    12
  val init: 'a -> 'a T
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    13
  val top: 'a T -> 'a
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    14
  val map: ('a -> 'a) -> 'a T -> 'a T
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    15
  val push: 'a T -> 'a T
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    16
  val pop: 'a T -> 'a T      (*exception Empty*)
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    17
end;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    18
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    19
structure Stack: STACK =
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    20
struct
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    21
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    22
type 'a T = 'a * 'a list;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    23
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    24
fun level (_, xs) = length xs;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    25
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    26
fun init x = (x, []);
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    27
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    28
fun top (x, _) = x;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    29
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    30
fun map f (x, xs) = (f x, xs);
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    31
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    32
fun push (x, xs) = (x, x :: xs);
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    33
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    34
fun pop (_, x :: xs) = (x, xs)
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    35
  | pop (_, []) = raise Empty;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    36
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    37
end;