------------------------------------------------------------------------
-- 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.Effectful as ListMonad
  using () renaming (module MonadProperties to ListMonadProp)
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.Product using (proj₂)
open import Effect.Monad
open import Function
open import Level
open import Relation.Binary.PropositionalEquality

open RawMonadPlus {f = zero} ListMonad.monadPlus
  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  =
    sym $ ListMonadProp.right-zero (flatten mxs)

  bind-nothing : {A B : Set} (mxs : Maybe (List A)) →
                 bind mxs nothing ≡ [] {A = 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