Mercurial > hg > Members > Moririn
annotate src/parallel_execution/stack.agda @ 485:a7548f01f013
proof pop2 function in agda
| author | ryokka |
|---|---|
| date | Fri, 29 Dec 2017 19:27:39 +0900 |
| parents | 8a22cfd174bf |
| children | 8e133a3938c0 |
| rev | line source |
|---|---|
| 154 | 1 module stack where |
| 2 | |
| 161 | 3 open import Relation.Binary.PropositionalEquality |
| 477 | 4 open import Relation.Binary.Core |
| 484 | 5 open import Data.Nat |
| 6 open import Level renaming (suc to succ ; zero to Zero) | |
| 478 | 7 |
| 484 | 8 ex : 1 + 2 ≡ 3 |
| 9 ex = refl | |
| 179 | 10 |
| 161 | 11 data Bool : Set where |
| 12 True : Bool | |
| 13 False : Bool | |
| 164 | 14 |
| 485 | 15 record _∧_ {a b : Set} : Set where |
| 16 field | |
| 17 pi1 : a | |
| 18 pi2 : b | |
| 477 | 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 | |
| 484 | 29 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
30 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t |
| 484 | 31 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t |
| 477 | 32 open Stack |
| 427 | 33 |
| 477 | 34 pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t |
| 35 pushStack {a} {t} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} )) | |
| 36 | |
| 37 popStack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a -> t) -> t | |
| 38 popStack {a} {t} s0 next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 ) | |
| 427 | 39 |
| 484 | 40 pop2Stack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t |
| 41 pop2Stack {a} {t} s0 next = pop2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2) | |
| 42 | |
| 43 getStack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a -> t) -> t | |
| 44 getStack {a} {t} s0 next = get s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 ) | |
| 45 | |
| 46 get2Stack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t | |
| 47 get2Stack {a} {t} s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2) | |
| 478 | 48 |
| 427 | 49 |
| 161 | 50 data Element (a : Set) : Set where |
| 51 cons : a -> Maybe (Element a) -> Element a | |
| 52 | |
| 53 datum : {a : Set} -> Element a -> a | |
| 54 datum (cons a _) = a | |
| 55 | |
| 56 next : {a : Set} -> Element a -> Maybe (Element a) | |
| 57 next (cons _ n) = n | |
| 58 | |
| 59 | |
| 164 | 60 {- |
| 61 -- cannot define recrusive record definition. so use linked list with maybe. | |
| 161 | 62 record Element {l : Level} (a : Set l) : Set (suc l) where |
| 63 field | |
| 164 | 64 datum : a -- `data` is reserved by Agda. |
| 161 | 65 next : Maybe (Element a) |
| 66 -} | |
| 155 | 67 |
| 68 | |
| 164 | 69 |
| 161 | 70 record SingleLinkedStack (a : Set) : Set where |
| 71 field | |
| 72 top : Maybe (Element a) | |
| 73 open SingleLinkedStack | |
| 155 | 74 |
| 161 | 75 pushSingleLinkedStack : {Data t : Set} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t |
| 76 pushSingleLinkedStack stack datum next = next stack1 | |
| 77 where | |
| 78 element = cons datum (top stack) | |
| 164 | 79 stack1 = record {top = Just element} |
| 161 | 80 |
| 155 | 81 |
| 161 | 82 popSingleLinkedStack : {a t : Set} -> 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) | |
| 154 | 86 where |
| 161 | 87 data1 = datum d |
| 88 stack1 = record { top = (next d) } | |
| 154 | 89 |
| 484 | 90 pop2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 91 pop2SingleLinkedStack {a} stack cs with (top stack) | |
| 92 ... | Nothing = cs stack Nothing Nothing | |
| 93 ... | Just d = pop2SingleLinkedStack' stack cs | |
| 94 where | |
| 95 pop2SingleLinkedStack' : {t : Set} -> 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 d)}) (Just (datum d)) (Just (datum d1)) | |
| 99 | |
| 100 | |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
101 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
|
102 getSingleLinkedStack stack cs with (top stack) |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
103 ... | Nothing = cs stack Nothing |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
104 ... | Just d = cs stack (Just data1) |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
105 where |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
106 data1 = datum d |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
107 |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
108 get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 484 | 109 get2SingleLinkedStack {a} stack cs with (top stack) |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
110 ... | Nothing = cs stack Nothing Nothing |
| 484 | 111 ... | Just d = get2SingleLinkedStack' stack cs |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
112 where |
| 484 | 113 get2SingleLinkedStack' : {t : Set} -> 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 | |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
118 |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
119 |
| 161 | 120 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a |
| 121 emptySingleLinkedStack = record {top = Nothing} | |
| 122 | |
| 164 | 123 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) |
| 161 | 124 createSingleLinkedStack = record { stack = emptySingleLinkedStack |
| 125 ; push = pushSingleLinkedStack | |
| 126 ; pop = popSingleLinkedStack | |
| 484 | 127 ; pop2 = pop2SingleLinkedStack |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
128 ; get = getSingleLinkedStack |
| 484 | 129 ; get2 = get2SingleLinkedStack |
| 161 | 130 } |
| 131 | |
| 156 | 132 |
| 161 | 133 test01 : {a : Set} -> SingleLinkedStack a -> Maybe a -> Bool |
| 134 test01 stack _ with (top stack) | |
| 135 ... | (Just _) = True | |
| 136 ... | Nothing = False | |
| 137 | |
| 156 | 138 |
| 161 | 139 test02 : {a : Set} -> SingleLinkedStack a -> Bool |
| 140 test02 stack = (popSingleLinkedStack stack) test01 | |
| 156 | 141 |
| 165 | 142 test03 : {a : Set} -> a -> Bool |
| 143 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02 | |
| 156 | 144 |
| 477 | 145 testStack01 : {a : Set} -> a -> Bool |
| 146 testStack01 v = pushStack createSingleLinkedStack v ( | |
| 147 \s -> popStack s (\s1 d1 -> True)) | |
| 148 | |
| 485 | 149 testStack02 : (Stack (SingleLinkedStack ℕ) -> Bool) -> Bool |
| 484 | 150 testStack02 cs = pushStack createSingleLinkedStack 1 ( |
| 151 \s -> pushStack s 2 cs) | |
| 477 | 152 |
| 485 | 153 |
| 154 testStack031 : (d1 d2 : ℕ ) -> Bool | |
| 155 testStack031 1 2 = True | |
| 156 testStack031 _ _ = False | |
| 157 | |
| 158 testStack032 : (d1 d2 : Maybe ℕ) -> Bool | |
| 159 testStack032 (Just d1) (Just d2) = testStack031 d1 d2 | |
| 160 testStack032 _ _ = False | |
| 484 | 161 |
| 485 | 162 testStack03 : Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool ) -> Bool |
| 163 testStack03 s cs = pop2Stack s ( | |
| 164 \s d1 d2 -> cs d1 d2 ) | |
| 484 | 165 |
| 485 | 166 testStack04 : Bool |
| 167 testStack04 = testStack02 (\s -> testStack03 s testStack032) | |
| 168 | |
| 169 testStack05 : Set | |
| 170 testStack05 = testStack04 ≡ True | |
| 171 | |
| 161 | 172 |
| 165 | 173 lemma : {A : Set} {a : A} -> test03 a ≡ False |
| 158 | 174 lemma = refl |
| 179 | 175 |
| 176 id : {A : Set} -> A -> A | |
| 177 id a = a | |
| 178 | |
| 179 | |
| 484 | 180 n-push : {A : Set} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A |
| 179 | 181 n-push zero s = s |
| 182 n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s) | |
| 183 | |
| 484 | 184 n-pop : {A : Set} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A |
| 179 | 185 n-pop zero s = s |
| 186 n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) | |
| 187 | |
| 188 open ≡-Reasoning | |
| 189 | |
| 190 push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s | |
| 191 push-pop-equiv s = refl | |
| 192 | |
| 484 | 193 push-and-n-pop : {A : Set} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s |
| 179 | 194 push-and-n-pop zero s = refl |
| 195 push-and-n-pop {A} {a} (suc n) s = begin | |
| 478 | 196 n-pop {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id) |
| 179 | 197 ≡⟨ refl ⟩ |
| 478 | 198 popSingleLinkedStack (n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) |
| 179 | 199 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩ |
| 478 | 200 popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) |
| 179 | 201 ≡⟨ refl ⟩ |
| 478 | 202 n-pop {A} {a} (suc n) s |
| 179 | 203 ∎ |
| 204 | |
| 205 | |
| 484 | 206 n-push-pop-equiv : {A : Set} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s |
| 179 | 207 n-push-pop-equiv zero s = refl |
| 208 n-push-pop-equiv {A} {a} (suc n) s = begin | |
| 478 | 209 n-pop {A} {a} (suc n) (n-push (suc n) s) |
| 179 | 210 ≡⟨ refl ⟩ |
| 478 | 211 n-pop {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) |
| 179 | 212 ≡⟨ push-and-n-pop n (n-push n s) ⟩ |
| 478 | 213 n-pop {A} {a} n (n-push n s) |
| 180 | 214 ≡⟨ n-push-pop-equiv n s ⟩ |
| 179 | 215 s |
| 216 ∎ | |
| 181 | 217 |
| 218 | |
| 484 | 219 n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : ℕ) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack |
| 181 | 220 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack |