Skip to content

Improve kernel parser exceptions

Viktor Kuncak requested to merge github/fork/cache-nez/positions into main

Created by: cache-nez

Most importantly, keep track of positions when parsing and report the error, highlighting the position where it occurred. Two types of errors are reported:

  • unexpected input: highlight the unexpected token and suggest expected kinds of input
  • expected term, got formula: highlight the unexpected formula

Since applications are eagerly converted to function or predicate application depending on the expected type, "expected formula, got term" error is currently not detected. This can be improved in the future.

Part of #86.

Merge request reports