Can read simple theory.

src/main/java/com/viklauverk/eventbtools/TestInternals.java

@@ -456,7 +456,7 @@ public static boolean testParserRenderer()
 
     public static boolean check(String in, String out, String out_with_types)
     {
-        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC;
+        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op;
 
         Formula fo = Formula.fromString(in, fc);
         String ot = fo.toStringWithTypes();
@@ -484,7 +484,7 @@ public static boolean check(String in, String out, String out_with_types)
 
     public static boolean checkFail(String in)
     {
-        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC;
+        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op;
         try
         {
             Formula f = Formula.fromString(in, fc);

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

@@ -655,7 +655,7 @@ public int lengthIgnoringAnsi(String s)
      */
     public void stopAlignments()
     {
-        assert(alignments_active_ == true) : "Internal error: Expected alignments to be active when starting alignments, but it was already active!";
+        assert(alignments_active_ == true) : "Internal error: Expected alignments to be active when stopping alignments, but it was inactive!";
         alignments_active_ = false;
 
         append("¤flush¤\n");
@@ -1149,10 +1149,10 @@ public void constructor(String s)
             append(colorize(BGreen, s));
             return;
         case TEX:
-            append("\\CNSTR{"+Util.texSafe(s)+"}");
+            append("\\CNST{"+Util.texSafe(s)+"}");
             return;
         case HTML:
-            append(" span(class=CNSTR)="+Util.quoteXMQ(s)+" ");
+            append(" span(class=CNST)="+Util.quoteXMQ(s)+" ");
             return;
         }
         assert (false) : "Unknown encoding "+render_target_;
@@ -1169,10 +1169,10 @@ public void destructor(String s)
             append(colorize(BGreen, s));
             return;
         case TEX:
-            append("\\DSTR{"+Util.texSafe(s)+"}");
+            append("\\DEST{"+Util.texSafe(s)+"}");
             return;
         case HTML:
-            append(" span(class=DSTR)="+Util.quoteXMQ(s)+" ");
+            append(" span(class=DEST)="+Util.quoteXMQ(s)+" ");
             return;
         }
         assert (false) : "Unknown encoding "+render_target_;

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

@@ -380,6 +380,21 @@ public boolean isPolymorphicDataType()
         return node_.isPolymorphicDataType();
     }
 
+    public boolean isConstructor()
+    {
+        return node_.isConstructor();
+    }
+
+    public boolean isDestructor()
+    {
+        return node_.isDestructor();
+    }
+
+    public boolean isOperator()
+    {
+        return node_.isOperator();
+    }
+
     public boolean equals(Formula f)
     {
         if (this == f) return true;

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

@@ -48,6 +48,9 @@ public static class MatchResult
         public Map<String,Formula> anys = new HashMap<>();
         public Map<String,Formula> numbers = new HashMap<>();
         public Map<String,Formula> polymorphic_data_types = new HashMap<>();
+        public Map<String,Formula> constructors = new HashMap<>();
+        public Map<String,Formula> destructors = new HashMap<>();
+        public Map<String,Formula> operators = new HashMap<>();
 
         public void clear()
         {
@@ -60,6 +63,9 @@ public void clear()
             anys.clear();
             numbers.clear();
             polymorphic_data_types.clear();
+            constructors.clear();
+            destructors.clear();
+            operators.clear();
         }
     }
 
@@ -75,14 +81,17 @@ public void clear()
      *
      * The patterns are always parsed using a symbol table containing:
      *
-     * predicate symbols: PQR
-     * expression symbols: EFG
-     * set symbols: STU
-     * variable symbols: xyz
-     * constant_symbols:cdf
-     * any symbols: ABC
-     * number symbols: NM
+     * predicate symbols: P Q R
+     * expression symbols: E F G
+     * set symbols: S T U
+     * variable symbols: x y z
+     * constant_symbols:c d f
+     * any symbols: A B C
+     * number symbols: N M
      * polymorphic_data_types: H
+     * constructors: cx (two character symbol)
+     * destructors: dx (two character symbol)
+     * operators: op (two character symbol)
      */
     public boolean match(Formula formula, String... pattern_strings)
     {
@@ -109,7 +118,7 @@ private static Formula lookupMatchRule(String s)
         Formula f = match_rules_.get(s);
         if (f != null) return f;
 
-        f = Formula.fromString(s, SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC);
+        f = Formula.fromString(s, SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op);
         match_rules_.put(s, f);
         return f;
     }
@@ -206,6 +215,24 @@ private static boolean tryMatch(Formula f, Formula p, MatchResult mr)
             if (!tryMetaMatch(f, p, mr)) return false;
             return okToAdd(f, p, mr.constants, "constants");
         }
