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