Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/cfg1.agda @ 405:af8f630b7e60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents 91781b7c65a8
children b85402051cdb
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible #-}
2
1 module cfg1 where 3 module cfg1 where
2 4
3 open import Level renaming ( suc to succ ; zero to Zero ) 5 open import Level renaming ( suc to succ ; zero to Zero )
4 open import Data.Nat hiding ( _≟_ ) 6 open import Data.Nat hiding ( _≟_ )
5 -- open import Data.Fin 7 -- open import Data.Fin
33 35
34 record CFGGrammer (Symbol : Set) : Set where 36 record CFGGrammer (Symbol : Set) : Set where
35 field 37 field
36 cfg : Symbol → Body Symbol 38 cfg : Symbol → Body Symbol
37 top : Symbol 39 top : Symbol
38 eq? : Symbol → Symbol → Bool 40 eqP : Symbol → Symbol → Bool
39 typeof : Symbol → Node Symbol 41 typeof : Symbol → Node Symbol
40 42
41 infixr 80 _｜_ 43 infixr 80 _｜_
42 infixr 90 _； 44 infixr 90 _；
43 infixr 100 _，_ 45 infixr 100 _，_
62 64
63 {-# TERMINATING #-} 65 {-# TERMINATING #-}
64 cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool 66 cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool
65 cfg-language1 cg Error x = false 67 cfg-language1 cg Error x = false
66 cfg-language1 cg (S ， seq) x with typeof cg S 68 cfg-language1 cg (S ， seq) x with typeof cg S
67 cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eq? cg x x' /\ cfg-language1 cg seq t 69 cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eqP cg x x' /\ cfg-language1 cg seq t
68 cfg-language1 cg (_ ， seq) [] | T x = false 70 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 71 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 72 cfg-language1 cg (S ．) x with typeof cg S
71 cfg-language1 cg (_ ．) (x' ∷ []) | T x = eq? cg x x' 73 cfg-language1 cg (_ ．) (x' ∷ []) | T x = eqP cg x x'
72 cfg-language1 cg (_ ．) _ | T x = false 74 cfg-language1 cg (_ ．) _ | T x = false
73 cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x 75 cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x
74 76
75 cfg-language0 cg _ [] = false 77 cfg-language0 cg _ [] = false
76 cfg-language0 cg (rule ｜ b) x = 78 cfg-language0 cg (rule ｜ b) x =
115 117
116 IFGrammer : CFGGrammer IFToken 118 IFGrammer : CFGGrammer IFToken
117 IFGrammer = record { 119 IFGrammer = record {
118 cfg = cfg' 120 cfg = cfg'
119 ; top = statement 121 ; top = statement
120 ; eq? = token-eq? 122 ; eqP = token-eq?
121 ; typeof = typeof-IFG 123 ; typeof = typeof-IFG
122 } where 124 } where
123 cfg' : IFToken → Body IFToken 125 cfg' : IFToken → Body IFToken
124 cfg' expr = EA ． ｜ EB ． ｜ EC ． ； 126 cfg' expr = EA ． ｜ EB ． ｜ EC ． ；
125 cfg' statement = 127 cfg' statement =
166 168
167 E1Grammer : CFGGrammer E1Token 169 E1Grammer : CFGGrammer E1Token
168 E1Grammer = record { 170 E1Grammer = record {
169 cfg = cfgE 171 cfg = cfgE
170 ; top = expr 172 ; top = expr
171 ; eq? = E1-token-eq? 173 ; eqP = E1-token-eq?
172 ; typeof = typeof-E1 174 ; typeof = typeof-E1
173 } where 175 } where
174 cfgE : E1Token → Body E1Token 176 cfgE : E1Token → Body E1Token
175 cfgE expr = term ． 177 cfgE expr = term ．
176 ； 178 ；
284 286
285 pda→cfg : {Symbol : Set} { Q : Set} → (pda : PDA Q Symbol Q) → CFGGrammer Symbol 287 pda→cfg : {Symbol : Set} { Q : Set} → (pda : PDA Q Symbol Q) → CFGGrammer Symbol
286 pda→cfg pda = record { 288 pda→cfg pda = record {
287 cfg = {!!} 289 cfg = {!!}
288 ; top = {!!} 290 ; top = {!!}
289 ; eq? = {!!} 291 ; eqP = {!!}
290 ; typeof = {!!} 292 ; typeof = {!!}
291 } 293 }
292 294
293 pda->cfg : {Symbol : Set} { Q : Set} → (start : Q) → (input : List Symbol) 295 pda->cfg : {Symbol : Set} { Q : Set} → (start : Q) → (input : List Symbol)
294 → (pda : PDA Q Symbol Q) 296 → (pda : PDA Q Symbol Q)
297 299
298 record CDGGrammer (Symbol : Set) : Set where 300 record CDGGrammer (Symbol : Set) : Set where
299 field 301 field
300 cdg : Seq Symbol → Body Symbol 302 cdg : Seq Symbol → Body Symbol
301 top : Symbol 303 top : Symbol
302 eq? : Symbol → Symbol → Bool 304 eqP : Symbol → Symbol → Bool
303 typeof : Symbol → Node Symbol 305 typeof : Symbol → Node Symbol
304 306