module sbconst 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.Product
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 epautomaton


-- all primitive state has id
-- Tree Q is sorted by id and is contents are unique

flatten : { Q : Set} → Tree Q  → List ℕ
flatten empty = []
flatten (leaf x x₁) = [ x ]
flatten (node x x₁ x₂ x₃) = flatten x₂ ++ [ x ] ++ flatten  x₃

listEq :  List ℕ  → List ℕ  → Bool
listEq [] [] = true
listEq [] ( _ ∷  _ )  = false
listEq ( _ ∷  _ ) [] = false
listEq ( h1 ∷ t1 ) ( h2 ∷ t2 ) with h1 ≟ h2
... | yes _ =  listEq t1 t2
... | no _ = false

infixr 7 _==_
_==_ : { Q : Set} → Tree Q  → Tree Q → Bool
x == y = listEq ( flatten x ) ( flatten y )

memberTT : { Q : Set} →  Tree Q  → Tree ( Tree  Q ) → Bool
memberTT t empty  = false
memberTT t (leaf x x₁) = t == x₁
memberTT t (node x x₁ x₂ x₃) with t == x₁
... | true = true
... | false = memberTT t x₂ ∨ memberTT t  x₃

lengthT : { Q : Set} →  Tree  Q  →  ℕ
lengthT t = length ( flatten t )

findT : { Q : Set} →  Tree Q  → Tree ( Tree  Q ) → Maybe ( Tree Q )
findT t empty  = nothing
findT t (leaf x x₁) =  just x₁
findT t (node x x₁ x₂ x₃) with t == x₁
... | true =  just x₁
... | false with findT t x₂
...    | (just y) = just y
...    | nothing  = findT t x₃

mergeT : { Q : Set} →  Tree Q  →  Tree  Q  →  Tree Q
mergeT empty t = t
mergeT (leaf x t0) t = insertT x t0 t
mergeT (node x t0  left right ) t =
      mergeT left ( insertT x t0 (mergeT right t ))

open εAutomaton

-- all inputs are exclusive each other ( only one input can happen )

-- merge Tree ( Maybe Σ × Tree Q )
merge-itεδ : { Σ Q : Set } →  εAutomaton Q Σ → Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q )
merge-itεδ NFA i t empty = leaf (Σid NFA i) ( just i , t )
merge-itεδ NFA i t (leaf x (i' , t1 )) with (Σid NFA i) ≟ x
... | no _ =  leaf x (i' , t1)
... | yes _ = leaf x (just i , mergeT t t1  )
merge-itεδ NFA i t (node x (i' , t1) left right ) with (Σid NFA i) ≟ x
... | no _ = node x (i' , t1) ( merge-itεδ NFA i t left ) ( merge-itεδ NFA i t right )
... | yes _ = node x (just i , mergeT t t1  )
    ( merge-itεδ NFA i t left ) ( merge-itεδ NFA i t right )

merge-iεδ : { Σ Q : Set } →  εAutomaton Q Σ → Maybe Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q )
merge-iεδ NFA nothing _ t = t
merge-iεδ NFA (just i) q t = merge-itεδ NFA i q t

merge-εδ : { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q )
merge-εδ NFA empty t = t
merge-εδ NFA (leaf x (i , t1) ) t = merge-iεδ NFA i t1 t
merge-εδ NFA (node x (i , t1) left right) t =
       merge-εδ NFA left ( merge-iεδ NFA i t1 ( merge-εδ NFA right t ) )

-- merge and find new state from newly created Tree ( Maybe Σ × Tree Q )
sbconst13 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) →  Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  Tree ( Tree Q )  × Tree ( Tree Q )  × ℕ )
sbconst13 NFA empty nt t n = (nt , t , n)
sbconst13 NFA (leaf x (p , q)) nt t n with memberTT q t
... | true = ( nt , t , n)
... | false = ( insertT n q nt , insertT n q t , n + 1 )
sbconst13 NFA (node x (_ , q) left right) nt t n with memberTT q t
sbconst13 NFA (node x (_ , q) left right) nt t n | true = ( nt , t , n )
sbconst13 NFA (node x (_ , q) left right) nt t n | false = p2
  where
    p1 = sbconst13 NFA left nt t n
    n1 =  proj₂ ( proj₂ p1 )
    p2 = sbconst13 NFA right (insertT n1 q ( proj₁ p1 )) (insertT n1 q ( proj₁ (proj₂ p1))) (n1 + 1 )
-- expand state to Tree ( Maybe Σ × Tree Q )
sbconst12 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree  Q  → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q )
sbconst12 NFA empty  s  = s
sbconst12 NFA (leaf x q) s  = merge-εδ NFA s (all-εδ NFA q)
sbconst12 NFA (node x q left right) s = sbconst12 NFA right (merge-εδ NFA (all-εδ NFA q) (sbconst12 NFA left s))
-- loop on state tree
sbconst11 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q )  → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  Tree ( Tree Q )  × Tree ( Tree  Q ) ×  ℕ )
sbconst11 NFA empty nt t n = (nt , t , n )
sbconst11 NFA (leaf x q) nt t n = sbconst13 NFA (sbconst12 NFA q empty ) nt t n
sbconst11 NFA (node x q left right ) nt t n = p3
  where
    p1 = sbconst11 NFA left nt t n
    p2 = sbconst13 NFA (sbconst12 NFA q empty ) (  proj₁ p1 ) ( proj₁  ( proj₂ p1 ) ) ( proj₂  ( proj₂ p1 ) )
    p3 = sbconst11 NFA right ( proj₁ p2 ) ( proj₁  ( proj₂ p2 )) ( proj₂  ( proj₂ p2 ))

