Mercurial > hg > Gears > GearsAgda

comparison src/parallel_execution/stack.agda @ 499:2c125aa7a577

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stack.agda leveled
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 09:34:46 +0900
parents 8e133a3938c0
children 6d984ea42fd2
comparison
equal deleted inserted replaced
498:01f0a2cdcc43 499:2c125aa7a577
1 open import Level renaming (suc to succ ) 1 open import Level renaming (suc to succ ; zero to Zero )
2 module stack where 2 module stack where
3 3
4 open import Relation.Binary.PropositionalEquality 4 open import Relation.Binary.PropositionalEquality
5 open import Relation.Binary.Core 5 open import Relation.Binary.Core
6 open import Data.Nat 6 open import Data.Nat
19 19
20 data Maybe {n : Level } (a : Set n) : Set n where 20 data Maybe {n : Level } (a : Set n) : Set n where
21 Nothing : Maybe a 21 Nothing : Maybe a
22 Just : a -> Maybe a 22 Just : a -> Maybe a
23 23
24 record Stack {n : Level } {a : Set n } {t : Set (succ n) }(stackImpl : Set n ) : Set (succ n ) where 24 record Stack {n m : Level } {a : Set n } {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) 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 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t 29 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
70 record SingleLinkedStack {n : Level } (a : Set n) : Set n where 70 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
71 field 71 field
72 top : Maybe (Element a) 72 top : Maybe (Element a)
73 open SingleLinkedStack 73 open SingleLinkedStack
74 74
75 pushSingleLinkedStack : {n : Level } {t : Set (succ n) } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t 75 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
76 pushSingleLinkedStack stack datum next = next stack1 76 pushSingleLinkedStack stack datum next = next stack1
77 where 77 where
78 element = cons datum (top stack) 78 element = cons datum (top stack)
79 stack1 = record {top = Just element} 79 stack1 = record {top = Just element}
80 80
81 81
82 popSingleLinkedStack : {n : Level } {t : Set (succ n) } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t 82 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
83 popSingleLinkedStack stack cs with (top stack) 83 popSingleLinkedStack stack cs with (top stack)
84 ... | Nothing = cs stack Nothing 84 ... | Nothing = cs stack Nothing
85 ... | Just d = cs stack1 (Just data1) 85 ... | Just d = cs stack1 (Just data1)
86 where 86 where
87 data1 = datum d 87 data1 = datum d
88 stack1 = record { top = (next d) } 88 stack1 = record { top = (next d) }
89 89
90 pop2SingleLinkedStack : {n : Level } {t : Set (succ n) } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t 90 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
91 pop2SingleLinkedStack {n} {t} {a} stack cs with (top stack) 91 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
92 ... | Nothing = cs stack Nothing Nothing 92 ... | Nothing = cs stack Nothing Nothing
93 ... | Just d = pop2SingleLinkedStack' stack cs 93 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
94 where 94 where
95 pop2SingleLinkedStack' : {n : Level } {t : Set (succ n) } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t 95 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
96 pop2SingleLinkedStack' stack cs with (next d) 96 pop2SingleLinkedStack' stack cs with (next d)
97 ... | Nothing = cs stack Nothing Nothing 97 ... | Nothing = cs stack Nothing Nothing
98 ... | Just d1 = cs (record {top = (next d)}) (Just (datum d)) (Just (datum d1)) 98 ... | Just d1 = cs (record {top = (next d)}) (Just (datum d)) (Just (datum d1))
99 99
100 100
101 getSingleLinkedStack : {n : Level } {t : Set (succ n) } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t 101 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
102 getSingleLinkedStack stack cs with (top stack) 102 getSingleLinkedStack stack cs with (top stack)
103 ... | Nothing = cs stack Nothing 103 ... | Nothing = cs stack Nothing
104 ... | Just d = cs stack (Just data1) 104 ... | Just d = cs stack (Just data1)
105 where 105 where
106 data1 = datum d 106 data1 = datum d
107 107
108 get2SingleLinkedStack : {n : Level } {t : Set (succ n) } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t 108 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
109 get2SingleLinkedStack {_} {t} {a} stack cs with (top stack) 109 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
110 ... | Nothing = cs stack Nothing Nothing 110 ... | Nothing = cs stack Nothing Nothing
111 ... | Just d = get2SingleLinkedStack' stack cs 111 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs
112 where 112 where
113 get2SingleLinkedStack' : {n : Level} {t : Set (succ n) } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t 113 get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
114 get2SingleLinkedStack' stack cs with (next d) 114 get2SingleLinkedStack' stack cs with (next d)
115 ... | Nothing = cs stack Nothing Nothing 115 ... | Nothing = cs stack Nothing Nothing
116 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1)) 116 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
117 117
118 118
119 119
120 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a 120 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
121 emptySingleLinkedStack = record {top = Nothing} 121 emptySingleLinkedStack = record {top = Nothing}
122 122
123 createSingleLinkedStack : {n : Level } {t : Set (succ n) } {a : Set n} -> Stack {n} {a} {t} (SingleLinkedStack a) 123 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
124 createSingleLinkedStack = record { stack = emptySingleLinkedStack 124 createSingleLinkedStack = record { stack = emptySingleLinkedStack
125 ; push = pushSingleLinkedStack 125 ; push = pushSingleLinkedStack
126 ; pop = popSingleLinkedStack 126 ; pop = popSingleLinkedStack
127 ; pop2 = pop2SingleLinkedStack 127 ; pop2 = pop2SingleLinkedStack
128 ; get = getSingleLinkedStack 128 ; get = getSingleLinkedStack
129 ; get2 = get2SingleLinkedStack 129 ; get2 = get2SingleLinkedStack
130 } 130 }
131 131
132 132
133 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool 133 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
134 test01 stack _ with (top stack) 134 test01 stack _ with (top stack)
135 ... | (Just _) = True 135 ... | (Just _) = True
136 ... | Nothing = False 136 ... | Nothing = False
137 137
138 138
140 test02 stack = popSingleLinkedStack stack test01 140 test02 stack = popSingleLinkedStack stack test01
141 141
142 test03 : {n : Level } {a : Set n} -> a -> Bool 142 test03 : {n : Level } {a : Set n} -> a -> Bool
143 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02 143 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
144 144
145 -- after a push and a pop, the stack is empty
146 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
147 lemma = refl
148
149 -- after push 1 and 2, pop2 get 1 and 2
150
145 testStack01 : {n : Level } {a : Set n} -> a -> Bool 151 testStack01 : {n : Level } {a : Set n} -> a -> Bool
146 testStack01 v = pushStack createSingleLinkedStack v ( 152 testStack01 v = pushStack createSingleLinkedStack v (
147 \s -> popStack s (\s1 d1 -> True)) 153 \s -> popStack s (\s1 d1 -> True))
148 154
149 testStack02 : (Stack (SingleLinkedStack ℕ) -> Bool) -> Bool 155 testStack02 : (Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
150 testStack02 cs = pushStack createSingleLinkedStack 1 ( 156 testStack02 cs = pushStack createSingleLinkedStack 1 (
151 \s -> pushStack s 2 cs) 157 \s -> pushStack s 2 cs)
152 158
153 159
154 testStack031 : (d1 d2 : ℕ ) -> Bool 160 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
155 testStack031 1 2 = True 161 testStack031 1 2 = True
156 testStack031 _ _ = False 162 testStack031 _ _ = False
157 163
158 testStack032 : (d1 d2 : Maybe ℕ) -> Bool 164 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
159 testStack032 (Just d1) (Just d2) = testStack031 d1 d2 165 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
160 testStack032 _ _ = False 166 testStack032 _ _ = False
161 167
162 testStack03 : Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool ) -> Bool 168 testStack03 : Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool ) -> Bool
163 testStack03 s cs = pop2Stack s ( 169 testStack03 s cs = pop2Stack s (
164 \s d1 d2 -> cs d1 d2 ) 170 \s d1 d2 -> cs d1 d2 )
165 171
166 testStack04 : Bool 172 testStack04 : Bool
167 testStack04 = testStack02 (\s -> testStack03 s testStack032) 173 testStack04 = testStack02 (\s -> testStack03 s testStack032)
168 174
169 testStack05 : { n : Level} -> Set n 175 testStack05 : Set (succ Zero)
170 testStack05 = {!!} -- testStack04 ≡ True 176 testStack05 = testStack04 ≡ True
171
172
173 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
174 lemma = refl
175 177
176 id : {n : Level} {A : Set n} -> A -> A 178 id : {n : Level} {A : Set n} -> A -> A
177 id a = a 179 id a = a
178 180
181 -- push a, n times
179 182
180 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A 183 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
181 n-push zero s = s 184 n-push zero s = s
182 n-push {_} {A} {a} (suc n) s = {!!} -- pushSingleLinkedStack (n-push {_} {A} {a} n s) a (\s -> ?) 185 n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s )
183 186
184 n-pop : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A 187 n-pop : {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
185 n-pop zero s = s 188 n-pop zero s = s
186 n-pop {_} {A} {a} (suc n) s = {!!} -- popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s) 189 n-pop {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
187 190
188 open ≡-Reasoning 191 open ≡-Reasoning
189 192
190 push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> {!!} -- popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s 193 push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
191 push-pop-equiv s = refl 194 push-pop-equiv s = refl
192 195
193 push-and-n-pop : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> {!!} -- n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s 196 push-and-n-pop : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {_} {A} {a} n s
194 push-and-n-pop zero s = refl 197 push-and-n-pop zero s = refl
195 push-and-n-pop {_} {A} {a} (suc n) s = begin 198 push-and-n-pop {_} {A} {a} (suc n) s = begin
196 {!!} -- n-pop {_} {n} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id) 199 n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
197 ≡⟨ refl ⟩ 200 ≡⟨ refl ⟩
198 {!!} -- popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) 201 popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
199 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> {!!})) (push-and-n-pop n s) ⟩ 202 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩
200 {!!} -- popSingleLinkedStack (n-pop {_} {n} {A} {a} n s) (\s _ -> s) 203 popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
201 ≡⟨ refl ⟩ 204 ≡⟨ refl ⟩
202 {!!} -- n-pop {_} {n} {A} {a} (suc n) s 205 n-pop {_} {A} {a} (suc n) s
203 ∎ 206 ∎
204 207
205 208
206 n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> {!!} -- (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s 209 n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {_} {A} {a} n (n-push {_} {A} {a} n s)) ≡ s
207 n-push-pop-equiv zero s = refl 210 n-push-pop-equiv zero s = refl
208 n-push-pop-equiv {A} {a} (suc n) s = begin 211 n-push-pop-equiv {_} {A} {a} (suc n) s = begin
209 n-pop {A} {a} (suc n) (n-push (suc n) s) 212 n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
210 ≡⟨ refl ⟩ 213 ≡⟨ refl ⟩
211 {!!} -- n-pop {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) 214 n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
212 ≡⟨ push-and-n-pop n (n-push n s) ⟩ 215 ≡⟨ push-and-n-pop n (n-push n s) ⟩
213 n-pop {A} {a} n (n-push n s) 216 n-pop {_} {A} {a} n (n-push n s)
214 ≡⟨ n-push-pop-equiv n s ⟩ 217 ≡⟨ n-push-pop-equiv n s ⟩
215 s 218 s
216 ∎ 219 ∎
217 220
218 221
219 n-push-pop-equiv-empty : {n : Level} {A : Set n} {a : A} -> (n : ℕ) -> n-pop {_} {A} {a} n (n-push {_} {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack 222 n-push-pop-equiv-empty : {n : Level} {A : Set n} {a : A} -> (n : ℕ) -> n-pop {_} {A} {a} n (n-push {_} {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack
220 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack 223 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack