From 9f9f285a82db1c2e11fb949e7b5f56ba16fde84b Mon Sep 17 00:00:00 2001
From: Florian Cassayre <florian.cassayre@gmail.com>
Date: Mon, 13 Jun 2022 16:26:39 +0200
Subject: [PATCH] Complete re-organization into separate modules
---
build.sbt | 88 ++++++++++++++++---
.../src}/main/scala/Example.scala | 14 +--
.../lisa/kernel/fol/CommonDefinitions.scala | 0
.../lisa/kernel/fol/EquivalenceChecker.scala | 5 +-
.../src}/main/scala/lisa/kernel/fol/FOL.scala | 0
.../lisa/kernel/fol/FormulaDefinitions.scala | 0
.../kernel/fol/FormulaLabelDefinitions.scala | 0
.../scala/lisa/kernel/fol/Substitutions.scala | 10 ++-
.../lisa/kernel/fol/TermDefinitions.scala | 0
.../kernel/fol/TermLabelDefinitions.scala | 0
.../scala/lisa/kernel/proof/Judgement.scala | 8 +-
.../lisa/kernel/proof/RunningTheory.scala | 31 ++++---
.../scala/lisa/kernel/proof/SCProof.scala | 4 +-
.../lisa/kernel/proof/SCProofChecker.scala | 41 +++++----
.../lisa/kernel/proof/SequentCalculus.scala | 2 +-
.../lisa/settheory/AxiomaticSetTheory.scala | 0
.../lisa/settheory/SetTheoryDefinitions.scala | 2 +-
.../lisa/settheory/SetTheoryTGAxioms.scala | 2 +-
.../lisa/settheory/SetTheoryZAxioms.scala | 2 +-
.../lisa/settheory/SetTheoryZFAxioms.scala | 2 +-
.../main/scala/lisa}/tptp/KernelParser.scala | 6 +-
.../scala/lisa}/tptp/ProblemGatherer.scala | 4 +-
.../src/main/scala/lisa}/tptp/package.scala | 2 +-
.../src/main/scala/lisa/utils}/Helpers.scala | 4 +-
.../scala/lisa/utils}/KernelHelpers.scala | 2 +-
.../src/main/scala/lisa/utils}/Library.scala | 4 +-
.../src/main/scala/lisa/utils}/Printer.scala | 2 +-
.../scala/lisa/utils}/TheoriesHelpers.scala | 4 +-
.../lisa/kernel/EquivalenceCheckerTests.scala | 4 +-
.../test/scala/lisa/kernel/FolTests.scala | 4 +-
.../lisa/kernel/IncorrectProofsTests.scala | 8 +-
.../test/scala/lisa/kernel/ProofTests.scala | 4 +-
.../scala/lisa}/test/ProofCheckerSuite.scala | 9 +-
.../test/scala/lisa/utils}/PrinterTest.scala | 4 +-
src/main/scala/{ => lisa}/proven/Main.scala | 4 +-
.../{ => lisa}/proven/SetTheoryLibrary.scala | 4 +-
.../proven/mathematics/Mapping.scala | 8 +-
.../proven/mathematics/SetTheory.scala | 8 +-
.../proven/tactics/Destructors.scala | 6 +-
.../proven/tactics/ProofTactics.scala | 6 +-
.../tactics/SimplePropositionalSolver.scala | 4 +-
.../lisa/proven/InitialProofsTests.scala | 10 +--
.../scala/lisa/proven/SimpleProverTests.scala | 12 +--
43 files changed, 196 insertions(+), 138 deletions(-)
rename {src => lisa-examples/src}/main/scala/Example.scala (95%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/CommonDefinitions.scala (100%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/EquivalenceChecker.scala (99%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/FOL.scala (100%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/FormulaDefinitions.scala (100%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala (100%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/Substitutions.scala (98%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/TermDefinitions.scala (100%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala (100%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/proof/Judgement.scala (94%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/proof/RunningTheory.scala (94%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/proof/SCProof.scala (99%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/proof/SCProofChecker.scala (94%)
rename {src => lisa-kernel/src}/main/scala/lisa/kernel/proof/SequentCalculus.scala (99%)
rename {src => lisa-theories/src}/main/scala/lisa/settheory/AxiomaticSetTheory.scala (100%)
rename {src => lisa-theories/src}/main/scala/lisa/settheory/SetTheoryDefinitions.scala (97%)
rename {src => lisa-theories/src}/main/scala/lisa/settheory/SetTheoryTGAxioms.scala (95%)
rename {src => lisa-theories/src}/main/scala/lisa/settheory/SetTheoryZAxioms.scala (97%)
rename {src => lisa-theories/src}/main/scala/lisa/settheory/SetTheoryZFAxioms.scala (95%)
rename {src/main/scala/utilities => lisa-tptp/src/main/scala/lisa}/tptp/KernelParser.scala (99%)
rename {src/main/scala/utilities => lisa-tptp/src/main/scala/lisa}/tptp/ProblemGatherer.scala (87%)
rename {src/main/scala/utilities => lisa-tptp/src/main/scala/lisa}/tptp/package.scala (93%)
rename {src/main/scala/utilities => lisa-utils/src/main/scala/lisa/utils}/Helpers.scala (71%)
rename {src/main/scala/utilities => lisa-utils/src/main/scala/lisa/utils}/KernelHelpers.scala (99%)
rename {src/main/scala/utilities => lisa-utils/src/main/scala/lisa/utils}/Library.scala (99%)
rename {src/main/scala/utilities => lisa-utils/src/main/scala/lisa/utils}/Printer.scala (99%)
rename {src/main/scala/utilities => lisa-utils/src/main/scala/lisa/utils}/TheoriesHelpers.scala (99%)
rename {src => lisa-utils/src}/test/scala/lisa/kernel/EquivalenceCheckerTests.scala (99%)
rename {src => lisa-utils/src}/test/scala/lisa/kernel/FolTests.scala (98%)
rename {src => lisa-utils/src}/test/scala/lisa/kernel/IncorrectProofsTests.scala (92%)
rename {src => lisa-utils/src}/test/scala/lisa/kernel/ProofTests.scala (97%)
rename {src/test/scala => lisa-utils/src/test/scala/lisa}/test/ProofCheckerSuite.scala (90%)
rename {src/test/scala/lisa/kernel => lisa-utils/src/test/scala/lisa/utils}/PrinterTest.scala (98%)
rename src/main/scala/{ => lisa}/proven/Main.scala (89%)
rename src/main/scala/{ => lisa}/proven/SetTheoryLibrary.scala (69%)
rename src/main/scala/{ => lisa}/proven/mathematics/Mapping.scala (99%)
rename src/main/scala/{ => lisa}/proven/mathematics/SetTheory.scala (99%)
rename src/main/scala/{ => lisa}/proven/tactics/Destructors.scala (92%)
rename src/main/scala/{ => lisa}/proven/tactics/ProofTactics.scala (98%)
rename src/main/scala/{ => lisa}/proven/tactics/SimplePropositionalSolver.scala (99%)
diff --git a/build.sbt b/build.sbt
index 1699b485..b82c7792 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,20 +1,80 @@
-name := "lisa"
-organization := "ch.epfl.lara"
-licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html"))
+inThisBuild(Def.settings(
+ organization := "ch.epfl.lara",
+ organizationName := "LARA",
+ 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"),
+))
-version := "0.1"
+val scala2 = "2.13.8"
+val scala3 = "3.1.3"
-scalaVersion := "3.1.3"
+lazy val commonSettings2 = Seq(
+ scalaVersion := scala2,
+)
+lazy val commonSettings3 = Seq(
+ scalaVersion := scala3,
+ scalacOptions ++= Seq(
+ "-feature",
+ "-deprecation",
+ //"-source:future",
+ "-language:implicitConversions",
+ //"-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",
+)
+
+lazy val root = Project(
+ id = "lisa-core",
+ base = file("."),
+)
+ .settings(commonSettings3)
+ .settings(
+ version := "0.1",
+ )
+ .dependsOn(kernel, utils, theories, tptp) // Everything but `examples`
+
+lazy val kernel = Project(
+ id = "lisa-kernel",
+ base = file("lisa-kernel"),
+)
+ .settings(commonSettings2)
+ .settings(
+ crossScalaVersions := Seq(scala3)
+ )
-scalacOptions ++= Seq("-deprecation", "-feature")
-scalacOptions ++= Seq(
- "-language:implicitConversions"
+lazy val utils = Project(
+ id = "lisa-utils",
+ base = file("lisa-utils"),
)
+ .settings(commonSettings3)
+ .dependsOn(kernel)
-libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test"
-libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4"
-Test / parallelExecution := false
+lazy val theories = Project(
+ id = "lisa-theories",
+ base = file("lisa-theories"),
+)
+ .settings(commonSettings3)
+ .dependsOn(utils)
-ThisBuild / semanticdbEnabled := true
-ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
-ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
+lazy val tptp = Project(
+ id = "lisa-tptp",
+ base = file("lisa-tptp"),
+)
+ .settings(commonSettings3)
+ .settings(
+ libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4",
+ )
+ .dependsOn(utils)
+
+lazy val examples = Project(
+ id = "lisa-examples",
+ base = file("lisa-examples"),
+)
+ .settings(commonSettings3)
+ .dependsOn(root)
diff --git a/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
similarity index 95%
rename from src/main/scala/Example.scala
rename to lisa-examples/src/main/scala/Example.scala
index dae950af..228994a7 100644
--- a/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 proven.tactics.SimplePropositionalSolver.solveSequent
-import utilities.Helpers.{_, given}
-import utilities.Printer.*
-import utilities.tptp.KernelParser.*
-import utilities.tptp.ProblemGatherer.*
-import utilities.tptp.*
+import lisa.proven.tactics.SimplePropositionalSolver.solveSequent
+import lisa.utils.Helpers.{_, given}
+import lisa.tptp.KernelParser.*
+import lisa.tptp.ProblemGatherer.*
+import lisa.tptp.*
/**
* Discover some of the elements of LISA to get started.
@@ -26,7 +26,7 @@ object Example {
* The last two lines don't need to be changed.
*/
def proofExample(): Unit = {
- object Ex extends proven.Main {
+ object Ex extends lisa.proven.Main {
THEOREM("fixedPointDoubleApplication") of "" PROOF {
steps(
???,
diff --git a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
similarity index 99%
rename from src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index 075e2054..def0f7fa 100644
--- a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -230,12 +230,13 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
case SimplePredicate(id, args) =>
val lab = "pred_" + id.id + "_" + id.arity
if (id == equality) {
- if (codesOfTerm(args(0)) == codesOfTerm(args(1)))
+ if (codesOfTerm(args(0)) == codesOfTerm(args(1))) {
phi.normalForm = Some(NLiteral(true))
parent.normalForm = Some(NLiteral(false))
- else
+ } else {
phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, (args map codesOfTerm).sorted))))
parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+ }
} else {
phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, args map codesOfTerm))))
parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
diff --git a/src/main/scala/lisa/kernel/fol/FOL.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FOL.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/FOL.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/FOL.scala
diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/Substitutions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
similarity index 98%
rename from src/main/scala/lisa/kernel/fol/Substitutions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
index e89e6079..0f2fe1f4 100644
--- a/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -66,9 +66,10 @@ trait Substitutions extends FormulaDefinitions {
t match {
case VariableTerm(_) => t
case FunctionTerm(label, args) =>
- label match
+ label match {
case label: SchematicFunctionLabel if label.arity == 0 => m.getOrElse(label, t)
case label => FunctionTerm(label, args.map(instantiateNullaryFunctionSchemas(_, m)))
+ }
}
}
@@ -87,13 +88,13 @@ trait Substitutions extends FormulaDefinitions {
case VariableTerm(_) => t
case FunctionTerm(label, args) =>
val newArgs = args.map(instantiateFunctionSchemas(_, m))
- label match
+ label match {
case label: ConstantFunctionLabel => FunctionTerm(label, newArgs)
case label: SchematicFunctionLabel =>
if (m.contains(label))
m(label)(newArgs) // = instantiateNullaryFunctionSchemas(m(label).body, (m(label).vars zip newArgs).toMap)
else FunctionTerm(label, newArgs)
-
+ }
}
}
@@ -160,9 +161,10 @@ trait Substitutions extends FormulaDefinitions {
require(m.forall { case (symbol, LambdaTermFormula(arguments, body)) => arguments.length == symbol.arity })
phi match {
case PredicateFormula(label, args) =>
- label match
+ label match {
case label: SchematicPredicateLabel if m.contains(label) => m(label)(args)
case label => phi
+ }
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchemas(_, m)))
case BinderFormula(label, bound, inner) =>
val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet
diff --git a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/TermDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/Judgement.scala
similarity index 94%
rename from src/main/scala/lisa/kernel/proof/Judgement.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/Judgement.scala
index e6fdb2f0..71374b9d 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -7,7 +7,7 @@ import lisa.kernel.proof.RunningTheory
* Typically, see [[SCProofChecker.checkSingleSCStep]] and [[SCProofChecker.checkSCProof]].
*/
sealed abstract class SCProofCheckerJudgement {
- import SCProofCheckerJudgement.*
+ import SCProofCheckerJudgement._
val proof: SCProof
/**
@@ -40,7 +40,7 @@ object SCProofCheckerJudgement {
* The judgement (or verdict) of a running theory.
*/
sealed abstract class RunningTheoryJudgement[+J <: RunningTheory#Justification] {
- import RunningTheoryJudgement.*
+ import RunningTheoryJudgement._
/**
* Whether this judgement is positive -- the justification could be imported into the running theory;
@@ -48,8 +48,8 @@ sealed abstract class RunningTheoryJudgement[+J <: RunningTheory#Justification]
* @return An instance of either [[ValidJustification]] or [[InvalidJustification]]
*/
def isValid: Boolean = this match {
- case _: ValidJustification[?] => true
- case _: InvalidJustification[?] => false
+ case _: ValidJustification[_] => true
+ case _: InvalidJustification[_] => false
}
def get: J = this match {
case ValidJustification(just) => just
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
similarity index 94%
rename from src/main/scala/lisa/kernel/proof/RunningTheory.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index ec979c1b..0a94eaeb 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -1,13 +1,13 @@
package lisa.kernel.proof
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.RunningTheoryJudgement.*
-import lisa.kernel.proof.SCProofChecker.*
-import lisa.kernel.proof.SequentCalculus.*
+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.mutable.{Map => mMap}
+import scala.collection.mutable.{Set => mSet}
/**
* This class describes the theory, i.e. the context and language, in which theorems are proven.
@@ -72,9 +72,10 @@ class RunningTheory {
* Check if a label is a symbol of the theory
*/
- def isSymbol(label: ConstantLabel): Boolean = label match
+ def isSymbol(label: ConstantLabel): Boolean = label match {
case c: ConstantFunctionLabel => funDefinitions.contains(c)
case c: ConstantPredicateLabel => predDefinitions.contains(c)
+ }
def isAvailable(label: ConstantLabel): Boolean = !knownSymbols.contains(label.id)
@@ -94,7 +95,7 @@ class RunningTheory {
private def proofToTheorem(name: String, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] =
if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
- if (belongsToTheory(proof.conclusion))
+ if (belongsToTheory(proof.conclusion)) {
val r = SCProofChecker.checkSCProof(proof)
r match {
case SCProofCheckerJudgement.SCValidProof(_) =>
@@ -104,6 +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("Not all imports of the proof are correctly justified.", None)
@@ -120,12 +122,12 @@ class RunningTheory {
val LambdaTermFormula(vars, body) = expression
if (belongsToTheory(body))
if (isAvailable(label))
- if (body.freeVariables.isEmpty && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty)
+ if (body.freeVariables.isEmpty && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty) {
val newDef = PredicateDefinition(label, expression)
predDefinitions.update(label, Some(newDef))
knownSymbols.update(label.id, label)
RunningTheoryJudgement.ValidJustification(newDef)
- else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
+ } else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
else InvalidJustification("The specified symbol id is already part of the theory and can't be redefined.", 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)
}
@@ -156,7 +158,7 @@ class RunningTheory {
if (belongsToTheory(body))
if (isAvailable(label))
if (body.freeVariables.subsetOf(Set(out)) && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty)
- if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
+ if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j))))) {
val r = SCProofChecker.checkSCProof(proof)
r match {
case SCProofCheckerJudgement.SCValidProof(_) =>
@@ -173,7 +175,7 @@ class RunningTheory {
}
case r @ SCProofCheckerJudgement.SCInvalidProof(_, path, message) => InvalidJustification("The given proof is incorrect: " + message, Some(r))
}
- else InvalidJustification("Not all imports of the proof are correctly justified.", None)
+ } else InvalidJustification("Not all imports of the proof are correctly justified.", None)
else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
else InvalidJustification("The specified symbol id is already part of the theory and can't be redefined.", 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)
@@ -277,9 +279,10 @@ class RunningTheory {
def addSymbol(s: ConstantLabel): Unit = {
if (isAvailable(s)) {
knownSymbols.update(s.id, s)
- s match
+ s match {
case c: ConstantFunctionLabel => funDefinitions.update(c, None)
case c: ConstantPredicateLabel => predDefinitions.update(c, None)
+ }
} else {}
}
@@ -327,5 +330,5 @@ object RunningTheory {
/**
* An empty theory suitable to reason about first order logic.
*/
- def PredicateLogic: RunningTheory = RunningTheory()
+ def PredicateLogic: RunningTheory = new RunningTheory()
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProof.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala
similarity index 99%
rename from src/main/scala/lisa/kernel/proof/SCProof.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala
index 244c795e..0892ef5d 100644
--- a/src/main/scala/lisa/kernel/proof/SCProof.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala
@@ -38,11 +38,11 @@ case class SCProof(steps: IndexedSeq[SCProofStep], imports: IndexedSeq[Sequent]
if (i >= 0)
if (i >= steps.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the steps Seq")
else steps(i).bot
- else
+ else {
val i2 = -(i + 1)
if (i2 >= imports.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the imports Seq")
else imports(i2)
-
+ }
}
/**
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
similarity index 94%
rename from src/main/scala/lisa/kernel/proof/SCProofChecker.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 1ae79196..34cf960d 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -1,9 +1,8 @@
package lisa.kernel.proof
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProofCheckerJudgement.*
-import lisa.kernel.proof.SequentCalculus.*
-import utilities.Printer
+import lisa.kernel.fol.FOL._
+import lisa.kernel.proof.SCProofCheckerJudgement._
+import lisa.kernel.proof.SequentCalculus._
object SCProofChecker {
@@ -73,28 +72,28 @@ object SCProofChecker {
* Γ, φ∧ψ |- Δ Γ, φ∧ψ |- Δ
*/
case LeftAnd(b, t1, phi, psi) =>
- if (isSameSet(ref(t1).right, b.right))
+ if (isSameSet(ref(t1).right, b.right)) {
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.")
- else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion must be the same.")
+ } else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- Δ Σ, ψ |- Π
* ------------------------
* Γ, Σ, φ∨ψ |- Δ, Π
*/
case LeftOr(b, t, disjuncts) =>
- if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)))
+ if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _))) {
val phiOrPsi = ConnectorFormula(Or, disjuncts)
if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
- else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+ } else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
/*
* Γ |- φ, Δ Σ, ψ |- Π
* ------------------------
@@ -119,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.")
@@ -202,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.")
@@ -349,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
@@ -367,13 +366,13 @@ object SCProofChecker {
*/
case RightSubstEq(b, t1, equals, lambdaPhi) =>
val sEqT_es = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
- if (isSameSet(ref(t1).left ++ sEqT_es, b.left))
+ if (isSameSet(ref(t1).left ++ sEqT_es, b.left)) {
val (s_es, t_es) = equals.unzip
val phi_s_for_f = lambdaPhi(s_es)
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
@@ -382,7 +381,7 @@ object SCProofChecker {
Nil,
s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ(s_) φ(t_), but it isn't the case."
)
- else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
+ } else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
/*
* Γ, φ(ψ_) |- Δ
* ---------------------
@@ -464,7 +463,7 @@ object SCProofChecker {
case SCSubproof(sp, premises, _) =>
if (premises.size == sp.imports.size) {
- val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)))
+ val invalid = premises.zipWithIndex.find { case (no, p) => !isSameSequent(ref(no), sp.imports(p)) }
if (invalid.isEmpty) {
checkSCProof(sp)
} else
@@ -489,12 +488,12 @@ object SCProofChecker {
*/
def checkSCProof(proof: SCProof): SCProofCheckerJudgement = {
val possibleError = proof.steps.view.zipWithIndex
- .map((step, no) =>
+ .map { case (step, no) =>
checkSingleSCStep(no, step, (i: Int) => proof.getSequent(i), Some(proof.imports.size)) match {
case SCInvalidProof(_, path, message) => SCInvalidProof(proof, no +: path, message)
case SCValidProof(_) => SCValidProof(proof)
}
- )
+ }
.find(j => !j.isValid)
if (possibleError.isEmpty) SCValidProof(proof)
else possibleError.get
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
similarity index 99%
rename from src/main/scala/lisa/kernel/proof/SequentCalculus.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index b0209090..15d677b9 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -1,6 +1,6 @@
package lisa.kernel.proof
-import lisa.kernel.fol.FOL.*
+import lisa.kernel.fol.FOL._
import scala.collection.immutable.Set
diff --git a/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala b/lisa-theories/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
similarity index 100%
rename from src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
rename to lisa-theories/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
similarity index 97%
rename from src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 8ecbc1f4..531076bd 100644
--- a/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 utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
/**
* Base trait for set theoretical axiom systems.
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
similarity index 95%
rename from src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index ec50a161..72e9bbb4 100644
--- a/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 utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
/**
* Axioms for the Tarski-Grothendieck theory (TG)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
similarity index 97%
rename from src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 4d1dcbad..f38aa7b1 100644
--- a/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 utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
/**
* Axioms for the Zermelo theory (Z)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
similarity index 95%
rename from src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 4cea73f7..fd0d2b67 100644
--- a/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 utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
/**
* Axioms for the Zermelo-Fraenkel theory (ZF)
diff --git a/src/main/scala/utilities/tptp/KernelParser.scala b/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
similarity index 99%
rename from src/main/scala/utilities/tptp/KernelParser.scala
rename to lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
index 215e85d7..df98eeac 100644
--- a/src/main/scala/utilities/tptp/KernelParser.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
@@ -1,4 +1,4 @@
-package utilities.tptp
+package lisa.tptp
import leo.datastructures.TPTP
import leo.datastructures.TPTP.CNF
@@ -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 utilities.Helpers.*
-import utilities.tptp.*
+import lisa.utils.Helpers.*
+import lisa.tptp.*
import java.io.File
import scala.util.matching.Regex
diff --git a/src/main/scala/utilities/tptp/ProblemGatherer.scala b/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
similarity index 87%
rename from src/main/scala/utilities/tptp/ProblemGatherer.scala
rename to lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
index ae1df1fa..8c1278c8 100644
--- a/src/main/scala/utilities/tptp/ProblemGatherer.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
@@ -1,6 +1,6 @@
-package utilities.tptp
+package lisa.tptp
-import KernelParser._
+import lisa.tptp.KernelParser._
object ProblemGatherer {
diff --git a/src/main/scala/utilities/tptp/package.scala b/lisa-tptp/src/main/scala/lisa/tptp/package.scala
similarity index 93%
rename from src/main/scala/utilities/tptp/package.scala
rename to lisa-tptp/src/main/scala/lisa/tptp/package.scala
index 538a2f41..b59b6938 100644
--- a/src/main/scala/utilities/tptp/package.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/package.scala
@@ -1,4 +1,4 @@
-package utilities.tptp
+package lisa.tptp
import lisa.kernel.fol.FOL as K
diff --git a/src/main/scala/utilities/Helpers.scala b/lisa-utils/src/main/scala/lisa/utils/Helpers.scala
similarity index 71%
rename from src/main/scala/utilities/Helpers.scala
rename to lisa-utils/src/main/scala/lisa/utils/Helpers.scala
index a6964731..0b8f8241 100644
--- a/src/main/scala/utilities/Helpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Helpers.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
/**
* A helper file that provides various syntactic sugars for LISA's FOL and proofs.
@@ -7,4 +7,4 @@ package utilities
* import utilities.Helpers.*
* </pre>
*/
-object Helpers extends TheoriesHelpers {}
+object Helpers extends TheoriesHelpers
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
similarity index 99%
rename from src/main/scala/utilities/KernelHelpers.scala
rename to lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 5dd3793c..6b378f9f 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheoryJudgement
diff --git a/src/main/scala/utilities/Library.scala b/lisa-utils/src/main/scala/lisa/utils/Library.scala
similarity index 99%
rename from src/main/scala/utilities/Library.scala
rename to lisa-utils/src/main/scala/lisa/utils/Library.scala
index 18a5fdad..c882e680 100644
--- a/src/main/scala/utilities/Library.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Library.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
import lisa.kernel.proof.RunningTheory
@@ -13,7 +13,7 @@ abstract class Library(val theory: RunningTheory) {
export lisa.kernel.proof.SequentCalculus.*
export lisa.kernel.proof.SCProof as Proof
export theory.{Justification, Theorem, Definition, Axiom, PredicateDefinition, FunctionDefinition}
- export Helpers.{*, given}
+ export lisa.utils.Helpers.{*, given}
import lisa.kernel.proof.RunningTheoryJudgement as Judgement
/**
diff --git a/src/main/scala/utilities/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
similarity index 99%
rename from src/main/scala/utilities/Printer.scala
rename to lisa-utils/src/main/scala/lisa/utils/Printer.scala
index c65ae1e7..c19f1266 100644
--- a/src/main/scala/utilities/Printer.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
similarity index 99%
rename from src/main/scala/utilities/TheoriesHelpers.scala
rename to lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
index 6c487530..265bfd7f 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
@@ -1,10 +1,10 @@
-package utilities
+package lisa.utils
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.proof.*
-import utilities.Printer
+import lisa.utils.Printer
/**
* A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
similarity index 99%
rename from src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index c499619e..fe309785 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -1,10 +1,10 @@
package lisa.kernel
-import utilities.Printer
+import lisa.utils.Printer
import lisa.kernel.fol.FOL
import lisa.kernel.fol.FOL.*
import org.scalatest.funsuite.AnyFunSuite
-import utilities.Helpers.*
+import lisa.utils.Helpers.*
import scala.collection.MapView
import scala.collection.mutable.ArrayBuffer
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
similarity index 98%
rename from src/test/scala/lisa/kernel/FolTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
index 42e6caed..f4b12ded 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import utilities.Printer
+import lisa.utils.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +8,7 @@ import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
import org.scalatest.funsuite.AnyFunSuite
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
import scala.collection.immutable.SortedSet
import scala.util.Random
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
similarity index 92%
rename from src/test/scala/lisa/kernel/IncorrectProofsTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 3d7aa18b..786e63ad 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -1,11 +1,10 @@
package lisa.kernel
-//import lisa.settheory.AxiomaticSetTheory.{emptySet, emptySetAxiom, pair, pairAxiom, useAxiom}
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import test.ProofCheckerSuite
-import utilities.Helpers.*
+import lisa.test.ProofCheckerSuite
+import lisa.utils.Helpers.*
import scala.collection.immutable.SortedSet
import scala.language.implicitConversions
@@ -23,9 +22,6 @@ class IncorrectProofsTests extends ProofCheckerSuite {
val g = PredicateFormula(gl, Seq.empty)
val h = PredicateFormula(hl, Seq.empty)
- val emptySetAxiom = lisa.settheory.AxiomaticSetTheory.emptySetAxiom
- val pairAxiom = lisa.settheory.AxiomaticSetTheory.pairAxiom
-
val incorrectProofs: Seq[SCProof] = List(
SCProof(
Hypothesis(emptySeq +< (x === x) +> (x === x), x === x),
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
similarity index 97%
rename from src/test/scala/lisa/kernel/ProofTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
index d5704b08..85f9210f 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import utilities.Printer
+import lisa.utils.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +8,7 @@ import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
import org.scalatest.funsuite.AnyFunSuite
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
import scala.util.Random
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
similarity index 90%
rename from src/test/scala/test/ProofCheckerSuite.scala
rename to lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
index caaee39f..dcb4fa26 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
@@ -1,14 +1,12 @@
-package test
+package lisa.test
-import utilities.Printer
+import lisa.utils.Printer
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 utilities.Helpers._
-import utilities.Helpers.given_Conversion_Boolean_List_String_Option
+import lisa.utils.Helpers.{_, given}
abstract class ProofCheckerSuite extends AnyFunSuite {
import lisa.kernel.fol.FOL.*
@@ -37,7 +35,6 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
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))
- val axioms = AxiomaticSetTheory.axioms
def checkProof(proof: SCProof): Unit = {
val judgement = checkSCProof(proof)
println(Printer.prettySCProof(judgement))
diff --git a/src/test/scala/lisa/kernel/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
similarity index 98%
rename from src/test/scala/lisa/kernel/PrinterTest.scala
rename to lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 67e91f29..e2675436 100644
--- a/src/test/scala/lisa/kernel/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -1,6 +1,6 @@
-package lisa.kernel
+package lisa.utils
-import utilities.Printer._
+import lisa.utils.Printer._
import lisa.kernel.fol.FOL._
import org.scalatest.funsuite.AnyFunSuite
diff --git a/src/main/scala/proven/Main.scala b/src/main/scala/lisa/proven/Main.scala
similarity index 89%
rename from src/main/scala/proven/Main.scala
rename to src/main/scala/lisa/proven/Main.scala
index 7ee72a6e..e69a7102 100644
--- a/src/main/scala/proven/Main.scala
+++ b/src/main/scala/lisa/proven/Main.scala
@@ -1,10 +1,10 @@
-package proven
+package lisa.proven
/**
* The parent trait of all theory files containing mathematical development
*/
trait Main {
- export proven.SetTheoryLibrary.{*, given}
+ export lisa.proven.SetTheoryLibrary.{*, given}
private val realOutput: String => Unit = println
private var outString: List[String] = List()
diff --git a/src/main/scala/proven/SetTheoryLibrary.scala b/src/main/scala/lisa/proven/SetTheoryLibrary.scala
similarity index 69%
rename from src/main/scala/proven/SetTheoryLibrary.scala
rename to src/main/scala/lisa/proven/SetTheoryLibrary.scala
index fd9e5250..8045393e 100644
--- a/src/main/scala/proven/SetTheoryLibrary.scala
+++ b/src/main/scala/lisa/proven/SetTheoryLibrary.scala
@@ -1,9 +1,9 @@
-package proven
+package lisa.proven
/**
* Specific implementation of [[utilities.Library]] for Set Theory, with a RunningTheory that is supposed to be used by the standard library.
*/
-object SetTheoryLibrary extends utilities.Library(lisa.settheory.AxiomaticSetTheory.runningSetTheory) {
+object SetTheoryLibrary extends lisa.utils.Library(lisa.settheory.AxiomaticSetTheory.runningSetTheory) {
val AxiomaticSetTheory: lisa.settheory.AxiomaticSetTheory.type = lisa.settheory.AxiomaticSetTheory
export AxiomaticSetTheory.*
diff --git a/src/main/scala/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
similarity index 99%
rename from src/main/scala/proven/mathematics/Mapping.scala
rename to src/main/scala/lisa/proven/mathematics/Mapping.scala
index ec687340..7267e0c7 100644
--- a/src/main/scala/proven/mathematics/Mapping.scala
+++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala
@@ -1,7 +1,7 @@
-package proven.mathematics
+package lisa.proven.mathematics
-import proven.tactics.Destructors.*
-import proven.tactics.ProofTactics.*
+import lisa.proven.tactics.Destructors.*
+import lisa.proven.tactics.ProofTactics.*
import SetTheory.*
@@ -9,7 +9,7 @@ import SetTheory.*
* This file contains theorem related to the replacement schema, i.e. how to "map" a set through a functional symbol.
* Leads to the definition of the cartesian product.
*/
-object Mapping extends proven.Main {
+object Mapping extends lisa.proven.Main {
THEOREM("functionalMapping") of
"∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
diff --git a/src/main/scala/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
similarity index 99%
rename from src/main/scala/proven/mathematics/SetTheory.scala
rename to src/main/scala/lisa/proven/mathematics/SetTheory.scala
index add21cfe..22822eb7 100644
--- a/src/main/scala/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -1,12 +1,12 @@
-package proven.mathematics
+package lisa.proven.mathematics
-import proven.tactics.Destructors.*
-import proven.tactics.ProofTactics.*
+import lisa.proven.tactics.Destructors.*
+import lisa.proven.tactics.ProofTactics.*
/**
* An embryo of mathematical development, containing a few example theorems and the definition of the ordered pair.
*/
-object SetTheory extends proven.Main {
+object SetTheory extends lisa.proven.Main {
THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF {
val y = SchematicFunctionLabel("y", 0)
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/lisa/proven/tactics/Destructors.scala
similarity index 92%
rename from src/main/scala/proven/tactics/Destructors.scala
rename to src/main/scala/lisa/proven/tactics/Destructors.scala
index 39f2c6cd..f7b978dd 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/lisa/proven/tactics/Destructors.scala
@@ -1,11 +1,11 @@
-package proven.tactics
+package lisa.proven.tactics
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.proof.SequentCalculus.*
-import proven.tactics.ProofTactics.hypothesis
-import utilities.Helpers.*
+import lisa.proven.tactics.ProofTactics.hypothesis
+import lisa.utils.Helpers.*
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/lisa/proven/tactics/ProofTactics.scala
similarity index 98%
rename from src/main/scala/proven/tactics/ProofTactics.scala
rename to src/main/scala/lisa/proven/tactics/ProofTactics.scala
index dde13d44..3567982a 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/lisa/proven/tactics/ProofTactics.scala
@@ -1,10 +1,10 @@
-package proven.tactics
+package lisa.proven.tactics
+import lisa.utils.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import utilities.Helpers.{_, given}
-import utilities.Printer.*
+import lisa.utils.Helpers.{_, given}
import scala.collection.immutable.Set
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
similarity index 99%
rename from src/main/scala/proven/tactics/SimplePropositionalSolver.scala
rename to src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
index 69e75d73..a38c006e 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
@@ -1,9 +1,9 @@
-package proven.tactics
+package lisa.proven.tactics
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import utilities.Helpers.*
+import lisa.utils.Helpers.*
import scala.collection.mutable.Set as mSet
diff --git a/src/test/scala/lisa/proven/InitialProofsTests.scala b/src/test/scala/lisa/proven/InitialProofsTests.scala
index 331a3f44..c9873cdc 100644
--- a/src/test/scala/lisa/proven/InitialProofsTests.scala
+++ b/src/test/scala/lisa/proven/InitialProofsTests.scala
@@ -1,18 +1,18 @@
package lisa.proven
-import utilities.Printer
-import test.ProofCheckerSuite
+import lisa.utils.Printer
+import lisa.test.ProofCheckerSuite
class InitialProofsTests extends ProofCheckerSuite {
- import proven.SetTheoryLibrary.*
+ import lisa.proven.SetTheoryLibrary.*
test("File SetTheory initialize well") {
- proven.mathematics.SetTheory
+ lisa.proven.mathematics.SetTheory
succeed
}
test("File Mapping initialize well") {
- proven.mathematics.Mapping
+ lisa.proven.mathematics.Mapping
succeed
}
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 8598562a..57599edf 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,16 +1,16 @@
package lisa.proven
-import utilities.Printer
-import utilities.Printer.*
+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 proven.tactics.SimplePropositionalSolver as SPS
-import utilities.Helpers.*
-import utilities.tptp.KernelParser.*
-import utilities.tptp.ProblemGatherer.getPRPproblems
+import lisa.proven.tactics.SimplePropositionalSolver as SPS
+import lisa.utils.Helpers.*
+import lisa.tptp.KernelParser.*
+import lisa.tptp.ProblemGatherer.getPRPproblems
class SimpleProverTests extends AnyFunSuite {
--
GitLab