{-# OPTIONS --safe #-}

module Problem19 where

open import Data.List hiding ([_])
open import Data.Product
open import Data.Empty
open import Data.List.Properties
open import Data.Sum
open import Data.Unit hiding (_≟_)
open import Data.Char
open import Data.Maybe
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality hiding ([_])

data Regex : Set where
    ∅ : Regex
    ε : Regex
    [_] : Char → Regex
    _∘_ : Regex → Regex → Regex
    _∪_ : Regex → Regex → Regex
    _⋆  : Regex → Regex

variable c : Char
variable R S : Regex
variable s t : List Char

data Matches : Regex → List Char → Set where
   empty : Matches ε []
   char  : Matches [ c ] (c ∷ [])
   comp  : Matches R s → Matches S t → Matches (R ∘ S) (s ++ t)
   un₁   : Matches R s → Matches (R ∪ S) s
   un₂   : Matches S s → Matches (R ∪ S) s
   starₑ : Matches (R ⋆) []
   starₛ : Matches R s → Matches (R ⋆) t → Matches (R ⋆) (s ++ t)

comp⁻¹ : Matches (R ∘ S) s → ∃₂ λ t₁ t₂ → t₁ ++ t₂ ≡ s × Matches R t₁ × Matches S t₂
comp⁻¹ (comp prf prf₁) = _ , _ , refl , prf , prf₁

star⁻¹′ : Matches (R ⋆) s → s ≡ [] ⊎ ∃[ c ] ∃[ t₁ ] ∃[ t₂ ] c ∷ t₁ ++ t₂ ≡ s × Matches R (c ∷ t₁) × Matches (R ⋆) t₂
star⁻¹′ starₑ = inj₁ refl
star⁻¹′ (starₛ {s = []} prf prf₁) = star⁻¹′ prf₁
star⁻¹′ (starₛ {s = x ∷ s} prf prf₁) = inj₂ (x , s , _ , refl , prf , prf₁)

Nullable : Regex → Set
Nullable ∅ = ⊥
Nullable ε = ⊤
Nullable [ x ] = ⊥
Nullable (r ∘ r₁) = Nullable r × Nullable r₁
Nullable (r ∪ r₁) = Nullable r ⊎ Nullable r₁
Nullable (r ⋆) = ⊤

nullable? : (r : Regex) → Dec (Nullable r)
nullable? ∅ = no (λ x → x)
nullable? ε = yes tt
nullable? [ x ] = no (λ x → x)
nullable? (r ∘ r₁) with nullable? r | nullable? r₁
... | no p  | _     = no λ (a , b) → p a
... | _     | no p  = no λ (a , b) → p b
... | yes p | yes q = yes (p , q)
nullable? (r ∪ r₁)  with nullable? r | nullable? r₁
... | yes p | _     = yes (inj₁ p)
... | _     | yes p = yes (inj₂ p)
... | no p  | no q  = no λ { (inj₁ a) → p a ; (inj₂ b) → q b }
nullable? (r ⋆) = yes tt

nullable-correct₁ : ∀ R → Nullable R → Matches R []
nullable-correct₁ ε        _               = empty
nullable-correct₁ (r ∘ r₁) (null₁ , null₂) = comp (nullable-correct₁ r null₁) (nullable-correct₁ r₁ null₂)
nullable-correct₁ (r ∪ r₁) (inj₁ null)     = un₁ (nullable-correct₁ r null)
nullable-correct₁ (r ∪ r₁) (inj₂ null)     = un₂ (nullable-correct₁ r₁ null)
nullable-correct₁ (r ⋆)    _               = starₑ

st≡[]⇒s≡[] : s ++ t ≡ [] → s ≡ []
st≡[]⇒s≡[] {[]} {t} prf = refl

st≡[]⇒t≡[] : s ++ t ≡ [] → t ≡ []
st≡[]⇒t≡[] {[]} {t} prf = prf

nullable-correct₂′ : ∀ {R} → Matches R s → s ≡ [] → Nullable R
nullable-correct₂′ empty            s≡[]  = _
nullable-correct₂′ (comp s∈r t∈r₁)  st≡[] = nullable-correct₂′ s∈r (st≡[]⇒s≡[] st≡[]) , nullable-correct₂′ t∈r₁ (st≡[]⇒t≡[] st≡[])
nullable-correct₂′ (un₁ s∈r)        s≡[]  = inj₁ (nullable-correct₂′ s∈r s≡[])
nullable-correct₂′ (un₂ s∈r)        s≡[]  = inj₂ (nullable-correct₂′ s∈r s≡[])
nullable-correct₂′ starₑ            s≡[]  = _
nullable-correct₂′ (starₛ s∈r s∈r₁) s≡[]  = _

nullable-correct₂ : ∀ R → Matches R [] → Nullable R
nullable-correct₂ r []∈r = nullable-correct₂′ []∈r refl

step : Regex → Char → Regex
step ∅ c = ∅
step ε c = ∅
step [ x ] c with c ≟ x
... |  yes p = ε
... |  no  p = ∅
step (r ∘ r₁) c with nullable? r
... | yes p = (step r c ∘ r₁) ∪ step r₁ c
... | no  p = step r c ∘ r₁
step (r ∪ r₁) c = step r c ∪ step r₁ c
step (r ⋆) c = step r c ∘ (r ⋆)

steps : Regex → List Char → Regex
steps R (x ∷ xs) = steps (step R x) xs
steps R [] = R

step-correct₁ : ∀ R c s → Matches (step R c) s → Matches R (c ∷ s)
step-correct₁ [ x ]    c s   prf   with c ≟ x
step-correct₁ [ x ]    c s empty | yes refl = char
step-correct₁ [ x ]    c s ()    | no p

step-correct₁ (R ∘ R₁) c s prf                   with nullable? R
step-correct₁ (R ∘ R₁) c s (un₁ (comp prf prf₁)) | yes p = comp (step-correct₁ R c _ prf) prf₁
step-correct₁ (R ∘ R₁) c s (un₂ prf)             | yes p = comp (nullable-correct₁ R p) (step-correct₁ R₁ c _ prf)
step-correct₁ (R ∘ R₁) c s (comp prf prf₁)       | no p  = comp (step-correct₁ R c _ prf) prf₁

step-correct₁ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₁ R c s prf)
step-correct₁ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₁ R₁ c s prf)

