Mercurial > hg > Gears > GearsAgda

changeset 483:9098ec0a9e6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
author ryokka
date Fri, 29 Dec 2017 11:07:18 +0900
parents 5859bed4edff
children 8a22cfd174bf da1dafcf1a45
files src/parallel_execution/stack.agda
diffstat 1 files changed, 38 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Fri Dec 29 04:42:44 2017 +0900
+++ b/src/parallel_execution/stack.agda	Fri Dec 29 11:07:18 2017 +0900
@@ -13,7 +13,7 @@
   False : Bool
 
 -- equal : {a : Set} -> a -> a -> Bool
--- equal x y with x ≡y
+-- equal x y with x ≡ y
 -- equal x .x | refl = True
 -- equal _ _ | _ = False
 
@@ -26,7 +26,8 @@
     stack : stackImpl
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-   
+    get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+    -- get2 : stackImpl -> (stackImpl -> (Maybe a -> Maybe a) -> t) -> t
 open Stack
 
 pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t
@@ -79,6 +80,40 @@
     data1  = datum d
     stack1 = record { top = (next d) }
 
+getSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+get2SingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = (getSingleLinkedStack2' stack cs)  Nothing
+  where
+    getSingleLinkedStack2' : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+    getSingleLinkedStack2' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing
+    ...              | Just d1 = cs stack (Just data1 data2)
+         where
+           data1 = datum d
+           data2 = datum d1
+
+
+-- get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+-- get2SingleLinkedStack stack cs with (top stack)
+-- ...                                | Nothing = cs stack  Nothing
+-- ...                                | Just d  = get2 cs stack
+--    where
+--      get2 : SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+--      get2 stack cs with (next d)
+-- ...                    | Nothing = cs stack Nothing
+-- ...                    | Just d d1 = cs stack (Just data1) (just data2)
+--                          where
+--                            data1  = datum d
+--                            data2  = datum d1
+
 
 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
 emptySingleLinkedStack = record {top = Nothing}
@@ -87,10 +122,10 @@
 createSingleLinkedStack = record { stack = emptySingleLinkedStack
                                  ; push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
+                                 ; get  = getSingleLinkedStack
                                  }
 
 
-
 test01 : {a : Set} -> SingleLinkedStack a -> Maybe a -> Bool
 test01 stack _ with (top stack)
 ...                  | (Just _) = True