# HG changeset patch
# User atton
# Date 1479205993 -32400
# Node ID 19cc626943e41ddde504c3dfd30033dea440be0f
# Parent  efef5d4df54f8e2c197892a909bd12f7777f4481
stack.agda

diff -r efef5d4df54f -r 19cc626943e4 src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Tue Nov 15 19:02:36 2016 +0900
+++ b/src/parallel_execution/stack.agda	Tue Nov 15 19:33:13 2016 +0900
@@ -1,13 +1,34 @@
 module stack where
 
-pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> ?) -> ?
+record Stack {a : Set} (stackImpl : Set a) where
+  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;
+}
+
+
+record Element {a : Set} : Set where
+  data : a
+  next : Maybe (Element a)
+
+record SingleLinkedStack {a : Set} : Set where
+  top : Maybe (Element a)
+
+pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> T) -> T
 pushSingleLinkedStack stack data next = next stack1
   where
     element = record {next = top stack; data = data}
     stack1  = record {top = just element}
 
 
-popSingleLinkedStack : Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
+popSingleLinkedStack : {a : Set} -> Maybe a -> Data -> (Code : Stack -> (Maybe a) -> T) -> T
 popSingleLinkedStack stack data next with (top stack) =
   ... | nothing = next stack nothing
   ... | just a  = next stack1 data1