{-# 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 Data.Empty 
open import finiteSet
open import fin

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 (is-derived 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 Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 

D-cong :  (r s : Regex Σ) → (x : Derivative r) (y : Derivative s) 
   → state x ≡ state y → is-derived x ≅ is-derived y  → x ≅ y
D-cong = ?

D-inject :  (r : Regex Σ) → {x y : Derivative r} → x ≡ y
D-inject r {x} {y} = HE.≅-to-≡  (D-cong r r x y ? ? )

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

-- 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ε : SB ε 0
    sbφ : 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 xn  → SB (x *) (suc xn)
    sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn  → ( sx : SB x xn ) (sy : SB y yn ) → SB (x & y) (suc yn)

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 n ε eq = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
        fb01 :  (q : SB ε 0) → sbε ≡ q
        fb01 sbε = refl
    fb00 zero φ eq = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
        fb01 :  (q : SB φ 0) → sbφ ≡ q
        fb01 sbφ = refl
    fb00 zero (r || r₁) eq = iso-fin (fin-∨ (fb00 zero r ?) (fb00 zero r₁ ?)) ?
    fb00 zero < x > eq = record { finite = 1 ; Q←F = λ _ → sb<> x ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
        fb01 : (q : SB < x > 0) → sb<> x ≡ q
        fb01 (sb<> x) = refl
    fb00 (suc n) (r *) eq = iso-fin (fb00 n r ?) ?
    fb00 (suc n) (r & r₁) eq = iso-fin (fin-∧ (fb00 n r ?) (fb00 n r₁ ?)) ?
    fb00 (suc n) (r || r₁) eq = iso-fin (fin-∨ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) ?
    fb00 zero (x *) ()
    fb00 zero (x & x₁) ()
    fb00 (suc n) φ z≤n =  fb00 n φ z≤n 
    fb00 (suc n) < x > z≤n = fb00 n < x > z≤n 

record SBf (r : Regex Σ) (n : ℕ) : Set where
    field
       rank=n    : rank r ≡ n
       f         : Derivative r → SB r n → Bool
       sb-inject : {x y : Derivative r} → f x ≡ f y → x ≡ y
       dec       : (a : SB r n → Bool ) →  Dec (Is (Derivative r) (SB r n → Bool) f a )

SBN : (r : Regex   Σ) → SBf r (rank r)
SBN ε = record { rank=n = refl ; f = fb02 ; sb-inject = fl05 ; dec = fl03 } where
    fb02 : Derivative ε → SB ε 0 → Bool
    fb02 d sbε = true
    fl03 : (a : SB ε 0 → Bool) → Dec (Is (Derivative ε) (SB ε 0 → Bool) fb02 a)
    fl03 a with a sbε | inspect a sbε
    ... | true | record { eq = eq1 } = yes record { a = record { state = ε ; is-derived = unit } 
         ; fa=c = f-extensionality fl04 } where
         fl04 : (x : SB ε 0) →  fb02 (record { state = ε ; is-derived = unit }) x ≡ a x
         fl04 sbε = sym eq1
    ... | false | record { eq = eq1} = no (λ n → ¬-bool {a sbε} eq1 (fl04 n)) where
         fl04 : Is (Derivative ε) (SB ε 0 → Bool) fb02 a → a sbε ≡ true
         fl04 n = sym (cong (λ k → k sbε) (Is.fa=c n))
    fl06 :  (y : Regex Σ) → (s : Σ) → ¬ ( regex-states y ε )
    fl06 y s x with derivative y s | inspect (derivative y) s
    ... | d | record { eq = eq1 } = ?
    fl05 :  {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y
    fl05 {x} {y} eq with is-derived x | inspect is-derived x 
    ... | unit | record { eq = eq1 } = ?
    ... | derive e s | record { eq = eq1 } = ?
SBN φ = ?
SBN (r *) = ?
SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? }
SBN (r || r₁) = ?
SBN < x > = record { rank=n = refl ; f = ? ; sb-inject = ? ; dec = ? } 

finite-derivative : (r : Regex   Σ) → FiniteSet (Derivative r) 
finite-derivative r = inject-fin (finSBTA r) record { f = SBf.f (SBN r) ; inject = SBf.sb-inject (SBN r) }  (SBf.dec (SBN r))