From a3e9f5d4233ffecd9438487e70498920092aae32 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Thu, 9 Jun 2022 18:09:17 +0200
Subject: [PATCH] Run scalafix on all project files
---
src/main/scala/Example.scala | 5 ++--
src/main/scala/lisa/kernel/Printer.scala | 5 ++--
.../lisa/kernel/proof/RunningTheory.scala | 8 +++----
.../scala/lisa/kernel/proof/SCProof.scala | 2 +-
.../lisa/kernel/proof/SCProofChecker.scala | 2 +-
.../lisa/settheory/SetTheoryDefinitions.scala | 2 +-
.../lisa/settheory/SetTheoryTGAxioms.scala | 2 +-
.../lisa/settheory/SetTheoryZAxioms.scala | 2 +-
.../lisa/settheory/SetTheoryZFAxioms.scala | 2 +-
src/main/scala/proven/DSetTheory/Part1.scala | 24 ++++++++++---------
.../scala/proven/ElementsOfSetTheory.scala | 16 ++++++-------
.../scala/proven/tactics/Destructors.scala | 6 ++---
.../scala/proven/tactics/ProofTactics.scala | 6 ++---
.../tactics/SimplePropositionalSolver.scala | 5 ++--
src/main/scala/tptp/KernelParser.scala | 10 ++++----
.../lisa/kernel/EquivalenceCheckerTests.scala | 3 ++-
src/test/scala/lisa/kernel/FolTests.scala | 11 +++++----
src/test/scala/lisa/kernel/PrinterTest.scala | 3 +--
src/test/scala/lisa/kernel/ProofTests.scala | 11 +++++----
.../proven/ElementsOfSetTheoryTests.scala | 12 +++++-----
.../scala/lisa/proven/SimpleProverTests.scala | 11 +++++----
src/test/scala/test/ProofCheckerSuite.scala | 9 +++----
22 files changed, 84 insertions(+), 73 deletions(-)
diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index c66802c1..6d4eb4ce 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -1,9 +1,10 @@
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.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.kernel.proof.{SCProof, SCProofChecker}
import proven.tactics.SimplePropositionalSolver.solveSequent
import tptp.KernelParser.*
import tptp.ProblemGatherer.getPRPproblems
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 860d5b49..3bac6470 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -1,9 +1,10 @@
package lisa.kernel
import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofCheckerJudgement
import lisa.kernel.proof.SCProofCheckerJudgement.*
-import lisa.kernel.proof.{SCProof, SCProofCheckerJudgement}
+import lisa.kernel.proof.SequentCalculus.*
/**
* A set of methods to pretty-print kernel trees.
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 0b076bc2..c68e8993 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -1,13 +1,13 @@
package lisa.kernel.proof
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.kernel.proof.SCProofChecker.*
import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheoryJudgement.*
+import lisa.kernel.proof.SCProofChecker.*
+import lisa.kernel.proof.SequentCalculus.*
+import scala.collection.immutable.Set
import scala.collection.mutable.Map as mMap
import scala.collection.mutable.Set as mSet
-import scala.collection.immutable.Set
-import lisa.kernel.proof.RunningTheoryJudgement.*
/**
* This class describes the theory, i.e. the context and language, in which theorems are proven.
diff --git a/src/main/scala/lisa/kernel/proof/SCProof.scala b/src/main/scala/lisa/kernel/proof/SCProof.scala
index f5645e55..65c40f8d 100644
--- a/src/main/scala/lisa/kernel/proof/SCProof.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProof.scala
@@ -1,7 +1,7 @@
package lisa.kernel.proof
-import lisa.kernel.proof.SequentCalculus._
import lisa.kernel.proof.SCProofChecker._
+import lisa.kernel.proof.SequentCalculus._
/**
* A SCPRoof (for Sequent Calculus Proof) is a (dependant) proof. While technically a proof is an Directed Acyclic Graph,
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 51d92d6a..ad72abfe 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -2,8 +2,8 @@ package lisa.kernel.proof
import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.proof.SCProofCheckerJudgement.*
+import lisa.kernel.proof.SequentCalculus.*
object SCProofChecker {
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 38549206..337e67fe 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -1,8 +1,8 @@
package lisa.settheory
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.fol.FOL._
import lisa.kernel.proof.RunningTheory
-import lisa.KernelHelpers.{given, _}
/**
* Base trait for set theoretical axiom systems.
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index e5ba1881..c2bedfa3 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -1,6 +1,6 @@
package lisa.settheory
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.fol.FOL._
-import lisa.KernelHelpers.{given, _}
/**
* Axioms for the Tarski-Grothendieck theory (TG)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 7a9ff334..7c7a7d22 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -1,8 +1,8 @@
package lisa.settheory
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
-import lisa.KernelHelpers.{given, _}
/**
* Axioms for the Zermelo theory (Z)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 06f6aee9..e3648b7e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -1,7 +1,7 @@
package lisa.settheory
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.fol.FOL._
-import lisa.KernelHelpers.{given, _}
/**
* Axioms for the Zermelo-Fraenkel theory (ZF)
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index e04d1b98..b82f09ff 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,20 +1,22 @@
package proven.DSetTheory
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.Printer
-import lisa.kernel.Printer.{prettyFormula, prettySCProof}
+import lisa.kernel.Printer.prettyFormula
+import lisa.kernel.Printer.prettySCProof
import lisa.kernel.fol.FOL
-import proven.tactics.ProofTactics.*
-import proven.tactics.Destructors.*
-import lisa.settheory.AxiomaticSetTheory.*
-import proven.ElementsOfSetTheory.{oPair, orderedPairDefinition}
-
-import scala.collection.immutable.SortedSet
-import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.*
import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.AxiomaticSetTheory.*
+import proven.ElementsOfSetTheory.oPair
+import proven.ElementsOfSetTheory.orderedPairDefinition
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
import scala.collection.immutable
+import scala.collection.immutable.SortedSet
object Part1 {
val theory = AxiomaticSetTheory.runningSetTheory
def axiom(f: Formula): theory.Axiom = theory.getAxiom(f).get
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index 288cdbf5..52934b10 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -1,18 +1,18 @@
package proven
+import lisa.KernelHelpers.{_, given}
+import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
-import lisa.KernelHelpers.{*, given}
-import lisa.kernel.Printer
-import proven.tactics.ProofTactics.*
-import proven.tactics.Destructors.*
-import lisa.settheory.AxiomaticSetTheory.*
-
-import scala.collection.immutable.SortedSet
-import lisa.kernel.proof.{SCProof, SCProofChecker}
import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.AxiomaticSetTheory.*
import proven.ElementsOfSetTheory.theory
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
import scala.collection.immutable
+import scala.collection.immutable.SortedSet
/**
* Some proofs in set theory. See it as a proof of concept.
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 68277462..36f53f3f 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -1,10 +1,10 @@
package proven.tactics
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.kernel.fol.FOL.*
import lisa.KernelHelpers.*
-import proven.tactics.ProofTactics.hypothesis
+import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import proven.tactics.ProofTactics.hypothesis
object Destructors {
def destructRightOr(p: SCProof, a: Formula, b: Formula): SCProof = {
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index 8fe34fad..191e77a1 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -1,12 +1,12 @@
package proven.tactics
+import lisa.KernelHelpers.{_, given}
+import lisa.kernel.Printer.*
import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import lisa.KernelHelpers.{*, given}
-import lisa.kernel.Printer.*
import scala.collection.immutable.Set
-import lisa.kernel.proof.SCProof
/**
* SCProof tactics are a set of strategies that help the user write proofs in a more expressive way
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
index 7d45e9d7..50d87de5 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -1,10 +1,11 @@
package proven.tactics
+import lisa.KernelHelpers.*
import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
+
import scala.collection.mutable.Set as mSet
-import lisa.KernelHelpers.*
-import lisa.kernel.proof.SCProof
/**
* A simple but complete solver for propositional logic. Will not terminate for large problems
diff --git a/src/main/scala/tptp/KernelParser.scala b/src/main/scala/tptp/KernelParser.scala
index 83485b3d..149453e3 100644
--- a/src/main/scala/tptp/KernelParser.scala
+++ b/src/main/scala/tptp/KernelParser.scala
@@ -1,16 +1,18 @@
package tptp
-import leo.modules.input.TPTPParser as Parser
-import Parser.TPTPParseException
import leo.datastructures.TPTP
-import leo.datastructures.TPTP.{CNF, FOF}
+import leo.datastructures.TPTP.CNF
+import leo.datastructures.TPTP.FOF
+import leo.modules.input.TPTPParser as Parser
+import lisa.KernelHelpers.*
import lisa.kernel.fol.FOL as K
import lisa.kernel.proof.SequentCalculus as SK
-import lisa.KernelHelpers.*
import java.io.File
import scala.util.matching.Regex
+import Parser.TPTPParseException
+
object KernelParser {
case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index 722d2c1f..f8ee2a8c 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -7,7 +7,8 @@ import lisa.kernel.fol.FOL.*
import org.scalatest.funsuite.AnyFunSuite
import scala.collection.MapView
-import scala.collection.mutable.{ArrayBuffer, ListBuffer}
+import scala.collection.mutable.ArrayBuffer
+import scala.collection.mutable.ListBuffer
import scala.util.Random
class EquivalenceCheckerTests extends AnyFunSuite {
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index 27a3eede..8f02688c 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,13 +1,14 @@
package lisa.kernel
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.Printer
-import lisa.kernel.proof.RunningTheory
-import org.scalatest.funsuite.AnyFunSuite
-import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
-import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.*
+import org.scalatest.funsuite.AnyFunSuite
import scala.collection.immutable.SortedSet
import scala.util.Random
diff --git a/src/test/scala/lisa/kernel/PrinterTest.scala b/src/test/scala/lisa/kernel/PrinterTest.scala
index 23edf5a2..cf6a4899 100644
--- a/src/test/scala/lisa/kernel/PrinterTest.scala
+++ b/src/test/scala/lisa/kernel/PrinterTest.scala
@@ -1,8 +1,7 @@
package lisa.kernel
-import lisa.kernel.fol.FOL._
import lisa.kernel.Printer._
-
+import lisa.kernel.fol.FOL._
import org.scalatest.funsuite.AnyFunSuite
class PrinterTest extends AnyFunSuite {
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index 665f9575..07b5a3a0 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,13 +1,14 @@
package lisa.kernel
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.Printer
-import lisa.kernel.proof.RunningTheory
-import org.scalatest.funsuite.AnyFunSuite
-import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
-import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.*
+import org.scalatest.funsuite.AnyFunSuite
import scala.util.Random
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index 5786462d..98ade22d 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -1,15 +1,15 @@
package proven
+import lisa.KernelHelpers.{_, given}
import lisa.kernel.Printer
-import lisa.settheory.AxiomaticSetTheory.*
-import test.ProofCheckerSuite
-import proven.tactics.ProofTactics
+import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
-import proven.ElementsOfSetTheory.*
import lisa.kernel.proof.SequentCalculus.Sequent
-import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.{*, given}
import lisa.kernel.proof.SequentCalculus.*
+import lisa.settheory.AxiomaticSetTheory.*
+import proven.ElementsOfSetTheory.*
+import proven.tactics.ProofTactics
+import test.ProofCheckerSuite
class ElementsOfSetTheoryTests extends ProofCheckerSuite {
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 8f56fe7b..9731249f 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,15 +1,16 @@
package proven
-import lisa.kernel.Printer.*
-import lisa.kernel.proof.{RunningTheory, SCProofChecker}
-import lisa.kernel.fol.FOL.*
import lisa.KernelHelpers.*
import lisa.kernel.Printer
+import lisa.kernel.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 tptp.ProblemGatherer.getPRPproblems
-import tptp.KernelParser.*
import proven.tactics.SimplePropositionalSolver as SPS
+import tptp.KernelParser.*
+import tptp.ProblemGatherer.getPRPproblems
class SimpleProverTests extends AnyFunSuite {
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index d91d1fd9..8a596186 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -1,13 +1,14 @@
package test
+import lisa.KernelHelpers._
+import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
import lisa.kernel.Printer
-import lisa.kernel.proof.SequentCalculus.{Sequent, isSameSequent}
+import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker._
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.SequentCalculus.isSameSequent
import lisa.settheory.AxiomaticSetTheory
import org.scalatest.funsuite.AnyFunSuite
-import lisa.kernel.proof.SCProof
-import lisa.KernelHelpers._
-import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
abstract class ProofCheckerSuite extends AnyFunSuite {
import lisa.kernel.fol.FOL.*
--
GitLab