{-# 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   : { z : Regex Σ} → z ≡ x → regex-states x z
    derive : { y z : Regex  Σ } → regex-states x y → (s : Σ) → z ≡  derivative y s → regex-states x z 

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 refl

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 refl } 
   ; 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 refl } is 

-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 

-- open import nfa
open import Data.Nat
open import Data.Nat.Properties hiding ( eq? )
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

open _∧_ 

fb20 : {r s r₁ s₁ : Regex Σ} → r & r₁ ≡ s & s₁ → (r ≡ s ) ∧  (r₁ ≡ s₁ )
fb20  refl = ⟪ refl , refl ⟫

fb21 : {r s r₁ s₁ : Regex Σ} → r || r₁ ≡ s || s₁ → (r ≡ s ) ∧  (r₁ ≡ s₁ )
fb21  refl = ⟪ refl , refl ⟫

rg-eq? : (r s : Regex Σ) → Dec ( r ≡ s )
rg-eq? ε ε = yes refl
rg-eq? ε φ = no (λ ())
rg-eq? ε (s *) = no (λ ())
rg-eq? ε (s & s₁) = no (λ ())
rg-eq? ε (s || s₁) = no (λ ())
rg-eq? ε < x > = no (λ ())
rg-eq? φ ε = no (λ ())
rg-eq? φ φ = yes refl
rg-eq? φ (s *) = no (λ ())
rg-eq? φ (s & s₁) = no (λ ())
rg-eq? φ (s || s₁) = no (λ ())
rg-eq? φ < x > = no (λ ())
rg-eq? (r *) ε = no (λ ())
rg-eq? (r *) φ = no (λ ())
rg-eq? (r *) (s *) with rg-eq? r s
... | yes eq = yes ( cong (_*) eq)
... | no ne = no (λ eq → ne (fb10 eq) ) where
     fb10 : {r s : Regex Σ} → (r *) ≡ (s *) → r ≡ s 
     fb10  refl = refl
rg-eq? (r *) (s & s₁) = no (λ ())
rg-eq? (r *) (s || s₁) = no (λ ())
rg-eq? (r *) < x > = no (λ ())
rg-eq? (r & r₁) ε = no (λ ())
rg-eq? (r & r₁) φ = no (λ ())
rg-eq? (r & r₁) (s *) = no (λ ())
rg-eq? (r & r₁) (s & s₁) with rg-eq? r s | rg-eq? r₁ s₁
... | yes y | yes y₁ = yes ( cong₂ _&_ y y₁)
... | yes y | no n  = no (λ eq → n (proj2 (fb20 eq) ))
... | no n  | yes y = no (λ eq → n (proj1 (fb20 eq) ))
... | no n  | no n₁ = no (λ eq → n (proj1 (fb20 eq) ))
rg-eq? (r & r₁) (s || s₁) = no (λ ())
rg-eq? (r & r₁) < x > = no (λ ())
rg-eq? (r || r₁) ε = no (λ ())
rg-eq? (r || r₁) φ = no (λ ())
rg-eq? (r || r₁) (s *) = no (λ ())
rg-eq? (r || r₁) (s & s₁) = no (λ ())
rg-eq? (r || r₁) (s || s₁) with rg-eq? r s | rg-eq? r₁ s₁
... | yes y | yes y₁ = yes ( cong₂ _||_ y y₁)
... | yes y | no n  = no (λ eq → n (proj2 (fb21 eq) ))
... | no n  | yes y = no (λ eq → n (proj1 (fb21 eq) ))
... | no n  | no n₁ = no (λ eq → n (proj1 (fb21 eq) ))
rg-eq? (r || r₁) < x > = no (λ ())
rg-eq? < x > ε = no (λ ())
rg-eq? < x > φ = no (λ ())
rg-eq? < x > (s *) = no (λ ())
rg-eq? < x > (s & s₁) = no (λ ())
rg-eq? < x > (s || s₁) = no (λ ())
rg-eq? < x > < x₁ > with eq? x x₁
... | yes y = yes (cong <_> y)
... | no n = no (λ eq → n (fb11 eq))   where
     fb11 : < x > ≡ < x₁ > → x ≡ x₁
     fb11 refl = refl

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 s : Regex Σ) → Set where
    sunit  : {r : Regex Σ} → SB r r
    sub|1  : {x y z : Regex Σ} → SB x z → SB (x || y) z
    sub|2  : {x y z : Regex Σ} → SB y z → SB (x || y) z
    sub*   : {x y : Regex Σ} → SB x y  → SB (x *) y
    sub&1  : (x y z : Regex Σ) → SB x z → SB (x & y) z
    sub&2  : (x y z : Regex Σ) → SB y z → SB (x & y) z
    sub*&  : (x y : Regex Σ) → rank x < rank y  → SB y x → SB (y *) (x & (y *)) 
    sub&&  : (x y z : Regex Σ) → rank z < rank (x & z)  → SB (x & y) z → SB (x & y) (z & y) 

