From f0f03b694d34b22106616a01aa00d1c376d9ef7e Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Tue, 4 Oct 2022 00:07:18 +0200
Subject: [PATCH] scalafix.
---
.../src/main/scala/lisa/utils/Printer.scala | 28 +++++++++----------
.../test/scala/lisa/utils/PrinterTest.scala | 2 +-
2 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
index eb732426..75c5837e 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 0d33b066..e8c2a63c 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"
--
GitLab