Mercurial > hg > Gears > GearsAgda

comparison src/parallel_execution/stack.agda @ 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 0223c07c3946
children 8a22cfd174bf
comparison
equal deleted inserted replaced
482:5859bed4edff 483:9098ec0a9e6b
11 data Bool : Set where 11 data Bool : Set where
12 True : Bool 12 True : Bool
13 False : Bool 13 False : Bool
14 14
15 -- equal : {a : Set} -> a -> a -> Bool 15 -- equal : {a : Set} -> a -> a -> Bool
16 -- equal x y with x ≡y 16 -- equal x y with x ≡ y
17 -- equal x .x | refl = True 17 -- equal x .x | refl = True
18 -- equal _ _ | _ = False 18 -- equal _ _ | _ = False
19 19
20 data Maybe (a : Set) : Set where 20 data Maybe (a : Set) : Set where
21 Nothing : Maybe a 21 Nothing : Maybe a
24 record Stack {a t : Set} (stackImpl : Set) : Set where 24 record Stack {a t : Set} (stackImpl : Set) : Set where
25 field 25 field
26 stack : stackImpl 26 stack : stackImpl
27 push : stackImpl -> a -> (stackImpl -> t) -> t 27 push : stackImpl -> a -> (stackImpl -> t) -> t
28 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t 28 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
29 29 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t
30 -- get2 : stackImpl -> (stackImpl -> (Maybe a -> Maybe a) -> t) -> t
30 open Stack 31 open Stack
31 32
32 pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t 33 pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t
33 pushStack {a} {t} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} )) 34 pushStack {a} {t} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
34 35
77 ... | Just d = cs stack1 (Just data1) 78 ... | Just d = cs stack1 (Just data1)
78 where 79 where
79 data1 = datum d 80 data1 = datum d
80 stack1 = record { top = (next d) } 81 stack1 = record { top = (next d) }
81 82
83 getSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
84 getSingleLinkedStack stack cs with (top stack)
85 ... | Nothing = cs stack Nothing
86 ... | Just d = cs stack (Just data1)
87 where
88 data1 = datum d
89
90 get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
91 get2SingleLinkedStack stack cs with (top stack)
92 ... | Nothing = cs stack Nothing Nothing
93 ... | Just d = (getSingleLinkedStack2' stack cs) Nothing
94 where
95 getSingleLinkedStack2' : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
96 getSingleLinkedStack2' stack cs with (next d)
97 ... | Nothing = cs stack Nothing
98 ... | Just d1 = cs stack (Just data1 data2)
99 where
100 data1 = datum d
101 data2 = datum d1
102
103
104 -- get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
105 -- get2SingleLinkedStack stack cs with (top stack)
106 -- ... | Nothing = cs stack Nothing
107 -- ... | Just d = get2 cs stack
108 -- where
109 -- get2 : SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
110 -- get2 stack cs with (next d)
111 -- ... | Nothing = cs stack Nothing
112 -- ... | Just d d1 = cs stack (Just data1) (just data2)
113 -- where
114 -- data1 = datum d
115 -- data2 = datum d1
116
82 117
83 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a 118 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
84 emptySingleLinkedStack = record {top = Nothing} 119 emptySingleLinkedStack = record {top = Nothing}
85 120
86 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) 121 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a)
87 createSingleLinkedStack = record { stack = emptySingleLinkedStack 122 createSingleLinkedStack = record { stack = emptySingleLinkedStack
88 ; push = pushSingleLinkedStack 123 ; push = pushSingleLinkedStack
89 ; pop = popSingleLinkedStack 124 ; pop = popSingleLinkedStack
125 ; get = getSingleLinkedStack
90 } 126 }
91
92 127
93 128
94 test01 : {a : Set} -> SingleLinkedStack a -> Maybe a -> Bool 129 test01 : {a : Set} -> SingleLinkedStack a -> Maybe a -> Bool
95 test01 stack _ with (top stack) 130 test01 stack _ with (top stack)
96 ... | (Just _) = True 131 ... | (Just _) = True