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
  -- TODO: Rename this constructor
  MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
  BeforeParse : (message : String) -> ParseError
  NestedErrors : (state : ParserInternal Id) -> (message : String)
    -> (rest : List ParseError) -> ParseError

Type Alias

public export
Parser : Type -> Type
Parser a = Eff [ParserState, Except ParseError] 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 f

Provide wrappers for rundownFirst for evaluating it in various contexts.

export
runFirstIO : HasIO io => MonadRec io =>
  (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
runFirstIODebug : (f : Parser a) -> String -> IO (Either ParseError a)
runFirstIODebug f str = do
  Just state <- newInternalIO str
    | _ => pure . Left $ BeforeParse "Empty input"
  runEff (rundownFirst f) [handleParserStateIODebug 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)

Attempt to parse one of the given input parsers, in the provided order, invoking the provided error action on failure.

The state will not be modified when an input parser fails

export
oneOfE : (err : String) -> List (Parser a) -> Parser a
oneOfE err xs = do
  start <- save
  oneOfE' err start [] xs
  where
    oneOfE' : (err : String) -> (start : ParserInternal Id) 
      -> (errs : List ParseError) -> List (Parser a) -> Parser a
    oneOfE' err start errs [] = do
      throw $ NestedErrors start err (reverse errs) 
    oneOfE' err start errs (x :: xs) = do
      x <- tryEither x
      case x of
        Right val => pure val
        Left error => oneOfE' err start (error :: errs) xs

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

-- TODO: Rename these
export
liftString : Parser (List Char) -> Parser String
liftString x = do
  xs <- x
  pure $ pack xs

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

Attempt to parse a specified character

export
charExact : Char -> Parser Char
charExact c = do
  result <- charExact' c
  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
theseChars : List Char -> Parser Char
theseChars cs = do
  pnote "Parsing one of: \{show cs}"
  result <- charPredicate (\x => any (== x) cs)
  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

export
exactString : String -> Parser String
exactString str with (asList str)
  exactString "" | [] = do
    pnote "Parsing the empty string"
    pure ""
  exactString input@(strCons c str) | (c :: x) = do
    pnote "Parsing exact string \{show input}"
    GotChar next <- charPredicate (== c)
      | GotError err => throwParseError "Got \{show err} expected \{show c}"
      | EndOfInput => throwParseError "End of input"
    rest <- exactString str | x
    pure input

Wrap a parser in delimiter characters, discarding the value of the delimiters

export
delimited : (before, after : Char) -> Parser a -> Parser a
delimited before after x = do
  pnote "Parsing delimited by \{show before} \{show after}"
  starting_state <- save
  _ <- charExact before
  Right val <- tryEither x
    | Left err => do
      load starting_state
      throw err
  Just _ <- tryMaybe $ charExact after
    | _ => do
      load starting_state
      throw $ MkParseError starting_state "Unmatched delimiter \{show before}"
  pure val

Consume any number of characters of the provided character class and discard the result. Also a version for doing so on both sides of a provided parser

export
nom : Parser Char -> Parser ()
nom x = do
  pnote "Nomming"
  _ <- many x
  pure ()

export
surround : (around : Parser Char) -> (item : Parser a) -> Parser a
surround around item = do
  pnote "Surrounding"
  nom around
  val <- item
  nom around
  pure val

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