{-# OPTIONS --without-K --safe #-}

open import Text.Parser.Types.Core using (Parameters)

module Text.Parser.Types {l} (P : Parameters l) where

open import Level.Bounded
open import Data.Nat.Base using (; _<_; _≤_)
open import Function.Base using (_∘′_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

open Text.Parser.Types.Core using (Success)

--------------------------------------------------------------------------------
-- PARSER

-- A parser is the ability to, given an input, return a computation for
-- a success.

record Parser (A : Set≤ l) (n : ) : Set l where
  constructor mkParser
  open Parameters P
  field runParser :  {m}  .(m  n)  Lift (Toks m)  M (Success Toks A m)
open Parser public