Mercurial > hg > Gears > GearsAgda
annotate src/parallel_execution/stack.agda @ 483:9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
author | ryokka |
---|---|
date | Fri, 29 Dec 2017 11:07:18 +0900 (2017-12-29) |
parents | 0223c07c3946 |
children | 8a22cfd174bf |
rev | line source |
---|---|
154 | 1 module stack where |
2 | |
161 | 3 open import Relation.Binary.PropositionalEquality |
477 | 4 open import Relation.Binary.Core |
161 | 5 |
478 | 6 |
179 | 7 data Nat : Set where |
8 zero : Nat | |
9 suc : Nat -> Nat | |
10 | |
161 | 11 data Bool : Set where |
12 True : Bool | |
13 False : Bool | |
164 | 14 |
477 | 15 -- equal : {a : Set} -> a -> a -> Bool |
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
16 -- equal x y with x ≡ y |
477 | 17 -- equal x .x | refl = True |
18 -- equal _ _ | _ = False | |
19 | |
161 | 20 data Maybe (a : Set) : Set where |
21 Nothing : Maybe a | |
22 Just : a -> Maybe a | |
23 | |
24 record Stack {a t : Set} (stackImpl : Set) : Set where | |
25 field | |
26 stack : stackImpl | |
27 push : stackImpl -> a -> (stackImpl -> t) -> t | |
28 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t | |
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
29 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
30 -- get2 : stackImpl -> (stackImpl -> (Maybe a -> Maybe a) -> t) -> t |
477 | 31 open Stack |
427 | 32 |
477 | 33 pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t |
34 pushStack {a} {t} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} )) | |
35 | |
36 popStack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a -> t) -> t | |
37 popStack {a} {t} s0 next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 ) | |
427 | 38 |
478 | 39 -- get : {a t si : Set} -> Stack si -> (Stack si -> t) -> t |
40 -- get {a} {t} s0 next = pop s0 (stack s0) (\s1 -> next (record s0 {})) | |
41 | |
427 | 42 |
161 | 43 data Element (a : Set) : Set where |
44 cons : a -> Maybe (Element a) -> Element a | |
45 | |
46 datum : {a : Set} -> Element a -> a | |
47 datum (cons a _) = a | |
48 | |
49 next : {a : Set} -> Element a -> Maybe (Element a) | |
50 next (cons _ n) = n | |
51 | |
52 | |
164 | 53 {- |
54 -- cannot define recrusive record definition. so use linked list with maybe. | |
161 | 55 record Element {l : Level} (a : Set l) : Set (suc l) where |
56 field | |
164 | 57 datum : a -- `data` is reserved by Agda. |
161 | 58 next : Maybe (Element a) |
59 -} | |
155 | 60 |
61 | |
164 | 62 |
161 | 63 record SingleLinkedStack (a : Set) : Set where |
64 field | |
65 top : Maybe (Element a) | |
66 open SingleLinkedStack | |
155 | 67 |
161 | 68 pushSingleLinkedStack : {Data t : Set} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t |
69 pushSingleLinkedStack stack datum next = next stack1 | |
70 where | |
71 element = cons datum (top stack) | |
164 | 72 stack1 = record {top = Just element} |
161 | 73 |
155 | 74 |
161 | 75 popSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
76 popSingleLinkedStack stack cs with (top stack) | |
77 ... | Nothing = cs stack Nothing | |
78 ... | Just d = cs stack1 (Just data1) | |
154 | 79 where |
161 | 80 data1 = datum d |
81 stack1 = record { top = (next d) } | |
154 | 82 |
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
83 getSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
84 getSingleLinkedStack stack cs with (top stack) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
85 ... | Nothing = cs stack Nothing |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
86 ... | Just d = cs stack (Just data1) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
87 where |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
88 data1 = datum d |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
89 |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
90 get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
91 get2SingleLinkedStack stack cs with (top stack) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
92 ... | Nothing = cs stack Nothing Nothing |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
93 ... | Just d = (getSingleLinkedStack2' stack cs) Nothing |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
94 where |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
95 getSingleLinkedStack2' : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
96 getSingleLinkedStack2' stack cs with (next d) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
97 ... | Nothing = cs stack Nothing |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
98 ... | Just d1 = cs stack (Just data1 data2) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
99 where |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
100 data1 = datum d |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
101 data2 = datum d1 |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
102 |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
103 |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
104 -- get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
105 -- get2SingleLinkedStack stack cs with (top stack) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
106 -- ... | Nothing = cs stack Nothing |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
107 -- ... | Just d = get2 cs stack |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
108 -- where |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
109 -- get2 : SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
110 -- get2 stack cs with (next d) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
111 -- ... | Nothing = cs stack Nothing |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
112 -- ... | Just d d1 = cs stack (Just data1) (just data2) |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
113 -- where |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
114 -- data1 = datum d |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
115 -- data2 = datum d1 |
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
116 |
154 | 117 |
161 | 118 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a |
119 emptySingleLinkedStack = record {top = Nothing} | |
120 | |
164 | 121 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) |
161 | 122 createSingleLinkedStack = record { stack = emptySingleLinkedStack |
123 ; push = pushSingleLinkedStack | |
124 ; pop = popSingleLinkedStack | |
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
125 ; get = getSingleLinkedStack |
161 | 126 } |
127 | |
156 | 128 |
161 | 129 test01 : {a : Set} -> SingleLinkedStack a -> Maybe a -> Bool |
130 test01 stack _ with (top stack) | |
131 ... | (Just _) = True | |
132 ... | Nothing = False | |
133 | |
156 | 134 |
161 | 135 test02 : {a : Set} -> SingleLinkedStack a -> Bool |
136 test02 stack = (popSingleLinkedStack stack) test01 | |
156 | 137 |
165 | 138 test03 : {a : Set} -> a -> Bool |
139 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02 | |
156 | 140 |
477 | 141 testStack01 : {a : Set} -> a -> Bool |
142 testStack01 v = pushStack createSingleLinkedStack v ( | |
143 \s -> popStack s (\s1 d1 -> True)) | |
144 | |
145 | |
161 | 146 |
165 | 147 lemma : {A : Set} {a : A} -> test03 a ≡ False |
158 | 148 lemma = refl |
179 | 149 |
150 id : {A : Set} -> A -> A | |
151 id a = a | |
152 | |
153 | |
154 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A | |
155 n-push zero s = s | |
156 n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s) | |
157 | |
158 n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A | |
159 n-pop zero s = s | |
160 n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) | |
161 | |
162 open ≡-Reasoning | |
163 | |
164 push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s | |
165 push-pop-equiv s = refl | |
166 | |
167 push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s | |
168 push-and-n-pop zero s = refl | |
169 push-and-n-pop {A} {a} (suc n) s = begin | |
478 | 170 n-pop {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id) |
179 | 171 ≡⟨ refl ⟩ |
478 | 172 popSingleLinkedStack (n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) |
179 | 173 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩ |
478 | 174 popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) |
179 | 175 ≡⟨ refl ⟩ |
478 | 176 n-pop {A} {a} (suc n) s |
179 | 177 ∎ |
178 | |
179 | |
180 n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s | |
181 n-push-pop-equiv zero s = refl | |
182 n-push-pop-equiv {A} {a} (suc n) s = begin | |
478 | 183 n-pop {A} {a} (suc n) (n-push (suc n) s) |
179 | 184 ≡⟨ refl ⟩ |
478 | 185 n-pop {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) |
179 | 186 ≡⟨ push-and-n-pop n (n-push n s) ⟩ |
478 | 187 n-pop {A} {a} n (n-push n s) |
180 | 188 ≡⟨ n-push-pop-equiv n s ⟩ |
179 | 189 s |
190 ∎ | |
181 | 191 |
192 | |
193 n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack | |
194 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack |