# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1545409803 -32400
# Node ID ae69102153a9c56a3177fc114db79f61f87a0fc4
# Parent  6f747411fd6df5e7c06069cc995a997cda3ab5ea
cfg done

diff -r 6f747411fd6d -r ae69102153a9 agda/cfg.agda
--- a/agda/cfg.agda	Fri Dec 21 23:06:32 2018 +0900
+++ b/agda/cfg.agda	Sat Dec 22 01:30:03 2018 +0900
@@ -13,18 +13,19 @@
 
 open import nfa
 
-record CFGGrammer (Node Node' : Set ) : Set where
+data IsTerm (Token : Set) : Set where
+    isTerm :  Token → IsTerm Token
+    noTerm  : IsTerm Token
+
+record CFGGrammer (Token : Set) (Node Node' : Set ) : Set (succ Zero) where
    field
       cfg : Node → List ( Node' )
       cfgmap : Node →  Node' 
       cfgtop : Node' 
       list : Node' → List Node 
+      term? :  Node' → IsTerm Token
+      cmp :  (x y : Token ) → Dec ( x  ≡  y )
 
-record DFGGrammer ( Node Node' : Set )  : Set where
-   field
-      dfg : List Node → List Node'
-      dfgmap : Node →  Node' 
-   
 data IFToken : Set where
    t:EA : IFToken
    t:EB : IFToken
@@ -39,6 +40,7 @@
 -- tokenizer : {Σ : Set} → List Σ  →  IFToken  
 -- tokenizer = {!!}
 
+
 data Expr : Set where
    Expr0 : Expr
    Expr1 : Expr
@@ -61,42 +63,15 @@
    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 ∷ []
 
-IFGrammer : CFGGrammer (IFNode IFToken)  (IFNode' IFToken)
-IFGrammer = record {
-      cfg = cfg
-    ; cfgmap = cfgmap
-    ; cfgtop = cfgtop
-    ; list = list-IFGrammer
-   } 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' ∷ []
-
-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
@@ -180,26 +155,79 @@
 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
+IFGrammer : CFGGrammer IFToken (IFNode IFToken)  (IFNode' IFToken)
+IFGrammer = record {
+      cfg = cfg
+    ; cfgmap = cfgmap
+    ; cfgtop = cfgtop
+    ; list = list-IFGrammer
+    ; term? = isTerm-IFGRammer
+    ; 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' ∷ []
+
+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
+
+
+cfg-language0 :  {Node Node' Token : Set} → CFGGrammer Token Node Node' → List Node →  List Token → 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-language2 : {Node Node' Token : Set} → CFGGrammer Token Node 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 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-language1 : CFGGrammer (IFNode IFToken)  (IFNode' IFToken) → List (IFNode' IFToken) →  List IFToken → Bool
+cfg-language1 : {Node Node' Token : Set} → CFGGrammer Token Node 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-language : CFGGrammer (IFNode IFToken)  (IFNode' IFToken) →  List IFToken → Bool
+
+cfg-language : {Node Node' Token : Set} → CFGGrammer Token Node Node' →  List Token → Bool
 cfg-language cg = cfg-language0 cg (list cg (cfgtop cg))
 
+cgftest1 = cfg-language IFGrammer (  t:SA ∷ [] ) 
 
+cgftest2 = cfg-language2 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  ∷ [] ) 
+
+cgftest8 = cfg-language IFGrammer  (t:IF  ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE  ∷ t:SB  ∷ [] ) 
+
diff -r 6f747411fd6d -r ae69102153a9 agda/regex1.agda
--- a/agda/regex1.agda	Fri Dec 21 23:06:32 2018 +0900
+++ b/agda/regex1.agda	Sat Dec 22 01:30:03 2018 +0900
@@ -40,7 +40,7 @@
       → ( 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
+  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
 {-# TERMINATING #-}
 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool