Mercurial > hg > GearsTemplate

comparison src/parallel_execution/stack.agda @ 590:9146d6017f18 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hg mv parallel_execution/* ..
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 16 Jan 2020 15:12:06 +0900
parents a4cab67624f7
children
comparison
equal deleted inserted replaced
589:a4cab67624f7 590:9146d6017f18
1 open import Level renaming (suc to succ ; zero to Zero )
2 module stack where
3
4 open import Relation.Binary.PropositionalEquality
5 open import Relation.Binary.Core
6 open import Data.Nat
7
8 ex : 1 + 2 ≡ 3
9 ex = refl
10
11 data Bool {n : Level } : Set n where
12 True : Bool
13 False : Bool
14
15 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
16 field
17 pi1 : a
18 pi2 : b
19
20 data Maybe {n : Level } (a : Set n) : Set n where
21 Nothing : Maybe a
22 Just : a -> Maybe a
23
24 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
25 field
26 push : stackImpl -> a -> (stackImpl -> t) -> t
27 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
28 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
29 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t
30 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
31 open StackMethods
32
33 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
34 field
35 stack : si
36 stackMethods : StackMethods {n} {m} a {t} si
37 pushStack : a -> (Stack a si -> t) -> t
38 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
39 popStack : (Stack a si -> Maybe a -> t) -> t
40 popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
41 pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
42 pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
43 getStack : (Stack a si -> Maybe a -> t) -> t
44 getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
45 get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
46 get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
47
48 open Stack
49
50 data Element {n : Level } (a : Set n) : Set n where
51 cons : a -> Maybe (Element a) -> Element a
52
53 datum : {n : Level } {a : Set n} -> Element a -> a
54 datum (cons a _) = a
55
56 next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
57 next (cons _ n) = n
58
59
60 {-
61 -- cannot define recrusive record definition. so use linked list with maybe.
62 record Element {l : Level} (a : Set n l) : Set n (suc l) where
63 field
64 datum : a -- `data` is reserved by Agda.
65 next : Maybe (Element a)
66 -}
67
68
69
70 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
71 field
72 top : Maybe (Element a)
73 open SingleLinkedStack
74
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
77 where
78 element = cons datum (top stack)
79 stack1 = record {top = Just element}
80
81
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)
84 ... | Nothing = cs stack Nothing
85 ... | Just d = cs stack1 (Just data1)
86 where
87 data1 = datum d
88 stack1 = record { top = (next d) }
89
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} {m} {t} {a} stack cs with (top stack)
92 ... | Nothing = cs stack Nothing Nothing
93 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
94 where
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)
97 ... | Nothing = cs stack Nothing Nothing
98 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
99
100
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)
103 ... | Nothing = cs stack Nothing
104 ... | Just d = cs stack (Just data1)
105 where
106 data1 = datum d
107
108 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
109 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
110 ... | Nothing = cs stack Nothing Nothing
111 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs
112 where
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)
115 ... | Nothing = cs stack Nothing Nothing
116 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
117
118
119
120 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
121 emptySingleLinkedStack = record {top = Nothing}
122
123 -----
124 -- Basic stack implementations are specifications of a Stack
125 --
126 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
127 singleLinkedStackSpec = record {
128 push = pushSingleLinkedStack
129 ; pop = popSingleLinkedStack
130 ; pop2 = pop2SingleLinkedStack
131 ; get = getSingleLinkedStack
132 ; get2 = get2SingleLinkedStack
133 }
134
135 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
136 createSingleLinkedStack = record {
137 stack = emptySingleLinkedStack ;
138 stackMethods = singleLinkedStackSpec
139 }
140
141 ----
142 --
143 -- proof of properties ( concrete cases )
144 --
145
146 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
147 test01 stack _ with (top stack)
148 ... | (Just _) = True
149 ... | Nothing = False
150
151
152 test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool
153 test02 stack = popSingleLinkedStack stack test01
154
155 test03 : {n : Level } {a : Set n} -> a -> Bool
156 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
157
158 -- after a push and a pop, the stack is empty
159 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
160 lemma = refl
161
162 testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m}
163 testStack01 v = pushStack createSingleLinkedStack v (
164 \s -> popStack s (\s1 d1 -> True))
165
166 -- after push 1 and 2, pop2 get 1 and 2
167
168 testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
169 testStack02 cs = pushStack createSingleLinkedStack 1 (
170 \s -> pushStack s 2 cs)
171
172
173 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
174 testStack031 2 1 = True
175 testStack031 _ _ = False
176
177 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
178 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
179 testStack032 _ _ = False
180
181 testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
182 testStack03 s cs = pop2Stack s (
183 \s d1 d2 -> cs d1 d2 )
184
185 testStack04 : Bool
186 testStack04 = testStack02 (\s -> testStack03 s testStack032)
187
188 testStack05 : testStack04 ≡ True
189 testStack05 = refl
190
191 ------
192 --
193 -- proof of properties with indefinite state of stack
194 --
195 -- this should be proved by properties of the stack inteface, not only by the implementation,
196 -- and the implementation have to provides the properties.
197 --
198 -- we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok.
199 -- anyway some implementations may result s != s3
200 --
201
202 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t} ( SingleLinkedStack D )
203 stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec }
204
205 push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
206 pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
207 push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
208
209
210 id : {n : Level} {A : Set n} -> A -> A
211 id a = a
212
213 -- push a, n times
214
215 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
216 n-push zero s = s
217 n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s )
218
219 n-pop : {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
220 n-pop zero s = s
221 n-pop {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
222
223 open ≡-Reasoning
224
225 push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
226 push-pop-equiv s = refl
227
228 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
229 push-and-n-pop zero s = refl
230 push-and-n-pop {_} {A} {a} (suc n) s = begin
231 n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
232 ≡⟨ refl ⟩
233 popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
234 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩
235 popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
236 ≡⟨ refl ⟩
237 n-pop {_} {A} {a} (suc n) s
238 ∎
239
240
241 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
242 n-push-pop-equiv zero s = refl
243 n-push-pop-equiv {_} {A} {a} (suc n) s = begin
244 n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
245 ≡⟨ refl ⟩
246 n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
247 ≡⟨ push-and-n-pop n (n-push n s) ⟩
248 n-pop {_} {A} {a} n (n-push n s)
249 ≡⟨ n-push-pop-equiv n s ⟩
250 s
251 ∎
252
253
254 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
255 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack