diff --git a/lisa-utils/src/main/scala/lisa/utils/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala index eb7324260b417a8f9e7e66301941dffa30c121b0..75c5837e7a10d245c93742811c7d1378c0af93f5 100644 --- a/lisa-utils/src/main/scala/lisa/utils/Printer.scala +++ b/lisa-utils/src/main/scala/lisa/utils/Printer.scala @@ -97,10 +97,10 @@ object Printer { def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) = ( - showErrorForLine, - prefixString, - Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "), - prettySequent(imp) + showErrorForLine, + prefixString, + Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "), + prettySequent(imp) ) Seq(pretty("Import", 0)) @@ -116,10 +116,10 @@ object Printer { def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) = ( - showErrorForLine, - prefixString, - Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "), - prettySequent(step.bot) + showErrorForLine, + prefixString, + Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "), + prettySequent(step.bot) ) step match { @@ -168,12 +168,12 @@ object Printer { val lines = prettySCProofRecursive(proof, 0, IndexedSeq.empty, IndexedSeq.empty) val maxStepNameLength = lines.map { case (_, _, stepName, _) => stepName.length }.maxOption.getOrElse(0) lines - .map { case (isMarked, indices, stepName, sequent) => - val suffix = Seq(indices, rightPadSpaces(stepName, maxStepNameLength), sequent) - val full = if (!judgement.isValid) (if (isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix - full.mkString(" ") - } - .mkString("\n") + (judgement match { + .map { case (isMarked, indices, stepName, sequent) => + val suffix = Seq(indices, rightPadSpaces(stepName, maxStepNameLength), sequent) + val full = if (!judgement.isValid) (if (isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix + full.mkString(" ") + } + .mkString("\n") + (judgement match { case SCValidProof(_) => "" case SCInvalidProof(proof, path, message) => s"\nProof checker has reported an error at line ${path.mkString(".")}: $message" }) diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala index 0d33b06630f5c07fbe1c2af097bde2b266d07662..e8c2a63c90a58f899a4306ff19a9a69046386a8b 100644 --- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala +++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala @@ -209,7 +209,7 @@ class PrinterTest extends AnyFunSuite with TestUtils { val existsYEq = BinderFormula(Exists, y, PredicateFormula(equality, Seq(y, y))) assert( Parser.printSequent(Sequent(Set(forallEq), Set(existsYEq, existsXEq))) == "∀ ?x. ?x = ?x ⊢ ∃ ?y. ?y = ?y; " + - "∃ ?x. ?x = ?x" + "∃ ?x. ?x = ?x" ) assert( Parser.printSequent(Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))) == "∀ ?x. ?x = ?x; p ⊢ ∃ ?y. ?y = ?y; ∃ ?x. ?x = ?x"