{-# TERMINATING #-}
sbconst0 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  →  ( Tree ( Tree  Q )  ×  ℕ )
sbconst0 NFA t t1 n0 with sbconst11 NFA t t1 empty n0
... | t2 , empty , n =  (t2 , n )
... | t2 , leaf x y , n = sbconst0 NFA ( proj₁  ( proj₂ p1 ))  (leaf x y) ( proj₂  ( proj₂ p1 ) )
       where
         p1 = sbconst11 NFA (leaf x y) t1 empty n
... | t2 , node x y left right , n = p4
       where
         p1 = sbconst0 NFA left t2 n
         p2 = sbconst11 NFA (leaf x y) (  proj₁  p1 ) empty (  proj₂ p1 )
         p3 = sbconst0 NFA right ( proj₁  p2 ) ( proj₂  ( proj₂ p2 ))
         p4 = sbconst0 NFA ( proj₁ ( proj₂ p2 )) ( proj₁  p3) ( proj₂  p3 )

nfa2dfa : { Σ Q : Set } →  εAutomaton Q Σ →  Automaton (Tree Q) Σ
nfa2dfa {Σ} {Q} NFA = record {
        δ  = δ'
     ;  astart =  astart'
     ;  aend = aend'
  }
    where
      MTree :  { Σ Q : Set } →  (x : εAutomaton Q Σ) →  Tree ( Tree  Q )
      MTree {Σ} {Q} NFA = εclosure (allState NFA ) (  εδ NFA )
      sbconst :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Tree  Q )
      sbconst NFA =  proj₁ (sbconst0 NFA ( MTree NFA ) (MTree NFA) zero)
      δ0 : Σ → Tree ( Maybe Σ × Tree Q ) → Tree Q
      δ0 x empty = empty
      δ0 x (leaf x₁ q) with  Σid NFA x ≟  x₁
      ... | no ¬p = empty
      ... | yes p with  proj₁ q
      ...     | nothing = empty
      ...     | just _ = proj₂ q
      δ0 x (node x₁ q left right) with  Σid NFA x ≟  x₁
      ... | no ¬p with δ0 x left
      ...    | empty = δ0 x right
      ...    | q1 = q1
      δ0 x (node x₁ q left right) | yes p with  proj₁ q
      ...     | nothing = empty
      ...     | just _ = proj₂ q
      δ' : Tree Q → Σ → Tree Q
      δ' t x with findT t ( MTree NFA )
      ... | nothing = leaf zero ( εstart NFA )   -- can't happen
      ... | just q  = δ0 x  (sbconst12 NFA q empty)
      astart' : Tree Q
      astart' =  leaf zero ( εstart NFA )
      aend' : Tree Q → Bool
      aend' empty = false
      aend' (leaf _ x)  = εend NFA x
      aend' (node _ x left right ) =
          aend' left ∨ εend NFA x ∨ aend' right