|
405
|
1 {-# OPTIONS --cubical-compatible #-}
|
|
|
2
|
|
46
|
3 module cfg1 where
|
|
|
4
|
|
|
5 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
6 open import Data.Nat hiding ( _≟_ )
|
|
275
|
7 -- open import Data.Fin
|
|
|
8 -- open import Data.Product
|
|
46
|
9 open import Data.List
|
|
|
10 open import Data.Maybe
|
|
275
|
11 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
|
|
46
|
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
13 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
275
|
14 open import logic
|
|
46
|
15
|
|
163
|
16 --
|
|
|
17 -- Java → Java Byte Code
|
|
|
18 --
|
|
|
19 -- CFG Stack Machine (PDA)
|
|
|
20 --
|
|
|
21
|
|
|
22
|
|
46
|
23 data Node (Symbol : Set) : Set where
|
|
|
24 T : Symbol → Node Symbol
|
|
|
25 N : Symbol → Node Symbol
|
|
|
26
|
|
|
27 data Seq (Symbol : Set) : Set where
|
|
|
28 _，_ : Symbol → Seq Symbol → Seq Symbol
|
|
|
29 _． : Symbol → Seq Symbol
|
|
|
30 Error : Seq Symbol
|
|
|
31
|
|
|
32 data Body (Symbol : Set) : Set where
|
|
|
33 _｜_ : Seq Symbol → Body Symbol → Body Symbol
|
|
|
34 _； : Seq Symbol → Body Symbol
|
|
|
35
|
|
|
36 record CFGGrammer (Symbol : Set) : Set where
|
|
|
37 field
|
|
|
38 cfg : Symbol → Body Symbol
|
|
|
39 top : Symbol
|
|
405
|
40 eqP : Symbol → Symbol → Bool
|
|
46
|
41 typeof : Symbol → Node Symbol
|
|
|
42
|
|
|
43 infixr 80 _｜_
|
|
|
44 infixr 90 _；
|
|
|
45 infixr 100 _，_
|
|
|
46 infixr 110 _．
|
|
|
47
|
|
|
48 open CFGGrammer
|
|
|
49
|
|
|
50 -----------------
|
|
|
51 --
|
|
|
52 -- CGF language
|
|
|
53 --
|
|
|
54 -----------------
|
|
|
55
|
|
|
56 split : {Σ : Set} → (List Σ → Bool)
|
|
|
57 → ( List Σ → Bool) → List Σ → Bool
|
|
275
|
58 split x y [] = x [] /\ y []
|
|
|
59 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
|
|
46
|
60 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
61
|
|
|
62
|
|
|
63 cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool
|
|
|
64
|
|
|
65 {-# TERMINATING #-}
|
|
|
66 cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool
|
|
|
67 cfg-language1 cg Error x = false
|
|
|
68 cfg-language1 cg (S ， seq) x with typeof cg S
|
|
405
|
69 cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eqP cg x x' /\ cfg-language1 cg seq t
|
|
46
|
70 cfg-language1 cg (_ ， seq) [] | T x = false
|
|
|
71 cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
|
|
|
72 cfg-language1 cg (S ．) x with typeof cg S
|
|
405
|
73 cfg-language1 cg (_ ．) (x' ∷ []) | T x = eqP cg x x'
|
|
46
|
74 cfg-language1 cg (_ ．) _ | T x = false
|
|
|
75 cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x
|
|
|
76
|
|
|
77 cfg-language0 cg _ [] = false
|
|
|
78 cfg-language0 cg (rule ｜ b) x =
|
|
275
|
79 cfg-language1 cg rule x \/ cfg-language0 cg b x
|
|
46
|
80 cfg-language0 cg (rule ；) x = cfg-language1 cg rule x
|
|
|
81
|
|
|
82 cfg-language : {Symbol : Set} → CFGGrammer Symbol → List Symbol → Bool
|
|
|
83 cfg-language cg = cfg-language0 cg (cfg cg (top cg ))
|
|
|
84
|
|
|
85
|
|
|
86 data IFToken : Set where
|
|
|
87 EA : IFToken
|
|
|
88 EB : IFToken
|
|
|
89 EC : IFToken
|
|
|
90 IF : IFToken
|
|
|
91 THEN : IFToken
|
|
|
92 ELSE : IFToken
|
|
|
93 SA : IFToken
|
|
|
94 SB : IFToken
|
|
|
95 SC : IFToken
|
|
|
96 expr : IFToken
|
|
|
97 statement : IFToken
|
|
|
98
|
|
|
99 token-eq? : IFToken → IFToken → Bool
|
|
|
100 token-eq? EA EA = true
|
|
|
101 token-eq? EB EB = true
|
|
|
102 token-eq? EC EC = true
|
|
|
103 token-eq? IF IF = true
|
|
|
104 token-eq? THEN THEN = true
|
|
|
105 token-eq? ELSE ELSE = true
|
|
|
106 token-eq? SA SA = true
|
|
|
107 token-eq? SB SB = true
|
|
|
108 token-eq? SC SC = true
|
|
|
109 token-eq? expr expr = true
|
|
|
110 token-eq? statement statement = true
|
|
|
111 token-eq? _ _ = false
|
|
|
112
|
|
|
113 typeof-IFG : IFToken → Node IFToken
|
|
|
114 typeof-IFG expr = N expr
|
|
|
115 typeof-IFG statement = N statement
|
|
|
116 typeof-IFG x = T x
|
|
|
117
|
|
|
118 IFGrammer : CFGGrammer IFToken
|
|
|
119 IFGrammer = record {
|
|
|
120 cfg = cfg'
|
|
|
121 ; top = statement
|
|
405
|
122 ; eqP = token-eq?
|
|
46
|
123 ; typeof = typeof-IFG
|
|
|
124 } where
|
|
|
125 cfg' : IFToken → Body IFToken
|
|
|
126 cfg' expr = EA ． ｜ EB ． ｜ EC ． ；
|
|
|
127 cfg' statement =
|
|
|
128 SA ． ｜ SB ． ｜ SC ．
|
|
|
129 ｜ IF ， expr ， THEN ， statement ．
|
|
|
130 ｜ IF ， expr ， THEN ， statement ， ELSE ， statement ．
|
|
|
131 ；
|
|
|
132 cfg' x = Error ；
|
|
|
133
|
|
|
134 cfgtest1 = cfg-language IFGrammer ( SA ∷ [] )
|
|
|
135
|
|
|
136 cfgtest2 = cfg-language1 IFGrammer ( SA ．) ( SA ∷ [] )
|
|
|
137
|
|
|
138 cfgtest3 = cfg-language1 IFGrammer ( SA ． ) ( SA ∷ [] )
|
|
|
139
|
|
|
140 cfgtest4 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ SA ∷ [] )
|
|
|
141
|
|
|
142 cfgtest5 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ． ) (IF ∷ EA ∷ THEN ∷ SA ∷ [] )
|
|
|
143 cfgtest6 = cfg-language1 IFGrammer ( statement ．)(IF ∷ EA ∷ SA ∷ [] )
|
|
|
144 cfgtest7 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ， ELSE ， statement ． )
|
|
|
145 (IF ∷ EA ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
146 cfgtest8 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
147 cfgtest9 = cfg-language IFGrammer (IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
148
|
|
138
|
149 data E1Token : Set where
|
|
|
150 e1 : E1Token
|
|
|
151 e[ : E1Token
|
|
|
152 e] : E1Token
|
|
|
153 expr : E1Token
|
|
|
154 term : E1Token
|
|
|
155
|
|
|
156 E1-token-eq? : E1Token → E1Token → Bool
|
|
|
157 E1-token-eq? e1 e1 = true
|
|
|
158 E1-token-eq? e[ e] = true
|
|
|
159 E1-token-eq? e] e] = true
|
|
|
160 E1-token-eq? expr expr = true
|
|
|
161 E1-token-eq? term term = true
|
|
|
162 E1-token-eq? _ _ = false
|
|
|
163
|
|
|
164 typeof-E1 : E1Token → Node E1Token
|
|
|
165 typeof-E1 expr = N expr
|
|
|
166 typeof-E1 term = N term
|
|
|
167 typeof-E1 x = T x
|
|
|
168
|
|
|
169 E1Grammer : CFGGrammer E1Token
|
|
|
170 E1Grammer = record {
|
|
|
171 cfg = cfgE
|
|
|
172 ; top = expr
|
|
405
|
173 ; eqP = E1-token-eq?
|
|
138
|
174 ; typeof = typeof-E1
|
|
|
175 } where
|
|
|
176 cfgE : E1Token → Body E1Token
|
|
|
177 cfgE expr = term ．
|
|
|
178 ；
|
|
|
179 cfgE term = e1 ．
|
|
|
180 ｜ e[ ， expr ， e] ．
|
|
|
181 ；
|
|
|
182 cfgE x = Error ；
|
|
|
183
|
|
|
184 ecfgtest1 = cfg-language E1Grammer ( e1 ∷ [] )
|
|
|
185 ecfgtest2 = cfg-language E1Grammer ( e[ ∷ e1 ∷ e] ∷ [] )
|
|
|
186 ecfgtest3 = cfg-language E1Grammer ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] )
|
|
275
|
187 ecfgtest4 = cfg-language E1Grammer ( e[ ∷ e1 ∷ [] )
|
|
138
|
188
|
|
274
|
189 open import Function
|
|
|
190
|
|
275
|
191 left : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
|
|
|
192 left ( e[ ∷ t ) fail next = next t
|
|
|
193 left t fail next = fail t
|
|
274
|
194
|
|
275
|
195 right : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
|
|
|
196 right ( e] ∷ t ) fail next = next t
|
|
|
197 right t fail next = fail t
|
|
274
|
198
|
|
|
199
|
|
|
200 {-# TERMINATING #-}
|
|
275
|
201 expr1 : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
|
|
|
202 expr1 ( e1 ∷ t ) fail next = next t
|
|
|
203 expr1 ( expr ∷ t ) fail next = next t
|
|
|
204 expr1 ( term ∷ t ) fail next = next t
|
|
|
205 expr1 x fail next = left x fail $ λ x → expr1 x fail $ λ x → right x fail $ next
|
|
277
|
206 -- expr1 x fail next = left x fail ( λ x → expr1 x fail ( λ x → right x fail ( next )))
|
|
275
|
207
|
|
|
208 cfgtest01 = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x → ⟪ true , x ⟫ )
|
|
|
209 cfgtest02 = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x → ⟪ true , x ⟫ )
|
|
|
210 cfgtest03 = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x → ⟪ true , x ⟫ )
|
|
|
211
|
|
|
212 open import pushdown
|
|
|
213
|
|
|
214 data CG1 : Set where
|
|
|
215 ce : CG1
|
|
|
216 c1 : CG1
|
|
|
217
|
|
|
218 pd : CG1 → E1Token → CG1 → CG1 ∧ PushDown CG1
|
|
|
219 pd c1 e[ s = ⟪ c1 , push c1 ⟫
|
|
|
220 pd c1 e] c1 = ⟪ c1 , pop ⟫
|
|
|
221 pd c1 e1 c1 = ⟪ c1 , none ⟫
|
|
|
222 pd s expr s1 = ⟪ c1 , none ⟫
|
|
|
223 pd s term s1 = ⟪ c1 , none ⟫
|
|
|
224 pd s _ s1 = ⟪ ce , none ⟫
|
|
|
225
|
|
|
226 pok : CG1 → Bool
|
|
|
227 pok c1 = true
|
|
|
228 pok s = false
|
|
274
|
229
|
|
275
|
230 pnc : PushDownAutomaton CG1 E1Token CG1
|
|
|
231 pnc = record {
|
|
|
232 pδ = pd
|
|
|
233 ; pempty = ce
|
|
|
234 ; pok = pok
|
|
|
235 }
|
|
|
236
|
|
|
237 pda-ce-test1 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) []
|
|
|
238 pda-ce-test2 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) []
|
|
|
239 pda-ce-test3 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e1 ∷ e] ∷ e1 ∷ [] ) []
|
|
|
240
|
|
276
|
241 record PNC (accept : Bool ) : Set where
|
|
275
|
242 field
|
|
276
|
243 orig-x : List E1Token
|
|
|
244 pnc-q : CG1
|
|
275
|
245 pnc-st : List CG1
|
|
276
|
246 pnc-p : CG1 → List CG1 → Bool
|
|
|
247 success : accept ≡ true → pnc-p pnc-q pnc-st ≡ true → PushDownAutomaton.paccept pnc c1 orig-x [] ≡ true
|
|
|
248 failure : accept ≡ false → pnc-p pnc-q pnc-st ≡ false → PushDownAutomaton.paccept pnc c1 orig-x [] ≡ false
|
|
275
|
249
|
|
|
250 open import Data.Unit
|
|
|
251
|
|
|
252 {-# TERMINATING #-}
|
|
276
|
253 expr1P : {n : Level } {t : Set n } → (x : List E1Token ) → PNC true
|
|
|
254 → ( fail : List E1Token → PNC false → t ) → ( next : List E1Token → PNC true → t ) → t
|
|
275
|
255 expr1P x _ _ _ = {!!}
|
|
|
256
|
|
|
257 expr1P-test : (x : List E1Token ) → ⊤
|
|
276
|
258 expr1P-test x = expr1P x record { orig-x = x ; pnc-q = c1 ; pnc-st = []
|
|
|
259 ; pnc-p = λ q st → PushDownAutomaton.paccept pnc q x st ; success = λ _ p → p ; failure = λ _ p → p }
|
|
|
260 (λ x p → {!!} ) (λ x p → {!!} )
|
|
275
|
261
|
|
318
|
262 ----
|
|
|
263 --
|
|
|
264 -- CFG to PDA
|
|
|
265 --
|
|
275
|
266
|
|
318
|
267 cfg→pda-state : {Symbol : Set} → CFGGrammer Symbol → Set
|
|
|
268 cfg→pda-state cfg = {!!}
|
|
275
|
269
|
|
318
|
270 cfg→pda-start : {Symbol : Set} → (cfg : CFGGrammer Symbol) → cfg→pda-state cfg
|
|
|
271 cfg→pda-start cfg = {!!}
|
|
|
272
|
|
|
273 cfg→pda : {Symbol : Set} → (cfg : CFGGrammer Symbol) → PDA (cfg→pda-state cfg) Symbol (cfg→pda-state cfg)
|
|
|
274 cfg→pda cfg = {!!}
|
|
|
275
|
|
|
276 cfg->pda : {Symbol : Set} → (input : List Symbol)
|
|
|
277 → (cfg : CFGGrammer Symbol)
|
|
|
278 → PDA.paccept (cfg→pda cfg ) (cfg→pda-start cfg) input [] ≡ cfg-language cfg input
|
|
|
279 cfg->pda = {!!}
|
|
|
280
|
|
|
281 ----
|
|
|
282 --
|
|
|
283 -- PDA to CFG
|
|
|
284 --
|
|
|
285 open import pushdown
|
|
|
286
|
|
|
287 pda→cfg : {Symbol : Set} { Q : Set} → (pda : PDA Q Symbol Q) → CFGGrammer Symbol
|
|
|
288 pda→cfg pda = record {
|
|
|
289 cfg = {!!}
|
|
|
290 ; top = {!!}
|
|
405
|
291 ; eqP = {!!}
|
|
318
|
292 ; typeof = {!!}
|
|
|
293 }
|
|
|
294
|
|
|
295 pda->cfg : {Symbol : Set} { Q : Set} → (start : Q) → (input : List Symbol)
|
|
|
296 → (pda : PDA Q Symbol Q)
|
|
|
297 → PDA.paccept pda start input [] ≡ cfg-language (pda→cfg pda) input
|
|
|
298 pda->cfg = {!!}
|
|
|
299
|
|
|
300 record CDGGrammer (Symbol : Set) : Set where
|
|
|
301 field
|
|
|
302 cdg : Seq Symbol → Body Symbol
|
|
|
303 top : Symbol
|
|
405
|
304 eqP : Symbol → Symbol → Bool
|
|
318
|
305 typeof : Symbol → Node Symbol
|
|
|
306
|
