|
36
|
1 module cfg where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to succ ; zero to Zero )
|
|
43
|
4 open import Data.Nat hiding ( _≟_ )
|
|
39
|
5 open import Data.Fin
|
|
36
|
6 open import Data.Product
|
|
39
|
7 open import Data.List
|
|
36
|
8 open import Data.Maybe
|
|
40
|
9 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
|
|
36
|
10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
11 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
40
|
12 -- open import Data.String
|
|
36
|
13
|
|
318
|
14 data IsTerm (Token : Set) : Set (succ Zero) where
|
|
41
|
15 isTerm : Token → IsTerm Token
|
|
|
16 noTerm : IsTerm Token
|
|
|
17
|
|
43
|
18 record CFGGrammer (Token Node : Set) : Set (succ Zero) where
|
|
39
|
19 field
|
|
42
|
20 cfg : Node → List ( List ( Node ) )
|
|
|
21 cfgtop : Node
|
|
|
22 term? : Node → IsTerm Token
|
|
43
|
23 tokensz : ℕ
|
|
|
24 tokenid : Token → Fin tokensz
|
|
41
|
25
|
|
|
26 open CFGGrammer
|
|
|
27
|
|
42
|
28 -----------------
|
|
|
29 --
|
|
|
30 -- CGF language
|
|
|
31 --
|
|
|
32 -----------------
|
|
|
33
|
|
41
|
34 split : {Σ : Set} → (List Σ → Bool)
|
|
|
35 → ( List Σ → Bool) → List Σ → Bool
|
|
|
36 split x y [] = x [] ∧ y []
|
|
|
37 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
38 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
39
|
|
|
40
|
|
43
|
41 cfg-language0 : {Node Token : Set} → CFGGrammer Token Node → List (List Node ) → List Token → Bool
|
|
40
|
42
|
|
|
43 {-# TERMINATING #-}
|
|
43
|
44 cfg-language2 : {Node Token : Set} → CFGGrammer Token Node → Node → List Token → Bool
|
|
41
|
45 cfg-language2 cg _ [] = false
|
|
|
46 cfg-language2 cg x (h1 ∷ [] ) with term? cg x
|
|
43
|
47 cfg-language2 cg x (h1 ∷ []) | isTerm t with tokenid cg h1 ≟ tokenid cg t
|
|
|
48 cfg-language2 cg x (h1 ∷ []) | isTerm t | yes p = true
|
|
41
|
49 cfg-language2 cg x (h1 ∷ []) | isTerm t | no ¬p = false
|
|
42
|
50 cfg-language2 cg x (h1 ∷ []) | noTerm = cfg-language0 cg (cfg cg x) ( h1 ∷ [] )
|
|
41
|
51 cfg-language2 cg x In with term? cg x
|
|
|
52 cfg-language2 cg x In | isTerm t = false
|
|
42
|
53 cfg-language2 cg x In | noTerm = cfg-language0 cg (cfg cg x ) In
|
|
40
|
54
|
|
43
|
55 cfg-language1 : {Node Token : Set} → CFGGrammer Token Node → List Node → List Token → Bool
|
|
41
|
56 cfg-language1 cg [] [] = true
|
|
40
|
57 cfg-language1 cg [] _ = false
|
|
|
58 cfg-language1 cg (node ∷ T) = split ( cfg-language2 cg node ) ( cfg-language1 cg T )
|
|
|
59
|
|
41
|
60 cfg-language0 cg [] [] = true
|
|
40
|
61 cfg-language0 cg [] _ = false
|
|
42
|
62 cfg-language0 cg (node ∷ T) In = cfg-language1 cg node In ∨ cfg-language0 cg T In
|
|
41
|
63
|
|
43
|
64 cfg-language : {Node Token : Set} → CFGGrammer Token Node → List Token → Bool
|
|
42
|
65 cfg-language cg = cfg-language0 cg (cfg cg (cfgtop cg))
|
|
|
66
|
|
|
67 -----------------
|
|
39
|
68
|
|
43
|
69 data IFToken : Set where
|
|
|
70 t:EA : IFToken
|
|
|
71 t:EB : IFToken
|
|
|
72 t:EC : IFToken
|
|
|
73 t:IF : IFToken
|
|
|
74 t:THEN : IFToken
|
|
|
75 t:ELSE : IFToken
|
|
|
76 t:SA : IFToken
|
|
|
77 t:SB : IFToken
|
|
|
78 t:SC : IFToken
|
|
|
79
|
|
|
80 IFtokenid : IFToken → Fin 9
|
|
|
81 IFtokenid t:EA = # 0
|
|
|
82 IFtokenid t:EB = # 1
|
|
|
83 IFtokenid t:EC = # 2
|
|
|
84 IFtokenid t:IF = # 3
|
|
|
85 IFtokenid t:THEN = # 4
|
|
|
86 IFtokenid t:ELSE = # 5
|
|
|
87 IFtokenid t:SA = # 6
|
|
|
88 IFtokenid t:SB = # 7
|
|
|
89 IFtokenid t:SC = # 8
|
|
|
90
|
|
|
91 data IFNode (T : Set) : Set where
|
|
|
92 Token : T → IFNode T
|
|
|
93 expr : IFNode T
|
|
|
94 statement : IFNode T
|
|
|
95
|
|
|
96 IFGrammer : CFGGrammer IFToken (IFNode IFToken)
|
|
|
97 IFGrammer = record {
|
|
|
98 cfg = cfg'
|
|
|
99 ; cfgtop = statement
|
|
|
100 ; term? = term?'
|
|
|
101 ; tokensz = 9
|
|
|
102 ; tokenid = IFtokenid
|
|
|
103 } where
|
|
|
104 term?' : IFNode IFToken → IsTerm IFToken
|
|
|
105 term?' (Token x) = isTerm x
|
|
|
106 term?' _ = noTerm
|
|
|
107 cfg' : IFNode IFToken → List ( List (IFNode IFToken) )
|
|
|
108 cfg' (Token t) = ( (Token t) ∷ [] ) ∷ []
|
|
|
109 cfg' expr = ( Token t:EA ∷ [] ) ∷
|
|
|
110 ( Token t:EB ∷ [] ) ∷
|
|
|
111 ( Token t:EC ∷ [] ) ∷ []
|
|
|
112 cfg' statement = ( Token t:SA ∷ [] ) ∷
|
|
|
113 ( Token t:SB ∷ [] ) ∷
|
|
|
114 ( Token t:SC ∷ [] ) ∷
|
|
|
115 ( Token t:IF ∷ expr ∷ statement ∷ [] ) ∷
|
|
|
116 ( Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ [] ) ∷ []
|
|
|
117
|
|
|
118
|
|
46
|
119 cfgtest1 = cfg-language IFGrammer ( t:SA ∷ [] )
|
|
39
|
120
|
|
46
|
121 cfgtest2 = cfg-language2 IFGrammer (Token t:SA) ( t:SA ∷ [] )
|
|
41
|
122
|
|
46
|
123 cfgtest3 = cfg-language1 IFGrammer (Token t:SA ∷ [] ) ( t:SA ∷ [] )
|
|
41
|
124
|
|
46
|
125 cfgtest4 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:SA ∷ [] )
|
|
41
|
126
|
|
46
|
127 cfgtest5 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:EA ∷ [] )
|
|
|
128 cfgtest6 = cfg-language2 IFGrammer statement (t:IF ∷ t:EA ∷ t:SA ∷ [] )
|
|
|
129 cfgtest7 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] )
|
|
41
|
130
|
|
46
|
131 cfgtest8 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] )
|
|
41
|
132
|
