From e39f6f653c1ad6680f599f7e8f27da4c52a23744 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir42@gmail.com>
Date: Thu, 3 Oct 2024 16:41:12 +0200
Subject: [PATCH] Reseal `Proof` trait, upgrade to Scala 3.4.2 (#225)
* Explicitly mark `of` and `has` as infix
* Reseal `Proof`
* Scala 3.4 automated rewrites
* Change scala version, set dynamic cross versions
* Update changelog
---
CHANGES.md | 5 ++
build.sbt | 10 ++--
.../main/scala/lisa/automation/Apply.scala | 2 +-
.../scala/lisa/automation/CommonTactics.scala | 8 +--
.../scala/lisa/automation/Substitution.scala | 8 +--
.../maths/settheory/types/TypeSystem.scala | 58 +++++++++----------
.../maths/settheory/types/adt/Frontend.scala | 6 +-
.../maths/settheory/types/adt/Helpers.scala | 2 +-
.../maths/settheory/types/adt/Tactics.scala | 8 +--
.../maths/settheory/types/adt/Untyped.scala | 14 ++---
.../src/main/scala/lisa/fol/Common.scala | 44 +++++++-------
.../src/main/scala/lisa/fol/Lambdas.scala | 2 +-
.../src/main/scala/lisa/fol/Sequents.scala | 2 +-
.../scala/lisa/prooflib/BasicStepTactic.scala | 4 +-
.../scala/lisa/prooflib/ProofsHelpers.scala | 2 +-
.../scala/lisa/prooflib/WithTheorems.scala | 5 +-
.../scala/lisa/utils/parsing/Parser.scala | 2 +-
.../lisa/utils/parsing/ParsingUtils.scala | 2 +-
18 files changed, 93 insertions(+), 91 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index b71a20ae..3c8fec63 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,10 @@
# Change List
+## 2024-07-22
+Resealed the `Proof` trait following a fix of the relevant compiler bug [scala/scala3#19031](https://github.com/scala/scala3/issues/19031).
+
+Updated to Scala 3.4.2, and relevant minor syntax changes from `-rewrite -source 3.4-migration`.
+
## 2024-04-12
Addition of the Congruence tactic, solving sequents by congruence closure using egraphs.
diff --git a/build.sbt b/build.sbt
index a38f440c..faa922e1 100644
--- a/build.sbt
+++ b/build.sbt
@@ -15,14 +15,14 @@ ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
ThisBuild / semanticdbEnabled := true
ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
+val scala2 = "2.13.8"
+val scala3 = "3.4.2"
+
val commonSettings = Seq(
- crossScalaVersions := Seq("3.3.3"),
+ crossScalaVersions := Seq(scala3, scala2),
run / fork := true
)
-val scala2 = "2.13.8"
-val scala3 = "3.3.3"
-
val commonSettings2 = commonSettings ++ Seq(
scalaVersion := scala2,
scalacOptions ++= Seq("-Ypatmat-exhaust-depth", "50")
@@ -30,7 +30,7 @@ val commonSettings2 = commonSettings ++ Seq(
val commonSettings3 = commonSettings ++ Seq(
scalaVersion := scala3,
scalacOptions ++= Seq(
- "-language:implicitConversions",
+ "-language:implicitConversions"
),
javaOptions += "-Xmx10G",
libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test",
diff --git a/lisa-sets/src/main/scala/lisa/automation/Apply.scala b/lisa-sets/src/main/scala/lisa/automation/Apply.scala
index a0c22d79..eb389628 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Apply.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Apply.scala
@@ -112,7 +112,7 @@ class Apply(using val lib: Library, val proof: lib.Proof)(thm: proof.Fact) exten
* @param tSubst the assignment for term variables
*/
private def substitute(using _proof: lib.Proof)(fact: _proof.Fact, fSubst: FormulaSubstitution, tSubst: TermSubstitution): _proof.Fact =
- fact.of(fSubst.toFSubstPair: _*).of(tSubst.toTSubstPair: _*)
+ fact.of(fSubst.toFSubstPair*).of(tSubst.toTSubstPair*)
/**
* Applies on method with a varargs instead of a sequence.
diff --git a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
index c5b8e80a..a81e8d9a 100644
--- a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
@@ -178,14 +178,14 @@ object CommonTactics {
// Instantiate terms in the definition
val subst = vars.zip(xs).map(tup => tup._1 := tup._2)
- val P = definition.f.substitute(subst: _*)
+ val P = definition.f.substitute(subst*)
val expected = P.substitute(y := fxs)
if (!F.isSame(expected, bot.right.head)) {
return proof.InvalidProofTactic("Right-hand side of bottom sequent should be of the form P(f(xs)).")
}
TacticSubproof {
- lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst: _*))
+ lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst*))
lib.thenHave((y === fxs) <=> P) by InstantiateForall(y)
lib.thenHave((fxs === fxs) <=> P.substitute(y := fxs)) by InstFunSchema(Map(y -> fxs))
lib.thenHave(P.substitute(y := fxs)) by Restate
@@ -218,7 +218,7 @@ object CommonTactics {
// val instantiations: Seq[(F.SchematicTermLabel, F.LambdaTermTerm)] = vars.zip(xs.map(x => F.LambdaTermTerm(Seq(), x)))
val subst = vars.zip(xs).map(tup => tup._1 := tup._2)
- val P = definition.f.substitute(subst: _*)
+ val P = definition.f.substitute(subst*)
// Instantiate terms in the definition
// val P = F.LambdaTermFormula(Seq(y), expr(xs))
@@ -248,7 +248,7 @@ object CommonTactics {
}
TacticSubproof {
- lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst: _*))
+ lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst*))
lib.thenHave((y === fxs) <=> P) by InstantiateForall(y)
lib.thenHave((fxs === fxs) <=> P.substitute(y := fxs)) by InstFunSchema(Map(y -> fxs))
lib.thenHave(P.substitute(y := fxs)) by Restate
diff --git a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
index fcc45642..79795e57 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
@@ -236,7 +236,7 @@ object Substitution {
leftContextReduced.termRules.map { case (_, (rule, subst)) =>
sourceOf.get(rule) match {
case Some(f: proof.Fact) =>
- f.of(subst.toSeq.map((l, r) => (l := r)): _*)
+ f.of(subst.toSeq.map((l, r) => (l := r))*)
// case Some(j: lib.theory.Justification) =>
// j.of(subst.toSeq.map((l, r) => (l, lambda(Seq(), r))): _*)
case _ =>
@@ -246,7 +246,7 @@ object Substitution {
leftContextReduced.formulaRules.map { case (_, (rule, subst)) =>
sourceOf.get(rule) match {
case Some(f: proof.Fact) =>
- f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r)): _*)
+ f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r))*)
// case Some(j: lib.theory.Justification) =>
// j.of(subst._1.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))) ++ subst._2.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))): _*)
case _ =>
@@ -257,7 +257,7 @@ object Substitution {
rightContextReduced.termRules.map { case (_, (rule, subst)) =>
sourceOf.get(rule) match {
case Some(f: proof.Fact) =>
- f.of(subst.toSeq.map((l, r) => (l := r)): _*)
+ f.of(subst.toSeq.map((l, r) => (l := r))*)
// case Some(j: lib.theory.Justification) =>
// j.of(subst.toSeq.map((l, r) => (l, lambda(Seq(), r))): _*)
case None =>
@@ -267,7 +267,7 @@ object Substitution {
rightContextReduced.formulaRules.map { case (_, (rule, subst)) =>
sourceOf.get(rule) match {
case Some(f: proof.Fact) =>
- f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r)): _*)
+ f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r))*)
// case Some(j: lib.theory.Justification) =>
// j.of(subst._1.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))) ++ subst._2.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))): _*)
case None =>
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
index 850103ca..ff939e4d 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
@@ -40,7 +40,7 @@ object TypeLib extends lisa.Main {
// C |> D is the functional class of functionals from the class C to the class D
// F is C |> D desugars into ∀(x, (x is C) => (F(x) is D))
- val testTheorem = Theorem((x is A, f is (A |=> B), F is (A |=> B) |> (A |=> B) ) |- (F(f)*(x) is B)) {
+ val testTheorem = Theorem((x `is` A, f `is` (A |=> B), F `is` (A |=> B) |> (A |=> B) ) |- (F(f)*(x) `is` B)) {
have(thesis) by TypeChecker.prove
}
@@ -87,7 +87,7 @@ object TypeSystem {
case class FunctionalClass(in: Seq[Class], args: Seq[Variable], out: Class, arity: Int) {
def formula[N <: Arity](f: (Term**N |-> Term)): Formula =
- val inner = (args.zip(in.toSeq).map((term, typ) => (term is typ).asFormula).reduceLeft((a, b) => a /\ b)) ==> (f.applySeq(args) is out)
+ val inner = (args.zip(in.toSeq).map((term, typ) => (term `is` typ).asFormula).reduceLeft((a, b) => a /\ b)) ==> (f.applySeq(args) `is` out)
args.foldRight(inner)((v, form) => forall(v, form))
override def toString(): String = in.map(_.toStringSeparated()).mkString("(", ", ", ")") + " |> " + out.toStringSeparated()
@@ -112,8 +112,8 @@ object TypeSystem {
}
extension [A <: Class](t: Term) {
- def is(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
- def ::(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
+ def is(clas:A): Formula & TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula & TypeAssignment[A]]
+ def ::(clas:A): Formula & TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula & TypeAssignment[A]]
def @@(t2: Term): AppliedFunction = AppliedFunction(t, t2)
def *(t2: Term): AppliedFunction = AppliedFunction(t, t2)
}
@@ -318,7 +318,7 @@ object TypeSystem {
extension (c: Constant) {
def typedWith[A <: Class](typ:A)(justif: JUSTIFICATION) : TypedConstant[A] =
- if justif.statement.right.size != 1 || justif.statement.left.size != 0 || !K.isSame((c is typ).asFormula.underlying, justif.statement.right.head.underlying) then
+ if justif.statement.right.size != 1 || justif.statement.left.size != 0 || !K.isSame((c `is` typ).asFormula.underlying, justif.statement.right.head.underlying) then
throw new IllegalArgumentException(s"A proof of typing of $c must be of the form ${c :: typ}, but the given justification shows ${justif.statement}.")
else TypedConstant(c.id, typ, justif)
}
@@ -345,7 +345,7 @@ object TypeSystem {
var typingError: proof.ProofTacticJudgement = null
bot.right.find(goal =>
goal match
- case (term is typ) =>
+ case (term `is` typ) =>
val ptj = typecheck(using SetTheoryLibrary)(context.toSeq, term, Some(typ))
if ptj.isValid then
success = ptj
@@ -378,21 +378,21 @@ object TypeSystem {
def innerTypecheck(context2: Map[Term, Seq[Class]], term:Term, typ:Option[Class]): Class= {
val possibleTypes = typingAssumptions.getOrElse(term, Nil)
if typ == Some(any) then
- have(term is any) by Restate.from(TypeLib.any.definition of (x := term))
+ have(term `is` any) by Restate.from(TypeLib.any.definition of (x := term))
any
else if typ.isEmpty && possibleTypes.size >=1 then
- have(term is possibleTypes.head) by Restate
+ have(term `is` possibleTypes.head) by Restate
possibleTypes.head
else if (typ.nonEmpty && possibleTypes.contains(typ.get)) then
- have(term is typ.get) by Restate
+ have(term `is` typ.get) by Restate
typ.get
else term match
case tc: TypedConstant[?] =>
if typ.isEmpty then
- have(tc is tc.typ) by Restate.from(tc.justif)
+ have(tc `is` tc.typ) by Restate.from(tc.justif)
tc.typ
- else if K.isSame((tc is typ.get).asFormula.underlying, (tc is tc.typ).asFormula.underlying) then
- have(tc is typ.get) by Restate.from(tc.justif)
+ else if K.isSame((tc `is` typ.get).asFormula.underlying, (tc `is` tc.typ).asFormula.underlying) then
+ have(tc `is` typ.get) by Restate.from(tc.justif)
typ.get
else throw TypingException("Constant " + tc + " expected to be of type " + typ + " but has type " + tc.typ + ".")
@@ -404,8 +404,8 @@ object TypeSystem {
funcType match
case inType |=> outType => typ match
case None =>
- if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
- have(term is outType) by Tautology.from(
+ if K.isSame((arg `is` inType).asFormula.underlying, (arg `is` argType).asFormula.underlying) then
+ have(term `is` outType) by Tautology.from(
funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
funcProof,
argProof
@@ -413,9 +413,9 @@ object TypeSystem {
outType
else throw
TypingException("Function " + func + " found to have type " + funcType + ", but argument " + arg + " has type " + argType + " instead of expected " + inType + ".")
- case Some(typ) if K.isSame((term is typ).asFormula.underlying, (term is outType).asFormula.underlying) =>
- if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
- have(term is outType) by Tautology.from(
+ case Some(typ) if K.isSame((term `is` typ).asFormula.underlying, (term `is` outType).asFormula.underlying) =>
+ if K.isSame((arg `is` inType).asFormula.underlying, (arg `is` argType).asFormula.underlying) then
+ have(term `is` outType) by Tautology.from(
funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
funcProof,
argProof
@@ -450,7 +450,7 @@ object TypeSystem {
labelTypes.find((labelType, step) =>
labelType.arity == args.size &&
(args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) =>
- K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying) //
+ K.isSame((argAndTypes._1 `is` inType).asFormula.underlying, (argAndTypes._1 `is` argAndTypes._2).asFormula.underlying) //
)
) match
case None =>
@@ -461,28 +461,28 @@ object TypeSystem {
val in: Seq[Class] = labelType.in.toSeq
//val labelProp = labelType.formula(label.asInstanceOf)
val labelPropStatement = step()
- val labInst = labelPropStatement.of(args: _*)
+ val labInst = labelPropStatement.of(args*)
val subst = (labelType.args zip args).map((v, a) => (v := a))
val newOut: Class = out match {
- case t: Term => t.substitute(subst: _*)
- case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+ case t: Term => t.substitute(subst*)
+ case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst*)
}
- have(term is newOut) by Tautology.from(
- (argTypesProofs :+ labInst ) : _*
+ have(term `is` newOut) by Tautology.from(
+ (argTypesProofs :+ labInst )*
)
newOut
case Some(typValue) =>
labelTypes.find((labelType, step) =>
labelType.arity == args.size &&
(args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) =>
- K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying)
+ K.isSame((argAndTypes._1 `is` inType).asFormula.underlying, (argAndTypes._1 `is` argAndTypes._2).asFormula.underlying)
) && {
val subst = (labelType.args zip args).map((v, a) => (v := a))
val newOut: Class = labelType.out match {
- case t: Term => t.substitute(subst: _*)
- case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+ case t: Term => t.substitute(subst*)
+ case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst*)
}
- K.isSame((term is newOut).asFormula.underlying, (term is typValue).asFormula.underlying)
+ K.isSame((term `is` newOut).asFormula.underlying, (term `is` typValue).asFormula.underlying)
}
) match
@@ -493,8 +493,8 @@ object TypeSystem {
val in: Seq[Class] = labelType.in.toSeq
//val labelProp = labelType.formula(label.asInstanceOf)
val labelPropStatement = step()
- have(term is typValue) by Tautology.from(
- (argTypesProofs :+ labelPropStatement.of(args: _*) ) : _*
+ have(term `is` typValue) by Tautology.from(
+ (argTypesProofs :+ labelPropStatement.of(args*) )*
)
typValue
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
index df6d157e..fa455cd3 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
@@ -201,7 +201,7 @@ object ADTSyntax {
val semanticCons = trimmedNames.tail.zip(syntacticCons).map(SemanticConstructor(_, _, syntacticADT))
val semanticADT = SemanticADT[N](syntacticADT, semanticCons)
val cons = semanticCons.map(Constructor(_))
- (ADT[N](semanticADT, cons), new constructors[N](cons : _*))
+ (ADT[N](semanticADT, cons), new constructors[N](cons*))
}
@@ -356,7 +356,7 @@ object ADTSyntax {
* @param adt the ADT
* @return a tuple containing the ADT and its constructors
*/
- private def extractConstructors[N <: Arity](adt: ADT[N]): (ADT[N], constructors[N]) = (adt, constructors(adt.constructors : _*))
+ private def extractConstructors[N <: Arity](adt: ADT[N]): (ADT[N], constructors[N]) = (adt, constructors(adt.constructors*))
/**
* Outputs a polymorphic ADT and constructors from a user specification
@@ -514,7 +514,7 @@ object ADTSyntax {
val subst = adtVar -> consTerm
val assumptions =
- (wellTypedSet(cons.underlying.semanticSignature(vars).map(p => (p._1, p._2.substitute(cons.underlying.typeVariablesSeq.zip(args).map(SubstPair(_, _)) : _*))))
+ (wellTypedSet(cons.underlying.semanticSignature(vars).map(p => (p._1, p._2.substitute(cons.underlying.typeVariablesSeq.zip(args).map(SubstPair(_, _))*))))
++
cons.underlying.syntacticSignature(vars).filter(_._2 == Self).map((v, _) => prop.substitute(adtVar -> v)))
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
index 5830f1aa..604b8c34 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
@@ -265,7 +265,7 @@ private[adt] object ADTDefinitions {
def substitute(p: SubstPair*): ConstructorArgument =
this match
case Self => Self
- case GroundType(t) => GroundType(t.substitute(p : _*))
+ case GroundType(t) => GroundType(t.substitute(p*))
}
/**
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
index cb825079..7a05b0b4 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
@@ -47,10 +47,10 @@ class Induction[M <: Arity](expectedVar: Option[Variable], expectedADT: Option[A
val prop = lambda[Term, Formula](x, propFun(x))
val typeVariablesSubstPairs = adt.typeVariables.toSeq.zip(typeVariablesSubst).map(SubstPair(_, _))
- val instTerm = adt(typeVariablesSubst : _*)
+ val instTerm = adt(typeVariablesSubst*)
- adt.constructors.foldLeft[proof.Fact](adt.induction.of((typeVariablesSubstPairs :+ (P := prop)): _*)) ( (acc, c) =>
- val inductiveCaseProof = cases(c)._1.zip(c.underlying.underlying.specification.map(_.substitute(typeVariablesSubstPairs : _*))).foldRight[proof.Fact](cases(c)._2) ( (el, acc2) =>
+ adt.constructors.foldLeft[proof.Fact](adt.induction.of((typeVariablesSubstPairs :+ (P := prop))*)) ( (acc, c) =>
+ val inductiveCaseProof = cases(c)._1.zip(c.underlying.underlying.specification.map(_.substitute(typeVariablesSubstPairs*))).foldRight[proof.Fact](cases(c)._2) ( (el, acc2) =>
val (v, ty) = el
val accRight: Formula = acc2.statement.right.head
ty match
@@ -140,7 +140,7 @@ class Induction[M <: Arity](expectedVar: Option[Variable], expectedADT: Option[A
val prop = inferedProp.getOrElse(bot.right.head)
val propFunction = (t: Term) => inferedProp.getOrElse(bot.right.head).substitute(inferedVar -> t)
- val assignment = inferedVar :: inferedADT(inferedArgs : _*)
+ val assignment = inferedVar :: inferedADT(inferedArgs*)
val context = (if inferedProp.isDefined then bot else bot -<< assignment).left
val builder = ADTSyntax.CaseBuilder[N, proof.ProofStep, (Sequent, Seq[Term], Variable)]((context |- prop, inferedArgs, inferedVar))
cases(using builder)
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
index 61dd75a7..cb3944c1 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
@@ -375,7 +375,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
// STEP 2.1: Prove that we can expand the domain of the (quantified) variables of the constructor
val andSeq =
for (v, ty) <- c.signature2 yield have((subsetST, varsWellTypedS) |- in(v, ty.getOrElse(t))) by Weakening(subsetElimination of (z := v))
- val expandingDomain = have((subsetST, varsWellTypedS) |- varsWellTypedT) by RightAnd(andSeq: _*)
+ val expandingDomain = have((subsetST, varsWellTypedS) |- varsWellTypedT) by RightAnd(andSeq*)
val weakeningLabelEq = have(labelEq |- labelEq) by Hypothesis
have((subsetST, varsWellTypedS, labelEq) |- varsWellTypedT /\ labelEq) by RightAnd(expandingDomain, weakeningLabelEq)
@@ -390,7 +390,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
// STEP 3: Prove that this holds for any constructor
// ? Steps 2 and 3 can be merged and optimized through the repeated use of an external theorem like [[ADTHelperTheorems.unionPreimageMonotonic]]
if constructors.isEmpty then have((subsetST, isConstructorXS) |- isConstructorXT) by Restate
- else have((subsetST, isConstructorXS) |- isConstructorXT) by LeftOr(isConstructorXSImpliesT: _*)
+ else have((subsetST, isConstructorXS) |- isConstructorXT) by LeftOr(isConstructorXSImpliesT*)
// STEP 4: Prove the thesis by showing that making the union with the function argument does not change the monotonicity
thenHave(subsetST |- isConstructorXS ==> isConstructorXT) by RightImplies
@@ -820,7 +820,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
case GroundType(t) =>
have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- in(v, t)) by Restate
- have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- constructorVarsInDomain(c, term)) by RightAnd(andSeq: _*)
+ have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- constructorVarsInDomain(c, term)) by RightAnd(andSeq*)
thenHave((hIsTheHeightFunction, exists(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n)))) |- constructorVarsInDomain(c, term)) by LeftExists
}
@@ -985,7 +985,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
for (v, ty) <- c.signature
yield have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- in(v, ty.getOrElse(app(h, successor(n))))) by Weakening(liftHeight of (y := v))
- val left = have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- constructorVarsInHSuccN) by RightAnd(liftHeightAndSequence: _*)
+ val left = have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- constructorVarsInHSuccN) by RightAnd(liftHeightAndSequence*)
val right = have(x === c.term |- x === c.term) by Hypothesis
have((hIsTheHeightFunction, in(n, N), constructorVarsInHN, (x === c.term)) |- constructorVarsInHSuccN /\ (x === c.term )) by RightAnd(
@@ -998,7 +998,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
thenHave((hIsTheHeightFunction, in(n, N), isConstructorCXHN) |- isConstructorXHSuccN) by Weakening
- have((hIsTheHeightFunction, in(n, N), isConstructorXHN) |- isConstructorXHSuccN) by LeftOr(liftConstructorHeightOrSequence: _*)
+ have((hIsTheHeightFunction, in(n, N), isConstructorXHN) |- isConstructorXHSuccN) by LeftOr(liftConstructorHeightOrSequence*)
// STEP 1.5: Show that x ∈ introductionFunction(height(n + 1)) => for some c, x = c(x1, ..., xn)
// with xi, ..., xj ∈ height(n + 1).
@@ -1156,7 +1156,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
).toSeq
- have((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, isConstructor(x, app(h, n))) |- P(x)) by LeftOr(orSeq: _*)
+ have((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, isConstructor(x, app(h, n))) |- P(x)) by LeftOr(orSeq*)
}
// STEP 2.2: Prove that if x ∈ height(n + 1) then P(x) holds.
@@ -1734,7 +1734,7 @@ private class SemanticConstructor[N <: Arity](using line: sourcecode.Line, file:
have(!inductionPreconditionIneq(c) |- isConstructorMap(c)) by Cut(conditionStrenghtening, lastStep)
thenHave(!inductionPreconditionIneq(c) |- isConstructor) by Weakening
- have(thesis) by LeftOr(negInductionPreconditionsOrSequence: _*)
+ have(thesis) by LeftOr(negInductionPreconditionsOrSequence*)
}
// STEP 2: Conclude
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index 77977eb2..3bb97657 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -79,7 +79,7 @@ trait Common {
* Substitution in the LisaObject of schematics symbols by values. It is not guaranteed by the type system that types of schematics and values match, and the substitution can fail if that is the case.
* This is the substitution function that should be implemented.
*/
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): T
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): T
def substituteUnsafe2[A <: SchematicLabel[?], B <: LisaObject[B]](map: Map[A, B]): T = substituteUnsafe(map.asInstanceOf)
/**
@@ -87,7 +87,7 @@ trait Common {
* This is the substitution that should be used when writing proofs.
*/
def substitute(pairs: SubstPair*): T = {
- substituteUnsafe(Map(pairs.map(s => (s._1, (s._2: LisaObject[_])))*))
+ substituteUnsafe(Map(pairs.map(s => (s._1, (s._2: LisaObject[?])))*))
}
def substituteOne[S <: LisaObject[S]](v: SchematicLabel[S], arg: S): T = substituteUnsafe(Map(v -> arg))
@@ -219,7 +219,7 @@ trait Common {
sealed trait ConstantTermLabel[A <: (Term | (Seq[Term] |-> Term)) & LisaObject[A]] extends TermLabel[A] with ConstantLabel[A] {
this: A & LisaObject[A] =>
val underlyingLabel: K.ConstantFunctionLabel
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantTermLabel[A]
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantTermLabel[A]
override def rename(newid: Identifier): ConstantTermLabel[A]
def freshRename(taken: Iterable[Identifier]): ConstantTermLabel[A]
}
@@ -276,7 +276,7 @@ trait Common {
*/
sealed trait FunctionLabel[N <: Arity] extends TermLabel[(Term ** N) |-> Term] with ((Term ** N) |-> Term) {
val underlyingLabel: K.TermLabel
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): (Term ** N) |-> Term
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): (Term ** N) |-> Term
def applyUnsafe(args: (Term ** N)): Term = AppliedFunctional(this, args.toSeq)
override def rename(newid: Identifier): FunctionLabel[N]
def freshRename(taken: Iterable[Identifier]): FunctionLabel[N]
@@ -293,7 +293,7 @@ trait Common {
val underlyingLabel: K.VariableLabel = K.VariableLabel(id)
val underlying = K.VariableTerm(underlyingLabel)
def applyUnsafe(args: Term ** 0) = this
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term = {
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Term = {
map.get(this) match {
case Some(subst) =>
subst match {
@@ -344,7 +344,7 @@ trait Common {
val underlyingLabel: K.ConstantFunctionLabel = K.ConstantFunctionLabel(id, 0)
val underlying = K.Term(underlyingLabel, Seq.empty)
def applyUnsafe(args: Term ** 0) = this
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Constant = this
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Constant = this
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def rename(newid: Identifier): Constant = Constant(newid)
@@ -387,7 +387,7 @@ trait Common {
case _ => Seq.empty
}
@nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ((Term ** N) |-> Term) = {
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ((Term ** N) |-> Term) = {
map.get(this) match {
case Some(subst) =>
subst match {
@@ -441,7 +441,7 @@ trait Common {
case AppliedFunctional(label, args) if (label == this) => args
case _ => Seq.empty
}
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantFunctionLabel[N] = this
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantFunctionLabel[N] = this
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def rename(newid: Identifier): ConstantFunctionLabel[N] = ConstantFunctionLabel(newid, arity)
@@ -486,7 +486,7 @@ trait Common {
*/
class AppliedFunctional(val label: FunctionLabel[?], val args: Seq[Term]) extends Term with Absolute {
override val underlying = K.Term(label.underlyingLabel, args.map(_.underlying))
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term =
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Term =
label.substituteUnsafe(map).applyUnsafe(args.map[Term]((x: Term) => x.substituteUnsafe(map)))
def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.flatMap(_.freeSchematicLabels)
@@ -567,7 +567,7 @@ trait Common {
sealed trait ConstantAtomicLabel[A <: (Formula | (Seq[Term] |-> Formula)) & LisaObject[A]] extends AtomicLabel[A] with ConstantLabel[A] {
this: A & LisaObject[A] =>
val underlyingLabel: K.ConstantAtomicLabel
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantAtomicLabel[A]
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantAtomicLabel[A]
override def rename(newid: Identifier): ConstantAtomicLabel[A]
def freshRename(taken: Iterable[Identifier]): ConstantAtomicLabel[A]
}
@@ -628,7 +628,7 @@ trait Common {
*/
sealed trait PredicateLabel[N <: Arity] extends AtomicLabel[(Term ** N) |-> Formula] with ((Term ** N) |-> Formula) with Absolute {
val underlyingLabel: K.AtomicLabel
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): (Term ** N) |-> Formula
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): (Term ** N) |-> Formula
def applyUnsafe(args: (Term ** N)): Formula = AppliedPredicate(this, args.toSeq)
override def rename(newid: Identifier): PredicateLabel[N]
def freshRename(taken: Iterable[Identifier]): PredicateLabel[N]
@@ -645,7 +645,7 @@ trait Common {
val underlyingLabel: K.VariableFormulaLabel = K.VariableFormulaLabel(id)
val underlying = K.AtomicFormula(underlyingLabel, Seq.empty)
def applyUnsafe(args: Term ** 0): Formula = this
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula = {
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Formula = {
map.get(this) match {
case Some(subst) =>
subst match {
@@ -674,7 +674,7 @@ trait Common {
val underlyingLabel: K.ConstantAtomicLabel = K.ConstantAtomicLabel(id, 0)
val underlying = K.AtomicFormula(underlyingLabel, Seq.empty)
def applyUnsafe(args: Term ** 0): Formula = this
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantFormula = this
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantFormula = this
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def rename(newid: Identifier): ConstantFormula = ConstantFormula(newid)
@@ -694,7 +694,7 @@ trait Common {
case _ => Seq.empty
}
@nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Term ** N, Formula] = {
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): |->[Term ** N, Formula] = {
map.get(this) match {
case Some(subst) =>
subst match {
@@ -723,7 +723,7 @@ trait Common {
case AppliedPredicate(label, args) if (label == this) => args
case _ => Seq.empty
}
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantPredicateLabel[N] = this
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantPredicateLabel[N] = this
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def rename(newid: Identifier): ConstantPredicateLabel[N] = ConstantPredicateLabel(newid, arity)
@@ -744,7 +744,7 @@ trait Common {
*/
case class AppliedPredicate(label: PredicateLabel[?], args: Seq[Term]) extends AtomicFormula with Absolute {
override val underlying = K.AtomicFormula(label.underlyingLabel, args.map(_.underlying))
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula =
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Formula =
label.substituteUnsafe(map).applyUnsafe(args.map[Term]((x: Term) => x.substituteUnsafe(map)))
def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.toSeq.flatMap(_.freeSchematicLabels)
@@ -769,7 +769,7 @@ trait Common {
def applySeq(args: Seq[Formula]): Formula = applyUnsafe(args)
def rename(newid: Identifier): ConnectorLabel
def freshRename(taken: Iterable[Identifier]): ConnectorLabel
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Seq[Formula], Formula]
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): |->[Seq[Formula], Formula]
def mkString(args: Seq[Formula]): String
def mkStringSeparated(args: Seq[Formula]): String
@@ -786,7 +786,7 @@ trait Common {
case _ => Seq.empty
}
@nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Formula ** N, Formula] = {
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): |->[Formula ** N, Formula] = {
map.get(this) match {
case Some(subst) =>
subst match {
@@ -820,7 +820,7 @@ trait Common {
case AppliedConnector(label, args) if (label == this) => args
case _ => Seq.empty
}
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): this.type = this
def applyUnsafe(args: Formula ** N): Formula = AppliedConnector(this, args.toSeq)
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
@@ -837,7 +837,7 @@ trait Common {
*/
case class AppliedConnector(label: ConnectorLabel, args: Seq[Formula]) extends Formula with Absolute {
override val underlying = K.ConnectorFormula(label.underlyingLabel, args.map(_.underlying))
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula =
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Formula =
label.applyUnsafe(args.map[Formula]((x: Formula) => x.substituteUnsafe(map)))
def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.flatMap(_.freeSchematicLabels)
def allSchematicLabels: Set[SchematicLabel[?]] = label.allSchematicLabels ++ args.flatMap(_.allSchematicLabels)
@@ -872,7 +872,7 @@ trait Common {
}
inline def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
inline def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
- inline def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
+ inline def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): this.type = this
override def toString() = id
}
@@ -885,7 +885,7 @@ trait Common {
def allSchematicLabels: Set[Common.this.SchematicLabel[?]] = body.allSchematicLabels + bound
def freeSchematicLabels: Set[Common.this.SchematicLabel[?]] = body.freeSchematicLabels - bound
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): BinderFormula = {
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): BinderFormula = {
val newSubst = map - bound
if (map.values.flatMap(_.freeSchematicLabels).toSet.contains(bound)) {
val taken: Set[SchematicLabel[?]] = body.allSchematicLabels ++ map.keys
diff --git a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
index bfc15237..45d1f868 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
@@ -34,7 +34,7 @@ trait Lambdas extends Common {
* @param map
* @return
*/
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): LambdaExpression[T, R, N] = {
+ def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): LambdaExpression[T, R, N] = {
val newSubst = map -- seqBounds
val conflict = map.values.flatMap(_.freeSchematicLabels).toSet.intersect(bounds.toSet.asInstanceOf)
if (conflict.nonEmpty) {
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index 792c75aa..7c8b4f35 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -30,7 +30,7 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
* @param map
* @return
*/
- def instantiateWithProof(map: Map[SchematicLabel[_], _ <: LisaObject[_]], index: Int): (Sequent, Seq[K.SCProofStep]) = {
+ def instantiateWithProof(map: Map[SchematicLabel[?], ? <: LisaObject[?]], index: Int): (Sequent, Seq[K.SCProofStep]) = {
val mTerm: Map[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]] =
map.collect[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]](p =>
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
index 0501f1b4..899c51da 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -187,7 +187,7 @@ object BasicStepTactic {
else
proof.InvalidProofTactic("Right-hand side of conclusion is not a superset of the one of the premises.")
} else if (pivots.forall(_.tail.isEmpty))
- LeftOr.withParameters(pivots.map(_.head): _*)(premises: _*)(bot)
+ LeftOr.withParameters(pivots.map(_.head)*)(premises*)(bot)
else
// some extraneous formulae
proof.InvalidProofTactic("Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
@@ -586,7 +586,7 @@ object BasicStepTactic {
else
proof.InvalidProofTactic("Left-hand side of conclusion is not a superset of the one of the premises.")
} else if (pivots.forall(_.tail.isEmpty))
- RightAnd.withParameters(pivots.map(_.head): _*)(premises: _*)(bot)
+ RightAnd.withParameters(pivots.map(_.head)*)(premises*)(bot)
else
// some extraneous formulae
proof.InvalidProofTactic("Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises +φ∧ψ.")
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
index ebe992a7..f6f030f8 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
@@ -120,7 +120,7 @@ trait ProofsHelpers {
}
extension (using proof: library.Proof)(fact: proof.Fact) {
- def of(insts: (F.SubstPair | F.Term)*): proof.InstantiatedFact = {
+ infix def of(insts: (F.SubstPair | F.Term)*): proof.InstantiatedFact = {
proof.InstantiatedFact(fact, insts)
}
def statement: F.Sequent = proof.sequentOfFact(fact)
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index fc920eb1..628ef7ff 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -26,10 +26,7 @@ trait WithTheorems {
*
* @param assump list of starting assumptions, usually propagated from outer proofs.
*/
- // TODO: reseal this class
- // see https://github.com/lampepfl/dotty/issues/19031
- // and https://github.com/epfl-lara/lisa/issues/190
- abstract class Proof(assump: List[F.Formula]) {
+ sealed abstract class Proof(assump: List[F.Formula]) {
val possibleGoal: Option[F.Sequent]
type SelfType = this.type
type OutsideFact >: JUSTIFICATION
diff --git a/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
index eb45a000..73e7af4a 100644
--- a/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
@@ -605,7 +605,7 @@ class Parser(
infixPredicateLabels ++
((and has Associativity.Left) ::
(or has Associativity.Left) ::
- (toplevelConnector has Associativity.None) :: Nil): _*
+ (toplevelConnector has Associativity.None) :: Nil)*
)(
(l, conn, r) => Termula(conn, Seq(l, r), (l.range._1, r.range._2)),
{
diff --git a/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala b/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala
index 6f1565ab..858f6abf 100644
--- a/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala
@@ -12,7 +12,7 @@ trait ParsingUtils extends Operators { self: Parsers =>
/**
* Indicates the associativity of the operator.
*/
- def has(associativity: lisa.utils.parsing.Associativity): PrecedenceLevel[Op] = PrecedenceLevel(operator, associativity)
+ infix def has(associativity: lisa.utils.parsing.Associativity): PrecedenceLevel[Op] = PrecedenceLevel(operator, associativity)
}
def singleInfix[Op, A](elem: Syntax[A], op: Syntax[Op])(function: (A, Op, A) => A, inverse: PartialFunction[A, (A, Op, A)] = PartialFunction.empty): Syntax[A] =
--
GitLab