{-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.List hiding ( [_] )
open import finiteSet

module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where

open import automaton
open import logic
open import regex

-- whether a regex accepts empty input
--
empty? : Regex  Σ → Bool
empty?  ε       = true
empty?  φ       = false
empty? (x *)    = true
empty? (x & y)  = empty? x /\ empty? y
empty? (x || y) = empty? x \/ empty? y
empty? < x >    = false

derivative :  Regex  Σ → Σ → Regex  Σ
derivative ε s = φ
derivative φ s = φ
derivative (x *) s with derivative x s
... | ε = x *
... | φ = φ
... | t = t & (x *)
derivative (x & y) s with empty? x
... | true with derivative x s | derivative y s
... | ε | φ = φ
... | ε | t = t || y
... | φ | t = t
... | x1 | φ = x1 & y
... | x1 | y1 = (x1 & y) || y1
derivative (x & y) s | false with derivative x s 
... | ε = y
... | φ = φ
... | t = t & y
derivative (x || y) s with derivative x s | derivative y s
... | φ | y1 = y1
... | x1 | φ = x1
... | x1 | y1 = x1 || y1
derivative < x > s with eq? x s
... | yes _ = ε
... | no  _ = φ

data regex-states (x : Regex  Σ ) : Regex  Σ → Set where
    unit   : regex-states x x
    derive : { y : Regex  Σ } → regex-states x y → (s : Σ)  → regex-states x ( derivative y s )

record Derivative (x : Regex  Σ ) : Set where
    field
       state : Regex  Σ
       is-derived : regex-states x state

open Derivative

derive-step : (r : Regex   Σ) (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
derive-step r d0 s = derive (is-derived d0) s

regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step r d s} 
   ; aend = λ d → empty? (state d) }  

regex-match : (r : Regex   Σ) →  (List Σ) → Bool
regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 

-- open import nfa
open import Data.Nat
-- open import Data.Nat hiding ( _<_ ; _>_ )
-- open import Data.Fin hiding ( _<_ )
open import nat
open import finiteSetUtil
open FiniteSet
open import Data.Fin hiding (_<_)

-- finiteness of derivative 
--    term generate   x & y   for each * and & only once
--      rank : Regex → ℕ 
--   r₀ & r₁ ... r
--   generated state is a subset of the term set

open import Relation.Binary.Definitions

rank : (r : Regex Σ) → ℕ
rank ε = 0
rank φ = 0
rank (r *) = suc (rank r)
rank (r & r₁) = suc (max (rank r) (rank r₁))
rank (r || r₁) = max (rank r) (rank r₁)
rank < x > = 0

data SB : (r : Regex Σ) → (rn : ℕ) → Set where
    sbε : (r : Regex Σ) → SB ε 0
    sbφ : (r : Regex Σ) → SB φ 0
    sb<> : (s : Σ) → SB < s > 0
    sb| : (x y : Regex Σ) → (xn yn xy : ℕ) → SB x xn → SB y yn → xy ≡  max xn yn  → SB (x || y)  xy
    sb* : (x : Regex Σ) → (xn : ℕ) → SB (x & (x *)) (suc xn)
    sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn  → SB (x & y) (suc yn)

SBTA : (r : Regex Σ) → Automaton (SB r (rank r) → Bool) Σ
SBTA = ?

open import bijection using ( InjectiveF ; Is )  

finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool)
finSBTA r = fin→ ( fb00 (rank r) r refl ) where
    fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≡ n → FiniteSet (SB r (rank r))
    fb00 zero ε eq = ?
    fb00 zero φ eq = ?
    fb00 zero (r || r₁) eq = ?
    fb00 zero < x > eq = ?
    fb00 (suc n) (r *) eq = ?
    fb00 (suc n) (r & r₁) eq = ?
    fb00 (suc n) (r || r₁) eq = ?

injSB : (r : Regex   Σ) → InjectiveF (Derivative r) (SB r (rank r) → Bool)
injSB r = record { f = fb01 (rank r) r refl ; inject = ? } where
     fb01 : (n : ℕ ) →  (r : Regex Σ) →  rank r ≡ n →  Derivative r → SB r (rank r) → Bool
     fb01 n r eq d sb with is-derived d 
     fb01 n r eq d sb | unit = true
     fb01 zero .ε eq d (sbε r) | derive {y} ss i = true
     fb01 zero .φ eq d (sbφ r) | derive {y} ss i = false
     fb01 zero .(< s >) eq d (sb<> s) | derive {y} ss i = ?
     fb01 zero .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
     fb01 (suc n) .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
     fb01 (suc n) .(x & (x *)) eq d (sb* x .(max (rank x) (rank (x *)))) | derive {y₂} ss i = ?
     fb01 (suc n) .(x & y) eq d (sb& x y xn .(max (rank x) (rank y)) x₁) | derive {y₂} ss i = ?

finite-derivative : (r : Regex   Σ) → FiniteSet (Derivative r) 
finite-derivative r = inject-fin (finSBTA r) (injSB r) ?