Introduce the proof judgement ADT

src/main/scala/lisa/kernel/Printer.scala

 package lisa.kernel
 
 import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus._
-import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SCProofCheckerJudgement.*
+import lisa.kernel.proof.{SCProof, SCProofCheckerJudgement}
 
 /**
  * A set of methods to pretty-print kernel trees.
@@ -182,10 +183,11 @@ object Printer {
     /**
      * Returns a string representation of this proof.
      * @param proof the proof
-     * @param showError if set, marks that particular step in the proof (`->`) as an error
+     * @param judgement optionally provide a proof checking judgement that will mark a particular step in the proof
+     *                  (`->`) 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, showError: Option[(Seq[Int], String)] = None): String = {
+    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))
@@ -205,7 +207,10 @@ object Printer {
         def prettySCProofRecursive(proof: SCProof, level: Int, tree: IndexedSeq[Int], topMostIndices: IndexedSeq[Int]): Seq[(Boolean, String, String, String)] = {
             val printedImports = proof.imports.zipWithIndex.reverse.flatMap { case (imp, i) =>
                 val currentTree = tree :+ (-i-1)
-                val showErrorForLine = showError.exists((position, reason) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0))
+                val showErrorForLine = judgement match {
+                    case SCValidProof => false
+                    case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
+                }
                 val prefix = (Seq.fill(level - topMostIndices.size)(None) ++  Seq.fill(topMostIndices.size)(None) :+ Some(-i-1)) ++ Seq.fill(maxLevel - level)(None)
                 val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
                 def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
@@ -220,7 +225,10 @@ object Printer {
             }
             printedImports ++ proof.steps.zipWithIndex.flatMap { case (step, i) =>
                 val currentTree = tree :+ i
-                val showErrorForLine = showError.exists((position, reason) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0))
+                val showErrorForLine = judgement match {
+                    case SCValidProof => false
+                    case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
+                }
                 val prefix = (Seq.fill(level - topMostIndices.size)(None) ++  Seq.fill(topMostIndices.size)(None) :+ Some(i)) ++ Seq.fill(maxLevel - level)(None)
                 val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
                 def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
@@ -276,9 +284,12 @@ object Printer {
         lines.map {
             case (isMarked, indices, stepName, sequent) =>
                 val suffix = Seq(indices, rightPadSpaces(stepName, maxStepNameLength), sequent)
-                val full = if(showError.nonEmpty) (if(isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix
+                val full = if(!judgement.isValid) (if(isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix
                 full.mkString(" ")
-        }.mkString("\n") + (if (showError.nonEmpty) s"\nProof checker has reported error at line ${showError.get._1}: ${showError.get._2}" else "")
+        }.mkString("\n") + (judgement match {
+            case SCValidProof => ""
+            case SCInvalidProof(path, message) => s"\nProof checker has reported error at line ${path.mkString(".")}: $message"
+        })
     }
 
 }

src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala

+package lisa.kernel.proof
+
+/**
+ * The judgement (or verdict) of a proof checking procedure.
+ * Typically, see [[SCProofChecker.checkSingleSCStep]] and [[SCProofChecker.checkSCProof]].
+ */
+sealed abstract class SCProofCheckerJudgement {
+    import SCProofCheckerJudgement.*
+
+    /**
+     * Whether this judgement is positive -- the proof is concluded to be valid;
+     * or negative -- the proof checker couldn't certify the validity of this proof.
+     * @return An instance of either [[SCValidProof]] or [[SCInvalidProof]]
+     */
+    def isValid: Boolean = this match {
+        case SCValidProof => true
+        case _: SCInvalidProof => false
+    }
+}
+
+object SCProofCheckerJudgement {
+    /**
+     * A positive judgement.
+     */
+    case object SCValidProof extends SCProofCheckerJudgement
+
+    /**
+     * A negative judgement.
+     * @param path The path of the error, expressed as indices
+     * @param message The error message that hints about the first error encountered
+     */
+    case class SCInvalidProof(path: Seq[Int], message: String) extends SCProofCheckerJudgement
+}

src/test/scala/lisa/kernel/ProofTests.scala

@@ -31,14 +31,14 @@ class ProofTests  extends AnyFunSuite {
     val s3 = LeftImplies((a ==> b) ==> a |- a, 2, 0, a ==> b, a)
     val s4 = RightImplies(() |- (a ==> b) ==> a ==> a, 3, (a ==> b) ==> a, a)
     val ppl: SCProof = SCProof(IndexedSeq(s0, s1, s2, s3, s4))
-    assert(predicateVerifier(ppl)._1)
+    assert(predicateVerifier(ppl).isValid)
   }
 
   test("Verification of substitution") {
     val t0 = Hypothesis(fp(x)|-fp(x), fp(x))
     val t1 = RightSubstEq(Set(fp(x), x === y) |- fp(y), 0, x, y, fp(sT()), sT)
     val pr = new SCProof(IndexedSeq(t0, t1))
-    assert(predicateVerifier(pr)._1)
+    assert(predicateVerifier(pr).isValid)
   }
 
   test("Commutativity on a random large formula") {
@@ -58,6 +58,6 @@ class ProofTests  extends AnyFunSuite {
     val orig = subformulas.next().head
     val swapped = subformulasSwapped.next().head
     val prf = SCProof(Vector(Hypothesis(Sequent(Set(orig), Set(orig)), orig), Rewrite(Sequent(Set(orig), Set(swapped)), 0)))
-    assert(predicateVerifier(prf)._1)
+    assert(predicateVerifier(prf).isValid)
   }
 }

src/test/scala/lisa/proven/SimpleProverTests.scala

@@ -13,7 +13,7 @@ import proven.tactics.SimplePropositionalSolver as SPS
 
 
 class SimpleProverTests extends AnyFunSuite {
-    
+
     test("Simple propositional logic proofs") {
         val problems = getPRPproblems.take(1)
 
@@ -24,7 +24,7 @@ class SimpleProverTests extends AnyFunSuite {
             val proof = SPS.solveSequent(sq)
             if (!Seq("Unsatisfiable", "Theorem", "Satisfiable").contains(pr.status)) println("Unknown status: "+pr.status+", "+pr.file)
 
-            assert(SCProofChecker.checkSCProof(proof)._1 == (pr.status =="Unsatisfiable" || pr.status == "Theorem"))
+            assert(SCProofChecker.checkSCProof(proof).isValid == (pr.status =="Unsatisfiable" || pr.status == "Theorem"))
 
         })
 

src/test/scala/test/ProofCheckerSuite.scala

@@ -26,12 +26,12 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
   }
 
   def checkProof(proof: SCProof, expected: Sequent): Unit = {
-    val error = checkSCProof(proof)
-    assert(error._1, "\n"+Printer.prettySCProof(proof, error))
+    val judgement = checkSCProof(proof)
+    assert(judgement.isValid, "\n"+Printer.prettySCProof(proof, judgement))
     assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
   }
 
   def checkIncorrectProof(incorrectProof: SCProof): Unit = {
-    assert(!checkSCProof(incorrectProof)._1, s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}")
+    assert(!checkSCProof(incorrectProof).isValid, s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}")
   }
 }