|
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
|
|
|
13 data Node (Symbol : Set) : Set where
|
|
|
14 T : Symbol → Node Symbol
|
|
|
15 N : Symbol → Node Symbol
|
|
|
16
|
|
|
17 data Seq (Symbol : Set) : Set where
|
|
|
18 _，_ : Symbol → Seq Symbol → Seq Symbol
|
|
|
19 _． : Symbol → Seq Symbol
|
|
|
20 Error : Seq Symbol
|
|
|
21
|
|
|
22 data Body (Symbol : Set) : Set where
|
|
|
23 _｜_ : Seq Symbol → Body Symbol → Body Symbol
|
|
|
24 _； : Seq Symbol → Body Symbol
|
|
|
25
|
|
|
26 record CFGGrammer (Symbol : Set) : Set where
|
|
|
27 field
|
|
|
28 cfg : Symbol → Body Symbol
|
|
|
29 top : Symbol
|
|
|
30 eq? : Symbol → Symbol → Bool
|
|
|
31 typeof : Symbol → Node Symbol
|
|
|
32
|
|
|
33 infixr 80 _｜_
|
|
|
34 infixr 90 _；
|
|
|
35 infixr 100 _，_
|
|
|
36 infixr 110 _．
|
|
|
37
|
|
|
38 open CFGGrammer
|
|
|
39
|
|
|
40 -----------------
|
|
|
41 --
|
|
|
42 -- CGF language
|
|
|
43 --
|
|
|
44 -----------------
|
|
|
45
|
|
|
46 split : {Σ : Set} → (List Σ → Bool)
|
|
|
47 → ( List Σ → Bool) → List Σ → Bool
|
|
|
48 split x y [] = x [] ∧ y []
|
|
|
49 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
50 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
51
|
|
|
52
|
|
|
53 cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool
|
|
|
54
|
|
|
55 {-# TERMINATING #-}
|
|
|
56 cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool
|
|
|
57 cfg-language1 cg Error x = false
|
|
|
58 cfg-language1 cg (S ， seq) x with typeof cg S
|
|
|
59 cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eq? cg x x' ∧ cfg-language1 cg seq t
|
|
|
60 cfg-language1 cg (_ ， seq) [] | T x = false
|
|
|
61 cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
|
|
|
62 cfg-language1 cg (S ．) x with typeof cg S
|
|
|
63 cfg-language1 cg (_ ．) (x' ∷ []) | T x = eq? cg x x'
|
|
|
64 cfg-language1 cg (_ ．) _ | T x = false
|
|
|
65 cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x
|
|
|
66
|
|
|
67 cfg-language0 cg _ [] = false
|
|
|
68 cfg-language0 cg (rule ｜ b) x =
|
|
|
69 cfg-language1 cg rule x ∨ cfg-language0 cg b x
|
|
|
70 cfg-language0 cg (rule ；) x = cfg-language1 cg rule x
|
|
|
71
|
|
|
72 cfg-language : {Symbol : Set} → CFGGrammer Symbol → List Symbol → Bool
|
|
|
73 cfg-language cg = cfg-language0 cg (cfg cg (top cg ))
|
|
|
74
|
|
|
75
|
|
|
76 data IFToken : Set where
|
|
|
77 EA : IFToken
|
|
|
78 EB : IFToken
|
|
|
79 EC : IFToken
|
|
|
80 IF : IFToken
|
|
|
81 THEN : IFToken
|
|
|
82 ELSE : IFToken
|
|
|
83 SA : IFToken
|
|
|
84 SB : IFToken
|
|
|
85 SC : IFToken
|
|
|
86 expr : IFToken
|
|
|
87 statement : IFToken
|
|
|
88
|
|
|
89 token-eq? : IFToken → IFToken → Bool
|
|
|
90 token-eq? EA EA = true
|
|
|
91 token-eq? EB EB = true
|
|
|
92 token-eq? EC EC = true
|
|
|
93 token-eq? IF IF = true
|
|
|
94 token-eq? THEN THEN = true
|
|
|
95 token-eq? ELSE ELSE = true
|
|
|
96 token-eq? SA SA = true
|
|
|
97 token-eq? SB SB = true
|
|
|
98 token-eq? SC SC = true
|
|
|
99 token-eq? expr expr = true
|
|
|
100 token-eq? statement statement = true
|
|
|
101 token-eq? _ _ = false
|
|
|
102
|
|
|
103 typeof-IFG : IFToken → Node IFToken
|
|
|
104 typeof-IFG expr = N expr
|
|
|
105 typeof-IFG statement = N statement
|
|
|
106 typeof-IFG x = T x
|
|
|
107
|
|
|
108 IFGrammer : CFGGrammer IFToken
|
|
|
109 IFGrammer = record {
|
|
|
110 cfg = cfg'
|
|
|
111 ; top = statement
|
|
|
112 ; eq? = token-eq?
|
|
|
113 ; typeof = typeof-IFG
|
|
|
114 } where
|
|
|
115 cfg' : IFToken → Body IFToken
|
|
|
116 cfg' expr = EA ． ｜ EB ． ｜ EC ． ；
|
|
|
117 cfg' statement =
|
|
|
118 SA ． ｜ SB ． ｜ SC ．
|
|
|
119 ｜ IF ， expr ， THEN ， statement ．
|
|
|
120 ｜ IF ， expr ， THEN ， statement ， ELSE ， statement ．
|
|
|
121 ；
|
|
|
122 cfg' x = Error ；
|
|
|
123
|
|
|
124 cfgtest1 = cfg-language IFGrammer ( SA ∷ [] )
|
|
|
125
|
|
|
126 cfgtest2 = cfg-language1 IFGrammer ( SA ．) ( SA ∷ [] )
|
|
|
127
|
|
|
128 cfgtest3 = cfg-language1 IFGrammer ( SA ． ) ( SA ∷ [] )
|
|
|
129
|
|
|
130 cfgtest4 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ SA ∷ [] )
|
|
|
131
|
|
|
132 cfgtest5 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ． ) (IF ∷ EA ∷ THEN ∷ SA ∷ [] )
|
|
|
133 cfgtest6 = cfg-language1 IFGrammer ( statement ．)(IF ∷ EA ∷ SA ∷ [] )
|
|
|
134 cfgtest7 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ， ELSE ， statement ． )
|
|
|
135 (IF ∷ EA ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
136 cfgtest8 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
137 cfgtest9 = cfg-language IFGrammer (IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] )
|
|
|
138
|
