```------------------------------------------------------------------------
-- Laws related to _⊛_ and return
------------------------------------------------------------------------

module TotalParserCombinators.Laws.ApplicativeFunctor where

open import Algebra
open import Coinduction
open import Data.List as List
import Data.List.Any.BagAndSetEquality as BSEq
open import Function

using () renaming (_⊛_ to _⊛′_; _>>=_ to _>>=′_)
private
module BagMonoid {A : Set} =
CommutativeMonoid (BSEq.commutativeMonoid _ A)

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

------------------------------------------------------------------------
-- _⊛_, return, _∣_ and fail form an applicative functor "with a zero
-- and a plus"

-- Together with the additive monoid laws we get something which
-- resembles an idempotent semiring (if we restrict ourselves to
-- language equivalence).

-- First note that _⊛_ can be defined using _>>=_.

private

-- A variant of "flip map".

pam : ∀ {Tok R₁ R₂ xs} →
Parser Tok R₁ xs → (f : R₁ → R₂) →
Parser Tok R₂ (xs >>=′ [_] ∘ f)
pam p f = p >>= (return ∘ f)

infixl 10 _⊛″_

-- Note that this definition forces the argument parsers.

_⊛″_ : ∀ {Tok R₁ R₂ fs xs} →
∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)               →
∞⟨ fs ⟩Parser Tok  R₁                     (flatten xs) →
Parser Tok       R₂  (flatten fs ⊛′ flatten xs)
p₁ ⊛″ p₂ = ♭? p₁ >>= pam (♭? p₂)

⊛-in-terms-of->>= :
∀ {Tok R₁ R₂ fs xs}
(p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)            )
(p₂ : ∞⟨ fs ⟩Parser Tok  R₁                   (flatten xs)) →
p₁ ⊛ p₂ ≅P p₁ ⊛″ p₂
⊛-in-terms-of->>= {R₁ = R₁} {R₂} {fs} {xs} p₁ p₂ =
BagMonoid.reflexive (Claims.⊛flatten-⊛-flatten (flatten fs) xs) ∷ λ t → ♯ (
D t (p₁ ⊛ p₂)                                         ≅⟨ D-⊛ p₁ p₂ ⟩

D t (♭? p₁) ⊛ ♭? p₂ ∣
return⋆ (flatten fs) ⊛ D t (♭? p₂)                    ≅⟨ ⊛-in-terms-of->>= (D t (♭? p₁)) (♭? p₂) ∣′
⊛-in-terms-of->>= (return⋆ (flatten fs)) (D t (♭? p₂)) ⟩
D t (♭? p₁) ⊛″ ♭? p₂ ∣
return⋆ (flatten fs) ⊛″ D t (♭? p₂)                   ≅⟨ (D t (♭? p₁) ⊛″ ♭? p₂ ∎) ∣′
([ ○ - ○ - ○ - ○ ] return⋆ (flatten fs) ∎ >>= λ f →
sym \$ lemma t f) ⟩
D t (♭? p₁) >>= pam (♭? p₂) ∣
return⋆ (flatten fs) >>= (λ f → D t (pam (♭? p₂) f))  ≅⟨ sym \$ D->>= (♭? p₁) (pam (♭? p₂)) ⟩

D t (♭? p₁ >>= pam (♭? p₂))                           ∎)
where
lemma : ∀ t (f : R₁ → R₂) →
D t (♭? p₂ >>= λ x → return (f x)) ≅P
D t (♭? p₂) >>= λ x → return (f x)
lemma t f =
D t (pam (♭? p₂) f)                    ≅⟨ D->>= (♭? p₂) (return ∘ f) ⟩

pam (D t (♭? p₂)) f ∣
(return⋆ (flatten xs) >>= λ _ → fail)  ≅⟨ (pam (D t (♭? p₂)) f ∎) ∣′
pam (D t (♭? p₂)) f ∣ fail             ≅⟨ AdditiveMonoid.right-identity (pam (D t (♭? p₂)) f) ⟩
pam (D t (♭? p₂)) f                    ∎

-- We can then reduce all the laws to corresponding laws for _>>=_.

-- The zero laws have already been proved.

open Derivative public
using () renaming (left-zero-⊛  to left-zero;
right-zero-⊛ to right-zero)

-- _⊛_ distributes from the left over _∣_.

left-distributive : ∀ {Tok R₁ R₂ fs xs₁ xs₂}
(p₁ : Parser Tok (R₁ → R₂) fs)
(p₂ : Parser Tok R₁ xs₁)
(p₃ : Parser Tok R₁ xs₂) →
p₁ ⊛ (p₂ ∣ p₃) ≅P p₁ ⊛ p₂ ∣ p₁ ⊛ p₃
left-distributive p₁ p₂ p₃ =
p₁ ⊛  (p₂ ∣ p₃)                     ≅⟨ ⊛-in-terms-of->>= p₁ (p₂ ∣ p₃) ⟩
p₁ ⊛″ (p₂ ∣ p₃)                     ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
Monad.right-distributive p₂ p₃ (return ∘ f)) ⟩
(p₁ >>= λ f → pam p₂ f ∣ pam p₃ f)  ≅⟨ Monad.left-distributive p₁ (pam p₂) (pam p₃) ⟩
p₁ ⊛″ p₂ ∣ p₁ ⊛″ p₃                 ≅⟨ sym \$ ⊛-in-terms-of->>= p₁ p₂ ∣′
⊛-in-terms-of->>= p₁ p₃ ⟩
p₁ ⊛  p₂ ∣ p₁ ⊛  p₃                 ∎

-- _⊛_ distributes from the right over _∣_.

right-distributive : ∀ {Tok R₁ R₂ fs₁ fs₂ xs}
(p₁ : Parser Tok (R₁ → R₂) fs₁)
(p₂ : Parser Tok (R₁ → R₂) fs₂)
(p₃ : Parser Tok R₁ xs) →
(p₁ ∣ p₂) ⊛ p₃ ≅P p₁ ⊛ p₃ ∣ p₂ ⊛ p₃
right-distributive p₁ p₂ p₃ =
(p₁ ∣ p₂) ⊛  p₃      ≅⟨ ⊛-in-terms-of->>= (p₁ ∣ p₂) p₃ ⟩
(p₁ ∣ p₂) ⊛″ p₃      ≅⟨ Monad.right-distributive p₁ p₂ (pam p₃) ⟩
p₁ ⊛″ p₃ ∣ p₂ ⊛″ p₃  ≅⟨ sym \$ ⊛-in-terms-of->>= p₁ p₃ ∣′
⊛-in-terms-of->>= p₂ p₃ ⟩
p₁ ⊛  p₃ ∣ p₂ ⊛  p₃  ∎

-- Applicative functor laws.

identity : ∀ {Tok R xs} (p : Parser Tok R xs) → return id ⊛ p ≅P p
identity p =
return id ⊛  p  ≅⟨ ⊛-in-terms-of->>= (return id) p ⟩
return id ⊛″ p  ≅⟨ Monad.left-identity id (pam p) ⟩
p >>= return    ≅⟨ Monad.right-identity p ⟩
p               ∎

homomorphism : ∀ {Tok R₁ R₂} (f : R₁ → R₂) (x : R₁) →
return f ⊛ return x ≅P return {Tok = Tok} (f x)
homomorphism f x =
return f ⊛  return x  ≅⟨ ⊛-in-terms-of->>= (return f) (return x) ⟩
return f ⊛″ return x  ≅⟨ Monad.left-identity f (pam (return x)) ⟩
pam (return x) f      ≅⟨ Monad.left-identity x (return ∘ f) ⟩
return (f x)          ∎

private

infixl 10 _⊛-cong_

_⊛-cong_ :
∀ {k Tok R₁ R₂ xs₁ xs₂ fs₁ fs₂}
{p₁ : Parser Tok (R₁ → R₂) fs₁} {p₂ : Parser Tok R₁ xs₁}
{p₃ : Parser Tok (R₁ → R₂) fs₂} {p₄ : Parser Tok R₁ xs₂} →
p₁ ≈[ k ]P p₃ → p₂ ≈[ k ]P p₄ → p₁ ⊛″ p₂ ≈[ k ]P p₃ ⊛″ p₄
_⊛-cong_ {p₁ = p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄ =
p₁ ⊛″ p₂  ≅⟨ sym \$ ⊛-in-terms-of->>= p₁ p₂ ⟩
p₁ ⊛  p₂  ≈⟨ [ ○ - ○ - ○ - ○ ] p₁≈p₃ ⊛ p₂≈p₄ ⟩
p₃ ⊛  p₄  ≅⟨ ⊛-in-terms-of->>= p₃ p₄ ⟩
p₃ ⊛″ p₄  ∎

pam-lemma : ∀ {Tok R₁ R₂ R₃ xs} {g : R₂ → List R₃}
(p₁ : Parser Tok R₁ xs) (f : R₁ → R₂)
(p₂ : (x : R₂) → Parser Tok R₃ (g x)) →
pam p₁ f >>= p₂ ≅P p₁ >>= λ x → p₂ (f x)
pam-lemma p₁ f p₂ =
pam p₁ f >>= p₂                     ≅⟨ sym \$ Monad.associative p₁ (return ∘ f) p₂ ⟩
(p₁ >>= λ x → return (f x) >>= p₂)  ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ x →
(p₁ >>= λ x → p₂ (f x))             ∎

composition :
∀ {Tok R₁ R₂ R₃ fs gs xs}
(p₁ : Parser Tok (R₂ → R₃) fs)
(p₂ : Parser Tok (R₁ → R₂) gs)
(p₃ : Parser Tok R₁        xs) →
return _∘′_ ⊛ p₁ ⊛ p₂ ⊛ p₃ ≅P p₁ ⊛ (p₂ ⊛ p₃)
composition p₁ p₂ p₃ =
return _∘′_ ⊛  p₁ ⊛  p₂ ⊛  p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁ ⊛ p₂) p₃ ⟩
return _∘′_ ⊛  p₁ ⊛  p₂ ⊛″ p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁) p₂ ⊛-cong (p₃ ∎) ⟩
return _∘′_ ⊛  p₁ ⊛″ p₂ ⊛″ p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_) p₁ ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
return _∘′_ ⊛″ p₁ ⊛″ p₂ ⊛″ p₃                   ≅⟨ Monad.left-identity _∘′_ (pam p₁) ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
pam p₁ _∘′_ ⊛″ p₂ ⊛″ p₃                         ≅⟨ pam-lemma p₁ _∘′_ (pam p₂) ⊛-cong (p₃ ∎) ⟩
((p₁ >>= λ f → pam p₂ (_∘′_ f)) ⊛″ p₃)          ≅⟨ sym \$ Monad.associative p₁ (λ f → pam p₂ (_∘′_ f)) (pam p₃) ⟩
(p₁ >>= λ f → pam p₂ (_∘′_ f) >>= pam p₃)       ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
pam-lemma p₂ (_∘′_ f) (pam p₃)) ⟩
(p₁ >>= λ f → p₂ >>= λ g → pam p₃ (f ∘′ g))     ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
[ ○ - ○ - ○ - ○ ] p₂ ∎ >>= λ g →
sym \$ pam-lemma p₃ g (return ∘ f)) ⟩
(p₁ >>= λ f → p₂ >>= λ g → pam (pam p₃ g) f)    ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
Monad.associative p₂ (pam p₃) (return ∘ f)) ⟩
p₁ ⊛″ (p₂ ⊛″ p₃)                                ≅⟨ sym \$ (p₁ ∎) ⊛-cong ⊛-in-terms-of->>= p₂ p₃ ⟩
p₁ ⊛″ (p₂ ⊛  p₃)                                ≅⟨ sym \$ ⊛-in-terms-of->>= p₁ (p₂ ⊛ p₃) ⟩
p₁ ⊛  (p₂ ⊛  p₃)                                ∎

interchange : ∀ {Tok R₁ R₂ fs}
(p : Parser Tok (R₁ → R₂) fs) (x : R₁) →
p ⊛ return x ≅P return (λ f → f x) ⊛ p
interchange p x =
p ⊛  return x               ≅⟨ ⊛-in-terms-of->>= p (return x) ⟩
p ⊛″ return x               ≅⟨ ([ ○ - ○ - ○ - ○ ] p ∎ >>= λ f →
Monad.left-identity x (return ∘ f)) ⟩
(p >>= λ f → return (f x))  ≅⟨ pam p (λ f → f x) ∎ ⟩
pam p (λ f → f x)           ≅⟨ sym \$ Monad.left-identity (λ f → f x) (pam p) ⟩
return (λ f → f x) ⊛″ p     ≅⟨ sym \$ ⊛-in-terms-of->>= (return (λ f → f x)) p ⟩
return (λ f → f x) ⊛  p     ∎
```