Mercurial > hg > Members > kono > Proof > automaton

changeset 275:7828beb7d849

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 Sat, 18 Dec 2021 19:34:19 +0900
parents 1c8ed1220489
children a14999c44cf9
files automaton-in-agda/src/cfg1.agda automaton-in-agda/src/pushdown.agda
diffstat 2 files changed, 95 insertions(+), 72 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/cfg1.agda	Sat Dec 18 16:27:46 2021 +0900
+++ b/automaton-in-agda/src/cfg1.agda	Sat Dec 18 19:34:19 2021 +0900
@@ -2,13 +2,14 @@
 
 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.Fin
+-- 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 logic
 
 --
 --   Java → Java Byte Code
@@ -52,8 +53,8 @@
 
 split : {Σ : Set} → (List Σ → Bool)
       → ( List Σ → Bool) → List Σ → Bool
-split x y  [] = x [] ∧ y []
-split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
+split x y  [] = x [] /\ y []
+split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
   split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
 
@@ -63,7 +64,7 @@
 cfg-language1 :  {Symbol  : Set} → CFGGrammer Symbol   → Seq Symbol  →  List Symbol → Bool
 cfg-language1 cg Error x = false
 cfg-language1 cg (S ， seq) x with typeof cg S
-cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eq? cg x x' ∧ cfg-language1 cg seq t
+cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eq? cg x x' /\ cfg-language1 cg seq t
 cfg-language1 cg (_ ， seq) [] | T x = false
 cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
 cfg-language1 cg (S ．) x with typeof cg S
@@ -73,7 +74,7 @@
 
 cfg-language0 cg _ [] = false
 cfg-language0 cg (rule ｜ b) x =
-     cfg-language1 cg rule x  ∨ cfg-language0 cg b x  
+     cfg-language1 cg rule x  \/ cfg-language0 cg b x  
 cfg-language0 cg (rule ；) x = cfg-language1 cg rule x  
 
 cfg-language :  {Symbol  : Set} → CFGGrammer Symbol   → List Symbol → Bool
@@ -181,25 +182,72 @@
 ecfgtest1 = cfg-language E1Grammer (  e1 ∷ [] )
 ecfgtest2 = cfg-language E1Grammer (  e[ ∷ e1 ∷ e] ∷ [] )
 ecfgtest3 = cfg-language E1Grammer (  e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] )
+ecfgtest4 = cfg-language E1Grammer (  e[ ∷ e1 ∷ [] )
 
 open import Function
 
-left : {t : Set } → List E1Token → ( List E1Token → t ) → t
-left ( e[ ∷ t ) next = next t
-left t next = next t 
+left : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
+left ( e[ ∷ t ) fail next = next t
+left t fail next = fail t 
 
-right : {t : Set } → List E1Token → ( List E1Token → t ) → t
-right ( e] ∷ t ) next = next t
-right t next = next t 
+right : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
+right ( e] ∷ t ) fail next = next t
+right t fail next = fail t 
 
 
 {-# TERMINATING #-}
-expr1 : {t : Set } → List E1Token → ( List E1Token → t ) → t
-expr1 ( e1 ∷ t ) next = next t
-expr1 ( expr ∷ t ) next = next t
-expr1 ( term  ∷ t ) next = next t
-expr1 x next = left x $ λ x → expr1 x $ λ x → right x $ next
+expr1 : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
+expr1 ( e1 ∷ t ) fail next = next t
+expr1 ( expr ∷ t ) fail next = next t
+expr1 ( term  ∷ t ) fail next = next t
+expr1 x fail next = left x fail $ λ x → expr1 x fail $ λ x → right x fail $ next
+
+cfgtest01  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x → ⟪ true , x ⟫ ) 
+cfgtest02  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x →  ⟪ true , x ⟫ )
+cfgtest03  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x →  ⟪ true , x ⟫ )
+
+open import pushdown
+
+data CG1 : Set where
+   ce : CG1
+   c1 : CG1
+
+pd  : CG1 → E1Token → CG1 → CG1 ∧ PushDown CG1
+pd c1 e[ s = ⟪ c1 , push c1 ⟫
+pd c1 e] c1 = ⟪ c1 , pop ⟫
+pd c1 e1 c1 = ⟪ c1 , none ⟫
+pd s expr s1 = ⟪ c1 , none ⟫
+pd s term s1 = ⟪ c1 , none ⟫
+pd s _ s1 = ⟪ ce , none ⟫
+
+pok  : CG1 → Bool
+pok c1  = true
+pok s  = false
 
