Mercurial > hg > Gears > GearsAgda
annotate src/parallel_execution/stack.agda @ 500:6d984ea42fd2
fix proof
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jan 2018 11:19:14 +0900 |
| parents | 2c125aa7a577 |
| children | 55077dd40a51 |
| rev | line source |
|---|---|
| 499 | 1 open import Level renaming (suc to succ ; zero to Zero ) |
| 496 | 2 module stack where |
| 154 | 3 |
| 161 | 4 open import Relation.Binary.PropositionalEquality |
| 477 | 5 open import Relation.Binary.Core |
| 484 | 6 open import Data.Nat |
| 478 | 7 |
| 484 | 8 ex : 1 + 2 ≡ 3 |
| 9 ex = refl | |
| 179 | 10 |
| 496 | 11 data Bool {n : Level } : Set (succ n) where |
| 161 | 12 True : Bool |
| 13 False : Bool | |
| 164 | 14 |
| 496 | 15 record _∧_ {n : Level } {a b : Set n} : Set n where |
| 485 | 16 field |
| 17 pi1 : a | |
| 18 pi2 : b | |
| 477 | 19 |
| 496 | 20 data Maybe {n : Level } (a : Set n) : Set n where |
| 161 | 21 Nothing : Maybe a |
| 22 Just : a -> Maybe a | |
| 23 | |
| 499 | 24 record Stack {n m : Level } {a : Set n } {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where |
| 161 | 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 |
| 496 | 34 pushStack : {n : Level } {t : Set (succ n)} {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} )) | |
| 477 | 36 |
| 496 | 37 popStack : {n : Level } { t : Set (succ n)} {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 ) | |
| 427 | 39 |
| 496 | 40 pop2Stack : {n : Level } { t : Set (succ n)} { 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) | |
| 484 | 42 |
| 496 | 43 getStack : {n : Level } {t : Set (succ n)} {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 ) | |
| 484 | 45 |
| 496 | 46 get2Stack : {n : Level } {t : Set (succ n)} {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) | |
| 478 | 48 |
| 427 | 49 |
| 496 | 50 data Element {n : Level } (a : Set n) : Set n where |
| 161 | 51 cons : a -> Maybe (Element a) -> Element a |
| 52 | |
| 496 | 53 datum : {n : Level } {a : Set n} -> Element a -> a |
| 161 | 54 datum (cons a _) = a |
| 55 | |
| 496 | 56 next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a) |
| 161 | 57 next (cons _ n) = n |
| 58 | |
| 59 | |
| 164 | 60 {- |
| 61 -- cannot define recrusive record definition. so use linked list with maybe. | |
| 496 | 62 record Element {l : Level} (a : Set n l) : Set n (suc l) where |
| 161 | 63 field |
| 164 | 64 datum : a -- `data` is reserved by Agda. |
| 161 | 65 next : Maybe (Element a) |
| 66 -} | |
| 155 | 67 |
| 68 | |
| 164 | 69 |
| 496 | 70 record SingleLinkedStack {n : Level } (a : Set n) : Set n where |
| 161 | 71 field |
| 72 top : Maybe (Element a) | |
| 73 open SingleLinkedStack | |
| 155 | 74 |
| 499 | 75 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t |
| 161 | 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 |
| 499 | 82 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
| 161 | 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 |
| 499 | 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) | |
| 484 | 92 ... | Nothing = cs stack Nothing Nothing |
| 499 | 93 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs |
| 484 | 94 where |
| 499 | 95 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 484 | 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 | |
| 499 | 101 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
|
483
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 |
| 499 | 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) | |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
110 ... | Nothing = cs stack Nothing Nothing |
| 499 | 111 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
112 where |
| 499 | 113 get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 484 | 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 |
| 496 | 120 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a |
| 161 | 121 emptySingleLinkedStack = record {top = Nothing} |
| 122 | |
| 499 | 123 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (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 |
| 499 | 133 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n} |
| 161 | 134 test01 stack _ with (top stack) |
| 135 ... | (Just _) = True | |
| 136 ... | Nothing = False | |
| 137 | |
| 156 | 138 |
| 496 | 139 test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool |
| 140 test02 stack = popSingleLinkedStack stack test01 | |
| 156 | 141 |
| 496 | 142 test03 : {n : Level } {a : Set n} -> a -> Bool |
| 165 | 143 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02 |
| 156 | 144 |
| 499 | 145 -- after a push and a pop, the stack is empty |
| 146 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False | |
| 147 lemma = refl | |
| 148 | |
| 496 | 149 testStack01 : {n : Level } {a : Set n} -> a -> Bool |
| 477 | 150 testStack01 v = pushStack createSingleLinkedStack v ( |
| 151 \s -> popStack s (\s1 d1 -> True)) | |
| 152 | |
| 500 | 153 -- after push 1 and 2, pop2 get 1 and 2 |
| 154 | |
| 155 testStack02 : ( Stack (SingleLinkedStack ℕ) -> Bool) -> Bool | |
| 484 | 156 testStack02 cs = pushStack createSingleLinkedStack 1 ( |
| 157 \s -> pushStack s 2 cs) | |
| 477 | 158 |
| 485 | 159 |
| 499 | 160 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero} |
| 500 | 161 testStack031 2 1 = True |
| 485 | 162 testStack031 _ _ = False |
| 163 | |
| 499 | 164 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero} |
| 485 | 165 testStack032 (Just d1) (Just d2) = testStack031 d1 d2 |
| 166 testStack032 _ _ = False | |
| 484 | 167 |
| 485 | 168 testStack03 : Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool ) -> Bool |
| 169 testStack03 s cs = pop2Stack s ( | |
| 170 \s d1 d2 -> cs d1 d2 ) | |
| 484 | 171 |
| 485 | 172 testStack04 : Bool |
| 173 testStack04 = testStack02 (\s -> testStack03 s testStack032) | |
| 174 | |
| 500 | 175 testStack05 : testStack04 ≡ True |
| 176 testStack05 = refl | |
| 179 | 177 |
| 496 | 178 id : {n : Level} {A : Set n} -> A -> A |
| 179 | 179 id a = a |
| 180 | |
| 499 | 181 -- push a, n times |
| 179 | 182 |
| 496 | 183 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A |
| 179 | 184 n-push zero s = s |
| 499 | 185 n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s ) |
| 179 | 186 |
| 499 | 187 n-pop : {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A |
| 179 | 188 n-pop zero s = s |
| 499 | 189 n-pop {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s ) |
| 179 | 190 |
| 191 open ≡-Reasoning | |
| 192 | |
| 499 | 193 push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s |
| 179 | 194 push-pop-equiv s = refl |
| 195 | |
| 499 | 196 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 |
| 179 | 197 push-and-n-pop zero s = refl |
| 496 | 198 push-and-n-pop {_} {A} {a} (suc n) s = begin |
| 499 | 199 n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id) |
| 179 | 200 ≡⟨ refl ⟩ |
| 499 | 201 popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) |
| 202 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩ | |
| 203 popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s) | |
| 179 | 204 ≡⟨ refl ⟩ |
| 499 | 205 n-pop {_} {A} {a} (suc n) s |
| 179 | 206 ∎ |
| 207 | |
| 208 | |
| 499 | 209 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 |
| 179 | 210 n-push-pop-equiv zero s = refl |
| 499 | 211 n-push-pop-equiv {_} {A} {a} (suc n) s = begin |
| 212 n-pop {_} {A} {a} (suc n) (n-push (suc n) s) | |
| 179 | 213 ≡⟨ refl ⟩ |
| 499 | 214 n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) |
| 179 | 215 ≡⟨ push-and-n-pop n (n-push n s) ⟩ |
| 499 | 216 n-pop {_} {A} {a} n (n-push n s) |
| 180 | 217 ≡⟨ n-push-pop-equiv n s ⟩ |
| 499 | 218 s |
| 179 | 219 ∎ |
| 181 | 220 |
| 221 | |
| 496 | 222 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 |
| 181 | 223 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack |