The interface of a `Parser`

module Parser.Interface
  
import public Data.List1

import public Parser.ParserState

import public Control.Eff

export infixr 4 >|
export infixr 5 >&

Parser Errors

Combine the parser state at time of error with an error message.

public export
data ParseError : Type where
  MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
  BeforeParse : (message : String) -> ParseError

Type Alias

public export
Parser : Type -> Type
Parser a = Eff [ParserState, Except ParseError, Choose] a

Error Generation

Provide a few effectful actions to generate an error from an error message, and either return it or throw it.

export
parseError : Has ParserState fs => (message : String) -> Eff fs ParseError
parseError message = do
  state <- save
  pure $ MkParseError state message

export
throwParseError : Has ParserState fs => Has (Except ParseError) fs =>
  (message : String) -> Eff fs a
throwParseError message = do
  err <- parseError message
  throw err

export
guardMaybe : Has ParserState fs => Has (Except ParseError) fs =>
  (message : String) -> Eff fs (Maybe a) -> Eff fs a
guardMaybe message x = do
  Just x <- x
    | _ => throwParseError message
  pure x

export
replaceError : (message : String) -> Parser (a -> Parser b)
replaceError message = do
  state <- save
  pure (\_ => throw $ MkParseError state message)

Running a parser

We will use the phrasing "rundown" to refer to running all the effects in the parser effect stack except ParserState, which is left in the effect stack to facilitate handling in the context of another monad or effect stack, since it benefits from mutability.

Rundown a parser, accepting the first returning parse, which may be failing or succeding, and automatically generating a "no valid parses" message in the event no paths in the Choice effect produce a returning parse.

export
rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a)
rundownFirst f = 
  runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f

Provide wrappers for rundownFirst for evaluating it in various contexts.

export
runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a)
runFirstIO f str = do
  Just state <- newInternalIO str
    | _ => pure . Left $ BeforeParse "Empty input"
  runEff (rundownFirst f) [handleParserStateIO state]

export
runFirst : (f : Parser a) -> String -> Eff fs (Either ParseError a)
runFirst f str = do
  Just state <- pure $ newInternal str
    | _ => pure . Left $ BeforeParse "Empty input"
  (result, _) <- lift . runParserState state . rundownFirst $ f
  pure result

export
runFirst' : (f : Parser a) -> String -> Either ParseError a
runFirst' f str = extract $ runFirst f str {fs = []}

Utility functionality

Parser combinators

Try to run a computation in the context of the Parser effect stack, if it fails (via Except), reset the state and resort to the supplied callback

Also supply a version specialized to ignore the error value, returning Just a if the parse succeeds, and Nothing if it fails.

export
try : (f : Parser a) -> (err : ParseError -> Parser a) -> Parser a
try f err = do
  starting_state <- save
  result <- lift . runExcept $ f
  case result of
    Left error => do
      load starting_state
      err error 
    Right result => pure result

export
tryMaybe : (f : Parser a) -> Parser (Maybe a)
tryMaybe f = try (map Just f) (\_ => pure Nothing)
  
export
tryEither : (f : Parser a) -> Parser (Either ParseError a)
tryEither f = try (map Right f) (pure . Left)

||| Converts any errors thrown by `f` into silent backtracking within `Choose`
export
tryEmpty : (f : Parser a) -> Parser a
tryEmpty f = try f (\_ => empty)

Attempt to parse one of the given input parsers, in the provided order, invoking the provided error action on failure. This will suppress any errors returned by the input parsers by mapping them to empty.

The state will not be modified when an input parser fails

export
oneOfE : Foldable f =>
  (err : Parser a) -> f (Parser a) -> Parser a
oneOfE err xs = foldr altE err xs
  where
    altE : Parser a -> Parser a -> Parser a
    altE f rest = (tryEmpty f) `alt` rest

Attempt to parse 0+ of an item

export
many : (f : Parser a) -> Parser (List a)
many f = do
  Just next <- tryMaybe f
    | _ => pure []
  map (next ::) $ many f

Attempt to parse 1+ of an item, invoking the supplied error action on failure

export
atLeastOne : (err : ParseError -> Parser (List1 a)) -> (f : Parser a)
  -> Parser (List1 a)
atLeastOne err f = do
  Right next <- tryEither f
    | Left e => err e
  map (next :::) $ many f

Lift a parser producing a List or List1 of Char into a parser producing a String

export
parseString : Parser (List Char) -> Parser String
parseString x = do
  xs <- x
  pure $ pack xs

export
parseString' : Parser (List1 Char) -> Parser String
parseString' x = parseString $ map forget x

Attempt to parse a specified character

export
parseExactChar : Char -> Parser Char
parseExactChar c = do
  result <- parseChar (== c) id
  case result of
    GotChar char => pure char
    GotError err => throwParseError "Got \{show err} Expected \{show c}"
    EndOfInput => throwParseError "End of input"

Attempt to parse one of a list of chars

export
parseTheseChars : List Char -> Parser Char
parseTheseChars cs = do
  result <- parseChar (\x => any (== x) cs) id
  case result of
    GotChar char => pure char
    GotError err => throwParseError "Got \{show err} Expected one of \{show cs}"
    EndOfInput => throwParseError "End of input"

Attempt to parse an exact string

exactString : String -> Parser String
exactString str with (asList str)
  exactString "" | [] = pure ""
  exactString input@(strCons c str) | (c :: x) = do
    GotChar next <- parseChar (== c) id
      | GotError err => throwParseError "Got \{show err} expected \{show c}"
      | EndOfInput => throwParseError "End of input"
    rest <- exactString str | x
    pure input

Composition of boolean functions

||| Return true if both of the predicates evaluate to true
public export
(>&) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool)
(>&) a b x = a x && b x

||| Return true if either of the predicates evaulates to true
public export
(>|) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool)
(>|) a b x = a x || b x

6.8 KiB Raw Blame History

The interface of a Parser