------------------------------------------------------------------------
-- Simplification of parsers
------------------------------------------------------------------------

module TotalParserCombinators.Simplification where

open import Coinduction
open import Data.List using (List)
open import Data.Maybe using (Maybe); open Data.Maybe.Maybe
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality
  using (refl) renaming (_≅_ to _≅H_)

open import TotalParserCombinators.Congruence
  hiding (return; fail; token) renaming (_∣_ to _∣′_)
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- A helper function

private

  force : ∀ {Tok R xs} (p : ∞ (Parser Tok R xs)) →
          ∃ λ (p′ : Parser _ _ xs) → ♭ p ≅P p′
  force p = (♭ p , (♭ p ∎))

------------------------------------------------------------------------
-- Simplification

-- The function simplify₁ simplifies the first "layer" of a parser,
-- down to the first occurrences of ♯_. The following simplifications
-- are applied in a bottom-up manner:
--
-- f <$> fail                  → fail
-- f <$> return x              → return (f x)
-- fail         ∣ p            → p
-- p            ∣ fail         → p
-- token >>= p₁ ∣ token >>= p₂ → token >>= (λ t → p₁ t ∣ p₂ t)  (*)
-- fail     ⊛ p                → fail
-- p        ⊛ fail             → fail
-- return f ⊛ return x         → return (f x)
-- fail     >>= p              → fail
-- return x >>= p              → p x
-- nonempty fail               → fail
-- cast eq p                   → p
--
-- (*) Currently only when p₁ and p₂ are not delayed.
--
-- An example of a possible future addition:
--
-- (p₁ >>= p₂) >>= p₃ → ♭? p₁ >>= λ x → ♭? (p₂ x) >>= (♭? ∘ p₃)

