From fbc8c0df765808c59955e10be4ae212fb5a31d55 Mon Sep 17 00:00:00 2001
From: Florian Cassayre <florian.cassayre@gmail.com>
Date: Tue, 14 Jun 2022 09:56:51 +0200
Subject: [PATCH] Re-enable scalafix/scalafmt, re-format everything
---
build.sbt | 33 +++++++++------
lisa-examples/src/main/scala/Example.scala | 4 +-
.../lisa/kernel/proof/RunningTheory.scala | 3 +-
.../lisa/kernel/proof/SCProofChecker.scala | 16 +++----
.../lisa/settheory/SetTheoryDefinitions.scala | 2 +-
.../lisa/settheory/SetTheoryTGAxioms.scala | 2 +-
.../lisa/settheory/SetTheoryZFAxioms.scala | 2 +-
.../main/scala/lisa/tptp/KernelParser.scala | 6 +--
.../scala/lisa/tptp/ProblemGatherer.scala | 2 +-
.../main/scala/lisa/utils/KernelHelpers.scala | 15 ++++---
.../src/main/scala/lisa/utils/Library.scala | 42 ++++++++++++-------
.../scala/lisa/utils/TheoriesHelpers.scala | 17 ++++----
.../lisa/kernel/EquivalenceCheckerTests.scala | 13 +++---
.../src/test/scala/lisa/kernel/FolTests.scala | 5 ++-
.../test/scala/lisa/kernel/ProofTests.scala | 7 ++--
.../scala/lisa/test/ProofCheckerSuite.scala | 10 +++--
.../test/scala/lisa/utils/PrinterTest.scala | 6 ++-
.../lisa/proven/tactics/ProofTactics.scala | 2 +-
.../tactics/SimplePropositionalSolver.scala | 12 +++---
.../lisa/proven/InitialProofsTests.scala | 3 +-
.../scala/lisa/proven/SimpleProverTests.scala | 10 +++--
21 files changed, 124 insertions(+), 88 deletions(-)
diff --git a/build.sbt b/build.sbt
index b82c7792..8f622c01 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,31 +4,37 @@ inThisBuild(Def.settings(
organizationHomepage := Some(url("https://lara.epfl.ch")),
licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html")),
versionScheme := Some("semver-spec"),
+ scalacOptions ++= Seq(
+ "-feature",
+ "-deprecation",
+ "-unchecked",
+ ),
+ semanticdbEnabled := true,
+ semanticdbVersion := scalafixSemanticdb.revision,
+ scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
))
val scala2 = "2.13.8"
val scala3 = "3.1.3"
-lazy val commonSettings2 = Seq(
+val commonSettings2 = Seq(
scalaVersion := scala2,
)
-lazy val commonSettings3 = Seq(
+val commonSettings3 = Seq(
scalaVersion := scala3,
scalacOptions ++= Seq(
- "-feature",
- "-deprecation",
- //"-source:future",
"-language:implicitConversions",
- //"-old-syntax",
- //"-no-indent",
+ //"-source:future", re-enable when liancheng/scalafix-organize-imports#221 is fixed
+ "-old-syntax",
+ "-no-indent",
),
libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
Test / parallelExecution := false,
- semanticdbEnabled := true,
- semanticdbVersion := scalafixSemanticdb.revision,
- scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0",
)
+def withTests(project: Project): ClasspathDependency =
+ project % "compile->compile;test->test"
+
lazy val root = Project(
id = "lisa-core",
base = file("."),
@@ -37,7 +43,8 @@ lazy val root = Project(
.settings(
version := "0.1",
)
- .dependsOn(kernel, utils, theories, tptp) // Everything but `examples`
+ .dependsOn(kernel, withTests(utils), theories, tptp) // Everything but `examples`
+ .aggregate(kernel, utils, theories, tptp) // To run tests on all modules
lazy val kernel = Project(
id = "lisa-kernel",
@@ -60,7 +67,7 @@ lazy val theories = Project(
base = file("lisa-theories"),
)
.settings(commonSettings3)
- .dependsOn(utils)
+ .dependsOn(withTests(utils))
lazy val tptp = Project(
id = "lisa-tptp",
@@ -70,7 +77,7 @@ lazy val tptp = Project(
.settings(
libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4",
)
- .dependsOn(utils)
+ .dependsOn(withTests(utils))
lazy val examples = Project(
id = "lisa-examples",
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 228994a7..725ef410 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -1,14 +1,14 @@
-import lisa.utils.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SCProofChecker.*
import lisa.kernel.proof.SequentCalculus.*
import lisa.proven.tactics.SimplePropositionalSolver.solveSequent
-import lisa.utils.Helpers.{_, given}
import lisa.tptp.KernelParser.*
import lisa.tptp.ProblemGatherer.*
import lisa.tptp.*
+import lisa.utils.Helpers.{_, given}
+import lisa.utils.Printer.*
/**
* Discover some of the elements of LISA to get started.
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 0a94eaeb..7d15e8e5 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -105,8 +105,7 @@ class RunningTheory {
case r @ SCProofCheckerJudgement.SCInvalidProof(_, _, message) =>
InvalidJustification("The given proof is incorrect: " + message, Some(r))
}
- }
- else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
+ } else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
else InvalidJustification("Not all imports of the proof are correctly justified.", None)
/**
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 34cf960d..a2ff683d 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -76,8 +76,8 @@ object SCProofChecker {
val phiAndPsi = ConnectorFormula(And, Seq(phi, psi))
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)
+ isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
+ isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi)
)
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
@@ -118,8 +118,8 @@ object SCProofChecker {
if (isSameSet(ref(t1).right, b.right))
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)
+ isSameSet(b.left + psiImpPhi, ref(t1).left + phiIffPsi) ||
+ isSameSet(b.left + phiImpPsi + psiImpPhi, ref(t1).left + phiIffPsi)
)
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
@@ -201,8 +201,8 @@ object SCProofChecker {
if (isSameSet(ref(t1).left, b.left))
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)
+ isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
+ isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi)
)
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
@@ -348,7 +348,7 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (
isSameSet(b.left + phi_t_for_f, ref(t1).left ++ sEqT_es + phi_s_for_f) ||
- isSameSet(b.left + phi_s_for_f, ref(t1).left ++ sEqT_es + phi_t_for_f)
+ isSameSet(b.left + phi_s_for_f, ref(t1).left ++ sEqT_es + phi_t_for_f)
)
SCValidProof(SCProof(step))
else
@@ -372,7 +372,7 @@ object SCProofChecker {
val phi_t_for_f = lambdaPhi(t_es)
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)
+ isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f)
)
SCValidProof(SCProof(step))
else
diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 531076bd..20263c2a 100644
--- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -1,6 +1,6 @@
package lisa.settheory
-import lisa.kernel.fol.FOL._
+import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.utils.Helpers.{_, given}
diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index 72e9bbb4..49624d35 100644
--- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -1,6 +1,6 @@
package lisa.settheory
-import lisa.kernel.fol.FOL._
+import lisa.kernel.fol.FOL.*
import lisa.utils.Helpers.{_, given}
/**
diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index fd0d2b67..bd95ad45 100644
--- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -1,6 +1,6 @@
package lisa.settheory
-import lisa.kernel.fol.FOL._
+import lisa.kernel.fol.FOL.*
import lisa.utils.Helpers.{_, given}
/**
diff --git a/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala b/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
index df98eeac..66455c19 100644
--- a/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
@@ -6,8 +6,8 @@ import leo.datastructures.TPTP.FOF
import leo.modules.input.TPTPParser as Parser
import lisa.kernel.fol.FOL as K
import lisa.kernel.proof.SequentCalculus as LK
-import lisa.utils.Helpers.*
import lisa.tptp.*
+import lisa.utils.Helpers.*
import java.io.File
import scala.util.matching.Regex
@@ -189,11 +189,11 @@ object KernelParser {
} else throw new Exception("Specified path is not a directory.")
} else throw new Exception("Specified path does not exist.")
- val r = probfiles.foldRight(List.empty[Problem])((p, current) =>
+ val r = probfiles.foldRight(List.empty[Problem])((p, current) => {
val md = getProblemInfos(p)
if (md.spc.exists(spc.contains)) problemToKernel(p, md) :: current
else current
- )
+ })
r
}
diff --git a/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala b/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
index 8c1278c8..d87de895 100644
--- a/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
@@ -1,6 +1,6 @@
package lisa.tptp
-import lisa.tptp.KernelParser._
+import lisa.tptp.KernelParser.*
object ProblemGatherer {
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 6b378f9f..e372a02e 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -120,20 +120,25 @@ trait KernelHelpers {
def apply(t: T): Set[S]
}
- given [S]: SetConverter[S, Unit] with
+ given [S]: SetConverter[S, Unit] with {
override def apply(u: Unit): Set[S] = Set.empty
+ }
- given [S]: SetConverter[S, EmptyTuple] with
+ given [S]: SetConverter[S, EmptyTuple] with {
override def apply(t: EmptyTuple): Set[S] = Set.empty
+ }
- given [S, H <: S, T <: Tuple](using SetConverter[S, T]): SetConverter[S, H *: T] with
+ given [S, H <: S, T <: Tuple](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
+ 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
+ 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)
diff --git a/lisa-utils/src/main/scala/lisa/utils/Library.scala b/lisa-utils/src/main/scala/lisa/utils/Library.scala
index c882e680..3863a9b6 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Library.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Library.scala
@@ -81,11 +81,12 @@ abstract class Library(val theory: RunningTheory) {
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
case class TheoremNameWithProof(name: String, statement: String, proof: Proof)(using String => Unit) {
- infix def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match
+ infix def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
+ }
/**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
@@ -98,18 +99,20 @@ abstract class Library(val theory: RunningTheory) {
/**
* Allows to create a definition by shortcut of a function symbol:
*/
- def simpleDefinition(symbol: String, expression: LambdaTermTerm): Judgement[theory.FunctionDefinition] =
+ def simpleDefinition(symbol: String, expression: LambdaTermTerm): Judgement[theory.FunctionDefinition] = {
val LambdaTermTerm(vars, body) = expression
val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicFunctions.map(_.id)).toSet, "y"))
val proof: Proof = simpleFunctionDefinition(expression, out)
theory.functionDefinition(symbol, LambdaTermFormula(vars, out === body), out, proof, Nil)
+ }
/**
* Allows to create a definition by existential uniqueness of a function symbol:
*/
- def complexDefinition(symbol: String, vars: Seq[SchematicFunctionLabel], v: SchematicFunctionLabel, f: Formula, proof: Proof, just: Seq[Justification]): Judgement[theory.FunctionDefinition] =
+ def complexDefinition(symbol: String, vars: Seq[SchematicFunctionLabel], v: SchematicFunctionLabel, f: Formula, proof: Proof, just: Seq[Justification]): Judgement[theory.FunctionDefinition] = {
val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ f.schematicFunctions.map(_.id)).toSet, "y"))
theory.functionDefinition(symbol, LambdaTermFormula(vars, instantiateFunctionSchemas(f, Map(v -> LambdaTermTerm(Nil, out)))), out, proof, just)
+ }
/**
* Allows to create a definition by shortcut of a function symbol:
@@ -127,24 +130,28 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
*/
- infix def as(t: Term)(using String => Unit): ConstantFunctionLabel =
- val definition = simpleDefinition(symbol, LambdaTermTerm(vars, t)) match
+ infix def as(t: Term)(using String => Unit): ConstantFunctionLabel = {
+ val definition = simpleDefinition(symbol, LambdaTermTerm(vars, t)) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
+ }
definition.label
+ }
/**
* Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
*/
- infix def as(f: Formula)(using String => Unit): ConstantPredicateLabel =
- val definition = simpleDefinition(symbol, LambdaTermFormula(vars, f)) match
+ infix def as(f: Formula)(using String => Unit): ConstantPredicateLabel = {
+ val definition = simpleDefinition(symbol, LambdaTermFormula(vars, f)) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
+ }
definition.label
+ }
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
@@ -182,13 +189,15 @@ abstract class Library(val theory: RunningTheory) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
- infix def using(justifications: theory.Justification*)(using String => Unit): ConstantFunctionLabel =
- val definition = complexDefinition(symbol, vars, out, f, proof, justifications) match
+ infix def using(justifications: theory.Justification*)(using String => Unit): ConstantFunctionLabel = {
+ val definition = complexDefinition(symbol, vars, out, f, proof, justifications) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
+ }
definition.label
+ }
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
@@ -239,41 +248,46 @@ abstract class Library(val theory: RunningTheory) {
* Fetch a Theorem by its name.
*/
def getTheorem(name: String): theory.Theorem =
- theory.getTheorem(name) match
+ theory.getTheorem(name) match {
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No theorem with name \"$name\" was found.")
+ }
/**
* Fetch an Axiom by its name.
*/
def getAxiom(name: String): theory.Axiom =
- theory.getAxiom(name) match
+ theory.getAxiom(name) match {
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No axiom with name \"$name\" was found.")
+ }
/**
* Fetch a Definition by its symbol.
*/
def getDefinition(name: String): theory.Definition =
- theory.getDefinition(name) match
+ theory.getDefinition(name) match {
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No definition for symbol \"$name\" was found.")
+ }
/**
* Prints a short representation of the last theorem or definition introduced
*/
- def show(using String => Unit): Justification = last match
+ def show(using String => Unit): Justification = last match {
case Some(value) => value.show
case None => throw new NoSuchElementException("There is nothing to show: No theorem or definition has been proved yet.")
+ }
// given Conversion[String, theory.Justification] = name => theory.getJustification(name).get
/**
* Converts different class that have a natural interpretation as a Sequent
*/
- private def sequantableToSequent(s: Sequentable): Sequent = s match
+ private def sequantableToSequent(s: Sequentable): Sequent = s match {
case j: Justification => theory.sequentFromJustification(j)
case f: Formula => () |- f
case s: Sequent => s
+ }
given Conversion[Sequentable, Sequent] = sequantableToSequent
given Conversion[Axiom, Formula] = theory.sequentFromJustification(_).right.head
diff --git a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
index 265bfd7f..58678892 100644
--- a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
@@ -69,18 +69,20 @@ trait TheoriesHelpers extends KernelHelpers {
* Outputs, with an implicit output function, a readable representation of the Axiom, Theorem or Definition.
*/
def show(using output: String => Unit): just.type = {
- just match
+ just match {
case thm: RunningTheory#Theorem => output(s" Theorem ${thm.name} := ${Printer.prettySequent(thm.proposition)}\n")
case axiom: RunningTheory#Axiom => output(s" Axiom ${axiom.name} := ${Printer.prettyFormula(axiom.ax)}\n")
case d: RunningTheory#Definition =>
- d match
+ d match {
case pd: RunningTheory#PredicateDefinition =>
output(s" Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.expression.vars.map(_())*) <=> pd.expression.body)}\n") // (label, args, phi)
case fd: RunningTheory#FunctionDefinition =>
output(s" Definition of function symbol ${Printer.prettyTerm(fd.label(fd.expression.vars.map(_())*))} := the ${fd.out.id} such that ${Printer
.prettyFormula((fd.out === fd.label(fd.expression.vars.map(_())*)) <=> fd.expression.body)})\n")
- // output(Printer.prettySequent(thm.proposition))
- // thm
+ }
+ // output(Printer.prettySequent(thm.proposition))
+ // thm
+ }
just
}
}
@@ -92,15 +94,16 @@ trait TheoriesHelpers extends KernelHelpers {
* Otherwise, output the error leading to the invalid justification and throw an error.
*/
def showAndGet(using output: String => Unit): J = {
- theoryJudgement match
+ theoryJudgement match {
case RunningTheoryJudgement.ValidJustification(just) =>
just.show
case InvalidJustification(message, error) =>
- output(s"$message\n${error match
+ output(s"$message\n${error match {
case Some(judgement) => Printer.prettySCProof(judgement)
case None => ""
- }")
+ }}")
theoryJudgement.get
+ }
}
}
diff --git a/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index fe309785..aa0c31f2 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -1,14 +1,15 @@
package lisa.kernel
-import lisa.utils.Printer
import lisa.kernel.fol.FOL
import lisa.kernel.fol.FOL.*
-import org.scalatest.funsuite.AnyFunSuite
import lisa.utils.Helpers.*
+import lisa.utils.Printer
+import org.scalatest.funsuite.AnyFunSuite
import scala.collection.MapView
import scala.collection.mutable.ArrayBuffer
import scala.collection.mutable.ListBuffer
+import scala.language.adhocExtensions
import scala.util.Random
class EquivalenceCheckerTests extends AnyFunSuite {
@@ -364,10 +365,10 @@ class EquivalenceCheckerTests extends AnyFunSuite {
test("All allowed transformations") {
val transformations: Seq[Random => Formula => Formula] = IndexedSeq(
- r => commutativeShuffle(1)(r) _,
- r => associativeShuffle(1)(r) _,
- r => addDoubleNegations(0.02)(r) _,
- r => addDeMorgans(0.05)(r) _
+ r => commutativeShuffle(1)(r),
+ r => associativeShuffle(1)(r),
+ r => addDoubleNegations(0.02)(r),
+ r => addDeMorgans(0.05)(r)
)
def randomTransformations(random: Random)(f: Formula): Formula = {
val n = random.nextInt(50)
diff --git a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
index f4b12ded..f39b1bd2 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,16 +1,17 @@
package lisa.kernel
-import lisa.utils.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
-import org.scalatest.funsuite.AnyFunSuite
import lisa.utils.Helpers.{_, given}
+import lisa.utils.Printer
+import org.scalatest.funsuite.AnyFunSuite
import scala.collection.immutable.SortedSet
+import scala.language.adhocExtensions
import scala.util.Random
class FolTests extends AnyFunSuite {
diff --git a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
index 85f9210f..53fa5f17 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,15 +1,16 @@
package lisa.kernel
-import lisa.utils.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
-import org.scalatest.funsuite.AnyFunSuite
import lisa.utils.Helpers.{_, given}
+import lisa.utils.Printer
+import org.scalatest.funsuite.AnyFunSuite
+import scala.language.adhocExtensions
import scala.util.Random
class ProofTests extends AnyFunSuite {
@@ -50,7 +51,7 @@ class ProofTests extends AnyFunSuite {
var subformulas = pairs.map(p => or(p.head, p.last)).grouped(2)
var subformulasSwapped = sPairs.map(p => if (r.nextBoolean()) or(p.head, p.last) else or(p.last, p.head)).grouped(2)
for (i <- 1 until k) {
- val op = if (i % 2 == 0) or _ else and _
+ val op = if (i % 2 == 0) or else and
subformulas = subformulas.map(sf => op(sf.head, sf.last)).grouped(2)
subformulasSwapped = subformulasSwapped.map(sf => if (r.nextBoolean()) op(sf.head, sf.last) else op(sf.last, sf.head)).grouped(2)
}
diff --git a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
index dcb4fa26..6765e70a 100644
--- a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
+++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
@@ -1,12 +1,14 @@
package lisa.test
-import lisa.utils.Printer
import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SCProofChecker._
+import lisa.kernel.proof.SCProofChecker.*
import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.proof.SequentCalculus.isSameSequent
-import org.scalatest.funsuite.AnyFunSuite
import lisa.utils.Helpers.{_, given}
+import lisa.utils.Printer
+import org.scalatest.funsuite.AnyFunSuite
+
+import scala.language.adhocExtensions
abstract class ProofCheckerSuite extends AnyFunSuite {
import lisa.kernel.fol.FOL.*
@@ -43,7 +45,7 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
def checkProof(proof: SCProof, expected: Sequent): Unit = {
val judgement = checkSCProof(proof)
- assert(judgement.isValid, "\n" + Printer.prettySCProof( judgement))
+ assert(judgement.isValid, "\n" + Printer.prettySCProof(judgement))
assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
}
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index e2675436..d19514fb 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -1,9 +1,11 @@
package lisa.utils
-import lisa.utils.Printer._
-import lisa.kernel.fol.FOL._
+import lisa.kernel.fol.FOL.*
+import lisa.utils.Printer.*
import org.scalatest.funsuite.AnyFunSuite
+import scala.language.adhocExtensions
+
class PrinterTest extends AnyFunSuite {
val (a, b, c) = (ConstantPredicateLabel("a", 0), ConstantPredicateLabel("b", 0), ConstantPredicateLabel("c", 0))
diff --git a/src/main/scala/lisa/proven/tactics/ProofTactics.scala b/src/main/scala/lisa/proven/tactics/ProofTactics.scala
index 3567982a..c75768cb 100644
--- a/src/main/scala/lisa/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/lisa/proven/tactics/ProofTactics.scala
@@ -1,10 +1,10 @@
package lisa.proven.tactics
-import lisa.utils.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
import lisa.utils.Helpers.{_, given}
+import lisa.utils.Printer.*
import scala.collection.immutable.Set
diff --git a/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
index a38c006e..c48c282d 100644
--- a/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
@@ -64,7 +64,7 @@ object SimplePropositionalSolver {
val proof1 = solveOrganisedSequent(left, right, s -< f +> phi, offset)
val proof2 = solveOrganisedSequent(rl, rr, s -< f +< psi, offset + proof1.size)
LeftImplies(s, proof1.size + offset - 1, proof1.size + proof2.size + offset - 1, phi, psi) :: (proof2 ++ proof1)
- } else if (left.iffs.nonEmpty)
+ } else if (left.iffs.nonEmpty) {
val f = left.iffs.head
val phi = f.args(0)
val psi = f.args(1)
@@ -73,7 +73,7 @@ object SimplePropositionalSolver {
left.updateFormula(psi ==> phi, true)
val proof = solveOrganisedSequent(left, right, s -< f +< (phi ==> psi) +< (psi ==> phi), offset)
LeftIff(s, proof.length - 1 + offset, phi, psi) :: proof
- else if (left.ands.nonEmpty) {
+ } else if (left.ands.nonEmpty) {
val f = left.ands.head
val phi = f.args(0)
val psi = f.args(1)
@@ -96,14 +96,14 @@ object SimplePropositionalSolver {
val proof1 = solveOrganisedSequent(left, right, s -< f +< phi, offset)
val proof2 = solveOrganisedSequent(rl, rr, s -< f +< psi, offset + proof1.size)
LeftOr(s, Seq(proof1.size + offset - 1, proof1.size + proof2.size + offset - 1), Seq(phi, psi)) :: (proof2 ++ proof1)
- } else if (right.negs.nonEmpty)
+ } else if (right.negs.nonEmpty) {
val f = right.negs.head
val phi = f.args.head
right.updateFormula(f, false)
left.updateFormula(phi, true)
val proof = solveOrganisedSequent(left, right, s -> f +< phi, offset)
RightNot(s, proof.length - 1 + offset, phi) :: proof
- else if (right.impliess.nonEmpty) {
+ } else if (right.impliess.nonEmpty) {
val f = right.impliess.head
val phi = f.args(0)
val psi = f.args(1)
@@ -112,7 +112,7 @@ object SimplePropositionalSolver {
right.updateFormula(psi, true)
val proof = solveOrganisedSequent(left, right, s -> f +< phi +> psi, offset)
RightImplies(s, proof.length - 1 + offset, phi, psi) :: proof
- } else if (right.iffs.nonEmpty)
+ } else if (right.iffs.nonEmpty) {
val f = right.iffs.head
val phi = f.args(0)
val psi = f.args(1)
@@ -124,7 +124,7 @@ object SimplePropositionalSolver {
val proof1 = solveOrganisedSequent(left, right, s -> f +> (phi ==> psi), offset)
val proof2 = solveOrganisedSequent(rl, rr, s -> f +> (psi ==> phi), offset + proof1.size)
RightIff(s, proof1.size + offset - 1, proof1.size + proof2.size + offset - 1, phi, psi) :: (proof2 ++ proof1)
- else if (right.ands.nonEmpty) {
+ } else if (right.ands.nonEmpty) {
val f = right.ands.head
val phi = f.args(0)
val psi = f.args(1)
diff --git a/src/test/scala/lisa/proven/InitialProofsTests.scala b/src/test/scala/lisa/proven/InitialProofsTests.scala
index c9873cdc..8872b041 100644
--- a/src/test/scala/lisa/proven/InitialProofsTests.scala
+++ b/src/test/scala/lisa/proven/InitialProofsTests.scala
@@ -1,7 +1,7 @@
package lisa.proven
-import lisa.utils.Printer
import lisa.test.ProofCheckerSuite
+import lisa.utils.Printer
class InitialProofsTests extends ProofCheckerSuite {
import lisa.proven.SetTheoryLibrary.*
@@ -16,5 +16,4 @@ class InitialProofsTests extends ProofCheckerSuite {
succeed
}
-
}
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 57599edf..e6ba8d3f 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,16 +1,18 @@
package lisa.proven
-import lisa.utils.Printer
-import lisa.utils.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.PredicateLogic
import lisa.kernel.proof.SCProofChecker
-import org.scalatest.funsuite.AnyFunSuite
import lisa.proven.tactics.SimplePropositionalSolver as SPS
-import lisa.utils.Helpers.*
import lisa.tptp.KernelParser.*
import lisa.tptp.ProblemGatherer.getPRPproblems
+import lisa.utils.Helpers.*
+import lisa.utils.Printer
+import lisa.utils.Printer.*
+import org.scalatest.funsuite.AnyFunSuite
+
+import scala.language.adhocExtensions
class SimpleProverTests extends AnyFunSuite {
--
GitLab