------------------------------------------------------------------------
-- Semantics of the parsers
------------------------------------------------------------------------

module TotalParserCombinators.Semantics where

open import Codata.Musical.Notation
open import Data.List hiding (drop)
open import Data.List.Relation.Binary.BagAndSetEquality
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe using (Maybe); open Data.Maybe.Maybe
open import Data.Product
open import Data.Unit using (⊤; tt)
open import Function
open import Function.Consequences.Propositional
open import Function.Related.Propositional as Related using (Related)
open import Level
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- Semantics

-- The semantics of the parsers. x ∈ p · s means that x can be the
-- result of applying the parser p to the string s. Note that the
-- semantics is defined inductively.

infix   <$>_
infixl  _⊛_   [_-_]_⊛_
infixl  _>>=_ [_-_]_>>=_
infix    _∈_·_

data _∈_·_ {Tok} :
       ∀ {R xs} → R → Parser Tok R xs → List Tok → Set₁ where
  return   : ∀ {R} {x : R} → x ∈ return x · []
  token    : ∀ {x} → x ∈ token · [ x ]
  ∣-left   : ∀ {R x xs₁ xs₂ s}
               {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
             (x∈p₁ : x ∈ p₁ · s) → x ∈ p₁ ∣ p₂ · s
  ∣-right  : ∀ {R x xs₂ s} xs₁
               {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
             (x∈p₂ : x ∈ p₂ · s) → x ∈ p₁ ∣ p₂ · s
  <$>_     : ∀ {R₁ R₂ x s xs} {p : Parser Tok R₁ xs} {f : R₁ → R₂}
             (x∈p : x ∈ p · s) → f x ∈ f <$> p · s
  _⊛_      : ∀ {R₁ R₂ f x s₁ s₂ fs xs}
               {p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)}
               {p₂ : ∞⟨ fs ⟩Parser Tok  R₁       (flatten xs)} →
             (f∈p₁ : f ∈ ♭? p₁ · s₁)
             (x∈p₂ : x ∈ ♭? p₂ · s₂) →
             f x ∈ p₁ ⊛ p₂ · s₁ ++ s₂
  _>>=_    : ∀ {R₁ R₂ x y s₁ s₂ xs} {f : Maybe (R₁ → List R₂)}
               {p₁ : ∞⟨ f ⟩Parser Tok R₁ (flatten xs)}
               {p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)}
             (x∈p₁ : x ∈ ♭? p₁ · s₁)
             (y∈p₂x : y ∈ ♭? (p₂ x) · s₂) →
             y ∈ p₁ >>= p₂ · s₁ ++ s₂
  nonempty : ∀ {R xs x y s} {p : Parser Tok R xs}
             (x∈p : y ∈ p · x ∷ s) → y ∈ nonempty p · x ∷ s
  cast     : ∀ {R xs₁ xs₂ x s}
               {xs₁≈xs₂ : xs₁ List-∼[ bag ] xs₂} {p : Parser Tok R xs₁}
             (x∈p : x ∈ p · s) → x ∈ cast xs₁≈xs₂ p · s

-- Some variants with fewer implicit arguments. (The arguments xs and
-- fs can usually not be inferred, but I do not want to mention them
-- in the paper, so I have made them implicit in the definition
-- above.)

[_-_]_⊛_ : ∀ {Tok R₁ R₂ f x s₁ s₂} xs fs
             {p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)}
             {p₂ : ∞⟨ fs ⟩Parser Tok  R₁       (flatten xs)} →
           f ∈ ♭? p₁ · s₁ → x ∈ ♭? p₂ · s₂ → f x ∈ p₁ ⊛ p₂ · s₁ ++ s₂
[ xs - fs ] f∈p₁ ⊛ x∈p₂ = _⊛_ {fs = fs} {xs = xs} f∈p₁ x∈p₂

[_-_]_>>=_ : ∀ {Tok R₁ R₂ x y s₁ s₂} (f : Maybe (R₁ → List R₂)) xs
               {p₁ : ∞⟨ f ⟩Parser Tok R₁ (flatten xs)}
               {p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)} →
             x ∈ ♭? p₁ · s₁ → y ∈ ♭? (p₂ x) · s₂ →
             y ∈ p₁ >>= p₂ · s₁ ++ s₂
[ f - xs ] x∈p₁ >>= y∈p₂x = _>>=_ {xs = xs} {f = f} x∈p₁ y∈p₂x

------------------------------------------------------------------------
-- Parser and language equivalence

