```------------------------------------------------------------------------
-- A breadth-first backend
------------------------------------------------------------------------

-- Similar to Brzozowski's "Derivatives of Regular Expressions".

-- TODO: Examine if the use of simplification really is an
-- optimisation.

module StructurallyRecursiveDescentParsing.Backend.BreadthFirst where

open import Category.Monad
open import Coinduction
open import Data.Bool
open import Data.Function hiding (_∶_)
open import Data.List as List
open import Data.List.Any
open Membership-≡
open RawMonad List.monad
using () renaming (_>>=_ to _>>=′_; return to return′)
open import Data.Product1 as Prod1 renaming (∃₀₁ to ∃; Σ₀₁ to Σ)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Relation.Binary.PropositionalEquality1 as Eq1

open import StructurallyRecursiveDescentParsing.Coinduction
open import StructurallyRecursiveDescentParsing.Parser
open import StructurallyRecursiveDescentParsing.Parser.Semantics
hiding (sound; complete)
open import StructurallyRecursiveDescentParsing.Backend.Simplification
as Simplification using (simplify)

------------------------------------------------------------------------
-- Parsing

private

-- Map then choice: y ∈ ⋁ f xs · s  iff  ∃ x ∈ xs. y ∈ f x · s.

⋁-initial : ∀ {R₁ R₂} → (R₁ → List R₂) → List R₁ → List R₂
⋁-initial e []       = _
⋁-initial e (x ∷ xs) = _

⋁ : ∀ {Tok R₁ R₂} {f : R₁ → List R₂} →
((x : R₁) → Parser Tok R₂ (f x)) → (xs : List R₁) →
Parser Tok R₂ (⋁-initial f xs)
⋁ f []       = fail
⋁ f (x ∷ xs) = f x ∣ ⋁ f xs

-- Functions calculating the index of the derivative.

mutual

∂-initial : ∀ {Tok R xs} → Tok → Parser Tok R xs → List R
∂-initial _ (return _)                = _
∂-initial _ fail                      = _
∂-initial _ token                     = _
∂-initial _ (_ ∣ _)                   = _
∂-initial _ (_ <\$> _)                 = _
∂-initial _ (⟨ _ ⟩ ⊛ ⟪ _ ⟫)           = _
∂-initial _ (⟪ _ ⟫ ⊛ ⟪ _ ⟫)           = _
∂-initial _ (⟨ _ ⟩ ⊛ ⟨ _ ⟩)           = _
∂-initial _ (⟪ _ ⟫ ⊛ ⟨ _ ⟩)           = _
∂-initial _ (_>>=_  {xs = []   } _ _) = _
∂-initial _ (_>>=_  {xs = _ ∷ _} _ _) = _
∂-initial _ (_>>=!_ {xs = []   } _ _) = _
∂-initial _ (_>>=!_ {xs = _ ∷ _} _ _) = _
∂-initial _ (nonempty _)              = _
∂-initial _ (cast _ _)                = _

∂-⋁-initial : ∀ {Tok R₁ R₂ y} {ys : List R₁} {f : R₁ → List R₂} →
Tok → List R₁ →
((x : R₁) → ∞? (Parser Tok R₂ (f x)) (y ∷ ys)) →
List R₂
∂-⋁-initial _ []      _ = _
∂-⋁-initial _ (_ ∷ _) _ = _

∂!-initial : ∀ {Tok R₁ R₂ xs y} {ys : List R₁} →
Tok → ∞? (Parser Tok R₂ xs) (y ∷ ys) → List R₂
∂!-initial _ ⟨ _ ⟩ = _

-- "Derivative": x ∈ ∂ t p · s  iff  x ∈ p · t ∷ s.

-- Note that these functions would not work with the simplified
-- parsers. The reason is that the analogue of p₁ !>>= p₂ is
-- sometimes changed to the analogue of p₁′ ?>>= p₂′, where p₂′ is
-- still dependently typed, and _?>>=_ does not accept dependently
-- typed arguments.

mutual

-- Note that simplification is currently not performed
-- (co)recursively under ♯₁_.

∂ : ∀ {Tok R xs}
(t : Tok) (p : Parser Tok R xs) → Parser Tok R (∂-initial t p)
∂ t (return x)                   = fail
∂ t fail                         = fail
∂ t token                        = return t
∂ t (p₁ ∣ p₂)                    = ∂ t p₁ ∣ ∂ t p₂
∂ t (f <\$> p)                    = f <\$> ∂ t p
∂ t (⟨ p₁ ⟩ ⊛ ⟪ p₂ ⟫)            = ⟨    ∂ t     p₁  ⟩ ⊛ ♯? (♭₁ p₂)
∂ t (⟪ p₁ ⟫ ⊛ ⟪ p₂ ⟫)            = ⟪ ♯₁ ∂ t (♭₁ p₁) ⟫ ⊛ ♯? (♭₁ p₂)
∂ t (⟨ p₁ ⟩ ⊛ ⟨_⟩ {f} {fs} p₂)   = ⟨    ∂ t     p₁  ⟩ ⊛ ♯?     p₂
∣ ♯? (⋁ return (f ∷ fs)) ⊛ ⟨ ∂ t p₂ ⟩
∂ t (⟪ p₁ ⟫ ⊛ ⟨_⟩ {f} {fs} p₂)   = ⟪ ♯₁ ∂ t (♭₁ p₁) ⟫ ⊛ ♯?     p₂
∣ ♯? (⋁ return (f ∷ fs)) ⊛ ⟨ ∂ t p₂ ⟩
∂ t (_>>=_ {xs = []}      p₁ p₂) = ∂ t p₁ >>= (λ x → ♯? (♭? (p₂ x)))
∂ t (_>>=_ {xs = x ∷ xs}  p₁ p₂) = ∂ t p₁ >>= (λ x → ♯? (♭? (p₂ x)))
∣ ∂-⋁ t (x ∷ xs) p₂
∂ t (_>>=!_ {xs = []}     p₁ p₂) = (♯₁ ∂ t (♭₁ p₁)) >>=! (λ x → ♯? (♭? (p₂ x)))
∂ t (_>>=!_ {xs = x ∷ xs} p₁ p₂) = (♯₁ ∂ t (♭₁ p₁)) >>=! (λ x → ♯? (♭? (p₂ x)))
∣ ∂-⋁ t (x ∷ xs) p₂
∂ t (nonempty p)                 = ∂ t p
∂ t (cast _ p)                   = ∂ t p

-- ⋁ is inlined here, because otherwise the termination checker
-- would not accept the code.

∂-⋁ : ∀ {Tok R₁ R₂ y} {ys : List R₁} {f : R₁ → List R₂}
(t : Tok) (xs : List R₁)
(p : (x : R₁) → ∞? (Parser Tok R₂ (f x)) (y ∷ ys)) →
Parser Tok R₂ (∂-⋁-initial t xs p)
∂-⋁ t []       p = fail
∂-⋁ t (x ∷ xs) p = ∂! t (p x) ∣ ∂-⋁ t xs p

∂! : ∀ {Tok R₁ R₂ xs y} {ys : List R₁}
(t : Tok) (p : ∞? (Parser Tok R₂ xs) (y ∷ ys)) →
Parser Tok R₂ (∂!-initial t p)
∂! t ⟨ p ⟩ = ∂ t p

-- Parsing: x ∈ parseComplete p s  iff  x ∈ p · s.

parseComplete : ∀ {Tok R xs} → Parser Tok R xs → List Tok → List R
parseComplete {xs = xs} p []      = xs
parseComplete           p (t ∷ s) = parseComplete (simplify (∂ t p)) s

------------------------------------------------------------------------
-- Soundness

private

⋁-sound : ∀ {Tok R₁ R₂ y s} {i : R₁ → List R₂} →
(f : (x : R₁) → Parser Tok R₂ (i x)) (xs : List R₁) →
y ∈ ⋁ f xs · s → ∃ λ x → Σ (x ∈ xs) λ _ → y ∈ f x · s
⋁-sound f []       ()
⋁-sound f (x ∷ xs) (∣ˡ    y∈fx)   = (x , here refl , y∈fx)
⋁-sound f (x ∷ xs) (∣ʳ ._ y∈⋁fxs) =
Prod1.map₀₁ id (Prod1.map₀₁ there (λ y∈ → y∈)) (⋁-sound f xs y∈⋁fxs)

mutual

∂-sound : ∀ {Tok R xs x s} {t} (p : Parser Tok R xs) →
x ∈ ∂ t p · s → x ∈ p · t ∷ s
∂-sound token                      return                    = token
∂-sound (p₁ ∣ p₂)                  (∣ˡ    x∈p₁)              = ∣ˡ     (∂-sound p₁ x∈p₁)
∂-sound (_∣_ {xs₁ = xs₁} p₁ p₂)    (∣ʳ ._ x∈p₂)              = ∣ʳ xs₁ (∂-sound p₂ x∈p₂)
∂-sound (f <\$> p)                  (<\$> x∈p)                 = <\$> ∂-sound p x∈p
∂-sound (⟨ p₁ ⟩ ⊛ ⟪ p₂ ⟫)                 (f∈p₁′   ⊛ x∈p₂)   = ∂-sound p₁ f∈p₁′ ⊛
cast∈ refl (♭?♯? (∂-initial _ p₁)) refl x∈p₂
∂-sound (⟪ p₁ ⟫ ⊛ ⟪ p₂ ⟫)                 (f∈p₁′   ⊛ x∈p₂)   = ∂-sound (♭₁ p₁) f∈p₁′ ⊛
cast∈ refl (♭?♯? (∂-initial _ (♭₁ p₁))) refl x∈p₂
∂-sound (⟨ p₁ ⟩ ⊛ ⟨ p₂ ⟩)          (∣ˡ    (f∈p₁′   ⊛ x∈p₂))  = ∂-sound p₁ f∈p₁′ ⊛
cast∈ refl (♭?♯? (∂-initial _ p₁)) refl x∈p₂
∂-sound (⟨ p₁ ⟩ ⊛ ⟨_⟩ {f} {fs} p₂) (∣ʳ ._ (f∈⋁f∷fs ⊛ x∈p₂′)) with ⋁-sound return (f ∷ fs)
(cast∈ refl (♭?♯? (∂-initial _ p₂)) refl f∈⋁f∷fs)
∂-sound (⟨ p₁ ⟩ ⊛ ⟨ p₂ ⟩)          (∣ʳ ._ (f∈⋁f∷fs ⊛ x∈p₂′)) | (f′ , f′∈f∷fs , return) =
initial-sound p₁ f′∈f∷fs ⊛ ∂-sound p₂ x∈p₂′
∂-sound (⟪ p₁ ⟫ ⊛ ⟨ p₂ ⟩)          (∣ˡ    (f∈p₁′   ⊛ x∈p₂))  = ∂-sound (♭₁ p₁) f∈p₁′ ⊛
cast∈ refl (♭?♯? (∂-initial _ (♭₁ p₁))) refl x∈p₂
∂-sound (⟪ p₁ ⟫ ⊛ ⟨_⟩ {f} {fs} p₂) (∣ʳ ._ (f∈⋁f∷fs ⊛ x∈p₂′)) with ⋁-sound return (f ∷ fs)
(cast∈ refl (♭?♯? (∂-initial _ p₂)) refl f∈⋁f∷fs)
∂-sound (⟪ p₁ ⟫ ⊛ ⟨ p₂ ⟩)          (∣ʳ ._ (f∈⋁f∷fs ⊛ x∈p₂′)) | (f′ , f′∈f∷fs , return) =
initial-sound (♭₁ p₁) f′∈f∷fs ⊛ ∂-sound p₂ x∈p₂′
∂-sound (_>>=_  {xs = x ∷ xs} p₁ p₂) (∣ʳ ._ z∈p₂′x)          with ∂-⋁-sound (x ∷ xs) p₂ z∈p₂′x
∂-sound (_>>=_  {xs = x ∷ xs} p₁ p₂) (∣ʳ ._ z∈p₂′x)          | (y , y∈x∷xs , z∈p₂′y) =
_>>=_ {p₂ = p₂} (initial-sound p₁ y∈x∷xs) z∈p₂′y
∂-sound (_>>=_  {xs = x ∷ xs} p₁ p₂) (∣ˡ (x∈p₁′ >>=  y∈p₂x)) = _>>=_ {p₂ = p₂} (∂-sound p₁ x∈p₁′)
(cast∈ refl (♭?♯? (∂-initial _ p₁)) refl y∈p₂x)
∂-sound (_>>=_  {xs = []}     p₁ p₂)     (x∈p₁′ >>=  y∈p₂x)  = ∂-sound p₁ x∈p₁′ >>=
cast∈ refl (♭?♯? (∂-initial _ p₁)) refl y∈p₂x
∂-sound (_>>=!_ {xs = x ∷ xs} p₁ p₂) (∣ʳ ._ z∈p₂′x)          with ∂-⋁-sound (x ∷ xs) p₂ z∈p₂′x
∂-sound (_>>=!_ {xs = x ∷ xs} p₁ p₂) (∣ʳ ._ z∈p₂′x)          | (y , y∈x∷xs , z∈p₂′y) =
_>>=!_ {p₂ = p₂} (initial-sound (♭₁ p₁) y∈x∷xs) z∈p₂′y
∂-sound (_>>=!_ {xs = x ∷ xs} p₁ p₂) (∣ˡ (x∈p₁′ >>=! y∈p₂x)) = _>>=!_ {p₂ = p₂} (∂-sound (♭₁ p₁) x∈p₁′)
(cast∈ refl (♭?♯? (∂-initial _ (♭₁ p₁))) refl y∈p₂x)
∂-sound (_>>=!_ {xs = []}     p₁ p₂)     (x∈p₁′ >>=! y∈p₂x)  = ∂-sound (♭₁ p₁) x∈p₁′ >>=!
cast∈ refl (♭?♯? (∂-initial _ (♭₁ p₁))) refl y∈p₂x
∂-sound (nonempty p)                x∈p                      = nonempty (∂-sound p x∈p)
∂-sound (cast _ p)                  x∈p                      = cast (∂-sound p x∈p)

∂-sound (return _) ()
∂-sound fail       ()

∂-⋁-sound : ∀ {Tok R₁ R₂ t z s y} {ys : List R₁} {f : R₁ → List R₂}
xs (p : (x : R₁) → ∞? (Parser Tok R₂ (f x)) (y ∷ ys)) →
z ∈ ∂-⋁ t xs p · s →
∃ λ x → Σ (x ∈ xs) λ _ → z ∈ ♭? (p x) · t ∷ s
∂-⋁-sound []       p ()
∂-⋁-sound (x ∷ xs) p (∣ˡ    z∈p₂′x)  = (x , here refl , ∂!-sound (p x) z∈p₂′x)
∂-⋁-sound (x ∷ xs) p (∣ʳ ._ z∈p₂′xs) =
Prod1.map₀₁ id (Prod1.map₀₁ there (λ z∈ → z∈))
(∂-⋁-sound xs p z∈p₂′xs)

∂!-sound : ∀ {Tok R₁ R₂ z t s xs y} {ys : List R₁}
(p : ∞? (Parser Tok R₂ xs) (y ∷ ys)) →
z ∈ ∂! t p · s → z ∈ ♭? p · t ∷ s
∂!-sound ⟨ p ⟩ z∈p′ = ∂-sound p z∈p′

sound : ∀ {Tok R xs x} {p : Parser Tok R xs} (s : List Tok) →
x ∈ parseComplete p s → x ∈ p · s
sound []      x∈p = initial-sound _ x∈p
sound (t ∷ s) x∈p =
∂-sound _ (Simplification.sound (sound s x∈p))

------------------------------------------------------------------------
-- Completeness

private

⋁-complete : ∀ {Tok R₁ R₂ x y s} {i : R₁ → List R₂} →
(f : (x : R₁) → Parser Tok R₂ (i x)) {xs : List R₁} →
x ∈ xs → y ∈ f x · s → y ∈ ⋁ f xs · s
⋁-complete         f (here refl)  y∈fx = ∣ˡ y∈fx
⋁-complete {i = i} f (there x∈xs) y∈fx = ∣ʳ (i _) (⋁-complete f x∈xs y∈fx)

mutual

∂-complete : ∀ {Tok R xs x s t} {p : Parser Tok R xs} →
x ∈ p · t ∷ s → x ∈ ∂ t p · s
∂-complete x∈p = ∂-complete′ _ x∈p refl
where
∂-complete′ : ∀ {Tok R xs x s s′ t} (p : Parser Tok R xs) →
x ∈ p · s′ → s′ ≡ t ∷ s → x ∈ ∂ t p · s
∂-complete′ token     token       refl = return

∂-complete′ (p₁ ∣ p₂) (∣ˡ   x∈p₁) refl = ∣ˡ                  (∂-complete x∈p₁)
∂-complete′ (p₁ ∣ p₂) (∣ʳ _ x∈p₂) refl = ∣ʳ (∂-initial _ p₁) (∂-complete x∈p₂)

∂-complete′ (f <\$> p) (<\$> x∈p)   refl = <\$> ∂-complete x∈p

∂-complete′ (⟨ p₁ ⟩ ⊛ ⟪ p₂ ⟫)
(_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl =     ∂-complete f∈p₁ ⊛
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ p₁))) refl x∈p₂
∂-complete′ (⟪ p₁ ⟫ ⊛ ⟪ p₂ ⟫)
(_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl =     ∂-complete f∈p₁ ⊛
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ (♭₁ p₁)))) refl x∈p₂
∂-complete′ (⟨ p₁ ⟩ ⊛ ⟨ p₂ ⟩)
(_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl = ∣ˡ (∂-complete f∈p₁ ⊛
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ p₁))) refl x∈p₂)
∂-complete′ (_⊛_ {xs = x ∷ xs} ⟨ p₁ ⟩ ⟨ p₂ ⟩)
(_⊛_ {s₁ = []}    f∈p₁ x∈p₂) refl = ∣ʳ (∂-initial _ p₁ ⊛′ (x ∷ xs))
(cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ p₂))) refl
(⋁-complete return (initial-complete f∈p₁) return) ⊛
∂-complete x∈p₂)
∂-complete′ (⟪ p₁ ⟫ ⊛ ⟨ p₂ ⟩)
(_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl = ∣ˡ (∂-complete f∈p₁ ⊛
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ (♭₁ p₁)))) refl x∈p₂)
∂-complete′ (⟪ p₁ ⟫ ⊛ ⟨ p₂ ⟩)
(_⊛_ {s₁ = []}    f∈p₁ x∈p₂) refl = ∣ʳ []
(cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ p₂))) refl
(⋁-complete return (initial-complete f∈p₁) return) ⊛
∂-complete x∈p₂)

∂-complete′ (_>>=_ {xs = x ∷ xs} {f} p₁ p₂)
(_>>=_ {s₁ = []}    x∈p₁ y∈p₂x) refl = ∣ʳ (∂-initial _ p₁ >>=′ f)
(∂-⋁-complete p₂ (initial-complete x∈p₁) y∈p₂x)
∂-complete′ (_>>=_ {xs = x ∷ xs}     p₁ p₂)
(_>>=_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl = ∣ˡ (∂-complete x∈p₁ >>=
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ p₁))) refl
y∈p₂x)
∂-complete′ (_>>=_ {R₁} {xs = []}    p₁ p₂)
(_>>=_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl =     ∂-complete x∈p₁ >>=
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ p₁))) refl
y∈p₂x

∂-complete′ (_>>=!_ {xs = x ∷ xs} p₁ p₂)
(_>>=!_ {s₁ = []}    x∈p₁ y∈p₂x) refl = ∣ʳ []
(∂-⋁-complete p₂ (initial-complete x∈p₁) y∈p₂x)
∂-complete′ (_>>=!_ {xs = x ∷ xs}     p₁ p₂)
(_>>=!_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl = ∣ˡ (∂-complete x∈p₁ >>=!
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ (♭₁ p₁)))) refl
y∈p₂x)
∂-complete′ (_>>=!_ {R₁} {xs = []}    p₁ p₂)
(_>>=!_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl =     ∂-complete x∈p₁ >>=!
cast∈ refl (Eq1.sym (♭?♯? (∂-initial _ (♭₁ p₁)))) refl
y∈p₂x

∂-complete′ (nonempty p) (nonempty x∈p) refl = ∂-complete x∈p

∂-complete′ (cast _ p) (cast x∈p) refl = ∂-complete x∈p

∂-complete′ (return _) () refl
∂-complete′ fail       () refl
∂-complete′ (_ ⊛ ⟪ _ ⟫)            (_⊛_    {s₁ = []} f∈p₁ _) _ with initial-complete f∈p₁
... | ()
∂-complete′ (_>>=_  {xs = []} _ _) (_>>=_  {s₁ = []} x∈p₁ _) _ with initial-complete x∈p₁
... | ()
∂-complete′ (_>>=!_ {xs = []} _ _) (_>>=!_ {s₁ = []} x∈p₁ _) _ with initial-complete x∈p₁
... | ()

∂-⋁-complete : ∀ {Tok R₁ R₂ x t z s xs y} {ys : List R₁}
{f : R₁ → List R₂}
(p : (x : R₁) → ∞? (Parser Tok R₂ (f x)) (y ∷ ys)) →
x ∈ xs → z ∈ ♭? (p x) · t ∷ s → z ∈ ∂-⋁ t xs p · s
∂-⋁-complete p (here refl)  y∈px = ∣ˡ (∂!-complete (p _) y∈px)
∂-⋁-complete p (there x∈xs) y∈px =
∣ʳ (∂!-initial _ (p _)) (∂-⋁-complete p x∈xs y∈px)

∂!-complete : ∀ {Tok R₁ R₂ z t s xs y} {ys : List R₁}
(p : ∞? (Parser Tok R₂ xs) (y ∷ ys)) →
z ∈ ♭? p · t ∷ s → z ∈ ∂! t p · s
∂!-complete ⟨ p ⟩ z∈p = ∂-complete z∈p

complete : ∀ {Tok R xs x} {p : Parser Tok R xs} (s : List Tok) →
x ∈ p · s → x ∈ parseComplete p s
complete []      x∈p = initial-complete x∈p
complete (t ∷ s) x∈p =
complete s (Simplification.complete (∂-complete x∈p))
```