record ISB (r : Regex Σ) : Set where
    field
        s : Regex Σ
        is-sub : SB r s

open import bijection using ( InjectiveF ; Is )  

finISB : (r : Regex Σ) → FiniteSet (ISB r)
finISB ε = record { finite = 1 ;  Q←F = λ _ → record { s = ε ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
    fb00 : (q : ISB ε) → record { s = ε ; is-sub = sunit } ≡ q
    fb00 record { s = .ε ; is-sub = sunit } = refl
    fb01 : (q : ISB ε) → record { s = ε ; is-sub = sunit } ≡ q
    fb01 record { s = .ε ; is-sub = sunit } = refl
finISB φ = record { finite = 1 ;  Q←F = λ _ → record { s = φ ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
    fb00 : (q : ISB φ) → record { s = φ ; is-sub = sunit } ≡ q
    fb00 record { s = .φ ; is-sub = sunit } = refl
    fb01 : (q : ISB φ) → record { s = φ ; is-sub = sunit } ≡ q
    fb01 record { s = .φ ; is-sub = sunit } = refl
finISB < s > = record { finite = 1 ;  Q←F = λ _ → record { s = < s > ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
    fb00 : (q : ISB < s >) → record { s = < s > ; is-sub = sunit } ≡ q
    fb00 record { s = < s > ; is-sub = sunit } = refl
    fb01 : (q : ISB < s >) → record { s = < s > ; is-sub = sunit } ≡ q
    fb01 record { s = < s > ; is-sub = sunit } = refl
finISB (x || y) = iso-fin (fin-∨1 (fin-∨ (finISB x) (finISB y))) record { fun← = fb00 ; fun→ = fb01 ; fiso← = {!!} ; fiso→ = {!!} } where
     fb00 : ISB (x || y) → One ∨ ISB x ∨ ISB y
     fb00 record { s = .(x || y) ; is-sub = sunit } = case1 one
     fb00 record { s = s ; is-sub = (sub|1 is-sub) } = case2 (case1 record { s = s ; is-sub = is-sub } )
     fb00 record { s = s ; is-sub = (sub|2 is-sub) } = case2 (case2 record { s = s ; is-sub = is-sub } )
     fb01 : One ∨ ISB x ∨ ISB y → ISB (x || y)
     fb01 (case1 one) = record { s = (x || y) ; is-sub = sunit } 
     fb01 (case2 (case1 record { s = s ; is-sub = is-sub })) = record { s = s ; is-sub = sub|1 is-sub  }
     fb01 (case2 (case2 record { s = s ; is-sub = is-sub })) = record { s = s ; is-sub = sub|2 is-sub  }
     fb02 : (x : One ∨ ISB x ∨ ISB y) → fb00 (fb01 x) ≡ x
     fb02 (case1 one) = refl
     fb02 (case2 (case1 record { s = s ; is-sub = is-sub })) = refl
     fb02 (case2 (case2 record { s = s ; is-sub = is-sub })) = refl

finISB (x & y) = iso-fin (fin-∨ (inject-fin (fin-∧ (finISB x) (finISB y)) fi {!!}) (fin-∨1 (fin-∨ (finISB x) (finISB y)))) {!!} where
     record Z : Set where
        field 
          x1 y1 z : Regex Σ
          lt : rank z < suc (max (rank x1) (rank z))
          is-sub : SB x1 z
     fb00 : ISB (x & y) → {!!}
     fb00 record { s = .(x & y) ; is-sub = sunit } = {!!}
     fb00 record { s = s ; is-sub = (sub&1 .x .y .s is-sub) } = {!!}
     fb00 record { s = s ; is-sub = (sub&2 .x .y .s is-sub) } = {!!}
     fb00 record { s = (z & y) ; is-sub = (sub&& x y z lt is-sub) } = {!!}
     fi : InjectiveF Z (ISB x ∧ ISB y)
     fi = record { f = f ; inject = {!!} } where
        f : Z → ISB x ∧ ISB y
        f z = ⟪ record { s = Z.x1 z ; is-sub = {!!} }  , {!!} ⟫
finISB (x *) = iso-fin (fin-∨ (inject-fin (finISB x) fi {!!} ) (fin-∨1 (finISB x) )) record { fun← = fb00 } where
     record Z : Set where
        field 
          z : Regex Σ
          lt : rank z < rank x
          is-sub : SB x z
     fi : InjectiveF Z (ISB x) 
     fi = record { f = f ; inject = {!!} } where
        f : Z → ISB x
        f z = record { s = Z.z z ; is-sub = Z.is-sub z }
     fb00 : ISB (x *) → {!!}
     fb00 record { s = .(x *) ; is-sub = sunit } = {!!}
     fb00 record { s = s ; is-sub = (sub* is-sub) } = {!!}
     fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }

toSB : (r : Regex   Σ) →  ISB r → Bool
toSB r record { s = s ; is-sub = is-sub } with rg-eq? r s
... | yes _ = true
... | no _ = false

sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
sbempty? ε f with f record { s = ε ; is-sub = sunit  }
... | true = true
... | false = false
sbempty? φ f = false
sbempty? (r *) f with f record { s = r * ; is-sub = sunit  }
... | true = true 
... | false = false 
sbempty? (r & r₁) f with f record { s = r & r₁ ; is-sub = sunit  }
... | false = false
... | true = empty? r /\ empty? r₁
sbempty? (r || r₁) f with f record { s = r || r₁ ; is-sub = sunit  }
... | false = false
... | true = empty? r \/ empty? r₁ 
sbempty? < x > f = false

sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
sbderive ε f s record { s = .ε ; is-sub = sunit } = false
sbderive φ f s record { s = t ; is-sub = is-sub } = false
sbderive (r *) f s record { s = t ; is-sub = is-sub } = ?
sbderive (r & r₁) f s record { s = t ; is-sub = is-sub } = ?
sbderive (r || r₁) f s record { s = .(r || r₁) ; is-sub = sunit } = ?
sbderive (r || r₁) f s record { s = t ; is-sub = (sub|1 is-sub) } = ?
sbderive (r || r₁) f s record { s = t ; is-sub = (sub|2 is-sub) } = ?
sbderive < x > f s record { s = t ; is-sub = is-sub } = ?

-- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
--    this is not correct because it contains s || s || s || .....

finSBTA : (r : Regex Σ) → FiniteSet (ISB r → Bool)
finSBTA r = fin→ ( finISB r )

regex→automaton1 : (r : Regex   Σ) → Automaton (ISB r  → Bool) Σ
regex→automaton1 r = record { δ = sbderive r ; aend = sbempty? r }

regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool
regex-match1 r is = accept ( regex→automaton1 r ) (λ sb → toSB r sb) is

derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match r x
derive-is-regex-language ε [] = refl
derive-is-regex-language ε (x ∷ x₁) = ?
derive-is-regex-language φ [] = refl
derive-is-regex-language φ (x ∷ x₁) = ?
derive-is-regex-language (r *) x = ?
derive-is-regex-language (r & r₁) x = ?
derive-is-regex-language (r || r₁) x = ?
derive-is-regex-language < x₁ > [] = refl
derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x
... | yes _  = refl
... | no _  = refl
derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = ? where -- rg01 (eq? x₁ x) where
    rg01 : Dec ( x₁ ≡ x ) →  regex-language < x₁ > eq? (x ∷ x₂ ∷ x₃ ) ≡ false
    rg01 (yes eq) = refl
    rg01 (no neq) = refl
    rg03 : (x s : Σ) → (derivative < x > s ≡ ε ) ∨ (derivative < x > s ≡ φ )
    rg03 x s with eq? x s
    ... | yes _ = case1 refl
    ... | no _ = case2 refl
    rg02 : regex-match < x₁ > (x ∷ x₂ ∷ x₃ ) ≡ false
    rg02 with rg03 x₁ x
    ... | case1 eq = ?
    ... | case2 eq = ?
--    immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b)

derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-match r x ≡ regex-match1 r x
derive=ISB ε [] = refl
derive=ISB ε (x ∷ x₁) = ?
derive=ISB φ [] = refl
derive=ISB φ (x ∷ x₁) = ?
derive=ISB (r *) x = ?
derive=ISB (r & r₁) x = ?
derive=ISB (r || r₁) x = ?
derive=ISB < x₁ > [] = refl
derive=ISB < x₁ > (x ∷ []) with eq? x₁ x
... | yes _ = ?
... | no _ = refl
derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ?

ISB-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match1 r x
ISB-is-regex-language r x = trans ( derive-is-regex-language r x ) (derive=ISB r x)