Changed printer test.

Now variables are always shown with a leading ? (except when following a binder)

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.
    */

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)
   }
 

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)
   }
 

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)

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)")
   }
 
 }