src/Pure/General/stack.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 21272 a87b27cdd142
child 28129 8f647d24b49f
permissions -rw-r--r--
filtering out some package theorems
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
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17368
diff changeset
    10
  type 'a T (*= 'a * 'a list*)
17368
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
21272
a87b27cdd142 separate map_top/all;
wenzelm
parents: 17756
diff changeset
    14
  val map_top: ('a -> 'a) -> 'a T -> 'a T
a87b27cdd142 separate map_top/all;
wenzelm
parents: 17756
diff changeset
    15
  val map_all: ('a -> 'a) -> 'a T -> 'a T
17368
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    16
  val push: 'a T -> 'a T
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    17
  val pop: 'a T -> 'a T      (*exception Empty*)
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    18
end;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    19
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    20
structure Stack: STACK =
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    21
struct
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    22
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    23
type 'a T = 'a * 'a list;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    24
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    25
fun level (_, xs) = length xs;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    26
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    27
fun init x = (x, []);
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    28
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    29
fun top (x, _) = x;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    30
21272
a87b27cdd142 separate map_top/all;
wenzelm
parents: 17756
diff changeset
    31
fun map_top f (x, xs) = (f x, xs);
a87b27cdd142 separate map_top/all;
wenzelm
parents: 17756
diff changeset
    32
a87b27cdd142 separate map_top/all;
wenzelm
parents: 17756
diff changeset
    33
fun map_all f (x, xs) = (f x, map f xs);
17368
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    34
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    35
fun push (x, xs) = (x, x :: xs);
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    36
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    37
fun pop (_, x :: xs) = (x, xs)
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    38
  | pop (_, []) = raise Empty;
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    39
e02adca07c31 Non-empty stacks.
wenzelm
parents:
diff changeset
    40
end;