diff --git a/src/main/scala/lisa/KernelHelpers.scala b/src/main/scala/lisa/KernelHelpers.scala
index afa8008b772cbc7fbacf9675770866a6caf86995..1541d31ab35712cdfc4ce11125accf0a6073d702 100644
--- a/src/main/scala/lisa/KernelHelpers.scala
+++ b/src/main/scala/lisa/KernelHelpers.scala
@@ -1,12 +1,19 @@
package lisa
-
+/**
+ * A helper file that provides various syntactic sugars for LISA.
+ * Usage:
+ * <pre>
+ * import lisa.KernelHelpers.*
+ * </pre>
+ */
object KernelHelpers {
import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.fol.FOL.*
- // Prefix
+ /* Prefix syntax */
+
def neg(f: Formula): Formula = ConnectorFormula(Neg, Seq(f))
def and(l: Formula, r: Formula): Formula = ConnectorFormula(And, Seq(l, r))
def or(l: Formula, r: Formula): Formula = ConnectorFormula(Or, Seq(l, r))
@@ -29,7 +36,8 @@ object KernelHelpers {
extension (label: BinderLabel)
def apply(bound: VariableLabel, inner: Formula): Formula = BinderFormula(label, bound, inner)
- // Infix
+ /* Infix syntax */
+
extension (f: Formula) {
def unary_! : Formula = neg(f)
infix def ==>(g: Formula): Formula = implies(f, g)
@@ -41,30 +49,50 @@ object KernelHelpers {
extension (t: Term)
infix def ===(u: Term): Formula = PredicateFormula(equality, Seq(t, u))
- // Other
+ /* Pattern matching extractors */
+
+ object ! {
+ def unapply(f: Formula): Option[Formula] = f match {
+ case ConnectorFormula(`Neg`, Seq(g)) => Some(g)
+ case _ => None
+ }
+ }
+
+ sealed abstract class UnapplyBinaryConnector(label: ConnectorLabel) {
+ def unapply(f: Formula): Option[(Formula, Formula)] = f match {
+ case ConnectorFormula(`label`, Seq(a, b)) => Some((a, b))
+ case _ => None
+ }
+ }
+ object ==> extends UnapplyBinaryConnector(Implies)
+ object <=> extends UnapplyBinaryConnector(Iff)
+ object /\ extends UnapplyBinaryConnector(And)
+ object \/ extends UnapplyBinaryConnector(Or)
+
+ sealed abstract class UnapplyBinaryPredicate(label: PredicateLabel) {
+ def unapply(f: Formula): Option[(Term, Term)] = f match {
+ case PredicateFormula(`label`, Seq(a, b)) => Some((a, b))
+ case _ => None
+ }
+ }
+ object === extends UnapplyBinaryPredicate(equality)
+
+ /* Conversions */
+
given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply
given Conversion[VariableTerm, VariableLabel] = _.label
- val emptySeq = Sequent(Set.empty, Set.empty)
-
- extension (l: Unit)
- infix def |-(r: Iterable[Formula]): Sequent = Sequent(Set.empty, r.toSet)
- infix def |-(r: Formula): Sequent = Sequent(Set.empty, Set(r))
- infix def |-(r: Unit): Sequent = emptySeq
- extension (l: Iterable[Formula])
- infix def |-(r: Iterable[Formula]): Sequent = Sequent(l.toSet, r.toSet)
- infix def |-(r: Formula): Sequent = Sequent(l.toSet, Set(r))
- infix def |-(r: Unit): Sequent = Sequent(l.toSet, Set.empty)
- extension (l: Formula)
- infix def |-(r: Iterable[Formula]): Sequent = Sequent(Set(l), r.toSet)
- infix def |-(r: Formula): Sequent = Sequent(Set(l), Set(r))
- infix def |-(r: Unit): Sequent = Sequent(Set(l), Set.empty)
+ given Conversion[PredicateFormula, PredicateLabel] = _.label
+
+ given Conversion[FunctionTerm, FunctionLabel] = _.label
// given Conversion[Tuple, List[Union[_.type]]] = _.toList
given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3)
+ /* Sequents */
+ val emptySeq: Sequent = Sequent(Set.empty, Set.empty)
extension (s: Sequent) {
infix def +<(f: Formula): Sequent = s.copy(left = s.left + f)
@@ -78,4 +106,34 @@ object KernelHelpers {
infix def ++(s1: Sequent): Sequent = s.copy(left = s.left ++ s1.left, right = s.right ++ s1.right)
infix def --(s1: Sequent): Sequent = s.copy(left = s.left -- s1.left, right = s.right -- s1.right)
}
+
+ /**
+ * Represents a converter of some object into a set.
+ * @tparam S The type of elements in that set
+ * @tparam T The type to convert from
+ */
+ protected trait SetConverter[S, T] {
+ def apply(t: T): Set[S]
+ }
+
+ given [S]: SetConverter[S, Unit] with
+ override def apply(u: Unit): Set[S] = Set.empty
+
+ given [S]: SetConverter[S, EmptyTuple] with
+ override def apply(t: EmptyTuple): Set[S] = Set.empty
+
+ given [S, H <: S, T <: Tuple, C1](using SetConverter[S, T]): SetConverter[S, H *: T] with
+ override def apply(t: H *: T): Set[S] = summon[SetConverter[S, T]].apply(t.tail) + t.head
+
+ given [S, T <: S]: SetConverter[S, T] with
+ override def apply(f: T): Set[S] = Set(f)
+
+ given [S, I <: Iterable[S]]: SetConverter[S, I] with
+ override def apply(s: I): Set[S] = s.toSet
+
+ private def any2set[S, A, T <: A](any: T)(using SetConverter[S, T]): Set[S] = summon[SetConverter[S, T]].apply(any)
+
+ extension [A, T1 <: A](left: T1)(using SetConverter[Formula, T1])
+ infix def |-[B, T2 <: B](right: T2)(using SetConverter[Formula, T2]): Sequent = Sequent(any2set(left), any2set(right))
+
}
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 6f27c597e980e9b2eaa4b6ba79ea9c7e6f5aaa12..35fb39c1141d25b063e25c0ea833d34734482735 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -1,8 +1,9 @@
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.
@@ -55,7 +56,12 @@ object Printer {
case Seq(l, r) => prettyInfix("~", prettyTerm(l), prettyTerm(r), compact)
case _ => throw new Exception
}
- case _ => prettyFunction(label.id, args.map(prettyTerm(_, compact)), compact)
+ case _ =>
+ val labelString = label match {
+ case ConstantPredicateLabel(id, _) => id
+ case SchematicPredicateLabel(id, _) => s"?$id"
+ }
+ prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
}
case ConnectorFormula(label, args) =>
(label, args) match {
@@ -160,7 +166,12 @@ object Printer {
case Seq(s) => prettyFunction("U", Seq(prettyTerm(s)), compact)
case _ => throw new Exception
}
- case _ => prettyFunction(label.id, args.map(prettyTerm(_, compact)), compact)
+ case _ =>
+ val labelString = label match {
+ case ConstantFunctionLabel(id, _) => id
+ case SchematicFunctionLabel(id, _) => s"?$id"
+ }
+ prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
}
}
@@ -179,20 +190,31 @@ 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
- * @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 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)
@@ -205,7 +227,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 +245,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) =
@@ -231,7 +259,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)
@@ -260,7 +289,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)
@@ -276,9 +305,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 an error at line ${path.mkString(".")}: $message"
+ })
}
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 11fd361ef0fb440dbc07828fa64b5fdc4f7422b2..6602e1cea1c6768b219ec0b6cf68a32d14a9a842 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -3,6 +3,7 @@ package lisa.kernel.proof
import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SCProofCheckerJudgement.*
object SCProofChecker {
@@ -21,16 +22,16 @@ object SCProofChecker {
* a proof's [[SCProof.getSequent]] function.
* @return
*/
- def checkSingleSCStep(no:Int, step: SCProofStep, references : Int => Sequent, importsSize: Option[Int]=None):(Boolean, List[Int], String) = {
+ def checkSingleSCStep(no:Int, step: SCProofStep, references : Int => Sequent, importsSize: Option[Int]=None): SCProofCheckerJudgement = {
val ref = references
val false_premise = step.premises.find(i => i >= no)
val false_premise2 = if (importsSize.nonEmpty) step.premises.find(i => i< -importsSize.get) else None
- val r: (Boolean, List[Int], String) =
+ val r: SCProofCheckerJudgement =
if (false_premise.nonEmpty)
- return (false, Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
- if (false_premise2.nonEmpty)
- return (false, Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
+ SCInvalidProof(Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
+ else if (false_premise2.nonEmpty)
+ SCInvalidProof(Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
else step match {
/*
* Γ |- Δ
@@ -38,7 +39,7 @@ object SCProofChecker {
* Γ |- Δ
*/
case Rewrite(s, t1) =>
- if (isSameSequent(s, ref(t1))) (true, Nil, "") else (false, Nil, s"The premise and the conclusion are not trivially equivalent.")
+ if (isSameSequent(s, ref(t1))) SCValidProof else SCInvalidProof(Nil, s"The premise and the conclusion are not trivially equivalent.")
/*
*
* --------------
@@ -46,10 +47,10 @@ object SCProofChecker {
*/
case Hypothesis(Sequent(left, right), phi) =>
if (contains(left, phi))
- if (contains(right, phi)) (true, Nil, "")
+ if (contains(right, phi)) SCValidProof
- else (false, Nil, s"Right-hand side does not contain formula φ")
- else (false, Nil, s"Left-hand side does not contain formula φ")
+ else SCInvalidProof(Nil, s"Right-hand side does not contain formula φ")
+ else SCInvalidProof(Nil, s"Left-hand side does not contain formula φ")
/*
* Γ |- Δ, φ φ, Σ |- Π
* ------------------------
@@ -60,11 +61,11 @@ object SCProofChecker {
if (isSameSet(b.right + phi, ref(t2).right union ref(t1).right))
if (contains(ref(t2).left, phi))
if (contains(ref(t1).right, phi))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of first premise does not contain φ as claimed.")
- else (false, Nil, s"Left-hand side of second premise does not contain φ as claimed.")
- else (false, Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
- else (false, Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of first premise does not contain φ as claimed.")
+ else SCInvalidProof(Nil, s"Left-hand side of second premise does not contain φ as claimed.")
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
// Left rules
/*
@@ -78,9 +79,9 @@ object SCProofChecker {
if (isSameSet(b.left + phi, ref(t1).left + phiAndPsi) ||
isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
- else (false, Nil, "Right-hand sides of the premise and the conclusion must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- Δ Σ, ψ |- Π
* ------------------------
@@ -90,9 +91,9 @@ object SCProofChecker {
if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)) )
val phiOrPsi = ConnectorFormula(Or, disjuncts)
if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
- (true, Nil, "")
- else (false, Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
- else (false, Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
/*
* Γ |- φ, Δ Σ, ψ |- Π
* ------------------------
@@ -102,9 +103,9 @@ object SCProofChecker {
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(b.right + phi, ref(t1).right union ref(t2).right))
if (isSameSet(b.left + psi, ref(t1).left union ref(t2).left + phiImpPsi))
- (true, Nil, "")
- else (false, Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
- else (false, Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
/*
* Γ, φ→ψ |- Δ Γ, φ→ψ, ψ→φ |- Δ
* -------------- or ---------------
@@ -118,9 +119,9 @@ object SCProofChecker {
if (isSameSet(b.left + phiImpPsi , ref(t1).left + phiIffPsi) ||
isSameSet(b.left + psiImpPhi , ref(t1).left + phiIffPsi) ||
isSameSet(b.left + phiImpPsi + psiImpPhi , ref(t1).left + phiIffPsi))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
- else (false, Nil, "Right-hand sides of premise and conclusion must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
+ else SCInvalidProof(Nil, "Right-hand sides of premise and conclusion must be the same.")
/*
* Γ |- φ, Δ
@@ -131,9 +132,9 @@ object SCProofChecker {
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.left, ref(t1).left + nPhi))
if (isSameSet(b.right + phi, ref(t1).right))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
- else (false, Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
+ else SCInvalidProof(Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
/*
* Γ, φ[t/x] |- Δ
@@ -143,9 +144,9 @@ object SCProofChecker {
case LeftForall(b, t1, phi, x, t) =>
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + substituteVariable(phi, x, t), ref(t1).left + BinderFormula(Forall, x, phi)))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
/*
* Γ, φ |- Δ
@@ -156,10 +157,10 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left + BinderFormula(Exists, x, phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
- (true, Nil, "")
- else (false, Nil, "The variable x must not be free in the resulting sequent.")
- else (false, Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof
+ else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
/*
* Γ, ∃y.∀x. (x=y) ↔ φ |- Δ
@@ -171,9 +172,9 @@ object SCProofChecker {
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + temp, ref(t1).left + BinderFormula(ExistsOne, x, phi)))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
// Right rules
/*
@@ -185,9 +186,9 @@ object SCProofChecker {
val phiAndPsi = ConnectorFormula(And, cunjuncts)
if (isSameSet(b.left, t.map(ref(_).left).reduce(_ union _)))
if (isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).reduce(_ union _) + phiAndPsi))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
- else (false, Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
/*
* Γ |- φ, Δ Γ |- φ, ψ, Δ
* -------------- or ---------------
@@ -199,9 +200,9 @@ object SCProofChecker {
if (isSameSet(b.right + phi, ref(t1).right + phiOrPsi) ||
isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
- else (false, Nil, "Left-hand sides of the premise and the conclusion must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
+ else SCInvalidProof(Nil, "Left-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- ψ, Δ
* --------------
@@ -211,9 +212,9 @@ object SCProofChecker {
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(ref(t1).left, b.left + phi))
if (isSameSet(b.right + psi, ref(t1).right + phiImpPsi))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
- else (false, Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
/*
* Γ |- a→ψ, Δ Σ |- ψ→φ, Π
* ----------------------------
@@ -225,9 +226,9 @@ object SCProofChecker {
val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
if (isSameSet(b.left, ref(t1).left union ref(t2).left))
if (isSameSet(b.right + phiImpPsi + psiImpPhi, ref(t1).right union ref(t2).right + phiIffPsi))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
- else (false, Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
/*
* Γ, φ |- Δ
* --------------
@@ -237,9 +238,9 @@ object SCProofChecker {
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.right, ref(t1).right + nPhi))
if (isSameSet(b.left + phi, ref(t1).left))
- (true, Nil, "")
- else (false, Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
- else (false, Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
/*
* Γ |- φ, Δ
* ------------------- if x is not free in the resulting sequent
@@ -249,10 +250,10 @@ object SCProofChecker {
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + phi, ref(t1).right + BinderFormula(Forall, x ,phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
- (true, Nil, "")
- else (false, Nil, "The variable x must not be free in the resulting sequent.")
- else (false, Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
- else (false, Nil, "Left-hand sides of conclusion and premise must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
+ else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same.")
/*
* Γ |- φ[t/x], Δ
* -------------------
@@ -261,9 +262,9 @@ object SCProofChecker {
case RightExists(b, t1, phi, x, t) =>
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + substituteVariable(phi, x, t), ref(t1).right + BinderFormula(Exists, x ,phi)))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
- else (false, Nil, "Left-hand sides or conclusion and premise must be the same.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
+ else SCInvalidProof(Nil, "Left-hand sides or conclusion and premise must be the same.")
/**
* <pre>
@@ -277,9 +278,9 @@ object SCProofChecker {
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + temp, ref(t1).right + BinderFormula(ExistsOne, x, phi)))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
- else (false, Nil, "Left-hand sides of conclusion and premise must be the same")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
+ else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same")
// Structural rules
@@ -291,9 +292,9 @@ object SCProofChecker {
case Weakening(b, t1) =>
if (isSubset(ref(t1).left, b.left))
if (isSubset(ref(t1).right, b.right))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
- else (false, Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
+ else SCInvalidProof(Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
// Equality Rules
/*
@@ -307,11 +308,11 @@ object SCProofChecker {
if (isSame(left, right))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left))
- (true, Nil, "")
- else (false, Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
- else (false, Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
- else (false, Nil, s"φ is not an instance of reflexivity.")
- case _ => (false, Nil, "φ is not an equality")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
+ else SCInvalidProof(Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
+ else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
+ case _ => SCInvalidProof(Nil, "φ is not an equality")
}
/*
@@ -324,10 +325,10 @@ object SCProofChecker {
case PredicateFormula(`equality`, Seq(left, right)) =>
if (isSame(left, right))
if (contains(b.right, phi))
- (true, Nil, "")
- else (false, Nil, s"Right-Hand side of conclusion does not contain φ")
- else (false, Nil, s"φ is not an instance of reflexivity.")
- case _ => (false, Nil, s"φ is not an equality.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-Hand side of conclusion does not contain φ")
+ else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
+ case _ => SCInvalidProof(Nil, s"φ is not an equality.")
}
/*
@@ -343,10 +344,10 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi_t_for_f, ref(t1).left + sEqT + phi_s_for_f) ||
isSameSet(b.left + phi_s_for_f, ref(t1).left + sEqT + phi_t_for_f))
- (true, Nil, "")
- else (false, Nil, "Left-hand sides of the conclusion + φ[s/?f] must be the same as left-hand side of the premise + s=t + φ[t/?f] (or with s and t swapped).")
- else (false, Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
- else (false, Nil, "Function schema ?f must have arity 0")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ[s/?f] must be the same as left-hand side of the premise + s=t + φ[t/?f] (or with s and t swapped).")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ else SCInvalidProof(Nil, "Function schema ?f must have arity 0")
/*
@@ -362,10 +363,10 @@ object SCProofChecker {
val phi_t_for_f = instantiateFunctionSchema(phi, f, t, Nil)
if (isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[s/?f] φ[t/?f], but it isn't the case." )
- else (false, Nil, "Left-hand sides of the premise + s=t must be the same as left-hand side of the premise.")
- else (false, Nil, "Function schema ?f must have arity 0.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[s/?f] φ[t/?f], but it isn't the case." )
+ else SCInvalidProof(Nil, "Left-hand sides of the premise + s=t must be the same as left-hand side of the premise.")
+ else SCInvalidProof(Nil, "Function schema ?f must have arity 0.")
/*
* Γ, φ[ψ/?q] |- Δ
* ---------------------
@@ -379,10 +380,10 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(ref(t1).left + psiIffTau + phi_tau_for_q, b.left + phi_psi_for_q) ||
isSameSet(ref(t1).left + psiIffTau + phi_psi_for_q, b.left + phi_tau_for_q))
- (true, Nil, "")
- else (false, Nil, "Left-hand sides of the conclusion + φ[ψ/?q] must be the same as left-hand side of the premise + ψ↔τ + φ[τ/?q] (or with ψ and τ swapped).")
- else (false, Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
- else (false, Nil, "Predicate schema ?q must have arity 0.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ[ψ/?q] must be the same as left-hand side of the premise + ψ↔τ + φ[τ/?q] (or with ψ and τ swapped).")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ else SCInvalidProof(Nil, "Predicate schema ?q must have arity 0.")
/*
* Γ |- φ[ψ/?p], Δ
@@ -397,10 +398,10 @@ object SCProofChecker {
if (isSameSet(ref(t1).left + psiIffTau, b.left))
if (isSameSet(b.right + phi_tau_for_q, ref(t1).right + phi_psi_for_q) ||
isSameSet(b.right + phi_psi_for_q, ref(t1).right + phi_tau_for_q))
- (true, Nil, "")
- else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case." )
- else (false, Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
- else (false, Nil, "Predicate schema ?q must have arity 0.")
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case." )
+ else SCInvalidProof(Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
+ else SCInvalidProof(Nil, "Predicate schema ?q must have arity 0.")
/**
* <pre>
* Γ |- Δ
@@ -412,9 +413,9 @@ object SCProofChecker {
val expected = (ref(t1).left.map(phi => instantiateFunctionSchema(phi, f, r, a)), ref(t1).right.map(phi => instantiateFunctionSchema(phi, f, r, a)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of premise instantiated with [?f/r(a)] must be the same as right-hand side of conclusion.")
- else (false, Nil, "Left-hand side of premise instantiated with [?f/r(a)] must be the same as left-hand side of conclusion.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?f/r(a)] must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(Nil, "Left-hand side of premise instantiated with [?f/r(a)] must be the same as left-hand side of conclusion.")
/**
* <pre>
@@ -427,45 +428,38 @@ object SCProofChecker {
val expected = (ref(t1).left.map(phi => instantiatePredicateSchema(phi, p, psi, a)), ref(t1).right.map(phi => instantiatePredicateSchema(phi, p, psi, a)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
- (true, Nil, "")
- else (false, Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
- else (false, Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] must be the same as left-hand side of conclusion.")
+ SCValidProof
+ else SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] must be the same as left-hand side of conclusion.")
case SCSubproof(sp, premises, _) =>
if (premises.size == sp.imports.size){
val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)) )
if (invalid.isEmpty){
- val r_subproof = checkSCProof(sp)
- if (r_subproof._1)
- (true, Nil, "")
- else (false, r_subproof._2, r_subproof._3)
- } else (false, Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
- } else (false, Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
+ checkSCProof(sp)
+ } else SCInvalidProof(Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
+ } else SCInvalidProof(Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
}
r
}
/**
- * Verifies if a given pure SequentCalculus is conditionally correct, as the imported sequents are assumed.
+ * Verifies if a given pure SequentCalculus is conditionally correct, as the imported sequents are assumed.
* If the proof is not correct, the functrion will report the faulty line and a brief explanation.
* @param proof A SC proof to check
- * @return (true, Nil, "") if the proof is correct, else (false, l, s) with l the path to the incorrect
- proof step and s an explanation.
- *
+ * @return SCValidProof if the proof is correct, else SCInvalidProof with the path to the incorrect proof step
+ * and an explanation.
*/
- def checkSCProof(proof: SCProof) : (Boolean, List[Int], String) = {
-
-
+ def checkSCProof(proof: SCProof): SCProofCheckerJudgement = {
val possibleError = proof.steps.view.zipWithIndex.map((step, no) =>
-
- val r = checkSingleSCStep(no, step, (i:Int) => proof.getSequent(i), Some(proof.imports.size))
- (r._1, no::r._2, r._3)
- ).find(p => !p._1 )
- if (possibleError.isEmpty) (true, Nil, "")
+ checkSingleSCStep(no, step, (i: Int) => proof.getSequent(i), Some(proof.imports.size)) match {
+ case SCInvalidProof(path, message) => SCInvalidProof(no +: path, message)
+ case SCValidProof => SCValidProof
+ }
+ ).find(j => !j.isValid)
+ if (possibleError.isEmpty) SCValidProof
else possibleError.get
-
-
}
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala b/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bf81d106f20b8587e6cd263bdefa6e6256f5e6b0
--- /dev/null
+++ b/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala
@@ -0,0 +1,33 @@
+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
+}
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index d2a91582516ff99e34a851dcdef73712570788cd..8389948f31f03fe9f877b3c202ca4c63e43921aa 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/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)
}
}
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 8f88cc953bed2e22bcb571b011f690d4bd645244..5eb2269e58a8b82afeb609df11377f521cd7bf3e 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/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"))
})
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index df8786aac3c0d1722d32f116de201259402add4b..57872adb26d740736a40539c375e261b6ab4c817 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/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}")
}
}