From 86649814a8b7a92638cfaaf8e84669b90425a32c Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Mon, 3 Oct 2022 18:45:34 +0200
Subject: [PATCH] Improve error reporting when parsing or printing fails
* When an unexpected token is encountered, add the string representation of the token
to the exception
* When printing of a sequent / formula / term fails, try to identify the smallest structure
on which the printing fails by attempting to print all subformulas and subterms. Report that
printing failed on the smallest structure rather than on the whole sequent / formula / term.
---
.../src/main/scala/lisa/utils/Parser.scala | 37 +++++++++++++++----
1 file changed, 30 insertions(+), 7 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index ffea1440..96d67b7f 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -27,16 +27,39 @@ object Parser {
private def extractParseResult[T](r: SequentParser.ParseResult[T]): T = r match {
case SequentParser.Parsed(value, _) => value
// TODO: at position
- // TODO: leaking implementation? Should I sugar tokens? -- Lexer.unapply once it's implemented
- case SequentParser.UnexpectedToken(token, _) => throw ParserException(s"Unexpected input: $token")
+ case SequentParser.UnexpectedToken(token, _) => throw ParserException(s"Unexpected input: ${SequentLexer.unapply(Iterator(token))}")
case SequentParser.UnexpectedEnd(_) => throw ParserException(s"Unexpected end of input")
}
- def printSequent(s: Sequent): String = SequentParser.printSequent(s).getOrElse(throw PrintFailedException(s))
-
- def printFormula(f: Formula): String = SequentParser.printFormula(f).getOrElse(throw PrintFailedException(f))
-
- def printTerm(t: Term): String = SequentParser.printTerm(t).getOrElse(throw PrintFailedException(t))
+ def printSequent(s: Sequent): String = SequentParser
+ .printSequent(s)
+ .getOrElse({
+ // attempt to print individual formulas. It might throw a more detailed PrintFailedException
+ s.left.foreach(printFormula)
+ s.right.foreach(printFormula)
+ throw PrintFailedException(s)
+ })
+
+ def printFormula(f: Formula): String = SequentParser
+ .printFormula(f)
+ .getOrElse({
+ f match {
+ case PredicateFormula(_, args) => args.foreach(printTerm)
+ case ConnectorFormula(_, args) => args.foreach(printFormula)
+ case BinderFormula(_, _, inner) => printFormula(inner)
+ }
+ throw PrintFailedException(f)
+ })
+
+ def printTerm(t: Term): String = SequentParser
+ .printTerm(t)
+ .getOrElse({
+ t match {
+ case FunctionTerm(_, args) => args.foreach(printTerm)
+ case VariableTerm(_) => ()
+ }
+ throw PrintFailedException(t)
+ })
private[Parser] object SequentLexer extends Lexers with CharLexers {
sealed abstract class FormulaToken(stringRepr: String) {
--
GitLab