diff --git a/build.sbt b/build.sbt index b3fa0c6b4c45b7befa78cbcee95d0ff0a8282cd6..6398b4f94b7ab83b7cde631eeaac402e360f77d3 100644 --- a/build.sbt +++ b/build.sbt @@ -26,8 +26,9 @@ val commonSettings3 = Seq( "-language:implicitConversions", //"-source:future", re-enable when liancheng/scalafix-organize-imports#221 is fixed "-no-indent", + "-old-syntax", "-source:future-migration", - "-rewrite", + //"-rewrite", ), libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test", libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1", diff --git a/lisa-front/src/test/scala/lisa/front/FrontMacroTests.scala b/lisa-front/src/test/scala/lisa/front/FrontMacroTests.scala index d579940e5ea83ca014c3dd6bde01e24241cddbab..1f13351ed4e09e877666c8e1e992a28c312079e2 100644 --- a/lisa-front/src/test/scala/lisa/front/FrontMacroTests.scala +++ b/lisa-front/src/test/scala/lisa/front/FrontMacroTests.scala @@ -1,6 +1,6 @@ package lisa.front -import lisa.front.{_, given} +import lisa.front.{*, given} import org.scalatest.funsuite.AnyFunSuite import scala.language.adhocExtensions @@ -21,12 +21,12 @@ class FrontMacroTests extends AnyFunSuite { val y0:Term = SchematicTermLabel[0]("y")() term"$y0" assert(term"{$f(x, $y0)}".toString == "{?f(x, ?y)}") - assert(formula"{} = {$f(x, $y0)}".toString == "∅ = {?f(x, ?y)}") + assert(formula"{} = {$f(x, $y0)}".toString == "? = {?f(x, ?y)}") val p0 = ConstantPredicateLabel[0]("p") val v = VariableLabel("x") - assert(sequent" |- $p0".toString == "⊢ p") - assert(partial"\ $v. $v = {}; f($y0) |- $p0 /\ b; ...".toString == raw"\x. f(?y); x = ∅ ⊢ p ∧ b; …") + assert(sequent" |- $p0".toString == "? p") + assert(partial"\ $v. $v = {}; f($y0) |- $p0 /\ b; ...".toString == raw"\x. f(?y); x = ? ? p ? b; ?") } */ } diff --git a/lisa-front/src/test/scala/lisa/front/UnificationTests.scala b/lisa-front/src/test/scala/lisa/front/UnificationTests.scala index 26103982bae86ac4eb44d61a3d3445290c2c168e..3c399541e42580a4f8b596eb19b8c639b6ba6fca 100644 --- a/lisa-front/src/test/scala/lisa/front/UnificationTests.scala +++ b/lisa-front/src/test/scala/lisa/front/UnificationTests.scala @@ -4,7 +4,7 @@ import lisa.front.fol.FOL.LabelType import lisa.front.fol.FOL.WithArityType import lisa.front.printer.FrontPositionedPrinter import lisa.front.printer.FrontPrintStyle -import lisa.front.{_, given} +import lisa.front.{*, given} import org.scalatest.Ignore import org.scalatest.funsuite.AnyFunSuite diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala index 4a9c48923083b6653116b105548b9aa321206cc0..d831a756fd622b8c2e1ca2b92ba7b4d7932e8fc7 100644 --- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala +++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala @@ -2,7 +2,7 @@ package lisa.settheory import lisa.kernel.fol.FOL.* import lisa.kernel.proof.RunningTheory -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} /** * Base trait for set theoretical axiom systems. diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala index 49624d35ac715b06f3c8006fdde0784a351e958a..944b63bf7fc1ba97ac60c1166e837fbfb3b50ea8 100644 --- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala +++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala @@ -1,7 +1,7 @@ package lisa.settheory import lisa.kernel.fol.FOL.* -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} /** * Axioms for the Tarski-Grothendieck theory (TG) diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala index b60d2f556e578474cb5d11884c1ba1b5a1c6c174..bdd4915f02efbe23177ef2e5f855e41e69f79315 100644 --- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala +++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala @@ -2,7 +2,7 @@ package lisa.settheory import lisa.kernel.fol.FOL.* import lisa.kernel.proof.RunningTheory -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} /** * Axioms for the Zermelo theory (Z) diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala index bd95ad4551a1c40f9cf94799a63cba71e1a93a06..e4379ea9bcfafc4695e1319d7b7ee22e347687a2 100644 --- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala +++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala @@ -1,7 +1,7 @@ package lisa.settheory import lisa.kernel.fol.FOL.* -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} /** * Axioms for the Zermelo-Fraenkel theory (ZF) diff --git a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala index c3e944f384a128592c3c19db01590b8c3a0c21b8..3de689b82444a090c144890ec5fa071d48f3c207 100644 --- a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala +++ b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala @@ -6,7 +6,7 @@ import lisa.kernel.proof.RunningTheory.* import lisa.kernel.proof.SCProof import lisa.kernel.proof.SCProofChecker import lisa.kernel.proof.SequentCalculus.* -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} import lisa.utils.Printer import org.scalatest.funsuite.AnyFunSuite diff --git a/lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala b/lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala index 1bf566e3b477295a18305539a7486eae43107baf..d62ef6adae16d4cc3cce902ade1685ee2cfd817b 100644 --- a/lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala +++ b/lisa-utils/src/test/scala/lisa/kernel/InvalidProofPathTests.scala @@ -4,7 +4,7 @@ import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof import lisa.kernel.proof.SequentCalculus.* import lisa.kernel.proof.* import lisa.test.ProofCheckerSuite -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} class InvalidProofPathTests extends ProofCheckerSuite { def checkPath(invalidProof: SCProof, expectedPath: Seq[Int]): Unit = { diff --git a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala index d00afd8968387ea163b9a40397d7d9cc756d3a96..c5ba765c5a6022df84aa9a99cf128055dfff78ec 100644 --- a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala +++ b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala @@ -6,7 +6,7 @@ import lisa.kernel.proof.RunningTheory.* import lisa.kernel.proof.SCProof import lisa.kernel.proof.SCProofChecker import lisa.kernel.proof.SequentCalculus.* -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} import lisa.utils.Printer import org.scalatest.funsuite.AnyFunSuite diff --git a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala index 4a989fa25d0b6d5bb6bdec5f1585ab99e0681f88..50212e1a7df0445b9ea44b1b940bfe1d80d40cd6 100644 --- a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala +++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala @@ -6,7 +6,7 @@ import lisa.kernel.proof.SCProofCheckerJudgement import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof import lisa.kernel.proof.SequentCalculus.Sequent import lisa.kernel.proof.SequentCalculus.isSameSequent -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} import lisa.utils.Printer import org.scalatest.funsuite.AnyFunSuite diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala b/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala index 151fdbb13bad568639c7cc65dd9d32dae8d45bb8..fe7678b850d0e741268c4bfecb1e3716574923c4 100644 --- a/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala +++ b/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala @@ -2,7 +2,7 @@ package lisa.test import lisa.kernel.fol.FOL.* import lisa.kernel.proof.RunningTheory -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} trait TestTheoryAxioms { final val p1 = ConstantPredicateLabel("p1", 1) diff --git a/src/main/scala/lisa/automation/kernel/ProofTactics.scala b/src/main/scala/lisa/automation/kernel/ProofTactics.scala index d90b8208ddd2b269f8ed2a17536ba0021505ecb1..43bc269543946a155ca4868df3cb7b17261115a3 100644 --- a/src/main/scala/lisa/automation/kernel/ProofTactics.scala +++ b/src/main/scala/lisa/automation/kernel/ProofTactics.scala @@ -3,7 +3,7 @@ package lisa.automation.kernel import lisa.kernel.fol.FOL.* import lisa.kernel.proof.SCProof import lisa.kernel.proof.SequentCalculus.* -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} import lisa.utils.Printer.* /** diff --git a/src/main/scala/lisa/proven/peano_example/Peano.scala b/src/main/scala/lisa/proven/peano_example/Peano.scala index 860cd3d6b040f722ea96dadc14abe4e27f3b071e..ff1020a893a915df7a711f1fc38d71ed7f484588 100644 --- a/src/main/scala/lisa/proven/peano_example/Peano.scala +++ b/src/main/scala/lisa/proven/peano_example/Peano.scala @@ -5,7 +5,7 @@ import lisa.kernel.fol.FOL.* import lisa.kernel.proof.RunningTheory import lisa.kernel.proof.SCProof import lisa.kernel.proof.SequentCalculus.* -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} import lisa.utils.Library import lisa.utils.Printer diff --git a/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala b/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala index 86fb94675dceb78a0eab75707fb2c8c309edc787..0200f11b8dbafaf4471045985a3a7772f7870642 100644 --- a/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala +++ b/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala @@ -2,7 +2,7 @@ package lisa.proven.peano_example import lisa.kernel.fol.FOL.* import lisa.kernel.proof.RunningTheory -import lisa.utils.Helpers.{_, given} +import lisa.utils.Helpers.{*, given} object PeanoArithmetics { final val (x, y, z) =