+        if (pt == Node.CONSTRUCTOR_SYMBOL)
+        {
+            if (!f.isConstructor()) return false;
+            if (!tryMetaMatch(f, p, mr)) return false;
+            return okToAdd(f, p, mr.constructors, "constructors");
+        }
+        if (pt == Node.DESTRUCTOR_SYMBOL)
+        {
+            if (!f.isDestructor()) return false;
+            if (!tryMetaMatch(f, p, mr)) return false;
+            return okToAdd(f, p, mr.destructors, "destructors");
+        }
+        if (pt == Node.OPERATOR_SYMBOL)
+        {
+            if (!f.isOperator()) return false;
+            if (!tryMetaMatch(f, p, mr)) return false;
+            return okToAdd(f, p, mr.operators, "operators");
+        }
         if (pt == Node.NUMBER_SYMBOL)
         {
             if (!f.isNumber()) return false;
@@ -353,6 +380,23 @@ public Set<String> numberNames()
         return match_results_.numbers.keySet();
     }
 
+    public Formula getAny(String a)
+    {
+        Formula f = match_results_.anys.get(a);
+        assert (f != null) : "Internal error, could not find any-symbol "+a+" in matched results.";
+        return f;
+    }
+
+    public Formula tryGetAny(String a)
+    {
+        return match_results_.anys.get(a);
+    }
+
+    public Set<String> anyNames()
+    {
+        return match_results_.anys.keySet();
+    }
+
     public Formula getPolymorphicDataType(String v)
     {
         Formula f = match_results_.polymorphic_data_types.get(v);
@@ -365,21 +409,40 @@ public Set<String> polymorphicDataTypeNames()
         return match_results_.polymorphic_data_types.keySet();
     }
 
-    public Formula getAny(String a)
+    public Formula getConstructor(String v)
     {
-        Formula f = match_results_.anys.get(a);
-        assert (f != null) : "Internal error, could not find any-symbol "+a+" in matched results.";
+        Formula f = match_results_.constructors.get(v);
+        assert (f != null) : "Internal error, could not find constructor "+v+" in matched results.";
         return f;
     }
 
-    public Formula tryGetAny(String a)
+    public Set<String> constructorNames()
     {
-        return match_results_.anys.get(a);
+        return match_results_.constructors.keySet();
     }
 
-    public Set<String> anyNames()
+    public Formula getDestructor(String v)
     {
-        return match_results_.anys.keySet();
+        Formula f = match_results_.destructors.get(v);
+        assert (f != null) : "Internal error, could not find destructor "+v+" in matched results.";
+        return f;
+    }
+
+    public Set<String> destructorNames()
+    {
+        return match_results_.destructors.keySet();
+    }
+
+    public Formula getOperator(String v)
+    {
+        Formula f = match_results_.operators.get(v);
+        assert (f != null) : "Internal error, could not find operator "+v+" in matched results.";
+        return f;
+    }
+
+    public Set<String> operatorNames()
+    {
+        return match_results_.operators.keySet();
     }
 
     public String matchedRule()
@@ -415,14 +478,27 @@ public String allMatches()
         {
             sb.append(n+"="+getNumber(n)+" ");
         }
+        for (String a : anyNames())
+        {
+            sb.append(a+"="+getAny(a)+" ");
+        }
         for (String n : polymorphicDataTypeNames())
         {
             sb.append(n+"="+getPolymorphicDataType(n)+" ");
         }
