Mercurial > hg > Members > kono > Proof > automaton

changeset 11:8e66865fd9af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix sbconst
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Aug 2018 11:44:41 +0900
parents 32fea87e21b8
children 5998479bb4ee
files agda/regex.agda agda/sbconst.agda
diffstat 2 files changed, 35 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regex.agda	Thu Aug 23 16:33:53 2018 +0900
+++ b/agda/regex.agda	Fri Aug 24 11:44:41 2018 +0900
@@ -117,11 +117,17 @@
        Rstates =  [ Rstart R ] ++ Rstates R 
      }
 
+In2toℕ : In2 → ℕ
+In2toℕ i1 = zero
+In2toℕ i2 = 1
+
+
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {
       εδ =  move 
     ; all-εδ =  cond1
     ; εid = λ s → state s
+    ; Σid = λ s → In2toℕ s
     ; allState = Rstates G
     ; εstart =   Rstart G
     ; εend = λ s → RSTend s }
--- a/agda/sbconst.agda	Thu Aug 23 16:33:53 2018 +0900
+++ b/agda/sbconst.agda	Fri Aug 24 11:44:41 2018 +0900
@@ -62,6 +62,7 @@
 
 -- all inputs are exclusive each other ( only one input can happen )
 
+-- merge Tree ( Maybe Σ × Tree Q ) 
 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
@@ -82,46 +83,43 @@
 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 )
-... | 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 )
-sbconst13 NFA (node x (_ , q) left right) t n | false = p2
+-- merge and find new state from newly created Tree ( Maybe Σ × Tree Q ) 
+sbconst13 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) →  Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  Tree ( Tree Q )  × Tree ( Tree Q )  × ℕ ) 
+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 )
+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 | false = p2
   where
-    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 = (  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
-    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
-sbconst11 NFA (node x q left right ) t n = p2
+    p1 = sbconst13 NFA left nt t n
+    p2 = sbconst13 NFA right (insertT (n + 1 ) q ( proj₁ p1 )) {!!} {!!}
+-- 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 = {!!}
   where
     p1 = sbconst11 NFA left  t n
-    p2 = sbconst11 NFA right ( proj₁  ( proj₂ ( sbconst12 NFA q t n))) (  proj₁ p1 )
+    p2 = sbconst11 NFA right ( proj₁  ( proj₂ {!!}) (  proj₁ p1 ))
        
 {-# TERMINATING #-}
-sbconst0 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  →  ( ℕ  ×  Tree ( Tree  Q ) )
+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)
-... | n , empty , t2 =  (n , t2 )
-... | n , leaf x y , t2 = sbconst0 NFA (  proj₁  ( proj₂ p1 ))    (leaf x y) (proj₁ p1) 
+... | t2 , empty , n =  (t2 , n )
+... | t2 , leaf x y , n = sbconst0 NFA (  proj₁  ( proj₂ p1 ))    (leaf x y) ({!!} p1) 
        where
          p1 = sbconst11 NFA (leaf x y) t1 n0
-... | n , node x y left right , t2 = p3
+... | t2 , node x y left right , n = p3
        where
          p1 = sbconst0 NFA left t2 n
-         p2 = sbconst11 NFA (leaf x y) ( proj₂ p1 ) (  proj₁  p1 ) 
+         p2 = sbconst11 NFA (leaf x y) ( {!!} p1 ) (  {!!}  p1 ) 
          p3 = sbconst0 NFA right ( proj₁  ( proj₂ p2))  n
 
 nfa2dfa : { Σ Q : Set } →  εAutomaton Q Σ →  Automaton (Tree Q) Σ
@@ -134,7 +132,7 @@
       MTree :  { Σ Q : Set } →  (x : εAutomaton Q Σ) →  Tree ( Tree  Q )
       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)
+      sbconst NFA =  proj₁ (sbconst0 NFA ( MTree NFA ) (MTree NFA) zero)
       δ' : Tree Q → Σ → Tree Q
       δ' t x with findT t ( MTree NFA )
       ... | nothing = leaf zero ( εstart NFA )   -- can't happen