--- a/src/parallel_execution/stack.agda	Mon Jan 01 18:58:05 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 19:14:09 2018 +0900
@@ -21,31 +21,31 @@
   Nothing : Maybe a
   Just    : a -> Maybe a
 
-record Stack {n m : Level } {a : Set n } {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+record StackMethods {n m : Level } {a : Set n } {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
   field
-    stack : stackImpl
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
     pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
     get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
     get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
-open Stack
-
-pushStack : {n m : Level } {t : Set m} {a si : Set n}  -> Stack si -> a -> (Stack si -> t) -> t
-pushStack s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
-
-popStack : {n m : Level } { t : Set m} {a si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
-popStack s0  next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
+open StackMethods
 
-pop2Stack : {n m : Level } { t : Set m} { a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
-pop2Stack s0 next = pop2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
+record Stack {n m : Level } {a : Set n } {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} {a} {t} si
+  pushStack :  a -> (Stack si -> t) -> t
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+  popStack : (Stack si -> Maybe a  -> t) -> t
+  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  pop2Stack :  (Stack si -> Maybe a -> Maybe a -> t) -> t
+  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  getStack :  (Stack si -> Maybe a  -> t) -> t
+  getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  get2Stack :  (Stack si -> Maybe a -> Maybe a -> t) -> t
+  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
 
-getStack : {n m : Level } {t : Set m} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
-getStack s0 next = get s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
-
-get2Stack : {n m : Level } {t : Set m} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
-get2Stack s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
-
+open Stack
 
 data Element {n : Level } (a : Set n) : Set n where
   cons : a -> Maybe (Element a) -> Element a
@@ -121,13 +121,16 @@
 emptySingleLinkedStack = record {top = Nothing}
 
 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
-createSingleLinkedStack = record { stack = emptySingleLinkedStack
-                                 ; push = pushSingleLinkedStack
+createSingleLinkedStack = record {
+                             stack = emptySingleLinkedStack ;
+                             stackMethods = record {
+                                   push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
                                  ; pop2 = pop2SingleLinkedStack
                                  ; get  = getSingleLinkedStack
                                  ; get2 = get2SingleLinkedStack
                                  }
+                           }
 
 
 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
@@ -176,6 +179,10 @@
 testStack05 = refl
 
 ------
+--
+-- this should be proved by properties of the stack inteface, not only by the implementation,
+--    and the implementation have to provides the properties.
+--
 -- push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : Stack (SingleLinkedStack D) ) ->
 --     pushStack s x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))))
 -- push->push->pop2 {l} {D} x y s = {!!}