```------------------------------------------------------------------------
-- A semantics which uses continuation-passing style
------------------------------------------------------------------------

module TotalParserCombinators.Semantics.Continuation where

open import Algebra
open import Coinduction
open import Data.List as List
open import Data.List.Any.Membership.Propositional
using (bag) renaming (_∼[_]_ to _List-∼[_]_)
import Data.List.Properties as ListProp
open import Data.Maybe using (Maybe)
open import Data.Product as Prod
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
module LM {Tok : Set} = Monoid (List.monoid Tok)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics as S
hiding ([_-_]_⊛_; [_-_]_>>=_)

-- 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 to be language equivalent to the semantics in
-- TotalParserCombinators.Semantics).

infix  60 <\$>_
infixl 50 [_-_]_⊛_
infixl 10 [_-_]_>>=_
infix   4 _⊕_∈_·_

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

-- A simple cast lemma.

private

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

-- The definition is sound and complete with respect to the one in
-- TotalParserCombinators.Semantics.

sound′ : ∀ {Tok R xs x s₂ s} {p : Parser Tok R xs} →
x ⊕ s₂ ∈ p · s → ∃ λ s₁ → s ≡ s₁ ++ s₂ × x ∈ p · s₁
sound′ return                      = ([]    , P.refl , return)
sound′ {x = x} token               = ([ x ] , P.refl , token)
sound′ (∣-left x∈p₁)               = Prod.map id (Prod.map id ∣-left)       (sound′ x∈p₁)
sound′ (∣-right e₁ x∈p₁)           = Prod.map id (Prod.map id (∣-right e₁)) (sound′ x∈p₁)
sound′ (<\$> x∈p)                   = Prod.map id (Prod.map id (<\$>_))       (sound′ x∈p)
sound′ ([ xs - fs ] f∈p₁ ⊛ x∈p₂)   with sound′ f∈p₁ | sound′ x∈p₂
sound′ ([ xs - fs ] f∈p₁ ⊛ x∈p₂)   | (s₁ , P.refl , f∈p₁′) | (s₂ , P.refl , x∈p₂′) =
(s₁ ++ s₂ , P.sym (LM.assoc s₁ s₂ _) ,
S.[_-_]_⊛_ xs fs f∈p₁′ x∈p₂′)
sound′ (nonempty s₁ x∈p)           with sound′ x∈p
sound′ (nonempty s₁ x∈p)           | (y ∷ s , eq , x∈p′) = (y ∷ s , eq , nonempty x∈p′)
sound′ (nonempty s₁ x∈p)           | ([]    , eq , x∈p′)
with ListProp.left-identity-unique (_ ∷ s₁) (P.sym eq)
sound′ (nonempty s₁ x∈p)           | ([]    , eq , x∈p′) | ()
sound′ (cast x∈p)                  = Prod.map id (Prod.map id cast) (sound′ x∈p)
sound′ ([ f - xs ] x∈p₁ >>= y∈p₂x) with sound′ x∈p₁ | sound′ y∈p₂x
sound′ ([ f - xs ] x∈p₁ >>= y∈p₂x) | (s₁ , P.refl , x∈p₁′) | (s₂ , P.refl , y∈p₂x′) =
(s₁ ++ s₂ , P.sym (LM.assoc s₁ s₂ _) , S.[_-_]_>>=_ f xs x∈p₁′ y∈p₂x′)

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

extend : ∀ {Tok R xs x s s′ s″} {p : Parser Tok R xs} →
x ⊕ s′ ∈ p · s → x ⊕ s′ ++ s″ ∈ p · s ++ s″
extend return                       = return
extend token                        = token
extend (∣-left x∈p₁)                = ∣-left     (extend x∈p₁)
extend (∣-right e₁ x∈p₂)            = ∣-right e₁ (extend x∈p₂)
extend (<\$> x∈p)                    = <\$> extend x∈p
extend ([ xs - fs ] f∈p₁ ⊛   x∈p₂)  = [ xs - fs ] extend f∈p₁ ⊛   extend x∈p₂
extend ([ f  - xs ] x∈p₁ >>= y∈p₂x) = [ f  - xs ] extend x∈p₁ >>= extend y∈p₂x
extend (cast x∈p)                   = cast (extend x∈p)
extend (nonempty s₁ x∈p)            = cast₂ (nonempty s₁ (cast₁ (extend x∈p)))
where
lem   = LM.assoc (_ ∷ s₁) _ _
cast₁ = cast∈′        lem
cast₂ = cast∈′ (P.sym lem)

complete : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
x ∈ p · s → x ⊕ [] ∈ p · s
complete return                                 = return
complete token                                  = token
complete (∣-left x∈p₁)                          = ∣-left     (complete x∈p₁)
complete (∣-right e₁ x∈p₂)                      = ∣-right e₁ (complete x∈p₂)
complete (<\$> x∈p)                              = <\$> complete x∈p
complete (_⊛_   {fs = fs} {xs = xs} f∈p₁ x∈p₂)  = [ xs - fs ] extend (complete f∈p₁) ⊛   complete x∈p₂
complete (_>>=_ {xs = xs} {f  = f}  x∈p₁ y∈p₂x) = [ f  - xs ] extend (complete x∈p₁) >>= complete y∈p₂x
complete (cast x∈p)                             = cast (complete x∈p)
complete (nonempty {s = s} x∈p)                 = cast₂ (nonempty s (cast₁ (complete x∈p)))
where
lem   = Prod.proj₂ LM.identity _
cast₁ = cast∈′ (P.sym lem)
cast₂ = cast∈′        lem

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