Mercurial > hg > Members > kono > Proof > automaton

changeset 6:8e8bca295494

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
regex wrote
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Aug 2018 11:59:36 +0900
parents f3de819eb3d0
children f1fbe6603066
files agda/regex.agda
diffstat 1 files changed, 29 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regex.agda	Wed Aug 15 11:25:46 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 11:59:36 2018 +0900
@@ -14,7 +14,7 @@
    _*    : Regex  Σ → Regex  Σ
    _&_   : Regex  Σ → Regex  Σ → Regex Σ
    _||_   : Regex  Σ → Regex  Σ → Regex Σ
-   <_>  : List   Σ → Regex  Σ
+   <_>  : Σ → Regex  Σ
 
 
 -- data  In2   : Set  where
@@ -54,12 +54,11 @@
       record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; RSTend = true } ;
                                 Rend = record { state = 0 ; move = λ q → [] ; RSTend = true }  ; Rnum = 1 } )
  where
-  listcase :  Maybe Σ →  List Σ → ℕ → List ℕ
-  listcase nothing _ _ = []
-  listcase (just q) [] n = []
-  listcase (just q) ( q'  ∷ t )  n with q ≟  q'
+  literal :  Maybe Σ →  Σ → ℕ → List ℕ
+  literal nothing _ _ = []
+  literal (just q)  q' n with q ≟  q'
   ... | yes _ = [ n ]
-  ... | no _ = listcase (just q) t n
+  ... | no _ = []
   generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ 
   generate (x *) R = record R' { Rstart =  record (Rstart R') { move = move0  }   ;
                                  Rend   =  record (Rend R')   { move = move1  }   }
@@ -78,19 +77,15 @@
        R2 : RNFA Σ 
        R2 = generate y R
        R1 : RNFA Σ 
-       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 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 )
+       R1 = generate x ( record R2 {  Rstart = Rstart R2 ; Rend = Rstart R2 } )
   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 :  RNFA  Σ 
+       R1 = generate x (  record R { Rnum = Rnum R + 1 } )
        S1 : RST Σ
-       S1 = record { state = Rnum R ; RSTend = RSTend R ; move  = λ q → [] }
-       R1 = generate x (  record R { Rnum = Rnum R +1 } )
+       S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move  = λ q → [] }
+       R2 :  RNFA  Σ
        R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1  } )
        move0 : Maybe Σ → List ℕ
        move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
@@ -102,16 +97,29 @@
        Rnum = Rnum R + 1 ;
        Rstart = record {
                state  = Rnum R
-             ; move = λ q → listcase q x ( state (Rstart R) )
+             ; move = λ q → literal q x ( state (Rstart R) )
              ; RSTend = false
-            }
-       Rstates =  Rstart R  ∷  Rstate R }
+            } ;
+       Rstates =  Rstart R  ∷  Rstates R }
+
+moveRegex : { Σ : Set } → List (RST Σ)  → ( RST Σ → ℕ )  → RST  Σ  → Maybe Σ →   List (RST  Σ)
+moveRegex { Σ} L sid s i = toRST ( move s i )
+   where
+       toRST : List ℕ → List ( RST  Σ )
+       toRST [] = []
+       toRST (h  ∷ t ) with findSbyNum h L sid
+       ... | nothing = toRST t 
+       ... | just s = s ∷ toRST t 
+
 
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {
-      εδ = λ s i → {!!} -- move s i
+      εδ = moveRegex ( Rstates G ) state
     ; εid = λ s → state s
-    ; allState = Rstates ( generateRNFA regex ieq )
-    ; εstart =  {!!} -- Rstart ( generateRNFA regex ieq )
+    ; allState = Rstates G
+    ; εstart =   Rstart G
     ; εend = λ s → RSTend s }
+      where
+          G : RNFA In2
+          G =  generateRNFA regex ieq