module regex where

open import Level renaming ( suc to succ ; zero to Zero )
-- open import Data.Fin
open import Data.Nat
open import Data.Product
-- open import Data.List
open import Data.Maybe
open import Data.Bool using ( Bool ; true ; false )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)


data Regex   ( Σ : Set  ) : Set  where
   _*    : Regex  Σ → Regex  Σ
   _&_   : Regex  Σ → Regex  Σ → Regex Σ
   _||_   : Regex  Σ → Regex  Σ → Regex Σ
   <_>  : Σ → Regex  Σ


-- data  In2   : Set  where
--    a : In2
--    b : In2

open import automaton
open import epautomaton


record RST ( Σ : Set )
     : Set where
   inductive
   field
      state :  ℕ
      move  :  Maybe Σ → Tree (RST Σ)
      cond  :  Maybe Σ
      RSTend : Bool

open RST

record RNFA ( Σ : Set )
     : Set where
   field
      Rstates : Tree ( RST Σ )
      Rstart :   RST Σ
      Rend :   RST Σ
      Rnum :  ℕ

open RNFA

[_] : { Σ : Set} → RST Σ  → Tree (RST Σ )
[ x ] = leaf ( state x ) x

[] : { Σ : Set} → Tree (RST Σ )
[] = empty


infixr 5 _++_

_++_ : { Q : Set} → Tree Q → Tree Q → Tree Q
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 → [] ; cond = nothing ; RSTend = true } ;
                                Rend = record { state = 0 ; move = λ q → [] ; cond = nothing ; RSTend = true }  ; Rnum = 1 } )
 where
  literal :  Maybe Σ →  Σ → ℕ → Tree (RST  Σ)
  literal nothing  q' n = []
  literal (just q)  q' n with q ≟  q'
  ... | yes _ = [ record { state = n ; move = λ i → empty ; cond = nothing ; RSTend = true  } ]
  ... | no _ = []
  generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ
  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 Σ → Tree (RST  Σ)
       move0 (just x) =  move (Rstart R') (just x )
       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
       R2 : RNFA Σ
       R2 = generate y R
       R1 : RNFA Σ
       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 (Rend R) ; move  = λ q → [] ; cond = nothing }
       R2 :  RNFA  Σ
       R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1  } )
       move0 : Maybe Σ → Tree (RST  Σ)
       move0 (just x) =  move (Rstart R1) (just x )
       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 {
               state  = Rnum R
             ; move = λ q → literal q x ( state (Rstart R) )
             ; cond = just x
             ; RSTend = false
            } ;
       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 }
      where
          G : RNFA In2
          G =  generateRNFA regex ieq
          GTree :  Tree ( Tree (RST In2) )
          GTree = εclosure (Rstates G) move
          cond2 : Maybe (Tree (RST In2) )  → Tree (Maybe In2 × Tree (RST In2))
          cond2 nothing =  empty
          cond2 (just empty) = empty
          cond2 (just (leaf n r)) = leaf n (  cond r , move r ( cond r ) )
          cond2 (just (node n r left  right )) = cond2 (just left ) ++ leaf n (  cond r , move r ( cond r ) ) ++  cond2 (just right )
          cond1 : RST In2 → Tree (Maybe In2 × Tree (RST In2))
          cond1 s = cond2 ( memberT ( state s ) GTree )