------------------------------------------------------------------------
-- 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₂′
p₂′         )
... | (_  , p₁′           , p₁≅p₁′)
| (._ , fail          , p₂≅∅)   = _ , _ , (
p₁   p₂    ≅⟨ p₁≅p₁′ ∣′ 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