Mercurial > hg > Members > kono > Proof > automaton

changeset 43:31e4bd173951

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
using Fin id
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Dec 2018 03:08:21 +0900
parents bbb39677d5ab
children aa15eff1aeb3
files agda/cfg.agda
diffstat 1 files changed, 60 insertions(+), 128 deletions(-) [+]
line wrap: on
line diff
--- a/agda/cfg.agda	Sat Dec 22 02:23:34 2018 +0900
+++ b/agda/cfg.agda	Sat Dec 22 03:08:21 2018 +0900
@@ -1,6 +1,7 @@
 module cfg where
 
 open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat  hiding ( _≟_ )
 open import Data.Fin
 open import Data.Product
 open import Data.List
@@ -16,132 +17,13 @@
     isTerm :  Token → IsTerm Token
     noTerm  : IsTerm Token
 
-record CFGGrammer (Token Node : Set) : Set (succ Zero) where
+record CFGGrammer  (Token Node : Set) : Set (succ Zero) where
    field
       cfg : Node → List ( List ( Node ) )
       cfgtop : Node
       term? :  Node → IsTerm Token
-      cmp :  (x y : Token ) → Dec ( x  ≡  y )
-
-data IFToken : Set where
-   t:EA : IFToken
-   t:EB : IFToken
-   t:EC : IFToken
-   t:IF : IFToken
-   t:THEN : IFToken
-   t:ELSE : IFToken
-   t:SA : IFToken
-   t:SB : IFToken
-   t:SC : IFToken
-
-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 (λ ())
-
-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
-    ; cfgtop = statement
-    ; term? = term?
-    ; cmp = cmpi
-   } where
-     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 ∷ [] ) ∷  [] 
+      tokensz : ℕ
+      tokenid : Token → Fin tokensz
 
 open CFGGrammer 
 
@@ -158,21 +40,21 @@
   split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
 
-cfg-language0 :  {Node  Token : Set} → CFGGrammer Token Node  → List (List Node ) →  List Token → Bool
+cfg-language0 :  {Node  Token : Set} → CFGGrammer  Token Node  → List (List Node ) →  List Token → Bool
 
 {-# TERMINATING #-}
-cfg-language2 : {Node  Token : Set} → CFGGrammer Token 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 with tokenid cg h1 ≟ tokenid cg t
+cfg-language2 cg x (h1 ∷ []) | isTerm t | yes p = true
 cfg-language2 cg x (h1 ∷ []) | isTerm t | no ¬p = false
 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 (cfg cg x ) In
 
-cfg-language1 : {Node  Token : Set} → CFGGrammer Token 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 )
@@ -181,11 +63,61 @@
 cfg-language0 cg [] _ = false
 cfg-language0 cg (node ∷ T) In = cfg-language1 cg node In ∨ cfg-language0 cg T In 
 
-cfg-language : {Node  Token : Set} → CFGGrammer Token Node  →  List Token → Bool
+cfg-language :  {Node  Token : Set} → CFGGrammer  Token Node  →  List Token → Bool
 cfg-language cg = cfg-language0 cg (cfg cg (cfgtop cg))
 
 -----------------
 
+data IFToken : Set where
+   t:EA : IFToken
+   t:EB : IFToken
+   t:EC : IFToken
+   t:IF : IFToken
+   t:THEN : IFToken
+   t:ELSE : IFToken
+   t:SA : IFToken
+   t:SB : IFToken
+   t:SC : IFToken
+
+IFtokenid : IFToken → Fin 9
+IFtokenid t:EA = # 0
+IFtokenid t:EB = # 1
+IFtokenid t:EC = # 2
+IFtokenid t:IF = # 3
+IFtokenid t:THEN = # 4
+IFtokenid t:ELSE = # 5
+IFtokenid t:SA = # 6
+IFtokenid t:SB = # 7
+IFtokenid t:SC = # 8
+
+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'
+    ; cfgtop = statement
+    ; term? = term?'
+    ; tokensz = 9
+    ; tokenid = IFtokenid
+   } where
+     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 ∷ [] ) ∷  [] 
+
+
 cgftest1 = cfg-language IFGrammer (  t:SA ∷ [] ) 
 
 cgftest2 = cfg-language2 IFGrammer (Token t:SA) (  t:SA ∷ [] )