record Stack {a t : Set} (stackImpl : Set) : Set  where
field
stack : stackImpl
push  : stackImpl -> a -> (stackImpl -> t) -> t
pop   : stackImpl -> (stackImpl -> Maybe a -> t) -> t
open Stack

pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t
pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} ))

popStack : {a t : Set} -> Stack a -> (Stack t -> t) -> t
popStack {a} {t} s0 next = (pop s0) (stack s0) (\s1 -> next s0)