# HG changeset patch
# User atton
# Date 1479407293 0
# Node ID b0c6e0392b00d46c97a03625b60c1fae32ba3d81
# Parent  f0c144c3861dc3c73ddf4902112fd94cdf02d39b
Add comment to stack.agda

diff -r f0c144c3861d -r b0c6e0392b00 src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Thu Nov 17 18:25:20 2016 +0000
+++ b/src/parallel_execution/stack.agda	Thu Nov 17 18:28:13 2016 +0000
@@ -5,7 +5,7 @@
 data Bool : Set where
   True  : Bool
   False : Bool
-  
+
 data Maybe (a : Set) : Set  where
   Nothing : Maybe a
   Just    : a -> Maybe a
@@ -26,15 +26,16 @@
 next (cons _ n) = n
 
 
-{-  
+{-
+-- cannot define recrusive record definition. so use linked list with maybe.
 record Element {l : Level} (a : Set l) : Set (suc l) where
   field
-    datum : a
+    datum : a  -- `data` is reserved by Agda.
     next : Maybe (Element a)
 -}
 
 
-  
+
 record SingleLinkedStack (a : Set) : Set where
   field
     top : Maybe (Element a)
@@ -44,8 +45,7 @@
 pushSingleLinkedStack stack datum next = next stack1
   where
     element = cons datum (top stack)
---    element = record {next = top stack; datum = datum}
-    stack1  = record {top = Just element} 
+    stack1  = record {top = Just element}
 
 
 popSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
@@ -60,7 +60,7 @@
 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
 emptySingleLinkedStack = record {top = Nothing}
 
-createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) 
+createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a)
 createSingleLinkedStack = record { stack = emptySingleLinkedStack
                                  ; push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
@@ -78,8 +78,8 @@
 test02 stack = (popSingleLinkedStack stack) test01
 
 test03 :  Bool
-test03 = pushSingleLinkedStack emptySingleLinkedStack (cons True Nothing) test02
---test03 = pushSingleLinkedStack emptySingleLinkedStack (False) test02
+test03 = pushSingleLinkedStack emptySingleLinkedStack (cons True Nothing) test02 -- ok
+--test03 = pushSingleLinkedStack emptySingleLinkedStack (False) test02 -- ok
 
 
 lemma : test03 ≡ False