|
7
|
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
|
