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

module StructurallyRecursiveDescentParsing.Simplified.Semantics where

open import Algebra
open import Coinduction
open import Data.Bool
open import Data.List as List
private
module LM {Tok : Set} = Monoid (List.monoid Tok)
open import Data.Product as Prod
open import Function
open import Data.Empty
open import Relation.Binary.PropositionalEquality

open import TotalParserCombinators.Coinduction
open import StructurallyRecursiveDescentParsing.Simplified
open import TotalParserCombinators.Semantics as Semantics
using (return; token; ∣ˡ; ∣ʳ; _>>=_; cast)
renaming (_∈_·_ to _∈′_·_)

------------------------------------------------------------------------
-- 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.

infixl 10 _?>>=_ _!>>=_
infix   4 _∈_·_

data _∈_·_ {Tok} : ∀ {R e} → R → Parser Tok e R → List Tok → Set1 where
return : ∀ {R} {x : R} → x ∈ return x · []
token  : ∀ {x} → x ∈ token · [ x ]
∣ˡ     : ∀ {R x e₁ e₂ s} {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₁ : x ∈ p₁ · s) → x ∈ p₁ ∣ p₂ · s
∣ʳ     : ∀ {R x e₂ s} e₁ {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₂ : x ∈ p₂ · s) → x ∈ p₁ ∣ p₂ · s
_?>>=_ : ∀ {R₁ R₂ x y e₂ s₁ s₂}
{p₁ : Parser Tok true R₁} {p₂ : R₁ → Parser Tok e₂ R₂}
(x∈p₁ : x ∈ p₁ · s₁) (y∈p₂x : y ∈ p₂ x · s₂) →
y ∈ p₁ ?>>= p₂ · s₁ ++ s₂
_!>>=_ : ∀ {R₁ R₂ x y} {e₂ : R₁ → Bool} {s₁ s₂}
{p₁ : Parser Tok false R₁}
{p₂ : (x : R₁) → ∞ (Parser Tok (e₂ x) R₂)}
(x∈p₁ : x ∈ p₁ · s₁) (y∈p₂x : y ∈ ♭ (p₂ x) · s₂) →
y ∈ p₁ !>>= p₂ · s₁ ++ s₂

------------------------------------------------------------------------
-- _∈_·_ is correct with respect to _∈′_·_

sound : ∀ {Tok e R} {p : Parser Tok e R} {x s} →
x ∈ p · s → x ∈′ ⟦ p ⟧ · s
sound return              = return
sound token               = token
sound (∣ˡ x∈p₁)           = cast (∣ˡ              (sound x∈p₁))
sound (∣ʳ _ {p₁} x∈p₂)    = cast (∣ʳ (initial p₁) (sound x∈p₂))
sound (_?>>=_ {p₂ = p₂}
x∈p₁ y∈p₂x) = cast (_>>=_ {p₂ = λ x → ⟨ ⟦ p₂ x ⟧ ⟩}
(sound x∈p₁) (sound y∈p₂x))
sound (x∈p₁ !>>= y∈p₂x)   = sound x∈p₁ >>= sound y∈p₂x

complete : ∀ {Tok e R} (p : Parser Tok e R) {x s} →
x ∈′ ⟦ p ⟧ · s → x ∈ p · s
complete (return x)       return              = return
complete fail             ()
complete token            token               = token
complete (p₁ ∣ p₂)        (cast (∣ˡ    x∈p₁)) = ∣ˡ    (complete p₁ x∈p₁)
complete (_∣_ {e₁} p₁ p₂) (cast (∣ʳ ._ x∈p₂)) = ∣ʳ e₁ (complete p₂ x∈p₂)
complete (p₁ ?>>= p₂)    (cast
(x∈p₁ >>= y∈p₂x))  = complete p₁ x∈p₁ ?>>=
complete (p₂ _) y∈p₂x
complete (p₁ !>>= p₂)      (x∈p₁ >>= y∈p₂x)   = complete p₁ x∈p₁ !>>=
complete (♭ (p₂ _)) y∈p₂x

------------------------------------------------------------------------
-- A lemma

-- A simple cast lemma.

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

------------------------------------------------------------------------
-- A variant of the semantics

-- The statement x ⊕ s₂ ∈ p · s means that there is some s₁ such that
-- s ≡ s₁ ++ s₂ and x ∈ p · s₁. This variant of the semantics is
-- perhaps harder to understand, but sometimes easier to work with
-- (and it is proved equivalent to the semantics above).

infix 4 _⊕_∈_·_

