--- a/src/Pure/General/stack.ML Tue Oct 28 09:32:18 2014 +0100
+++ b/src/Pure/General/stack.ML Tue Oct 28 09:57:12 2014 +0100
@@ -6,7 +6,9 @@
signature STACK =
sig
- type 'a T = 'a * 'a list
+ type 'a T
+ val make: 'a -> 'a list -> 'a T
+ val dest: 'a T -> 'a * 'a list
val level: 'a T -> int
val init: 'a -> 'a T
val top: 'a T -> 'a
@@ -19,21 +21,27 @@
structure Stack: STACK =
struct
-type 'a T = 'a * 'a list;
-
-fun level (_, xs) = length xs;
+abstype 'a T = Stack of 'a * 'a list
+with
-fun init x = (x, []);
+fun make x xs = Stack (x, xs);
+fun dest (Stack (x, xs)) = (x, xs);
-fun top (x, _) = x;
+fun level (Stack (_, xs)) = length xs;
+
+fun init x = Stack (x, []);
-fun map_top f (x, xs) = (f x, xs);
+fun top (Stack (x, _)) = x;
-fun map_all f (x, xs) = (f x, map f xs);
+fun map_top f (Stack (x, xs)) = Stack (f x, xs);
-fun push (x, xs) = (x, x :: xs);
+fun map_all f (Stack (x, xs)) = Stack (f x, map f xs);
-fun pop (_, x :: xs) = (x, xs)
- | pop (_, []) = raise List.Empty;
+fun push (Stack (x, xs)) = Stack (x, x :: xs);
+
+fun pop (Stack (_, x :: xs)) = Stack (x, xs)
+ | pop (Stack (_, [])) = raise List.Empty;
end;
+
+end;