Mercurial > hg > Members > kono > Proof > automaton

changeset 12:5998479bb4ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sbconst done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Aug 2018 13:08:14 +0900
parents 8e66865fd9af
children 02b4ecc9972c
files agda/sbconst.agda
diffstat 1 files changed, 33 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/agda/sbconst.agda	Fri Aug 24 11:44:41 2018 +0900
+++ b/agda/sbconst.agda	Fri Aug 24 13:08:14 2018 +0900
@@ -88,39 +88,42 @@
 sbconst13 NFA empty nt t n = (nt , t , n)
 sbconst13 NFA (leaf x (p , q)) nt t n with memberTT q t
 ... | true = ( nt , t , n)
-... | false = ( {!!} , {!!} , n + 1 )
+... | false = ( insertT n q nt , insertT n q t , n + 1 )
 sbconst13 NFA (node x (_ , q) left right) nt t n with memberTT q t
-sbconst13 NFA (node x (_ , q) left right) nt t n | true = ( empty , {!!} , {!!} )
+sbconst13 NFA (node x (_ , q) left right) nt t n | true = ( nt , t , n )
 sbconst13 NFA (node x (_ , q) left right) nt t n | false = p2
   where
     p1 = sbconst13 NFA left nt t n
-    p2 = sbconst13 NFA right (insertT (n + 1 ) q ( proj₁ p1 )) {!!} {!!}
+    n1 =  proj₂ ( proj₂ p1 )
+    p2 = sbconst13 NFA right (insertT n1 q ( proj₁ p1 )) (insertT n1 q ( proj₁ (proj₂ p1))) (n1 + 1 )
 -- expand state to Tree ( Maybe Σ × Tree Q )
 sbconst12 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree  Q  → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q )
 sbconst12 NFA empty  s  = s
 sbconst12 NFA (leaf x q) s  = merge-εδ NFA s (all-εδ NFA q)
 sbconst12 NFA (node x q left right) s = sbconst12 NFA right (merge-εδ NFA (all-εδ NFA q) (sbconst12 NFA left s))
 -- loop on state tree
-sbconst11 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  Tree ( Tree Q )  × Tree ( Tree  Q ) ×  ℕ )
-sbconst11 NFA empty t n = (empty , t , n )
-sbconst11 NFA (leaf x q) t n = {!!} -- sbconst13 NFA (sbconst12 NFA q empty ) t n
-sbconst11 NFA (node x q left right ) t n = {!!}
+sbconst11 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q )  → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  Tree ( Tree Q )  × Tree ( Tree  Q ) ×  ℕ )
+sbconst11 NFA empty nt t n = (nt , t , n )
+sbconst11 NFA (leaf x q) nt t n = sbconst13 NFA (sbconst12 NFA q empty ) nt t n
+sbconst11 NFA (node x q left right ) nt t n = p3
   where
-    p1 = sbconst11 NFA left  t n
-    p2 = sbconst11 NFA right ( proj₁  ( proj₂ {!!}) (  proj₁ p1 ))
+    p1 = sbconst11 NFA left nt t n
+    p2 = sbconst13 NFA (sbconst12 NFA q empty ) (  proj₁ p1 ) ( proj₁  ( proj₂ p1 ) ) ( proj₂  ( proj₂ p1 ) )
+    p3 = sbconst11 NFA right ( proj₁ p2 ) ( proj₁  ( proj₂ p2 )) ( proj₂  ( proj₂ p2 )) 
        
 {-# TERMINATING #-}
 sbconst0 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  →  ( Tree ( Tree  Q )  ×  ℕ )
-sbconst0 NFA t t1 n0 with sbconst11 NFA t t1 (lengthT t)
+sbconst0 NFA t t1 n0 with sbconst11 NFA t t1 empty n0
 ... | t2 , empty , n =  (t2 , n )
-... | t2 , leaf x y , n = sbconst0 NFA (  proj₁  ( proj₂ p1 ))    (leaf x y) ({!!} p1) 
+... | t2 , leaf x y , n = sbconst0 NFA ( proj₁  ( proj₂ p1 ))  (leaf x y) ( proj₂  ( proj₂ p1 ) )
        where
-         p1 = sbconst11 NFA (leaf x y) t1 n0
-... | t2 , node x y left right , n = p3
+         p1 = sbconst11 NFA (leaf x y) t1 empty n
+... | t2 , node x y left right , n = p4
        where
          p1 = sbconst0 NFA left t2 n
-         p2 = sbconst11 NFA (leaf x y) ( {!!} p1 ) (  {!!}  p1 ) 
-         p3 = sbconst0 NFA right ( proj₁  ( proj₂ p2))  n
+         p2 = sbconst11 NFA (leaf x y) (  proj₁  p1 ) empty (  proj₂ p1 ) 
+         p3 = sbconst0 NFA right ( proj₁  p2 ) ( proj₂  ( proj₂ p2 ))
+         p4 = sbconst0 NFA ( proj₁ ( proj₂ p2 )) ( proj₁  p3) ( proj₂  p3 )
 
 nfa2dfa : { Σ Q : Set } →  εAutomaton Q Σ →  Automaton (Tree Q) Σ
 nfa2dfa {Σ} {Q} NFA = record {
@@ -133,10 +136,24 @@
       MTree {Σ} {Q} NFA = εclosure (allState NFA ) (  εδ NFA )
       sbconst :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Tree  Q )
       sbconst NFA =  proj₁ (sbconst0 NFA ( MTree NFA ) (MTree NFA) zero)
+      δ0 : Σ → Tree ( Maybe Σ × Tree Q ) → Tree Q
+      δ0 x empty = empty
+      δ0 x (leaf x₁ q) with  Σid NFA x ≟  x₁
+      ... | no ¬p = empty
+      ... | yes p with  proj₁ q
+      ...     | nothing = empty
+      ...     | just _ = proj₂ q
+      δ0 x (node x₁ q left right) with  Σid NFA x ≟  x₁ 
+      ... | no ¬p with δ0 x left
+      ...    | empty = δ0 x right
+      ...    | q1 = q1
+      δ0 x (node x₁ q left right) | yes p with  proj₁ q
+      ...     | nothing = empty
+      ...     | just _ = proj₂ q
       δ' : Tree Q → Σ → Tree Q
       δ' t x with findT t ( MTree NFA )
       ... | nothing = leaf zero ( εstart NFA )   -- can't happen
-      ... | just q  = {!!} -- nextstate q zero empty
+      ... | just q  = δ0 x  (sbconst12 NFA q empty)
       astart' : Tree Q
       astart' =  leaf zero ( εstart NFA )
       aend' : Tree Q → Bool