From 4c6aa9a953d58448a9fdf8b28f7e7c7a2781feca Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Tue, 19 Jul 2022 13:23:15 +0200
Subject: [PATCH] ran scalafixAll
---
.../scala/lisa/test/ProofCheckerSuite.scala | 86 +++++++++----------
1 file changed, 43 insertions(+), 43 deletions(-)
diff --git a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
index 7f5c4e7a..6c3d6c4f 100644
--- a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
+++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
@@ -12,48 +12,48 @@ import scala.language.adhocExtensions
abstract class ProofCheckerSuite extends AnyFunSuite {
- import lisa.kernel.fol.FOL.*
-
- protected val (xl, yl, zl, wl, xpl, ypl, zpl, wpl) = (
- VariableLabel("x"),
- VariableLabel("y"),
- VariableLabel("z"),
- VariableLabel("w"),
- VariableLabel("x'"),
- VariableLabel("y'"),
- VariableLabel("z'"),
- VariableLabel("w'")
+ import lisa.kernel.fol.FOL.*
+
+ protected val (xl, yl, zl, wl, xpl, ypl, zpl, wpl) = (
+ VariableLabel("x"),
+ VariableLabel("y"),
+ VariableLabel("z"),
+ VariableLabel("w"),
+ VariableLabel("x'"),
+ VariableLabel("y'"),
+ VariableLabel("z'"),
+ VariableLabel("w'")
+ )
+ protected val (x, y, z, w, xp, yp, zp, wp) = (
+ VariableTerm(xl),
+ VariableTerm(yl),
+ VariableTerm(zl),
+ VariableTerm(wl),
+ VariableTerm(xpl),
+ VariableTerm(ypl),
+ VariableTerm(zpl),
+ VariableTerm(wpl)
+ )
+
+ protected val (sl, tl, ul, vl) = (VariableLabel("s"), VariableLabel("t"), VariableLabel("u"), VariableLabel("v"))
+ protected val (s, t, u, v) = (VariableTerm(sl), VariableTerm(tl), VariableTerm(ul), VariableTerm(vl))
+
+ def checkProof(proof: SCProof): Unit = {
+ val judgement = checkSCProof(proof)
+ println(Printer.prettySCProof(judgement))
+ println(s"\n(${proof.totalLength} proof steps in total)")
+ }
+
+ def checkProof(proof: SCProof, expected: Sequent): Unit = {
+ val judgement = checkSCProof(proof)
+ assert(judgement.isValid, "\n" + Printer.prettySCProof(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).isValid,
+ s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}"
)
- protected val (x, y, z, w, xp, yp, zp, wp) = (
- VariableTerm(xl),
- VariableTerm(yl),
- VariableTerm(zl),
- VariableTerm(wl),
- VariableTerm(xpl),
- VariableTerm(ypl),
- VariableTerm(zpl),
- VariableTerm(wpl)
- )
-
- protected val (sl, tl, ul, vl) = (VariableLabel("s"), VariableLabel("t"), VariableLabel("u"), VariableLabel("v"))
- protected val (s, t, u, v) = (VariableTerm(sl), VariableTerm(tl), VariableTerm(ul), VariableTerm(vl))
-
- def checkProof(proof: SCProof): Unit = {
- val judgement = checkSCProof(proof)
- println(Printer.prettySCProof(judgement))
- println(s"\n(${proof.totalLength} proof steps in total)")
- }
-
- def checkProof(proof: SCProof, expected: Sequent): Unit = {
- val judgement = checkSCProof(proof)
- assert(judgement.isValid, "\n" + Printer.prettySCProof(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).isValid,
- s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}"
- )
- }
+ }
}
--
GitLab