Mercurial > hg > Gears > GearsAgda

comparison src/parallel_execution/stack.agda @ 501:55077dd40a51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stack.agda comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 18:32:20 +0900
parents 6d984ea42fd2
children 8d997f0c9b2c
comparison
equal deleted inserted replaced
500:6d984ea42fd2 501:55077dd40a51
6 open import Data.Nat 6 open import Data.Nat
7 7
8 ex : 1 + 2 ≡ 3 8 ex : 1 + 2 ≡ 3
9 ex = refl 9 ex = refl
10 10
11 data Bool {n : Level } : Set (succ n) where 11 data Bool {n : Level } : Set n where
12 True : Bool 12 True : Bool
13 False : Bool 13 False : Bool
14 14
15 record _∧_ {n : Level } {a b : Set n} : Set n where 15 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
16 field 16 field
17 pi1 : a 17 pi1 : a
18 pi2 : b 18 pi2 : b
19 19
20 data Maybe {n : Level } (a : Set n) : Set n where 20 data Maybe {n : Level } (a : Set n) : Set n where
29 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t 29 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
30 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t 30 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t
31 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t 31 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
32 open Stack 32 open Stack
33 33
34 pushStack : {n : Level } {t : Set (succ n)} {a si : Set n} -> Stack si -> a -> (Stack si -> t) -> t 34 pushStack : {n m : Level } {t : Set m} {a si : Set n} -> Stack si -> a -> (Stack si -> t) -> t
35 pushStack {t} {a} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} )) 35 pushStack s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
36 36
37 popStack : {n : Level } { t : Set (succ n)} {a si : Set n} -> Stack si -> (Stack si -> Maybe a -> t) -> t 37 popStack : {n m : Level } { t : Set m} {a si : Set n} -> Stack si -> (Stack si -> Maybe a -> t) -> t
38 popStack {t} {a} s0 next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 ) 38 popStack s0 next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
39 39
40 pop2Stack : {n : Level } { t : Set (succ n)} { a si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t 40 pop2Stack : {n m : Level } { t : Set m} { a si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
41 pop2Stack {t} {a} s0 next = pop2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2) 41 pop2Stack s0 next = pop2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
42 42
43 getStack : {n : Level } {t : Set (succ n)} {a si : Set n} -> Stack si -> (Stack si -> Maybe a -> t) -> t 43 getStack : {n m : Level } {t : Set m} {a si : Set n} -> Stack si -> (Stack si -> Maybe a -> t) -> t
44 getStack {t} {a} s0 next = get s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 ) 44 getStack s0 next = get s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
45 45
46 get2Stack : {n : Level } {t : Set (succ n)} {a si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t 46 get2Stack : {n m : Level } {t : Set m} {a si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
47 get2Stack {t} {a} s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2) 47 get2Stack s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
48 48
49 49
50 data Element {n : Level } (a : Set n) : Set n where 50 data Element {n : Level } (a : Set n) : Set n where
51 cons : a -> Maybe (Element a) -> Element a 51 cons : a -> Maybe (Element a) -> Element a
52 52
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 testStack01 : {n : Level } {a : Set n} -> a -> Bool 149 testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m}
150 testStack01 v = pushStack createSingleLinkedStack v ( 150 testStack01 v = pushStack createSingleLinkedStack v (
151 \s -> popStack s (\s1 d1 -> True)) 151 \s -> popStack s (\s1 d1 -> True))
152 152
153 -- after push 1 and 2, pop2 get 1 and 2 153 -- after push 1 and 2, pop2 get 1 and 2
154 154
155 testStack02 : ( Stack (SingleLinkedStack ℕ) -> Bool) -> Bool 155 testStack02 : {m : Level } -> ( Stack (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
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}
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
167 167
168 testStack03 : Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool ) -> Bool 168 testStack03 : {m : Level } -> Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
169 testStack03 s cs = pop2Stack s ( 169 testStack03 s cs = pop2Stack s (
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 : testStack04 ≡ True 175 testStack05 : testStack04 ≡ True
176 testStack05 = refl 176 testStack05 = refl
177
178 ------
179 -- push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : Stack (SingleLinkedStack D) ) ->
180 -- pushStack s x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))))
181 -- push->push->pop2 {l} {D} x y s = {!!}
182
177 183
178 id : {n : Level} {A : Set n} -> A -> A 184 id : {n : Level} {A : Set n} -> A -> A
179 id a = a 185 id a = a
180 186
181 -- push a, n times 187 -- push a, n times