```------------------------------------------------------------------------
-- The parser type
------------------------------------------------------------------------

module TotalParserCombinators.Parser where

open import Algebra
open import Codata.Musical.Notation
open import Data.List
open import Data.Maybe using (Maybe; nothing; just)
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.Product using (proj₂)
open import Function
open import Level
open import Relation.Binary.PropositionalEquality

using ()
renaming ( pure  to return′
; ∅     to fail′
; _∣_   to _∣′_
; _⊛_   to _⊛′_
; _>>=_ to _>>=′_
)

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

-- Flattening for potential lists.

flatten : {A : Set} → Maybe (List A) → List A
flatten nothing   = []
flatten (just xs) = xs

-- fs ⊛flatten mxs is a variant of fs ⊛′ flatten mxs, with the
-- property that fs ⊛flatten nothing evaluates to [].

_⊛flatten_ : {A B : Set} → List (A → B) → Maybe (List A) → List B
fs ⊛flatten nothing = []
fs ⊛flatten just xs = fs ⊛′ xs

-- Applies the function to the value, returning the empty list if
-- there is no function.

apply : {A B : Set} → Maybe (A → List B) → A → List B
apply nothing  x = []
apply (just f) x = f x

-- bind mxs mf is a variant of flatten mxs >>=′ apply mf, with the
-- property that bind mxs nothing evaluates to [].

bind :  {A B : Set} → Maybe (List A) → Maybe (A → List B) → List B
bind mxs nothing  = []
bind mxs (just f) = flatten mxs >>=′ f

-- Verification of some claims made above.

module Claims where

⊛flatten-⊛-flatten : ∀ {A B : Set} (fs : List (A → B)) mxs →
fs ⊛flatten mxs ≡ (fs ⊛′ flatten mxs)
⊛flatten-⊛-flatten fs nothing   = sym \$ ListMonadProp.right-zero fs
⊛flatten-⊛-flatten fs (just xs) = refl

⊛flatten-nothing : {A B : Set} (fs : List (A → B)) →
fs ⊛flatten nothing ≡ []
⊛flatten-nothing fs = refl

bind-flatten->>=-apply : ∀ {A B : Set} mxs (mf : Maybe (A → List B)) →
bind mxs mf ≡ (flatten mxs >>=′ apply mf)
bind-flatten->>=-apply mxs (just f) = refl
bind-flatten->>=-apply mxs nothing  =

bind-nothing : {A B : Set} (mxs : Maybe (List A)) →
bind mxs nothing ≡ [] {A = B}
bind-nothing mxs = refl

------------------------------------------------------------------------
-- Parsers

infixl 50 _⊛_ _<\$>_ _⊛flatten_
infixl 10 _>>=_
infixl  5 _∣_

-- The list index is the "initial bag"; it contains the results which
-- can be emitted without consuming any input. For
--   p : Parser Tok R xs
-- we have
--   x ∈ xs  iff  x ∈ p · []
-- (see TotalParserCombinators.InitialBag).

mutual

data Parser (Tok : Set) : (R : Set) → List R → Set₁ where
return   : ∀ {R} (x : R) → Parser Tok R (return′ x)
fail     : ∀ {R} → Parser Tok R fail′
token    : Parser Tok Tok fail′
_∣_      : ∀ {R xs₁ xs₂}
(p₁ : Parser Tok R  xs₁       )
(p₂ : Parser Tok R         xs₂) →
Parser Tok R (xs₁ ∣′ xs₂)
_<\$>_    : ∀ {R₁ R₂ xs}
(f : R₁ → R₂)
(p : Parser Tok R₁        xs) →
Parser Tok R₂ (map f xs)
_⊛_      : ∀ {R₁ R₂ fs xs}
(p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)            )
(p₂ : ∞⟨ fs ⟩Parser Tok  R₁                   (flatten xs)) →
Parser Tok       R₂  (flatten fs ⊛flatten xs)
_>>=_    : ∀ {R₁ R₂ xs} {f : Maybe (R₁ → List R₂)}
(p₁ :            ∞⟨ f  ⟩Parser Tok R₁ (flatten xs))
(p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)) →
Parser Tok R₂ (bind xs f)
nonempty : ∀ {R xs} (p : Parser Tok R xs) → Parser Tok R []
cast     : ∀ {R xs₁ xs₂} (xs₁≈xs₂ : xs₁ ∼[ bag ] xs₂)
(p : Parser Tok R xs₁) → Parser Tok R xs₂

∞⟨_⟩Parser : {A : Set} → Maybe A → Set → (R : Set) → List R → Set₁
∞⟨ nothing ⟩Parser Tok R₁ xs = ∞ (Parser Tok R₁ xs)
∞⟨ just _  ⟩Parser Tok R₁ xs =    Parser Tok R₁ xs

-- Note that, with the definition above, a sequenced parser is
-- /allowed/ to be delayed if the "other" parser is not nullable, but
-- it does not have to be.

-- Note also that it would be safe to make the first argument of _>>=_
-- coinductive if apply f x ≡_[] for all x in xs. I suspect that this
-- criterion would be awkward to work with, though. Instead I only
-- allow the argument to be coinductive if f ≡ nothing.

-- Finally note that some of the combinators above are not included in
-- the paper "Total Parser Combinators".

------------------------------------------------------------------------
-- Examples

private

-- Note that these parsers can be both left and right recursive:

leftRight : ∀ {R Tok} → Parser Tok R _
leftRight {R} = ♯ (const <\$> leftRight) ⊛ ♯ leftRight {R}

leftRight′ : ∀ {R Tok} → Parser Tok R _
leftRight′ {R} = ♯ leftRight′ {R} >>= λ _ → ♯ leftRight′

-- More examples, included to ensure that all implicit arguments are
-- inferred automatically.

p : {Tok R : Set} → Parser Tok R _
p = token >>= λ _ → ♯ p

p′ : {Tok : Set} → Parser Tok Tok _
p′ = ♯ p′ >>= λ _ → token

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

-- Returns the initial bag.

initial-bag : ∀ {Tok R xs} → Parser Tok R xs → List R
initial-bag {xs = xs} _ = xs

-- Forces if necessary.

♭? : ∀ {Tok R₁ R₂} {m : Maybe R₂} {xs} →
∞⟨ m ⟩Parser Tok R₁ xs → Parser Tok R₁ xs
♭? {m = nothing} = ♭
♭? {m = just _}  = id

-- Is the argument parser forced? If the result is just something,
-- then it is.

forced? : ∀ {Tok A R xs} {m : Maybe A} →
∞⟨ m ⟩Parser Tok R xs → Maybe A
forced? {m = m} _ = m

forced?′ : {Tok R₁ R₂ A : Set} {m : Maybe A} {f : R₁ → List R₂} →
((x : R₁) → ∞⟨ m ⟩Parser Tok R₂ (f x)) → Maybe A
forced?′ {m = m} _ = m

-- Short synonyms for just and nothing. ◌ stands for "delayed" (think
-- "not here") and ○ for "not delayed".

◌ : {R : Set} → Maybe R
◌ = nothing

○ : {R : Set} {x : R} → Maybe R
○ {x = x} = just x
```