From 7121b9e4d2ed2cfd95ffcb45536fda3708f0e351 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Thu, 9 Jun 2022 16:29:13 +0200
Subject: [PATCH] refactoring
---
src/main/scala/Example.scala | 7 ++++---
.../scala/lisa/kernel/proof/Judgement.scala | 2 +-
.../lisa/settheory/SetTheoryDefinitions.scala | 2 +-
.../lisa/settheory/SetTheoryTGAxioms.scala | 2 +-
.../scala/lisa/settheory/SetTheoryZAxioms.scala | 2 +-
.../lisa/settheory/SetTheoryZFAxioms.scala | 2 +-
src/main/scala/proven/DSetTheory/Part1.scala | 2 +-
src/main/scala/proven/ElementsOfSetTheory.scala | 9 ++++++++-
src/main/scala/proven/tactics/Destructors.scala | 4 +++-
.../scala/proven/tactics/ProofTactics.scala | 3 ++-
.../tactics/SimplePropositionalSolver.scala | 3 ++-
.../{lisa => utilities}/KernelHelpers.scala | 4 ++--
.../{ => utilities}/tptp/KernelParser.scala | 17 ++++++-----------
.../{ => utilities}/tptp/ProblemGatherer.scala | 4 ++--
src/main/scala/utilities/tptp/package.scala | 9 +++++++++
.../lisa/kernel/EquivalenceCheckerTests.scala | 2 +-
src/test/scala/lisa/kernel/FolTests.scala | 2 +-
.../lisa/kernel/IncorrectProofsTests.scala | 2 +-
src/test/scala/lisa/kernel/ProofTests.scala | 2 +-
.../lisa/proven/ElementsOfSetTheoryTests.scala | 3 ++-
.../scala/lisa/proven/SimpleProverTests.scala | 6 +++---
src/test/scala/test/ProofCheckerSuite.scala | 5 +++--
22 files changed, 56 insertions(+), 38 deletions(-)
rename src/main/scala/{lisa => utilities}/KernelHelpers.scala (99%)
rename src/main/scala/{ => utilities}/tptp/KernelParser.scala (94%)
rename src/main/scala/{ => utilities}/tptp/ProblemGatherer.scala (89%)
create mode 100644 src/main/scala/utilities/tptp/package.scala
diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index 6d4eb4ce..8e7eb102 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -1,4 +1,7 @@
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
+import utilities.tptp.ProblemGatherer.*
+import utilities.tptp.KernelParser.*
+import utilities.tptp.*
import lisa.kernel.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
@@ -6,8 +9,6 @@ import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SCProofChecker.*
import lisa.kernel.proof.SequentCalculus.*
import proven.tactics.SimplePropositionalSolver.solveSequent
-import tptp.KernelParser.*
-import tptp.ProblemGatherer.getPRPproblems
/**
* Discover some of the elements of LISA to get started.
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
index 6d3abfb7..680d70b4 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -53,7 +53,7 @@ sealed abstract class RunningTheoryJudgement[J <: RunningTheory#Justification] {
def get: J = this match {
case ValidJustification(just) => just
case InvalidJustification(message, error) =>
- throw new InvalidJustificationException(message, error)
+ throw InvalidJustificationException(message, error)
}
}
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index a2f3b2b7..3f630ed2 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 utilities.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 c2bedfa3..12fcff5c 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 utilities.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 7c7a7d22..da11ebd9 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 utilities.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 e3648b7e..24271f81 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 utilities.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 b82f09ff..4a8b0fb2 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,5 +1,5 @@
package proven.DSetTheory
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
import lisa.kernel.Printer
import lisa.kernel.Printer.prettyFormula
import lisa.kernel.Printer.prettySCProof
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index 52934b10..11aaa022 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -1,10 +1,17 @@
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 utilities.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
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 36f53f3f..396c6caa 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -1,7 +1,9 @@
package proven.tactics
-import lisa.KernelHelpers.*
+import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.fol.FOL.*
+import utilities.KernelHelpers.*
+import proven.tactics.ProofTactics.hypothesis
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
import proven.tactics.ProofTactics.hypothesis
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index 191e77a1..bd90e0a7 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -1,10 +1,11 @@
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 utilities.KernelHelpers.{*, given}
+import lisa.kernel.Printer.*
import scala.collection.immutable.Set
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
index 50d87de5..87b85b60 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -1,11 +1,12 @@
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 utilities.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/lisa/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
similarity index 99%
rename from src/main/scala/lisa/KernelHelpers.scala
rename to src/main/scala/utilities/KernelHelpers.scala
index 90be4463..b55795ff 100644
--- a/src/main/scala/lisa/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -1,4 +1,4 @@
-package lisa
+package utilities
/**
* A helper file that provides various syntactic sugars for LISA.
@@ -9,8 +9,8 @@ package lisa
*/
object KernelHelpers {
- import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.fol.FOL.*
+ import lisa.kernel.proof.SequentCalculus.Sequent
/* Prefix syntax */
diff --git a/src/main/scala/tptp/KernelParser.scala b/src/main/scala/utilities/tptp/KernelParser.scala
similarity index 94%
rename from src/main/scala/tptp/KernelParser.scala
rename to src/main/scala/utilities/tptp/KernelParser.scala
index 149453e3..036242c5 100644
--- a/src/main/scala/tptp/KernelParser.scala
+++ b/src/main/scala/utilities/tptp/KernelParser.scala
@@ -1,12 +1,13 @@
-package tptp
+package utilities.tptp
import leo.datastructures.TPTP
import leo.datastructures.TPTP.CNF
import leo.datastructures.TPTP.FOF
+import utilities.tptp.*
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.kernel.proof.SequentCalculus as LK
+import utilities.KernelHelpers.*
import java.io.File
import scala.util.matching.Regex
@@ -15,12 +16,6 @@ import Parser.TPTPParseException
object KernelParser {
- case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
-
- case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedFormula])
-
- case class FileNotAcceptedException(msg: String, file: String) extends Exception(msg + " File: " + file)
-
private case class ProblemMetadata(file: String, domain: String, problem: String, status: String, spc: Seq[String])
/**
@@ -152,10 +147,10 @@ object KernelParser {
* @param problem a problem, containing a list of annotated formulas from a tptp file
* @return a sequent with axioms of the problem on the left, and the conjecture on the right
*/
- def problemToSequent(problem: Problem): SK.Sequent = {
+ def problemToSequent(problem: Problem): LK.Sequent = {
if (problem.spc.contains("CNF")) problem.formulas.map(_.formula) |- ()
else
- problem.formulas.foldLeft[SK.Sequent](() |- ())((s, f) =>
+ problem.formulas.foldLeft[LK.Sequent](() |- ())((s, f) =>
if (f._1 == "axiom") s +< f._3
else if (f._1 == "conjecture" && s.right.isEmpty) s +> f._3
else throw Exception("Can only agglomerate axioms and one conjecture into a sequents")
diff --git a/src/main/scala/tptp/ProblemGatherer.scala b/src/main/scala/utilities/tptp/ProblemGatherer.scala
similarity index 89%
rename from src/main/scala/tptp/ProblemGatherer.scala
rename to src/main/scala/utilities/tptp/ProblemGatherer.scala
index 41644e14..ae1df1fa 100644
--- a/src/main/scala/tptp/ProblemGatherer.scala
+++ b/src/main/scala/utilities/tptp/ProblemGatherer.scala
@@ -1,6 +1,6 @@
-package tptp
+package utilities.tptp
-import tptp.KernelParser._
+import KernelParser._
object ProblemGatherer {
diff --git a/src/main/scala/utilities/tptp/package.scala b/src/main/scala/utilities/tptp/package.scala
new file mode 100644
index 00000000..538a2f41
--- /dev/null
+++ b/src/main/scala/utilities/tptp/package.scala
@@ -0,0 +1,9 @@
+package utilities.tptp
+
+import lisa.kernel.fol.FOL as K
+
+case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
+
+case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedFormula])
+
+case class FileNotAcceptedException(msg: String, file: String) extends Exception(msg + " File: " + file)
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index f8ee2a8c..518ce3f9 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import lisa.KernelHelpers.*
+import utilities.KernelHelpers.*
import lisa.kernel.Printer
import lisa.kernel.fol.FOL
import lisa.kernel.fol.FOL.*
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index 8f02688c..615d58e1 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 9259274b..213336b6 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -1,7 +1,7 @@
package lisa.kernel
//import lisa.settheory.AxiomaticSetTheory.{emptySet, emptySetAxiom, pair, pairAxiom, useAxiom}
-import lisa.KernelHelpers.*
+import utilities.KernelHelpers.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index 07b5a3a0..b1324337 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index 98ade22d..fde50ed0 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -1,10 +1,11 @@
package proven
-import lisa.KernelHelpers.{_, given}
import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.fol.FOL.*
+import utilities.KernelHelpers.{*, given}
import lisa.kernel.proof.SequentCalculus.*
import lisa.settheory.AxiomaticSetTheory.*
import proven.ElementsOfSetTheory.*
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 9731249f..05bd4c4a 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,6 +1,6 @@
package proven
-import lisa.KernelHelpers.*
+import utilities.KernelHelpers.*
import lisa.kernel.Printer
import lisa.kernel.Printer.*
import lisa.kernel.fol.FOL.*
@@ -8,9 +8,9 @@ import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.PredicateLogic
import lisa.kernel.proof.SCProofChecker
import org.scalatest.funsuite.AnyFunSuite
+import utilities.tptp.ProblemGatherer.getPRPproblems
+import utilities.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 8a596186..08d91983 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -1,7 +1,5 @@
package test
-import lisa.KernelHelpers._
-import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
import lisa.kernel.Printer
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker._
@@ -9,6 +7,9 @@ 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 utilities.KernelHelpers._
+import utilities.KernelHelpers.given_Conversion_Boolean_List_String_Option
abstract class ProofCheckerSuite extends AnyFunSuite {
import lisa.kernel.fol.FOL.*
--
GitLab