--- a/agda/regex.agda	Wed Aug 15 03:37:57 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 04:51:04 2018 +0900
@@ -37,15 +37,22 @@
      : Set where
    field
       Rstates : List ( RST Σ )
-      Rstart :  ℕ
-      Rend :  ℕ
+      Rstart :   RST Σ
+      Rend :   RST Σ
       Rnum :  ℕ
 
 open RNFA
 
+mergeℕ :  List ℕ → List ℕ → List ℕ
+mergeℕ [] L = L
+mergeℕ (h ∷ t ) L with member h L
+... | true = mergeℕ t L
+... | false =  h  ∷  mergeℕ t L
+
 generateRNFA :  { Σ : Set  } → ( Regex  Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) →  RNFA  Σ
 generateRNFA  {Σ} regex _≟_ = generate regex (
-      record { Rstates = [ record { state = 0 ; move = λ q → [] ; RSTend = true } ] ; Rstart = 0 ; Rend = 0 ; Rnum = 1 } )
+      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 _ _ = []
@@ -54,15 +61,38 @@
   ... | yes _ = [ n ]
   ... | no _ = listcase (just q) t n
   generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ 
-  generate (x *) R = record R { Rstart = {!!} ; Rstates = Rstates R ++ ( {!!}  ∷  {!!}  ∷  [] ) }
-  generate (x & y) R = {!!}
-  generate (x || y) R = {!!}
+  generate (x *) R = record R' { Rstart =  record (Rstart R') { move = move0  }   ;
+                                 Rend   =  record (Rend R')   { move = move1  }   }
+    where
+       R' : RNFA Σ 
+       R' = generate x R
+       move0 : Maybe Σ → List ℕ
+       move0 nothing = mergeℕ (move (Rstart R') nothing) [ state (Rend R') ]
+       move0 (just x) =  move (Rstart R') (just x )
+       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 ;
+                                   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 = {!!} } } )
+       move0 : Maybe Σ → List ℕ
+       move0 nothing = mergeℕ (move (Rstart R2) nothing) [ state (Rend R2) ]
+       move0 (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 = {!!} } } )
   generate < x > R = record R {
        Rnum = Rnum R + 1 ;
        Rstates = Rstates R ++ (
             record {
                state  = Rnum R
-             ; move = λ q → listcase q x (Rstart R)
+             ; move = λ q → listcase q x ( state (Rstart R) )
              ; RSTend = false
             }   ∷  [] ) }