infix  _∼[_]_ _≈_ _≅_ _≲_ _≲→_

-- There are two kinds of equivalences. Parser equivalences are
-- stronger, and correspond to bag equality. Language equivalences are
-- weaker, and correspond to set equality.

open Data.List.Relation.Binary.BagAndSetEquality public
  using (Kind)
  renaming ( bag      to parser
           ; set      to language
           ; subbag   to subparser
           ; subset   to sublanguage
           ; superbag to superparser
           ; superset to superlanguage
           )

-- General definition of equivalence between parsers. (Note that this
-- definition also gives access to some ordering relations.)

_∼[_]_ : ∀ {Tok R xs₁ xs₂} →
         Parser Tok R xs₁ → Kind → Parser Tok R xs₂ → Set₁
p₁ ∼[ k ] p₂ = ∀ {x s} → Related k (x ∈ p₁ · s) (x ∈ p₂ · s)

-- Language equivalence. (Corresponds to set equality.)

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

-- Parser equivalence. (Corresponds to bag equality.)

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

-- p₁ ≲ p₂ means that the language defined by p₂ contains all the
-- string/result pairs contained in the language defined by p₁.

_≲_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
p₁ ≲ p₂ = p₁ ∼[ sublanguage ] p₂

-- A variant of p₁ ≲ p₂.

_≲→_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
p₁ ≲→ p₂ = ∀ {x s} → x ∈ p₁ · s → x ∈ p₂ · s

-- The relation _≲_ is pointwise logically equivalent to p₁ ≲→ p₂.

≲⇔≲→ :
  ∀ {Tok R xs₁ xs₂} {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
  p₁ ≲ p₂ ⇔ p₁ ≲→ p₂
≲⇔≲→ = mk⇔
  (λ f {x = x} {s = s} → Func.to (f {x = x} {s = s}))
  (λ f {x = x} {s = s} → mk⟶ (f {x = x} {s = s}))

-- p₁ ≈ p₂ iff both p₁ ≲ p₂ and p₂ ≲ p₁.

≈⇔≲≳ : ∀ {Tok R xs₁ xs₂}
         {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
       p₁ ≈ p₂ ⇔ (p₁ ≲ p₂ × p₂ ≲ p₁)
≈⇔≲≳ = mk⇔
  (λ p₁≈p₂  →
     ((λ {x s} → mk⟶ (Equivalence.to   (p₁≈p₂ {x = x} {s = s})))
     , λ {x s} → mk⟶ (Equivalence.from (p₁≈p₂ {x = x} {s = s}))))
  (λ p₁≲≳p₂ → λ {x s} →
     mk⇔ (Func.to (proj₁ p₁≲≳p₂ {s = s}))
       (Func.to (proj₂ p₁≲≳p₂ {s = s})))

-- Parser equivalence implies language equivalence.

≅⇒≈ : ∀ {Tok R xs₁ xs₂}
        {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
      p₁ ≅ p₂ → p₁ ≈ p₂
≅⇒≈ p₁≅p₂ = Related.↔⇒ p₁≅p₂

-- Language equivalence does not (in general) imply parser
-- equivalence.

¬≈⇒≅ : ¬ (∀ {Tok R xs₁ xs₂}
            {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
          p₁ ≈ p₂ → p₁ ≅ p₂)
¬≈⇒≅ hyp with inverseʳ⇒injective _ (Inverse.inverseʳ p₁≅p₂)
                {∣-left return} {∣-right [ tt ] return} (lemma _ _)
  where
  p₁ : Parser ⊤ ⊤ _
  p₁ = return tt ∣ return tt

  p₂ : Parser ⊤ ⊤ _
  p₂ = return tt

  p₁≲p₂ : p₁ ≲→ p₂
  p₁≲p₂ (∣-left     return) = return
  p₁≲p₂ (∣-right ._ return) = return

  p₁≅p₂ : p₁ ≅ p₂
  p₁≅p₂ = hyp $ mk⇔ p₁≲p₂ ∣-left

  lemma : ∀ {x s} (x∈₁ x∈₂ : x ∈ p₂ · s) → x∈₁ ≡ x∈₂
  lemma return return = P.refl

... | ()

------------------------------------------------------------------------
-- A simple cast lemma

cast∈ : ∀ {Tok R xs} {p p′ : Parser Tok R xs} {x x′ s s′} →
        x ≡ x′ → p ≡ p′ → s ≡ s′ → x ∈ p · s → x′ ∈ p′ · s′
cast∈ P.refl P.refl P.refl x∈ = x∈