Mercurial > hg > Gears > GearsAgda

changeset 164:b0c6e0392b00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add comment to stack.agda
author atton
date Thu, 17 Nov 2016 18:28:13 +0000
parents f0c144c3861d
children bf26f1105862
files src/parallel_execution/stack.agda
diffstat 1 files changed, 9 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- 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