--- a/agda/regex.agda	Wed Aug 15 11:59:36 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 14:37:11 2018 +0900
@@ -3,7 +3,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 -- open import Data.Fin
 open import Data.Nat
-open import Data.List 
+-- open import Data.List 
 open import Data.Maybe 
 open import Data.Bool using ( Bool ; true ; false )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
@@ -26,9 +26,10 @@
 
 record RST ( Σ : Set )
      : Set where
+   inductive
    field
       state :  ℕ
-      move  :  Maybe Σ → List ℕ
+      move  :  Maybe Σ → Tree (RST Σ)
       RSTend : Bool
 
 open RST
@@ -36,28 +37,37 @@
 record RNFA ( Σ : Set )
      : Set where
    field
-      Rstates : List ( RST Σ )
+      Rstates : Tree ( RST Σ )
       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
+[_] : { Σ : Set} → RST Σ  → Tree (RST Σ )
+[ x ] = leaf ( state x ) x
+
+[] : { Σ : Set} → Tree (RST Σ )
+[] = empty
+
+
+infixr 5 _++_ 
+
+_++_ : { Σ : Set} → Tree (RST Σ ) → Tree (RST Σ ) → Tree (RST Σ )
+empty ++ t = t
+leaf n e ++ t = insertT n e t
+node n e left right ++ t =
+        left ++ ( insertT n e  (right ++ t ) )
 
 generateRNFA :  { Σ : Set  } → ( Regex  Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) →  RNFA  Σ
 generateRNFA  {Σ} regex _≟_ = generate regex (
       record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; RSTend = true } ;
                                 Rend = record { state = 0 ; move = λ q → [] ; RSTend = true }  ; Rnum = 1 } )
  where
-  literal :  Maybe Σ →  Σ → ℕ → List ℕ
-  literal nothing _ _ = []
+  literal :  Maybe Σ →  Σ → ℕ → Tree (RST  Σ)
+  literal nothing  q' n = []
   literal (just q)  q' n with q ≟  q'
-  ... | yes _ = [ n ]
+  ... | yes _ = [ record { state = n ; move = λ i → empty ; RSTend = true  } ]
   ... | no _ = []
   generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ 
   generate (x *) R = record R' { Rstart =  record (Rstart R') { move = move0  }   ;
@@ -65,12 +75,12 @@
     where
        R' : RNFA Σ 
        R' = generate x R
-       move0 : Maybe Σ → List ℕ
-       move0 nothing = mergeℕ (move (Rstart R') nothing) [ state (Rend R') ]
+       move0 : Maybe Σ → Tree (RST  Σ)
        move0 (just x) =  move (Rstart R') (just x )
-       move1 : Maybe Σ → List ℕ
-       move1 nothing = mergeℕ (move (Rstart R') nothing) (  state (Rend R')  ∷ state (Rend R')  ∷ [] ) 
+       move0 nothing = move (Rstart R') nothing ++ [ Rend R' ]
+       move1 : Maybe Σ → Tree (RST  Σ)
        move1 (just x) =  move (Rstart R') (just x )
+       move1 nothing = move (Rstart R') nothing ++  [ Rstart R' ]  ++ [ Rend R'  ]
   generate (x & y) R = record R1 { Rend = Rend R2 ;
                                    Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
     where
@@ -87,12 +97,12 @@
        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) ]
+       move0 : Maybe Σ → Tree (RST  Σ)
        move0 (just x) =  move (Rstart R1) (just x )
-       move1 : Maybe Σ → List ℕ
-       move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
+       move0 nothing = move (Rstart R1) nothing ++ [ Rstart R2 ]
+       move1 : Maybe Σ → Tree (RST  Σ)
        move1 (just x) =  move (Rend R1) (just x )
+       move1 nothing = move (Rend R1) nothing ++ [ Rend R2 ]
   generate < x > R = record R {
        Rnum = Rnum R + 1 ;
        Rstart = record {
@@ -100,21 +110,12 @@
              ; move = λ q → literal q x ( state (Rstart R) )
              ; RSTend = false
             } ;
-       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 
-
+       Rstates =  [ Rstart R ] ++ Rstates R 
+     }
 
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {
-      εδ = moveRegex ( Rstates G ) state
+      εδ =  move 
     ; εid = λ s → state s
     ; allState = Rstates G
     ; εstart =   Rstart G