------------------------------------------------------------------------
-- Pointwise lifting of (binary) initial bag operators to parsers
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

open import Data.List
import Data.List.Any as Any
open import Function.Related as Related using (Kind)
open Any.Membership-≡ using (_∈_) renaming (_∼[_]_ to _List-∼[_]_)

module TotalParserCombinators.Pointwise
(R₁ R₂ : Set) {R₃ : Set}

-- Some kinds of equality.
{K : Set} (⌊_⌋ : K  Kind)

-- An initial bag operator.
(_∙_ : List R₁  List R₂  List R₃)

-- The operator must preserve the given notions of equality.
(_∙-cong_ :  {k xs₁ xs₁′ xs₂ xs₂′}
xs₁ List-∼[  k  ] xs₁′  xs₂ List-∼[  k  ] xs₂′
(xs₁  xs₂) List-∼[  k  ] (xs₁′  xs₂′))
where

open import Coinduction
open import Function
open import Function.Equality using (_⟨\$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Function.Inverse using (_↔_; module Inverse)

open import TotalParserCombinators.Congruence as C using (_∼[_]P_; _≅P_)
import TotalParserCombinators.Congruence.Sound as CS
open import TotalParserCombinators.Derivative as D
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics using (_∈_·_)

------------------------------------------------------------------------
-- Lift

-- A lifting of the initial bag operator _∙_ to the level of parsers.
--
-- Note that this definition is closely related to Theorem 4.4 in
-- Brzozowski's paper "Derivatives of Regular Expressions".
--
-- Note also that _∙_ is allowed to pattern match on the input
-- indices, so it may not be obvious that lift preserves equality.
-- This fact is established explicitly below (by making use of
-- _∙-cong_).

lift :  {Tok xs₁ xs₂}
Parser Tok R₁ xs₁  Parser Tok R₂ xs₂
Parser Tok R₃ (xs₁  xs₂)
lift p₁ p₂ =
(token >>= λ t   lift (D t p₁) (D t p₂))
return⋆ (initial-bag p₁  initial-bag p₂)

------------------------------------------------------------------------
-- Properties of lift

-- D distributes over lift.

D-lift :  {Tok xs₁ xs₂ t}
(p₁ : Parser Tok R₁ xs₁) (p₂ : Parser Tok R₂ xs₂)
D t (lift p₁ p₂) ≅P lift (D t p₁) (D t p₂)
D-lift {xs₁ = xs₁} {xs₂} {t} p₁ p₂ =
D t (lift p₁ p₂)                               ≅⟨ D t (lift p₁ p₂)

(return t >>= λ t  lift (D t p₁) (D t p₂))
D t (return⋆ (xs₁  xs₂))                    ≅⟨ Monad.left-identity t  t  lift (D t p₁) (D t p₂))
D.D-return⋆ (xs₁  xs₂)
lift (D t p₁) (D t p₂)  fail                  ≅⟨ AdditiveMonoid.right-identity (lift (D t p₁) (D t p₂))

lift (D t p₁) (D t p₂)
where open C using (_≅⟨_⟩_; _∎; _∣_)

-- lift preserves equality.

lift-cong :  {k Tok xs₁ xs₁′ xs₂ xs₂′}
{p₁ : Parser Tok R₁ xs₁} {p₁′ : Parser Tok R₁ xs₁′}
{p₂ : Parser Tok R₂ xs₂} {p₂′ : Parser Tok R₂ xs₂′}
p₁ ∼[  k  ]P p₁′  p₂ ∼[  k  ]P p₂′
lift p₁ p₂ ∼[  k  ]P lift p₁′ p₂′
lift-cong {k} {xs₁ = xs₁} {xs₁′} {xs₂} {xs₂′} {p₁} {p₁′} {p₂} {p₂′}
p₁≈p₁′ p₂≈p₂′ = lemma  λ t   (
D t (lift p₁ p₂)          ≅⟨ D-lift p₁ p₂
lift (D t p₁) (D t p₂)    ∼⟨ lift-cong (CS.D-cong p₁≈p₁′) (CS.D-cong p₂≈p₂′)
lift (D t p₁′) (D t p₂′)  ≅⟨ sym (D-lift p₁′ p₂′)
D t (lift p₁′ p₂′)        )
where
open C using (_≅⟨_⟩_; _∼⟨_⟩_; _∎; sym; _∷_)

lemma : (xs₁  xs₂) List-∼[  k  ] (xs₁′  xs₂′)
lemma = I.cong (CS.sound p₁≈p₁′) ∙-cong I.cong (CS.sound p₂≈p₂′)

-- Lifts a property from _∙_ to lift. For examples of its use, see
-- TotalParserCombinators.{And,AsymmetricChoice,Not}.

lift-property :
(P :  {}  (R₁  Set )  (R₂  Set )  (R₃  Set )  Set )

(P-cong :
{}  {F₁  : R₁  Set }  {F₂  : R₂  Set }  {F₃  : R₃  Set }
{ℓ′} {F₁′ : R₁  Set ℓ′} {F₂′ : R₂  Set ℓ′} {F₃′ : R₃  Set ℓ′}
(∀ x  F₁ x  F₁′ x)  (∀ x  F₂ x  F₂′ x)  (∀ x  F₃ x  F₃′ x)
P F₁ F₂ F₃  P F₁′ F₂′ F₃′)

(P-∙ :
{xs₁ xs₂}
P  x  x  xs₁)  x  x  xs₂)  x  x  (xs₁  xs₂)))

{Tok xs₁ xs₂ s}
(p₁ : Parser Tok R₁ xs₁) (p₂ : Parser Tok R₂ xs₂)
P  x  x  p₁ · s)  x  x  p₂ · s)  x  x  lift p₁ p₂ · s)

lift-property P P-cong P-∙ {s = []} p₁ p₂ =
Equivalence.from
(P  x  x  p₁ · [])  x  x  p₂ · [])
x  x  lift p₁ p₂ · [])                            ∼⟨ P-cong  _  I.correct)  _  I.correct)  _  I.correct)

P  x  x  initial-bag p₁)  x  x  initial-bag p₂)
x  x  (initial-bag p₁  initial-bag p₂))

) ⟨\$⟩ P-∙
where open Related.EquationalReasoning

lift-property P P-cong P-∙ {s = t  s} p₁ p₂ =
Equivalence.from
(P  x  x  p₁ · t  s)  x  x  p₂ · t  s)
x  x  lift p₁ p₂ · t  s)                 ∼⟨ sym \$ P-cong  _  D.correct)  _  D.correct)  _  D.correct)

P  x  x  D t p₁ · s)  x  x  D t p₂ · s)
x  x  D t (lift p₁ p₂) · s)               ∼⟨ P-cong  _  _ )  _  _ )  _  CS.sound (D-lift p₁ p₂))

P  x  x  D t p₁ · s)  x  x  D t p₂ · s)
x  x  lift (D t p₁) (D t p₂) · s)

) ⟨\$⟩ lift-property P P-cong P-∙ (D t p₁) (D t p₂)
where open Related.EquationalReasoning