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

open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Function.Related as Related using (Kind; SK-sym)

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₂′))

open import Codata.Musical.Notation
open import Function.Base
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₂′)        )
  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₂ =
    (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₂ =
    (P  x  x  p₁ · t  s)  x  x  p₂ · t  s)
        x  x  lift p₁ p₂ · t  s)                 ∼⟨ SK-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