step-correct₁ (R ⋆)    c s (comp prf prf₁) = starₛ (step-correct₁ R c _ prf) prf₁

step-correct₂ : ∀ R c s → Matches R (c ∷ s) → Matches (step R c) s
step-correct₂ [ x ]    c s char with x ≟ x
... | yes p = empty
... | no  p = ⊥-elim (p refl)
step-correct₂ (R ∘ R₁) c s prf with nullable? R | comp⁻¹ prf
... | yes p | []     , t₂ , refl , prf , prf₁ = un₂ (step-correct₂ R₁ c s prf₁)
... | yes p | x ∷ t₁ , t₂ , eq   , prf , prf₁ =
  un₁ (subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
    (comp (step-correct₂ R x t₁ prf) prf₁))
... | no p  | []     , t₂ , eq   , prf , prf₁ = ⊥-elim (p (nullable-correct₂ R prf))
... | no p  | x ∷ t₁ , t₂ , eq   , prf , prf₁ =
  subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
    (comp (step-correct₂ R x t₁ prf) prf₁)
step-correct₂ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₂ R c s prf)
step-correct₂ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₂ R₁ c s prf)
step-correct₂ (R ⋆)    c s prf with star⁻¹′ prf
... | inj₂ (x , t₁ , t₂ , eq , prf , prf₁) =
  subst₂ Matches (cong (λ - → step R - ∘ (R ⋆)) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
    (comp (step-correct₂ R x t₁ prf) prf₁)

steps-correct₁ : ∀ R s → Matches (steps R s) [] → Matches R s
steps-correct₁ R []      prf = prf
steps-correct₁ R (x ∷ s) prf = step-correct₁ R x s (steps-correct₁ (step R x) s prf)

steps-correct₂ : ∀ R s → Matches R s → Matches (steps R s) []
steps-correct₂ R []      prf = prf
steps-correct₂ R (x ∷ s) prf = steps-correct₂ (step R x) s (step-correct₂ R x s prf)

check-lemma₁ : ∀ R s → Nullable (steps R s) → Matches R s
check-lemma₁ R s null = steps-correct₁ R s (nullable-correct₁ (steps R s) null)

check-lemma₂ : ∀ R s → Matches R s → Nullable (steps R s)
check-lemma₂ R s prf = nullable-correct₂ (steps R s) (steps-correct₂ R s prf)

check : (R : Regex) (s : List Char) → Dec (Matches R s)
check R s with nullable? (steps R s)
... | yes p = yes (check-lemma₁ R s p)
... | no p = no λ m → p (check-lemma₂ R s m)