From 6172b840021d27fdd08af262959b099df2b081ed Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Sat, 16 Jul 2022 22:11:51 +0200
Subject: [PATCH] Add utils to follow the path to an incorrect proof step and
to create an error message from invalid proof judgement
---
.../main/scala/lisa/utils/KernelHelpers.scala | 26 ++++++++++++++++---
1 file changed, 23 insertions(+), 3 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index a5bb1b41..594a6fbf 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -4,9 +4,8 @@ import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheoryJudgement
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SequentCalculus
-import lisa.kernel.proof.SequentCalculus.Rewrite
-import lisa.kernel.proof.SequentCalculus.isSameSequent
+import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof
+import lisa.kernel.proof.SequentCalculus._
/**
* A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
@@ -153,4 +152,25 @@ trait KernelHelpers {
s.left.map(phi => instantiateTermSchemas(phi, m)) |- s.right.map(phi => instantiateTermSchemas(phi, m))
}
+ extension (sp: SCSubproof) {
+ def followPath(path: Seq[Int]): SCProofStep = path match {
+ case Nil => sp
+ case n :: Nil => sp.sp(n)
+ case n :: ns =>
+ assert(sp.sp.steps(n).isInstanceOf[SCSubproof], s"Got $path but next step is not a subproof: ${sp.sp.steps(n).getClass}")
+ sp.sp.steps(n).asInstanceOf[SCSubproof].followPath(ns)
+ }
+ }
+
+ extension (p: SCProof) {
+ def followPath(path: Seq[Int]): SCProofStep = SCSubproof(p, p.imports.indices).followPath(path)
+ }
+
+ extension (judgement: SCInvalidProof) {
+ def errorMsg: String =
+ s"""Failed to prove
+ |${lisa.utils.Printer.prettySequent(judgement.proof.followPath(judgement.path).bot)}
+ |(step ${judgement.path.mkString("->")}): ${judgement.message}""".stripMargin
+ }
+
}
--
GitLab