Add NodeType bits and add Destructor.

src/main/antlr4/com/viklauverk/eventbtools/core/EvBFormula.g4

@@ -272,6 +272,9 @@ expression
    | { symbol_table.isNumberSymbol(_input.LT(1).getText()) }?     sym=SYMBOL meta? # NumberSymbol
    | { symbol_table.isNonFreeVariableSymbol(_input.LT(1).getText()) }?   variable=SYMBOL meta? # NonFreeExpressionVariable
    | { symbol_table.isVariableSymbol(_input.LT(1).getText()) }?   variable=SYMBOL  PRIM? meta? # ExpressionVariable
+   | { symbol_table.isConstructorSymbol(_input.LT(1).getText()) }? constructor=SYMBOL meta? # Constructor
+   | { symbol_table.isDestructorSymbol(_input.LT(1).getText()) }? destructor=SYMBOL meta? # Destructor
+   | { symbol_table.isOperatorSymbol(_input.LT(1).getText()) }? operator=SYMBOL meta? # Operator
    | { symbol_table.isConstantSymbol(_input.LT(1).getText()) }?   constant=SYMBOL meta?        # ExpressionConstant
    // Should we be able to talk about all functions such that their applications give such and such result? For the moment, we can't.
    | { symbol_table.isVariableSymbol(_input.LT(1).getText()) }?   variable=SYMBOL PRIM? INV? meta? '(' inner=expression ')' # VariableFunctionApplication

src/main/java/com/viklauverk/eventbtools/core/AllRenders.java

@@ -43,28 +43,29 @@ public class AllRenders
     private SystemSearch system_search_;
 
     @SuppressWarnings("this-escape")
-    public AllRenders(RenderTheory rt,
-                      RenderPolymorphicDataType rpdt,
-                      RenderContext rc,
+    public AllRenders(RenderContext rc,
                       RenderMachine rm,
                       RenderEvent re,
                       RenderFormula rf,
+                      RenderTheory rt,
+                      RenderPolymorphicDataType rpdt,
                       Canvas c)
     {
-        rt_ = rt;
-        rpdt_ = rpdt;
         rc_ = rc;
         rm_ = rm;
         re_ = re;
         rf_ = rf;
+        rt_ = rt;
+        rpdt_ = rpdt;
         system_search_ = new SystemSearch();
 
         root_canvas_ = c;
         current_ = c;
-        rt_.setRenders(this);
         rc_.setRenders(this);
         rm_.setRenders(this);
         re_.setRenders(this);
+        rt_.setRenders(this);
+        rpdt_.setRenders(this);
     }
 
     public Canvas currentCanvas()

src/main/java/com/viklauverk/eventbtools/core/Canvas.java

@@ -1138,6 +1138,66 @@ public void constant(String s)
         assert (false) : "Unknown encoding "+render_target_;
     }
 
