Mercurial > hg > Members > kono > Proof > automaton

changeset 5:f3de819eb3d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Aug 2018 11:25:46 +0900
parents 843f155846fb
children 8e8bca295494
files agda/automaton.agda agda/regex.agda
diffstat 2 files changed, 33 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Wed Aug 15 04:51:04 2018 +0900
+++ b/agda/automaton.agda	Wed Aug 15 11:25:46 2018 +0900
@@ -162,8 +162,18 @@
           εstart : Q
           εend  : Q → Bool 
 
+findSbyNum : {Q : Set } → ℕ → List Q → ( Q  →  ℕ )  → Maybe Q
+findSbyNum _ [] _ = nothing
+findSbyNum n ( s  ∷ t ) sid with sid s  ≟ n
+... | yes _ = just s
+... | no _ = findSbyNum n t sid
+
 open εAutomaton
 
+--
+--  find ε connected state by following ε transition
+--    keep track state list in C
+--    if already tracked, skip it
 εclosure : { Q : Set } { Σ : Set  }
     → εAutomaton Q  Σ
     → List ( List  ℕ )
@@ -178,7 +188,7 @@
          ... | false =  closure2 t ( (εid M n1)  ∷ C )
          ... | true  =  closure2 t C
          closure1 : ℕ →  List  ℕ 
-         closure1 n with nth n (allState  M)
+         closure1 n with findSbyNum n (allState  M) (εid M)
          ... | nothing = []
          ... | just q = closure2 (εδ M q nothing) [ n ]
          closure :  List  ℕ → List ( List  ℕ )
@@ -199,7 +209,7 @@
      DummyUA = record { nδ = λ n i → [] ;  sid = εid M ; nstart = εstart M  ; nend =  εend M  }
      nδ1 : List  ℕ → Σ → List Q
      nδ1 [] _ = []
-     nδ1 (h  ∷ t ) i with nth h ( allState  M)
+     nδ1 (h  ∷ t ) i with findSbyNum h ( allState  M) (εid M)
      ... | nothing =  nδ1 t i
      ... | just q = merge DummyUA ( εδ M q ( just i )) ( nδ1 t i )
      nδ' : Q → Σ → List Q
--- a/agda/regex.agda	Wed Aug 15 04:51:04 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 11:25:46 2018 +0900
@@ -40,7 +40,7 @@
       Rstart :   RST Σ
       Rend :   RST Σ
       Rnum :  ℕ
-
+   
 open RNFA
 
 mergeℕ :  List ℕ → List ℕ → List ℕ
@@ -72,30 +72,40 @@
        move1 : Maybe Σ → List ℕ
        move1 nothing = mergeℕ (move (Rstart R') nothing) (  state (Rend R')  ∷ state (Rend R')  ∷ [] ) 
        move1 (just x) =  move (Rstart R') (just x )
-  generate (x & y) R = record R1 { Rstart =  Rstart R1 ; Rend = Rend R2 ;
+  generate (x & y) R = record R1 { Rend = Rend R2 ;
                                    Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
     where
        R2 : RNFA Σ 
        R2 = generate y R
        R1 : RNFA Σ 
-       R1 = generate x ( record R2 {  Rnum = Rnum R2 + 1 ; Rend = Rstart R2 ; Rstart = record { state = Rnum R2  ; RSTend = false ; move = {!!} } } )
+       R1 = generate x ( record R2 {  Rstart = record (Rstart R1) { move = move0  } ; Rend = record (Rend R1) { move = move1 } } )
        move0 : Maybe Σ → List ℕ
-       move0 nothing = mergeℕ (move (Rstart R2) nothing) [ state (Rend R2) ]
-       move0 (just x) =  {!!}
+       move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
+       move0 (just x) =  move (Rstart R1) (just x )
+       move1 : Maybe Σ → List ℕ
+       move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
+       move1 (just x) =  move (Rend R1) (just x )
   generate (x || y) R =  record R1 { Rstart =  Rstart R1 ; Rend = Rend R2 ;
                                    Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] }
     where
-       R1 = generate x ( record R  {  Rnum = Rnum R  + 1 ; Rend = Rstart R  ; Rstart = record { state = Rnum R   ; RSTend = false ; move = {!!} } } )
-       R2 = generate y ( record R2 {  Rnum = Rnum R2 + 1 ; Rend = Rstart R2 ; Rstart = record { state = Rnum R2  ; RSTend = false ; move = {!!} } } )
+       S1 : RST Σ
+       S1 = record { state = Rnum R ; RSTend = RSTend R ; move  = λ q → [] }
+       R1 = generate x (  record R { Rnum = Rnum R +1 } )
+       R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1  } )
+       move0 : Maybe Σ → List ℕ
+       move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
+       move0 (just x) =  move (Rstart R1) (just x )
+       move1 : Maybe Σ → List ℕ
+       move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
+       move1 (just x) =  move (Rend R1) (just x )
   generate < x > R = record R {
        Rnum = Rnum R + 1 ;
-       Rstates = Rstates R ++ (
-            record {
+       Rstart = record {
                state  = Rnum R
              ; move = λ q → listcase q x ( state (Rstart R) )
              ; RSTend = false
-            }   ∷  [] ) }
-
+            }
+       Rstates =  Rstart R  ∷  Rstate R }
 
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {