From 034c70fa29c5c76ecadd9a95dacb1cf4b61dddc9 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Thu, 23 Jun 2022 17:16:19 +0200
Subject: [PATCH] Moved project lisa to root Changed final class into sealed
class for scala2 compiler
---
build.sbt | 2 +-
lisa-examples/src/main/scala/Example.scala | 2 +-
.../main/scala/lisa/kernel/fol/FormulaDefinitions.scala | 6 +++---
.../scala/lisa/kernel/fol/FormulaLabelDefinitions.scala | 4 ++--
.../src/main/scala/lisa/kernel/fol/TermDefinitions.scala | 4 ++--
.../main/scala/lisa/kernel/fol/TermLabelDefinitions.scala | 6 +++---
.../src/main/scala/lisa/kernel/proof/RunningTheory.scala | 8 ++++----
{lisa/src => src}/main/scala/lisa/proven/Main.scala | 0
.../main/scala/lisa/proven/SetTheoryLibrary.scala | 0
.../main/scala/lisa/proven/mathematics/Mapping.scala | 0
.../main/scala/lisa/proven/mathematics/SetTheory.scala | 0
.../main/scala/lisa/proven/tactics/Destructors.scala | 0
.../main/scala/lisa/proven/tactics/ProofTactics.scala | 0
.../lisa/proven/tactics/SimplePropositionalSolver.scala | 0
.../test/scala/lisa/proven/InitialProofsTests.scala | 0
.../test/scala/lisa/proven/SimpleProverTests.scala | 0
16 files changed, 16 insertions(+), 16 deletions(-)
rename {lisa/src => src}/main/scala/lisa/proven/Main.scala (100%)
rename {lisa/src => src}/main/scala/lisa/proven/SetTheoryLibrary.scala (100%)
rename {lisa/src => src}/main/scala/lisa/proven/mathematics/Mapping.scala (100%)
rename {lisa/src => src}/main/scala/lisa/proven/mathematics/SetTheory.scala (100%)
rename {lisa/src => src}/main/scala/lisa/proven/tactics/Destructors.scala (100%)
rename {lisa/src => src}/main/scala/lisa/proven/tactics/ProofTactics.scala (100%)
rename {lisa/src => src}/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala (100%)
rename {lisa/src => src}/test/scala/lisa/proven/InitialProofsTests.scala (100%)
rename {lisa/src => src}/test/scala/lisa/proven/SimpleProverTests.scala (100%)
diff --git a/build.sbt b/build.sbt
index 83ed4704..06d0a312 100644
--- a/build.sbt
+++ b/build.sbt
@@ -37,7 +37,7 @@ def withTests(project: Project): ClasspathDependency =
lazy val root = Project(
id = "lisa",
- base = file("lisa"),
+ base = file("."),
)
.settings(commonSettings3)
.settings(
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 725ef410..85e45928 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -15,7 +15,7 @@ import lisa.utils.Printer.*
*/
object Example {
def main(args: Array[String]): Unit = {
- proofExample() // uncomment when exercise finished
+ //proofExample() // uncomment when exercise finished
// solverExample()
// tptpExample()
}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 7f5d4044..0a19f260 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -22,7 +22,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
/**
* The formula counterpart of [[PredicateLabel]].
*/
- final case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
+ sealed case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
override def constantPredicates: Set[ConstantPredicateLabel] = label match {
@@ -41,7 +41,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
/**
* The formula counterpart of [[ConnectorLabel]].
*/
- final case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
+ sealed case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions)
@@ -54,7 +54,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
/**
* The formula counterpart of [[BinderLabel]].
*/
- final case class BinderFormula(label: BinderLabel, bound: VariableLabel, inner: Formula) extends Formula {
+ sealed case class BinderFormula(label: BinderLabel, bound: VariableLabel, inner: Formula) extends Formula {
override def freeVariables: Set[VariableLabel] = inner.freeVariables - bound
override def constantFunctions: Set[ConstantFunctionLabel] = inner.constantFunctions
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index 28b6c869..b1d14331 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -41,7 +41,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
/**
* A standard predicate symbol. Typical example are equality (=) and membership (∈)
*/
- final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with ConstantLabel
+ sealed case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with ConstantLabel
/**
* The equality symbol (=) for first order logic.
@@ -51,7 +51,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
/**
* A predicate symbol that can be instantiated with any formula.
*/
- final case class SchematicPredicateLabel(id: String, arity: Int) extends PredicateLabel
+ sealed case class SchematicPredicateLabel(id: String, arity: Int) extends PredicateLabel
/**
* The label for a connector, namely a function taking a fixed number of formulas and returning another formula.
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
index 3a01b5ea..e98ca824 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -26,7 +26,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
*
* @param label The label of the variable.
*/
- final case class VariableTerm(label: VariableLabel) extends Term {
+ sealed case class VariableTerm(label: VariableLabel) extends Term {
override def freeVariables: Set[VariableLabel] = Set(label)
override def constantFunctions: Set[ConstantFunctionLabel] = Set.empty
@@ -39,7 +39,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
* @param label The label of the node
* @param args children of the node. The number of argument must be equal to the arity of the function.
*/
- final case class FunctionTerm(label: FunctionLabel, args: Seq[Term]) extends Term {
+ sealed case class FunctionTerm(label: FunctionLabel, args: Seq[Term]) extends Term {
require(label.arity == args.size)
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
index 4d36c247..c2691946 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -34,7 +34,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
*
* @param id The name of the variable, for example "x" or "y".
*/
- final case class VariableLabel(id: String) extends TermLabel {
+ sealed case class VariableLabel(id: String) extends TermLabel {
val name: String = id
}
@@ -54,7 +54,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
* @param id The name of the function symbol.
* @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
*/
- final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with ConstantLabel
+ sealed case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with ConstantLabel
/**
* A schematic function symbol that can be substituted.
@@ -62,7 +62,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
* @param id The name of the function symbol.
* @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
*/
- final case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel
+ sealed case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel
/**
* A function returning true if and only if the two symbols are considered "the same".
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 7d15e8e5..ce544cf2 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -29,12 +29,12 @@ class RunningTheory {
/**
* A theorem encapsulate a sequent and assert that this sequent has been correctly proven and may be used safely in further proofs.
*/
- final case class Theorem private[RunningTheory] (name: String, proposition: Sequent) extends Justification
+ sealed case class Theorem private[RunningTheory] (name: String, proposition: Sequent) extends Justification
/**
* An axiom is any formula that is assumed and considered true within the theory. It can freely be used later in any proof.
*/
- final case class Axiom private[RunningTheory] (name: String, ax: Formula) extends Justification
+ sealed case class Axiom private[RunningTheory] (name: String, ax: Formula) extends Justification
/**
* A definition can be either a PredicateDefinition or a FunctionDefinition.
@@ -47,7 +47,7 @@ class RunningTheory {
* @param label The name and arity of the new symbol
* @param expression The formula, depending on terms, that define the symbol.
*/
- final case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, expression: LambdaTermFormula) extends Definition
+ sealed case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, expression: LambdaTermFormula) extends Definition
/**
* Define a function symbol as the unique element that has some property. The existence and uniqueness
@@ -58,7 +58,7 @@ class RunningTheory {
* @param out The variable representing the result of the function in phi
* @param expression The formula, with term parameters, defining the function.
*/
- final case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, out: VariableLabel, expression: LambdaTermFormula) extends Definition
+ sealed case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, out: VariableLabel, expression: LambdaTermFormula) extends Definition
private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
private[proof] val theorems: mMap[String, Theorem] = mMap.empty
diff --git a/lisa/src/main/scala/lisa/proven/Main.scala b/src/main/scala/lisa/proven/Main.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/Main.scala
rename to src/main/scala/lisa/proven/Main.scala
diff --git a/lisa/src/main/scala/lisa/proven/SetTheoryLibrary.scala b/src/main/scala/lisa/proven/SetTheoryLibrary.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/SetTheoryLibrary.scala
rename to src/main/scala/lisa/proven/SetTheoryLibrary.scala
diff --git a/lisa/src/main/scala/lisa/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/mathematics/Mapping.scala
rename to src/main/scala/lisa/proven/mathematics/Mapping.scala
diff --git a/lisa/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/mathematics/SetTheory.scala
rename to src/main/scala/lisa/proven/mathematics/SetTheory.scala
diff --git a/lisa/src/main/scala/lisa/proven/tactics/Destructors.scala b/src/main/scala/lisa/proven/tactics/Destructors.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/tactics/Destructors.scala
rename to src/main/scala/lisa/proven/tactics/Destructors.scala
diff --git a/lisa/src/main/scala/lisa/proven/tactics/ProofTactics.scala b/src/main/scala/lisa/proven/tactics/ProofTactics.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/tactics/ProofTactics.scala
rename to src/main/scala/lisa/proven/tactics/ProofTactics.scala
diff --git a/lisa/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
rename to src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
diff --git a/lisa/src/test/scala/lisa/proven/InitialProofsTests.scala b/src/test/scala/lisa/proven/InitialProofsTests.scala
similarity index 100%
rename from lisa/src/test/scala/lisa/proven/InitialProofsTests.scala
rename to src/test/scala/lisa/proven/InitialProofsTests.scala
diff --git a/lisa/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
similarity index 100%
rename from lisa/src/test/scala/lisa/proven/SimpleProverTests.scala
rename to src/test/scala/lisa/proven/SimpleProverTests.scala
--
GitLab