diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 3bac64702d2853550b42941c9d957aa76bec5164..044c181af93298f6b417766f488985bdd860a746 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -37,7 +37,7 @@ object Printer {
ConstantFunctionLabel("power_set", 1),
ConstantFunctionLabel("union", 1)
)
- private val nonAtomicPredicates = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
+ private val nonAtomicPredicates: Set[PredicateLabel] = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
private def prettyFormulaInternal(formula: Formula, isRightMost: Boolean, compact: Boolean): String = formula match {
case PredicateFormula(label, args) =>
diff --git a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
index 3e34019fbcf179fd0991f7b3c34086a685705ee5..65906e987404b68b249b1056434a26e2897e501e 100644
--- a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -20,6 +20,11 @@ private[fol] trait CommonDefinitions {
val id: String
}
+ /**
+ * Marks classes that can represent symbols in a theory
+ */
+ trait TheorySymbol
+
def freshId(taken: Set[String], base: String): String = {
var i = 0;
while (taken contains base + "_" + i) i += 1
diff --git a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index 81de8601f0bad8f71ddc954341e616a1ee9199d1..3439bc0ae1887e6908dc63bce6aa091718078dcb 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -41,12 +41,12 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
/**
* A standard predicate symbol. Typical example are equality (=) and membership (∈)
*/
- final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel
+ final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with TheorySymbol
/**
* The equality symbol (=) for first order logic.
*/
- val equality: PredicateLabel = ConstantPredicateLabel("=", 2)
+ val equality: ConstantPredicateLabel = ConstantPredicateLabel("=", 2)
/**
* A predicate symbol that can be instantiated with any formula.
diff --git a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
index a7ca828850f01241667a46a0c587b3f644d9c722..24c501dce518654244c15ceb3562e85dd3696c53 100644
--- a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -54,7 +54,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
* @param id The name of the function symbol.
* @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
*/
- final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel
+ final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with TheorySymbol
/**
* A schematic function symbol that can be substituted.
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index c68e8993b38a39e19e1cf9363ef50494509efabe..15175569f99403ed26236b9d7f4cfb1cbab7e3ed 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -62,18 +62,12 @@ class RunningTheory {
private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
private[proof] val theorems: mMap[String, Theorem] = mMap.empty
- private[proof] val funDefinitions: mMap[FunctionLabel, Option[FunctionDefinition]] = mMap.empty
- private[proof] val predDefinitions: mMap[PredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None)
+ private[proof] val definitions: mMap[TheorySymbol, Option[Definition]] = mMap(equality -> None)
/**
* Check if a label is a symbol of the theory
*/
- def isAcceptedFunctionLabel(label: FunctionLabel): Boolean = funDefinitions.contains(label)
-
- /**
- * Check if a label is a symbol of the theory
- */
- def isAcceptedPredicateLabel(label: PredicateLabel): Boolean = predDefinitions.contains(label)
+ def isSymbol(label: TheorySymbol): Boolean = definitions.contains(label)
/**
* From a given proof, if it is true in the Running theory, add that theorem to the theory and returns it.
@@ -108,10 +102,10 @@ class RunningTheory {
*/
def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
if (belongsToTheory(phi))
- if (!isAcceptedPredicateLabel(label))
+ if (!isSymbol(label))
if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
val newDef = PredicateDefinition(label, args, phi)
- predDefinitions.update(label, Some(newDef))
+ definitions.update(label, Some(newDef))
RunningTheoryJudgement.ValidJustification(newDef)
else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
else InvalidJustification("The specified symbol is already part of the theory and can't be redefined.", None)
@@ -141,7 +135,7 @@ class RunningTheory {
phi: Formula
): RunningTheoryJudgement[this.FunctionDefinition] = {
if (belongsToTheory(phi))
- if (!isAcceptedFunctionLabel(label))
+ if (!isSymbol(label))
if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
val r = SCProofChecker.checkSCProof(proof)
@@ -153,7 +147,7 @@ class RunningTheory {
val subst2 = bindAll(Forall, args.reverse, BinderFormula(ExistsOne, out, phi))
if (isSame(r.head, subst) || isSame(r.head, subst2)) {
val newDef = FunctionDefinition(label, args, out, phi)
- funDefinitions.update(label, Some(newDef))
+ definitions.update(label, Some(newDef))
RunningTheoryJudgement.ValidJustification(newDef)
} else InvalidJustification("The proof is correct but its conclusion does not correspond to a definition for for the formula phi.", None)
case _ => InvalidJustification("The conclusion of the proof must have an empty left hand side, and a single formula on the right hand side.", None)
@@ -201,7 +195,7 @@ class RunningTheory {
def belongsToTheory(phi: Formula): Boolean = phi match {
case PredicateFormula(label, args) =>
label match {
- case _: ConstantPredicateLabel => isAcceptedPredicateLabel(label) && args.forall(belongsToTheory)
+ case l: ConstantPredicateLabel => isSymbol(l) && args.forall(belongsToTheory)
case _: SchematicPredicateLabel => args.forall(belongsToTheory)
}
case ConnectorFormula(label, args) => args.forall(belongsToTheory)
@@ -222,7 +216,7 @@ class RunningTheory {
case VariableTerm(label) => true
case FunctionTerm(label, args) =>
label match {
- case _: ConstantFunctionLabel => isAcceptedFunctionLabel(label) && args.forall(belongsToTheory(_))
+ case l: ConstantFunctionLabel => isSymbol(l) && args.forall(belongsToTheory(_))
case _: SchematicFunctionLabel => args.forall(belongsToTheory(_))
}
@@ -261,14 +255,13 @@ class RunningTheory {
* For example, This function can add the empty set symbol to a theory, and then an axiom asserting
* the it is empty can be introduced as well.
*/
- def addSymbol(l: FunctionLabel): Unit = funDefinitions.update(l, None)
- def addSymbol(l: PredicateLabel): Unit = predDefinitions.update(l, None)
+ def addSymbol(s: TheorySymbol): Unit = definitions.update(s, None)
/**
* Public accessor to the set of symbol currently in the theory's language.
* @return the set of symbol currently in the theory's language.
*/
- def language: (List[(FunctionLabel, Option[FunctionDefinition])], List[(PredicateLabel, Option[PredicateDefinition])]) = (funDefinitions.toList, predDefinitions.toList)
+ def language: List[(TheorySymbol, Option[Definition])] = definitions.toList
/**
* Public accessor to the current set of axioms of the theory
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 337e67feb6c7d460d98f77577944bc79d891612d..a2f3b2b7df8bdaf254183f4adfd25361a490781d 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -16,20 +16,20 @@ private[settheory] trait SetTheoryDefinitions {
final val sPhi = SchematicPredicateLabel("P", 2)
final val sPsi = SchematicPredicateLabel("P", 3)
// Predicates
- final val in: PredicateLabel = ConstantPredicateLabel("set_membership", 2)
- final val subset: PredicateLabel = ConstantPredicateLabel("subset_of", 2)
- final val sim: PredicateLabel = ConstantPredicateLabel("same_cardinality", 2) // Equicardinality
+ final val in = ConstantPredicateLabel("set_membership", 2)
+ final val subset = ConstantPredicateLabel("subset_of", 2)
+ final val sim = ConstantPredicateLabel("same_cardinality", 2) // Equicardinality
final val predicates = Set(in, subset, sim)
// val application
// val pick
// Functions
- final val emptySet: FunctionLabel = ConstantFunctionLabel("empty_set", 0)
- final val pair: FunctionLabel = ConstantFunctionLabel("unordered_pair", 2)
- final val singleton: FunctionLabel = ConstantFunctionLabel("singleton", 1)
- final val powerSet: FunctionLabel = ConstantFunctionLabel("power_set", 1)
- final val union: FunctionLabel = ConstantFunctionLabel("union", 1)
- final val universe: FunctionLabel = ConstantFunctionLabel("universe", 1)
+ final val emptySet = ConstantFunctionLabel("empty_set", 0)
+ final val pair = ConstantFunctionLabel("unordered_pair", 2)
+ final val singleton = ConstantFunctionLabel("singleton", 1)
+ final val powerSet = ConstantFunctionLabel("power_set", 1)
+ final val union = ConstantFunctionLabel("union", 1)
+ final val universe = ConstantFunctionLabel("universe", 1)
final val functions = Set(emptySet, pair, singleton, powerSet, union, universe)
val runningSetTheory: RunningTheory = new RunningTheory()