private
 mutual

  simplify₁ : ∀ {Tok R xs} (p : Parser Tok R xs) →
              ∃₂ λ xs (p′ : Parser Tok R xs) → p ≅P p′

  -- • return:

  simplify₁ (return x) = (_ , return x , (return x ∎))

  -- • fail:

  simplify₁ fail       = (_ , fail     , (fail ∎))

  -- • token:

  simplify₁ token      = (_ , token    , (token ∎))

  -- • _<$>_:

  simplify₁ (f <$> p) with simplify₁ p
  ... | (._ , fail     , p≅∅)  = _ , _ , (
                                 f <$> p     ≅⟨ (λ _ → refl) <$> p≅∅ ⟩
                                 f <$> fail  ≅⟨ <$>.zero ⟩
                                 fail        ∎)
  ... | (._ , return x , p≅ε)  = _ , _ , (
                                 f <$> p         ≅⟨ (λ x → refl {x = f x}) <$> p≅ε ⟩
                                 f <$> return x  ≅⟨ <$>.homomorphism f ⟩
                                 return (f x)    ∎)
  ... | (_  , p′       , p≅p′) = _ , _ , (
                                 f <$> p   ≅⟨ (λ _ → refl) <$> p≅p′ ⟩
                                 f <$> p′  ∎)

  -- • _∣_:

  simplify₁ (p₁ ∣ p₂) with simplify₁ p₁ | simplify₁ p₂
  ... | (._ , fail          , p₁≅∅)
      | (_  , p₂′           , p₂≅p₂′) = _ , _ , (
                                        p₁   ∣ p₂   ≅⟨ p₁≅∅ ∣′ p₂≅p₂′ ⟩
                                        fail ∣ p₂′  ≅⟨ AdditiveMonoid.left-identity p₂′ ⟩
                                        p₂′         ∎)
  ... | (_  , p₁′           , p₁≅p₁′)
      | (._ , fail          , p₂≅∅)   = _ , _ , (
                                        p₁  ∣ p₂    ≅⟨ p₁≅p₁′ ∣′ p₂≅∅ ⟩
                                        p₁′ ∣ fail  ≅⟨ AdditiveMonoid.right-identity p₁′ ⟩
                                        p₁′         ∎)
  ... | (._ , _>>=_ {xs = just ._}
                    {f  = just _}
                    token p₁′ , p₁≅…)
      | (._ , _>>=_ {xs = just ._}
                    {f  = just _}
                    token p₂′ , p₂≅…) = _ , _ , (
                                        p₁            ∣ p₂               ≅⟨ p₁≅… ∣′ p₂≅… ⟩
                                        token >>= p₁′ ∣ token >>= p₂′    ≅⟨ [ ○ - ○ - ○ - ○ ] token ∎ >>= (λ x → p₁′ x ∎) ∣′
                                                                            [ ○ - ○ - ○ - ○ ] token ∎ >>= (λ x → p₂′ x ∎) ⟩
                                        token >>= p₁′ ∣ token >>= p₂′    ≅⟨ sym $ Monad.left-distributive token p₁′ p₂′ ⟩
                                        token >>= (λ t → p₁′ t ∣ p₂′ t)  ∎)
  ... | (_  , p₁′           , p₁≅p₁′)
      | (_  , p₂′           , p₂≅p₂′) = _ , _ , (
                                        p₁  ∣ p₂   ≅⟨ p₁≅p₁′ ∣′ p₂≅p₂′ ⟩
                                        p₁′ ∣ p₂′  ∎)

  -- • _⊛_:

  simplify₁ (p₁ ⊛ p₂) =
    helper _ _ p₁ p₂ (simplify₁′ p₁) (simplify₁′ p₂) refl refl
    where
    -- token ⊛ token is never type correct, but Agda's case-splitting
    -- machinery cannot see this, so instead of a with clause the
    -- following ugly machinery is used.

    cast₁ : ∀ {Tok R R₁ R₁′ xs xs′} {ys : Maybe (List R)} →
            (R≡  : R₁ ≡ R₁′) → xs ≅H xs′ →
            ∞⟨ ys ⟩Parser Tok R₁′ (flatten xs′) →
            ∞⟨ ys ⟩Parser Tok R₁  (flatten xs)
    cast₁ refl refl p = p

    helper : ∀ {Tok R₁ R₁′ R₂} fs xs {xs′}
               (p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs))
               (p₂ : ∞⟨ fs ⟩Parser Tok  R₁′      (flatten xs′)) →
             (∃₂ λ xs (p₁′ : Parser _ _ xs) → ♭? p₁ ≅P p₁′) →
             (∃₂ λ xs (p₂′ : Parser _ _ xs) → ♭? p₂ ≅P p₂′) →
             (R≡  : R₁ ≡ R₁′) →
             (xs≅ : xs ≅H xs′) →
             ∃₂ λ xs (p′ : Parser _ _ xs) → p₁ ⊛ cast₁ R≡ xs≅ p₂ ≅P p′
    helper fs xs p₁ p₂ (._ , fail , p₁≅∅) _ refl refl = _ , _ , (
      p₁   ⊛ p₂     ≅⟨ [ xs - ○ - fs - ○ ] p₁≅∅ ⊛ (♭? p₂ ∎) ⟩
      fail ⊛ ♭? p₂  ≅⟨ ApplicativeFunctor.left-zero (♭? p₂) ⟩
      fail          ∎)
    helper fs xs p₁ p₂ _ (._ , fail , p₂≅∅) refl refl = _ , _ , (
      p₁    ⊛ p₂    ≅⟨ [ xs - ○ - fs - ○ ] ♭? p₁ ∎ ⊛ p₂≅∅ ⟩
      ♭? p₁ ⊛ fail  ≅⟨ ApplicativeFunctor.right-zero (♭? p₁) ⟩
      fail          ∎)
    helper fs xs p₁ p₂ (._ , return f , p₁≅ε) (._ , return x , p₂≅ε)
           refl refl = _ , _ , (
      p₁       ⊛ p₂        ≅⟨ [ xs - ○ - fs - ○ ] p₁≅ε ⊛ p₂≅ε ⟩
      return f ⊛ return x  ≅⟨ ApplicativeFunctor.homomorphism f x ⟩
      return (f x)         ∎)
    helper fs xs p₁ p₂ p₁′ p₂′ R≡ xs≅ =
      helper′ fs xs p₁ p₂ p₁′ p₂′ R≡ xs≅
      where
      helper′ :
        ∀ {Tok R₁ R₁′ R₂} fs xs {xs′}
          (p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs))
          (p₂ : ∞⟨ fs ⟩Parser Tok  R₁′      (flatten xs′)) →
        (∃₂ λ xs (p₁′ : Parser _ _ xs) → ♭? p₁ ≅P p₁′) →
        (∃₂ λ xs (p₂′ : Parser _ _ xs) → ♭? p₂ ≅P p₂′) →
        (R≡  : R₁ ≡ R₁′) →
        (xs≅ : xs ≅H xs′) →
        ∃₂ λ xs (p′ : Parser _ _ xs) → p₁ ⊛ cast₁ R≡ xs≅ p₂ ≅P p′
      helper′ fs xs p₁ p₂ (_ , p₁′ , p₁≅p₁′) (_ , p₂′ , p₂≅p₂′)
              refl refl = _ , _ , (
        p₁  ⊛ p₂   ≅⟨ [ xs - ○ - fs - ○ ] p₁≅p₁′ ⊛ p₂≅p₂′ ⟩
        p₁′ ⊛ p₂′  ∎)

  -- • _>>=_:

  simplify₁ (_>>=_ {xs = xs} {f = f} p₁ p₂) with simplify₁′ p₁
  ... | (._ , fail     , p₁≅∅)  = _ , _ , (
                                  p₁   >>= p₂         ≅⟨ [ f - ○ - xs - ○ ] p₁≅∅ >>= (λ x → ♭? (p₂ x) ∎) ⟩
                                  fail >>= (♭? ∘ p₂)  ≅⟨ Monad.left-zero (♭? ∘ p₂) ⟩
                                  fail                ∎)
  ... | (._ , return x , p₁≅ε) with simplify₁′ (p₂ x)
  ...   | (_ , p₂x′ , p₂x≅p₂x′) = _ , _ , (
                                  p₁       >>= p₂         ≅⟨ [ f - ○ - xs - ○ ] p₁≅ε >>= (λ x → ♭? (p₂ x) ∎) ⟩
                                  return x >>= (♭? ∘ p₂)  ≅⟨ Monad.left-identity x (♭? ∘ p₂) ⟩
                                  ♭? (p₂ x)               ≅⟨ p₂x≅p₂x′ ⟩
                                  p₂x′                    ∎)
  simplify₁ (_>>=_ {xs = xs} {f = f} p₁ p₂)
      | (_ , p₁′ , p₁≅p₁′)      = _ , _ , (
                                  p₁  >>= p₂         ≅⟨ [ f - ○ - xs - ○ ] p₁≅p₁′ >>= (λ x → ♭? (p₂ x) ∎) ⟩
                                  p₁′ >>= (♭? ∘ p₂)  ∎)

  -- • nonempty:

  simplify₁ (nonempty p) with simplify₁ p
  ... | (._ , fail , p≅∅)  = _ , _ , (
                             nonempty p     ≅⟨ nonempty p≅∅ ⟩
                             nonempty fail  ≅⟨ Nonempty.zero ⟩
                             fail           ∎)
  ... | (_  , p′   , p≅p′) = _ , _ , (
                             nonempty p   ≅⟨ nonempty p≅p′ ⟩
                             nonempty p′  ∎)

  -- • cast:

  simplify₁ (cast xs₁≈xs₂ p) with simplify₁ p
  ... | (_ , p′ , p≅p′) = _ , _ , (
                          cast xs₁≈xs₂ p  ≅⟨ Cast.correct ⟩
                          p               ≅⟨ p≅p′ ⟩
                          p′              ∎)

  -- Note that if an argument parser is delayed, then simplification
  -- is not applied recursively (because this could lead to
  -- non-termination). Partial simplification, for instance up to a
  -- predetermined depth, would be possible, but for simplicity
  -- delayed parsers are simply forced and returned.

  simplify₁′ : ∀ {Tok R R′ xs} {m : Maybe R′}
               (p : ∞⟨ m ⟩Parser Tok R xs) →
               ∃₂ λ xs (p′ : Parser Tok R xs) → ♭? p ≅P p′
  simplify₁′ {m = nothing} p = (_ , ♭ p , (♭ p ∎))
  simplify₁′ {m = just _}  p = simplify₁ p

-- A simplifier.

simplify-initial : ∀ {Tok R xs} → Parser Tok R xs → List R
simplify-initial = proj₁ ∘ simplify₁

simplify : ∀ {Tok R xs} (p : Parser Tok R xs) →
           Parser Tok R (simplify-initial p)
simplify p = proj₁ $ proj₂ $ simplify₁ p

-- The simplifier is correct.

correct : ∀ {Tok R xs} {p : Parser Tok R xs} → simplify p ≅P p
correct {p = p} = sym $ proj₂ $ proj₂ $ simplify₁ p