--- a/src/parallel_execution/stack.agda	Fri Oct 06 19:48:42 2017 +0900
+++ b/src/parallel_execution/stack.agda	Sat Oct 07 18:22:31 2017 +0900
@@ -20,6 +20,13 @@
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
 
+pushStack : {a t : Set} -> Stack -> a -> (Stack -> t) -> t
+pushStack {a} {t} s0 d next = (stackImpl s0) (stack s0) d (\s1 -> next (record s0 {stack = s1;} ))
+
+popStack : {a t : Set} -> Stack -> (Stack -> t) -> t
+popStack {a} {t} s0  next = (stackImpl s0) (stack s0) (\s1 -> next s0)
+
+
 data Element (a : Set) : Set where
   cons : a -> Maybe (Element a) -> Element a