-        for (String a : anyNames())
+        for (String n : constructorNames())
         {
-            sb.append(a+"="+getAny(a)+" ");
+            sb.append(n+"="+getConstructor(n)+" ");
+        }
+        for (String n : destructorNames())
+        {
+            sb.append(n+"="+getDestructor(n)+" ");
         }
+        for (String n : operatorNames())
+        {
+            sb.append(n+"="+getOperator(n)+" ");
+        }
+
         return sb.toString().trim();
     }
 

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

@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 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
@@ -23,7 +23,7 @@
 public
 class Prover
 {
-    SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC;
+    SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op;
 
     // _a stands for antecedent
     // _c stands for consequent

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

@@ -94,4 +94,9 @@ public void visit_PolymorphicDataTypesStart(Theory thr)
         cnvs().append("}\n");
     }
 
+    @Override
+    public void visit_PolymorphicDataTypesEnd(Theory thr)
+    {
+    }
+
 }

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

@@ -712,8 +712,6 @@ public void addDefaults()
         set_symbols_.add("T");
         set_symbols_.add("U");
 
-        polymorphic_data_type_symbols_.add("H");
-
         variable_symbols_.add("x");
         variable_symbols_.add("y");
         variable_symbols_.add("z");
@@ -728,14 +726,19 @@ public void addDefaults()
         any_symbols_.add("A");
         any_symbols_.add("B");
         any_symbols_.add("C");
+
+        polymorphic_data_type_symbols_.add("H");
+        constructor_symbols_.add("cx");
+        destructor_symbols_.add("dx");
+        operator_symbols_.add("op");
     }
 
-    public static SymbolTable PQR_EFG_STU_xyz_cdf_NM_ABC;
+    public static SymbolTable PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op;
 
     static
     {
         SymbolTable st = new SymbolTable("plain");
         st.addDefaults();
-        PQR_EFG_STU_xyz_cdf_NM_ABC = st;
+        PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op = st;
     }
 }

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

