-- FILE: stack.mod

mod* ELEMENT { [Element] }

mod! STACKpre (X :: ELEMENT) {
 [ Stack ]
 op empty : -> Stack
 op push : Element Stack -> Stack 
 op pop_ : Stack -> Stack   
 op top_ : Stack -> Element 

 eq top push (E:Element, S:Stack) = E .	
 eq pop push (E:Element, S:Stack) = S . }

open (STACKpre + EQL)
ops e1 e2 : -> Element .
red top push(e2, pop pop push(e1,empty)) = e2 .
close

mod! STACK (X :: ELEMENT) {
 [ EmptyStack NonEmptyStack < Stack ]
 op empty : -> EmptyStack
 op push : Element Stack -> NonEmptyStack 
 op pop_ : NonEmptyStack -> Stack   
          -- only applicable to NonEmptyStack
 op top_ : NonEmptyStack -> Element 
          -- only applicable to NonEmptyStack

 eq top push (E:Element, S:Stack) = E .	
 eq pop push (E:Element, S:Stack) = S . }

open (STACK + EQL)
ops e1 e2 : -> Element .
red top push(e2, pop pop push(e1,empty)) = e2 .
close

set verbose on

select STACKpre
parse top push(e2:Element, pop pop push(e1:Element,empty))  .
red in STACKpre : top push(e2:Element, pop pop push(e1:Element,empty))  .

select STACK
parse top push(e2:Element, pop pop push(e1:Element,empty))  .
red in STACK : top push(e2:Element, pop pop push(e1:Element,empty))  .