+    public void constructor(String s)
+    {
+        switch (render_target_)
+        {
+        case PLAIN:
+            append(s);
+            return;
+        case TERMINAL:
+            append(colorize(BGreen, s));
+            return;
+        case TEX:
+            append("\\CNSTR{"+Util.texSafe(s)+"}");
+            return;
+        case HTML:
+            append(" span(class=CNSTR)="+Util.quoteXMQ(s)+" ");
+            return;
+        }
+        assert (false) : "Unknown encoding "+render_target_;
+    }
+
+    public void destructor(String s)
+    {
+        switch (render_target_)
+        {
+        case PLAIN:
+            append(s);
+            return;
+        case TERMINAL:
+            append(colorize(BGreen, s));
+            return;
+        case TEX:
+            append("\\DSTR{"+Util.texSafe(s)+"}");
+            return;
+        case HTML:
+            append(" span(class=DSTR)="+Util.quoteXMQ(s)+" ");
+            return;
+        }
+        assert (false) : "Unknown encoding "+render_target_;
+    }
+
+    public void operator(String s)
+    {
+        switch (render_target_)
+        {
+        case PLAIN:
+            append(s);
+            return;
+        case TERMINAL:
+            append(colorize(BGreen, s));
+            return;
+        case TEX:
+            append("\\OPRT{"+Util.texSafe(s)+"}");
+            return;
+        case HTML:
+            append(" span(class=OPRT)="+Util.quoteXMQ(s)+" ");
+            return;
+        }
+        assert (false) : "Unknown encoding "+render_target_;
+    }
+
     public void primitiveSet(String s)
     {
         switch (render_target_)

src/main/java/com/viklauverk/eventbtools/core/Constructor.java

@@ -17,13 +17,25 @@
 
 package com.viklauverk.eventbtools.core;
 
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+import java.util.HashMap;
+import java.util.Set;
+import java.util.HashSet;
+import java.util.stream.Collectors;
+
 public class Constructor extends Typed
 {
     private String name_;
     private String comment_;
     private Formula definition_;
     private PolymorphicDataType polymorphic_datatype_;
 
+    private Map<String,Destructor> destructors_ = new HashMap<>();
+    private List<Destructor> destructor_ordering_ = new ArrayList<>();
+    private List<String> destructor_names_ = new ArrayList<>();
+
     public Constructor(String n, PolymorphicDataType pdt)
     {
         name_ = n;
@@ -70,4 +82,27 @@ public boolean hasDefinition()
     {
         return definition_ != null;
     }
+
+    public void addDestructor(Destructor o)
+    {
+        destructors_.put(o.name(), o);
+        destructor_ordering_.add(o);
+        destructor_names_ = destructors_.keySet().stream().sorted().collect(Collectors.toList());
+    }
+
+    public Destructor getDestructor(String name)
+    {
+        return destructors_.get(name);
+    }
+
+    public List<Destructor> destructorOrdering()
+    {
+        return destructor_ordering_;
+    }
+
+    public List<String> destructorNames()
+    {
+        return destructor_names_;
+    }
+
 }

src/main/java/com/viklauverk/eventbtools/core/Destructor.java

@@ -0,0 +1,73 @@
+/*
+ Copyright (C) 2021-2024 Viklauverk AB
+
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU Affero General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ GNU Affero General Public License for more details.
+
+ You should have received a copy of the GNU Affero General Public License
+ along with this program.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+package com.viklauverk.eventbtools.core;
+
+public class Destructor extends Typed
+{
+    private String name_;
+    private String comment_;
+    private Formula definition_;
+    private Constructor constructor_;
+
+    public Destructor(String n, Constructor cnstr)
+    {
+        name_ = n;
+        constructor_ = cnstr;
+    }
+
+    @Override
+    public String toString()
+    {
+        return name_;
+    }
+
+    public String name()
+    {
+        return name_;
+    }
+
+    public String comment()
+    {
+        return comment_;
+    }
+
+    public void addComment(String c)
+    {
+        comment_ = c;
+    }
+
+    public void setDefinition(Formula f)
+    {
+        definition_ = f;
+    }
+
+    public Formula definition()
+    {
+        return definition_;
+    }
+
+    public boolean hasDefinition()
+    {
+        return definition_ != null;
+    }
+
+    public Constructor constructor()
+    {
+        return constructor_;
+    }
+}

src/main/java/com/viklauverk/eventbtools/core/FormulaBuilder.java

@@ -174,6 +174,24 @@ public Formula visitExpressionConstant(EvBFormulaParser.ExpressionConstantContex
         return FormulaFactory.newConstantSymbol(ctx.constant.getText(), visitOptionalMeta(ctx.meta()));
     }
 
+    @Override
+    public Formula visitConstructor(EvBFormulaParser.ConstructorContext ctx)
+    {
+        return FormulaFactory.newConstructorSymbol(ctx.constructor.getText(), visitOptionalMeta(ctx.meta()));
+    }
+
+    @Override
+    public Formula visitDestructor(EvBFormulaParser.DestructorContext ctx)
+    {
+        return FormulaFactory.newDestructorSymbol(ctx.destructor.getText(), visitOptionalMeta(ctx.meta()));
+    }
+
+    @Override
+    public Formula visitOperator(EvBFormulaParser.OperatorContext ctx)
+    {
+        return FormulaFactory.newOperatorSymbol(ctx.operator.getText(), visitOptionalMeta(ctx.meta()));
+    }
+
     @Override
     public Formula visitVariableFunctionApplication(EvBFormulaParser.VariableFunctionApplicationContext ctx)
     {

src/main/java/com/viklauverk/eventbtools/core/FormulaFactory.java

@@ -135,6 +135,24 @@ Formula newSetSymbol (String s, Formula meta)
         return new Formula(Node.SET_SYMBOL, Symbols.intern(s), meta);
     }
 
+    public static
+    Formula newConstructorSymbol (String s, Formula meta)
+    {
+        return new Formula(Node.CONSTRUCTOR_SYMBOL, Symbols.intern(s), meta);
+    }
+
+    public static
+    Formula newDestructorSymbol (String s, Formula meta)
+    {
+        return new Formula(Node.DESTRUCTOR_SYMBOL, Symbols.intern(s), meta);
+    }
+
+    public static
+    Formula newOperatorSymbol (String s, Formula meta)
+    {
+        return new Formula(Node.OPERATOR_SYMBOL, Symbols.intern(s), meta);
+    }
+
     public static
     Formula newPolymorphicDataTypeSymbol(String s, Formula parameters, Formula meta)
     {

src/main/java/com/viklauverk/eventbtools/core/FormulaVisitor.java

@@ -38,6 +38,9 @@ public interface FormulaVisitor
     Formula visit_VARIABLE_NONFREE_SYMBOL(Formula i);
     Formula visit_CONSTANT_SYMBOL(Formula i);
     Formula visit_POLYMORPHIC_DATA_TYPE_SYMBOL(Formula i);
+    Formula visit_CONSTRUCTOR_SYMBOL(Formula i);
+    Formula visit_DESTRUCTOR_SYMBOL(Formula i);
+    Formula visit_OPERATOR_SYMBOL(Formula i);
     Formula visit_APPLICATION(Formula i);
     Formula visit_PARENTHESISED_PREDICATE(Formula i);
     Formula visit_PARENTHESISED_EXPRESSION(Formula i);