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

module TotalParserCombinators.Semantics where

open import Coinduction
open import Data.List hiding (drop)
import Data.List.Any as Any
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.Equality using (_⟨\$⟩_)
open import Function.Equivalence as Eq using (_⇔_; module Equivalent)
open import Function.Inverse as Inv
using (_⇿_; module Inverse; Isomorphism)
open import Level
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open Any.Membership-≡ using (bag) renaming (_≈[_]_ to _List-≈[_]_)

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  60 <\$>_
infixl 50 _⊛_   [_-_]_⊛_
infixl 10 _>>=_ [_-_]_>>=_
infix   4 _∈_·_

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 4 _≈[_]_ _≈_ _≅_ _≲_

-- 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 Any.Membership-≡ public
using (Kind) renaming (bag to parser; set to language)

-- General definition of equivalence between parsers.

_≈[_]_ : ∀ {Tok R xs₁ xs₂} →
Parser Tok R xs₁ → Kind → Parser Tok R xs₂ → Set₁
p₁ ≈[ k ] p₂ = ∀ {x s} → Isomorphism 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₂ = ∀ {x s} → x ∈ p₁ · s → x ∈ p₂ · 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₁)
≈⇔≲≳ = Eq.equivalent {t = suc zero}
(λ p₁≈p₂  → ((λ {_} → _⟨\$⟩_ (Equivalent.to   p₁≈p₂))
, λ {_} → _⟨\$⟩_ (Equivalent.from p₁≈p₂)))
(λ p₁≲≳p₂ {s} → Eq.equivalent (proj₁ p₁≲≳p₂ {s})
(proj₂ p₁≲≳p₂ {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₂ = Inv.⇿⇒ 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 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 \$ Eq.equivalent 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∈
```