Rename TheorySymbol to ConstantLabel. Add SchematicLabel marker for symmetry

src/main/scala/lisa/kernel/fol/CommonDefinitions.scala

@@ -21,9 +21,15 @@ private[fol] trait CommonDefinitions {
   }
 
   /**
-   * Marks classes that can represent symbols in a theory
+   * Constant label can represent a symbol of a theory
    */
-  trait TheorySymbol
+  trait ConstantLabel extends Label
+
+  /**
+   * Schematic label in a formula can be substituted by any constant label of the respective
+   * kind (predicate or function)
+   */
+  trait SchematicLabel extends Label
 
   def freshId(taken: Set[String], base: String): String = {
     var i = 0;

src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala

@@ -41,7 +41,7 @@ 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 with TheorySymbol
+  final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with ConstantLabel
 
   /**
    * The equality symbol (=) for first order logic.

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 with TheorySymbol
+  final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with ConstantLabel
 
   /**
    * A schematic function symbol that can be substituted.

src/main/scala/lisa/kernel/proof/RunningTheory.scala

@@ -62,12 +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 definitions: mMap[TheorySymbol, Option[Definition]] = mMap(equality -> None)
+  private[proof] val definitions: mMap[ConstantLabel, Option[Definition]] = mMap(equality -> None)
 
   /**
    * Check if a label is a symbol of the theory
    */
-  def isSymbol(label: TheorySymbol): Boolean = definitions.contains(label)
+  def isSymbol(label: ConstantLabel): 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.
@@ -255,13 +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(s: TheorySymbol): Unit = definitions.update(s, None)
+  def addSymbol(s: ConstantLabel): 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[(TheorySymbol, Option[Definition])] = definitions.toList
+  def language: List[(ConstantLabel, Option[Definition])] = definitions.toList
 
   /**
    * Public accessor to the current set of axioms of the theory