------------------------------------------------------------------------
-- A language of parser equivalence proofs
------------------------------------------------------------------------

-- This module defines yet another set of equivalence relations and
-- preorders for parsers. For symmetric kinds these relations are
-- equalities (compatible equivalence relations) by construction, and
-- they are sound and complete with respect to the previously defined
-- equivalences (see TotalParserCombinators.Congruence.Sound for the
-- soundness proof). This means that parser and language equivalence
-- are also equalities. The related orderings are compatible
-- preorders.

module TotalParserCombinators.Congruence where

open import Codata.Musical.Notation
open import Data.List
open import Data.List.Relation.Binary.BagAndSetEquality
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe hiding (_>>=_)
open import Data.Nat hiding (_^_)
open import Data.Product
open import Data.Vec.Recursive
open import Function
open import Function.Related.Propositional using (SymmetricKind; ⌊_⌋)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_)

open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.CoinductiveEquality as CE
  using (_∼[_]c_; _∷_)
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
  hiding ([_-_]_⊛_; [_-_]_>>=_)

infixl  [_-_]_⊛_ [_-_-_-_]_⊛_ _<$>_
infix   [_-_]_>>=_ [_-_-_-_]_>>=_
infixl   _∣_
infix    _∷_
infix    _∼[_]P_ ∞⟨_⟩_∼[_]P_ _≅P_ _≈P_
infix    _∎
infixr   _∼⟨_⟩_ _≅⟨_⟩_

------------------------------------------------------------------------
-- Helper functions

flatten₁ : {A : Set} → Maybe (Maybe A ^ ) → Maybe A
flatten₁ nothing        = nothing
flatten₁ (just (m , _)) = m

flatten₂ : {A : Set} → Maybe (Maybe A ^ ) → Maybe A
flatten₂ nothing        = nothing
flatten₂ (just (_ , m)) = m

------------------------------------------------------------------------
-- Equivalence proof programs

