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

module TotalParserCombinators.Parser where

open import Algebra
open import Category.Monad
open import Coinduction
open import Data.List as List
open import Data.Maybe
import Data.List.Any as Any
import Data.List.Properties as ListProp
open import Data.Product using (proj₂)
open import Function
open import Relation.Binary.PropositionalEquality

open Any.Membership-≡
open RawMonadPlus List.monadPlus
  using ()
  renaming ( return 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 $ ListProp.Monad.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  =
    sym $ ListProp.Monad.right-zero (flatten mxs)

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

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

infixl  _⊛_ _<$>_ _⊛flatten_
infixl  _>>=_
infixl   _∣_

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