|
46
|
1 module cfg1 where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
4 open import Data.Nat hiding ( _≟_ )
|
|
|
5 open import Data.Fin
|
|
|
6 open import Data.Product
|
|
|
7 open import Data.List
|
|
|
8 open import Data.Maybe
|
|
|
9 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
|
|
|
10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
11 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
12
|
|
163
|
13 --
|
|
|
14 -- Java → Java Byte Code
|
|
|
15 --
|
|
|
16 -- CFG Stack Machine (PDA)
|
|
|
17 --
|
|
|
18
|
|
|
19
|
|
46
|
20 data Node (Symbol : Set) : Set where
|
|
|
21 T : Symbol → Node Symbol
|
|
|
22 N : Symbol → Node Symbol
|
|
|
23
|
|
|
24 data Seq (Symbol : Set) : Set where
|
|
|
25 _，_ : Symbol → Seq Symbol → Seq Symbol
|
|
|
26 _． : Symbol → Seq Symbol
|
|
|
27 Error : Seq Symbol
|
|
|
28
|
|
|
29 data Body (Symbol : Set) : Set where
|
|
|
30 _｜_ : Seq Symbol → Body Symbol → Body Symbol
|
|
|
31 _； : Seq Symbol → Body Symbol
|
|
|
32
|
|
|
33 record CFGGrammer (Symbol : Set) : Set where
|
|
|
34 field
|
|
|
35 cfg : Symbol → Body Symbol
|
|
|
36 top : Symbol
|
|
|
37 eq? : Symbol → Symbol → Bool
|
|
|
38 typeof : Symbol → Node Symbol
|
|
|
39
|
|
|
40 infixr 80 _｜_
|
|
|
41 infixr 90 _；
|
|
|
42 infixr 100 _，_
|
|
|
43 infixr 110 _．
|
|
|
44
|
|
|
45 open CFGGrammer
|
|
|
46
|
|
|
47 -----------------
|
|
|
48 --
|
|
|
49 -- CGF language
|
|
|
50 --
|
|
|
51 -----------------
|
|
|
52
|
|
|
53 split : {Σ : Set} → (List Σ → Bool)
|
|
|
54 → ( List Σ → Bool) → List Σ → Bool
|
|
|
55 split x y [] = x [] ∧ y []
|
|
|
56 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
57 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
58
|
|
|
59
|
|
|
60 cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool
|
|
|
61
|
|
|
62 {-# TERMINATING #-}
|
|
|
63 cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool
|
|
|
64 cfg-language1 cg Error x = false
|
|
|
65 cfg-language1 cg (S ， seq) x with typeof cg S
|
|
|
66 cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eq? cg x x' ∧ cfg-language1 cg seq t
|
|
|
67 cfg-language1 cg (_ ， seq) [] | T x = false
|
|
|
68 cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
|
|
|
69 cfg-language1 cg (S ．) x with typeof cg S
|
|
|
70 cfg-language1 cg (_ ．) (x' ∷ []) | T x = eq? cg x x'
|
|
|
71 cfg-language1 cg (_ ．) _ | T x = false
|
|
|
72 cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x
|
|
|
73
|
|
|
74 cfg-language0 cg _ [] = false
|
|
|
75 cfg-language0 cg (rule ｜ b) x =
|
|
|
76 cfg-language1 cg rule x ∨ cfg-language0 cg b x
|
|
|
77 cfg-language0 cg (rule ；) x = cfg-language1 cg rule x
|
|
|
78
|
|
|
79 cfg-language : {Symbol : Set} → CFGGrammer Symbol → List Symbol → Bool
|
|
|
80 cfg-language cg = cfg-language0 cg (cfg cg (top cg ))
|
|
|
81
|
|
|
82
|
|
|
83 data IFToken : Set where
|
|
|
84 EA : IFToken
|
|
|
85 EB : IFToken
|
|
|
86 EC : IFToken
|
|
|
87 IF : IFToken
|
|
|
88 THEN : IFToken
|
|
|
89 ELSE : IFToken
|
|
|
90 SA : IFToken
|
|
|
91 SB : IFToken
|
|
|
92 SC : IFToken
|
|
|
93 expr : IFToken
|
|
|
94 statement : IFToken
|
|
|
95
|
|
|
96 token-eq? : IFToken → IFToken → Bool
|
|
|
97 token-eq? EA EA = true
|
|
|
98 token-eq? EB EB = true
|
|
|
99 token-eq? EC EC = true
|
|
|
100 token-eq? IF IF = true
|
|
|
101 token-eq? THEN THEN = true
|
|
|
102 token-eq? ELSE ELSE = true
|
|
|
103 token-eq? SA SA = true
|
|
|
104 token-eq? SB SB = true
|
|
|
105 token-eq? SC SC = true
|
|
|
106 token-eq? expr expr = true
|
|
|
107 token-eq? statement statement = true
|
|
|
108 token-eq? _ _ = false
|
|
|
109
|
|
|
110 typeof-IFG : IFToken → Node IFToken
|
|
|
111 typeof-IFG expr = N expr
|
|
|
112 typeof-IFG statement = N statement
|
|
|
113 typeof-IFG x = T x
|
|
|
114
|
|
|
115 IFGrammer : CFGGrammer IFToken
|
|
|
116 IFGrammer = record {
|
|
|
117 cfg = cfg'
|
|
|
118 ; top = statement
|
|
|
119 ; eq? = token-eq?
|
|
|
120 ; typeof = typeof-IFG
|
|
|
121 } where
|
|
|
122 cfg' : IFToken → Body IFToken
|
|
|
123 cfg' expr = EA ． ｜ EB ． ｜ EC ． ；
|
|
|
124 cfg' statement =
|
|
|
125 SA ． ｜ SB ． ｜ SC ．
|
|
|
126 ｜ IF ， expr ， THEN ， statement ．
|
|
|
127 ｜ IF ， expr ， THEN ， statement ， ELSE ， statement ．
|
|
|
128 ；
|
|
|
129 cfg' x = Error ；
|
|
|
130
|
|
|
131 cfgtest1 = cfg-language IFGrammer ( SA ∷ [] )
|
|
|
132
|
|
|
133 cfgtest2 = cfg-language1 IFGrammer ( SA ．) ( SA ∷ [] )
|
|
|
134
|
|
|
135 cfgtest3 = cfg-language1 IFGrammer ( SA ． ) ( SA ∷ [] )
|
|
|
136
|
|
|
137 cfgtest4 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ SA ∷ [] )
|
|
|
138
|
|
|
139 cfgtest5 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ． ) (IF ∷ EA ∷ THEN ∷ SA ∷ [] )
|
|
|
140 cfgtest6 = cfg-language1 IFGrammer ( statement ．)(IF ∷ EA ∷ SA ∷ [] )
|
|
|
141 cfgtest7 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ， ELSE ， statement ． )
|
|
|
142 (IF ∷ EA ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
143 cfgtest8 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
144 cfgtest9 = cfg-language IFGrammer (IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
145
|
|
138
|
146 data E1Token : Set where
|
|
|
147 e1 : E1Token
|
|
|
148 e[ : E1Token
|
|
|
149 e] : E1Token
|
|
|
150 expr : E1Token
|
|
|
151 term : E1Token
|
|
|
152
|
|
|
153 E1-token-eq? : E1Token → E1Token → Bool
|
|
|
154 E1-token-eq? e1 e1 = true
|
|
|
155 E1-token-eq? e[ e] = true
|
|
|
156 E1-token-eq? e] e] = true
|
|
|
157 E1-token-eq? expr expr = true
|
|
|
158 E1-token-eq? term term = true
|
|
|
159 E1-token-eq? _ _ = false
|
|
|
160
|
|
|
161 typeof-E1 : E1Token → Node E1Token
|
|
|
162 typeof-E1 expr = N expr
|
|
|
163 typeof-E1 term = N term
|
|
|
164 typeof-E1 x = T x
|
|
|
165
|
|
|
166 E1Grammer : CFGGrammer E1Token
|
|
|
167 E1Grammer = record {
|
|
|
168 cfg = cfgE
|
|
|
169 ; top = expr
|
|
|
170 ; eq? = E1-token-eq?
|
|
|
171 ; typeof = typeof-E1
|
|
|
172 } where
|
|
|
173 cfgE : E1Token → Body E1Token
|
|
|
174 cfgE expr = term ．
|
|
|
175 ；
|
|
|
176 cfgE term = e1 ．
|
|
|
177 ｜ e[ ， expr ， e] ．
|
|
|
178 ；
|
|
|
179 cfgE x = Error ；
|
|
|
180
|
|
|
181 ecfgtest1 = cfg-language E1Grammer ( e1 ∷ [] )
|
|
|
182 ecfgtest2 = cfg-language E1Grammer ( e[ ∷ e1 ∷ e] ∷ [] )
|
|
|
183 ecfgtest3 = cfg-language E1Grammer ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] )
|
|
|
184
|