data _⊕_∈_·_ {Tok} : ∀ {R e} → R → List Tok →
Parser Tok e R → List Tok → Set1 where
return : ∀ {R} {x : R} {s} → x ⊕ s ∈ return x · s
token  : ∀ {x s} → x ⊕ s ∈ token · x ∷ s
∣ˡ     : ∀ {R x e₁ e₂ s s₁}
{p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₁ : x ⊕ s₁ ∈ p₁ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
∣ʳ     : ∀ {R x e₂ s s₁} e₁
{p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₂ : x ⊕ s₁ ∈ p₂ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
_?>>=_ : ∀ {R₁ R₂ x y e₂ s s₁ s₂}
{p₁ : Parser Tok true R₁} {p₂ : R₁ → Parser Tok e₂ R₂}
(x∈p₁ : x ⊕ s₁ ∈ p₁ · s) (y∈p₂x : y ⊕ s₂ ∈ p₂ x · s₁) →
y ⊕ s₂ ∈ p₁ ?>>= p₂ · s
_!>>=_ : ∀ {R₁ R₂ x y} {e₂ : R₁ → Bool} {s s₁ s₂}
{p₁ : Parser Tok false R₁}
{p₂ : (x : R₁) → ∞ (Parser Tok (e₂ x) R₂)}
(x∈p₁ : x ⊕ s₁ ∈ p₁ · s) (y∈p₂x : y ⊕ s₂ ∈ ♭ (p₂ x) · s₁) →
y ⊕ s₂ ∈ p₁ !>>= p₂ · s

-- The definition is sound and complete with respect to the one above.

⊕-sound′ : ∀ {Tok R e x s₂ s} {p : Parser Tok e R} →
x ⊕ s₂ ∈ p · s → ∃ λ s₁ → (s ≡ s₁ ++ s₂) × (x ∈ p · s₁)
⊕-sound′ return            = ([]    , refl , return)
⊕-sound′ {x = x} token     = ([ x ] , refl , token)
⊕-sound′ (∣ˡ x∈p₁)         with ⊕-sound′ x∈p₁
⊕-sound′ (∣ˡ x∈p₁)         | (s₁ , refl , x∈p₁′) = (s₁ , refl , ∣ˡ    x∈p₁′)
⊕-sound′ (∣ʳ e₁ x∈p₁)      with ⊕-sound′ x∈p₁
⊕-sound′ (∣ʳ e₁ x∈p₁)      | (s₁ , refl , x∈p₁′) = (s₁ , refl , ∣ʳ e₁ x∈p₁′)
⊕-sound′ (x∈p₁ ?>>= y∈p₂x) with ⊕-sound′ x∈p₁ | ⊕-sound′ y∈p₂x
⊕-sound′ (x∈p₁ ?>>= y∈p₂x) | (s₁ , refl , x∈p₁′) | (s₂ , refl , y∈p₂x′) =
(s₁ ++ s₂ , sym (LM.assoc s₁ s₂ _)
, x∈p₁′ ?>>= y∈p₂x′)
⊕-sound′ (x∈p₁ !>>= y∈p₂x) with ⊕-sound′ x∈p₁ | ⊕-sound′ y∈p₂x
⊕-sound′ (x∈p₁ !>>= y∈p₂x) | (s₁ , refl , x∈p₁′) | (s₂ , refl , y∈p₂x′) =
(s₁ ++ s₂ , sym (LM.assoc s₁ s₂ _)
, x∈p₁′ !>>= y∈p₂x′)

⊕-sound : ∀ {Tok R e x s} {p : Parser Tok e R} →
x ⊕ [] ∈ p · s → x ∈ p · s
⊕-sound x∈p with ⊕-sound′ x∈p
⊕-sound x∈p | (s , refl , x∈p′) with s ++ [] | proj₂ LM.identity s
⊕-sound x∈p | (s , refl , x∈p′) | .s | refl = x∈p′

extend : ∀ {Tok R e x s s′ s″} {p : Parser Tok e R} →
x ⊕ s′ ∈ p · s → x ⊕ s′ ++ s″ ∈ p · s ++ s″
extend return            = return
extend token             = token
extend (∣ˡ x∈p₁)         = ∣ˡ    (extend x∈p₁)
extend (∣ʳ e₁ x∈p₂)      = ∣ʳ e₁ (extend x∈p₂)
extend (x∈p₁ ?>>= y∈p₂x) = extend x∈p₁ ?>>= extend y∈p₂x
extend (x∈p₁ !>>= y∈p₂x) = extend x∈p₁ !>>= extend y∈p₂x

⊕-complete : ∀ {Tok R e x s} {p : Parser Tok e R} →
x ∈ p · s → x ⊕ [] ∈ p · s
⊕-complete return            = return
⊕-complete token             = token
⊕-complete (∣ˡ x∈p₁)         = ∣ˡ    (⊕-complete x∈p₁)
⊕-complete (∣ʳ e₁ x∈p₂)      = ∣ʳ e₁ (⊕-complete x∈p₂)
⊕-complete (x∈p₁ ?>>= y∈p₂x) = extend (⊕-complete x∈p₁) ?>>=
⊕-complete y∈p₂x
⊕-complete (x∈p₁ !>>= y∈p₂x) = extend (⊕-complete x∈p₁) !>>=
⊕-complete y∈p₂x

⊕-complete′ : ∀ {Tok R e x s₂ s} {p : Parser Tok e R} →
(∃ λ s₁ → s ≡ s₁ ++ s₂ × x ∈ p · s₁) →
x ⊕ s₂ ∈ p · s
⊕-complete′ (s₁ , refl , x∈p) = extend (⊕-complete x∈p)
```