diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a7cf713b6141de847d924750425f5fdcddd4646b..592af2bb38e1478f987c363b5132b205e5fef930 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -21,4 +21,8 @@ jobs:
run: sbt "scalafixAll --check"
- name: Check format
run: sbt scalafmtCheckAll
+ - name: Compile sets
+ run: sbt "lisa-sets / compile"
+ - name: Compile examples
+ run: sbt "lisa-examples / compile"
diff --git a/Reference Manual/kernel.tex b/Reference Manual/kernel.tex
index 11da88b3b34d47ce1e3f29b7a839dfc27e9f3643..8d0fd362bc402a387bb7184d02b7fbbe010358d9 100644
--- a/Reference Manual/kernel.tex
+++ b/Reference Manual/kernel.tex
@@ -69,7 +69,7 @@ Schematic symbols on the other hand, are uninterpreted --- they can represent an
where $\mathcal{L}_{Predicate}$ is the set of \textit{predicate labels}:
%
\begin{align}
- \mathcal{L}_{Predicate} := & ~\ConstantPredicateLabel(\textnormal{Id}, \textnormal{Arity}) \\
+ \mathcal{L}_{Predicate} := & ~\ConstantAtomicLabel(\textnormal{Id}, \textnormal{Arity}) \\
\mid & ~\SchematicPredicateLabel(\textnormal{Id}, \textnormal{Arity})~,
\end{align}
%
@@ -114,11 +114,11 @@ Schematic symbols on the other hand, are uninterpreted --- they can represent an
\end{definition}
\begin{example}[Formula]The following are typical examples of formula labels:
\begin{align*}
- \True & := \ConstantPredicateLabel(``\True", 0) \\
- \False & := \ConstantPredicateLabel(``\False", 0) \\
+ \True & := \ConstantAtomicLabel(``\True", 0) \\
+ \False & := \ConstantAtomicLabel(``\False", 0) \\
X & := \SchematicPredicateLabel(``X", 0) \\
- = & := \ConstantPredicateLabel(``=", 2) \\
- {\in} & := \ConstantPredicateLabel(``{\in}", 2) \\
+ = & := \ConstantAtomicLabel(``=", 2) \\
+ {\in} & := \ConstantAtomicLabel(``{\in}", 2) \\
P & := \SchematicPredicateLabel(``P", 1) \\
\neg & := \ConstantConnectorLabel(``{\neg}", 1) \\
\land & := \ConstantConnectorLabel(``{\land}", -1) \\
@@ -728,7 +728,7 @@ LISA's kernel allows to define two kinds of objects: Function (or Term) symbols
A definition in LISA is one of those two kinds of objects: A predicate definition or a function definition.
\begin{lstlisting}
PredicateDefinition(
- label: ConstantPredicateLabel,
+ label: ConstantAtomicLabel,
expression: LambdaTermFormula
)
\end{lstlisting}
@@ -807,7 +807,7 @@ Once a definition has been introduced, future theorems can refer to those defini
A predicate definition &
\begin{lstlisting}[linewidth=19.5em]
PredicateDefinition(
- label: ConstantPredicateLabel,
+ label: ConstantAtomicLabel,
expression: LambdaTermFormula
)
@@ -861,7 +861,7 @@ Once a definition has been introduced, future theorems can refer to those defini
\makecell[l]{Make a new \\predicate definition} &
\begin{lstlisting}[linewidth=19.5em]
makePredicateDefinition(
- label: ConstantPredicateLabel,
+ label: ConstantAtomicLabel,
expression: LambdaTermFormula
)
\end{lstlisting}
diff --git a/Reference Manual/lisa.pdf b/Reference Manual/lisa.pdf
index eaf56b7b5c01b55cc12b6f2af64db6b51935ed3d..371e8030840fa106d5fd471a92ace6ccf3f6ad19 100644
Binary files a/Reference Manual/lisa.pdf and b/Reference Manual/lisa.pdf differ
diff --git a/Reference Manual/shortcuts.tex b/Reference Manual/shortcuts.tex
index 6518fc5c769a24a909dcd613c0995dcd8fee4434..4f33644a7569c1425107e27dc153cfe06ed14960 100644
--- a/Reference Manual/shortcuts.tex
+++ b/Reference Manual/shortcuts.tex
@@ -4,7 +4,7 @@
\newcommand\ConstantTermLabel{\operatorname{ConstantTermLabel}}
\newcommand\SchematicTermLabel{\operatorname{SchematicTermLabel}}
-\newcommand\ConstantPredicateLabel{\operatorname{ConstantPredicateLabel}}
+\newcommand\ConstantAtomicLabel{\operatorname{ConstantAtomicLabel}}
\newcommand\SchematicPredicateLabel{\operatorname{SchematicPredicateLabel}}
\newcommand\ConstantConnectorLabel{\operatorname{ConstantConnectorLabel}}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index ee35a369898d54ab21fcb5c12c9f8823dd87d49d..dccfed2bfe62df031cbeec89a61f7a1500eb3764 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -80,7 +80,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
private[EquivalenceChecker] var normalForm: Option[NormalFormula] = None
def getNormalForm = normalForm
}
- case class SimplePredicate(id: PredicateLabel, args: Seq[Term], polarity: Boolean) extends SimpleFormula {
+ case class SimplePredicate(id: AtomicLabel, args: Seq[Term], polarity: Boolean) extends SimpleFormula {
override def toString: String = s"SimplePredicate($id, $args, $polarity)"
val size = 1
}
@@ -125,7 +125,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
def recoverFormula: Formula = toFormulaAIG(this)
}
sealed abstract class NonTraversable extends NormalFormula
- case class NormalPredicate(id: PredicateLabel, args: Seq[Term], polarity: Boolean) extends NonTraversable {
+ case class NormalPredicate(id: AtomicLabel, args: Seq[Term], polarity: Boolean) extends NonTraversable {
override def toString: String = s"NormalPredicate($id, $args, $polarity)"
}
case class NormalSchemConnector(id: SchematicConnectorLabel, args: Seq[NormalFormula], polarity: Boolean) extends NonTraversable
@@ -141,7 +141,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
else {
val r: Formula = f match {
case NormalPredicate(id, args, polarity) =>
- if (polarity) PredicateFormula(id, args) else ConnectorFormula(Neg, Seq(PredicateFormula(id, args)))
+ if (polarity) AtomicFormula(id, args) else ConnectorFormula(Neg, Seq(AtomicFormula(id, args)))
case NormalSchemConnector(id, args, polarity) =>
val f = ConnectorFormula(id, args.map(toFormulaAIG))
if (polarity) f else ConnectorFormula(Neg, Seq(f))
@@ -151,7 +151,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
case NormalForall(x, inner, polarity) =>
val f = BinderFormula(Forall, VariableLabel(x), toFormulaAIG(inner))
if (polarity) f else ConnectorFormula(Neg, Seq(f))
- case NormalLiteral(polarity) => if (polarity) PredicateFormula(top, Seq()) else PredicateFormula(bot, Seq())
+ case NormalLiteral(polarity) => if (polarity) AtomicFormula(top, Seq()) else AtomicFormula(bot, Seq())
}
f.formulaAIG = Some(r)
r
@@ -171,7 +171,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
}
val r = f match{
case NormalPredicate(id, args, polarity) =>
- if (positive==polarity) PredicateFormula(id, args) else ConnectorFormula(Neg, Seq(PredicateFormula(id, args)))
+ if (positive==polarity) AtomicFormula(id, args) else ConnectorFormula(Neg, Seq(AtomicFormula(id, args)))
case NormalSchemConnector(id, args, polarity) =>
val f = ConnectorFormula(id, args.map(toFormulaNNF(_, true)))
if (positive==polarity) f else ConnectorFormula(Neg, Seq(f))
@@ -185,7 +185,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
BinderFormula(Forall, VariableLabel(x), toFormulaNNF(inner, true))
else
BinderFormula(Exists, VariableLabel(x), toFormulaNNF(inner, false))
- case NormalLiteral(polarity) => if (polarity) PredicateFormula(top, Seq()) else PredicateFormula(bot, Seq())
+ case NormalLiteral(polarity) => if (polarity) AtomicFormula(top, Seq()) else AtomicFormula(bot, Seq())
}
if (positive) f.formulaP = Some(r)
else f.formulaN = Some(r)
@@ -246,7 +246,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
getInversePolar(f.polarFormula.get)
} else {
val r = f match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
if (label == top) SimpleLiteral(polarity)
else if (label == bot) SimpleLiteral(!polarity)
else SimplePredicate(label, args, polarity)
@@ -279,7 +279,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
case Exists => SimpleForall(bound.id, polarize(inner, false), !polarity)
case ExistsOne =>
val y = VariableLabel(freshId(inner.freeVariables.map(_.id), bound.id))
- val c = PredicateFormula(equality, Seq(VariableTerm(bound), VariableTerm(y)))
+ val c = AtomicFormula(equality, Seq(VariableTerm(bound), VariableTerm(y)))
val newInner = polarize(ConnectorFormula(Iff, Seq(c, inner)), true)
SimpleForall(y.id, SimpleForall(bound.id, newInner, false), !polarity)
}
@@ -489,7 +489,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
// transform a LISA formula into a simpler, desugarised version with less symbols. Conjunction, implication, iff, existsOne are treated as alliases and translated.
def removeSugar1(phi: Formula): PolarFormula = {
phi match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
if (label == top) PolarLiteral(true)
else if (label == bot) PolarLiteral(false)
else PolarPredicate(label, args.toList)
@@ -627,8 +627,8 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
val r: List[NormalFormula] = phi match {
case PolarPredicate(label, args) =>
val lab = label match {
- case _: ConstantPredicateLabel => "cp_" + label.id + "_" + label.arity
- case _: SchematicVarOrPredLabel => "sp_" + label.id + "_" + label.arity
+ case _: ConstantAtomicLabel => "cp_" + label.id + "_" + label.arity
+ case _: SchematicAtomicLabel => "sp_" + label.id + "_" + label.arity
}
if (label == top) {
phi.normalForm = Some(NLiteral(true))
@@ -675,8 +675,8 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
val r: List[NormalFormula] = phi match {
case PolarPredicate(label, args) =>
val lab = label match {
- case _: ConstantPredicateLabel => "cp_" + label.id + "_" + label.arity
- case _: SchematicVarOrPredLabel => "sp_" + label.id + "_" + label.arity
+ case _: ConstantAtomicLabel => "cp_" + label.id + "_" + label.arity
+ case _: SchematicAtomicLabel => "sp_" + label.id + "_" + label.arity
}
if (label == top) {
phi.normalForm = Some(NLiteral(true))
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 4ff7416bdb0ef4ce3fc76d386999add986cbeb0f..192460cef0720730e79aa50cc2c7df627cd13afb 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -33,12 +33,12 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
/**
* @return The list of constant predicate symbols in the formula.
*/
- def constantPredicateLabels: Set[ConstantPredicateLabel]
+ def constantAtomicLabels: Set[ConstantAtomicLabel]
/**
* @return The list of schematic predicate symbols in the formula, including variable formulas .
*/
- def schematicPredicateLabels: Set[SchematicVarOrPredLabel]
+ def schematicAtomicLabels: Set[SchematicAtomicLabel]
/**
* @return The list of schematic connector symbols in the formula.
@@ -49,7 +49,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* @return The list of schematic connector, predicate and formula variable symbols in the formula.
*/
def schematicFormulaLabels: Set[SchematicFormulaLabel] =
- (schematicPredicateLabels.toSet: Set[SchematicFormulaLabel]) union (schematicConnectorLabels.toSet: Set[SchematicFormulaLabel])
+ (schematicAtomicLabels.toSet: Set[SchematicFormulaLabel]) union (schematicConnectorLabels.toSet: Set[SchematicFormulaLabel])
/**
* @return The list of free formula variable symbols in the formula
@@ -66,9 +66,9 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
}
/**
- * The formula counterpart of [[PredicateLabel]].
+ * The formula counterpart of [[AtomicLabel]].
*/
- sealed case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
+ sealed case class AtomicFormula(label: AtomicLabel, args: Seq[Term]) extends Formula {
require(label.arity == args.size)
override def constantTermLabels: Set[ConstantFunctionLabel] =
args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantTermLabels)
@@ -78,12 +78,12 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
args.foldLeft(Set.empty[SchematicTermLabel])((prev, next) => prev union next.freeSchematicTermLabels)
override def freeVariables: Set[VariableLabel] =
args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
- override def constantPredicateLabels: Set[ConstantPredicateLabel] = label match {
- case l: ConstantPredicateLabel => Set(l)
+ override def constantAtomicLabels: Set[ConstantAtomicLabel] = label match {
+ case l: ConstantAtomicLabel => Set(l)
case _ => Set()
}
- override def schematicPredicateLabels: Set[SchematicVarOrPredLabel] = label match {
- case l: SchematicVarOrPredLabel => Set(l)
+ override def schematicAtomicLabels: Set[SchematicAtomicLabel] = label match {
+ case l: SchematicAtomicLabel => Set(l)
case _ => Set()
}
override def schematicConnectorLabels: Set[SchematicConnectorLabel] = Set()
@@ -108,10 +108,10 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
args.foldLeft(Set.empty[SchematicTermLabel])((prev, next) => prev union next.freeSchematicTermLabels)
override def freeVariables: Set[VariableLabel] =
args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
- override def constantPredicateLabels: Set[ConstantPredicateLabel] =
- args.foldLeft(Set.empty[ConstantPredicateLabel])((prev, next) => prev union next.constantPredicateLabels)
- override def schematicPredicateLabels: Set[SchematicVarOrPredLabel] =
- args.foldLeft(Set.empty[SchematicVarOrPredLabel])((prev, next) => prev union next.schematicPredicateLabels)
+ override def constantAtomicLabels: Set[ConstantAtomicLabel] =
+ args.foldLeft(Set.empty[ConstantAtomicLabel])((prev, next) => prev union next.constantAtomicLabels)
+ override def schematicAtomicLabels: Set[SchematicAtomicLabel] =
+ args.foldLeft(Set.empty[SchematicAtomicLabel])((prev, next) => prev union next.schematicAtomicLabels)
override def schematicConnectorLabels: Set[SchematicConnectorLabel] = label match {
case l: ConstantConnectorLabel =>
args.foldLeft(Set.empty[SchematicConnectorLabel])((prev, next) => prev union next.schematicConnectorLabels)
@@ -130,8 +130,8 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
override def schematicTermLabels: Set[SchematicTermLabel] = inner.schematicTermLabels
override def freeSchematicTermLabels: Set[SchematicTermLabel] = inner.freeSchematicTermLabels - bound
override def freeVariables: Set[VariableLabel] = inner.freeVariables - bound
- override def constantPredicateLabels: Set[ConstantPredicateLabel] = inner.constantPredicateLabels
- override def schematicPredicateLabels: Set[SchematicVarOrPredLabel] = inner.schematicPredicateLabels
+ override def constantAtomicLabels: Set[ConstantAtomicLabel] = inner.constantAtomicLabels
+ override def schematicAtomicLabels: Set[SchematicAtomicLabel] = inner.schematicAtomicLabels
override def schematicConnectorLabels: Set[SchematicConnectorLabel] = inner.schematicConnectorLabels
override def freeVariableFormulaLabels: Set[VariableFormulaLabel] = inner.freeVariableFormulaLabels
}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index d7245a1508bc946f6f94402c7eadcc07388eb305..61e7507746d4b0f65d87b4b4fcdcd1ecf98868d7 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -16,7 +16,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
* The label for a predicate, namely a function taking a fixed number of terms and returning a formula.
* In logical terms it is a predicate symbol.
*/
- sealed trait PredicateLabel extends FormulaLabel {
+ sealed trait AtomicLabel extends FormulaLabel {
require(arity < MaxArity && arity >= 0)
}
@@ -30,15 +30,15 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
/**
* A standard predicate symbol. Typical example are equality (=) and membership (∈)
*/
- sealed case class ConstantPredicateLabel(id: Identifier, arity: Int) extends PredicateLabel with ConstantLabel
+ sealed case class ConstantAtomicLabel(id: Identifier, arity: Int) extends AtomicLabel with ConstantLabel
/**
* The equality symbol (=) for first order logic.
* It is represented as any other predicate symbol but has unique semantic and deduction rules.
*/
- val equality: ConstantPredicateLabel = ConstantPredicateLabel(Identifier("="), 2)
- val top: ConstantPredicateLabel = ConstantPredicateLabel(Identifier("⊤"), 0)
- val bot: ConstantPredicateLabel = ConstantPredicateLabel(Identifier("⊥"), 0)
+ val equality: ConstantAtomicLabel = ConstantAtomicLabel(Identifier("="), 2)
+ val top: ConstantAtomicLabel = ConstantAtomicLabel(Identifier("⊤"), 0)
+ val bot: ConstantAtomicLabel = ConstantAtomicLabel(Identifier("⊥"), 0)
/**
* The label for a connector, namely a function taking a fixed number of formulas and returning another formula.
@@ -63,19 +63,19 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
/**
* A schematic symbol whose arguments are any number of Terms. This means the symbol is either a variable formula or a predicate schema
*/
- sealed trait SchematicVarOrPredLabel extends SchematicFormulaLabel with PredicateLabel
+ sealed trait SchematicAtomicLabel extends SchematicFormulaLabel with AtomicLabel
/**
* A predicate symbol of arity 0 that can be instantiated with any formula.
*/
- sealed case class VariableFormulaLabel(id: Identifier) extends SchematicVarOrPredLabel {
+ sealed case class VariableFormulaLabel(id: Identifier) extends SchematicAtomicLabel {
val arity = 0
}
/**
* A predicate symbol of non-zero arity that can be instantiated with any functional formula taking term arguments.
*/
- sealed case class SchematicPredicateLabel(id: Identifier, arity: Int) extends SchematicVarOrPredLabel
+ sealed case class SchematicPredicateLabel(id: Identifier, arity: Int) extends SchematicAtomicLabel
/**
* A predicate symbol of non-zero arity that can be instantiated with any functional formula taking formula arguments.
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
index eec5e3ec61999a3e9d14545d09b3d3c473138066..f3f04bc26dde398a1c1b3b6793383dfa46cab02a 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -88,7 +88,7 @@ trait Substitutions extends FormulaDefinitions {
* @return t[m]
*/
def substituteVariablesInFormula(phi: Formula, m: Map[VariableLabel, Term], takenIds: Seq[Identifier] = Seq[Identifier]()): Formula = phi match {
- case PredicateFormula(label, args) => PredicateFormula(label, args.map(substituteVariablesInTerm(_, m)))
+ case AtomicFormula(label, args) => AtomicFormula(label, args.map(substituteVariablesInTerm(_, m)))
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(substituteVariablesInFormula(_, m)))
case BinderFormula(label, bound, inner) =>
val newSubst = m - bound
@@ -109,8 +109,8 @@ trait Substitutions extends FormulaDefinitions {
* @return t[m]
*/
def substituteFormulaVariables(phi: Formula, m: Map[VariableFormulaLabel, Formula], takenIds: Seq[Identifier] = Seq[Identifier]()): Formula = phi match {
- case PredicateFormula(label: VariableFormulaLabel, _) => m.getOrElse(label, phi)
- case _: PredicateFormula => phi
+ case AtomicFormula(label: VariableFormulaLabel, _) => m.getOrElse(label, phi)
+ case _: AtomicFormula => phi
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(substituteFormulaVariables(_, m, takenIds)))
case BinderFormula(label, bound, inner) =>
val fv = m.values.flatMap(_.freeVariables).toSet
@@ -132,7 +132,7 @@ trait Substitutions extends FormulaDefinitions {
def instantiateTermSchemas(phi: Formula, m: Map[SchematicTermLabel, LambdaTermTerm]): Formula = {
require(m.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity })
phi match {
- case PredicateFormula(label, args) => PredicateFormula(label, args.map(a => instantiateTermSchemasInTerm(a, m)))
+ case AtomicFormula(label, args) => AtomicFormula(label, args.map(a => instantiateTermSchemasInTerm(a, m)))
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateTermSchemas(_, m)))
case BinderFormula(label, bound, inner) =>
val newSubst = m - bound
@@ -152,12 +152,12 @@ trait Substitutions extends FormulaDefinitions {
* @param m The map from schematic predicate symbols to lambda expressions Term(s) -> Formula [[LambdaTermFormula]].
* @return phi[m]
*/
- def instantiatePredicateSchemas(phi: Formula, m: Map[SchematicVarOrPredLabel, LambdaTermFormula]): Formula = {
+ def instantiatePredicateSchemas(phi: Formula, m: Map[SchematicAtomicLabel, LambdaTermFormula]): Formula = {
require(m.forall { case (symbol, LambdaTermFormula(arguments, body)) => arguments.length == symbol.arity })
phi match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
label match {
- case label: SchematicVarOrPredLabel if m.contains(label) => m(label)(args)
+ case label: SchematicAtomicLabel if m.contains(label) => m(label)(args)
case _ => phi
}
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchemas(_, m)))
@@ -181,7 +181,7 @@ trait Substitutions extends FormulaDefinitions {
def instantiateConnectorSchemas(phi: Formula, m: Map[SchematicConnectorLabel, LambdaFormulaFormula]): Formula = {
require(m.forall { case (symbol, LambdaFormulaFormula(arguments, body)) => arguments.length == symbol.arity })
phi match {
- case _: PredicateFormula => phi
+ case _: AtomicFormula => phi
case ConnectorFormula(label, args) =>
val newArgs = args.map(instantiateConnectorSchemas(_, m))
label match {
@@ -208,18 +208,18 @@ trait Substitutions extends FormulaDefinitions {
def instantiateSchemas(
phi: Formula,
mCon: Map[SchematicConnectorLabel, LambdaFormulaFormula],
- mPred: Map[SchematicVarOrPredLabel, LambdaTermFormula],
+ mPred: Map[SchematicAtomicLabel, LambdaTermFormula],
mTerm: Map[SchematicTermLabel, LambdaTermTerm]
): Formula = {
require(mCon.forall { case (symbol, LambdaFormulaFormula(arguments, body)) => arguments.length == symbol.arity })
require(mPred.forall { case (symbol, LambdaTermFormula(arguments, body)) => arguments.length == symbol.arity })
require(mTerm.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity })
phi match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
val newArgs = args.map(a => instantiateTermSchemasInTerm(a, mTerm))
label match {
- case label: SchematicVarOrPredLabel if mPred.contains(label) => mPred(label)(newArgs)
- case _ => PredicateFormula(label, newArgs)
+ case label: SchematicAtomicLabel if mPred.contains(label) => mPred(label)(newArgs)
+ case _ => AtomicFormula(label, newArgs)
}
case ConnectorFormula(label, args) =>
val newArgs = args.map(a => instantiateSchemas(a, mCon, mPred, mTerm))
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index b8bd954ed436b3e17281a1f335f62dea97b55fb3..8167d9f7a7f1efae36fa7f30f5e3e43c7bc39c41 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -45,7 +45,7 @@ class RunningTheory {
* @param label The name and arity of the new symbol
* @param expression The formula, depending on terms, that define the symbol.
*/
- sealed case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, expression: LambdaTermFormula) extends Definition
+ sealed case class PredicateDefinition private[RunningTheory] (label: ConstantAtomicLabel, expression: LambdaTermFormula) extends Definition
/**
* Define a function symbol as the unique element that has some property. The existence and uniqueness
@@ -63,7 +63,7 @@ class RunningTheory {
private[proof] val theorems: mMap[String, Theorem] = mMap.empty
private[proof] val funDefinitions: mMap[ConstantFunctionLabel, Option[FunctionDefinition]] = mMap.empty
- private[proof] val predDefinitions: mMap[ConstantPredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None, top -> None, bot -> None)
+ private[proof] val predDefinitions: mMap[ConstantAtomicLabel, Option[PredicateDefinition]] = mMap(equality -> None, top -> None, bot -> None)
private[proof] val knownSymbols: mMap[Identifier, ConstantLabel] = mMap(equality.id -> equality)
@@ -113,11 +113,11 @@ class RunningTheory {
* @param expression The functional formula defining the predicate.
* @return A definition object if the parameters are correct,
*/
- def makePredicateDefinition(label: ConstantPredicateLabel, expression: LambdaTermFormula): RunningTheoryJudgement[this.PredicateDefinition] = {
+ def makePredicateDefinition(label: ConstantAtomicLabel, expression: LambdaTermFormula): RunningTheoryJudgement[this.PredicateDefinition] = {
val LambdaTermFormula(vars, body) = expression
if (belongsToTheory(body))
if (isAvailable(label))
- if (body.freeSchematicTermLabels.subsetOf(vars.toSet) && body.schematicPredicateLabels.isEmpty) {
+ if (body.freeSchematicTermLabels.subsetOf(vars.toSet) && body.schematicAtomicLabels.isEmpty) {
val newDef = PredicateDefinition(label, expression)
predDefinitions.update(label, Some(newDef))
knownSymbols.update(label.id, label)
@@ -196,7 +196,7 @@ class RunningTheory {
case Theorem(name, proposition, _) => proposition
case Axiom(name, ax) => Sequent(Set.empty, Set(ax))
case PredicateDefinition(label, LambdaTermFormula(vars, body)) =>
- val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, vars.map(VariableTerm.apply)), body))
+ val inner = ConnectorFormula(Iff, Seq(AtomicFormula(label, vars.map(VariableTerm.apply)), body))
Sequent(Set(), Set(inner))
case FunctionDefinition(label, out, LambdaTermFormula(vars, body), _) =>
val inner = BinderFormula(
@@ -205,7 +205,7 @@ class RunningTheory {
ConnectorFormula(
Iff,
Seq(
- PredicateFormula(equality, Seq(Term(label, vars.map(VariableTerm.apply)), VariableTerm(out))),
+ AtomicFormula(equality, Seq(Term(label, vars.map(VariableTerm.apply)), VariableTerm(out))),
body
)
)
@@ -242,7 +242,7 @@ class RunningTheory {
knownSymbols.update(s.id, s)
s match {
case c: ConstantFunctionLabel => funDefinitions.update(c, None)
- case c: ConstantPredicateLabel => predDefinitions.update(c, None)
+ case c: ConstantAtomicLabel => predDefinitions.update(c, None)
}
} else {}
}
@@ -251,7 +251,7 @@ class RunningTheory {
* Add all constant symbols in the sequent. Note that this can't be reversed and will prevent from giving them a definition later.
*/
def makeFormulaBelongToTheory(phi: Formula): Unit = {
- phi.constantPredicateLabels.foreach(addSymbol)
+ phi.constantAtomicLabels.foreach(addSymbol)
phi.constantTermLabels.foreach(addSymbol)
}
@@ -270,9 +270,9 @@ class RunningTheory {
* @return Weather phi belongs to the specified language
*/
def belongsToTheory(phi: Formula): Boolean = phi match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
label match {
- case l: ConstantPredicateLabel => isSymbol(l) && args.forall(belongsToTheory)
+ case l: ConstantAtomicLabel => isSymbol(l) && args.forall(belongsToTheory)
case _ => args.forall(belongsToTheory)
}
case ConnectorFormula(label, args) => args.forall(belongsToTheory)
@@ -315,7 +315,7 @@ class RunningTheory {
*/
def isSymbol(label: ConstantLabel): Boolean = label match {
case c: ConstantFunctionLabel => funDefinitions.contains(c)
- case c: ConstantPredicateLabel => predDefinitions.contains(c)
+ case c: ConstantAtomicLabel => predDefinitions.contains(c)
}
/**
@@ -344,7 +344,7 @@ class RunningTheory {
/**
* Get the definition of the given label, if it is defined in the theory.
*/
- def getDefinition(label: ConstantPredicateLabel): Option[PredicateDefinition] = predDefinitions.get(label).flatten
+ def getDefinition(label: ConstantAtomicLabel): Option[PredicateDefinition] = predDefinitions.get(label).flatten
/**
* Get the definition of the given label, if it is defined in the theory.
@@ -365,7 +365,7 @@ class RunningTheory {
* Get the definition for the given identifier, if it is defined in the theory.
*/
def getDefinition(name: Identifier): Option[Definition] = knownSymbols.get(name).flatMap {
- case f: ConstantPredicateLabel => getDefinition(f)
+ case f: ConstantAtomicLabel => getDefinition(f)
case f: ConstantFunctionLabel => getDefinition(f)
}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 08ea38d49097d97b98bf24b4c714e69523b60432..a4c89b54bef12937c5f6165e31d543298eeba909 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -42,7 +42,7 @@ object SCProofChecker {
* Γ |- Γ
*/
case RestateTrue(s) =>
- val truth = Sequent(Set(), Set(PredicateFormula(top, Nil)))
+ val truth = Sequent(Set(), Set(AtomicFormula(top, Nil)))
if (isSameSequent(s, truth)) SCValidProof(SCProof(step)) else SCInvalidProof(SCProof(step), Nil, s"The desired conclusion is not a trivial tautology")
/*
*
@@ -180,7 +180,7 @@ object SCProofChecker {
*/
case LeftExistsOne(b, t1, phi, x) =>
val y = VariableLabel(freshId(phi.freeVariables.map(_.id), x.id))
- val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+ val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(AtomicFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + temp, ref(t1).left + BinderFormula(ExistsOne, x, phi)))
SCValidProof(SCProof(step))
@@ -296,7 +296,7 @@ object SCProofChecker {
*/
case RightExistsOne(b, t1, phi, x) =>
val y = VariableLabel(freshId(phi.freeVariables.map(_.id), x.id))
- val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+ val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(AtomicFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + temp, ref(t1).right + BinderFormula(ExistsOne, x, phi)))
SCValidProof(SCProof(step))
@@ -322,7 +322,7 @@ object SCProofChecker {
*/
case LeftRefl(b, t1, phi) =>
phi match {
- case PredicateFormula(`equality`, Seq(left, right)) =>
+ case AtomicFormula(`equality`, Seq(left, right)) =>
if (isSameTerm(left, right))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left))
@@ -340,7 +340,7 @@ object SCProofChecker {
*/
case RightRefl(b, phi) =>
phi match {
- case PredicateFormula(`equality`, Seq(left, right)) =>
+ case AtomicFormula(`equality`, Seq(left, right)) =>
if (isSameTerm(left, right))
if (contains(b.right, phi))
SCValidProof(SCProof(step))
@@ -358,7 +358,7 @@ object SCProofChecker {
val (s_es, t_es) = equals.unzip
val phi_s_for_f = lambdaPhi(s_es)
val phi_t_for_f = lambdaPhi(t_es)
- val sEqT_es = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
+ val sEqT_es = equals map { case (s, t) => AtomicFormula(equality, Seq(s, t)) }
if (isSameSet(b.right, ref(t1).right))
if (
@@ -380,7 +380,7 @@ object SCProofChecker {
* Γ, (s=t)_ |- φ(t_), Δ
*/
case RightSubstEq(b, t1, equals, lambdaPhi) =>
- val sEqT_es = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
+ val sEqT_es = equals map { case (s, t) => AtomicFormula(equality, Seq(s, t)) }
if (isSameSet(ref(t1).left ++ sEqT_es, b.left)) {
val (s_es, t_es) = equals.unzip
val phi_s_for_f = lambdaPhi(s_es)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index 44e8df4b86d22104cd5b8f707da15e514fe8e817..d089f29a421214a61b5c4c3449a4a1a238c1eb60 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -317,7 +317,7 @@ object SequentCalculus {
bot: Sequent,
t1: Int,
mCon: Map[SchematicConnectorLabel, LambdaFormulaFormula],
- mPred: Map[SchematicVarOrPredLabel, LambdaTermFormula],
+ mPred: Map[SchematicAtomicLabel, LambdaTermFormula],
mTerm: Map[SchematicTermLabel, LambdaTermTerm]
) extends SCProofStep { val premises = Seq(t1) }
diff --git a/lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala b/lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala
index 27dec673f87586773f700f4e58f504d7e423eba8..12c9f70f44a7e0c43bcaac7bf46b39a146b5e297 100644
--- a/lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala
+++ b/lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala
@@ -249,7 +249,7 @@ object SetTheoryLibrary extends lisa.prooflib.Library {
def ∈(that: Term): Formula = in(thi, that)
def ⊆(that: Term): Formula = subset(thi, that)
- def =/=(that: Term): Formula = !(===(thi, that))
+ def =/=(that: Term): Formula = !(thi === that)
}
diff --git a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
index 81b299ca867b5d09c74b427a4aef67ba5b49efd6..6de053d76693ba36dbbe031267d3faf66214aab4 100644
--- a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
@@ -110,10 +110,10 @@ object CommonTactics {
// Infer y from the equalities in the uniqueness sequent
uniquenessSeq.right.collectFirst {
- case F.PredicateFormula(F.`equality`, Seq(`x`, (y: F.Variable))) if x != y && F.contains(uniquenessSeq.left, phi.substitute(x := y)) =>
+ case F.AppliedPredicate(F.`equality`, Seq(`x`, (y: F.Variable))) if x != y && F.contains(uniquenessSeq.left, phi.substitute(x := y)) =>
y
- case F.PredicateFormula(F.`equality`, List(F.AppliedTerm(y: F.Variable, _), F.AppliedTerm(`x`, _))) if x != y && F.contains(uniquenessSeq.left, phi.substitute(x := y)) =>
+ case F.AppliedPredicate(F.`equality`, List(F.AppliedFunction(y: F.Variable, _), F.AppliedFunction(`x`, _))) if x != y && F.contains(uniquenessSeq.left, phi.substitute(x := y)) =>
y
} match {
case Some(y) => ExistenceAndUniqueness.withParameters(phi, x, y)(existence, uniqueness)(bot)
@@ -144,11 +144,11 @@ object CommonTactics {
case _ => return proof.InvalidProofTactic("Could not get definition of function.")
}
val method = expr.f.substituteUnsafe(expr.vars.zip(xs).toMap) match {
- case F.ConnectorFormula(
+ case F.AppliedConnector(
F.And,
Seq(
- F.ConnectorFormula(F.Implies, Seq(a, _)),
- F.ConnectorFormula(F.Implies, Seq(b, _))
+ F.AppliedConnector(F.Implies, Seq(a, _)),
+ F.AppliedConnector(F.Implies, Seq(b, _))
)
) if F.isSame(F.Neg(a), b) =>
conditional
@@ -173,20 +173,21 @@ object CommonTactics {
}
val y = definition.out
val vars = definition.vars
+ val fxs = f.applyUnsafe(xs)
// Instantiate terms in the definition
val subst = vars.zip(xs).map(tup => tup._1 := tup._2)
val P = definition.f.substitute(subst: _*)
- val expected = P.substitute(y := f(xs))
+ 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 === f(xs)) <=> P)) by Tautology.from(uniqueness, definition.of(subst: _*))
- lib.thenHave((y === f(xs)) <=> P) by InstantiateForall(y)
- lib.thenHave((f(xs) === f(xs)) <=> P.substitute(y := f(xs))) by InstFunSchema(Map(y -> f(xs)))
- lib.thenHave(P.substitute(y := f(xs))) by Restate
+ 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
}
case _ => proof.InvalidProofTactic("Could not get definition of function.")
@@ -223,11 +224,11 @@ object CommonTactics {
// Unfold the conditional definition to find Q
val phi = F.And(bot.left.toSeq)
val Q: F.LambdaExpression[F.Term, F.Formula, 1] = P.body match {
- case F.ConnectorFormula(
+ case F.AppliedConnector(
F.And,
Seq(
- F.ConnectorFormula(F.Implies, Seq(a, f)),
- F.ConnectorFormula(F.Implies, Seq(b, g))
+ F.AppliedConnector(F.Implies, Seq(a, f)),
+ F.AppliedConnector(F.Implies, Seq(b, g))
)
) if F.isSame(F.Neg(a), b) =>
if (F.isSame(a, phi)) F.lambda(y, f)
@@ -238,18 +239,20 @@ object CommonTactics {
return proof.InvalidProofTactic("Definition is not conditional.")
}
- val expected = P.substitute(y := f(xs))
+ val fxs = f.applyUnsafe(xs)
+
+ 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 Q(f(xs)).")
+ return proof.InvalidProofTactic("Right-hand side of bottom sequent should be of the form Q(fxs).")
}
TacticSubproof {
- lib.have(F.∀(y, (y === f(xs)) <=> P(Seq(y)))) by Tautology.from(uniqueness, definition.of(subst: _*))
- lib.thenHave((y === f(xs)) <=> P(Seq(y))) by InstantiateForall(y)
- lib.thenHave((f(xs) === f(xs)) <=> P(Seq(f(xs)))) by InstFunSchema(Map(y -> f(xs)))
- lib.thenHave(P(Seq(f(xs)))) by Restate
- lib.thenHave(phi ==> Q(Seq(f(xs)))) by Tautology
- lib.thenHave(phi |- Q(Seq(f(xs)))) by Restate
+ 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
+ lib.thenHave(phi ==> Q(fxs)) by Tautology
+ lib.thenHave(phi |- Q(fxs)) by Restate
}
case _ => proof.InvalidProofTactic("Could not get definition of function.")
diff --git a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
index 31d7fad9104052e95131a0a9145e3ae2d722d86f..c5fd1620389878222dead2a862083d6c1cfb9290 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
@@ -87,28 +87,28 @@ object Substitution {
substitutions.foreach {
case f: F.Formula =>
f match {
- case F.PredicateFormula(F.equality, Seq(l, r)) =>
+ case F.AppliedPredicate(F.equality, Seq(l, r)) =>
confinedEqualitiesPre = (l, r) :: confinedEqualitiesPre
- case F.ConnectorFormula(F.Iff, Seq(l, r)) =>
+ case F.AppliedConnector(F.Iff, Seq(l, r)) =>
confinedIffsPre = (l, r) :: confinedIffsPre
case _ => ()
}
case j: lib.JUSTIFICATION =>
j.statement.right.head match {
- case F.PredicateFormula(F.equality, Seq(l, r)) =>
+ case F.AppliedPredicate(F.equality, Seq(l, r)) =>
updateSource((l, r), j)
freeEqualitiesPre = (l, r) :: freeEqualitiesPre
- case F.ConnectorFormula(F.Iff, Seq(l, r)) =>
+ case F.AppliedConnector(F.Iff, Seq(l, r)) =>
updateSource((l, r), j)
freeIffsPre = (l, r) :: freeIffsPre
case _ => ()
}
case f: proof.Fact @unchecked =>
proof.sequentOfFact(f).right.head match {
- case F.PredicateFormula(F.equality, Seq(l, r)) =>
+ case F.AppliedPredicate(F.equality, Seq(l, r)) =>
updateSource((l, r), f)
confinedEqualitiesPre = (l, r) :: confinedEqualitiesPre
- case F.ConnectorFormula(F.Iff, Seq(l, r)) =>
+ case F.AppliedConnector(F.Iff, Seq(l, r)) =>
updateSource((l, r), f)
confinedIffsPre = (l, r) :: confinedIffsPre
case _ => ()
@@ -122,14 +122,14 @@ object Substitution {
val confinedIffs: List[(F.Formula, F.Formula)] = confinedIffsPre ++ confinedIffsPre.map(_.swap)
val filteredPrem: Seq[F.Formula] = (premiseSequent.left filter {
- case F.PredicateFormula(F.equality, Seq(l, r)) if freeEqualities.contains((l, r)) || confinedEqualities.contains((l, r)) => false
- case F.ConnectorFormula(F.Iff, Seq(l, r)) if freeIffs.contains((l, r)) || confinedIffs.contains((l, r)) => false
+ case F.AppliedPredicate(F.equality, Seq(l, r)) if freeEqualities.contains((l, r)) || confinedEqualities.contains((l, r)) => false
+ case F.AppliedConnector(F.Iff, Seq(l, r)) if freeIffs.contains((l, r)) || confinedIffs.contains((l, r)) => false
case _ => true
}).toSeq
val filteredBot: Seq[F.Formula] = (bot.left filter {
- case F.PredicateFormula(F.equality, Seq(l, r)) if freeEqualities.contains((l, r)) || confinedEqualities.contains((l, r)) => false
- case F.ConnectorFormula(F.Iff, Seq(l, r)) if freeIffs.contains((l, r)) || confinedIffs.contains((l, r)) => false
+ case F.AppliedPredicate(F.equality, Seq(l, r)) if freeEqualities.contains((l, r)) || confinedEqualities.contains((l, r)) => false
+ case F.AppliedConnector(F.Iff, Seq(l, r)) if freeIffs.contains((l, r)) || confinedIffs.contains((l, r)) => false
case _ => true
}).toSeq
@@ -167,15 +167,15 @@ object Substitution {
// actually construct proof
TacticSubproof {
- def eq(rule: (Term, Term)) = PredicateFormula(equality, Seq(rule._1, rule._2))
- def iff(rule: (Formula, Formula)) = ConnectorFormula(Iff, Seq(rule._1, rule._2))
+ def eq(rule: (Term, Term)) = AppliedPredicate(equality, Seq(rule._1, rule._2))
+ def iff(rule: (Formula, Formula)) = AppliedConnector(Iff, Seq(rule._1, rule._2))
def eqSource(rule: (Term, Term)) = lib.have(eq(rule) |- eq(rule)) by SimpleDeducedSteps.Restate
def iffSource(rule: (Formula, Formula)) = lib.have(iff(rule) |- iff(rule)) by SimpleDeducedSteps.Restate
val leftContexts: Seq[UnificationUtils.FormulaRewriteLambda] = leftContextsOpt.get // remove the options
val rightContexts: Seq[UnificationUtils.FormulaRewriteLambda] = rightContextsOpt.get // remove the options
- val leftBody = ConnectorFormula(And, leftContexts.map(f => f.body))
+ val leftBody = AppliedConnector(And, leftContexts.map(f => f.body))
val defaultLeft = UnificationUtils.FormulaRewriteLambda(body = leftBody)
@@ -187,7 +187,7 @@ object Substitution {
)
}
- val rightBody = ConnectorFormula(Or, rightContexts.map(f => f.body))
+ val rightBody = AppliedConnector(Or, rightContexts.map(f => f.body))
val defaultRight = UnificationUtils.FormulaRewriteLambda(body = rightBody)
@@ -274,7 +274,7 @@ object Substitution {
val (formulaInputsL, formulaInputsR) = (formulaInputs.map(_._1), formulaInputs.map(_._2))
// get premise into the right form
- val prem = ConnectorFormula(And, filteredPrem.toSeq) |- ConnectorFormula(Or, premiseSequent.right.toSeq)
+ val prem = AppliedConnector(And, filteredPrem.toSeq) |- AppliedConnector(Or, premiseSequent.right.toSeq)
val eqs = termInputs.map(eq(_))
val iffs = formulaInputs.map(iff(_))
val premiseWithSubst = prem ++<< (eqs |- ()) ++<< (iffs |- ())
@@ -383,7 +383,8 @@ object Substitution {
else {
val induct = condflat(t.args.map(te => findSubterm2(te, subs)))
if (!induct._2) (t, false)
- else (t.label(induct._1), true)
+ else
+ (t.label.applySeq(induct._1), true)
}
@@ -392,14 +393,14 @@ object Substitution {
f match {
case f: VariableFormula => (f, false)
case f: ConstantFormula => (f, false)
- case PredicateFormula(label, args) =>
+ case AppliedPredicate(label, args) =>
val induct = condflat(args.map(findSubterm2(_, subs)))
if (!induct._2) (f, false)
- else (PredicateFormula(label, induct._1), true)
- case ConnectorFormula(label, args) =>
+ else (AppliedPredicate(label, induct._1), true)
+ case AppliedConnector(label, args) =>
val induct = condflat(args.map(findSubterm2(_, subs)))
if (!induct._2) (f, false)
- else (ConnectorFormula(label, induct._1), true)
+ else (AppliedConnector(label, induct._1), true)
case BinderFormula(label, bound, inner) =>
val fv_in_f = subs.flatMap(e => e._2.freeVariables + e._1)
if (!fv_in_f.contains(bound)) {
@@ -422,10 +423,10 @@ object Substitution {
else
f match {
case f: AtomicFormula => (f, false)
- case ConnectorFormula(label, args) =>
+ case AppliedConnector(label, args) =>
val induct = condflat(args.map(findSubformula2(_, subs)))
if (!induct._2) (f, false)
- else (ConnectorFormula(label, induct._1), true)
+ else (AppliedConnector(label, induct._1), true)
case BinderFormula(label, bound, inner) =>
val fv_in_f = subs.flatMap(_._2.freeVariables)
if (!fv_in_f.contains(bound)) {
@@ -468,13 +469,13 @@ object Substitution {
)(premise: proof.Fact)(rightLeft: Boolean = false, toLeft: Boolean = true, toRight: Boolean = true): proof.ProofTacticJudgement = {
import lisa.utils.K
val originSequent = proof.getSequent(premise)
- val leftOrigin = ConnectorFormula(And, originSequent.left.toSeq)
- val rightOrigin = ConnectorFormula(Or, originSequent.right.toSeq)
+ val leftOrigin = AppliedConnector(And, originSequent.left.toSeq)
+ val rightOrigin = AppliedConnector(Or, originSequent.right.toSeq)
if (!toLeft && !toRight) return proof.InvalidProofTactic("applyLeftRight called with no substitution selected (toLeft or toRight).")
phi match {
- case PredicateFormula(label, args) if label == equality =>
+ case AppliedPredicate(label, args) if label == equality =>
val left = args(0)
val right = args(1)
val fv_in_phi = (originSequent.left ++ originSequent.right).flatMap(_.allSchematicLabels).map(_.id)
@@ -490,12 +491,12 @@ object Substitution {
case v: proof.ValidProofTactic => return v
}
- val leftForm = ConnectorFormula(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val rightForm = ConnectorFormula(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val newleft = if (toLeft) isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.left
- val newright = if (toRight) isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.right
- val result1: Sequent = (ConnectorFormula(And, newleft.toSeq), phi) |- rightOrigin
- val result2: Sequent = result1.left |- ConnectorFormula(Or, newright.toSeq)
+ val leftForm = AppliedConnector(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val rightForm = AppliedConnector(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val newleft = if (toLeft) isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.applyUnsafe(Seq(right))) else originSequent.left
+ val newright = if (toRight) isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.applyUnsafe(Seq(right))) else originSequent.right
+ val result1: Sequent = (AppliedConnector(And, newleft.toSeq), phi) |- rightOrigin
+ val result2: Sequent = result1.left |- AppliedConnector(Or, newright.toSeq)
var scproof: Seq[K.SCProofStep] = Seq(K.Restate((leftOrigin |- rightOrigin).underlying, -1))
if (toLeft)
scproof = scproof :+ K.LeftSubstEq(result1.underlying, scproof.length - 1, List(left.underlying -> right.underlying), K.LambdaTermFormula(Seq(v.underlyingLabel), leftForm.underlying))
@@ -510,7 +511,7 @@ object Substitution {
Seq(premise)
)
- case ConnectorFormula(label, args) if label == Iff =>
+ case AppliedConnector(label, args) if label == Iff =>
val left = args(0)
val right = args(1)
val fv_in_phi = (originSequent.left ++ originSequent.right).flatMap(_.allSchematicLabels).map(_.id)
@@ -526,12 +527,12 @@ object Substitution {
case v: proof.ValidProofTactic => return v
}
- val leftForm = ConnectorFormula(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val rightForm = ConnectorFormula(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
- val newleft = if (toLeft) isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.left
- val newright = if (toRight) isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) else originSequent.right
- val result1: Sequent = (ConnectorFormula(And, newleft.toSeq), phi) |- rightOrigin
- val result2: Sequent = result1.left |- ConnectorFormula(Or, newright.toSeq)
+ val leftForm = AppliedConnector(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val rightForm = AppliedConnector(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val newleft = if (toLeft) isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.applyUnsafe(Seq(right))) else originSequent.left
+ val newright = if (toRight) isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.applyUnsafe(Seq(right))) else originSequent.right
+ val result1: Sequent = (AppliedConnector(And, newleft.toSeq), phi) |- rightOrigin
+ val result2: Sequent = result1.left |- AppliedConnector(Or, newright.toSeq)
var scproof: Seq[K.SCProofStep] = Seq(K.Restate((leftOrigin |- rightOrigin).underlying, -1))
if (toLeft)
diff --git a/lisa-sets/src/main/scala/lisa/automation/Tableau.scala b/lisa-sets/src/main/scala/lisa/automation/Tableau.scala
index ebc26493faabf1de2e954da860af42940d7bed7c..f084af4e3513dca9195d4bfe1b831c543c719be2 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Tableau.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Tableau.scala
@@ -102,7 +102,7 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
beta: List[ConnectorFormula], // label = Or
delta: List[BinderFormula], // Exists(...))
gamma: List[BinderFormula], // Forall(...)
- atoms: (List[PredicateFormula], List[PredicateFormula]), // split into positive and negatives!
+ atoms: (List[AtomicFormula], List[AtomicFormula]), // split into positive and negatives!
unifiable: Map[VariableLabel, BinderFormula], // map between metavariables and the original formula they came from
skolemized: Set[VariableLabel], // set of variables that have been skolemized
triedInstantiation: Map[VariableLabel, Set[Term]], // map between metavariables and the term they were already instantiated with
@@ -119,9 +119,9 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
if (gamma.nonEmpty && gamma.head.uniqueNumber == f.uniqueNumber) copy(gamma = gamma.tail) else throw Exception("First formula of gamma is not f")
case ConnectorFormula(And, args) =>
if (alpha.nonEmpty && alpha.head.uniqueNumber == f.uniqueNumber) copy(alpha = alpha.tail) else throw Exception("First formula of alpha is not f")
- case f @ PredicateFormula(id, args) =>
+ case f @ AtomicFormula(id, args) =>
throw Exception("Should not pop Atoms")
- case f @ ConnectorFormula(Neg, List(PredicateFormula(id, args))) =>
+ case f @ ConnectorFormula(Neg, List(AtomicFormula(id, args))) =>
throw Exception("Should not pop Atoms")
case _ => ???
@@ -130,9 +130,9 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
case f @ ConnectorFormula(Or, args) => this.copy(beta = f :: beta)
case f @ BinderFormula(Exists, x, inner) => this.copy(delta = f :: delta)
case f @ BinderFormula(Forall, x, inner) => this.copy(gamma = f :: gamma)
- case f @ PredicateFormula(id, args) =>
+ case f @ AtomicFormula(id, args) =>
this.copy(atoms = (f :: atoms._1, atoms._2))
- case ConnectorFormula(Neg, List(f @ PredicateFormula(id, args))) =>
+ case ConnectorFormula(Neg, List(f @ AtomicFormula(id, args))) =>
this.copy(atoms = (atoms._1, f :: atoms._2))
case _ => ???
@@ -164,7 +164,7 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
(l :+ nf, nn, ns)
)
(ConnectorFormula(label, nArgs), nnId, nSeen)
- case pf: PredicateFormula => (pf, nextId, seen)
+ case pf: AtomicFormula => (pf, nextId, seen)
case BinderFormula(label, x, inner) =>
if (seen.contains(x))
val (nInner, nnId, nSeen) = makeVariableNamesUnique(inner, nextId + 1, seen)
@@ -211,9 +211,9 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
/**
* Detect if two atoms can be unified, and if so, return a substitution that unifies them.
*/
- def unifyPred(pos: PredicateFormula, neg: PredicateFormula, br: Branch): Option[Substitution] = {
+ def unifyPred(pos: AtomicFormula, neg: AtomicFormula, br: Branch): Option[Substitution] = {
(pos, neg) match
- case (PredicateFormula(id1, args1), PredicateFormula(id2, args2)) if (id1 == id2 && args1.size == args2.size) =>
+ case (AtomicFormula(id1, args1), AtomicFormula(id2, args2)) if (id1 == id2 && args1.size == args2.size) =>
args1
.zip(args2)
.foldLeft(Some(Substitution.empty): Option[Substitution])((prev, next) =>
@@ -239,7 +239,7 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
val newMapTerm = newMap.map((k, v) => k -> VariableTerm(v))
val inverseNewMap = newMap.map((k, v) => v -> k).toMap
val inverseNewMapTerm = inverseNewMap.map((k, v) => k -> VariableTerm(v))
- val pos = branch.atoms._1.map(pred => substituteVariablesInFormula(pred, newMapTerm, Seq())).asInstanceOf[List[PredicateFormula]].iterator
+ val pos = branch.atoms._1.map(pred => substituteVariablesInFormula(pred, newMapTerm, Seq())).asInstanceOf[List[AtomicFormula]].iterator
var substitutions: List[(Substitution, Set[Formula])] = Nil
while (pos.hasNext) {
@@ -255,7 +255,6 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
}
}
-
val cr1 = substitutions.map((sub, set) =>
(
sub.flatMap((v, t) =>
@@ -437,6 +436,6 @@ object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequent
def instantiate(f: Formula, x: VariableLabel, t: Term): Formula = f match
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiate(_, x, t)))
- case PredicateFormula(id, args) => PredicateFormula(id, args.map(substituteVariablesInTerm(_, Substitution(x -> t))))
+ case AtomicFormula(id, args) => AtomicFormula(id, args.map(substituteVariablesInTerm(_, Substitution(x -> t))))
case BinderFormula(label, y, inner) => if (x == y) f else BinderFormula(label, y, instantiate(inner, x, t))
}
diff --git a/lisa-sets/src/main/scala/lisa/automation/Tautology.scala b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
index d9bd7a2bb19ec824b1c709159b3d91b27fa1be6f..f217058c289448d9fa29d215c0147d3fbc01e29f 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
@@ -109,8 +109,8 @@ object Tautology extends ProofTactic with ProofSequentTactic with ProofFactSeque
def findBestAtom(f: Formula): Option[Formula] = {
val atoms: scala.collection.mutable.Map[Formula, Int] = scala.collection.mutable.Map.empty
def findAtoms2(f: Formula, add: Formula => Unit): Unit = f match {
- case PredicateFormula(label, _) if label != top && label != bot => add(f)
- case PredicateFormula(_, _) => ()
+ case AtomicFormula(label, _) if label != top && label != bot => add(f)
+ case AtomicFormula(_, _) => ()
case ConnectorFormula(label, args) =>
label match {
case label: ConstantConnectorLabel => args.foreach(c => findAtoms2(c, add))
@@ -172,10 +172,10 @@ object Tautology extends ProofTactic with ProofSequentTactic with ProofFactSeque
private def findSubterm2(f: Formula, subs: Seq[(VariableLabel, Term)]): (Formula, Boolean) = {
f match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
val induct = condflat(args.map(findSubterm2(_, subs)))
if (!induct._2) (f, false)
- else (PredicateFormula(label, induct._1), true)
+ else (AtomicFormula(label, induct._1), true)
case ConnectorFormula(label, args) =>
val induct = condflat(args.map(findSubterm2(_, subs)))
if (!induct._2) (f, false)
@@ -201,7 +201,7 @@ object Tautology extends ProofTactic with ProofSequentTactic with ProofFactSeque
if (eq.nonEmpty) (eq.get._1(), true)
else
f match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
(f, false)
case ConnectorFormula(label, args) =>
val induct = condflat(args.map(findSubformula2(_, subs)))
diff --git a/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala b/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
index e36014f0df4a2e9baa582c4a0796250dfa99b95d..09dcb5e259c00646d7a8da5b6488ffe351088d09 100644
--- a/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
@@ -56,7 +56,7 @@ object SetTheoryTactics {
val t1 = Variable(freshId(takenIDs, x.id))
val t2 = Variable(freshId(takenIDs, y.id))
- val prop = (in(t2, originalSet) /\ separationPredicate(Seq(t2, originalSet)))
+ val prop = (in(t2, originalSet) /\ separationPredicate(t2, originalSet)) // TODO (Seq(t2, originalSet)
def fprop(z: Term) = forall(t2, in(t2, z) <=> prop)
/**
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
index 17a98e489822747f2d92ce8cc7537d6196ad9394..996d55eea3ee24a4ed3480f6a4271283a2f2ccef 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
@@ -61,7 +61,7 @@ object InductiveSets extends lisa.Main {
* Natural Numbers (Inductive definition) --- The intersection of all
* inductive sets is the set of natural numbers, N.
*/
- val naturalsInductive = DEF(EmptyTuple) --> The(z, ∀(t, in(t, z) <=> (∀(y, inductive(y) ==> in(t, y)))))(inductiveIntersectionUniqueness)
+ val naturalsInductive = DEF() --> The(z, ∀(t, in(t, z) <=> (∀(y, inductive(y) ==> in(t, y)))))(inductiveIntersectionUniqueness)
/**
* Theorem --- Natural numbers form an inductive set
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
index 5308dac92fef35f0492b6221b028c6cae37ddbd5..6182209bd8378c5dddb3f79c72b4b7d856b96553 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
@@ -548,7 +548,7 @@ object Recursion extends lisa.Main {
)
) by Tautology.from(
lastStep,
- universalEquivalenceDistribution of (P -> lambda(b, in(b, B) ==> (in(pair(n, b), p2) \/ (n === b))), Q -> lambda(
+ universalEquivalenceDistribution of (P := lambda(b, in(b, B) ==> (in(pair(n, b), p2) \/ (n === b))), Q := lambda(
b,
(in(b, initialSegment(p, a1)) /\ !(app(k1, b) === app(k2, b))) ==> (in(pair(n, b), p2) \/ (n === b))
))
diff --git a/lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala b/lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala
index 4e889f4ed826d23412f02491318d207d4f6957db..e422b6f159670ee2de0513a748826719e46dc267 100644
--- a/lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala
+++ b/lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala
@@ -23,7 +23,7 @@ object PeanoArithmetics extends lisa.prooflib.Library {
final val ax6timesDistrib: Formula = forall(x, forall(y, times(x, s(y)) === plus(times(x, y), x)))
final val ax7induction: Formula = (sPhi(zero) /\ forall(x, sPhi(x) ==> sPhi(s(x)))) ==> forall(x, sPhi(x))
- final val functions: Set[ConstantTermLabel] = Set(ConstantFunctionLabel("0", 0), s, plus, times)
+ final val functions: Set[ConstantTermLabel[?]] = Set(ConstantFunctionLabel("0", 0), s, plus, times)
functions.foreach(l => theory.addSymbol(l.underlyingLabel))
private val peanoAxioms: Set[(String, Formula)] = Set(
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index 0e12da49bfc73f2d8dea3c45f0e743023d501fc2..cc69891602f8d7811cd170a0c4e9855b1e7cf22f 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -5,9 +5,8 @@ import lisa.utils.UserLisaException
import scala.annotation.nowarn
import scala.annotation.showAsInfix
+import scala.annotation.targetName
import scala.compiletime.ops.int.-
-import scala.reflect.ClassTag
-import scala.runtime.ScalaRunTime
import K.given_Conversion_Identifier_String
@@ -21,34 +20,17 @@ trait Common {
type Arity = Int & Singleton
/**
- * Define the type of tuples of Arity N. If N=-1, T***N = List[T] (arbitrary arity).
+ * Type of sequences of length N
*/
- @showAsInfix
- type ***[+T, N <: Arity] <: (Tuple | Seq[T]) & Matchable = N match {
- case -1 => Seq[T]
- case 0 => EmptyTuple
- case _ => T *: (T *** (N - 1))
+ opaque type **[+T, N <: Arity] >: Seq[T] = Seq[T]
+ object ** {
+ def apply[T, N <: Arity](args: T*): T ** N = args.toSeq
+ def unapplySeq[T, N <: Arity](arg: T ** N): Option[Seq[T]] = Some(arg)
}
- /**
- * The union of the types of N-tuples and lists. Usually, filling a List for a T**N forfeits arity checking at compile time.
- */
- type **[+T, N <: Arity] = Seq[T] | ***[T, N]
-
extension [T, N <: Arity](self: T ** N) {
- @nowarn("msg=checked at runtime")
- @nowarn("msg=match may not be exhaustive")
- def toSeq: Seq[T] = self match {
- case l: Seq[T] => l
- case tup: Tuple =>
- tup.productIterator.toSeq.asInstanceOf[Seq[T]]
- }
- @nowarn("msg=checked at runtime")
- @nowarn("msg=match may not be exhaustive")
- def map[U](f: T => U): U ** N = self match {
- case l: Seq[T] => l.map(f).asInstanceOf[(U ** (N))]
- case tup: Tuple => tup.map[[t] =>> U]([u] => (x: u) => f(x.asInstanceOf[T])).asInstanceOf
- }
+ def toSeq: Seq[T] = self
+ def map[U](f: T => U): U ** N = self.map(f)
}
@@ -95,8 +77,8 @@ trait Common {
def lift: T & this.type = this
/**
- * Substitution in the LisaObject of schematics 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 that should be implemented.
+ * 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 substituteUnsafe2[A <: SchematicLabel[?], B <: LisaObject[B]](map: Map[A, B]): T = substituteUnsafe(map.asInstanceOf)
@@ -133,7 +115,7 @@ trait Common {
*/
@showAsInfix
infix trait |->[-I, +O <: LisaObject[O]] extends LisaObject[I |-> O] {
- def apply(arg: I): O
+ def applyUnsafe(arg: I): O
}
@@ -179,7 +161,7 @@ trait Common {
/**
* ConstantLabel represent constants in the theory and can't be freely substituted.
*/
- sealed trait ConstantLabel[-A <: LisaObject[A]] extends Label[A] with Matchable {
+ sealed trait ConstantLabel[-A <: LisaObject[A]] extends Label[A] {
this: A & LisaObject[A] =>
def rename(newid: Identifier): ConstantLabel[A]
def freshRename(taken: Iterable[Identifier]): ConstantLabel[A]
@@ -205,10 +187,9 @@ trait Common {
* The type of terms, corresponding to [[K.Term]]. It can be either of a [[Variable]], a [[Constant]]
* a [[ConstantFunctionLabel]] or a [[SchematicFunctionLabel]].
*/
- sealed trait Term extends TermOrFormula with LisaObject[Term] with (Term ** 0 |-> Term) {
- def apply(args: Term ** 0): Term = this
+ sealed trait Term extends TermOrFormula with LisaObject[Term] {
val underlying: K.Term
- val label: TermLabel
+ val label: TermLabel[?]
val args: Seq[Term]
def toStringSeparated(): String = toString()
}
@@ -217,13 +198,17 @@ trait Common {
* A TermLabel is a [[LisaObject]] of type ((Term ** N) |-> Term), that is represented by a functional label.
* It can be either a [[SchematicFunctionLabel]] or a [[ConstantFunctionLabel]]. It corresponds to [[K.TermLabel]]
*/
- sealed trait TermLabel extends (Seq[Term] |-> Term) with Absolute {
+ sealed trait TermLabel[A <: (Term | (Seq[Term] |-> Term)) & LisaObject[A]] extends Label[A] with Absolute {
+ this: A & LisaObject[A] =>
val arity: Arity
def id: Identifier
val underlyingLabel: K.TermLabel
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): (Seq[Term] |-> Term)
- def rename(newid: Identifier): TermLabel
- def freshRename(taken: Iterable[Identifier]): TermLabel
+ def applySeq(args: Seq[Term]): Term = this match
+ case l: Variable => l.applyUnsafe(args)
+ case l: Constant => l.applyUnsafe(args)
+ case l: FunctionLabel[?] => l.applyUnsafe(args)
+ def rename(newid: Identifier): TermLabel[A]
+ def freshRename(taken: Iterable[Identifier]): TermLabel[A]
def mkString(args: Seq[Term]): String
def mkStringSeparated(args: Seq[Term]): String = mkString(args)
}
@@ -231,11 +216,12 @@ trait Common {
/**
* A constant [[TermLabel]], which can be either a [[Constant]] symbol or a [[ConstantFunctionSymbol]]. Corresponds to a [[K.ConstantFunctionLabel]]
*/
- sealed trait ConstantTermLabel extends TermLabel with ConstantLabel[Seq[Term] |-> Term] {
+ 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
- override def rename(newid: Identifier): ConstantTermLabel
- def freshRename(taken: Iterable[Identifier]): ConstantTermLabel
+ def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantTermLabel[A]
+ override def rename(newid: Identifier): ConstantTermLabel[A]
+ def freshRename(taken: Iterable[Identifier]): ConstantTermLabel[A]
}
object ConstantTermLabel {
@@ -246,7 +232,7 @@ trait Common {
* @param arity The arity of the new symbol
* @return The new symbol
*/
- def apply[N <: Arity](id: Identifier, arity: N): ConstantFunctionLabelOfArity[N] = arity match {
+ def apply[N <: Arity](id: Identifier, arity: N): ConstantTermLabelOfArity[N] = arity match {
case a: 0 => Constant(id)
case n: N => ConstantFunctionLabel[N](id, arity)
}
@@ -255,29 +241,18 @@ trait Common {
/**
* Types of constant term labels: [[Constant]] for if N = 0, [[ConstantFunctionLabel]] otherwise.
*/
- type ConstantFunctionLabelOfArity[N <: Arity] <: ConstantTermLabel = N match
+ type ConstantTermLabelOfArity[N <: Arity] <: ConstantTermLabel[?] = N match
case 0 => Constant
case N => ConstantFunctionLabel[N]
- object ConstantFunctionLabelOfArity {
-
- /**
- * Construct a ConstantTermLabel according to arity:
- * A [[Constant]] for arity 0, a [[ConstantFunctionLabel]] otherwise.
- * @param id The identifier of the new symbol
- * @param arity The arity of the new symbol
- * @return The new symbol
- */
- def apply[N <: Arity](id: Identifier, arity: N): ConstantFunctionLabelOfArity[N] = ConstantTermLabel[N](id, arity)
- }
/**
* A schematic [[TermLabel]], which can be either a [[Variable]] symbol or a [[SchematicFunctionSymbol]]. Corresponds to a [[K.SchematicFunctionLabel]]
*/
- sealed trait SchematicTermLabel extends TermLabel with SchematicLabel[Seq[Term] |-> Term] {
+ sealed trait SchematicTermLabel[A <: (Term | (Seq[Term] |-> Term)) & LisaObject[A]] extends TermLabel[A] with SchematicLabel[A] {
+ this: A & LisaObject[A] =>
val underlyingLabel: K.SchematicTermLabel
- override def rename(newid: Identifier): SchematicTermLabel
- def freshRename(taken: Iterable[Identifier]): SchematicTermLabel
- def mkString(args: Seq[Term]): String
+ override def rename(newid: Identifier): SchematicTermLabel[A]
+ def freshRename(taken: Iterable[Identifier]): SchematicTermLabel[A]
}
object SchematicTermLabel { // Companion
/**
@@ -292,34 +267,34 @@ trait Common {
case n: N => new SchematicFunctionLabel[N](id, arity)
}
}
- type SchematicFunctionLabelOfArity[N <: Arity] <: SchematicTermLabel = N match
+ type SchematicFunctionLabelOfArity[N <: Arity] <: SchematicTermLabel[?] = N match
case 0 => Variable
case N => SchematicFunctionLabel[N]
- object SchematicFunctionLabelOfArity { // Companion
- /**
- * Construct a SchematicTermLabel according to arity:
- * A [[Variable]] for arity 0, a [[SchematicFunctionLabel]] otherwise.
- * @param id The identifier of the new symbol
- * @param arity The arity of the new symbol
- * @return The new symbol
- */
- def apply[N <: Arity](id: Identifier, arity: N): SchematicFunctionLabelOfArity[N] = SchematicTermLabel[N](id, arity)
+
+ /**
+ * Can be either a [[ConstantFunctionSymbol]] symbol or a [[SchematicFunctionSymbol]]. Corresponds to a [[K.TermLabel]]
+ */
+ 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 applyUnsafe(args: (Term ** N)): Term = AppliedFunction(this, args.toSeq)
+ override def rename(newid: Identifier): FunctionLabel[N]
+ def freshRename(taken: Iterable[Identifier]): FunctionLabel[N]
}
/**
* A Variable, corresponding to [[K.VariableLabel]], is a schematic symbol for terms.
* It counts both as the label and as the term itself.
*/
- case class Variable(id: Identifier) extends SchematicTermLabel with Term with Absolute with SchematicLabel[Term] {
+ case class Variable(id: Identifier) extends SchematicTermLabel[Term] with Term with Absolute {
val arity: 0 = 0
val label: Variable = this
val args: Seq[Nothing] = Seq.empty
- override val underlyingLabel: K.VariableLabel = K.VariableLabel(id)
- override val underlying = K.VariableTerm(underlyingLabel)
- override def apply(args: Term ** 0) = this
- @nowarn("msg=Unreachable")
- override def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term = {
- map.get(this.asInstanceOf) match {
+ 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 = {
+ map.get(this) match {
case Some(subst) =>
subst match {
case s: Term => s
@@ -330,7 +305,7 @@ trait Common {
}
def freeSchematicLabels: Set[SchematicLabel[?]] = Set(this)
def allSchematicLabels: Set[SchematicLabel[?]] = Set(this)
- override def rename(newid: Identifier): Variable = Variable(newid)
+ def rename(newid: Identifier): Variable = Variable(newid)
def freshRename(taken: Iterable[Identifier]): Variable = rename(K.freshId(taken, id))
override def toString(): String = id
def mkString(args: Seq[Term]): String = if (args.size == 0) toString() else toString() + "(" + "illegal_arguments: " + args.mkString(", ") + ")"
@@ -340,18 +315,18 @@ trait Common {
* A Constant, corresponding to [[K.ConstantLabel]], is a label for terms.
* It counts both as the label and as the term itself.
*/
- case class Constant(id: Identifier) extends ConstantTermLabel with Term with Absolute with ConstantLabel[Constant] with LisaObject[Constant] {
+ case class Constant(id: Identifier) extends Term with Absolute with ConstantTermLabel[Constant] with LisaObject[Constant] {
val arity: 0 = 0
val label: Constant = this
val args: Seq[Nothing] = Seq.empty
- override val underlyingLabel: K.ConstantFunctionLabel = K.ConstantFunctionLabel(id, 0)
- override val underlying = K.Term(underlyingLabel, Seq())
- override def apply(args: Term ** 0) = this
+ 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
- override def rename(newid: Identifier): Constant = Constant(newid)
- def freshRename(taken: Iterable[Identifier]): Constant = rename(K.freshId(taken, id))
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
+ def rename(newid: Identifier): Constant = Constant(newid)
+ def freshRename(taken: Iterable[Identifier]): Constant = rename(K.freshId(taken, id))
override def toString(): String = id
def mkString(args: Seq[Term]): String = if (args.size == 0) toString() else toString() + "(" + "illegal_arguments: " + args.mkString(", ") + ")"
}
@@ -360,16 +335,16 @@ trait Common {
* A schematic functional label (corresponding to [[K.SchematicFunctionLabel]]) is a functional label and also a schematic label.
* It can be substituted by any expression of type (Term ** N) |-> Term
*/
- case class SchematicFunctionLabel[N <: Arity](val id: Identifier, val arity: N) extends SchematicTermLabel with SchematicLabel[(Term ** N) |-> Term] with ((Term ** N) |-> Term) {
+ case class SchematicFunctionLabel[N <: Arity](val id: Identifier, val arity: N) extends SchematicTermLabel[(Term ** N) |-> Term] with FunctionLabel[N] {
val underlyingLabel: K.SchematicTermLabel = K.SchematicFunctionLabel(id, arity)
- def apply(args: (Term ** N)): Term = AppliedTerm(this, args.toSeq)
- def unapplySeq(t: AppliedTerm): Seq[Term] = t match {
- case AppliedTerm(label, args) if (label == this) => args
+
+ def unapplySeq(t: AppliedFunction): Seq[Term] = t match {
+ case AppliedFunction(label, args) if (label == this) => args
case _ => Seq.empty
}
- @nowarn
+ @nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ((Term ** N) |-> Term) = {
- map.get(this.asInstanceOf) match {
+ map.get(this) match {
case Some(subst) =>
subst match {
case s: ((Term ** N) |-> Term) => s
@@ -390,20 +365,18 @@ trait Common {
/**
* A constant functional label of arity N.
*/
- case class ConstantFunctionLabel[N <: Arity](id: Identifier, arity: N) extends ConstantTermLabel with ConstantLabel[((Term ** N) |-> Term)] with ((Term ** N) |-> Term) {
+ case class ConstantFunctionLabel[N <: Arity](id: Identifier, arity: N) extends ConstantTermLabel[((Term ** N) |-> Term)] with FunctionLabel[N] {
val underlyingLabel: K.ConstantFunctionLabel = K.ConstantFunctionLabel(id, arity)
- var infix: Boolean = false
- def apply(args: (Term ** N)): Term = AppliedTerm(this, args.toSeq)
- def unapplySeq(t: AppliedTerm): Seq[Term] = t match {
- case AppliedTerm(label, args) if (label == this) => args
+ private var infix: Boolean = false
+ def unapplySeq(t: AppliedFunction): Seq[Term] = t match {
+ case AppliedFunction(label, args) if (label == this) => args
case _ => Seq.empty
}
- inline def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type =
- this
- def rename(newid: Identifier): ConstantFunctionLabel[N] = ConstantFunctionLabel(newid, arity)
- def freshRename(taken: Iterable[Identifier]): ConstantFunctionLabel[N] = rename(K.freshId(taken, id))
+ 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)
+ def freshRename(taken: Iterable[Identifier]): ConstantFunctionLabel[N] = rename(K.freshId(taken, id))
override def toString(): String = id
def mkString(args: Seq[Term]): String = if (infix) (args(0).toString() + " " + toString() + " " + args(1).toString()) else toString() + "(" + args.mkString(", ") + ")"
override def mkStringSeparated(args: Seq[Term]): String = if (infix) "(" + mkString(args) + ")" else mkString(args)
@@ -418,19 +391,15 @@ trait Common {
/**
* A term made from a functional label of arity N and N arguments
*/
- case class AppliedTerm(f: TermLabel, args: Seq[Term]) extends Term with Absolute {
- val label: TermLabel = f
- assert(f.arity != 0)
- override val underlying = K.Term(f.underlyingLabel, args.map(_.underlying))
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term = {
- f.substituteUnsafe(map)(
- args.map[Term]((x: Term) => x.substituteUnsafe(map))
- )
- }
- def freeSchematicLabels: Set[SchematicLabel[?]] = f.freeSchematicLabels ++ args.flatMap(_.freeSchematicLabels)
- def allSchematicLabels: Set[SchematicLabel[?]] = f.allSchematicLabels ++ args.flatMap(_.allSchematicLabels)
- override def toString: String = f.mkString(args)
- override def toStringSeparated(): String = f.mkString(args)
+ case class AppliedFunction(label: FunctionLabel[?], args: Seq[Term]) extends Term with Absolute {
+ override val underlying = K.Term(label.underlyingLabel, args.map(_.underlying))
+ 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)
+ def allSchematicLabels: Set[SchematicLabel[?]] = label.allSchematicLabels ++ args.flatMap(_.allSchematicLabels)
+ override def toString: String = label.mkString(args)
+ override def toStringSeparated(): String = label.mkString(args)
}
//////////////////////////////////////
@@ -440,11 +409,7 @@ trait Common {
/**
* The type of formulas, corresponding to [[K.Formula]]
*/
- sealed trait Formula extends TermOrFormula with LisaObject[Formula] with ((Term ** 0) |-> Formula) {
- val arity: Arity = 0
- // val label:PredicateLabel|ConnectorLabel
- // val args:Seq[Term]|Seq[Formula]
- def apply(args: Term ** 0): Formula = this
+ sealed trait Formula extends TermOrFormula with LisaObject[Formula] {
val underlying: K.Formula
def toStringSeparated() = toString()
}
@@ -454,61 +419,119 @@ trait Common {
/////////////////////
sealed trait AtomicFormula extends Formula {
- val label: PredicateLabel
+ val label: AtomicLabel[?]
val args: Seq[Term]
}
/**
- * A PredicateLabel is a [[LisaObject]] of type ((Term ** N) |-> Formula), that is represented by a predicate label.
+ * A AtomicLabel is a [[LisaObject]] of type ((Term ** N) |-> Formula), that is represented by a predicate label.
* It can be either a [[SchematicPredicateLabel]] or a [[ConstantPredicateLabel]].
*/
- sealed trait PredicateLabel extends (Seq[Term] |-> Formula) with Absolute {
+ sealed trait AtomicLabel[A <: (Formula | (Seq[Term] |-> Formula)) & LisaObject[A]] extends Label[A] with Absolute {
+ this: A & LisaObject[A] =>
val arity: Arity
def id: Identifier
- val underlyingLabel: K.PredicateLabel
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): (Seq[Term] |-> Formula)
- def rename(newid: Identifier): PredicateLabel
- def freshRename(taken: Iterable[Identifier]): PredicateLabel
+ val underlyingLabel: K.AtomicLabel
+ def applySeq(args: Seq[Term]): Formula = this match
+ case l: VariableFormula => l.applyUnsafe(args)
+ case l: ConstantFormula => l.applyUnsafe(args)
+ case l: PredicateLabel[?] => l.applyUnsafe(args)
+
+ def rename(newid: Identifier): AtomicLabel[A]
+ def freshRename(taken: Iterable[Identifier]): AtomicLabel[A]
def mkString(args: Seq[Term]): String
def mkStringSeparated(args: Seq[Term]): String = mkString(args)
}
- sealed trait ConstantConstOrPredLabel extends PredicateLabel with ConstantLabel[Seq[Term] |-> Formula] {
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantConstOrPredLabel
- override def rename(newid: Identifier): ConstantConstOrPredLabel
- def freshRename(taken: Iterable[Identifier]): ConstantConstOrPredLabel
+ /**
+ * A constant [[AtomicLabel]], which can be either a [[ConstantFormula]] symbol or a [[ConstantPredicateSymbol]]. Corresponds to a [[K.ConstantAtomicLabel]]
+ */
+ 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]
+ override def rename(newid: Identifier): ConstantAtomicLabel[A]
+ def freshRename(taken: Iterable[Identifier]): ConstantAtomicLabel[A]
+ }
+ object ConstantAtomicLabel {
+
+ /**
+ * Construct a ConstantTermLabel according to arity:
+ * A [[Constant]] for arity 0, a [[ConstantFunctionLabel]] otherwise.
+ * @param id The identifier of the new symbol
+ * @param arity The arity of the new symbol
+ * @return The new symbol
+ */
+ def apply[N <: Arity](id: Identifier, arity: N): ConstantAtomicLabelOfArity[N] = arity match {
+ case a: 0 => ConstantFormula(id)
+ case n: N => ConstantPredicateLabel[N](id, arity)
+ }
}
- type ConstantPredicateLabelOfArity[N <: Arity] <: ConstantConstOrPredLabel = N match {
+
+ /**
+ * Types of constant atomic labels: [[ConstantFormula]] for if N = 0, [[ConstantPredicateLabel]] otherwise.
+ */
+ type ConstantAtomicLabelOfArity[N <: Arity] <: ConstantAtomicLabel[?] = N match {
case 0 => ConstantFormula
case N => ConstantPredicateLabel[N]
}
- sealed trait SchematicVarOrPredLabel extends PredicateLabel with SchematicLabel[Seq[Term] |-> Formula] {
- override def rename(newid: Identifier): SchematicVarOrPredLabel
- def freshRename(taken: Iterable[Identifier]): SchematicVarOrPredLabel
+ /**
+ * A schematic [[AtomicLabel]], which can be either a [[VariableFormula]] symbol or a [[SchematicPredicateLabel]]. Corresponds to a [[K.SchematicAtomicLabel]]
+ */
+ sealed trait SchematicAtomicLabel[A <: (Formula | (Seq[Term] |-> Formula)) & LisaObject[A]] extends AtomicLabel[A] with SchematicLabel[A] {
+ this: A & LisaObject[A] =>
+ override def rename(newid: Identifier): SchematicAtomicLabel[A]
+ def freshRename(taken: Iterable[Identifier]): SchematicAtomicLabel[A]
+
}
- type SchematicPredicateLabelOfArity[N <: Arity] <: SchematicVarOrPredLabel = N match {
+ object SchematicAtomicLabel { // Companion
+ /**
+ * Construct a SchematicTermLabel according to arity:
+ * A [[Variable]] for arity 0, a [[SchematicFunctionLabel]] otherwise.
+ * @param id The identifier of the new symbol
+ * @param arity The arity of the new symbol
+ * @return The new symbol
+ */
+ def apply[N <: Arity](id: Identifier, arity: N): SchematicAtomicLabelOfArity[N] = arity match {
+ case a: 0 => new VariableFormula(id)
+ case n: N => new SchematicPredicateLabel[N](id, arity)
+ }
+ }
+
+ type SchematicAtomicLabelOfArity[N <: Arity] <: SchematicAtomicLabel[?] = N match {
case 0 => VariableFormula
case N => SchematicPredicateLabel[N]
}
+ /**
+ * Can be either a [[ConstantFunctionSymbol]] symbol or a [[SchematicFunctionSymbol]]. Corresponds to a [[K.TermLabel]]
+ */
+ 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 applyUnsafe(args: (Term ** N)): Formula = AppliedPredicate(this, args.toSeq)
+ override def rename(newid: Identifier): PredicateLabel[N]
+ def freshRename(taken: Iterable[Identifier]): PredicateLabel[N]
+ }
+
/**
* A Variable for formulas, corresponding to [[K.VariableFormulaLabel]], is a schematic symbol for formulas.
* It counts both as the label and as the term itself.
*/
- case class VariableFormula(id: Identifier) extends SchematicVarOrPredLabel with AtomicFormula with Absolute with SchematicLabel[Formula] {
+ case class VariableFormula(id: Identifier) extends SchematicAtomicLabel[Formula] with AtomicFormula with Absolute {
override val arity: 0 = 0
val label: VariableFormula = this
- val args: Seq[Nothing] = Seq()
+ val args: Seq[Nothing] = Seq.empty
val underlyingLabel: K.VariableFormulaLabel = K.VariableFormulaLabel(id)
- val underlying = K.PredicateFormula(underlyingLabel, Seq())
- override def apply(args: Term ** 0): Formula = this
- @nowarn("msg=Unreachable")
+ val underlying = K.AtomicFormula(underlyingLabel, Seq.empty)
+ def applyUnsafe(args: Term ** 0): Formula = this
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula = {
- map.get(this.asInstanceOf) match {
+ map.get(this) match {
case Some(subst) =>
subst match {
case s: Formula => s
+ case _ => throw SubstitutionException()
}
case None => this
}
@@ -525,14 +548,14 @@ trait Common {
* A Constant formula, corresponding to [[K.ConstantFormulaLabel]].
* It counts both as the label and as the formula itself. Usually either True or False.
*/
- case class ConstantFormula(id: Identifier) extends ConstantConstOrPredLabel with AtomicFormula with Absolute with ConstantLabel[Formula] {
+ case class ConstantFormula(id: Identifier) extends ConstantAtomicLabel[Formula] with AtomicFormula with Absolute with ConstantLabel[Formula] {
override val arity: 0 = 0
val label: ConstantFormula = this
- val args: Seq[Nothing] = Seq()
- val underlyingLabel: K.ConstantPredicateLabel = K.ConstantPredicateLabel(id, 0)
- val underlying = K.PredicateFormula(underlyingLabel, Seq())
- override def apply(args: Term ** 0): Formula = this
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
+ val args: Seq[Nothing] = Seq.empty
+ 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 freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def rename(newid: Identifier): ConstantFormula = ConstantFormula(newid)
@@ -542,22 +565,22 @@ trait Common {
}
/**
- * A schematic predicate label (corresponding to [[K.SchematicPredicateLabel]]) is a [[PredicateLabel]] and also a [[SchematicLabel]].
+ * A schematic predicate label (corresponding to [[K.SchematicPredicateLabel]]) is a [[AtomicLabel]] and also a [[SchematicLabel]].
* It can be substituted by any expression of type (Term ** N) |-> Formula
*/
- case class SchematicPredicateLabel[N <: Arity](id: Identifier, arity: N) extends SchematicVarOrPredLabel with SchematicLabel[(Term ** N) |-> Formula] with ((Term ** N) |-> Formula) {
+ case class SchematicPredicateLabel[N <: Arity](id: Identifier, arity: N) extends SchematicAtomicLabel[(Term ** N) |-> Formula] with PredicateLabel[N] {
val underlyingLabel: K.SchematicPredicateLabel = K.SchematicPredicateLabel(id, arity)
- def apply(args: (Term ** N)): Formula = PredicateFormula(this, args.toSeq)
- def unapplySeq(t: AppliedTerm): Seq[Term] = t match {
- case AppliedTerm(label, args) if (label == this) => args
+ def unapplySeq(t: AppliedFunction): Seq[Term] = t match {
+ case AppliedFunction(label, args) if (label == this) => args
case _ => Seq.empty
}
- @nowarn
+ @nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Term ** N, Formula] = {
- map.get(this.asInstanceOf) match {
+ map.get(this) match {
case Some(subst) =>
subst match {
case s: |->[Term ** N, Formula] => s
+ case _ => throw SubstitutionException()
}
case None => this
}
@@ -569,21 +592,19 @@ trait Common {
override def toString(): String = id
def mkString(args: Seq[Term]): String = toString() + "(" + args.mkString(", ") + ")"
override def mkStringSeparated(args: Seq[Term]): String = mkString(args)
-
}
/**
- * A constant predicate label corresponding to [[K.ConstantPredicateLabel]].
+ * A constant predicate label corresponding to [[K.ConstantAtomicLabel]] of arity >= 1.
*/
- case class ConstantPredicateLabel[N <: Arity](id: Identifier, arity: N) extends ConstantConstOrPredLabel with ConstantLabel[Term ** N |-> Formula] with ((Term ** N) |-> Formula) {
- val underlyingLabel: K.ConstantPredicateLabel = K.ConstantPredicateLabel(id, arity)
+ case class ConstantPredicateLabel[N <: Arity](id: Identifier, arity: N) extends ConstantAtomicLabel[Term ** N |-> Formula] with PredicateLabel[N] {
+ val underlyingLabel: K.ConstantAtomicLabel = K.ConstantAtomicLabel(id, arity)
private var infix = false
- def apply(args: (Term ** N)): Formula = PredicateFormula(this, args.toSeq)
- def unapplySeq(f: PredicateFormula): Seq[Term] = f match {
- case PredicateFormula(label, args) if (label == this) => args
+ def unapplySeq(f: AppliedPredicate): Seq[Term] = f match {
+ case AppliedPredicate(label, args) if (label == this) => args
case _ => Seq.empty
}
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = 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)
@@ -602,18 +623,16 @@ trait Common {
/**
* A formula made from a predicate label of arity N and N arguments
*/
- case class PredicateFormula(p: PredicateLabel, args: Seq[Term]) extends AtomicFormula with Absolute {
- assert(p.arity != 0)
- val label: PredicateLabel = p
- override val underlying = K.PredicateFormula(p.underlyingLabel, args.map(_.underlying))
+ 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 =
- p.substituteUnsafe(map)(args.map[Term]((x: Term) => x.substituteUnsafe(map)))
+ label.substituteUnsafe(map).applyUnsafe(args.map[Term]((x: Term) => x.substituteUnsafe(map)))
- def freeSchematicLabels: Set[SchematicLabel[?]] = p.freeSchematicLabels ++ args.toSeq.flatMap(_.freeSchematicLabels)
- def allSchematicLabels: Set[SchematicLabel[?]] = p.allSchematicLabels ++ args.toSeq.flatMap(_.allSchematicLabels)
+ def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.toSeq.flatMap(_.freeSchematicLabels)
+ def allSchematicLabels: Set[SchematicLabel[?]] = label.allSchematicLabels ++ args.toSeq.flatMap(_.allSchematicLabels)
- override def toString: String = p.mkString(args)
- override def toStringSeparated(): String = p.mkString(args)
+ override def toString: String = label.mkString(args)
+ override def toStringSeparated(): String = label.mkString(args)
}
////////////////
@@ -624,15 +643,16 @@ trait Common {
* A ConnectorLabel is a [[LisaObject]] of type ((Formula ** N) |-> Formula), that is represented by a connector label in the kernel.
* It can be either a [[SchematicConnectorLabel]] or a [[ConstantConnectorLabel]].
*/
- sealed trait ConnectorLabel extends (Seq[Formula] |-> Formula) with Absolute {
+ sealed trait ConnectorLabel extends (Seq[Formula] |-> Formula) with Label[(Seq[Formula] |-> Formula)] with Absolute {
val arity: Arity
def id: Identifier
val underlyingLabel: K.ConnectorLabel
+ 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 mkString(args: Seq[Formula]): String
- def mkStringSeparated(args: Seq[Formula]): String = mkString(args)
+ def mkStringSeparated(args: Seq[Formula]): String
}
@@ -642,28 +662,31 @@ trait Common {
*/
case class SchematicConnectorLabel[N <: Arity](id: Identifier, arity: N) extends ConnectorLabel with SchematicLabel[Formula ** N |-> Formula] with ((Formula ** N) |-> Formula) {
val underlyingLabel: K.SchematicConnectorLabel = K.SchematicConnectorLabel(id, arity)
- @nowarn
+ def unapplySeq(f: AppliedPredicate): Seq[Term] = f match {
+ case AppliedPredicate(label, args) if (label == this) => args
+ 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] = {
- map.get(this.asInstanceOf) match {
+ map.get(this) match {
case Some(subst) =>
subst match {
case s: |->[Formula ** N, Formula] => s
+ case _ => throw SubstitutionException()
}
case None => this
}
}
// def apply(args: Seq[Formula]): Formula = apply(args)
- def apply(args: Formula ** N): Formula = ConnectorFormula(this, args.toSeq)
- def unapplySeq(f: PredicateFormula): Seq[Term] = f match {
- case PredicateFormula(label, args) if (label == this) => args
- case _ => Seq.empty
- }
+ def applyUnsafe(args: Formula ** N): Formula = AppliedConnector(this, args.toSeq)
+
def freeSchematicLabels: Set[SchematicLabel[?]] = Set(this)
def allSchematicLabels: Set[SchematicLabel[?]] = Set(this)
def rename(newid: Identifier): SchematicConnectorLabel[N] = SchematicConnectorLabel(newid, arity)
def freshRename(taken: Iterable[Identifier]): SchematicConnectorLabel[N] = rename(K.freshId(taken, id))
override def toString(): String = id
def mkString(args: Seq[Formula]): String = toString() + "(" + args.mkString(", ") + ")"
+ def mkStringSeparated(args: Seq[Formula]): String = mkString(args)
}
@@ -674,18 +697,18 @@ trait Common {
trait ConstantConnectorLabel[N <: Arity] extends ConnectorLabel with ConstantLabel[Formula ** N |-> Formula] with ((Formula ** N) |-> Formula) {
val underlyingLabel: K.ConstantConnectorLabel
def id: Identifier = underlyingLabel.id
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
- def apply(args: Formula ** N): Formula = ConnectorFormula(this, args.toSeq)
- def unapplySeq(f: ConnectorFormula): Seq[Formula] = f match {
- case ConnectorFormula(label, args) if (label == this) => args
+ def unapplySeq(f: AppliedConnector): Seq[Formula] = f match {
+ case AppliedConnector(label, args) if (label == this) => args
case _ => Seq.empty
}
+ 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
def rename(newid: Identifier): ConstantConnectorLabel[N] = throw new Error("Can't rename a constant connector label")
def freshRename(taken: Iterable[Identifier]): ConstantConnectorLabel[N] = rename(K.freshId(taken, id))
override def toString(): String = id
- def mkString(args: Seq[Formula]): String = if (args.length == 2) ("(" + args(0).toString() + " " + toString() + " " + args(1).toString()) + ")" else toString() + "(" + args.mkString(", ") + ")"
+ def mkString(args: Seq[Formula]): String = if (args.length == 2) (args(0).toString() + " " + toString() + " " + args(1).toString()) else toString() + "(" + args.mkString(", ") + ")"
override def mkStringSeparated(args: Seq[Formula]): String = if (args.length == 2) "(" + mkString(args) + ")" else mkString(args)
}
@@ -693,24 +716,16 @@ trait Common {
/**
* A formula made from a connector label of arity N and N arguments
*/
- case class ConnectorFormula(p: ConnectorLabel, args: Seq[Formula]) extends Formula with Absolute {
- // assert(args.length == p.arity)
- val label: ConnectorLabel = p
- override val underlying = K.ConnectorFormula(p.underlyingLabel, args.map(_.underlying))
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula = {
- val p2 = p.substituteUnsafe(map)
- p2 match {
- case p2: ConnectorLabel => ConnectorFormula(p2, args.map[Formula]((x: Formula) => x.substituteUnsafe(map)))
- case _ => p2(args.map[Formula]((x: Formula) => x.substituteUnsafe(map)))
- }
- }
-
- def freeSchematicLabels: Set[SchematicLabel[?]] = p.freeSchematicLabels ++ args.flatMap(_.freeSchematicLabels)
- def allSchematicLabels: Set[SchematicLabel[?]] = p.allSchematicLabels ++ args.flatMap(_.allSchematicLabels)
- // override def substituteUnsafe(v: Variable, subs: Term) = PredicateFormulaFormula[N](f, args.map(_.substituteUnsafe(v, subs)))
+ 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 =
+ 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)
+ // override def substituteUnsafe(v: Variable, subs: Term) = AppliedPredicateFormula[N](f, args.map(_.substituteUnsafe(v, subs)))
- override def toString: String = p.mkString(args)
- override def toStringSeparated(): String = p.mkString(args)
+ override def toString: String = label.mkString(args)
+ override def toStringSeparated(): String = label.mkString(args)
}
/////////////
@@ -727,10 +742,11 @@ trait Common {
/**
* A binder label that exactly correspond to a kernel binder, i.e. \exists, \forall and \exists!
*/
- trait BaseBinderLabel extends BinderLabel with Absolute {
+ trait BaseBinderLabel extends BinderLabel with ((Variable, Formula) |-> BinderFormula) with Absolute {
val underlyingLabel: K.BinderLabel
- def apply(arg: (Variable, Formula)): BinderFormula = BinderFormula(this, arg._1, arg._2)
+ def applyUnsafe(arg: (Variable, Formula)): BinderFormula = BinderFormula(this, arg._1, arg._2)
+ def apply(v: Variable, f: Formula): BinderFormula = applyUnsafe((v, f))
inline def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
inline def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
inline def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
@@ -741,13 +757,13 @@ trait Common {
/**
* A quantified formula made of a [[BaseBinderLabel]] and an underlying formula, in a namefull representation.
*/
- case class BinderFormula(f: BaseBinderLabel, bound: Variable, body: Formula) extends Formula with Absolute {
+ case class BinderFormula(f: BaseBinderLabel, bound: Variable, body: Formula) extends Absolute with Formula with LisaObject[BinderFormula] {
override val underlying = K.BinderFormula(f.underlyingLabel, bound.underlyingLabel, body.underlying)
def allSchematicLabels: Set[Common.this.SchematicLabel[?]] = body.allSchematicLabels + bound
def freeSchematicLabels: Set[Common.this.SchematicLabel[?]] = body.freeSchematicLabels - bound
- def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula = {
- val newSubst = map - bound.asInstanceOf
+ 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
val newBound: Variable = bound.rename(lisa.utils.KernelHelpers.freshId(taken.map(_.id), bound.id))
@@ -763,4 +779,29 @@ trait Common {
}
def instantiateBinder(f: BinderFormula, t: Term): Formula = f.body.substituteUnsafe(Map(f.bound -> t))
+ // Application methods for |->
+
+ extension [S, T <: LisaObject[T]](t: (S ** -1) |-> T) {
+ def apply(s: Seq[S]): T = t.applyUnsafe(s)
+ }
+ extension [S, T <: LisaObject[T], N <: Arity](t: (S ** N) |-> T) {
+ def applySeq(s: Seq[S]): T = t.applyUnsafe(s)
+ }
+
+ extension [S, T <: LisaObject[T]](t: (S ** 1) |-> T) {
+ def apply(s1: S): T = t.applyUnsafe(Seq(s1))
+ }
+ extension [S, T <: LisaObject[T]](t: (S ** 2) |-> T) {
+ def apply(s1: S, s2: S): T = t.applyUnsafe(Seq(s1, s2))
+ }
+ extension [S <: LisaObject[S], T <: LisaObject[T]](t: (S ** 3) |-> T) {
+ def apply(s1: S, s2: S, s3: S): T = t.applyUnsafe(Seq(s1, s2, s3))
+ }
+ extension [S <: LisaObject[S], T <: LisaObject[T]](t: (S ** 4) |-> T) {
+ def apply(s1: S, s2: S, s3: S, s4: S): T = t.applyUnsafe(Seq(s1, s2, s3, s4))
+ }
+ extension [S <: LisaObject[S], T <: LisaObject[T]](t: (S ** 5) |-> T) {
+ def apply(s1: S, s2: S, s3: S, s4: S, s5: S): T = t.applyUnsafe(Seq(s1, s2, s3, s4, s5))
+ }
+
}
diff --git a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
index e4039adf9f798e4b3c2e9b74b61baab86a1a9412..576a279c370fe7cb2572a8455cd4d533debb1ebb 100644
--- a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
@@ -6,9 +6,6 @@ import lisa.utils.FOLParser
import lisa.utils.K
import lisa.utils.LisaException
-import scala.annotation.targetName
-import scala.reflect.ClassTag
-
/**
* A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
* Usage:
@@ -36,7 +33,7 @@ object FOLHelpers {
LambdaExpression(s, a._2, s.length.asInstanceOf)
}
- given [T <: LisaObject[T]]: Conversion[T, T *** 1] = _ *: EmptyTuple
+ given [T <: LisaObject[T]]: Conversion[T, T ** 1] = **.apply[T, 1](_)
given Conversion[Int, Arity] = _.asInstanceOf
@@ -58,13 +55,13 @@ object FOLHelpers {
////////////////////////////////////////
// TermLabel
- def asFrontLabel(tl: K.TermLabel): TermLabel = tl match
+ def asFrontLabel(tl: K.TermLabel): TermLabel[?] = tl match
case tl: K.ConstantFunctionLabel => asFrontLabel(tl)
case tl: K.SchematicTermLabel => asFrontLabel(tl)
- def asFrontLabel[N <: Arity](cfl: K.ConstantFunctionLabel): ConstantFunctionLabelOfArity[N] = cfl.arity.asInstanceOf[N] match
+ def asFrontLabel[N <: Arity](cfl: K.ConstantFunctionLabel): ConstantTermLabelOfArity[N] = cfl.arity.asInstanceOf[N] match
case n: 0 => Constant(cfl.id)
case n: N => ConstantFunctionLabel[N](cfl.id, n)
- def asFrontLabel(stl: K.SchematicTermLabel): SchematicTermLabel = stl match
+ def asFrontLabel(stl: K.SchematicTermLabel): SchematicTermLabel[?] = stl match
case v: K.VariableLabel => asFrontLabel(v)
case v: K.SchematicFunctionLabel => asFrontLabel(v)
def asFrontLabel[N <: Arity](sfl: K.SchematicFunctionLabel): SchematicFunctionLabel[N] =
@@ -72,28 +69,28 @@ object FOLHelpers {
def asFrontLabel(v: K.VariableLabel): Variable = Variable(v.id)
// Term
- def asFront(t: K.Term): Term = asFrontLabel(t.label)(t.args.map(asFront))
+ def asFront(t: K.Term): Term = asFrontLabel(t.label).applySeq(t.args.map(asFront))
// FormulaLabel
- def asFrontLabel(fl: K.FormulaLabel): PredicateLabel | ConnectorLabel | BinderLabel = fl match
+ def asFrontLabel(fl: K.FormulaLabel): AtomicLabel[?] | ConnectorLabel | BinderLabel = fl match
case fl: K.ConnectorLabel => asFrontLabel(fl)
- case fl: K.PredicateLabel => asFrontLabel(fl)
+ case fl: K.AtomicLabel => asFrontLabel(fl)
case fl: K.BinderLabel => asFrontLabel(fl)
- def asFrontLabel(pl: K.PredicateLabel): PredicateLabel = pl match
- case pl: K.ConstantPredicateLabel => asFrontLabel(pl)
- case pl: K.SchematicVarOrPredLabel => asFrontLabel(pl)
+ def asFrontLabel(pl: K.AtomicLabel): AtomicLabel[?] = pl match
+ case pl: K.ConstantAtomicLabel => asFrontLabel(pl)
+ case pl: K.SchematicAtomicLabel => asFrontLabel(pl)
def asFrontLabel(cl: K.ConnectorLabel): ConnectorLabel = cl match
case cl: K.ConstantConnectorLabel => asFrontLabel(cl)
case cl: K.SchematicConnectorLabel => asFrontLabel(cl)
- def asFrontLabel[N <: Arity](cpl: K.ConstantPredicateLabel): ConstantPredicateLabelOfArity[N] = cpl.arity.asInstanceOf[N] match
+ def asFrontLabel[N <: Arity](cpl: K.ConstantAtomicLabel): ConstantAtomicLabelOfArity[N] = cpl.arity.asInstanceOf[N] match
case n: 0 => ConstantFormula(cpl.id)
case n: N => ConstantPredicateLabel(cpl.id, cpl.arity.asInstanceOf)
- def asFrontLabel(sfl: K.SchematicFormulaLabel): SchematicVarOrPredLabel | SchematicConnectorLabel[?] =
+ def asFrontLabel(sfl: K.SchematicFormulaLabel): SchematicAtomicLabel[?] | SchematicConnectorLabel[?] =
sfl match
case v: K.VariableFormulaLabel => asFrontLabel(v)
case v: K.SchematicPredicateLabel => asFrontLabel(v)
case v: K.SchematicConnectorLabel => asFrontLabel(v)
- def asFrontLabel(svop: K.SchematicVarOrPredLabel): SchematicVarOrPredLabel = svop match
+ def asFrontLabel(svop: K.SchematicAtomicLabel): SchematicAtomicLabel[?] = svop match
case v: K.VariableFormulaLabel => asFrontLabel(v)
case v: K.SchematicPredicateLabel => asFrontLabel(v)
def asFrontLabel(v: K.VariableFormulaLabel): VariableFormula = VariableFormula(v.id)
@@ -115,15 +112,15 @@ object FOLHelpers {
// Formula
def asFront(f: K.Formula): Formula = f match
- case f: K.PredicateFormula => asFront(f)
+ case f: K.AtomicFormula => asFront(f)
case f: K.ConnectorFormula => asFront(f)
case f: K.BinderFormula => asFront(f)
- def asFront(pf: K.PredicateFormula): Formula =
- asFrontLabel(pf.label)(pf.args.map(asFront))
+ def asFront(pf: K.AtomicFormula): Formula =
+ asFrontLabel(pf.label).applySeq(pf.args.map(asFront))
def asFront(cf: K.ConnectorFormula): Formula =
- asFrontLabel(cf.label)(cf.args.map(asFront))
+ asFrontLabel(cf.label).applyUnsafe(cf.args.map(asFront))
def asFront(bf: K.BinderFormula): BinderFormula =
- asFrontLabel(bf.label)(asFrontLabel(bf.bound), asFront(bf.inner))
+ asFrontLabel(bf.label).apply(asFrontLabel(bf.bound), asFront(bf.inner))
// Sequents
def asFront(s: K.Sequent): Sequent = Sequent(s.left.map(asFront), s.right.map(asFront))
diff --git a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
index 2f20405a6a962edb2b25020f9add0f4c59b92adf..2bc2a98405a173ff63d1821cf78421d53c3b8c2b 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
@@ -23,7 +23,7 @@ trait Lambdas extends Common {
assert(arity == bounds.length)
private val seqBounds = bounds.toSeq
- def apply(args: T ** N): R = body.substituteUnsafe((bounds zip args.toSeq).toMap)
+ def applyUnsafe(args: T ** N): R = body.substituteUnsafe((bounds zip args.toSeq).toMap)
def appUnsafe(args: Seq[T]): R = body.substituteUnsafe((bounds zip args.toSeq).toMap)
/**
@@ -61,11 +61,11 @@ trait Lambdas extends Common {
* Construct a Lambda expression with multiple variables
*/
def lambda[T <: LisaObject[T], R <: LisaObject[R], N <: Arity, Tu <: Tuple](bounds: Tu, body: R)(using Tuple.Union[Tu] <:< SchematicLabel[T], Tuple.Size[Tu] =:= N): LambdaExpression[T, R, N] = {
- val boundsSeq = bounds.asInstanceOf[SchematicLabel[T] *** N].toSeq
- LambdaExpression[T, R, N](boundsSeq, body, boundsSeq.length.asInstanceOf)
+ val boundsSeq = bounds.toList
+ LambdaExpression[T, R, N](boundsSeq.asInstanceOf, body, boundsSeq.length.asInstanceOf)
}
def lambda[T <: LisaObject[T], R <: LisaObject[R]](bounds: Seq[SchematicLabel[T]], body: R): LambdaExpression[T, R, ?] = {
- val boundsSeq = bounds.toSeq
+ val boundsSeq = bounds
LambdaExpression(boundsSeq, body, boundsSeq.length.asInstanceOf)
}
diff --git a/lisa-utils/src/main/scala/lisa/fol/Predef.scala b/lisa-utils/src/main/scala/lisa/fol/Predef.scala
index 4d280b389a7f801455fe920bca805d556a855136..c5cd8d3a7ab827e88796cb542cdfb31d62ad372f 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Predef.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Predef.scala
@@ -66,7 +66,7 @@ trait Predef extends Common {
val ∃! : ExistsOne.type = existsOne
extension (f: Formula) {
- def unary_! = Neg(f *: EmptyTuple)
+ def unary_! = Neg(f)
infix inline def ==>(g: Formula): Formula = Implies(f, g)
infix inline def <=>(g: Formula): Formula = Iff(f, g)
infix inline def /\(g: Formula): Formula = And(List(f, g))
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index 31c62f3c40029626c4745bea61cba5e90944eee8..8209575d40ad0fde4ebd18578b6a9709efe8bbc1 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -40,9 +40,9 @@ trait Sequents extends Common with lisa.fol.Lambdas {
p._2 match {
case l: LambdaExpression[Term, Term, ?] @unchecked if (l.bounds.isEmpty || l.bounds.head.isInstanceOf[Variable]) & l.body.isInstanceOf[Term] =>
(p._1.asInstanceOf, l)
- case s: TermLabel =>
+ case s: TermLabel[?] =>
val vars = nFreshId(Seq(s.id), s.arity).map(id => Variable(id))
- (sl, LambdaExpression(vars, s(vars), s.arity))
+ (sl, LambdaExpression(vars, s.applySeq(vars), s.arity))
}
}
)
@@ -53,9 +53,9 @@ trait Sequents extends Common with lisa.fol.Lambdas {
case sl: SchematicPredicateLabel[?] =>
p._2 match {
case l: LambdaExpression[Term, Formula, ?] @unchecked if (l.bounds.isEmpty || l.bounds.head.isInstanceOf[Variable]) & l.body.isInstanceOf[Formula] => (sl, l)
- case s: PredicateLabel =>
+ case s: AtomicLabel[?] =>
val vars = nFreshId(Seq(s.id), s.arity).map(id => Variable(id))
- (sl, LambdaExpression(vars, s(vars), s.arity))
+ (sl, LambdaExpression(vars, s.applySeq(vars), s.arity))
}
}
)
@@ -66,7 +66,7 @@ trait Sequents extends Common with lisa.fol.Lambdas {
case l: LambdaExpression[Formula, Formula, ?] @unchecked if (l.bounds.isEmpty || l.bounds.head.isInstanceOf[VariableFormula]) & l.body.isInstanceOf[Formula] => (sl, l)
case s: ConnectorLabel =>
val vars = nFreshId(Seq(s.id), s.arity).map(VariableFormula.apply)
- (sl, LambdaExpression(vars, s(vars), s.arity))
+ (sl, LambdaExpression(vars, s.applyUnsafe(vars), s.arity))
}
}
)
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
index 80f40640caa88e7b4e6322e3bb517ff961da7a8e..320ea5a6e74496b10f24e49dfca4c0c5f3376d43 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -43,7 +43,7 @@ object BasicStepTactic {
object RewriteTrue extends ProofTactic with ProofSequentTactic {
def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
val botK = bot.underlying
- if (!K.isSameSequent(botK, () `K|-` K.PredicateFormula(K.top, Nil)))
+ if (!K.isSameSequent(botK, () `K|-` K.AtomicFormula(K.top, Nil)))
proof.InvalidProofTactic("The desired conclusion is not a trivial tautology.")
else
proof.ValidProofTactic(bot, Seq(K.RestateTrue(botK)), Seq())
@@ -130,7 +130,7 @@ object BasicStepTactic {
if (!pivot.isEmpty && pivot.tail.isEmpty)
pivot.head match {
- case F.ConnectorFormula(F.And, Seq(phi, psi)) =>
+ case F.AppliedConnector(F.And, Seq(phi, psi)) =>
if (premiseSequent.left.contains(phi))
LeftAnd.withParameters(phi, psi)(premise)(bot)
else
@@ -280,7 +280,7 @@ object BasicStepTactic {
proof.InvalidProofTactic("Right-hand side of conclusion is not a superset of the premises.")
else
pivot.head match {
- case F.ConnectorFormula(F.Implies, Seq(phi, psi)) => LeftIff.withParameters(phi, psi)(premise)(bot)
+ case F.AppliedConnector(F.Implies, Seq(phi, psi)) => LeftIff.withParameters(phi, psi)(premise)(bot)
case _ => proof.InvalidProofTactic("Could not infer a pivot implication from premise.")
}
}
@@ -501,7 +501,7 @@ object BasicStepTactic {
K.BinderFormula(
K.Forall,
xK,
- K.ConnectorFormula(K.Iff, List(K.PredicateFormula(K.equality, List(K.VariableTerm(xK), K.VariableTerm(y))), phiK))
+ K.ConnectorFormula(K.Iff, List(K.AtomicFormula(K.equality, List(K.VariableTerm(xK), K.VariableTerm(y))), phiK))
)
)
lazy val quantified = K.BinderFormula(K.ExistsOne, xK, phiK)
@@ -528,7 +528,7 @@ object BasicStepTactic {
else if (instantiatedPivot.tail.isEmpty) {
instantiatedPivot.head match {
// ∃_. ∀x. _ ⇔ φ == extract ==> x, phi
- case F.BinderFormula(F.Exists, _, F.BinderFormula(F.Forall, x, F.ConnectorFormula(F.Iff, Seq(_, phi)))) => LeftExistsOne.withParameters(phi, x)(premise)(bot)
+ case F.BinderFormula(F.Exists, _, F.BinderFormula(F.Forall, x, F.AppliedConnector(F.Iff, Seq(_, phi)))) => LeftExistsOne.withParameters(phi, x)(premise)(bot)
case _ => proof.InvalidProofTactic("Could not infer an existentially quantified pivot from premise and conclusion.")
}
} else
@@ -624,7 +624,7 @@ object BasicStepTactic {
if (!pivot.isEmpty && pivot.tail.isEmpty)
pivot.head match {
- case F.ConnectorFormula(F.Or, Seq(phi, psi)) =>
+ case F.AppliedConnector(F.Or, Seq(phi, psi)) =>
if (premiseSequent.left.contains(phi))
RightOr.withParameters(phi, psi)(premise)(bot)
else
@@ -728,7 +728,7 @@ object BasicStepTactic {
proof.InvalidProofTactic("Left-hand side of conclusion is not a superset of the premises.")
else if (pivot.tail.isEmpty)
pivot.head match {
- case F.ConnectorFormula(F.Implies, Seq(phi, psi)) => RightIff.withParameters(phi, psi)(prem1, prem2)(bot)
+ case F.AppliedConnector(F.Implies, Seq(phi, psi)) => RightIff.withParameters(phi, psi)(prem1, prem2)(bot)
case _ => proof.InvalidProofTactic("Could not infer an implication as pivot from premise and conclusion.")
}
else
@@ -954,7 +954,7 @@ object BasicStepTactic {
K.BinderFormula(
K.Forall,
xK,
- K.ConnectorFormula(K.Iff, List(K.PredicateFormula(K.equality, List(K.VariableTerm(xK), K.VariableTerm(y))), phiK))
+ K.ConnectorFormula(K.Iff, List(K.AtomicFormula(K.equality, List(K.VariableTerm(xK), K.VariableTerm(y))), phiK))
)
)
lazy val quantified = K.BinderFormula(K.ExistsOne, xK, phiK)
@@ -981,7 +981,7 @@ object BasicStepTactic {
else if (instantiatedPivot.tail.isEmpty) {
instantiatedPivot.head match {
// ∃_. ∀x. _ ⇔ φ == extract ==> x, phi
- case F.BinderFormula(F.Exists, _, F.BinderFormula(F.Forall, x, F.ConnectorFormula(F.Iff, Seq(_, phi)))) =>
+ case F.BinderFormula(F.Exists, _, F.BinderFormula(F.Forall, x, F.AppliedConnector(F.Iff, Seq(_, phi)))) =>
RightExistsOne.withParameters(phi, x)(premise)(bot)
case _ => proof.InvalidProofTactic("Could not infer an existentially quantified pivot from premise and conclusion.")
}
@@ -1036,7 +1036,7 @@ object BasicStepTactic {
proof.InvalidProofTactic("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
else
faK match {
- case K.PredicateFormula(K.equality, Seq(left, right)) =>
+ case K.AtomicFormula(K.equality, Seq(left, right)) =>
if (K.isSameTerm(left, right))
proof.ValidProofTactic(bot, Seq(K.LeftRefl(botK, -1, faK)), Seq(premise))
else
@@ -1071,7 +1071,7 @@ object BasicStepTactic {
proof.InvalidProofTactic("Right-hand side of conclusion does not contain φ.")
else
faK match {
- case K.PredicateFormula(K.equality, Seq(left, right)) =>
+ case K.AtomicFormula(K.equality, Seq(left, right)) =>
if (K.isSameTerm(left, right))
proof.ValidProofTactic(bot, Seq(K.RightRefl(botK, faK)), Seq())
else
@@ -1087,8 +1087,8 @@ object BasicStepTactic {
val pivot: Option[F.Formula] = bot.right.find(f =>
val Eq = F.equality // (F.equality: (F.|->[F.**[F.Term, 2], F.Formula]))
f match {
- case F.PredicateFormula(e, Seq(l, r)) =>
- (F.equality: F.PredicateLabel) == (e: F.PredicateLabel) && l == r // termequality
+ case F.AppliedPredicate(e, Seq(l, r)) =>
+ (F.equality) == (e) && l == r // termequality
case _ => false
}
)
@@ -1124,7 +1124,7 @@ object BasicStepTactic {
lazy val (s_es, t_es) = equalsK.unzip
lazy val phi_s = lambdaPhiK(s_es)
lazy val phi_t = lambdaPhiK(t_es)
- lazy val equalities = equalsK map { case (s, t) => K.PredicateFormula(K.equality, Seq(s, t)) }
+ lazy val equalities = equalsK map { case (s, t) => K.AtomicFormula(K.equality, Seq(s, t)) }
if (!K.isSameSet(botK.right, premiseSequent.right))
proof.InvalidProofTactic("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
@@ -1159,7 +1159,7 @@ object BasicStepTactic {
lazy val (s_es, t_es) = equalsK.unzip
lazy val phi_s = lambdaPhiK(s_es)
lazy val phi_t = lambdaPhiK(t_es)
- lazy val equalities = equalsK map { case (s, t) => K.PredicateFormula(K.equality, Seq(s, t)) }
+ lazy val equalities = equalsK map { case (s, t) => K.AtomicFormula(K.equality, Seq(s, t)) }
if (!K.isSameSet(botK.left, premiseSequent.left ++ equalities))
proof.InvalidProofTactic("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (s=t)_.")
@@ -1175,10 +1175,10 @@ object BasicStepTactic {
def apply2(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
lazy val premiseSequent = proof.getSequent(premise)
- val premRight = F.ConnectorFormula(F.Or, premiseSequent.right.toSeq)
- val botRight = F.ConnectorFormula(F.Or, bot.right.toSeq)
+ val premRight = F.AppliedConnector(F.Or, premiseSequent.right.toSeq)
+ val botRight = F.AppliedConnector(F.Or, bot.right.toSeq)
- val equalities = bot.left.toSeq.collect { case F.PredicateFormula(F.equality, Seq(l, r)) => (l, r) }
+ val equalities = bot.left.toSeq.collect { case F.AppliedPredicate(F.equality, Seq(l, r)) => (l, r) }
val undereqs = equalities.toList.map(p => (p._1.underlying, p._2.underlying))
val canReach = UnificationUtils.getContextFormula(
first = premRight,
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
index 23ba931d5186fab1f474e6c1c9833bfadc14f84f..b6541e71d0a2b720ac7cc22ae5b9d5a478998532 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
@@ -146,24 +146,30 @@ trait ProofsHelpers {
class The(val out: Variable, val f: Formula)(
val just: JUSTIFICATION
)
- class definitionWithVars[N <: Arity](val args: Variable *** N) {
+ class definitionWithVars[N <: Arity](val args: Seq[Variable]) {
// inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(t: Term) = simpleDefinition(lambda(args, t, args.length))
// inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(f: Formula) = predicateDefinition(lambda(args, f, args.length))
- inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(t: The): ConstantFunctionLabelOfArity[N] =
- FunctionDefinition[N](name.value, line.value, file.value)(args.toSeq, t.out, t.f, t.just).label
+ inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(t: The): ConstantTermLabelOfArity[N] =
+ FunctionDefinition[N](name.value, line.value, file.value)(args, t.out, t.f, t.just).label
- inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(term: Term): ConstantFunctionLabelOfArity[N] =
- SimpleFunctionDefinition[N](name.value, line.value, file.value)(lambda(args.toSeq, term).asInstanceOf).label
+ inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(term: Term): ConstantTermLabelOfArity[N] =
+ SimpleFunctionDefinition[N](name.value, line.value, file.value)(lambda(args, term).asInstanceOf).label
- inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(formula: Formula): ConstantPredicateLabelOfArity[N] =
- PredicateDefinition[N](name.value, line.value, file.value)(lambda(args.toSeq, formula).asInstanceOf).label
+ inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(formula: Formula): ConstantAtomicLabelOfArity[N] =
+ PredicateDefinition[N](name.value, line.value, file.value)(lambda(args, formula).asInstanceOf).label
}
- def DEF[N <: Arity, T <: Tuple](args: T)(using Tuple.Size[T] =:= N, Tuple.Union[T] <:< Variable): definitionWithVars[N] = new definitionWithVars[N](args.asInstanceOf)
- def DEF(arg: Variable): definitionWithVars[1] = new definitionWithVars[1](EmptyTuple.*:[Variable, EmptyTuple](arg)) // todo conversion to empty tuple gets bad type
+ def DEF(): definitionWithVars[0] = new definitionWithVars[0](Nil)
+ def DEF(a: Variable): definitionWithVars[1] = new definitionWithVars[1](Seq(a))
+ def DEF(a: Variable, b: Variable): definitionWithVars[2] = new definitionWithVars[2](Seq(a, b))
+ def DEF(a: Variable, b: Variable, c: Variable): definitionWithVars[3] = new definitionWithVars[3](Seq(a, b, c))
+ def DEF(a: Variable, b: Variable, c: Variable, d: Variable): definitionWithVars[4] = new definitionWithVars[4](Seq(a, b, c, d))
+ def DEF(a: Variable, b: Variable, c: Variable, d: Variable, e: Variable): definitionWithVars[5] = new definitionWithVars[5](Seq(a, b, c, d, e))
+ def DEF(a: Variable, b: Variable, c: Variable, d: Variable, e: Variable, f: Variable): definitionWithVars[6] = new definitionWithVars[6](Seq(a, b, c, d, e, f))
+ def DEF(a: Variable, b: Variable, c: Variable, d: Variable, e: Variable, f: Variable, g: Variable): definitionWithVars[7] = new definitionWithVars[7](Seq(a, b, c, d, e, f, g))
// def DEF: definitionWithVars[0] = new definitionWithVars[0](EmptyTuple) //todo conversion to empty tuple gets bad type
@@ -178,12 +184,13 @@ trait ProofsHelpers {
val f: F.Formula,
j: JUSTIFICATION
) extends DEFINITION(line, file) {
+ def funWithArgs = label.applySeq(vars)
override def repr: String =
- s" ${if (withSorry) " Sorry" else ""} Definition of function symbol ${label(vars)} := the ${out} such that ${(out === label(vars)) <=> f})\n"
+ s" ${if (withSorry) " Sorry" else ""} Definition of function symbol ${funWithArgs} := the ${out} such that ${(out === funWithArgs) <=> f})\n"
// val expr = LambdaExpression[Term, Formula, N](vars, f, valueOf[N])
- lazy val label: ConstantFunctionLabelOfArity[N] = (if (vars.length == 0) F.Constant(name) else F.ConstantFunctionLabel[N](name, vars.length.asInstanceOf)).asInstanceOf
+ lazy val label: ConstantTermLabelOfArity[N] = (if (vars.length == 0) F.Constant(name) else F.ConstantFunctionLabel[N](name, vars.length.asInstanceOf)).asInstanceOf
val innerJustification: theory.FunctionDefinition = {
val conclusion: F.Sequent = j.statement
@@ -209,8 +216,8 @@ trait ProofsHelpers {
}
val proven = conclusion.right.head match {
case F.BinderFormula(F.ExistsOne, bound, inner) => inner
- case F.BinderFormula(F.Exists, x, F.BinderFormula(F.Forall, y, F.ConnectorFormula(F.Iff, Seq(l, r)))) if F.isSame(l, x === y) => r
- case F.BinderFormula(F.Exists, x, F.BinderFormula(F.Forall, y, F.ConnectorFormula(F.Iff, Seq(l, r)))) if F.isSame(r, x === y) => l
+ case F.BinderFormula(F.Exists, x, F.BinderFormula(F.Forall, y, F.AppliedConnector(F.Iff, Seq(l, r)))) if F.isSame(l, x === y) => r
+ case F.BinderFormula(F.Exists, x, F.BinderFormula(F.Forall, y, F.AppliedConnector(F.Iff, Seq(l, r)))) if F.isSame(r, x === y) => l
case _ =>
om.lisaThrow(
UserInvalidDefinitionException(
@@ -266,13 +273,7 @@ trait ProofsHelpers {
() |- F.Forall(
out,
Iff(
- equality(
- (label match {
- case l: F.Constant => l
- case l: F.ConstantFunctionLabel[?] => l(vars)
- }),
- out
- ),
+ equality(label.applySeq(vars), out),
f
)
)
@@ -306,11 +307,11 @@ trait ProofsHelpers {
lazy val vars: Seq[F.Variable] = lambda.bounds.asInstanceOf
val arity = lambda.arity
- lazy val label: ConstantPredicateLabelOfArity[N] = {
+ lazy val label: ConstantAtomicLabelOfArity[N] = {
(
if (vars.length == 0) F.ConstantFormula(name)
else F.ConstantPredicateLabel[N](name, vars.length.asInstanceOf[N])
- ).asInstanceOf[ConstantPredicateLabelOfArity[N]]
+ ).asInstanceOf[ConstantAtomicLabelOfArity[N]]
}
val innerJustification: theory.PredicateDefinition = {
@@ -354,14 +355,7 @@ trait ProofsHelpers {
}
}
- val statement: F.Sequent = () |- Iff(
- (label match {
- case l: F.ConstantFormula => l
- case l: F.ConstantPredicateLabel[?] => l(vars)
- }),
- lambda.body
- )
-
+ val statement: F.Sequent = () |- Iff(label.applySeq(vars), lambda.body)
library.last = Some(this)
}
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index 2fa698e2256a674ed7d05dbe561ae3e409140128..24614ca346eaae469dfffeba1a11fb1a57d67c31 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -41,7 +41,7 @@ trait WithTheorems {
fact: Fact,
insts: Seq[F.SubstPair] /*,
instsConn: Map[K.SchematicConnectorLabel, K.LambdaFormulaFormula],
- instsPred: Map[K.SchematicVarOrPredLabel, K.LambdaTermFormula],
+ instsPred: Map[K.SchematicAtomicLabel, K.LambdaTermFormula],
instsTerm: Map[K.SchematicTermLabel, K.LambdaTermTerm]*/
) {
val baseFormula: F.Sequent = sequentOfFact(fact)
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 62381a492a9fe2196e8ef6c769bc4ab35b5d2175..122f418d0380e12854820d9ba339db22ec967a2a 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -54,12 +54,12 @@ object KernelHelpers {
}
}
- extension [L <: PredicateLabel](label: L) {
- def apply(args: Term*): Formula = PredicateFormula(label, args)
+ extension [L <: AtomicLabel](label: L) {
+ def apply(args: Term*): Formula = AtomicFormula(label, args)
@targetName("applySeq")
- def apply(args: Seq[Term]): Formula = PredicateFormula(label, args)
+ def apply(args: Seq[Term]): Formula = AtomicFormula(label, args)
def unapply(f: Formula): Option[Seq[Term]] = f match {
- case PredicateFormula(`label`, args) => Some(args)
+ case AtomicFormula(`label`, args) => Some(args)
case _ => None
}
}
@@ -93,18 +93,18 @@ object KernelHelpers {
}
extension (t: Term) {
- infix def ===(u: Term): Formula = PredicateFormula(equality, Seq(t, u))
- infix def ＝(u: Term): Formula = PredicateFormula(equality, Seq(t, u))
+ infix def ===(u: Term): Formula = AtomicFormula(equality, Seq(t, u))
+ infix def ＝(u: Term): Formula = AtomicFormula(equality, Seq(t, u))
}
/* Conversions */
given Conversion[TermLabel, Term] = Term(_, Seq())
given Conversion[Term, TermLabel] = _.label
- given Conversion[PredicateLabel, PredicateFormula] = PredicateFormula(_, Seq())
- given Conversion[PredicateFormula, PredicateLabel] = _.label
+ given Conversion[AtomicLabel, AtomicFormula] = AtomicFormula(_, Seq())
+ given Conversion[AtomicFormula, AtomicLabel] = _.label
- given Conversion[VariableFormulaLabel, PredicateFormula] = PredicateFormula(_, Seq())
+ given Conversion[VariableFormulaLabel, AtomicFormula] = AtomicFormula(_, Seq())
given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3)
given Conversion[Formula, Sequent] = () |- _
@@ -196,7 +196,7 @@ object KernelHelpers {
// Instatiation functions for formulas lifted to sequents.
- def instantiatePredicateSchemaInSequent(s: Sequent, m: Map[SchematicVarOrPredLabel, LambdaTermFormula]): Sequent = {
+ def instantiatePredicateSchemaInSequent(s: Sequent, m: Map[SchematicAtomicLabel, LambdaTermFormula]): Sequent = {
s.left.map(phi => instantiatePredicateSchemas(phi, m)) |- s.right.map(phi => instantiatePredicateSchemas(phi, m))
}
@@ -207,7 +207,7 @@ object KernelHelpers {
def instantiateSchemaInSequent(
s: Sequent,
mCon: Map[SchematicConnectorLabel, LambdaFormulaFormula],
- mPred: Map[SchematicVarOrPredLabel, LambdaTermFormula],
+ mPred: Map[SchematicAtomicLabel, LambdaTermFormula],
mTerm: Map[SchematicTermLabel, LambdaTermTerm]
): Sequent = {
s.left.map(phi => instantiateSchemas(phi, mCon, mPred, mTerm)) |- s.right.map(phi => instantiateSchemas(phi, mCon, mPred, mTerm))
@@ -372,7 +372,7 @@ object KernelHelpers {
* of the theorem to have more explicit writing and for sanity check. See also [[lisa.kernel.proof.RunningTheory.makePredicateDefinition]]
*/
def predicateDefinition(symbol: String, expression: LambdaTermFormula): RunningTheoryJudgement[theory.PredicateDefinition] = {
- val label = ConstantPredicateLabel(symbol, expression.vars.size)
+ val label = ConstantAtomicLabel(symbol, expression.vars.size)
theory.makePredicateDefinition(label, expression)
}
@@ -389,9 +389,9 @@ object KernelHelpers {
* @return The List of undefined symols
*/
def findUndefinedSymbols(phi: Formula): Set[ConstantLabel] = phi match {
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
label match {
- case l: ConstantPredicateLabel => ((if (theory.isSymbol(l)) Nil else List(l)) ++ args.flatMap(findUndefinedSymbols)).toSet
+ case l: ConstantAtomicLabel => ((if (theory.isSymbol(l)) Nil else List(l)) ++ args.flatMap(findUndefinedSymbols)).toSet
case _ => args.flatMap(findUndefinedSymbols).toSet
}
case ConnectorFormula(label, args) => args.flatMap(findUndefinedSymbols).toSet
diff --git a/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala b/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
index cc8980574b7242aa7cf59fd712e331ea29677743..5f620aa8757cd7ce1e0e7ff9758c865bab3c7807 100644
--- a/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
@@ -172,8 +172,8 @@ object ProofsShrink {
isSubset(subset.left, superset.left) && isSubset(subset.right, superset.right)
def schematicConnectorLabels(sequent: Sequent): Set[SchematicConnectorLabel] =
(sequent.left ++ sequent.right).flatMap(_.schematicConnectorLabels)
- def schematicPredicatesLabels(sequent: Sequent): Set[SchematicVarOrPredLabel] =
- (sequent.left ++ sequent.right).flatMap(_.schematicPredicateLabels)
+ def schematicPredicatesLabels(sequent: Sequent): Set[SchematicAtomicLabel] =
+ (sequent.left ++ sequent.right).flatMap(_.schematicAtomicLabels)
def schematicTermLabels(sequent: Sequent): Set[SchematicTermLabel] =
(sequent.left ++ sequent.right).flatMap(_.schematicTermLabels)
def schematicLabels(sequent: Sequent): Set[SchematicLabel] = {
diff --git a/lisa-utils/src/main/scala/lisa/utils/Serialization.scala b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
index 8abcd231a65c284edc30f0618e059f18abe4b75a..88e0e8dbda4a67ab4e15612b9ce9ff227d8d281f 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
@@ -52,7 +52,7 @@ object Serialization {
// Injectively represent a FormulaLabel as a string.
def formulaLabelToString(label: FormulaLabel): String =
label match
- case l: ConstantPredicateLabel => "cpl_" + l.id.name + "_" + l.id.no + "_" + l.arity
+ case l: ConstantAtomicLabel => "cpl_" + l.id.name + "_" + l.id.no + "_" + l.arity
case l: SchematicPredicateLabel => "spl_" + l.id.name + "_" + l.id.no + "_" + l.arity
case l: ConstantConnectorLabel => "ccl_" + l.id.name + "_" + l.id.no + "_" + l.arity
case l: SchematicConnectorLabel => "scl_" + l.id.name + "_" + l.id.no + "_" + l.arity
@@ -79,7 +79,7 @@ object Serialization {
// write a formula label to an OutputStream
def formulaLabelToDOS(label: FormulaLabel, dos: DataOutputStream): Unit =
label match
- case l: ConstantPredicateLabel =>
+ case l: ConstantAtomicLabel =>
dos.writeByte(3)
dos.writeUTF(l.id.name)
dos.writeInt(l.id.no)
@@ -133,7 +133,7 @@ object Serialization {
case Some(line) => line
case None =>
val nextLine = formula match
- case PredicateFormula(label, args) =>
+ case AtomicFormula(label, args) =>
val na = args.map(t => lineOfTerm(t))
formulaLabelToDOS(label, treesDOS)
na.foreach(t => treesDOS.writeInt(t))
@@ -426,7 +426,7 @@ object Serialization {
val name = dis.readUTF()
val no = dis.readInt()
val arity = dis.readInt()
- ConstantPredicateLabel(Identifier(name, no), arity)
+ ConstantAtomicLabel(Identifier(name, no), arity)
case 4 =>
val name = dis.readUTF()
val no = dis.readInt()
@@ -469,9 +469,9 @@ object Serialization {
termMap(lineNo) = Term(l, args)
case l: FormulaLabel =>
val formula = label match
- case l: PredicateLabel =>
+ case l: AtomicLabel =>
val args = (1 to l.arity).map(_ => termMap(treesDIS.readInt())).toSeq
- PredicateFormula(l, args)
+ AtomicFormula(l, args)
case l: ConnectorLabel =>
val ar = treesDIS.readShort()
val args = (1 to ar).map(_ => formulaMap(treesDIS.readInt())).toSeq
@@ -590,7 +590,7 @@ object Serialization {
sequentFromProofDIS(),
proofDIS.readInt(),
(1 to proofDIS.readShort()).map(_ => (labelFromInputStream(proofDIS).asInstanceOf[SchematicConnectorLabel], lffFromProofDIS())).toMap,
- (1 to proofDIS.readShort()).map(_ => (labelFromInputStream(proofDIS).asInstanceOf[SchematicVarOrPredLabel], ltfFromProofDIS())).toMap,
+ (1 to proofDIS.readShort()).map(_ => (labelFromInputStream(proofDIS).asInstanceOf[SchematicAtomicLabel], ltfFromProofDIS())).toMap,
(1 to proofDIS.readShort()).map(_ => (labelFromInputStream(proofDIS).asInstanceOf[SchematicTermLabel], lttFromProofDIS())).toMap
)
else if (psType == sorry) Sorry(sequentFromProofDIS())
@@ -659,7 +659,7 @@ object Serialization {
case Array(name, no, arity) => theory.getDefinition(ConstantFunctionLabel(Identifier(name, no.toInt), arity.toInt)).get
case 'p' =>
name.split("_") match
- case Array(name, no, arity) => theory.getDefinition(ConstantPredicateLabel(Identifier(name, no.toInt), arity.toInt)).get
+ case Array(name, no, arity) => theory.getDefinition(ConstantAtomicLabel(Identifier(name, no.toInt), arity.toInt)).get
}
if debug then
// To avoid conflicts where a theorem already exists, for example in test suits.
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 683905e09a76343517b06dc6b0b1c81aa06baf8b..eb45a000161d23a55ecacf5c4c62d7fd1587cd7e 100644
--- a/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
@@ -43,7 +43,7 @@ object UnreachableException extends ParserException("Internal error: expected un
class PrintFailedException(inp: Sequent | Formula | Term) extends ParserException(s"Printing of $inp failed unexpectedly")
/**
- * @param synonymToCanonical information about synonyms that correspond to the same FunctionLabel / PredicateLabel.
+ * @param synonymToCanonical information about synonyms that correspond to the same FunctionLabel / AtomicLabel.
* Can be constructed with [[lisa.utils.SynonymInfoBuilder]]
* @param infixPredicates list of infix predicates' names
* @param infixFunctions list of infix functions and their associativity in the decreasing order of priority
@@ -140,7 +140,7 @@ class Parser(
.printTermula(f.toTermula)
.getOrElse({
f match {
- case PredicateFormula(_, args) => args.foreach(printTerm)
+ case AtomicFormula(_, args) => args.foreach(printTerm)
case ConnectorFormula(_, args) => args.foreach(printFormula)
case BinderFormula(_, _, inner) => printFormula(inner)
}
@@ -312,24 +312,24 @@ class Parser(
* <p> - to be converted to a formula, `args` of the termula are interpreted as formulas until a predicate application is observed;
* `args` of the predicate application are terms.
*
- * <p> Convention: since the difference between `TermLabel`s and `PredicateLabel`s is purely semantic and Termula needs
+ * <p> Convention: since the difference between `TermLabel`s and `AtomicLabel`s is purely semantic and Termula needs
* FormulaLabels (because of connector and binder labels), all TermLabels are translated to the corresponding
* PredicateLabels (see [[toTermula]]).
*
- * @param label `PredicateLabel` for predicates and functions, `ConnectorLabel` or `BinderLabel`
- * @param args Predicate / function arguments for `PredicateLabel`, connected formulas for `ConnectorLabel`,
+ * @param label `AtomicLabel` for predicates and functions, `ConnectorLabel` or `BinderLabel`
+ * @param args Predicate / function arguments for `AtomicLabel`, connected formulas for `ConnectorLabel`,
* `Seq(VariableFormulaLabel(bound), inner)` for `BinderLabel`
*/
case class Termula(label: RangedLabel, args: Seq[Termula], range: (Int, Int)) {
def toTerm: Term = label.folLabel match {
case _: BinderLabel | _: ConnectorLabel => throw ExpectedTermGotFormula(range)
- case t: ConstantPredicateLabel => Term(ConstantFunctionLabel(t.id, t.arity), args.map(_.toTerm))
+ case t: ConstantAtomicLabel => Term(ConstantFunctionLabel(t.id, t.arity), args.map(_.toTerm))
case t: SchematicPredicateLabel => Term(SchematicFunctionLabel(t.id, t.arity), args.map(_.toTerm))
case v: VariableFormulaLabel => Term(VariableLabel(v.id), Seq())
}
def toFormula: Formula = label.folLabel match {
- case p: PredicateLabel => PredicateFormula(p, args.map(_.toTerm))
+ case p: AtomicLabel => AtomicFormula(p, args.map(_.toTerm))
case c: ConnectorLabel => ConnectorFormula(c, args.map(_.toFormula))
case b: BinderLabel =>
args match {
@@ -349,7 +349,7 @@ class Parser(
}
f match {
- case PredicateFormula(label, args) => Termula(label, args.map(_.toTermula), UNKNOWN_RANGE)
+ case AtomicFormula(label, args) => Termula(label, args.map(_.toTermula), UNKNOWN_RANGE)
// case ConnectorFormula(And | Or, Seq(singleArg)) => singleArg.toTermula
case ConnectorFormula(label, args) => Termula(label, args.map(_.toTermula), UNKNOWN_RANGE)
case BinderFormula(label, bound, inner) => Termula(label, Seq(Termula(VariableFormulaLabel(bound.id), Seq(), UNKNOWN_RANGE), inner.toTermula), UNKNOWN_RANGE)
@@ -363,7 +363,7 @@ class Parser(
def apply(f: FOL.FormulaLabel): RangedLabel = RangedLabel(f, UNKNOWN_RANGE)
}
val newLabel = t.label match {
- case ConstantFunctionLabel(id, arity) => ConstantPredicateLabel(id, arity)
+ case ConstantFunctionLabel(id, arity) => ConstantAtomicLabel(id, arity)
case SchematicFunctionLabel(id, arity) => SchematicPredicateLabel(id, arity)
case VariableLabel(id) => VariableFormulaLabel(id)
}
@@ -499,7 +499,7 @@ class Parser(
t.label.folLabel match {
case VariableFormulaLabel(id) => SchematicToken(id, t.label.range) ~ None
case SchematicPredicateLabel(id, _) => SchematicToken(id, t.range) ~ Some(RangedTermulaSeq(t.args, argsRange))
- case ConstantPredicateLabel(id, arity) =>
+ case ConstantAtomicLabel(id, arity) =>
ConstantToken(synonymToCanonical.getPrintName(id), t.label.range) ~
(if (arity == 0) None else Some(RangedTermulaSeq(t.args, argsRange)))
case _ => throw UnreachableException
@@ -512,7 +512,7 @@ class Parser(
val args: Seq[Termula] = optArgs.map(_.ts).getOrElse(Seq())
val l = p match {
- case ConstantToken(id, _) => ConstantPredicateLabel(synonymToCanonical.getInternalName(id), args.size)
+ case ConstantToken(id, _) => ConstantAtomicLabel(synonymToCanonical.getInternalName(id), args.size)
case SchematicToken(id, _) =>
if (args.isEmpty) VariableFormulaLabel(id) else SchematicPredicateLabel(id, args.size)
case SchematicConnectorToken(id, _) => SchematicConnectorLabel(id, args.size)
@@ -523,7 +523,7 @@ class Parser(
Termula(RangedLabel(l, p.range), args, (p.range._1, optArgs.map(_.range._2).getOrElse(p.range._2)))
},
{
- case t @ Termula(RangedLabel(_: PredicateLabel, _), _, _) => Seq(reconstructPrefixApplication(t))
+ case t @ Termula(RangedLabel(_: AtomicLabel, _), _, _) => Seq(reconstructPrefixApplication(t))
case t @ Termula(RangedLabel(SchematicConnectorLabel(id, _), r), args, _) =>
val argsRange = (t.label.range._2 + 1, t.range._2)
Seq(SchematicConnectorToken(id, r) ~ Some(RangedTermulaSeq(args, argsRange)))
@@ -541,11 +541,11 @@ class Parser(
val infixFunctionLabels: List[PrecedenceLevel[RangedLabel]] = infixFunctions.map({ case (l, assoc) =>
elem(InfixKind(l)).map[RangedLabel](
{
- case InfixToken(`l`, range) => RangedLabel(ConstantPredicateLabel(synonymToCanonical.getInternalName(l), INFIX_ARITY), range)
+ case InfixToken(`l`, range) => RangedLabel(ConstantAtomicLabel(synonymToCanonical.getInternalName(l), INFIX_ARITY), range)
case _ => throw UnreachableException
},
{
- case RangedLabel(ConstantPredicateLabel(id, INFIX_ARITY), range) => Seq(InfixToken(synonymToCanonical.getPrintName(id), range))
+ case RangedLabel(ConstantAtomicLabel(id, INFIX_ARITY), range) => Seq(InfixToken(synonymToCanonical.getPrintName(id), range))
case _ => throw UnreachableException
}
) has assoc
@@ -554,11 +554,11 @@ class Parser(
val infixPredicateLabels: List[PrecedenceLevel[RangedLabel]] = infixPredicates.map(l =>
elem(InfixKind(l)).map[RangedLabel](
{
- case InfixToken(`l`, range) => RangedLabel(ConstantPredicateLabel(synonymToCanonical.getInternalName(l), INFIX_ARITY), range)
+ case InfixToken(`l`, range) => RangedLabel(ConstantAtomicLabel(synonymToCanonical.getInternalName(l), INFIX_ARITY), range)
case _ => throw UnreachableException
},
{
- case RangedLabel(ConstantPredicateLabel(id, INFIX_ARITY), range) => Seq(InfixToken(synonymToCanonical.getPrintName(id), range))
+ case RangedLabel(ConstantAtomicLabel(id, INFIX_ARITY), range) => Seq(InfixToken(synonymToCanonical.getPrintName(id), range))
case _ => throw UnreachableException
}
) has Associativity.None
@@ -609,7 +609,7 @@ class Parser(
)(
(l, conn, r) => Termula(conn, Seq(l, r), (l.range._1, r.range._2)),
{
- case Termula(pred @ RangedLabel(ConstantPredicateLabel(_, INFIX_ARITY), _), Seq(l, r), _) => (l, pred, r)
+ case Termula(pred @ RangedLabel(ConstantAtomicLabel(_, INFIX_ARITY), _), Seq(l, r), _) => (l, pred, r)
case Termula(conn @ RangedLabel(_: ConnectorLabel, _), Seq(l, r), _) =>
(l, conn, r)
case Termula(conn @ RangedLabel(_: ConnectorLabel, _), l +: rest, _) if rest.nonEmpty =>
diff --git a/lisa-utils/src/main/scala/lisa/utils/parsing/SynonymInfo.scala b/lisa-utils/src/main/scala/lisa/utils/parsing/SynonymInfo.scala
index f930b5eff2c13edf4dfdee2ccdd53ce68995a2af..2ab844296813fd706ac14b4865ab16f1147e353a 100644
--- a/lisa-utils/src/main/scala/lisa/utils/parsing/SynonymInfo.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/parsing/SynonymInfo.scala
@@ -12,7 +12,7 @@ case class SynonymInfo(private val synonymToCanonical: Map[String, CanonicalId])
def getPrintName(id: String): String = synonymToCanonical.get(id).map(_.print).getOrElse(id)
/**
- * @return the synonym of `id` that is used to construct the corresponding `ConstantPredicateLabel` or
+ * @return the synonym of `id` that is used to construct the corresponding `ConstantAtomicLabel` or
* `ConstantFunctionLabel`. If not available, `id` has no known synonyms, so return `id` itself.
*/
def getInternalName(id: String): String = synonymToCanonical.get(id).map(_.internal).getOrElse(id)
diff --git a/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala b/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
index 41e3ffb040fcc2a3393e28b7489990ab9b8c5390..18202949f2e08f7745a6c7a5175e48d2eda20051 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
@@ -32,7 +32,7 @@ object KernelParser {
*/
def convertToKernel(formula: FOF.Formula): K.Formula = {
formula match {
- case FOF.AtomicFormula(f, args) => K.PredicateFormula(K.ConstantPredicateLabel(f, args.size), args map convertTermToKernel)
+ case FOF.AtomicFormula(f, args) => K.AtomicFormula(K.ConstantAtomicLabel(f, args.size), args map convertTermToKernel)
case FOF.QuantifiedFormula(quantifier, variableList, body) =>
quantifier match {
case FOF.! => variableList.foldRight(convertToKernel(body))((s, f) => K.Forall(K.VariableLabel(s), f))
@@ -63,8 +63,8 @@ object KernelParser {
K.ConnectorFormula(
K.Or,
formula.map {
- case CNF.PositiveAtomic(formula) => K.PredicateFormula(K.ConstantPredicateLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
- case CNF.NegativeAtomic(formula) => !K.PredicateFormula(K.ConstantPredicateLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
+ case CNF.PositiveAtomic(formula) => K.AtomicFormula(K.ConstantAtomicLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
+ case CNF.NegativeAtomic(formula) => !K.AtomicFormula(K.ConstantAtomicLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
case CNF.Equality(left, right) => K.equality(convertTermToKernel(left), convertTermToKernel(right))
case CNF.Inequality(left, right) => !K.equality(convertTermToKernel(left), convertTermToKernel(right))
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/unification/UnificationUtils.scala b/lisa-utils/src/main/scala/lisa/utils/unification/UnificationUtils.scala
index f8f481f62b604b28d938addc1cf1855557bb2156..dcc762fa59274b5788a8c5639d0c83cd5672efa6 100644
--- a/lisa-utils/src/main/scala/lisa/utils/unification/UnificationUtils.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/unification/UnificationUtils.scala
@@ -203,7 +203,7 @@ object UnificationUtils {
}
}
- case (ConnectorFormula(labelR, argsR), ConnectorFormula(labelT, argsT)) if labelR == labelT =>
+ case (AppliedConnector(labelR, argsR), AppliedConnector(labelT, argsT)) if labelR == labelT =>
if (argsR.length != argsT.length)
// quick discard
None
@@ -222,7 +222,7 @@ object UnificationUtils {
else if (template == reference && reference == formulaSubstitution.getOrElse(template, reference)) Some(formulaSubstitution, termSubstitution)
else None
- case (PredicateFormula(labelR, argsR), PredicateFormula(labelT, argsT)) if labelR == labelT =>
+ case (AppliedPredicate(labelR, argsR), AppliedPredicate(labelT, argsT)) if labelR == labelT =>
if (argsR.length != argsT.length)
// quick discard
None
@@ -419,7 +419,7 @@ object UnificationUtils {
if (innerSubstitutions.exists(_.isEmpty)) None
else {
val retrieved = innerSubstitutions.map(_.get)
- val body = first.label(retrieved.map(_.body))
+ val body = first.label.applySeq(retrieved.map(_.body))
val lambda =
retrieved.foldLeft(TermRewriteLambda(body = body)) { case (currentLambda, nextLambda) =>
TermRewriteLambda(
@@ -564,7 +564,7 @@ object UnificationUtils {
innerSubst.map(s => s.copy(body = BinderFormula(labelF, freshVar, s.body)))
}
- case (ConnectorFormula(labelF, argsF), ConnectorFormula(labelS, argsS)) =>
+ case (AppliedConnector(labelF, argsF), AppliedConnector(labelS, argsS)) =>
if (argsF.length != argsS.length)
// quick discard
None
@@ -575,7 +575,7 @@ object UnificationUtils {
if (innerSubstitutions.exists(_.isEmpty)) None
else {
val retrieved = innerSubstitutions.map(_.get)
- val body = ConnectorFormula(labelF, retrieved.map(_.body))
+ val body = AppliedConnector(labelF, retrieved.map(_.body))
val lambda =
retrieved.foldLeft(FormulaRewriteLambda(body = body)) { case (currentLambda, nextLambda) =>
FormulaRewriteLambda(
@@ -588,7 +588,7 @@ object UnificationUtils {
}
}
- case (PredicateFormula(labelF, argsF), PredicateFormula(labelS, argsS)) =>
+ case (AppliedPredicate(labelF, argsF), AppliedPredicate(labelS, argsS)) =>
if (argsF.length != argsS.length)
// quick discard
None
@@ -599,7 +599,7 @@ object UnificationUtils {
if (innerSubstitutions.exists(_.isEmpty)) None
else {
val retrieved = innerSubstitutions.map(_.get)
- val body = PredicateFormula(labelF, retrieved.map(_.body))
+ val body = AppliedPredicate(labelF, retrieved.map(_.body))
val lambda =
retrieved.foldLeft(FormulaRewriteLambda(body = body)) { case (currentLambda, nextLambda) =>
FormulaRewriteLambda(
diff --git a/lisa-utils/src/test/scala/lisa/TestTheoryAxioms.scala b/lisa-utils/src/test/scala/lisa/TestTheoryAxioms.scala
index 37a37463e15c9a1546251be076c95c5d5b56d41d..aeaa403d38593fd688c26099b36864f88c66841d 100644
--- a/lisa-utils/src/test/scala/lisa/TestTheoryAxioms.scala
+++ b/lisa-utils/src/test/scala/lisa/TestTheoryAxioms.scala
@@ -5,8 +5,8 @@ import lisa.kernel.proof.RunningTheory
import lisa.utils.KernelHelpers.{_, given}
trait TestTheoryAxioms {
- final val p1 = ConstantPredicateLabel("p1", 1)
- final val p2 = ConstantPredicateLabel("p2", 1)
+ final val p1 = ConstantAtomicLabel("p1", 1)
+ final val p2 = ConstantAtomicLabel("p2", 1)
final val f1 = ConstantFunctionLabel("f1", 1)
final val fixedElement = ConstantFunctionLabel("fixedElement", 0)
final val anotherFixed = ConstantFunctionLabel("anotherElement", 0)
diff --git a/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index d4cf7f0ec3afaa6bbed39647e319b488ff2450cb..81a39258f708cc27e40604cddf9485fb9b54527c 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -54,7 +54,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
val generator = nameGenerator()
() => {
val id = generator()
- PredicateFormula(ConstantPredicateLabel(id, 0), Seq.empty)
+ AtomicFormula(ConstantAtomicLabel(id, 0), Seq.empty)
}
}
@@ -81,7 +81,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
// Reuse existing name
connectors(random.nextInt(connectors.size))
}
- PredicateFormula(ConstantPredicateLabel(name, 0), Seq.empty)
+ AtomicFormula(ConstantAtomicLabel(name, 0), Seq.empty)
} else {
// Branch
val nextP = p * c
@@ -169,7 +169,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
def repeatApply[T](n: Int)(f: T => T)(initial: T): T = if (n > 0) repeatApply(n - 1)(f)(f(initial)) else initial
def commutativeShuffle(iterations: Int)(random: Random)(f: Formula): Formula = {
def transform(f: Formula): Formula = f match {
- case PredicateFormula(label, args) => f
+ case AtomicFormula(label, args) => f
case ConnectorFormula(label, args) =>
val newArgs = label match {
case And | Or | Iff => random.shuffle(args)
@@ -182,7 +182,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
}
def associativeShuffle(iterations: Int)(random: Random)(f: Formula): Formula = {
def transform(f: Formula): Formula = f match {
- case PredicateFormula(label, args) => f
+ case AtomicFormula(label, args) => f
// Simple for now, assume binary operations
case ConnectorFormula(label1 @ (And | Or), Seq(ConnectorFormula(label2, Seq(a1, a2)), a3)) if label1 == label2 =>
if (random.nextBoolean()) {
@@ -206,7 +206,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
if (random.nextDouble() < p) neg(neg(transform(f)))
else
f match {
- case _: PredicateFormula => f
+ case _: AtomicFormula => f
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(transform))
case BinderFormula(label, bound, inner) => BinderFormula(label, bound, transform(inner))
}
@@ -214,7 +214,7 @@ class EquivalenceCheckerTests extends AnyFunSuite {
}
def addDeMorgans(p: Double)(random: Random)(f: Formula): Formula = {
def transform(f: Formula): Formula = f match {
- case _: PredicateFormula => f
+ case _: AtomicFormula => f
case ConnectorFormula(label, args) =>
val map: Map[ConnectorLabel, ConnectorLabel] = Map(And -> Or, Or -> And)
map.get(label) match {
diff --git a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
index b38d2283eae4786b00ff9820a8b057fd99fe10c8..bc769dd8c2cecb31223b805e58a833788d6a0573 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
@@ -60,20 +60,20 @@ class FolTests extends AnyFunSuite {
val r = gen.between(0, 7)
if (r <= 1) {
val name = "" + ('A' to 'E')(gen.between(0, 5))
- PredicateFormula(ConstantPredicateLabel(name, 0), Seq())
+ AtomicFormula(ConstantAtomicLabel(name, 0), Seq())
} else if (r <= 3) {
val name = "" + ('A' to 'E')(gen.between(0, 5))
- PredicateFormula(ConstantPredicateLabel(name, 1), Seq(termGenerator(maxDepth - 1, gen)))
+ AtomicFormula(ConstantAtomicLabel(name, 1), Seq(termGenerator(maxDepth - 1, gen)))
} else if (r <= 5) {
val s = gen.between(0, 3)
- if (s == 0) PredicateFormula(equality, Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ if (s == 0) AtomicFormula(equality, Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
else {
val name = "" + ('A' to 'E')(gen.between(0, 5))
- PredicateFormula(ConstantPredicateLabel(name, 2), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ AtomicFormula(ConstantAtomicLabel(name, 2), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
}
} else {
val name = "" + ('A' to 'E')(gen.between(0, 5))
- PredicateFormula(ConstantPredicateLabel(name, 3), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
+ AtomicFormula(ConstantAtomicLabel(name, 3), Seq(termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen), termGenerator(maxDepth - 1, gen)))
}
} else {
@@ -98,9 +98,9 @@ class FolTests extends AnyFunSuite {
private val x = VariableLabel("x")
private val y = VariableLabel("y")
private val z = VariableLabel("z")
- private val a = PredicateFormula(ConstantPredicateLabel("A", 0), Seq())
- private val b = PredicateFormula(ConstantPredicateLabel("B", 0), Seq())
- private val fp = ConstantPredicateLabel("F", 1)
+ private val a = AtomicFormula(ConstantAtomicLabel("A", 0), Seq())
+ private val b = AtomicFormula(ConstantAtomicLabel("B", 0), Seq())
+ private val fp = ConstantAtomicLabel("F", 1)
private val sT = VariableLabel("t")
def test_some_random_formulas(n: Int, maxDepth: Int): Unit = {
diff --git a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 13df37d7c8449f0e9e8d5c933117adce72ca76e9..05933f01b6ae3f045c9be6bfe99d808cb522d762 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -20,9 +20,9 @@ class IncorrectProofsTests extends ProofCheckerSuite {
implicit def proofStepToProof(proofStep: SCProofStep): SCProof = SCProof(proofStep)
val (fl, gl, hl) = (VariableFormulaLabel("f"), VariableFormulaLabel("g"), VariableFormulaLabel("h"))
- val f = PredicateFormula(fl, Seq.empty) // Some arbitrary formulas
- val g = PredicateFormula(gl, Seq.empty)
- val h = PredicateFormula(hl, Seq.empty)
+ val f = AtomicFormula(fl, Seq.empty) // Some arbitrary formulas
+ val g = AtomicFormula(gl, Seq.empty)
+ val h = AtomicFormula(hl, Seq.empty)
val incorrectProofs: Seq[SCProof] = List(
SCProof(
diff --git a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
index 9e06ffad72e338730202543f78a6c9c353f4057c..474f4fee9052d1b7fe9407819df244f656c6e325 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
@@ -19,9 +19,9 @@ class ProofTests extends AnyFunSuite {
private val x = VariableLabel("x")
private val y = VariableLabel("y")
private val z = VariableLabel("z")
- private val a = PredicateFormula(ConstantPredicateLabel("A", 0), Seq())
- private val b = PredicateFormula(ConstantPredicateLabel("B", 0), Seq())
- private val fp = ConstantPredicateLabel("F", 1)
+ private val a = AtomicFormula(ConstantAtomicLabel("A", 0), Seq())
+ private val b = AtomicFormula(ConstantAtomicLabel("B", 0), Seq())
+ private val fp = ConstantAtomicLabel("F", 1)
val sT = VariableLabel("t")
test("Verification of Pierce law") {
@@ -44,7 +44,7 @@ class ProofTests extends AnyFunSuite {
test("Commutativity on a random large formula") {
val k = 9
val r = new Random()
- val vars = (0 until 1 << k).map(i => PredicateFormula(ConstantPredicateLabel(s"P$i", 0), Seq()))
+ val vars = (0 until 1 << k).map(i => AtomicFormula(ConstantAtomicLabel(s"P$i", 0), Seq()))
val pairs = vars.grouped(2)
val sPairs = vars.grouped(2)
diff --git a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
index 8a2fa3e79209ca986aa50b47588e84a0c172875b..e1ee7a350a13e1acf264bee1c6fdcdb85c561c59 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
@@ -97,7 +97,7 @@ class SubstitutionTest extends AnyFunSuite {
}
test("Substitution of Predicates in Formulas") {
- case class $(f: Formula, m: (SchematicVarOrPredLabel, LambdaTermFormula)*)
+ case class $(f: Formula, m: (SchematicAtomicLabel, LambdaTermFormula)*)
extension (c: $) {
inline infix def _VS_(t2: Formula): Assertion = {
assert(
@@ -141,7 +141,7 @@ class SubstitutionTest extends AnyFunSuite {
}
test("Simultaneous Substitutions in Formulas") {
- case class $(f: Formula, m: ((SchematicConnectorLabel, LambdaFormulaFormula) | (SchematicVarOrPredLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm))*)
+ case class $(f: Formula, m: ((SchematicConnectorLabel, LambdaFormulaFormula) | (SchematicAtomicLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm))*)
extension (c: $) {
inline infix def _VS_(t2: Formula): Assertion = {
val mCon: Map[SchematicConnectorLabel, LambdaFormulaFormula] = c.m
@@ -150,9 +150,9 @@ class SubstitutionTest extends AnyFunSuite {
})
.toMap
.asInstanceOf
- val mPred: Map[SchematicVarOrPredLabel, LambdaTermFormula] = c.m
+ val mPred: Map[SchematicAtomicLabel, LambdaTermFormula] = c.m
.collect({
- case e if e._1.isInstanceOf[SchematicVarOrPredLabel] => e
+ case e if e._1.isInstanceOf[SchematicAtomicLabel] => e
})
.toMap
.asInstanceOf
diff --git a/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala b/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala
index e7c6520dc5fc0559c1daddd35f025c6e87b3c566..8d46bbcf40ebfdb571658c16eb62d75f8d7dc9dd 100644
--- a/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/BasicTacticTest.scala
@@ -1477,23 +1477,23 @@ class BasicTacticTest extends ProofTacticTestLib {
val Z = LambdaTermFormula(Seq(x, y), g(x, y))
val correct = List(
- ("'P('x); 'f('x) |- 'R('y)", "'P('x); ('x = 'x) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](f -> Y)),
- ("'P('x); 'Q('x) /\\ 'f('x) |- 'R('y)", "'P('x); 'Q('x) /\\ 'x = 'x |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](f -> Y)),
- ("'P('x); 'h('x, 'y) |- 'R('y)", "'P('x); 'g('x, 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z)),
- ("'h('y, 'y); 'h('x, 'y) |- 'R('y)", "'g('y, 'y); 'g('x, 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z)),
- ("'P('x); 'g('x, 'y) |- 'R('y)", "'P('x); 'g('x, 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z)),
- ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y); 'x = 'x", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z, f -> Y))
+ ("'P('x); 'f('x) |- 'R('y)", "'P('x); ('x = 'x) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](f -> Y)),
+ ("'P('x); 'Q('x) /\\ 'f('x) |- 'R('y)", "'P('x); 'Q('x) /\\ 'x = 'x |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](f -> Y)),
+ ("'P('x); 'h('x, 'y) |- 'R('y)", "'P('x); 'g('x, 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z)),
+ ("'h('y, 'y); 'h('x, 'y) |- 'R('y)", "'g('y, 'y); 'g('x, 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z)),
+ ("'P('x); 'g('x, 'y) |- 'R('y)", "'P('x); 'g('x, 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z)),
+ ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y); 'x = 'x", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z, f -> Y))
)
val incorrect = List(
- ("'P('x); 'f('x) = 'y |- 'R('y)", "'P('x); !('x = 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](f -> Y)),
- ("'P('x); 'f('x) |- 'R('y)", "'P('x); 'Q('y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](f -> Y)),
- ("'P('x); 'h('x, 'y) |- 'R('y)", "'P('x); 'h('x, 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z)),
- ("'h('y, 'y); 'h('x, 'y) |- 'R('y)", "'g('y, 'y); 'g('y, 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z)),
- ("'P('x); 'g('x, 'y) |- 'R('y)", "'P('x); 'h('x, 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z)),
- ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y); 'x = 't", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z, f -> Y)),
- ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y); 'x = 'x", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z)),
- ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y)", Map[SchematicVarOrPredLabel, LambdaTermFormula](h -> Z, f -> Y))
+ ("'P('x); 'f('x) = 'y |- 'R('y)", "'P('x); !('x = 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](f -> Y)),
+ ("'P('x); 'f('x) |- 'R('y)", "'P('x); 'Q('y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](f -> Y)),
+ ("'P('x); 'h('x, 'y) |- 'R('y)", "'P('x); 'h('x, 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z)),
+ ("'h('y, 'y); 'h('x, 'y) |- 'R('y)", "'g('y, 'y); 'g('y, 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z)),
+ ("'P('x); 'g('x, 'y) |- 'R('y)", "'P('x); 'h('x, 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z)),
+ ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y); 'x = 't", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z, f -> Y)),
+ ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y); 'x = 'x", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z)),
+ ("'P('x); 'g('x, 'y) |- 'R('y); 'f('x)", "'P('x); 'g('x, 'y) |- 'R('y)", Map[SchematicAtomicLabel, LambdaTermFormula](h -> Z, f -> Y))
)
testTacticCases(correct, incorrect) { (stmt1, stmt2, termMap) =>
diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
index 01457e990d796e1363fbd7016bd0a45dc7923796..a0cad24c1c3d1bf0ca1f489d481fa6198a49dca3 100644
--- a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
@@ -44,8 +44,8 @@ class ParserTest extends AnyFunSuite with TestUtils {
}
test("0-ary predicate") {
- assert(FOLParser.parseFormula("a") == PredicateFormula(ConstantPredicateLabel("a", 0), Seq()))
- assert(FOLParser.parseFormula("a()") == PredicateFormula(ConstantPredicateLabel("a", 0), Seq()))
+ assert(FOLParser.parseFormula("a") == AtomicFormula(ConstantAtomicLabel("a", 0), Seq()))
+ assert(FOLParser.parseFormula("a()") == AtomicFormula(ConstantAtomicLabel("a", 0), Seq()))
}
test("boolean constants") {
@@ -61,14 +61,14 @@ class ParserTest extends AnyFunSuite with TestUtils {
}
test("predicate application") {
- assert(FOLParser.parseFormula("p(x, y, z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(cx, cy, cz)))
- assert(FOLParser.parseFormula("p('x, 'y, 'z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z)))
+ assert(FOLParser.parseFormula("p(x, y, z)") == AtomicFormula(ConstantAtomicLabel("p", 3), Seq(cx, cy, cz)))
+ assert(FOLParser.parseFormula("p('x, 'y, 'z)") == AtomicFormula(ConstantAtomicLabel("p", 3), Seq(x, y, z)))
}
test("equality") {
- assert(FOLParser.parseFormula("(x = x)") == PredicateFormula(equality, Seq(cx, cx)))
- assert(FOLParser.parseFormula("x = x") == PredicateFormula(equality, Seq(cx, cx)))
- assert(FOLParser.parseFormula("a ∧ ('x = 'x)") == ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x)))))
+ assert(FOLParser.parseFormula("(x = x)") == AtomicFormula(equality, Seq(cx, cx)))
+ assert(FOLParser.parseFormula("x = x") == AtomicFormula(equality, Seq(cx, cx)))
+ assert(FOLParser.parseFormula("a ∧ ('x = 'x)") == ConnectorFormula(And, Seq(a, AtomicFormula(equality, Seq(x, x)))))
}
test("unicode connectors") {
@@ -131,13 +131,13 @@ class ParserTest extends AnyFunSuite with TestUtils {
}
test("quantifiers") {
- assert(FOLParser.parseFormula("∀ 'x. (p)") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
- assert(FOLParser.parseFormula("∃ 'x. (p)") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
- assert(FOLParser.parseFormula("∃! 'x. (p)") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+ assert(FOLParser.parseFormula("∀ 'x. (p)") == BinderFormula(Forall, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq())))
+ assert(FOLParser.parseFormula("∃ 'x. (p)") == BinderFormula(Exists, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq())))
+ assert(FOLParser.parseFormula("∃! 'x. (p)") == BinderFormula(ExistsOne, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq())))
- assert(FOLParser.parseFormula("∀ 'x. p") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
- assert(FOLParser.parseFormula("∃ 'x. p") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
- assert(FOLParser.parseFormula("∃! 'x. p") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+ assert(FOLParser.parseFormula("∀ 'x. p") == BinderFormula(Forall, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq())))
+ assert(FOLParser.parseFormula("∃ 'x. p") == BinderFormula(Exists, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq())))
+ assert(FOLParser.parseFormula("∃! 'x. p") == BinderFormula(ExistsOne, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq())))
}
test("nested quantifiers") {
@@ -150,7 +150,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
FOLParser.parseFormula("∀ 'x. p('x) ∧ q('x)") == BinderFormula(
Forall,
x,
- ConnectorFormula(And, Seq(PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x)), PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))))
+ ConnectorFormula(And, Seq(AtomicFormula(ConstantAtomicLabel("p", 1), Seq(x)), AtomicFormula(ConstantAtomicLabel("q", 1), Seq(x))))
)
)
@@ -160,8 +160,8 @@ class ParserTest extends AnyFunSuite with TestUtils {
FOLParser.parseFormula("(∀ 'x. p('x)) ∧ q('x)") == ConnectorFormula(
And,
Seq(
- BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x))),
- PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))
+ BinderFormula(Forall, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 1), Seq(x))),
+ AtomicFormula(ConstantAtomicLabel("q", 1), Seq(x))
)
)
)
@@ -181,7 +181,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
}
test("complex formulas") {
- assert(FOLParser.parseFormula("∀x. 'x = 'x") == BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x))))
+ assert(FOLParser.parseFormula("∀x. 'x = 'x") == BinderFormula(Forall, x, AtomicFormula(equality, Seq(x, x))))
}
test("parser limitations") {
@@ -191,23 +191,23 @@ class ParserTest extends AnyFunSuite with TestUtils {
}
test("sequent") {
- val forallEq = BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))
+ val forallEq = BinderFormula(Forall, x, AtomicFormula(equality, Seq(x, x)))
assert(FOLParser.parseSequent("∀x. 'x = 'x") == Sequent(Set(), Set(forallEq)))
assert(FOLParser.parseSequent("⊢ ∀x. 'x = 'x") == Sequent(Set(), Set(forallEq)))
assert(FOLParser.parseSequent("∀x. 'x = 'x ⊢ ∀x. 'x = 'x") == Sequent(Set(forallEq), Set(forallEq)))
- val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
+ val existsXEq = BinderFormula(Exists, x, AtomicFormula(equality, Seq(x, x)))
assert(FOLParser.parseSequent("∀x. 'x = 'x ⊢ ∃x. 'x = 'x") == Sequent(Set(forallEq), Set(existsXEq)))
- val existsYEq = BinderFormula(Exists, y, PredicateFormula(equality, Seq(y, y)))
+ val existsYEq = BinderFormula(Exists, y, AtomicFormula(equality, Seq(y, y)))
assert(FOLParser.parseSequent("∀x. 'x = 'x ⊢ ∃x. 'x = 'x; ∃y. 'y = 'y") == Sequent(Set(forallEq), Set(existsYEq, existsXEq)))
assert(
FOLParser.parseSequent("p ; ∀x. 'x = 'x ⊢ ∃x. 'x = 'x; ∃y. 'y = 'y") ==
- Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))
+ Sequent(Set(forallEq, AtomicFormula(ConstantAtomicLabel("p", 0), Seq())), Set(existsYEq, existsXEq))
)
}
test("sequents from Mapping and SetTheory") {
val va = VariableLabel("a")
- val leftAndRight = BinderFormula(ExistsOne, x, PredicateFormula(sPhi2, Seq(x, va)))
+ val leftAndRight = BinderFormula(ExistsOne, x, AtomicFormula(sPhi2, Seq(x, va)))
assert(FOLParser.parseSequent("∃!x. 'phi('x, 'a) ⊢ ∃!x. 'phi('x, 'a)") == Sequent(Set(leftAndRight), Set(leftAndRight)))
assert(
@@ -233,11 +233,11 @@ class ParserTest extends AnyFunSuite with TestUtils {
test("equivalent names") {
val parser = Parser(SynonymInfoBuilder().addSynonyms(in.id, "∊").build, "∊" :: Nil, Nil)
- assert(parser.parseFormula("x∊y") == PredicateFormula(in, Seq(cx, cy)))
- assert(parser.parseFormula("x ∊ y") == PredicateFormula(in, Seq(cx, cy)))
- assert(parser.parseFormula("'x ∊ 'y") == PredicateFormula(in, Seq(x, y)))
- assert(parser.parseFormula("('x ∊ 'y) /\\ a") == ConnectorFormula(And, Seq(PredicateFormula(in, Seq(x, y)), a)))
- assert(parser.parseFormula("a \\/ ('x ∊ 'y)") == ConnectorFormula(Or, Seq(a, PredicateFormula(in, Seq(x, y)))))
+ assert(parser.parseFormula("x∊y") == AtomicFormula(in, Seq(cx, cy)))
+ assert(parser.parseFormula("x ∊ y") == AtomicFormula(in, Seq(cx, cy)))
+ assert(parser.parseFormula("'x ∊ 'y") == AtomicFormula(in, Seq(x, y)))
+ assert(parser.parseFormula("('x ∊ 'y) /\\ a") == ConnectorFormula(And, Seq(AtomicFormula(in, Seq(x, y)), a)))
+ assert(parser.parseFormula("a \\/ ('x ∊ 'y)") == ConnectorFormula(Or, Seq(a, AtomicFormula(in, Seq(x, y)))))
}
test("infix functions") {
@@ -248,19 +248,19 @@ class ParserTest extends AnyFunSuite with TestUtils {
test("mix of infix functions and infix predicates") {
val parser = Parser(SynonymInfoBuilder().addSynonyms(in.id, "∊").addSynonyms(plus.id, "+").build, "∊" :: Nil, ("+", Associativity.Left) :: Nil)
- assert(parser.parseFormula("(x + y) ∊ z") == PredicateFormula(in, Seq(Term(plus, Seq(cx, cy)), cz)))
+ assert(parser.parseFormula("(x + y) ∊ z") == AtomicFormula(in, Seq(Term(plus, Seq(cx, cy)), cz)))
assert(
parser.parseFormula("x ∊ y /\\ x ∊ z /\\ (x + y) ∊ z") == ConnectorFormula(
And,
- Seq(ConnectorFormula(And, Seq(PredicateFormula(in, Seq(cx, cy)), PredicateFormula(in, Seq(cx, cz)))), PredicateFormula(in, Seq(Term(plus, Seq(cx, cy)), cz)))
+ Seq(ConnectorFormula(And, Seq(AtomicFormula(in, Seq(cx, cy)), AtomicFormula(in, Seq(cx, cz)))), AtomicFormula(in, Seq(Term(plus, Seq(cx, cy)), cz)))
)
)
}
test("infix function and predicate priority") {
val parser = Parser(SynonymInfoBuilder().addSynonyms(plus.id, "+").build, equality.id :: Nil, ("+", Associativity.Left) :: Nil)
- assert(parser.parseFormula("(x + y) = (y + x)") == PredicateFormula(equality, Seq(plus(cx, cy), plus(cy, cx))))
- assert(parser.parseFormula("x + y = y + x") == PredicateFormula(equality, Seq(plus(cx, cy), plus(cy, cx))))
+ assert(parser.parseFormula("(x + y) = (y + x)") == AtomicFormula(equality, Seq(plus(cx, cy), plus(cy, cx))))
+ assert(parser.parseFormula("x + y = y + x") == AtomicFormula(equality, Seq(plus(cx, cy), plus(cy, cx))))
}
test("parser exception: unexpected input") {
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 5a776019118ac05d6b4b3f12be8c8e79dc31f5f2..8f2132419c0c4670d5215b786f4ae3b84fc7ed41 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -31,17 +31,17 @@ class PrinterTest extends AnyFunSuite with TestUtils {
FOLParser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(Neg, Seq(b)))), ConnectorFormula(Neg, Seq(c))))) == "¬a ∧ ¬b ∧ ¬c"
)
- assert(FOLParser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ 'x = 'x")
+ assert(FOLParser.printFormula(ConnectorFormula(And, Seq(a, AtomicFormula(equality, Seq(x, x))))) == "a ∧ 'x = 'x")
- assert(FOLParser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀'x. 'x = 'x")
- assert(FOLParser.printFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ (∀'x. 'x = 'x)")
+ assert(FOLParser.printFormula(BinderFormula(Forall, x, AtomicFormula(equality, Seq(x, x)))) == "∀'x. 'x = 'x")
+ assert(FOLParser.printFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, AtomicFormula(equality, Seq(x, x)))))) == "a ∧ (∀'x. 'x = 'x)")
assert(FOLParser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀'x. b) ∧ a")
assert(FOLParser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀'x. b) ∧ a")
assert(FOLParser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀'x. b) ∨ a")
assert(FOLParser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀'x. ∃'y. ∃!'z. a")
- assert(FOLParser.printFormula(PredicateFormula(ConstantPredicateLabel("f", 3), Seq(x, y, z))) == "f('x, 'y, 'z)")
+ assert(FOLParser.printFormula(AtomicFormula(ConstantAtomicLabel("f", 3), Seq(x, y, z))) == "f('x, 'y, 'z)")
}
test("constant") {
@@ -77,17 +77,17 @@ class PrinterTest extends AnyFunSuite with TestUtils {
}
test("0-ary predicate") {
- assert(FOLParser.printFormula(PredicateFormula(ConstantPredicateLabel("a", 0), Seq())) == "a")
+ assert(FOLParser.printFormula(AtomicFormula(ConstantAtomicLabel("a", 0), Seq())) == "a")
}
test("predicate application") {
- assert(FOLParser.printFormula(PredicateFormula(ConstantPredicateLabel("p", 3), Seq(cx, cy, cz))) == "p(x, y, z)")
- assert(FOLParser.printFormula(PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z))) == "p('x, 'y, 'z)")
+ assert(FOLParser.printFormula(AtomicFormula(ConstantAtomicLabel("p", 3), Seq(cx, cy, cz))) == "p(x, y, z)")
+ assert(FOLParser.printFormula(AtomicFormula(ConstantAtomicLabel("p", 3), Seq(x, y, z))) == "p('x, 'y, 'z)")
}
test("equality") {
- assert(FOLParser.printFormula(PredicateFormula(equality, Seq(cx, cx))) == "x = x")
- assert(FOLParser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ 'x = 'x")
+ assert(FOLParser.printFormula(AtomicFormula(equality, Seq(cx, cx))) == "x = x")
+ assert(FOLParser.printFormula(ConnectorFormula(And, Seq(a, AtomicFormula(equality, Seq(x, x))))) == "a ∧ 'x = 'x")
}
test("toplevel connectors") {
@@ -166,9 +166,9 @@ class PrinterTest extends AnyFunSuite with TestUtils {
}
test("quantifiers") {
- assert(FOLParser.printFormula(BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∀'x. p")
- assert(FOLParser.printFormula(BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃'x. p")
- assert(FOLParser.printFormula(BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃!'x. p")
+ assert(FOLParser.printFormula(BinderFormula(Forall, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq()))) == "∀'x. p")
+ assert(FOLParser.printFormula(BinderFormula(Exists, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq()))) == "∃'x. p")
+ assert(FOLParser.printFormula(BinderFormula(ExistsOne, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 0), Seq()))) == "∃!'x. p")
}
test("nested quantifiers") {
@@ -182,7 +182,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
BinderFormula(
Forall,
x,
- ConnectorFormula(And, Seq(PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x)), PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))))
+ ConnectorFormula(And, Seq(AtomicFormula(ConstantAtomicLabel("p", 1), Seq(x)), AtomicFormula(ConstantAtomicLabel("q", 1), Seq(x))))
)
) == "∀'x. p('x) ∧ q('x)"
)
@@ -194,8 +194,8 @@ class PrinterTest extends AnyFunSuite with TestUtils {
ConnectorFormula(
And,
Seq(
- BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x))),
- PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))
+ BinderFormula(Forall, VariableLabel("x"), AtomicFormula(ConstantAtomicLabel("p", 1), Seq(x))),
+ AtomicFormula(ConstantAtomicLabel("q", 1), Seq(x))
)
)
) == "(∀'x. p('x)) ∧ q('x)"
@@ -215,35 +215,35 @@ class PrinterTest extends AnyFunSuite with TestUtils {
}
test("complex formulas") {
- assert(FOLParser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀'x. 'x = 'x")
+ assert(FOLParser.printFormula(BinderFormula(Forall, x, AtomicFormula(equality, Seq(x, x)))) == "∀'x. 'x = 'x")
}
test("sequent") {
- val forallEq = BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))
+ val forallEq = BinderFormula(Forall, x, AtomicFormula(equality, Seq(x, x)))
assert(FOLParser.printSequent(Sequent(Set(), Set(forallEq))) == "⊢ ∀'x. 'x = 'x")
assert(FOLParser.printSequent(Sequent(Set(forallEq), Set(forallEq))) == "∀'x. 'x = 'x ⊢ ∀'x. 'x = 'x")
- val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
+ val existsXEq = BinderFormula(Exists, x, AtomicFormula(equality, Seq(x, x)))
assert(FOLParser.printSequent(Sequent(Set(forallEq), Set(existsXEq))) == "∀'x. 'x = 'x ⊢ ∃'x. 'x = 'x")
}
// warning: this test might be flaky because formula order is not fixed in sequents but fixed in the string representation
test("sequent with multiple formulas") {
- val forallEq = BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))
- val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
- val existsYEq = BinderFormula(Exists, y, PredicateFormula(equality, Seq(y, y)))
+ val forallEq = BinderFormula(Forall, x, AtomicFormula(equality, Seq(x, x)))
+ val existsXEq = BinderFormula(Exists, x, AtomicFormula(equality, Seq(x, x)))
+ val existsYEq = BinderFormula(Exists, y, AtomicFormula(equality, Seq(y, y)))
assert(
FOLParser.printSequent(Sequent(Set(forallEq), Set(existsYEq, existsXEq))) == "∀'x. 'x = 'x ⊢ ∃'y. 'y = 'y; " +
"∃'x. 'x = 'x"
)
assert(
- FOLParser.printSequent(Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))) == "∀'x. 'x = 'x; p ⊢ ∃'y. 'y = 'y; ∃'x. 'x = 'x"
+ FOLParser.printSequent(Sequent(Set(forallEq, AtomicFormula(ConstantAtomicLabel("p", 0), Seq())), Set(existsYEq, existsXEq))) == "∀'x. 'x = 'x; p ⊢ ∃'y. 'y = 'y; ∃'x. 'x = 'x"
)
}
// warning: this test might be flaky because formula order is not fixed in sequents but fixed in the string representation
test("sequents from Mapping and SetTheory") {
val va = VariableLabel("a")
- val leftAndRight = BinderFormula(ExistsOne, x, PredicateFormula(sPhi2, Seq(x, va)))
+ val leftAndRight = BinderFormula(ExistsOne, x, AtomicFormula(sPhi2, Seq(x, va)))
assert(FOLParser.printSequent(Sequent(Set(leftAndRight), Set(leftAndRight))) == "∃!'x. 'phi('x, 'a) ⊢ ∃!'x. 'phi('x, 'a)")
assert(
@@ -274,18 +274,18 @@ class PrinterTest extends AnyFunSuite with TestUtils {
}
test("infix predicates") {
- val in = ConstantPredicateLabel("∊", 2)
- val prefixIn = ConstantPredicateLabel("elem", 2)
+ val in = ConstantAtomicLabel("∊", 2)
+ val prefixIn = ConstantAtomicLabel("elem", 2)
val parser = Parser(SynonymInfoBuilder().addSynonyms(prefixIn.id, in.id).build, in.id :: Nil, Nil)
- assert(parser.printFormula(PredicateFormula(in, Seq(cx, cy))) == "x ∊ y")
- assert(parser.printFormula(PredicateFormula(in, Seq(x, y))) == "'x ∊ 'y")
- assert(parser.printFormula(ConnectorFormula(And, Seq(PredicateFormula(in, Seq(x, y)), a))) == "'x ∊ 'y ∧ a")
- assert(parser.printFormula(ConnectorFormula(Or, Seq(a, PredicateFormula(in, Seq(x, y))))) == "a ∨ 'x ∊ 'y")
-
- assert(parser.printFormula(PredicateFormula(prefixIn, Seq(cx, cy))) == "x ∊ y")
- assert(parser.printFormula(PredicateFormula(prefixIn, Seq(x, y))) == "'x ∊ 'y")
- assert(parser.printFormula(ConnectorFormula(And, Seq(PredicateFormula(prefixIn, Seq(x, y)), a))) == "'x ∊ 'y ∧ a")
- assert(parser.printFormula(ConnectorFormula(Or, Seq(a, PredicateFormula(prefixIn, Seq(x, y))))) == "a ∨ 'x ∊ 'y")
+ assert(parser.printFormula(AtomicFormula(in, Seq(cx, cy))) == "x ∊ y")
+ assert(parser.printFormula(AtomicFormula(in, Seq(x, y))) == "'x ∊ 'y")
+ assert(parser.printFormula(ConnectorFormula(And, Seq(AtomicFormula(in, Seq(x, y)), a))) == "'x ∊ 'y ∧ a")
+ assert(parser.printFormula(ConnectorFormula(Or, Seq(a, AtomicFormula(in, Seq(x, y))))) == "a ∨ 'x ∊ 'y")
+
+ assert(parser.printFormula(AtomicFormula(prefixIn, Seq(cx, cy))) == "x ∊ y")
+ assert(parser.printFormula(AtomicFormula(prefixIn, Seq(x, y))) == "'x ∊ 'y")
+ assert(parser.printFormula(ConnectorFormula(And, Seq(AtomicFormula(prefixIn, Seq(x, y)), a))) == "'x ∊ 'y ∧ a")
+ assert(parser.printFormula(ConnectorFormula(Or, Seq(a, AtomicFormula(prefixIn, Seq(x, y))))) == "a ∨ 'x ∊ 'y")
}
test("infix functions") {
@@ -296,12 +296,12 @@ class PrinterTest extends AnyFunSuite with TestUtils {
/*
test("mix of infix functions and infix predicates") {
val parser = Parser(SynonymInfoBuilder().addSynonyms(in.id, "∊").addSynonyms(plus.id, "+").build, "∊" :: Nil, ("+", Associativity.Left) :: Nil)
- assert(parser.printFormula(PredicateFormula(in, Seq(Term(plus, Seq(cx, cy)), cz))) == "x + y ∊ z")
+ assert(parser.printFormula(AtomicFormula(in, Seq(Term(plus, Seq(cx, cy)), cz))) == "x + y ∊ z")
assert(
parser.printFormula(
ConnectorFormula(
And,
- Seq(ConnectorFormula(And, Seq(PredicateFormula(in, Seq(cx, cy)), PredicateFormula(in, Seq(cx, cz)))), PredicateFormula(in, Seq(Term(plus, Seq(cx, cy)), cz)))
+ Seq(ConnectorFormula(And, Seq(AtomicFormula(in, Seq(cx, cy)), AtomicFormula(in, Seq(cx, cz)))), AtomicFormula(in, Seq(Term(plus, Seq(cx, cy)), cz)))
)
) == "x ∊ y ∧ x ∊ z ∧ x + y ∊ z"
)
diff --git a/lisa-utils/src/test/scala/lisa/utils/TestUtils.scala b/lisa-utils/src/test/scala/lisa/utils/TestUtils.scala
index daaa06674beacf01e20b13375d3e042cb566a6e8..243bd3c1aa5f274f7708e7c47ff916cdde9a117c 100644
--- a/lisa-utils/src/test/scala/lisa/utils/TestUtils.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/TestUtils.scala
@@ -8,8 +8,8 @@ import lisa.utils.KernelHelpers.{_, given}
import lisa.utils.{_, given}
trait TestUtils {
- val (a, b, c) = (ConstantPredicateLabel("a", 0), ConstantPredicateLabel("b", 0), ConstantPredicateLabel("c", 0))
- val p = ConstantPredicateLabel("p", 1)
+ val (a, b, c) = (ConstantAtomicLabel("a", 0), ConstantAtomicLabel("b", 0), ConstantAtomicLabel("c", 0))
+ val p = ConstantAtomicLabel("p", 1)
val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
val (x1, y1, z1) = (VariableLabel("x1"), VariableLabel("y1"), VariableLabel("z1"))
val (xPrime, yPrime, zPrime) = (VariableLabel("x'"), VariableLabel("y'"), VariableLabel("z'"))
@@ -18,9 +18,9 @@ trait TestUtils {
val (sf1, sf2, sf3) = (SchematicFunctionLabel("f", 1), SchematicFunctionLabel("f", 2), SchematicFunctionLabel("f", 3))
val (sPhi1, sPhi2) = (SchematicPredicateLabel("phi", 1), SchematicPredicateLabel("phi", 2))
val (sc1, sc2) = (SchematicConnectorLabel("c", 1), SchematicConnectorLabel("c", 2))
- val (in, plus) = (ConstantPredicateLabel("elem", 2), ConstantFunctionLabel("+", 2))
+ val (in, plus) = (ConstantAtomicLabel("elem", 2), ConstantFunctionLabel("+", 2))
- given Conversion[PredicateLabel, PredicateFormula] = PredicateFormula(_, Seq.empty)
+ given Conversion[AtomicLabel, AtomicFormula] = AtomicFormula(_, Seq.empty)
given Conversion[ConstantFunctionLabel, Term] = Term(_, Seq())