--- a/src/parallel_execution/stack.agda	Wed Nov 16 21:29:01 2016 +0900
+++ b/src/parallel_execution/stack.agda	Thu Nov 17 18:23:56 2016 +0000
@@ -1,51 +1,86 @@
 module stack where
 
-record Stack {a : Set} (stackImpl : Set a) where
-  stack : stackImpl
-  push : stackImpl -> a -> (stackImpl -> T) -> T
-  pop  : stackImpl -> (stackImpl -> maybe a -> T) -> T
+open import Relation.Binary.PropositionalEquality
+
+data Bool : Set where
+  True  : Bool
+  False : Bool
   
+data Maybe (a : Set) : Set  where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+
+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
 
-createSingleLinkedStack : Stack (SingleLinkedStack {a})
-createSingleLinkedStack = record { 
-  stack = record { top = nothing;}
-  push  = pushSingleLinkedStack;
-  pop   = popSingleLinkedStack;
-}
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+
+{-  
+record Element {l : Level} (a : Set l) : Set (suc l) where
+  field
+    datum : a
+    next : Maybe (Element a)
+-}
 
 
-record Element {a : Set} : Set where
-  data : a
-  next : Maybe (Element a)
+  
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
 
-record SingleLinkedStack {a : Set} : Set where
-  top : Maybe (Element a)
+pushSingleLinkedStack : {Data t : Set} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+--    element = record {next = top stack; datum = datum}
+    stack1  = record {top = Just element} 
+
 
-pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> T) -> T
-pushSingleLinkedStack stack data next = next stack1
+popSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
   where
-    element = record {next = top stack; data = data}
-    stack1  = record {top = just element}
+    data1  = datum d
+    stack1 = record { top = (next d) }
 
 
-popSingleLinkedStack : {a : Set} -> Stack -> (Code : Stack -> (Maybe a) -> T) -> T
-popSingleLinkedStack stack next with (top  stack) =
-  ... | nothing = next stack nothing
-  ... | just d  = next stack1 data1
-    where
-      data1 = data d
-      stack1 = record { top = (next d)}
+emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
+emptySingleLinkedStack = record {top = Nothing}
+
+createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) 
+createSingleLinkedStack = record { stack = emptySingleLinkedStack
+                                 ; push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 }
+
 
 
-test01 : Stack -> Maybe a -> T
-test01 stack nothing  = false
-test01 stack (just _) = true
+test01 : {a : Set} -> SingleLinkedStack a -> Maybe a -> Bool
+test01 stack _ with (top stack)
+...                  | (Just _) = True
+...                  | Nothing  = False
+
 
-test02 : Stack -> T
-test02 stack = (pop stack) test01
+test02 : {a : Set} -> SingleLinkedStack a -> Bool
+test02 stack = (popSingleLinkedStack stack) test01
 
-test03 : T
-test03 = push createSingleLinkedStack true test02
+test03 :  Bool
+test03 = pushSingleLinkedStack emptySingleLinkedStack (cons True Nothing) test02
+--test03 = pushSingleLinkedStack emptySingleLinkedStack (False) test02
 
-lemma : test01 == false
+
+lemma : test03 ≡ False
 lemma = refl