-cfgtest01  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) (λ x → x )
-cfgtest02  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) (λ x → x )
-cfgtest03  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ e] ∷ [] ) (λ x → x )
+pnc : PushDownAutomaton CG1 E1Token CG1
+pnc = record {
+         pδ  = pd
+      ;  pempty = ce
+      ;  pok = pok
+   }  
+
+pda-ce-test1 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) []
+pda-ce-test2 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) []
+pda-ce-test3 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e1 ∷ e] ∷ e1 ∷ [] ) []
+
+record PNC : Set where
+  field
+    pnc-q  : CG1
+    pnc-st : List CG1
+
+open import Data.Unit
+
+{-# TERMINATING #-}
+expr1P : {n : Level } {t : Set n } → (x : List E1Token ) → PNC → ( fail : List E1Token → PNC → t ) → ( next : List E1Token → PNC → t ) → t
+expr1P x _ _ _ = {!!}
+
+expr1P-test : (x : List E1Token ) →  ⊤
+expr1P-test x = expr1P x record {pnc-q = c1 ; pnc-st = [] } (λ x p → {!!} ) (λ x p → {!!} )
+
+
+
--- a/automaton-in-agda/src/pushdown.agda	Sat Dec 18 16:27:46 2021 +0900
+++ b/automaton-in-agda/src/pushdown.agda	Sat Dec 18 19:34:19 2021 +0900
@@ -4,48 +4,47 @@
 open import Data.Nat
 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 Level renaming ( suc to succ ; zero to Zero )
-open import Data.Product
+-- open import Data.Product
+open import logic
 
 
 data PushDown   (  Γ : Set  ) : Set  where
    pop    : PushDown  Γ
    push   :  Γ → PushDown  Γ
+   none   :  PushDown  Γ
 
 
 record PushDownAutomaton ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
        : Set  where
     field
-        pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
+        pδ : Q → Σ →  Γ → Q ∧ ( PushDown  Γ )
         pok : Q → Bool
         pempty : Γ
-    pmoves :  Q → List  Γ  → Σ → ( Q × List  Γ )
+    pmoves :  Q → List  Γ  → Σ → ( Q ∧ List  Γ )
     pmoves q [] i with pδ q i pempty
-    pmoves q [] i | qn , pop = ( qn , [] )
-    pmoves q [] i | qn , push x = ( qn , ( x ∷  [] ) )
+    pmoves q [] i | ⟪ qn , pop ⟫ =  ⟪  qn , [] ⟫
+    pmoves q [] i | ⟪ qn , push x ⟫ =  ⟪ qn , ( x ∷  [] )  ⟫
+    pmoves q [] i | ⟪ qn , none ⟫ =  ⟪ qn ,  [] ⟫
     pmoves q (  H  ∷ T  ) i with pδ q i H
-    pmoves q (H ∷ T) i | qn , pop =  ( qn , T )
-    pmoves q (H ∷ T) i | qn , push x = ( qn , ( x ∷ H ∷ T) )
+    pmoves q (H ∷ T) i | ⟪ qn , pop ⟫ =  ⟪ qn , T  ⟫
+    pmoves q (H ∷ T) i | ⟪ qn , none ⟫ =  ⟪ qn , (H ∷ T)  ⟫
+    pmoves q (H ∷ T) i | ⟪ qn , push x ⟫ =  ⟪ qn ,  x ∷ H ∷ T  ⟫
 
     paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
     paccept q [] [] = pok q
     paccept q ( H  ∷ T) [] with pδ q H pempty
-    paccept q (H ∷ T) [] | qn , pop = paccept qn T []
-    paccept q (H ∷ T) [] | qn , push x = paccept qn T (x  ∷ [] )
+    paccept q (H ∷ T) [] | ⟪ qn , pop ⟫ = paccept qn T []
+    paccept q (H ∷ T) [] | ⟪ qn , none ⟫ = paccept qn T []
+    paccept q (H ∷ T) [] | ⟪ qn , push x ⟫ = paccept qn T (x  ∷ [] )
     paccept q [] (_ ∷ _ ) = false
     paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
-    ... | (nq , pop )     = paccept nq T ST
-    ... | (nq , push ns ) = paccept nq T ( ns  ∷  SH ∷ ST )
-
-
---  0011
---  00000111111
-inputnn : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
-inputnn zero {_} _ _ s = s
-inputnn (suc n) x y s = x  ∷ ( inputnn n x y ( y  ∷ s ) )       
+    ... | ⟪ nq , pop ⟫     = paccept nq T ST
+    ... | ⟪ nq , none ⟫    = paccept nq T (SH ∷ ST)
+    ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns  ∷  SH ∷ ST )
 
 
 data  States0   : Set  where
