Mercurial > hg > Members > kono > Proof > automaton

changeset 40:6f747411fd6d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 21 Dec 2018 23:06:32 +0900
parents 3f099f353f1c
children ae69102153a9
files agda/cfg.agda
diffstat 1 files changed, 168 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/agda/cfg.agda	Fri Dec 21 10:56:18 2018 +0900
+++ b/agda/cfg.agda	Fri Dec 21 23:06:32 2018 +0900
@@ -6,24 +6,24 @@
 open import Data.Product
 open import Data.List
 open import Data.Maybe
-open import Data.Bool using ( Bool ; true ; false )
+open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Data.String
+-- open import Data.String
 
 open import nfa
 
-data Node ( Term NonTerm : Set )  : Set  where
-   term : Term → Node Term NonTerm
-   nonterm : NonTerm → Node Term NonTerm
-
-record CFGGrammer (Node : Set ) : Set where
+record CFGGrammer (Node Node' : Set ) : Set where
    field
-      cfg : Node → List ( Node )
+      cfg : Node → List ( Node' )
+      cfgmap : Node →  Node' 
+      cfgtop : Node' 
+      list : Node' → List Node 
 
-record DFGGrammer ( Node : Set )  : Set where
+record DFGGrammer ( Node Node' : Set )  : Set where
    field
-      dfg : List Node → List Node 
+      dfg : List Node → List Node'
+      dfgmap : Node →  Node' 
    
 data IFToken : Set where
    t:EA : IFToken
@@ -36,33 +36,170 @@
    t:SB : IFToken
    t:SC : IFToken
 
-tokenizer : {Σ : Set} → List Σ  →  IFToken  
-tokenizer = {!!}
+-- 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 : (Fin 3) → IFNode T
-   Statement : (Fin 5) → IFNode T
+   expr : Expr → IFNode T
+   statement : Statement → IFNode T
 
-IFGrammer : CFGGrammer (IFNode IFToken)
+data IFNode' (T : Set) : Set where
+   Token' : T → IFNode' T
+   expr' : IFNode' T
+   statement' : IFNode' T
+
+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 ∷ []
+
+IFGrammer : CFGGrammer (IFNode IFToken)  (IFNode' IFToken)
 IFGrammer = record {
       cfg = cfg
+    ; cfgmap = cfgmap
+    ; cfgtop = cfgtop
+    ; list = list-IFGrammer
    } where
-     cfg :  IFNode IFToken → List (IFNode IFToken)
-     cfg (Token t) =  (Token t)  ∷ [] 
-     cfg (Expr zero) =  Token t:EA  ∷ [] 
-     cfg (Expr (suc zero)) =  Token t:EB  ∷ [] 
-     cfg (Expr (suc (suc zero))) =  Token t:EC  ∷ [] 
-     cfg (Expr (suc (suc (suc ()))))
-     cfg (Statement zero) = ( Token t:SA   ∷ [])
-     cfg (Statement (suc (zero))) = ( Token t:SB   ∷ [])
-     cfg (Statement (suc (suc zero))) = ( Token t:SC   ∷ [])
-     cfg (Statement (suc (suc (suc zero)))) = ( Token t:IF ∷ Expr {!!}  ∷ Statement {!!}  ∷ [])
-     cfg (Statement (suc (suc (suc (suc zero))))) = ( Token t:IF ∷ Expr {!!} ∷ Statement {!!}  ∷ Token t:ELSE ∷ Statement {!!}  ∷ [])
-     cfg (Statement (suc (suc (suc (suc (suc ())))))) 
+     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' ∷ []
+
+open CFGGrammer 
+
+split : {Σ : Set} → (List Σ → Bool)
+      → ( List Σ → Bool) → List Σ → Bool
+split x y  [] = x [] ∧ y []
+split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
+  split (λ t1 → x ( ( h ∷ [] ) ++ t1 ))  (λ t2 → y t2 ) t
+
+cmpi : (x y : IFToken ) → Dec ( x  ≡ y )
+cmpi t:EA t:EA = yes refl
+cmpi t:EB t:EB = yes refl
+cmpi t:EC t:EC = yes refl
+cmpi t:IF t:IF = yes refl
+cmpi t:THEN t:THEN = yes refl
+cmpi t:ELSE t:ELSE = yes refl
+cmpi t:SA t:SA = yes refl
+cmpi t:SB t:SB = yes refl
+cmpi t:SC t:SC = yes refl
+cmpi t:EA t:EB = no (λ ())
+cmpi t:EA t:EC = no (λ ())
+cmpi t:EA t:IF = no (λ ())
+cmpi t:EA t:THEN = no (λ ())
+cmpi t:EA t:ELSE = no (λ ())
+cmpi t:EA t:SA = no (λ ())
+cmpi t:EA t:SB = no (λ ())
+cmpi t:EA t:SC = no (λ ())
+cmpi t:EB t:EA = no (λ ())
+cmpi t:EB t:EC = no (λ ())
+cmpi t:EB t:IF = no (λ ())
+cmpi t:EB t:THEN = no (λ ())
+cmpi t:EB t:ELSE = no (λ ())
+cmpi t:EB t:SA = no (λ ())
+cmpi t:EB t:SB = no (λ ())
+cmpi t:EB t:SC = no (λ ())
+cmpi t:EC t:EA = no (λ ())
+cmpi t:EC t:EB = no (λ ())
+cmpi t:EC t:IF = no (λ ())
+cmpi t:EC t:THEN = no (λ ())
+cmpi t:EC t:ELSE = no (λ ())
+cmpi t:EC t:SA = no (λ ())
+cmpi t:EC t:SB = no (λ ())
+cmpi t:EC t:SC = no (λ ())
+cmpi t:IF t:EA = no (λ ())
+cmpi t:IF t:EB = no (λ ())
+cmpi t:IF t:EC = no (λ ())
+cmpi t:IF t:THEN = no (λ ())
+cmpi t:IF t:ELSE = no (λ ())
+cmpi t:IF t:SA = no (λ ())
+cmpi t:IF t:SB = no (λ ())
+cmpi t:IF t:SC = no (λ ())
+cmpi t:THEN t:EA = no (λ ())
+cmpi t:THEN t:EB = no (λ ())
+cmpi t:THEN t:EC = no (λ ())
+cmpi t:THEN t:IF = no (λ ())
+cmpi t:THEN t:ELSE = no (λ ())
+cmpi t:THEN t:SA = no (λ ())
+cmpi t:THEN t:SB = no (λ ())
+cmpi t:THEN t:SC = no (λ ())
+cmpi t:ELSE t:EA = no (λ ())
+cmpi t:ELSE t:EB = no (λ ())
+cmpi t:ELSE t:EC = no (λ ())
+cmpi t:ELSE t:IF = no (λ ())
+cmpi t:ELSE t:THEN = no (λ ())
+cmpi t:ELSE t:SA = no (λ ())
+cmpi t:ELSE t:SB = no (λ ())
+cmpi t:ELSE t:SC = no (λ ())
+cmpi t:SA t:EA = no (λ ())
+cmpi t:SA t:EB = no (λ ())
+cmpi t:SA t:EC = no (λ ())
+cmpi t:SA t:IF = no (λ ())
+cmpi t:SA t:THEN = no (λ ())
+cmpi t:SA t:ELSE = no (λ ())
+cmpi t:SA t:SB = no (λ ())
+cmpi t:SA t:SC = no (λ ())
+cmpi t:SB t:EA = no (λ ())
+cmpi t:SB t:EB = no (λ ())
+cmpi t:SB t:EC = no (λ ())
+cmpi t:SB t:IF = no (λ ())
+cmpi t:SB t:THEN = no (λ ())
+cmpi t:SB t:ELSE = no (λ ())
+cmpi t:SB t:SA = no (λ ())
+cmpi t:SB t:SC = no (λ ())
+cmpi t:SC t:EA = no (λ ())
+cmpi t:SC t:EB = no (λ ())
+cmpi t:SC t:EC = no (λ ())
+cmpi t:SC t:IF = no (λ ())
+cmpi t:SC t:THEN = no (λ ())
+cmpi t:SC t:ELSE = no (λ ())
+cmpi t:SC t:SA = no (λ ())
+cmpi t:SC t:SB = no (λ ())
+
+cfg-language0 : CFGGrammer (IFNode IFToken)  (IFNode' IFToken) → List (IFNode IFToken) →  List IFToken → Bool
+
+{-# TERMINATING #-}
+cfg-language2 : CFGGrammer (IFNode IFToken)  (IFNode' IFToken) → IFNode' IFToken  → List IFToken → Bool
+cfg-language2 cg (Token' x) [] = false
+cfg-language2 cg (Token' x) (h1  ∷ [] ) with cmpi x h1
+... | yes _ = true
+... | no _ = false
+cfg-language2 cg (Token' x) _ = false
+cfg-language2 cg expr' = cfg-language0 cg (list cg expr')
+cfg-language2 cg statement' =  cfg-language0 cg (list cg statement')
+
+cfg-language1 : CFGGrammer (IFNode IFToken)  (IFNode' IFToken) → List (IFNode' IFToken) →  List IFToken → Bool
+cfg-language1 cg [] _ = false
+cfg-language1 cg (node ∷ T) = split ( cfg-language2 cg node ) ( cfg-language1 cg T )
+
+cfg-language0 cg [] _ = false
+cfg-language0 cg (node ∷ T) In = cfg-language1 cg (cfg cg node) In ∨ cfg-language0 cg T In 
+
+cfg-language : CFGGrammer (IFNode IFToken)  (IFNode' IFToken) →  List IFToken → Bool
+cfg-language cg = cfg-language0 cg (list cg (cfgtop cg))
 
 
-cfg-language : {Σ : Set} → CFGGrammer {!!} → {n : ℕ } (fin : FiniteSet Σ {n}) →  List Σ → Bool
-cfg-language = {!!}
-
-