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