equal
deleted
inserted
replaced
|
1 (* Title: Pure/General/stack.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 Non-empty stacks. |
|
6 *) |
|
7 |
|
8 signature STACK = |
|
9 sig |
|
10 type 'a T = 'a * 'a list |
|
11 val level: 'a T -> int |
|
12 val init: 'a -> 'a T |
|
13 val top: 'a T -> 'a |
|
14 val map: ('a -> 'a) -> 'a T -> 'a T |
|
15 val push: 'a T -> 'a T |
|
16 val pop: 'a T -> 'a T (*exception Empty*) |
|
17 end; |
|
18 |
|
19 structure Stack: STACK = |
|
20 struct |
|
21 |
|
22 type 'a T = 'a * 'a list; |
|
23 |
|
24 fun level (_, xs) = length xs; |
|
25 |
|
26 fun init x = (x, []); |
|
27 |
|
28 fun top (x, _) = x; |
|
29 |
|
30 fun map f (x, xs) = (f x, xs); |
|
31 |
|
32 fun push (x, xs) = (x, x :: xs); |
|
33 |
|
34 fun pop (_, x :: xs) = (x, xs) |
|
35 | pop (_, []) = raise Empty; |
|
36 |
|
37 end; |