Mercurial > hg > Members > kono > Proof > automaton

changeset 10:32fea87e21b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge Σ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 23 Aug 2018 16:33:53 +0900
parents e7bb980408fb
children 8e66865fd9af
files agda/epautomaton.agda agda/sbconst.agda
diffstat 2 files changed, 54 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/agda/epautomaton.agda	Wed Aug 22 21:59:24 2018 +0900
+++ b/agda/epautomaton.agda	Thu Aug 23 16:33:53 2018 +0900
@@ -60,6 +60,7 @@
           εδ : Q → Maybe Σ → Tree Q
           all-εδ : Q → Tree ( Maybe Σ × Tree Q )
           εid : Q  →  ℕ
+          Σid : Σ  →  ℕ
           allState : Tree Q
           εstart : Q
           εend  : Q → Bool 
@@ -94,6 +95,7 @@
          closure (node n e left right) =
               node n (closure1 n) ( closure left ) ( closure right ) 
 
+
 εAutomaton2U : { Q : Set } { Σ : Set  }
     → εAutomaton Q  Σ → NAutomaton Q  Σ
 εAutomaton2U {Q} { Σ} M = record {
@@ -104,18 +106,16 @@
   } where
      MTree :  Tree ( Tree  Q )
      MTree = εclosure (allState M ) (  εδ M )
+     flatten :  Tree  Q → List Q
+     flatten empty = []
+     flatten (leaf x q) = [ q ]
+     flatten (node x q left right) = flatten left ++ [ q ] ++ flatten right
      nδ1 : Tree Q → Σ → List Q
      nδ1 empty i = []
-     nδ1 (leaf n q) i = [ q ]
-     nδ1 (node n q left right) i = nδ1 left i ++ [ q ] ++ nδ1 right i
+     nδ1 (leaf n q) i =  flatten (εδ M q (just i))
+     nδ1 (node n q left right) i = nδ1 left i ++ ( flatten (εδ M q (just i) )) ++ nδ1 right i
      nδ' : Q → Σ → List Q
      nδ' q i with memberT ( εid M q ) MTree
      ... | nothing = []
      ... | just x = nδ1 x i
 
-
-
-
-
-
-
--- a/agda/sbconst.agda	Wed Aug 22 21:59:24 2018 +0900
+++ b/agda/sbconst.agda	Thu Aug 23 16:33:53 2018 +0900
@@ -12,6 +12,10 @@
 open import automaton
 open import epautomaton
 
+
+-- all primitive state has id
+-- Tree Q is sorted by id and is contents are unique
+
 flatten : { Q : Set} → Tree Q  → List ℕ 
 flatten empty = []
 flatten (leaf x x₁) = [ x ]
@@ -29,7 +33,7 @@
 _==_ : { Q : Set} → Tree Q  → Tree Q → Bool
 x == y = listEq ( flatten x ) ( flatten y )
 
-memberTT : { Q : Set} →  Tree  Q  → Tree ( Tree  Q ) → Bool
+memberTT : { Q : Set} →  Tree Q  → Tree ( Tree  Q ) → Bool
 memberTT t empty  = false
 memberTT t (leaf x x₁) = t == x₁
 memberTT t (node x x₁ x₂ x₃) with t == x₁
@@ -48,27 +52,57 @@
 ...    | (just y) = just y
 ...    | nothing  = findT t x₃
 
+mergeT : { Q : Set} →  Tree Q  →  Tree  Q  →  Tree Q 
+mergeT empty t = t
+mergeT (leaf x t0) t = insertT x t0 t
+mergeT (node x t0  left right ) t =
+      mergeT left ( insertT x t0 (mergeT right t ))
+
 open εAutomaton
 
+-- all inputs are exclusive each other ( only one input can happen )
 
