module epautomaton where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
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)

open import automaton
open import nfa-list

nth : {S : Set } →  ℕ → List S → Maybe S
nth _ [] = nothing
nth 0 ( x  ∷ _ ) = just x
nth (suc n) ( _  ∷ t ) = nth n t

member :  ℕ → List ℕ → Bool
member _ [] = false
member n ( x  ∷ t ) with n ≟ x
... | yes _ = true
... | no _ =  member n t


data STree (S E : Set ) : Set where
   empty :  STree S E
   leaf :  S → E → STree S E
   node :  S → E → STree S E  → STree S E → STree S E

Tree : Set → Set
Tree E = STree ℕ E

insertT :  {E : Set} → ℕ → E → Tree E → Tree E
insertT {E} n e empty = leaf n e
insertT {E} n e (leaf n1 e1 ) with  n ≟ n1  |  n ≤? n1
... | yes _ |  _ = leaf n e
... | no _ | yes _  = node n e ( leaf n1 e1 ) empty
... | no _ | no _  = node n e empty (  leaf n1 e1 )
insertT {E} n e (node n1 e1 left right ) with n ≟ n1 | n ≤? n1
... | yes _ |  _ = node n e left right
... | no _ | yes _  = node n1 e1 ( insertT n e left ) right
... | no _ | no _   = node n1 e1 left ( insertT n e right )

memberT :  {E : Set } → ℕ → Tree E → Maybe E
memberT _ empty = nothing
memberT n (leaf n1 e) with n ≟ n1
... | yes _ = just e
... | no _ = nothing
memberT n (node n1 e1 left right) with n ≟ n1 | n ≤? n1
... | yes _ | _ = just e1
memberT n (node n1 e1 left right) | no ¬p | (yes p) = memberT n left
memberT n (node n1 e1 left right) | no ¬p | (no ¬p₁) = memberT n right

open import Data.Product

record εAutomaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
          εδ : Q → Maybe Σ → Tree Q
          all-εδ : Q → Tree ( Maybe Σ × Tree Q )
          εid : Q  →  ℕ
          Σid : Σ  →  ℕ
          allState : Tree Q
          εstart : Q
          εend  : Q → Bool

open εAutomaton

--
--  find ε connected state by following ε transition
--    keep track state list in C
--    if already tracked, skip it
εclosure : { Q : Set } { Σ : Set  }
    → ( allState :  Tree Q )
    → ( εδ : Q → Maybe Σ → Tree Q )
    → Tree ( Tree  Q )
εclosure {Q} { Σ} allState εδ  = closure (  allState   )
    where
         closure2 :  Tree Q →  Tree Q →  Tree Q
         closure2 empty C = C
         closure2 ( leaf n1 q ) C with memberT n1 C
         ... | just _  =  C
         ... | nothing =  insertT n1 q C
         closure2 ( node n1 q left right ) C with memberT n1 C
         ... | just _  =  closure2 left ( closure2 right C )
         ... | nothing =  insertT n1 q (closure2 left ( closure2 right C ))
         closure1 : ℕ →  Tree  Q
         closure1 n with memberT n (allState  )
         ... | nothing = empty
         ... | just q = closure2 (εδ  q nothing) ( leaf n q )
         closure :  Tree Q  → Tree ( Tree  Q )
         closure empty = empty
         closure (leaf n e) = (leaf n (closure1 n)  )
         closure (node n e left right) =
              node n (closure1 n) ( closure left ) ( closure right )


εAutomaton2U : { Q : Set } { Σ : Set  }
    → εAutomaton Q  Σ → NAutomaton Q  Σ
εAutomaton2U {Q} { Σ} M = record {
     nδ = nδ' ;
     sid = εid M ;
     nstart = εstart M  ;
     nend =  εend M
  } where
     MTree :  Tree ( Tree  Q )
     MTree = εclosure (allState M ) (  εδ M )
     flatten :  Tree  Q → List Q
     flatten empty = []
     flatten (leaf x q) = [ q ]
     flatten (node x q left right) = flatten left ++ [ q ] ++ flatten right
     nδ1 : Tree Q → Σ → List Q
     nδ1 empty i = []
     nδ1 (leaf n q) i =  flatten (εδ M q (just i))
     nδ1 (node n q left right) i = nδ1 left i ++ ( flatten (εδ M q (just i) )) ++ nδ1 right i
     nδ' : Q → Σ → List Q
     nδ' q i with memberT ( εid M q ) MTree
     ... | nothing = []
     ... | just x = nδ1 x i