From 98c5dd6238cfaca5c2e75472b704451a33f79590 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fredrik=20=C3=96hrstr=C3=B6m?= <oehrstroem@gmail.com>
Date: Tue, 9 Jul 2024 19:14:07 +0200
Subject: [PATCH] Add NodeType bits and add Destructor.

---
 .../viklauverk/eventbtools/core/EvBFormula.g4 |   3 +
 .../eventbtools/core/AllRenders.java          |  13 +-
 .../viklauverk/eventbtools/core/Canvas.java   |  60 ++++
 .../eventbtools/core/Constructor.java         |  35 +++
 .../eventbtools/core/Destructor.java          |  73 +++++
 .../eventbtools/core/FormulaBuilder.java      |  18 ++
 .../eventbtools/core/FormulaFactory.java      |  18 ++
 .../eventbtools/core/FormulaVisitor.java      |   3 +
 .../com/viklauverk/eventbtools/core/Node.java | 264 +++++++++---------
 .../viklauverk/eventbtools/core/NodeType.java |  40 +++
 .../eventbtools/core/PolymorphicDataType.java |   4 +
 .../core/RenderFormulaUnicode.java            |  15 +
 .../core/RenderPolymorphicDataTypeSearch.java |  12 +
 .../eventbtools/core/RenderTheory.java        |   5 +
 .../eventbtools/core/RenderTheorySearch.java  |  15 +
 .../eventbtools/core/SymbolTable.java         | 143 +++++++++-
 .../com/viklauverk/eventbtools/core/Sys.java  |  32 +--
 .../viklauverk/eventbtools/core/Theory.java   |  11 +-
 .../eventbtools/core/WalkFormula.java         |   6 +
 .../eventbtools/core/cmd/CmdSysLsParts.java   |   4 +-
 20 files changed, 605 insertions(+), 169 deletions(-)
 create mode 100644 src/main/java/com/viklauverk/eventbtools/core/Destructor.java
 create mode 100644 src/main/java/com/viklauverk/eventbtools/core/NodeType.java

diff --git a/src/main/antlr4/com/viklauverk/eventbtools/core/EvBFormula.g4 b/src/main/antlr4/com/viklauverk/eventbtools/core/EvBFormula.g4
index d926094..63c07fa 100644
--- a/src/main/antlr4/com/viklauverk/eventbtools/core/EvBFormula.g4
+++ b/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
diff --git a/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java b/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java
index d004e37..41b03ee 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java
+++ b/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()
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Canvas.java b/src/main/java/com/viklauverk/eventbtools/core/Canvas.java
index 56b2f42..4b89470 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/Canvas.java
+++ b/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_)
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Constructor.java b/src/main/java/com/viklauverk/eventbtools/core/Constructor.java
index 1336a6f..93e0364 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/Constructor.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/Constructor.java
@@ -17,6 +17,14 @@
 
 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_;
@@ -24,6 +32,10 @@ public class Constructor extends Typed
     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_;
+    }
+
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Destructor.java b/src/main/java/com/viklauverk/eventbtools/core/Destructor.java
new file mode 100644
index 0000000..ab56eeb
--- /dev/null
+++ b/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_;
+    }
+}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/FormulaBuilder.java b/src/main/java/com/viklauverk/eventbtools/core/FormulaBuilder.java
index 5a3a855..0e9a3bb 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/FormulaBuilder.java
+++ b/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)
     {
diff --git a/src/main/java/com/viklauverk/eventbtools/core/FormulaFactory.java b/src/main/java/com/viklauverk/eventbtools/core/FormulaFactory.java
index 91b9425..5713390 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/FormulaFactory.java
+++ b/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)
     {
diff --git a/src/main/java/com/viklauverk/eventbtools/core/FormulaVisitor.java b/src/main/java/com/viklauverk/eventbtools/core/FormulaVisitor.java
index 00667a4..862c66a 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/FormulaVisitor.java
+++ b/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);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Node.java b/src/main/java/com/viklauverk/eventbtools/core/Node.java
index ade9c79..55a3f7c 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/Node.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/Node.java
@@ -17,209 +17,209 @@
 
 package com.viklauverk.eventbtools.core;
 
