Mercurial > hg > Members > Moririn

comparison src/parallel_execution/stack.agda @ 500:6d984ea42fd2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix proof
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 11:19:14 +0900
parents 2c125aa7a577
children 55077dd40a51
comparison
equal deleted inserted replaced
499:2c125aa7a577 500:6d984ea42fd2
144 144
145 -- after a push and a pop, the stack is empty 145 -- after a push and a pop, the stack is empty
146 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False 146 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
147 lemma = refl 147 lemma = refl
148 148
149 -- after push 1 and 2, pop2 get 1 and 2
150
151 testStack01 : {n : Level } {a : Set n} -> a -> Bool 149 testStack01 : {n : Level } {a : Set n} -> a -> Bool
152 testStack01 v = pushStack createSingleLinkedStack v ( 150 testStack01 v = pushStack createSingleLinkedStack v (
153 \s -> popStack s (\s1 d1 -> True)) 151 \s -> popStack s (\s1 d1 -> True))
154 152
155 testStack02 : (Stack (SingleLinkedStack ℕ) -> Bool) -> Bool 153 -- after push 1 and 2, pop2 get 1 and 2
154
155 testStack02 : ( Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
156 testStack02 cs = pushStack createSingleLinkedStack 1 ( 156 testStack02 cs = pushStack createSingleLinkedStack 1 (
157 \s -> pushStack s 2 cs) 157 \s -> pushStack s 2 cs)
158 158
159 159
160 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero} 160 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
161 testStack031 1 2 = True 161 testStack031 2 1 = True
162 testStack031 _ _ = False 162 testStack031 _ _ = False
163 163
164 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero} 164 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
165 testStack032 (Just d1) (Just d2) = testStack031 d1 d2 165 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
166 testStack032 _ _ = False 166 testStack032 _ _ = False
170 \s d1 d2 -> cs d1 d2 ) 170 \s d1 d2 -> cs d1 d2 )
171 171
172 testStack04 : Bool 172 testStack04 : Bool
173 testStack04 = testStack02 (\s -> testStack03 s testStack032) 173 testStack04 = testStack02 (\s -> testStack03 s testStack032)
174 174
175 testStack05 : Set (succ Zero) 175 testStack05 : testStack04 ≡ True
176 testStack05 = testStack04 ≡ True 176 testStack05 = refl
177 177
178 id : {n : Level} {A : Set n} -> A -> A 178 id : {n : Level} {A : Set n} -> A -> A
179 id a = a 179 id a = a
180 180
181 -- push a, n times 181 -- push a, n times