-sbconst13 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Tree  Q )  →  ℕ  → (  ℕ × Tree ( Tree Q )  × Tree ( Tree  Q ) )
-sbconst13 NFA empty t n = (n , empty , t )
+merge-itεδ : { Σ Q : Set } →  εAutomaton Q Σ → Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q ) 
+merge-itεδ NFA i t empty = leaf (Σid NFA i) ( just i , t ) 
+merge-itεδ NFA i t (leaf x (i' , t1 )) with (Σid NFA i) ≟ x
+... | no _ =  leaf x (i' , t1)
+... | yes _ = leaf x (just i , mergeT t t1  )
+merge-itεδ NFA i t (node x (i' , t1) left right ) with (Σid NFA i) ≟ x
+... | no _ = node x (i' , t1) ( merge-itεδ NFA i t left ) ( merge-itεδ NFA i t right )
+... | yes _ = node x (just i , mergeT t t1  )
+    ( merge-itεδ NFA i t left ) ( merge-itεδ NFA i t right )
+
+merge-iεδ : { Σ Q : Set } →  εAutomaton Q Σ → Maybe Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q ) 
+merge-iεδ NFA nothing _ t = t
+merge-iεδ NFA (just i) q t = merge-itεδ NFA i q t
+
+merge-εδ : { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q ) 
+merge-εδ NFA empty t = t
+merge-εδ NFA (leaf x (i , t1) ) t = merge-iεδ NFA i t1 t
+merge-εδ NFA (node x (i , t1) left right) t =
+       merge-εδ NFA left ( merge-iεδ NFA i t1 ( merge-εδ NFA right t ) )
+   
+
+sbconst13 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Tree  Q )  →  ℕ  → (  ℕ × Tree ( Tree Q )  ) 
+sbconst13 NFA empty t n = (n , empty )
 sbconst13 NFA (leaf x (p , q)) t n with memberTT q t
-... | true = ( n , empty , t )
-... | false = ( n + 1 , leaf x q , insertT x q t )
+... | true = ( n , empty )
+... | false = ( n + 1 , leaf x q )
 sbconst13 NFA (node x (_ , q) left right) t n with memberTT q t
-sbconst13 NFA (node x (_ , q) left right) t n | true = ( n , empty , t )
+sbconst13 NFA (node x (_ , q) left right) t n | true = ( n , empty )
 sbconst13 NFA (node x (_ , q) left right) t n | false = p2
   where
-    p1 = sbconst13 NFA left  t n
-    p2 = sbconst13 NFA right (insertT (n + 1 ) q (  proj₁  ( proj₂ p1 ) ) ) ( n + 1 )
+    p1 = sbconst13 NFA left t n
+    p2 = sbconst13 NFA right (insertT (n + 1 ) q ( proj₂ p1 )) (proj₁   p1 )
 sbconst12 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree  Q  → Tree ( Tree  Q )  →  ℕ  → (  ℕ × Tree ( Tree Q )  × Tree ( Tree  Q ) )
 sbconst12 NFA empty t n = ( n , empty , t )
-sbconst12 NFA (leaf x q) t n = sbconst13 NFA ( all-εδ NFA q) t n
+sbconst12 NFA (leaf x q) t n = (  n + 1 ,  proj₂ t1  , {!!} ( proj₂ t1)  t )
+    where t1 = sbconst13 NFA ( all-εδ NFA q) t zero
 sbconst12 NFA (node x q left right) t n = p2
   where
-    p1 = sbconst12 NFA left  t n
-    p2 = sbconst12 NFA right ( proj₁  ( proj₂ ( sbconst13 NFA ( all-εδ NFA q) t n))) (  proj₁ p1 )
+    t1 =  sbconst13 NFA ( all-εδ NFA q) t zero
+    p1 = sbconst12 NFA left  {!!} (  proj₁ t1 )
+    p2 = sbconst12 NFA right ( proj₁ (proj₂ p1)  )  (proj₁ p1 )
 sbconst11 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  ℕ × Tree ( Tree Q )  × Tree ( Tree  Q ) )
 sbconst11 NFA empty t n = (n , empty , t)
 sbconst11 NFA (leaf x q) t n = sbconst12 NFA q t n
@@ -104,7 +138,7 @@
       δ' : Tree Q → Σ → Tree Q
       δ' t x with findT t ( MTree NFA )
       ... | nothing = leaf zero ( εstart NFA )   -- can't happen
-      ... | just q  = {!!}
+      ... | just q  = {!!} -- nextstate q zero empty
       astart' : Tree Q
       astart' =  leaf zero ( εstart NFA )
       aend' : Tree Q → Bool