diff --git a/.scalafmt.conf b/.scalafmt.conf index cae07f41..1e296967 100644 --- a/.scalafmt.conf +++ b/.scalafmt.conf @@ -1,4 +1,4 @@ -version = 3.4.2 +version = 3.7.13 runner.dialect = scala3 @@ -8,4 +8,7 @@ docstrings.style = Asterisk docstrings.oneline = unfold docstrings.wrap = no -align.preset = none \ No newline at end of file +# align and indentation settings +align.preset = none +assumeStandardLibraryStripMargin = true +align.stripMargin = true diff --git a/build.sbt b/build.sbt index bc9c0c1b..a38f440c 100644 --- a/build.sbt +++ b/build.sbt @@ -14,19 +14,14 @@ ThisBuild / scalacOptions ++= Seq( ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8") ThisBuild / semanticdbEnabled := true ThisBuild / semanticdbVersion := scalafixSemanticdb.revision -ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0" - - - val commonSettings = Seq( - crossScalaVersions := Seq("3.3.1"), + crossScalaVersions := Seq("3.3.3"), run / fork := true ) - val scala2 = "2.13.8" -val scala3 = "3.3.1" +val scala3 = "3.3.3" val commonSettings2 = commonSettings ++ Seq( scalaVersion := scala2, @@ -36,15 +31,10 @@ val commonSettings3 = commonSettings ++ Seq( scalaVersion := scala3, scalacOptions ++= Seq( "-language:implicitConversions", - - // "-source:future", re-enable when liancheng/scalafix-organize-imports#221 is fixed - ), javaOptions += "-Xmx10G", - libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test", - libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.3.0", - //libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1", - // libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13), + libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test", + libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.4.1", Test / parallelExecution := false ) @@ -63,12 +53,14 @@ silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard"))) lazy val root = Project( id = "lisa", - base = file(".") + base = file("."), ) .settings(commonSettings3) .dependsOn(kernel, withTests(utils), withTests(sets)) // Everything but `examples` .aggregate(utils) // To run tests on all modules +Compile / run := (sets / Compile / run).evaluated + lazy val kernel = Project( id = "lisa-kernel", base = file("lisa-kernel") diff --git a/lisa-examples/src/main/scala/ADTExample.scala b/lisa-examples/src/main/scala/ADTExample.scala index 8314d18c..77b8abc7 100644 --- a/lisa-examples/src/main/scala/ADTExample.scala +++ b/lisa-examples/src/main/scala/ADTExample.scala @@ -46,12 +46,12 @@ object ADTExample extends lisa.Main { show(nil.intro) show(cons.intro) - Lemma(nil(A) :: list(A)){ + Lemma(nil(A) :: list(A)) { have(thesis) by TypeChecker.prove - } - Lemma((x :: A, l :: list(A)) |- cons(A) * x * l :: list(A)){ + } + Lemma((x :: A, l :: list(A)) |- cons(A) * x * l :: list(A)) { have(thesis) by TypeChecker.prove - } + } // Induction show(list.induction) @@ -69,12 +69,11 @@ object ADTExample extends lisa.Main { } val pred = fun(nat, nat): - Case(zero): - zero - Case(succ, n): + Case(zero): + zero + Case(succ, n): n - // ************************ // * 4 : Induction Tactic * // ************************ @@ -103,16 +102,16 @@ object ADTExample extends lisa.Main { val typeNil = have(nil(A) :: list(A)) by TypeChecker.prove val typeCons = have((y :: A, l :: list(A)) |- cons(A) * y * l :: list(A)) by TypeChecker.prove - have(l :: list(A) |- forall(x, x :: A ==> !(l === cons(A) * x * l))) by Induction(){ + have(l :: list(A) |- forall(x, x :: A ==> !(l === cons(A) * x * l))) by Induction() { Case(nil) subproof { have(x :: A ==> !(nil(A) === cons(A) * x * nil(A))) by Tautology.from(list.injectivity(nil, cons) of (y0 := x, y1 := nil(A)), typeNil) thenHave(forall(x, x :: A ==> !(nil(A) === cons(A) * x * nil(A)))) by RightForall } Case(cons, y, l) subproof { have((y :: A ==> !(l === cons(A) * y * l), y :: A, l :: list(A)) |- x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l))) by Tautology.from( - cons.injectivity of (x0 := y, x1 := l, y0 := x, y1 := cons(A) * y * l), - typeCons - ) + cons.injectivity of (x0 := y, x1 := l, y0 := x, y1 := cons(A) * y * l), + typeCons + ) thenHave((y :: A ==> !(l === cons(A) * y * l), y :: A, l :: list(A)) |- forall(x, x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l)))) by RightForall thenHave((forall(x, x :: A ==> !(l === cons(A) * x * l)), y :: A, l :: list(A)) |- forall(x, x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l)))) by LeftForall } @@ -122,4 +121,4 @@ object ADTExample extends lisa.Main { thenHave(thesis) by Tautology } -} \ No newline at end of file +} diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala index 87ec3821..494964d9 100644 --- a/lisa-examples/src/main/scala/Example.scala +++ b/lisa-examples/src/main/scala/Example.scala @@ -1,9 +1,9 @@ +import lisa.automation.Congruence import lisa.automation.Substitution.{ApplyRules as Substitute} import lisa.automation.Tableau import lisa.automation.atp.Goeland -import lisa.automation.Congruence -object Example extends lisa.Main { +object Example extends lisa.Main: draft() val x = variable @@ -62,91 +62,82 @@ object Example extends lisa.Main { have(thesis) by Tableau } - val buveurs2 = Theorem(exists(x, P(x) ==> forall(y, P(y)))) { - have(thesis) by Goeland//("goeland/Example.buveurs2_sol") - } - - - val a = variable - val one = variable - val two = variable - val * = SchematicFunctionLabel("*", 2) - val << = SchematicFunctionLabel("<<", 2) - val / = SchematicFunctionLabel("/", 2) - private val star: SchematicFunctionLabel[2] = * - private val shift: SchematicFunctionLabel[2] = << - private val divide: SchematicFunctionLabel[2] = / - - while (true) { - () - } - - extension (t:Term) { - def *(u:Term) = star(t, u) - def <<(u:Term) = shift(t, u) - def /(u:Term) = divide(t, u) - } - val congruence = Theorem(((a*two) === (a< union(unorderedPair(x, singleton(x))) - show - - val inductiveSet = DEF(x) --> in(∅, x) /\ forall(y, in(y, x) ==> in(succ(y), x)) - show + // val succ = DEF(x) --> union(unorderedPair(x, singleton(x))) + // show - */ + // val inductiveSet = DEF(x) --> in(∅, x) /\ forall(y, in(y, x) ==> in(succ(y), x)) + // show - - - - -// Simple tactic definition for LISA DSL -/* -import lisa.automation.kernel.OLPropositionalSolver.* - -object SimpleTautology extends ProofTactic { - def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = { - val redF = reducedForm(f) - if (redF == ⊤) { - Restate(decisionsPos |- f :: decisionsNeg) - } else if (redF == ⊥) { - proof.InvalidProofTactic("Sequent is not a propositional tautology") - } else { - val atom = findBestAtom(redF).get - def substInRedF(f: Formula) = redF.substituted(atom -> f) - TacticSubproof { - have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg)) - val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom) - have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg)) - val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom) - have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2) - thenHave(decisionsPos |- f :: decisionsNeg) by Restate - } - } - } + // Simple tactic definition for LISA DSL + + // object SimpleTautology extends ProofTactic { + // def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = { + // val redF = reducedForm(f) + // if (redF == ⊤) { + // Restate(decisionsPos |- f :: decisionsNeg) + // } else if (redF == ⊥) { + // proof.InvalidProofTactic("Sequent is not a propositional tautology") + // } else { + // val atom = findBestAtom(redF).get + // def substInRedF(f: Formula) = redF.substituted(atom -> f) + // TacticSubproof { + // have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg)) + // val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom) + // have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg)) + // val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom) + // have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2) + // thenHave(decisionsPos |- f :: decisionsNeg) by Restate + // } + // } + // } + + // def solveSequent(using proof: library.Proof)(bot: Sequent) = + // TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula + // have(solveFormula(sequentToFormula(bot), Nil, Nil)) + // thenHave(bot) by Restate.from + // } + // } - def solveSequent(using proof: library.Proof)(bot: Sequent) = - TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula - have(solveFormula(sequentToFormula(bot), Nil, Nil)) - thenHave(bot) by Restate.from - } -} -*/ - - // val a = formulaVariable() - // val b = formulaVariable() - // val c = formulaVariable() + // val a = formulaVariable + // val b = formulaVariable + // val c = formulaVariable // val testTheorem = Lemma((a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))) { // have(thesis) by SimpleTautology.solveSequent // } // show -} +/** + * Example showing discharge of proofs using the Goeland theorem prover. Will + * fail if Goeland is not available on PATH. + */ +object GoelandExample extends lisa.Main: + val x = variable + val y = variable + val P = predicate[1] + val f = function[1] + + val buveurs2 = Theorem(exists(x, P(x) ==> forall(y, P(y)))) { + have(thesis) by Goeland // ("goeland/Example.buveurs2_sol") + } diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala index a0cad24c..b6e20602 100644 --- a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala +++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala @@ -268,9 +268,9 @@ class ParserTest extends AnyFunSuite with TestUtils { FOLParser.parseFormula("f(x y)") } catch { case e: UnexpectedInputException => assert(e.getMessage.startsWith(""" - |f(x y) - | ^ - |Unexpected input""".stripMargin)) + |f(x y) + | ^ + |Unexpected input""".stripMargin)) } } @@ -280,9 +280,9 @@ class ParserTest extends AnyFunSuite with TestUtils { } catch { case e: UnexpectedInputException => assert(e.getMessage.startsWith(""" - |x = (a /\ b) - | ^^^^^^ - |Unexpected input: expected term""".stripMargin)) + |x = (a /\ b) + | ^^^^^^ + |Unexpected input: expected term""".stripMargin)) } } } diff --git a/project/build.properties b/project/build.properties index 553c9d3e..3116db21 100644 --- a/project/build.properties +++ b/project/build.properties @@ -1,2 +1,2 @@ -sbt.version = 1.9.3 +sbt.version = 1.9.9 diff --git a/project/plugins.sbt b/project/plugins.sbt index c731d18c..39038ece 100644 --- a/project/plugins.sbt +++ b/project/plugins.sbt @@ -1,3 +1,3 @@ -addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.1.0") -addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.9.34") -addSbtPlugin("org.scalameta" % "sbt-scalafmt" % "2.4.6") +addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "2.2.0") +addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.11.1") +addSbtPlugin("org.scalameta" % "sbt-scalafmt" % "2.5.2")