Mercurial > hg > Papers > 2018 > ryokka-thesis

comparison final_pre/src/stack-subtype-sample.agda @ 7:28f900230c26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final_pre
author ryokka
date Mon, 19 Feb 2018 23:32:24 +0900
parents
children
comparison
equal deleted inserted replaced
6:d927f6b3d2b3 7:28f900230c26
1 module stack-subtype-sample where
2
3 open import Level renaming (suc to S ; zero to O)
4 open import Function
5 open import Data.Nat
6 open import Data.Maybe
7 open import Relation.Binary.PropositionalEquality
8
9 open import stack-subtype ℕ
10 open import subtype Context as N
11 open import subtype Meta as M
12
13
14 record Num : Set where
15 field
16 num : ℕ
17
18 instance
19 NumIsNormalDataSegment : N.DataSegment Num
20 NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
21 ; set = (\c n -> record c {n = Num.num n})}
22 NumIsMetaDataSegment : M.DataSegment Num
23 NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)})
24 ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})}
25
26
27 plus3 : Num -> Num
28 plus3 record { num = n } = record {num = n + 3}
29
30 plus3CS : N.CodeSegment Num Num
31 plus3CS = N.cs plus3
32
33
34
35 plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
36 -> M.CodeSegment Num (Meta)
37 plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
38 where
39 co = Meta.context mc
40 con : Num -> Context
41 con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
42 st = Meta.stack mc
43
44
45
46
47 push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta
48 push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
49 where
50 con = record { n = 4 ; element = just 0}
51 code = N.cs (\c -> c)
52 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
53
54
55 push-sample-equiv : push-sample ≡ record { nextCS = liftContext plus3CS
56 ; stack = record { top = nothing}
57 ; context = record { n = 9} }
58 push-sample-equiv = refl
59
60
61 pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta
62 pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc
63 where
64 con = record { n = 4 ; element = just 0}
65 code = N.cs (\c -> c)
66 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
67
68
69
70 pushed-sample-equiv : {m : Meta} ->
71 pushed-sample {m} ≡ record { nextCS = liftContext plus3CS
72 ; stack = record { top = just (cons 0 nothing) }
73 ; context = record { n = 12} }
74 pushed-sample-equiv = refl
75
76
77
78 pushNum : N.CodeSegment Context Context
79 pushNum = N.cs pn
80 where
81 pn : Context -> Context
82 pn record { n = n } = record { n = pred n ; element = just n}
83
84
85 pushOnce : Meta -> Meta
86 pushOnce m = M.exec pushSingleLinkedStackCS m
87
88 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
89 n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id
90 n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m))
91
92 popOnce : Meta -> Meta
93 popOnce m = M.exec popSingleLinkedStackCS m
94
95 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
96 n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id
97 n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m))
98
99
100
101 initMeta : ℕ -> Maybe ℕ -> N.CodeSegment Context Context -> Meta
102 initMeta n mn code = record { context = record { n = n ; element = mn}
103 ; stack = emptySingleLinkedStack
104 ; nextCS = code
105 }
106
107 n-push-cs-exec = M.exec (n-push {meta} 3) meta
108 where
109 meta = (initMeta 5 (just 9) pushNum)
110
111
112 n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = pushNum
113 ; context = record {n = 2 ; element = just 3}
114 ; stack = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}}
115 n-push-cs-exec-equiv = refl
116
117
118 n-pop-cs-exec = M.exec (n-pop {meta} 4) meta
119 where
120 meta = record { nextCS = N.cs id
121 ; context = record { n = 0 ; element = nothing}
122 ; stack = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))}
123 }
124
125 n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS = N.cs id
126 ; context = record { n = 0 ; element = just 6}
127 ; stack = record { top = just (cons 5 nothing)}
128 }
129
130 n-pop-cs-exec-equiv = refl
131
132
133 open ≡-Reasoning
134
135 id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta
136 id-meta n e s = record { context = record {n = n ; element = just e}
137 ; nextCS = (N.cs id) ; stack = s}
138
139 exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m)
140 exec-comp (M.cs x) (M.cs _) m = refl
141
142
143 push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁
144 push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
145 where
146 meta = id-meta n e record {top = just (cons x (just s))}
147
148 push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s
149 push-pop n e x s = refl
150
151
152
153 pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
154 pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta
155 ≡ M.exec (n-push {meta} n) meta
156 where
157 meta = id-meta cn ce s
158
159 pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s
160
161 pop-n-push zero cn ce s = refl
162 pop-n-push (suc n) cn ce s = begin
163 M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s)
164 ≡⟨ refl ⟩
165 M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
166 ≡⟨ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩
167 M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
168 ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
169 M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
170 ≡⟨ refl ⟩
171 M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
172 ≡⟨ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩
173 M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
174 ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩
175 M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
176 ≡⟨ refl ⟩
177 M.exec (n-push n) (pushOnce (id-meta cn ce s))
178 ≡⟨ refl ⟩
179 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
180 ≡⟨ refl ⟩
181 M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)
182 ∎
183
184
185
186 n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
187 n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta
188 where
189 meta = id-meta cn ce st
190
191 n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s
192 n-push-pop zero cn ce s = refl
193 n-push-pop (suc n) cn ce s = begin
194 M.exec (M.csComp {id-meta cn ce s} (n-pop {id-meta cn ce s} (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
195 ≡⟨ refl ⟩
196 M.exec (M.csComp {id-meta cn ce s} (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
197 ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s) ⟩
198 M.exec (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))
199 ≡⟨ refl ⟩
200 M.exec (n-pop n) (popOnce (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
201 ≡⟨ refl ⟩
202 M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
203 ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) ⟩
204 M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s))
205 ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (pop-n-push n cn ce s) ⟩
206 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
207 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩
208 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
209 ≡⟨ n-push-pop n cn ce s ⟩
210 id-meta cn ce s
211 ∎
212