From 850ff7e6287407b2328fc1f5d54bc6d80828d645 Mon Sep 17 00:00:00 2001
From: Florian Cassayre <florian.cassayre@gmail.com>
Date: Tue, 1 Mar 2022 11:42:16 +0100
Subject: [PATCH] Fix the indenting of imports in the printer
---
src/main/scala/lisa/kernel/Printer.scala | 31 ++++++++++++++++--------
1 file changed, 21 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index cd8c20e2..9123f72b 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -180,6 +180,17 @@ object Printer {
Seq(prettyFormulas(sequent.left), "⊢", prettyFormulas(sequent.right)).filter(_.nonEmpty).mkString(spaceSeparator(compact))
}
+ /**
+ * Returns a string representation of the line number in a proof.
+ * Example output:
+ * <pre>
+ * 0:2:1
+ * </pre>
+ * @param line the line number
+ * @return the string representation of this line number
+ */
+ def prettyLineNumber(line: Seq[Int]): String = line.mkString(":")
+
/**
* Returns a string representation of this proof.
* @param proof the proof
@@ -187,14 +198,13 @@ object Printer {
* (`->`) as an error. The proof is considered to be valid by default
* @return a string where each indented line corresponds to a step in the proof
*/
- def prettySCProof(proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof): String = {
- def computeMaxNumbering(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
- val resultWithCurrent = result.updated(level, Math.max(proof.steps.size - 1, result(level)))
- proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumbering(sp.sp, level + 1, if(acc.size <= level + 1) acc :+ 0 else acc))
+ def prettySCProof(proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof, forceDisplaySubproofs: Boolean = false): String = {
+ def computeMaxNumberingLengths(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
+ val resultWithCurrent = result.updated(level, (Seq((proof.steps.size - 1).toString.length, result(level)) ++ (if(proof.imports.nonEmpty) Seq((-proof.imports.size).toString.length) else Seq.empty)).max)
+ proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumberingLengths(sp.sp, level + 1, if(acc.size <= level + 1) acc :+ 0 else acc))
}
- val maxNumbering = computeMaxNumbering(proof, 0, IndexedSeq(0)) // The maximum value for each number column
- val maxNumberingLengths = maxNumbering.map(_.toString.length)
- val maxLevel = maxNumbering.size - 1
+ val maxNumberingLengths = computeMaxNumberingLengths(proof, 0, IndexedSeq(0)) // The maximum value for each number column
+ val maxLevel = maxNumberingLengths.size - 1
def leftPadSpaces(v: Any, n: Int): String = {
val s = String.valueOf(v)
@@ -239,7 +249,8 @@ object Printer {
prettySequent(step.bot)
)
step match {
- case sp @ SCSubproof(_, _, true) => pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if(i == 0) topMostIndices else IndexedSeq.empty) :+ i)
+ case sp @ SCSubproof(_, _, display) if display || forceDisplaySubproofs =>
+ pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if(i == 0) topMostIndices else IndexedSeq.empty) :+ i)
case other =>
val line = other match {
case Rewrite(_, t1) => pretty("Rewrite", t1)
@@ -268,7 +279,7 @@ object Printer {
case RightSubstIff(_, t1, _, _, _, _) => pretty("R. SubstIff", t1)
case InstFunSchema(_, t1, _, _, _) => pretty("?Fun Instantiation", t1)
case InstPredSchema(_, t1, _, _, _) => pretty("?Pred Instantiation", t1)
- case SCSubproof(_, _, false) => pretty("SCSubproof (hidden)")
+ case SCSubproof(_, _, false) => pretty("Subproof (hidden)")
case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
}
Seq(line)
@@ -288,7 +299,7 @@ object Printer {
full.mkString(" ")
}.mkString("\n") + (judgement match {
case SCValidProof => ""
- case SCInvalidProof(path, message) => s"\nProof checker has reported error at line ${path.mkString(".")}: $message"
+ case SCInvalidProof(path, message) => s"\nProof checker has reported an error at line ${path.mkString(".")}: $message"
})
}
--
GitLab