mutual

  _≅P_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
  p₁ ≅P p₂ = p₁ ∼[ parser ]P p₂

  _≈P_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
  p₁ ≈P p₂ = p₁ ∼[ language ]P p₂

  data _∼[_]P_ {Tok} :
         ∀ {R xs₁ xs₂} →
         Parser Tok R xs₁ → Kind → Parser Tok R xs₂ → Set₁ where

    -- This constructor, which corresponds to CE._∷_, ensures that the
    -- relation is complete.

    _∷_ : ∀ {k R xs₁ xs₂}
            {p₁ : Parser Tok R xs₁}
            {p₂ : Parser Tok R xs₂}
          (xs₁≈xs₂ : xs₁ List-∼[ k ] xs₂)
          (Dp₁≈Dp₂ : ∀ t → ∞ (D t p₁ ∼[ k ]P D t p₂)) →
          p₁ ∼[ k ]P p₂

    -- Equational reasoning.

    _∎     : ∀ {k R xs} (p : Parser Tok R xs) → p ∼[ k ]P p

    _∼⟨_⟩_ : ∀ {k R xs₁ xs₂ xs₃}
               (p₁ : Parser Tok R xs₁)
               {p₂ : Parser Tok R xs₂}
               {p₃ : Parser Tok R xs₃}
             (p₁≈p₂ : p₁ ∼[ k ]P p₂) (p₂≈p₃ : p₂ ∼[ k ]P p₃) →
             p₁ ∼[ k ]P p₃

    _≅⟨_⟩_ : ∀ {k R xs₁ xs₂ xs₃}
               (p₁ : Parser Tok R xs₁)
               {p₂ : Parser Tok R xs₂}
               {p₃ : Parser Tok R xs₃}
             (p₁≅p₂ : p₁ ≅P p₂) (p₂≈p₃ : p₂ ∼[ k ]P p₃) →
             p₁ ∼[ k ]P p₃

    sym : ∀ {k : SymmetricKind} {R xs₁ xs₂}
            {p₁ : Parser Tok R xs₁}
            {p₂ : Parser Tok R xs₂}
          (p₁≈p₂ : p₁ ∼[ ⌊ k ⌋ ]P p₂) → p₂ ∼[ ⌊ k ⌋ ]P p₁

    -- Congruences.

    return : ∀ {k R} {x₁ x₂ : R}
             (x₁≡x₂ : x₁ ≡ x₂) → return x₁ ∼[ k ]P return x₂

    fail : ∀ {k R} → fail {R = R} ∼[ k ]P fail {R = R}

    token : ∀ {k} → token ∼[ k ]P token

    _∣_ : ∀ {k R 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₁≈p₃ : p₁ ∼[ k ]P p₃) (p₂≈p₄ : p₂ ∼[ k ]P p₄) →
          p₁ ∣ p₂ ∼[ k ]P p₃ ∣ p₄

    _<$>_ : ∀ {k R₁ R₂} {f₁ f₂ : R₁ → R₂} {xs₁ xs₂}
              {p₁ : Parser Tok R₁ xs₁}
              {p₂ : Parser Tok R₁ xs₂}
            (f₁≗f₂ : f₁ ≗ f₂) (p₁≈p₂ : p₁ ∼[ k ]P p₂) →
            f₁ <$> p₁ ∼[ k ]P f₂ <$> p₂

    [_-_]_⊛_ :
      ∀ {k R₁ R₂} xs₁xs₂ fs₁fs₂ →
      let xs₁ = flatten₁ xs₁xs₂; xs₂ = flatten₂ xs₁xs₂
          fs₁ = flatten₁ fs₁fs₂; fs₂ = flatten₂ fs₁fs₂ in
        {p₁ : ∞⟨ xs₁ ⟩Parser Tok (R₁ → R₂) (flatten fs₁)}
        {p₂ : ∞⟨ fs₁ ⟩Parser Tok  R₁       (flatten xs₁)}
        {p₃ : ∞⟨ xs₂ ⟩Parser Tok (R₁ → R₂) (flatten fs₂)}
        {p₄ : ∞⟨ fs₂ ⟩Parser Tok  R₁       (flatten xs₂)}
      (p₁≈p₃ : ∞⟨ xs₁xs₂ ⟩ p₁ ∼[ k ]P p₃)
      (p₂≈p₄ : ∞⟨ fs₁fs₂ ⟩ p₂ ∼[ k ]P p₄) →
      p₁ ⊛ p₂ ∼[ k ]P p₃ ⊛ p₄

    [_-_]_>>=_ :
      ∀ {k R₁ R₂} (f₁f₂ : Maybe (Maybe (R₁ → List R₂) ^ )) xs₁xs₂ →
      let f₁  = flatten₁ f₁f₂;   f₂  = flatten₂ f₁f₂
          xs₁ = flatten₁ xs₁xs₂; xs₂ = flatten₂ xs₁xs₂ in
        {p₁ : ∞⟨ f₁ ⟩Parser Tok R₁ (flatten xs₁)}
        {p₂ : (x : R₁) → ∞⟨ xs₁ ⟩Parser Tok R₂ (apply f₁ x)}
        {p₃ : ∞⟨ f₂ ⟩Parser Tok R₁ (flatten xs₂)}
        {p₄ : (x : R₁) → ∞⟨ xs₂ ⟩Parser Tok R₂ (apply f₂ x)}
      (p₁≈p₃ : ∞⟨ f₁f₂ ⟩ p₁ ∼[ k ]P p₃)
      (p₂≈p₄ : ∀ x → ∞⟨ xs₁xs₂ ⟩ p₂ x ∼[ k ]P p₄ x) →
      p₁ >>= p₂ ∼[ k ]P p₃ >>= p₄

    nonempty : ∀ {k R xs₁ xs₂}
                 {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
               (p₁≈p₂ : p₁ ∼[ k ]P p₂) → nonempty p₁ ∼[ k ]P nonempty p₂

    cast : ∀ {k R xs₁ xs₂ xs₁′ xs₂′}
             {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
             {xs₁≈xs₁′ : xs₁ List-∼[ bag ] xs₁′}
             {xs₂≈xs₂′ : xs₂ List-∼[ bag ] xs₂′}
           (p₁≈p₂ : p₁ ∼[ k ]P p₂) →
           cast xs₁≈xs₁′ p₁ ∼[ k ]P cast xs₂≈xs₂′ p₂

  -- Certain proofs can be coinductive if both sides are delayed.

  ∞⟨_⟩_∼[_]P_ :
    ∀ {Tok R xs₁ xs₂} {A : Set} (m₁m₂ : Maybe (Maybe A ^ )) →
    ∞⟨ flatten₁ m₁m₂ ⟩Parser Tok R xs₁ → Kind →
    ∞⟨ flatten₂ m₁m₂ ⟩Parser Tok R xs₂ → Set₁
  ∞⟨ nothing ⟩ p₁ ∼[ k ]P p₂ = ∞ (♭  p₁ ∼[ k ]P ♭  p₂)
  ∞⟨ just _  ⟩ p₁ ∼[ k ]P p₂ =    ♭? p₁ ∼[ k ]P ♭? p₂

------------------------------------------------------------------------
-- Some derived combinators

[_-_-_-_]_⊛_ :
  ∀ {k Tok R₁ R₂} xs₁ xs₂ fs₁ fs₂
    {p₁ : ∞⟨ xs₁ ⟩Parser Tok (R₁ → R₂) (flatten fs₁)}
    {p₂ : ∞⟨ fs₁ ⟩Parser Tok  R₁       (flatten xs₁)}
    {p₃ : ∞⟨ xs₂ ⟩Parser Tok (R₁ → R₂) (flatten fs₂)}
    {p₄ : ∞⟨ fs₂ ⟩Parser Tok  R₁       (flatten xs₂)} →
  ♭? p₁ ∼[ k ]P ♭? p₃ → ♭? p₂ ∼[ k ]P ♭? p₄ → p₁ ⊛ p₂ ∼[ k ]P p₃ ⊛ p₄
[ xs₁ - xs₂ - fs₁ - fs₂ ] p₁≈p₃ ⊛ p₂≈p₄ =
  [ just (xs₁ , xs₂) - just (fs₁ , fs₂) ] p₁≈p₃ ⊛ p₂≈p₄

[_-_-_-_]_>>=_ :
  ∀ {k Tok R₁ R₂} (f₁ f₂ : Maybe (R₁ → List R₂)) xs₁ xs₂
    {p₁ : ∞⟨ f₁ ⟩Parser Tok R₁ (flatten xs₁)}
    {p₂ : (x : R₁) → ∞⟨ xs₁ ⟩Parser Tok R₂ (apply f₁ x)}
    {p₃ : ∞⟨ f₂ ⟩Parser Tok R₁ (flatten xs₂)}
    {p₄ : (x : R₁) → ∞⟨ xs₂ ⟩Parser Tok R₂ (apply f₂ x)} →
  ♭? p₁ ∼[ k ]P ♭? p₃ → (∀ x → ♭? (p₂ x) ∼[ k ]P ♭? (p₄ x)) →
  p₁ >>= p₂ ∼[ k ]P p₃ >>= p₄
[ f₁ - f₂ - xs₁ - xs₂ ] p₁≈p₃ >>= p₂≈p₄ =
  [ just (f₁ , f₂) - just (xs₁ , xs₂) ] p₁≈p₃ >>= p₂≈p₄

------------------------------------------------------------------------
-- Completeness

complete : ∀ {k Tok R xs₁ xs₂}
             {p₁ : Parser Tok R xs₁}
             {p₂ : Parser Tok R xs₂} →
           p₁ ∼[ k ] p₂ → p₁ ∼[ k ]P p₂
complete = complete′ ∘ CE.complete
  where
  complete′ : ∀ {k Tok R xs₁ xs₂}
                {p₁ : Parser Tok R xs₁}
                {p₂ : Parser Tok R xs₂} →
              p₁ ∼[ k ]c p₂ → p₁ ∼[ k ]P p₂
  complete′ (xs₁≈xs₂ ∷ Dp₁≈Dp₂) =
    xs₁≈xs₂ ∷ λ t → ♯ complete′ (♭ (Dp₁≈Dp₂ t))