diff --git a/CHANGES.md b/CHANGES.md
index b71a20ae617b283b2021c8b7a59e2543de53cd74..3c8fec63a70518c5abad966eb7a2fd8897c5114f 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 a38f440c5b80478e6f07c9ea140850aaf88d01b9..faa922e1e7c8215109d83f2c8c64f552f7c769a6 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 a0c22d7902b93a43077c45b2cb160993e506eb84..eb3896284829c6d5133dc275abea8ff51a0f8fa0 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 c5b8e80a2cd9c2908dddbd36c43a3b6e1699dd5d..a81e8d9ac610529e5518ff8eb7aaf7472104bbf2 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 fcc4564297b0e76faef9198a100a05ec63d463d3..79795e57d8c7cca0827fa68c43420ad17caab6b5 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 850103caa9d80adacaeb8202a08a38684113cb9f..ff939e4dcc5d458d3e59f5817b00f92d5be389a7 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 df6d157e3b4d0ce6cc2ed20d0eda85c935942e7d..fa455cd3933c5089e7a6cce74431e08579a87be0 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 5830f1aab2e5cdf4acd0c20726ff0bae21e083ad..604b8c34b5d83dc283e26d190aedda62b148174c 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 cb82507988075654da70cda3dd340e4dab5739cd..7a05b0b49d23ec0c4d17832f26cdadc726aa6216 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 61dd75a7ebeabdc40fe8f5e3241709afed215374..cb3944c1aad757656068b55a57642db816bf435f 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 77977eb2aa151312116cc0dd188ffaf4d995a6f0..3bb97657726158427a1c37aae79e395f86e5f7d8 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 bfc1523755fcdc3f1fd961db8924b0e4155141a1..45d1f8689adac8ce7644badcabd0895b82b238aa 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 792c75aa199107bbc5f7a6b6fd626f68d47f7350..7c8b4f355c74b36c4b73dc11fe5ab212ea1a47df 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 0501f1b40fb89b60dc9d9677d2f716f32f59bd69..899c51da745ce3e079738e0952626aff68d7f1bc 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 ebe992a7996fef41a414cd6d072fbf898a00d135..f6f030f8ed044a9e040d85defc6f69238e9ecf17 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 fc920eb1b7b8a027f88a4a976eb87e0964599828..628ef7ffa902cdfff00b9198327b0103dcf2f329 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 eb45a000161d23a55ecacf5c4c62d7fd1587cd7e..73e7af4a1bd06e15a029637be725943085430c02 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 6f1565ab117979dd736d43e32c17918685a86793..858f6abffb8426a1c553b8a5ff391075d1242f2b 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] =