module regex where

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.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 Σ
   <_>  : List   Σ → Regex  Σ


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

open import automaton


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

open RST

record RNFA ( Σ : Set )
     : Set where
   field
      states : List ( RST Σ )
   map1  : ( List ( RST Σ ) ) → ℕ →  RST Σ 
   map1 [] _ ()
   map1 ( h ∷ t ) 0 = h
   map1 ( h ∷ t ) (suc n) = map1 t n
   map   :  ℕ →  RST Σ 
   map n =  map1 n states
   start :  RST Σ
   start = map 3

open RNFA

generateRNFA :  { Σ : Set  } → ( (q q' : Σ) → Dec ( q ≡  q' ))  →  ( Regex  Σ ) →  RNFA  Σ
generateRNFA  {Σ} _≟_ regex = record {
          start = generate regex true 2
              [ record { state = 0 ; move = λ q → [] ; RSTend = true } ]
              [ record { state = 1 ; move = λ q → [] ; RSTend = false } ]
       ;  end = λ s → RSTend s
    } where
  listcase :  Σ →  List Σ → List ( RST  Σ ) → List ( RST  Σ ) → List ( RST  Σ )
  listcase q [] ok else = else
  listcase q ( q'  ∷ t )  ok else with q ≟  q'
  ... | yes _ = ok
  ... | no _ = listcase q t ok else
  generate : ( Regex  Σ ) → Bool → ℕ  → List ( RST  Σ ) → List ( RST  Σ ) → ( RST  Σ )
  generate (x *) end n next else = loop
     where 
       loop : RST  Σ
       repeat : RST  Σ
       loop = generate x end (n + 1) [ repeat ] else
       repeat = record {
               state = n
             ; move = {!!}
             ; RSTend = end
            } 
  generate (x & y) end n next else = {!!}
  generate (x || y) end n next else = {!!}
  generate < x > end n next else = record {
       state = n
     ; move = λ q → listcase q x end else
     ; RSTend = false
    }  


regex2nfa :  (regex : Regex In2 ) → NAutomaton (RST In2) In2 
regex2nfa regex = record {
      nδ = λ s i → move s i
    ; sid = λ s → state s
    ; nstart =  start ( generateRNFA ieq regex )
    ; nend = λ s → RSTend s }