@@ -55,17 +54,15 @@
    i0 : In2
    i1 : In2
 
-test0 = inputnn 5 i0 i1 []
- 
 pnn : PushDownAutomaton States0 In2 States0
 pnn = record {
          pδ  = pδ
       ;  pempty = sr
       ;  pok = λ q → true
    } where
-        pδ  : States0 → In2 → States0 → States0 × PushDown States0
-        pδ sr i0 _ = (sr , push sr) 
-        pδ sr i1 _ = (sr , pop ) 
+        pδ  : States0 → In2 → States0 → States0 ∧ PushDown States0
+        pδ sr i0 _ = ⟪ sr , push sr ⟫
+        pδ sr i1 _ = ⟪ sr , pop  ⟫ 
 
 data  States1   : Set  where
    ss : States1
@@ -80,11 +77,11 @@
         pok1 :  States1 → Bool
         pok1 ss = false
         pok1 st = true
-        pδ  : States1 → In2 → States1 → States1 × PushDown States1
-        pδ ss i0 _ = (ss , push ss) 
-        pδ ss i1 _ = (st , pop) 
-        pδ st i0 _ = (st , push ss) 
-        pδ st i1 _ = (st , pop ) 
+        pδ  : States1 → In2 → States1 → States1 ∧ PushDown States1
+        pδ ss i0 _ = ⟪ ss , push ss ⟫ 
+        pδ ss i1 _ = ⟪ st , pop ⟫ 
+        pδ st i0 _ = ⟪ st , push ss ⟫ 
+        pδ st i1 _ = ⟪ st , pop  ⟫ 
 
 test1 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
 test2 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) []
@@ -94,25 +91,3 @@
 test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
 test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []
 
-open import Data.Empty
-
-test70 : (n : ℕ ) → (x : List In2) →  PushDownAutomaton.paccept pnn sr x [] ≡ true → inputnn n i0 i1 [] ≡ x
-test70 zero [] refl = refl
-test70 zero (x ∷ y) pa = ⊥-elim (test701 pa) where
-   test701 : PushDownAutomaton.paccept pnn sr (x ∷ y) [] ≡ true → ⊥
-   test701 pa with  PushDownAutomaton.pδ pnn sr x sr
-   ... | sr , pop = {!!}
-   ... | sr , push x = {!!}
-test70 (suc n) x pa = {!!}
-
-test71 : (n : ℕ ) → (x : List In2)  → inputnn n i0 i1 [] ≡ x →  PushDownAutomaton.paccept pnn sr x [] ≡ true
-test71 = {!!}
-
-test7 : (n : ℕ ) →  PushDownAutomaton.paccept pnn sr (inputnn n i0 i1 []) [] ≡ true
-test7 zero = refl
-test7 (suc n) with test7 n
-... | t = test7lem [] t where
-     test7lem : (x : List States0) → PushDownAutomaton.paccept pnn sr (inputnn n i0 i1 [])              x  ≡ true
-                                   → PushDownAutomaton.paccept pnn sr (inputnn n i0 i1 (i1 ∷ [])) (sr ∷ x) ≡ true
-     test7lem x with PushDownAutomaton.paccept pnn sr (inputnn (suc n) i0 i1 [])                (sr ∷ x)
-     ... | t2 = {!!}