From 620f705695f96483a1781206637a056b4f3db761 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Tue, 19 Jul 2022 13:39:49 +0200
Subject: [PATCH] Changed printer test. Now variables are always shown with a
leading ? (except when following a binder)
---
.../main/scala/lisa/kernel/fol/CommonDefinitions.scala | 7 -------
.../scala/lisa/kernel/fol/FormulaLabelDefinitions.scala | 4 ++--
.../main/scala/lisa/kernel/fol/TermLabelDefinitions.scala | 2 +-
lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala | 1 +
lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala | 8 ++++----
5 files changed, 8 insertions(+), 14 deletions(-)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
index 901989ed..1faa2a20 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -6,13 +6,6 @@ package lisa.kernel.fol
private[fol] trait CommonDefinitions {
val MaxArity: Int = 1000000
- /**
- * An object with arity information for tree-like structures.
- */
- protected trait Arity {
- val arity: Int
- }
-
/**
* An labelled node for tree-like structures.
*/
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 27f1bcbb..d3252743 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -34,7 +34,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 abstract class PredicateLabel extends FormulaLabel with Arity {
+ sealed abstract class PredicateLabel extends FormulaLabel {
require(arity < MaxArity && arity >= 0)
}
@@ -68,7 +68,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
/**
* The label for a connector, namely a function taking a fixed number of formulas and returning another formula.
*/
- sealed abstract class ConnectorLabel(val id: String, val arity: Int) extends FormulaLabel with Arity {
+ sealed abstract class ConnectorLabel(val id: String, val arity: Int) extends FormulaLabel {
require(arity < MaxArity && arity >= -1)
}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
index 163e8d36..3c2ca18d 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -35,7 +35,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
* Standard function symbols denote a particular function. Schematic function symbols
* can be instantiated with any term. This is particularly useful to express axiom schemas.
*/
- sealed abstract class FunctionLabel extends TermLabel with Arity {
+ sealed abstract class FunctionLabel extends TermLabel {
require(arity >= 0 && arity < MaxArity)
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 1452de69..a5bb1b41 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -89,6 +89,7 @@ trait KernelHelpers {
given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply
given Conversion[VariableTerm, VariableLabel] = _.label
given Conversion[PredicateFormula, PredicateLabel] = _.label
+ given Conversion[PredicateLabel, Formula] = _.apply()
given Conversion[FunctionTerm, FunctionLabel] = _.label
given Conversion[SchematicFunctionLabel, Term] = _.apply()
given Conversion[VariableFormulaLabel, PredicateFormula] = PredicateFormula.apply(_, Nil)
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index d19514fb..33f62829 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -28,17 +28,17 @@ class PrinterTest extends AnyFunSuite {
assert(prettyFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(ConnectorFormula(And, Seq(a, b))))))) == "¬¬(a ∧ b)")
assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(b)), ConnectorFormula(Neg, Seq(c))))))) == "¬a ∧ ¬b ∧ ¬c")
- assert(prettyFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ (x = x)")
+ assert(prettyFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ (?x = ?x)")
- assert(prettyFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀x. x = x")
- assert(prettyFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ ∀x. x = x")
+ assert(prettyFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀x. ?x = ?x")
+ assert(prettyFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ ∀x. ?x = ?x")
assert(prettyFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀x. b) ∧ a")
assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "(a ∧ ∀x. b) ∧ a")
assert(prettyFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀x. b) ∨ a")
assert(prettyFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀x. ∃y. ∃!z. a")
- assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(x, y, z)")
+ assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(?x, ?y, ?z)")
}
}
--
GitLab