@@ -377,6 +377,9 @@ public class Templates {
 "\\definecolor{EvBCarrierSet}{HTML}{\\DarkGreen}%\n"+
 "\\definecolor{EvBPrimitiveSet}{HTML}{000000}%\n"+
 "\\definecolor{EvBPolymorphicDataType}{HTML}{000000}%\n"+
+"\\definecolor{EvBConstructor}{HTML}{000000}%\n"+
+"\\definecolor{EvBDestructor}{HTML}{000000}%\n"+
+"\\definecolor{EvBOperator}{HTML}{000000}%\n"+
 "\\definecolor{EvBComment}{HTML}{000000}%\n"+
 "\\definecolor{EvBLabel}{HTML}{0066cc}%\n"+
 "\\definecolor{EvBNames}{HTML}{000000}%\n"+
@@ -397,6 +400,9 @@ public class Templates {
 "\\definecolor{EvBCarrierSet}{HTML}{000000}%\n"+
 "\\definecolor{EvBPrimitiveSet}{HTML}{000000}%\n"+
 "\\definecolor{EvBPolymorphicDataType}{HTML}{\\Cyan}%\n"+
+"\\definecolor{EvBConstructor}{HTML}{\\Cyan}%\n"+
+"\\definecolor{EvBDestructor}{HTML}{\\Cyan}%\n"+
+"\\definecolor{EvBOperator}{HTML}{\\Cyan}%\n"+
 "\\definecolor{EvBComment}{HTML}{000000}%\n"+
 "\\definecolor{EvBLabel}{HTML}{000000}%\n"+
 "\\definecolor{EvBNames}{HTML}{000000}%\n"+
@@ -426,6 +432,9 @@ public class Templates {
 "\\newcommand{\\CSET}[1]{\\EVBTtextrm{\\EVBTcolor{EvBCarrierSet}#1}}%\n"+
 "\\newcommand{\\PSET}[1]{\\EVBTtextrm{\\EVBTcolor{EvBPrimitiveSet}#1}}%\n"+
 "\\newcommand{\\PDT}[1]{\\EVBTtextrm{\\EVBTcolor{EvBPolymorphicDataType}#1}}%\n"+
+"\\newcommand{\\CNST}[1]{\\EVBTtextrm{\\EVBTcolor{EvBConstructor}#1}}%\n"+
+"\\newcommand{\\DEST}[1]{\\EVBTtextrm{\\EVBTcolor{EvBDestructor}#1}}%\n"+
+"\\newcommand{\\OPER}[1]{\\EVBTtextrm{\\EVBTcolor{EvBOperator}#1}}%\n"+
 "\\newcommand{\\EXPR}[1]{\\EVBTtexttt{\\EVBTcolor{EvBExpression}#1}}%\n"+
 "\\newcommand{\\PRED}[1]{\\EVBTtexttt{\\EVBTcolor{EvBPredicate}#1}}%\n"+
 "\\newcommand{\\NONF}[1]{\\EVBTmathit{\\EVBTcolor{EvBNonFree}#1}}%\n"+

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

@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 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
@@ -79,7 +79,7 @@ public static boolean testContainingCardinalitys()
     public static boolean testm(String in, String out, String out_with_metas,
                                 String out_with_types, String out_with_metas_and_types)
     {
-        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC;
+        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op;
 
         Formula fo = Formula.fromString(in, fc);
 

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

@@ -195,7 +195,7 @@ else if (c == null)
      */
     private void extractPossibleImplTypesFromPredicate(Formula predicate, SymbolTable symbols)
     {
-        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC;
+        SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op;
         Formula fo = Formula.fromString("x:S", fc);
         boolean ok = pattern().match(predicate,
                                      "conjunction",     "P & Q",

templates/TeXDefinitions

@@ -182,6 +182,9 @@
 \definecolor{EvBCarrierSet}{HTML}{\DarkGreen}%
 \definecolor{EvBPrimitiveSet}{HTML}{000000}%
 \definecolor{EvBPolymorphicDataType}{HTML}{000000}%
+\definecolor{EvBConstructor}{HTML}{000000}%
+\definecolor{EvBDestructor}{HTML}{000000}%
+\definecolor{EvBOperator}{HTML}{000000}%
 \definecolor{EvBComment}{HTML}{000000}%
 \definecolor{EvBLabel}{HTML}{0066cc}%
 \definecolor{EvBNames}{HTML}{000000}%
@@ -202,6 +205,9 @@
 \definecolor{EvBCarrierSet}{HTML}{000000}%
 \definecolor{EvBPrimitiveSet}{HTML}{000000}%
 \definecolor{EvBPolymorphicDataType}{HTML}{\Cyan}%
+\definecolor{EvBConstructor}{HTML}{\Cyan}%
+\definecolor{EvBDestructor}{HTML}{\Cyan}%
+\definecolor{EvBOperator}{HTML}{\Cyan}%
 \definecolor{EvBComment}{HTML}{000000}%
 \definecolor{EvBLabel}{HTML}{000000}%
 \definecolor{EvBNames}{HTML}{000000}%
@@ -231,6 +237,9 @@
 \newcommand{\CSET}[1]{\EVBTtextrm{\EVBTcolor{EvBCarrierSet}#1}}%
 \newcommand{\PSET}[1]{\EVBTtextrm{\EVBTcolor{EvBPrimitiveSet}#1}}%
 \newcommand{\PDT}[1]{\EVBTtextrm{\EVBTcolor{EvBPolymorphicDataType}#1}}%
+\newcommand{\CNST}[1]{\EVBTtextrm{\EVBTcolor{EvBConstructor}#1}}%
+\newcommand{\DEST}[1]{\EVBTtextrm{\EVBTcolor{EvBDestructor}#1}}%
+\newcommand{\OPER}[1]{\EVBTtextrm{\EVBTcolor{EvBOperator}#1}}%
 \newcommand{\EXPR}[1]{\EVBTtexttt{\EVBTcolor{EvBExpression}#1}}%
 \newcommand{\PRED}[1]{\EVBTtexttt{\EVBTcolor{EvBPredicate}#1}}%
 \newcommand{\NONF}[1]{\EVBTmathit{\EVBTcolor{EvBNonFree}#1}}%