Parser Errors

Error handling for parsing is done purely within IO. Errors are thrown as exceptions, which are then captured by the TCM monad. This has two drawbacks:

  • There is coupling between the part of the code where the errors are thrown (which are of type ParseError`), and the part of the code where the errors are captured (where only exceptions of type ParseError` are caught). This coupling is however not reflected on the types.
  • All errors produced during parsing are necessarily fatal. That is, it is not possible to produce warnings and then carry-on typechecking.

Proposed solution:

  • Create a Parser monad (let's call it ParserM, of type ParserM a = ExceptT ParserError (WriterT [ParserWarning] a)
    • Note the ordering of transformers: we want to recover the warnings, even if we also get an error.
  • Write a function liftParse :: ParserM a -> TCM a, that:
    1. Outputs the warnings resulting from parsing (if any).
    2. Fails with an error if the parsing resulted in a ParseError (i.e. no 'a' was returned).

Use case:

At the moment, the only use case for this are comments spanning multiple code blocks in a literate file. This is an error right now, but it does not have to be. The only situation where this causes problems is when rendering a literate file using the LaTeX or the HTML back-end. In this case, the comment token will be rendered separately from the literate text it overlaps.