Mercurial > hg > Members > kono > Proof > automaton
changeset 42:bbb39677d5ab
list base CFG
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Dec 2018 02:23:34 +0900 |
| parents | ae69102153a9 |
| children | 31e4bd173951 |
| files | agda/cfg.agda |
| diffstat | 1 files changed, 46 insertions(+), 77 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/cfg.agda Sat Dec 22 01:30:03 2018 +0900 +++ b/agda/cfg.agda Sat Dec 22 02:23:34 2018 +0900 @@ -2,7 +2,6 @@ open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Fin -open import Data.Nat open import Data.Product open import Data.List open import Data.Maybe @@ -17,13 +16,11 @@ isTerm : Token → IsTerm Token noTerm : IsTerm Token -record CFGGrammer (Token : Set) (Node Node' : Set ) : Set (succ Zero) where +record CFGGrammer (Token Node : Set) : Set (succ Zero) where field - cfg : Node → List ( Node' ) - cfgmap : Node → Node' - cfgtop : Node' - list : Node' → List Node - term? : Node' → IsTerm Token + cfg : Node → List ( List ( Node ) ) + cfgtop : Node + term? : Node → IsTerm Token cmp : (x y : Token ) → Dec ( x ≡ y ) data IFToken : Set where @@ -37,41 +34,6 @@ t:SB : IFToken t:SC : IFToken --- tokenizer : {Σ : Set} → List Σ → IFToken --- tokenizer = {!!} - - -data Expr : Set where - Expr0 : Expr - Expr1 : Expr - Expr2 : Expr - -data Statement : Set where - Statement0 : Statement - Statement1 : Statement - Statement2 : Statement - Statement3 : Statement - Statement4 : Statement - -data IFNode (T : Set) : Set where - Token : T → IFNode T - expr : Expr → IFNode T - statement : Statement → IFNode T - -data IFNode' (T : Set) : Set where - Token' : T → IFNode' T - expr' : IFNode' T - statement' : IFNode' T - -isTerm-IFGRammer : IFNode' IFToken → IsTerm IFToken -isTerm-IFGRammer (Token' x) = isTerm x -isTerm-IFGRammer _ = noTerm - -list-IFGrammer : IFNode' IFToken → List ( IFNode IFToken ) -list-IFGrammer (Token' t) = Token t ∷ [] -list-IFGrammer expr' = expr Expr0 ∷ expr Expr1 ∷ expr Expr2 ∷ [] -list-IFGrammer statement' = statement Statement0 ∷ statement Statement1 ∷ statement Statement2 ∷ statement Statement3 ∷ statement Statement4 ∷ [] - cmpi : (x y : IFToken ) → Dec ( x ≡ y ) cmpi t:EA t:EA = yes refl cmpi t:EB t:EB = yes refl @@ -155,33 +117,40 @@ cmpi t:SC t:SA = no (λ ()) cmpi t:SC t:SB = no (λ ()) -IFGrammer : CFGGrammer IFToken (IFNode IFToken) (IFNode' IFToken) +data IFNode (T : Set) : Set where + Token : T → IFNode T + expr : IFNode T + statement : IFNode T + +IFGrammer : CFGGrammer IFToken (IFNode IFToken) IFGrammer = record { cfg = cfg - ; cfgmap = cfgmap - ; cfgtop = cfgtop - ; list = list-IFGrammer - ; term? = isTerm-IFGRammer + ; cfgtop = statement + ; term? = term? ; cmp = cmpi } where - cfgtop = statement' - cfgmap : IFNode IFToken → IFNode' IFToken - cfgmap (Token t) = Token' t - cfgmap (expr e) = expr' - cfgmap (statement s) = statement' - cfg : IFNode IFToken → List (IFNode' IFToken) - cfg (Token t) = (Token' t) ∷ [] - cfg (expr Expr0) = Token' t:EA ∷ [] - cfg (expr Expr1) = Token' t:EB ∷ [] - cfg (expr Expr2) = Token' t:EC ∷ [] - cfg (statement Statement0) = Token' t:SA ∷ [] - cfg (statement Statement1) = Token' t:SB ∷ [] - cfg (statement Statement2) = Token' t:SC ∷ [] - cfg (statement Statement3) = Token' t:IF ∷ expr' ∷ statement' ∷ [] - cfg (statement Statement4) = Token' t:IF ∷ expr' ∷ statement' ∷ Token' t:ELSE ∷ statement' ∷ [] + term? : IFNode IFToken → IsTerm IFToken + term? (Token x) = isTerm x + term? _ = noTerm + cfg : IFNode IFToken → List ( List (IFNode IFToken) ) + cfg (Token t) = ( (Token t) ∷ [] ) ∷ [] + cfg expr = ( Token t:EA ∷ [] ) ∷ + ( Token t:EB ∷ [] ) ∷ + ( Token t:EC ∷ [] ) ∷ [] + cfg statement = ( Token t:SA ∷ [] ) ∷ + ( Token t:SB ∷ [] ) ∷ + ( Token t:SC ∷ [] ) ∷ + ( Token t:IF ∷ expr ∷ statement ∷ [] ) ∷ + ( Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ [] ) ∷ [] open CFGGrammer +----------------- +-- +-- CGF language +-- +----------------- + split : {Σ : Set} → (List Σ → Bool) → ( List Σ → Bool) → List Σ → Bool split x y [] = x [] ∧ y [] @@ -189,45 +158,45 @@ split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t -cfg-language0 : {Node Node' Token : Set} → CFGGrammer Token Node Node' → List Node → List Token → Bool +cfg-language0 : {Node Token : Set} → CFGGrammer Token Node → List (List Node ) → List Token → Bool {-# TERMINATING #-} -cfg-language2 : {Node Node' Token : Set} → CFGGrammer Token Node Node' → Node' → List Token → Bool +cfg-language2 : {Node Token : Set} → CFGGrammer Token Node → Node → List Token → Bool cfg-language2 cg _ [] = false cfg-language2 cg x (h1 ∷ [] ) with term? cg x cfg-language2 cg x (h1 ∷ []) | isTerm t with cmp cg h1 t cfg-language2 cg x (h1 ∷ []) | isTerm t | yes refl = true cfg-language2 cg x (h1 ∷ []) | isTerm t | no ¬p = false -cfg-language2 cg x (h1 ∷ []) | noTerm = cfg-language0 cg (list cg x ) ( h1 ∷ [] ) +cfg-language2 cg x (h1 ∷ []) | noTerm = cfg-language0 cg (cfg cg x) ( h1 ∷ [] ) cfg-language2 cg x In with term? cg x cfg-language2 cg x In | isTerm t = false -cfg-language2 cg x In | noTerm = cfg-language0 cg (list cg x ) In +cfg-language2 cg x In | noTerm = cfg-language0 cg (cfg cg x ) In -cfg-language1 : {Node Node' Token : Set} → CFGGrammer Token Node Node' → List Node' → List Token → Bool +cfg-language1 : {Node Token : Set} → CFGGrammer Token Node → List Node → List Token → Bool cfg-language1 cg [] [] = true cfg-language1 cg [] _ = false cfg-language1 cg (node ∷ T) = split ( cfg-language2 cg node ) ( cfg-language1 cg T ) - cfg-language0 cg [] [] = true cfg-language0 cg [] _ = false -cfg-language0 cg (node ∷ T) In = cfg-language1 cg (cfg cg node) In ∨ cfg-language0 cg T In - +cfg-language0 cg (node ∷ T) In = cfg-language1 cg node In ∨ cfg-language0 cg T In -cfg-language : {Node Node' Token : Set} → CFGGrammer Token Node Node' → List Token → Bool -cfg-language cg = cfg-language0 cg (list cg (cfgtop cg)) +cfg-language : {Node Token : Set} → CFGGrammer Token Node → List Token → Bool +cfg-language cg = cfg-language0 cg (cfg cg (cfgtop cg)) + +----------------- cgftest1 = cfg-language IFGrammer ( t:SA ∷ [] ) -cgftest2 = cfg-language2 IFGrammer (Token' t:SA) ( t:SA ∷ [] ) +cgftest2 = cfg-language2 IFGrammer (Token t:SA) ( t:SA ∷ [] ) -cgftest3 = cfg-language1 IFGrammer (Token' t:SA ∷ [] ) ( t:SA ∷ [] ) +cgftest3 = cfg-language1 IFGrammer (Token t:SA ∷ [] ) ( t:SA ∷ [] ) cgftest4 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:SA ∷ [] ) -cgftest5 = cfg-language1 IFGrammer (Token' t:IF ∷ expr' ∷ statement' ∷ []) (t:IF ∷ t:EA ∷ t:EA ∷ [] ) -cgftest6 = cfg-language2 IFGrammer statement' (t:IF ∷ t:EA ∷ t:SA ∷ [] ) -cgftest7 = cfg-language1 IFGrammer (Token' t:IF ∷ expr' ∷ statement' ∷ Token' t:ELSE ∷ statement' ∷ []) (t:IF ∷ t:EA ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) +cgftest5 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:EA ∷ [] ) +cgftest6 = cfg-language2 IFGrammer statement (t:IF ∷ t:EA ∷ t:SA ∷ [] ) +cgftest7 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) cgftest8 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] )