+import static com.viklauverk.eventbtools.core.NodeType.*;
+
 public enum Node
 {
     // 1) is_predicate 2) is_expression 3) is_set 4) is_data_type 5) is_variable 6) is_constant 7) is_symbol 8) is_relation 9) is_function
 
-    NONE(false, false, false, false, false, false, false, false, false), // No element.
-    TRUE(true, false, false, false, false, false, false, false, false),  // The predicate true.
-    FALSE(true, false, false, false, false, false, false, false, false), // The predicate false.
+    NONE(0), // No element.
+    TRUE(PRE.bit),  // The predicate true.
+    FALSE(PRE.bit), // The predicate false.
 
     // First basic symbols are expressions
-    NUMBER(false, true, false, false, false, false, false, false, false),          // 1, 2, 3 etc
-    PREDICATE_SYMBOL(true, false, false, false, false, false, true, false, false), // A symbol representing a predicate, eg P,Q or R
-    EXPRESSION_SYMBOL(false, true, false, false, false, false, true, false, false),// A symbol representing an expression, eg E,F or G
-    SET_SYMBOL(false, false, true, false, false, false, true, false, false),       // A symbol representing any set, eg S,T or U
-    VARIABLE_SYMBOL(false, true, false, false, true, false, true, false, false),   // A symbol representing a variable, eg x,y,z,w,x1,floor,speed
-    VARIABLE_PRIM_SYMBOL(false, true, false, false, true, false, true, false, false),   // A prim variable symbol, eg x',y',floor'
-    VARIABLE_NONFREE_SYMBOL(false, true, false, false, true, false, true, false, false), // A symbol capture by ! or #, ie declared inside the predicate.
-    CONSTANT_SYMBOL(false, false, false, false, false, true, true, false, false),  // A constant symbol: set element, constant function, eg c,d,f
-    ANY_SYMBOL(false, false, false, false, false, false, true, false, false),      // Symbol that matches any other element, eg A,B,C.
-    NUMBER_SYMBOL(false, false, false, false, false, false, true, false, false),   // Symbol that matches a number.
-    POLYMORPHIC_DATA_TYPE_SYMBOL(false, false, true, true, false, false, true, false, false), // A symbol representing a data type, eg H List, Seq
-
-    LIST_OF_VARIABLES(false, false, false, false, false, false, false, false, false), // x,y,z := 1,2,3
-    LIST_OF_NONFREE_VARIABLES(false, false, false, false, false, false, false, false, false), // In a forall ∀x,y,z· or exists ∃a,b· the variables are such a list.
-    LIST_OF_EXPRESSIONS(false, false, false, false, false, false, false, false, false), // In a partition {a},{b},{c} is a list of sets.
-    LIST_OF_TYPES(false, false, false, false, false, false, false, false, false), // In a DataType Seq(NAT) Map(NAT,INT)
-
-    PARENTHESISED_PREDICATE(true, false, false, false, false, false, false, false, false), // A predicate wrapped in parenthesis.
-    PARENTHESISED_EXPRESSION(false, true, false, false, false, false, false, false, false), // An expression wrapped in parenthesis.
+    NUMBER(EXP.bit), // 1, 2, 3 etc
+    PREDICATE_SYMBOL(PRE.bit | SYM.bit), // A symbol representing a predicate, eg P,Q or R
+    EXPRESSION_SYMBOL(EXP.bit | SYM.bit), // A symbol representing an expression, eg E,F or G
+    SET_SYMBOL(SET.bit | SYM.bit), // A symbol representing any set, eg S,T or U
+    VARIABLE_SYMBOL(EXP.bit | VAR.bit | SYM.bit), // A symbol representing a variable, eg x,y,z,w,x1,floor,speed
+    VARIABLE_PRIM_SYMBOL(EXP.bit | VAR.bit | SYM.bit), // A prim variable symbol, eg x',y',floor'
+    VARIABLE_NONFREE_SYMBOL(EXP.bit | VAR.bit | SYM.bit), // A symbol capture by ! or #, ie declared inside the predicate.
+    CONSTANT_SYMBOL(CON.bit | SYM.bit), // A constant symbol: set element, constant function, eg c,d,f
+    ANY_SYMBOL(SYM.bit), // Symbol that matches any other element, eg A,B,C.
+    NUMBER_SYMBOL(SYM.bit), // Symbol that matches a number.
+    POLYMORPHIC_DATA_TYPE_SYMBOL(SET.bit | PDT.bit | SYM.bit), // A symbol representing a data type, eg H List, Seq
+    CONSTRUCTOR_SYMBOL(CNS.bit | SYM.bit), // A constructor symbol: nil cons
+    DESTRUCTOR_SYMBOL(DES.bit | SYM.bit), // A destructor symbol: head tail
+    OPERATOR_SYMBOL(OPE.bit | SYM.bit), // An operator symbol: append seqSize
+
+    LIST_OF_VARIABLES(0), // x,y,z := 1,2,3
+    LIST_OF_NONFREE_VARIABLES(0), // In a forall ∀x,y,z· or exists ∃a,b· the variables are such a list.
+    LIST_OF_EXPRESSIONS(0), // In a partition {a},{b},{c} is a list of sets.
+    LIST_OF_TYPES(0), // In a DataType Seq(NAT) Map(NAT,INT)
+
+    PARENTHESISED_PREDICATE(PRE.bit), // A predicate wrapped in parenthesis.
+    PARENTHESISED_EXPRESSION(EXP.bit), // An expression wrapped in parenthesis.
 
     // Propositional logic
-    CONJUNCTION(true, false, false, false, false, false, false, false, false),
-    IMPLICATION(true, false, false, false, false, false, false, false, false),
-    NEGATION(true, false, false, false, false, false, false, false, false),
-    DISJUNCTION(true, false, false, false, false, false, false, false, false),
-    EQUIVALENCE(true, false, false, false, false, false, false, false, false),
+    CONJUNCTION(PRE.bit),
+    IMPLICATION(PRE.bit),
+    NEGATION(PRE.bit),
+    DISJUNCTION(PRE.bit),
+    EQUIVALENCE(PRE.bit),
 
     // Addition of substitution to preds, vars and expressions
-    BECOME_EQ(false, false, false, false, false, false, false, false, false),    // x:=E
-    BECOME_EQ_FUNC_APP(false, false, false, false, false, false, false, false, false), // x(t):=E
-    BECOME_IN(false, false, false, false, false, false, false, false, false),    // x::S
-    BECOME_SUCH(false, false, false, false, false, false, false, false, false),  // x:|=P
-    APPLICATION(false, false, false, false, false, false, false, false, false),  // [x:=E]P
+    BECOME_EQ(0),    // x:=E
+    BECOME_EQ_FUNC_APP(0), // x(t):=E
+    BECOME_IN(0),    // x::S
+    BECOME_SUCH(0),  // x:|=P
+    APPLICATION(0),  // [x:=E]P
 
     // Adding quantifiers for predicate logic
-    UNIVERSALQ(true, false, false, false, false, false, false, false, false),
-    EXISTENTIALQ(true, false, false, false, false, false, false, false, false),
+    UNIVERSALQ(PRE.bit),
+    EXISTENTIALQ(PRE.bit),
 
     // Expressions can be equals in predicates
-    EQUALS(true, false, false, false, false, false, false, false, false),
-    NOT_EQUALS(true, false, false, false, false, false, false, false, false),
-    LESS_THAN(true, false, false, false, false, false, false, false, false),
-    GREATER_THAN(true, false, false, false, false, false, false, false, false),
-    LESS_THAN_OR_EQUAL(true, false, false, false, false, false, false, false, false),
-    GREATER_THAN_OR_EQUAL(true, false, false, false, false, false, false, false, false),
+    EQUALS(PRE.bit),
+    NOT_EQUALS(PRE.bit),
+    LESS_THAN(PRE.bit),
+    GREATER_THAN(PRE.bit),
+    LESS_THAN_OR_EQUAL(PRE.bit),
+    GREATER_THAN_OR_EQUAL(PRE.bit),
 
     // A choice from a set makes an expression
-    CHOICE(false, true, false, false, false, false, false, false, false),
+    CHOICE(EXP.bit),
 
     // Set membership is a predicate
-    MEMBERSHIP(true, false, false, false, false, false, false, false, false),
-    NOT_MEMBERSHIP(true, false, false, false, false, false, false, false, false),
-    SUBSET(true, false, false, false, false, false, false, false, false),
-    NOT_SUBSET(true, false, false, false, false, false, false, false, false),
-    STRICT_SUBSET(true, false, false, false, false, false, false, false, false),
-    NOT_STRICT_SUBSET(true, false, false, false, false, false, false, false, false),
-    FINITE(true, false, false, false, false, false, false, false, false),
-    OF_TYPE(true, false, false, false, false, false, false, false, false),
+    MEMBERSHIP(PRE.bit),
+    NOT_MEMBERSHIP(PRE.bit),
+    SUBSET(PRE.bit),
+    NOT_SUBSET(PRE.bit),
+    STRICT_SUBSET(PRE.bit),
+    NOT_STRICT_SUBSET(PRE.bit),
+    FINITE(PRE.bit),
+    OF_TYPE(PRE.bit),
 
     // Partition is a special case that generates a lot of predicates.
-    PARTITION(false, false, false, false, false, false, false, false, false),
+    PARTITION(0),
 
     // Cardinality is a natural number aka an expression
-    CARDINALITY(false, true, false, false, false, false, false, false, false),
+    CARDINALITY(EXP.bit),
 
     // These create new sets, and thus expressions.
-    CARTESIAN_PRODUCT(false, true, true, false, false, false, false, false, false),
-    POWER_SET(false, true, true, false, false, false, false, false, false),
-    POWER1_SET(false, true, true, false, false, false, false, false, false),
-    G_UNION(false, true, true, false, false, false, false, false, false),
-    G_INTER(false, true, true, false, false, false, false, false, false),
-    Q_UNION(false, true, true, false, false, false, false, false, false),
-    Q_INTER(false, true, true, false, false, false, false, false, false),
-    DOMAIN(false, true, true, false, false, false, false, false, false),
-    RANGE(false, true, true, false, false, false, false, false, false),
-    SET_UNION(false, true, true, false, false, false, false, false, false),
-    SET_INTERSECTION(false, true, true, false, false, false, false, false, false),
-    SET_MINUS(false, true, true, false, false, false, false, false, false),
-    SET_COMPREHENSION(false, true, true, false, false, false, false, false, false),
-    SET_COMPREHENSION_SPECIAL(false, true, true, false, false, false, false, false, false),
-
-    LAMBDA_ABSTRACTION(false, true, true, false, false, false, false, false, false),
+    CARTESIAN_PRODUCT(EXP.bit | SET.bit),
+    POWER_SET(EXP.bit | SET.bit),
+    POWER1_SET(EXP.bit | SET.bit),
+    G_UNION(EXP.bit | SET.bit),
+    G_INTER(EXP.bit | SET.bit),
+    Q_UNION(EXP.bit | SET.bit),
+    Q_INTER(EXP.bit | SET.bit),
+    DOMAIN(EXP.bit | SET.bit),
+    RANGE(EXP.bit | SET.bit),
+    SET_UNION(EXP.bit | SET.bit),
+    SET_INTERSECTION(EXP.bit | SET.bit),
+    SET_MINUS(EXP.bit | SET.bit),
+    SET_COMPREHENSION(EXP.bit | SET.bit),
+    SET_COMPREHENSION_SPECIAL(EXP.bit | SET.bit),
+
+    LAMBDA_ABSTRACTION(EXP.bit | SET.bit),
 
     // S <-> T   Any ordered pair is allowed.
-    RELATION(false, true, true, false, false, false, false, true, false),
+    RELATION(EXP.bit | SET.bit | REL.bit),
 
     // S <<-> T  All elements in S are part of at least one pair.
-    TOTAL_RELATION(false, true, true, false, false, false, false, true, false),
+    TOTAL_RELATION(EXP.bit | SET.bit | REL.bit),
 
     // S <->> T  All elements in T are part of at least one pair.
-    SURJECTIVE_RELATION(false, true, true, false, false, false, false, true, false),
+    SURJECTIVE_RELATION(EXP.bit | SET.bit | REL.bit),
 
     // S <<->> T All elements in S and T are part of at least one pair.
-    SURJECTIVE_TOTAL_RELATION(false, true, true, false, false, false, false, true, false),
+    SURJECTIVE_TOTAL_RELATION(EXP.bit | SET.bit | REL.bit),
 
     // S +-> T   An element in S can only be part of a single pair.
-    PARTIAL_FUNCTION(false, true, true, false, false, false, false, true, true),
+    PARTIAL_FUNCTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S --> T   Every element in S is in a single pair.
-    TOTAL_FUNCTION(false, true, true, false, false, false, false, true, true),
+    TOTAL_FUNCTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S >+> T   A partial function where each element in T can only be part of a single pair. One-to-One relations.
-    PARTIAL_INJECTION(false, true, true, false, false, false, false, true, true),
+    PARTIAL_INJECTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S >-> T   A partial function where all elements in S are part of a single pair.
-    TOTAL_INJECTION(false, true, true, false, false, false, false, true, true),
+    TOTAL_INJECTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S +->> T  A partial function where all elements in T are part of a single pair. Onto relations
-    PARTIAL_SURJECTION(false, true, true, false, false, false, false, true, true),
+    PARTIAL_SURJECTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S -->> T  A partial function where all elements in T are part of a single pair.
-    TOTAL_SURJECTION(false, true, true, false, false, false, false, true, true),
+    TOTAL_SURJECTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S >->> T  All elements in S and T are in uniqe pairs. Every element has its own inverse.
-    TOTAL_BIJECTION(false, true, true, false, false, false, false, true, true),
+    TOTAL_BIJECTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S ; T  Forward composition
-    FORWARD_COMPOSITION(false, true, true, false, false, false, false, true, true),
+    FORWARD_COMPOSITION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S circ T  Backward composition
-    BACKWARD_COMPOSITION(false, true, true, false, false, false, false, true, true),
+    BACKWARD_COMPOSITION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S <| r  Domain restriction
-    DOMAIN_RESTRICTION(false, true, true, false, false, false, false, true, true),
+    DOMAIN_RESTRICTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // S <<| r  Domain subtraction
-    DOMAIN_SUBTRACTION(false, true, true, false, false, false, false, true, true),
+    DOMAIN_SUBTRACTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // r |> S  Range restriction
-    RANGE_RESTRICTION(false, true, true, false, false, false, false, true, true),
+    RANGE_RESTRICTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
     // r |>> S Range subtraction
-    RANGE_SUBTRACTION(false, true, true, false, false, false, false, true, true),
+    RANGE_SUBTRACTION(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
-    INVERT(false, true, true, false, false, false, false, true, true),
-    RELATION_IMAGE(false, true, true, false, false, false, false, true, true),
-    OVERRIDE(false, true, true, false, false, false, false, true, true),
-    DIRECT_PRODUCT(false, true, true, false, false, false, false, true, true),
-    PARALLEL_PRODUCT(false, true, true, false, false, false, false, true, true),
+    INVERT(EXP.bit | SET.bit | REL.bit | FUN.bit),
+    RELATION_IMAGE(EXP.bit | SET.bit | REL.bit | FUN.bit),
+    OVERRIDE(EXP.bit | SET.bit | REL.bit | FUN.bit),
+    DIRECT_PRODUCT(EXP.bit | SET.bit | REL.bit | FUN.bit),
+    PARALLEL_PRODUCT(EXP.bit | SET.bit | REL.bit | FUN.bit),
 
-    UP_TO(false, true, true, false, false, false, false, false, false),
+    UP_TO(EXP.bit | SET.bit),
 
-    FUNC_APP(false, true, false, false, false, false, false, false, false),
-    FUNC_INV_APP(false, true, false, false, false, false, false, false, false),
+    FUNC_APP(EXP.bit),
+    FUNC_INV_APP(EXP.bit),
 
     // These are pre-defined sets
-    EMPTY_SET(false, true, true, false, false, false, false, false, false),
-    ID_SET(false, true, true, false, false, false, false, false, false),
-    NAT_SET(false, true, true, false, false, false, false, false, false),
-    NAT1_SET(false, true, true, false, false, false, false, false, false),
-    INT_SET(false, true, true, false, false, false, false, false, false),
-    BOOL_SET(false, true, true, false, false, false, false, false, false),
-    ENUMERATED_SET(false, true, true, false, false, false, false, false, false), // { alfa, beta }
+    EMPTY_SET(EXP.bit | SET.bit),
+    ID_SET(EXP.bit | SET.bit),
+    NAT_SET(EXP.bit | SET.bit),
+    NAT1_SET(EXP.bit | SET.bit),
+    INT_SET(EXP.bit | SET.bit),
+    BOOL_SET(EXP.bit | SET.bit),
+    ENUMERATED_SET(EXP.bit | SET.bit), // { alfa, beta }
 
     // These are operations on numbers.
-    UNARY_MINUS(false, true, false, false, false, false, false, false, false),
-    ADDITION(false, true, false, false, false, false, false, false, false),
-    SUBTRACTION(false, true, false, false, false, false, false, false, false),
-    MULTIPLICATION(false, true, false, false, false, false, false, false, false),
-    DIVISION(false, true, false, false, false, false, false, false, false),
-    MODULO(false, true, false, false, false, false, false, false, false),
-    EXPONENTIATION(false, true, false, false, false, false, false, false, false),
-    MINIMUM(false, true, false, false, false, false, false, false, false),
-    MAXIMUM(false, true, false, false, false, false, false, false, false),
+    UNARY_MINUS(EXP.bit),
+    ADDITION(EXP.bit),
+    SUBTRACTION(EXP.bit),
+    MULTIPLICATION(EXP.bit),
+    DIVISION(EXP.bit),
+    MODULO(EXP.bit),
+    EXPONENTIATION(EXP.bit),
+    MINIMUM(EXP.bit),
+    MAXIMUM(EXP.bit),
 
     // Translate a predicate into a BOOL expression.
-    TEST_BOOL(false, true, false, false, false, false, false, false, false),
+    TEST_BOOL(EXP.bit),
 
-    MAPSTO(false, true, false, false, false, false, false, false, false),
-    PRJ1(false, true, false, false, false, false, false, false, false),
-    PRJ2(false, true, false, false, false, false, false, false, false);
+    MAPSTO(EXP.bit),
+    PRJ1(EXP.bit),
+    PRJ2(EXP.bit);
 
-    private final boolean is_predicate_, is_expression_, is_set_, is_polymorphic_data_type_, is_variable_, is_constant_, is_symbol_, is_relation_, is_function_;
+    private final int bits_;
 
-    Node(boolean ip, boolean ie, boolean is, boolean idt, boolean iv, boolean ic, boolean iss, boolean ir, boolean isf)
+    Node(int bits)
     {
-        is_predicate_ = ip;
-        is_expression_ = ie;
-        is_set_ = is;
-        is_polymorphic_data_type_ = idt;
-        is_variable_ = iv;
-        is_constant_ = ic;
-        is_symbol_ = iss;
-        is_relation_ = ir;
-        is_function_ = isf;
+        bits_ = bits;
     }
 
-    boolean isPredicate() { return is_predicate_; }
-    boolean isExpression() { return is_expression_; }
-    boolean isSet() { return is_set_; }
-    boolean isPolymorphicDataType() { return is_polymorphic_data_type_; }
-    boolean isVariable() { return is_variable_; }
-    boolean isConstant() { return is_constant_; }
-    boolean isSymbol() { return is_symbol_; }
-    boolean isRelation() { return is_relation_; }
-    boolean isFunction() { return is_function_; }
+    boolean isPredicate() { return (bits_ & NodeType.PRE.bit) != 0; }
+    boolean isExpression() { return (bits_ & NodeType.EXP.bit) != 0; }
+    boolean isSet() { return (bits_ & NodeType.SET.bit) != 0; }
+    boolean isVariable() { return (bits_ & NodeType.VAR.bit) != 0; }
+    boolean isConstant() { return (bits_ & NodeType.CON.bit) != 0; }
+    boolean isSymbol() { return (bits_ & NodeType.SYM.bit) != 0; }
+    boolean isRelation() { return (bits_ & NodeType.REL.bit) != 0; }
+    boolean isFunction() { return (bits_ & NodeType.FUN.bit) != 0; }
+    boolean isPolymorphicDataType() { return (bits_ & NodeType.PDT.bit) != 0; }
+    boolean isConstructor() { return (bits_ & NodeType.CNS.bit) != 0; }
+    boolean isDestructor() { return (bits_ & NodeType.DES.bit) != 0; }
+    boolean isOperator() { return (bits_ & NodeType.OPE.bit) != 0; }
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/NodeType.java b/src/main/java/com/viklauverk/eventbtools/core/NodeType.java
new file mode 100644
index 0000000..f45287a
--- /dev/null
+++ b/src/main/java/com/viklauverk/eventbtools/core/NodeType.java
@@ -0,0 +1,40 @@
+/*
+ Copyright (C) 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 enum NodeType
+{
+    PRE(1),
+    EXP(2),
+    SET(4),
+    VAR(8),
+    CON(16),
+    SYM(32),
+    REL(64),
+    FUN(128),
+    PDT(256),
+    CNS(512),
+    DES(1024),
+    OPE(2048);
+
+    public int bit;
+    NodeType(int b)
+    {
+        bit = b;
+    }
+}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/PolymorphicDataType.java b/src/main/java/com/viklauverk/eventbtools/core/PolymorphicDataType.java
index 7965482..e993d2e 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/PolymorphicDataType.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/PolymorphicDataType.java
@@ -53,9 +53,11 @@ public PolymorphicDataType(String bn, Theory t)
 
         constructors_ = new HashMap<>();
         constructor_names_ = new ArrayList<>();
+        constructor_ordering_ = new ArrayList<>();
 
         operators_ = new HashMap<>();
         operator_names_ = new ArrayList<>();
+        operator_ordering_ = new ArrayList<>();
         theory_ = t;
     }
 
@@ -119,6 +121,7 @@ public void addTypeParameter(String p)
     public void addConstructor(Constructor o)
     {
         constructors_.put(o.name(), o);
+        constructor_ordering_.add(o);
         constructor_names_ = constructors_.keySet().stream().sorted().collect(Collectors.toList());
     }
 
@@ -140,6 +143,7 @@ public List<String> constructorNames()
     public void addOperator(Operator o)
     {
         operators_.put(o.name(), o);
+        operator_ordering_.add(o);
         operator_names_ = operators_.keySet().stream().sorted().collect(Collectors.toList());
     }
 
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderFormulaUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderFormulaUnicode.java
index 9cc66d5..064cf50 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderFormulaUnicode.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderFormulaUnicode.java
@@ -501,6 +501,21 @@ public String c(String unicode, String ascii)
         return i;
     }
 
+    @Override public Formula visit_CONSTRUCTOR_SYMBOL(Formula i)
+    {
+        cnvs().constructor(Symbols.name(i.intData())); visitMeta(i); return i;
+    }
+
+    @Override public Formula visit_DESTRUCTOR_SYMBOL(Formula i)
+    {
+        cnvs().destructor(Symbols.name(i.intData())); visitMeta(i); return i;
+    }
+
+    @Override public Formula visit_OPERATOR_SYMBOL(Formula i)
+    {
+        cnvs().operator(Symbols.name(i.intData())); visitMeta(i); return i;
+    }
+
     @Override public Formula visit_VARIABLE_PRIM_SYMBOL(Formula i)
     {
         cnvs().variable(
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeSearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeSearch.java
index ed227c5..a5febc7 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeSearch.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeSearch.java
@@ -19,4 +19,16 @@
 
 public class RenderPolymorphicDataTypeSearch extends RenderPolymorphicDataType
 {
+    @Override
+    public void visit_PolymorphicDataTypeStart(PolymorphicDataType pdt)
+    {
+        renders().search().addPart(buildPolymorphicDataTypePartName(pdt));
+    }
+
+    @Override
+    public void visit_Constructor(PolymorphicDataType pdt, Constructor cnstr)
+    {
+        renders().search().addPart(buildConstructorPartName(pdt, cnstr));
+    }
+
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java
index 57bb058..20b32f2 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java
@@ -58,4 +58,9 @@ protected String buildTheoryDataTypePartName(Theory thr, PolymorphicDataType pdt
         return thr.name()+"/datatype/"+pdt.longName();
     }
 
+    protected String buildOperatorPartName(Operator oprt)
+    {
+        return oprt.name();
+    }
+
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java
index c825f08..cf9c95a 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java
@@ -19,4 +19,19 @@
 
 public class RenderTheorySearch extends RenderTheory
 {
+    public void visit_TheoryStart(Theory thr)
+    {
+        renders().search().addPart(buildTheoryPartName(thr));
+    }
+
+    public void visit_Import(Theory thr, Theory ext) { }
+
+    public void visit_Operator(Theory thr, Operator oprt)
+    {
+        renders().search().addPart(buildOperatorPartName(oprt));
+    }
+
+    public void visit_Axiom(Theory thr, Axiom axiom)
+    {
+    }
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java b/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java
index 178e628..62369f1 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java
@@ -61,8 +61,14 @@ public String toString()
     private Set<String> polymorphic_data_type_symbols_ = new HashSet<>(); // H List Seq
     private Map<String,PolymorphicDataType> polymorphic_data_types_ = new HashMap<>();
 
-    private Set<String> polymorphic_operator_symbols_ = new HashSet<>(); // seq seqSize listSize append
-    private Map<String,Operator> polymorphic_operators_ = new HashMap<>(); // Theory added operators.
+    private Set<String> constructor_symbols_ = new HashSet<>(); // nil epoch cons
+    private Map<String,Constructor> constructors_ = new HashMap<>();
+
+    private Set<String> destructor_symbols_ = new HashSet<>(); // head tail
+    private Map<String,Destructor> destructors_ = new HashMap<>();
+
+    private Set<String> operator_symbols_ = new HashSet<>(); // seq seqSize listSize append
+    private Map<String,Operator> operators_ = new HashMap<>(); // Theory added operators.
 
     private LinkedList<Frame> frames_ = new LinkedList<>();
 
@@ -170,7 +176,7 @@ public void addPolymorphicDataTypeSymbols(String... s)
 
     public Set<String> polymorphicOperatorSymbols()
     {
-        return polymorphic_operator_symbols_;
+        return operator_symbols_;
     }
 
     public boolean isPredicateSymbol(String p)
@@ -402,6 +408,112 @@ public void addConstantSymbols(List<String> s)
         constant_symbols_.addAll(s);
     }
 
+    // Constructor /////////////////////////////////////////////////////////////
+
+    public Constructor getConstructor(Formula name)
+    {
+        return getConstructor(name.symbol());
+    }
+
+    public Constructor getConstructor(String name)
+    {
+        Constructor var = constructors_.get(name);
+        if (var != null) return var;
+        for (SymbolTable parent : parents_)
+        {
+            var = parent.getConstructor(name);
+            if (var != null) return var;
+        }
+        return null;
+    }
+
+    public boolean isConstructorSymbol(String c)
+    {
+        boolean is = constructor_symbols_.contains(c);
+        if (is) return true;
+        for (SymbolTable parent : parents_)
+        {
+            is = parent.isConstructorSymbol(c);
+            if (is) return true;
+        }
+        return false;
+    }
+
+    public void addConstructorSymbol(String s)
+    {
+        constructor_symbols_.add(s);
+    }
+
+    public void addConstructor(Constructor c)
+    {
+        constructor_symbols_.add(c.name());
+        constructors_.put(c.name(), c);
+    }
+
+    public void addConstructorSymbols(String... s)
+    {
+        constructor_symbols_.addAll(Arrays.asList(s));
+    }
+
+    public void addConstructorSymbols(List<String> s)
+    {
+        constructor_symbols_.addAll(s);
+    }
+
+    // Destructor /////////////////////////////////////////////////////////////
+
+    public Destructor getDestructor(Formula name)
+    {
+        return getDestructor(name.symbol());
+    }
+
+    public Destructor getDestructor(String name)
+    {
+        Destructor var = destructors_.get(name);
+        if (var != null) return var;
+        for (SymbolTable parent : parents_)
+        {
+            var = parent.getDestructor(name);
+            if (var != null) return var;
+        }
+        return null;
+    }
+
+    public boolean isDestructorSymbol(String c)
+    {
+        boolean is = destructor_symbols_.contains(c);
+        if (is) return true;
+        for (SymbolTable parent : parents_)
+        {
+            is = parent.isDestructorSymbol(c);
+            if (is) return true;
+        }
+        return false;
+    }
+
+    public void addDestructorSymbol(String s)
+    {
+        destructor_symbols_.add(s);
+    }
+
+    public void addDestructor(Destructor c)
+    {
+        destructor_symbols_.add(c.name());
+        destructors_.put(c.name(), c);
+    }
+
+    public void addDestructorSymbols(String... s)
+    {
+        destructor_symbols_.addAll(Arrays.asList(s));
+    }
+
+    public void addDestructorSymbols(List<String> s)
+    {
+        destructor_symbols_.addAll(s);
+    }
+
+    // Number ////////////////////////////////////////////////
+
     public boolean isNumberSymbol(String p)
     {
         boolean is = number_symbols_.contains(p);
@@ -476,17 +588,17 @@ public boolean isPolymorphicDataTypeSymbol(String base_name)
 
     public void addPolymorphicOperator(Operator o)
     {
-        polymorphic_operator_symbols_.add(o.name());
-        polymorphic_operators_.put(o.name(), o);
+        operator_symbols_.add(o.name());
+        operators_.put(o.name(), o);
     }
 
-    public boolean isPolymorphicOperatorSymbol(String p)
+    public boolean isOperatorSymbol(String p)
     {
-        boolean is = polymorphic_operator_symbols_.contains(p);
+        boolean is = operator_symbols_.contains(p);
         if (is) return true;
         for (SymbolTable parent : parents_)
         {
-            is = parent.isPolymorphicOperatorSymbol(p);
+            is = parent.isOperatorSymbol(p);
             if (is) return true;
         }
         return false;
@@ -494,12 +606,12 @@ public boolean isPolymorphicOperatorSymbol(String p)
 
     public void addPolymorphicOperatorSymbol(String s)
     {
-        polymorphic_operator_symbols_.add(s);
+        operator_symbols_.add(s);
     }
 
     public void addPolymorphicOperatorSymbols(String... s)
     {
-        polymorphic_operator_symbols_.addAll(Arrays.asList(s));
+        operator_symbols_.addAll(Arrays.asList(s));
     }
 
     public boolean isUnknownSymbol(String p)
@@ -512,6 +624,9 @@ public boolean isUnknownSymbol(String p)
         if (isConstantSymbol(p)) return false;
         if (isNumberSymbol(p)) return false;
         if (isAnySymbol(p)) return false;
+        if (isPolymorphicDataTypeSymbol(p)) return false;
+        if (isConstructorSymbol(p)) return false;
+        if (isDestructorSymbol(p)) return false;
         return true;
     }
 
@@ -564,9 +679,13 @@ public String print()
         o.append("-\n");
         o.append("variables: "+Canvas.flow(80, printSyms(variable_symbols_)));
         o.append("-\n");
-        o.append("polytypes: "+Canvas.flow(80, printSyms(polymorphic_data_type_symbols_)));
+        o.append("datatypes: "+Canvas.flow(80, printSyms(polymorphic_data_type_symbols_)));
+        o.append("-\n");
+        o.append("constructors: "+Canvas.flow(80, printSyms(constructor_symbols_)));
+        o.append("-\n");
+        o.append("destructors: "+Canvas.flow(80, printSyms(destructor_symbols_)));
         o.append("-\n");
-        o.append("polyops: "+Canvas.flow(80, printSyms(polymorphic_operator_symbols_)));
+        o.append("operators: "+Canvas.flow(80, printSyms(operator_symbols_)));
 
         // The anys are special and used for wildcard matching. We only print these
         // if there are any to print.
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Sys.java b/src/main/java/com/viklauverk/eventbtools/core/Sys.java
index 366b1ad..71fd916 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/Sys.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/Sys.java
@@ -488,11 +488,11 @@ public void walkSystem(AllRenders ar, String pattern)
         }
     }
 
-    public List<String> listParts()
+    public List<String> listParts(String pattern)
     {
         AllRenders ar = lookupSearchWalker();
 
-        walkSystem(ar, "");
+        walkSystem(ar, pattern);
 
         return ar.search().foundParts();
     }
@@ -524,12 +524,12 @@ public String show(ShowSettings ss, Canvas canvas, String pattern)
     AllRenders lookupSearchWalker()
     {
         return new AllRenders(
-            new RenderTheorySearch(),
-            new RenderPolymorphicDataTypeSearch(),
             new RenderContextSearch(),
             new RenderMachineSearch(),
             new RenderEventSearch(),
             new RenderFormulaSearch(null),
+            new RenderTheorySearch(),
+            new RenderPolymorphicDataTypeSearch(),
             null);
     }
 
@@ -538,36 +538,36 @@ AllRenders lookupRenders(RenderTarget format, Canvas canvas)
         switch (format)
         {
         case PLAIN:
-            return new AllRenders(new RenderTheoryUnicode(),
-                                  new RenderPolymorphicDataTypeUnicode(),
-                                  new RenderContextUnicode(),
+            return new AllRenders(new RenderContextUnicode(),
                                   new RenderMachineUnicode(),
                                   new RenderEventUnicode(),
                                   new RenderFormulaUnicode(canvas),
+                                  new RenderTheoryUnicode(),
+                                  new RenderPolymorphicDataTypeUnicode(),
                                   canvas);
         case TERMINAL:
-            return new AllRenders(new RenderTheoryUnicode(),
-                                  new RenderPolymorphicDataTypeUnicode(),
-                                  new RenderContextUnicode(),
+            return new AllRenders(new RenderContextUnicode(),
                                   new RenderMachineUnicode(),
                                   new RenderEventUnicode(),
                                   new RenderFormulaUnicode(canvas),
+                                  new RenderTheoryUnicode(),
+                                  new RenderPolymorphicDataTypeUnicode(),
                                   canvas);
         case TEX:
-           return new AllRenders(new RenderTheoryTeX(),
-                                 new RenderPolymorphicDataTypeTeX(),
-                                 new RenderContextTeX(),
+           return new AllRenders(new RenderContextTeX(),
                                  new RenderMachineTeX(),
                                  new RenderEventTeX(),
                                  new RenderFormulaTeX(canvas),
+                                 new RenderTheoryTeX(),
+                                 new RenderPolymorphicDataTypeTeX(),
                                  canvas);
         case HTML:
-           return new AllRenders(new RenderTheoryHtmq(),
-                                 new RenderPolymorphicDataTypeHtmq(),
-                                 new RenderContextHtmq(),
+           return new AllRenders(new RenderContextHtmq(),
                                  new RenderMachineHtmq(),
                                  new RenderEventHtmq(),
                                  new RenderFormulaHtmq(canvas),
+                                 new RenderTheoryHtmq(),
+                                 new RenderPolymorphicDataTypeHtmq(),
                                  canvas);
         }
         assert (false) : "No case for format: "+format;
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Theory.java b/src/main/java/com/viklauverk/eventbtools/core/Theory.java
index bff48d1..b27dbac 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/Theory.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/Theory.java
@@ -630,12 +630,21 @@ void buildSymbolTable()
         */
 
         symbol_table_ = sys_.newTheorySymbolTable(name_);
-        //symbol_table_.addParents(parents);
 
         for (PolymorphicDataType pdt : polymorphicDataTypeOrdering())
         {
             log.debug("added polymorphic data type %s to symbol table %s", pdt.longName(), symbol_table_.name());
             symbol_table_.addPolymorphicDataType(pdt);
+            for (Constructor cnstr : pdt.constructorOrdering())
+            {
+                log.debug("    constructor %s", cnstr.name());
+                symbol_table_.addConstructor(cnstr);
+                for (Destructor dstr : cnstr.destructorOrdering())
+                {
+                    log.debug("        destructor %s", dstr.name());
+                    symbol_table_.addDestructor(dstr);
+                }
+            }
         }
         for (Operator c : operatorOrdering())
         {
diff --git a/src/main/java/com/viklauverk/eventbtools/core/WalkFormula.java b/src/main/java/com/viklauverk/eventbtools/core/WalkFormula.java
index 48e270c..8736359 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/WalkFormula.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/WalkFormula.java
@@ -56,6 +56,9 @@ public void exitNode(Formula f) {}
     public Formula visit_VARIABLE_PRIM_SYMBOL(Formula i) { return i; }
     public Formula visit_VARIABLE_NONFREE_SYMBOL(Formula i) { return i; }
     public Formula visit_CONSTANT_SYMBOL(Formula i) { return i; }
+    public Formula visit_CONSTRUCTOR_SYMBOL(Formula i) { return i; }
+    public Formula visit_DESTRUCTOR_SYMBOL(Formula i) { return i; }
+    public Formula visit_OPERATOR_SYMBOL(Formula i) { return i; }
     public Formula visit_APPLICATION(Formula i) { visitLeft(i); visitRight(i); return i; }
     public Formula visit_PARENTHESISED_PREDICATE(Formula i) { visitChild(i); return i; }
     public Formula visit_PARENTHESISED_EXPRESSION(Formula i) { visitChild(i); return i; }
@@ -183,6 +186,9 @@ Formula innerVisit(Formula ii)
         case VARIABLE_PRIM_SYMBOL: i = visit_VARIABLE_PRIM_SYMBOL(i); break;
         case VARIABLE_NONFREE_SYMBOL: i = visit_VARIABLE_NONFREE_SYMBOL(i); break;
         case CONSTANT_SYMBOL: i = visit_CONSTANT_SYMBOL(i); break;
+        case CONSTRUCTOR_SYMBOL: i = visit_CONSTRUCTOR_SYMBOL(i); break;
+        case DESTRUCTOR_SYMBOL: i = visit_DESTRUCTOR_SYMBOL(i); break;
+        case OPERATOR_SYMBOL: i = visit_OPERATOR_SYMBOL(i); break;
         case APPLICATION: i = visit_APPLICATION(i); break;
         case PARENTHESISED_PREDICATE: i = visit_PARENTHESISED_PREDICATE(i); break;
         case PARENTHESISED_EXPRESSION: i = visit_PARENTHESISED_EXPRESSION(i); break;
diff --git a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java
index 2cf0e3f..ca8b1e9 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java
@@ -34,10 +34,10 @@ public String go()
         String part = line_.trim();
         try
         {
-            List<String> parts = console_.sys().listParts();
+            List<String> parts = console_.sys().listParts(part);
             StringBuilder sb = new StringBuilder();
             for (String p : parts) {
-                if (p.indexOf(part) != -1) sb.append(p+"\n");
+                sb.append(p+"\n");
             }
             return sb.toString();
         }