Jump into console with correct symbol table set when parse fails. Thi…

…s helps debugging parse fails of forumlas.

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

@@ -220,9 +220,13 @@ substitution
    ;
 
 listOfNonFreeSymbols
-   : SYMBOL (',' SYMBOL)*                          # ListOfNonFreeVariables
+   : SYMBOL ofTyping? (',' SYMBOL ofTyping? )*                          # ListOfNonFreeVariables
    ;
 
+ofTyping
+    : OFTYPE meta? type=expression                 # OfTypeVar
+    ;
+
 listOfSymbols
    : SYMBOL (',' SYMBOL)*                          # ListOfVariables
    ;
@@ -241,7 +245,7 @@ predicate
    | left=predicate operator=EQUIV meta? right=predicate  # Equivalence
    | left=predicate operator=OR meta? right=predicate     # Disjunction
    | operator=NOT meta? right=predicate                   # Negation
-   | { symbol_table.isOperatorSymbol(OperatorNotationType.PREFIX, OperatorType.PREDICATE, _input.LT(1).getText()) }? operator=SYMBOL meta? ( '(' parameters=listOfPredicates ')' )?  # OperatorPrefixPredicate
+   | { symbol_table.isOperatorSymbol(OperatorNotationType.PREFIX, OperatorType.PREDICATE, _input.LT(1).getText()) }? operator=SYMBOL meta? ( '(' parameters=listOfExpressions ')' )?  # OperatorPrefixPredicate
    | ALL meta? left=listOfNonFreeSymbols
      { pushFrame(((UniversalContext)_localctx).left); }
      QDOT right=predicate
@@ -401,10 +405,6 @@ listOfExpressions
    : expression (',' expression)*
    ;
 
-listOfPredicates
-   : predicate (',' predicate)*
-   ;
-
 meta
    : '«' ( substitution | predicate | expression ) '»' #MetaFormula
    ;

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

@@ -20,6 +20,7 @@
 import com.viklauverk.eventbtools.core.Machine;
 import com.viklauverk.eventbtools.core.Sys;
 
+import com.viklauverk.eventbtools.core.AbortIntoConsole;
 import com.viklauverk.eventbtools.core.Canvas;
 import com.viklauverk.eventbtools.core.Console;
 import com.viklauverk.eventbtools.core.ConsoleException;
@@ -69,8 +70,15 @@ public static void run(Settings s) throws Exception
                                            s.commonSettings().sourceDir(),
                                            s.commonSettings().theoryRootDir()));
         }
-        sys.loadTheoriesAndContextsAndMachines(s.commonSettings().sourceDir(), s.commonSettings().theoryRootDir());
-
+        try
+        {
+            sys.loadTheoriesAndContextsAndMachines(s.commonSettings().sourceDir(), s.commonSettings().theoryRootDir());
+        }
+        catch (AbortIntoConsole e)
+        {
+            sys.console().forceCurrentSymbolTable(e.symbolTable());
+            System.out.println(e.formula());
+        }
         Canvas canvas = new Canvas();
         canvas.setRenderTarget(RenderTarget.TERMINAL);
         RenderAttributes ra = sys.console().renderAttributes();

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

@@ -0,0 +1,45 @@
+/*
+ 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;
+
+import org.antlr.v4.runtime.misc.ParseCancellationException;
+
+public class AbortIntoConsole extends Error
+{
+    private static final long serialVersionUID = 1L;
+
+    private String formula_;
+    private transient SymbolTable symbol_table_;
+
+    public AbortIntoConsole(String msg, String formula, SymbolTable st)
+    {
+        super(msg);
+        formula_ = formula;
+        symbol_table_ = st;
+    }
+
+    public String formula()
+    {
+        return formula_;
+    }
+
+    public SymbolTable symbolTable()
+    {
+        return symbol_table_;
+    }
+}

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

@@ -149,6 +149,11 @@ public String renderPart(String name, RenderTarget rt, RenderAttributes ra)
         return result;
     }
 
+    public void forceCurrentSymbolTable(SymbolTable st)
+    {
+        current_symbol_table_ = st;
+    }
+
     void pushSymbolTable(String name)
     {
         SymbolTable st = sys_.newSymbolTable(name);

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

@@ -296,9 +296,8 @@ Formula fromString (String s, SymbolTable fc)
         {
             System.out.print("Could not parse formula:\n    ");
             System.out.println(s);
-            System.out.println("\nWhile using symbol table:");
-            fc.print();
-            System.exit(1);
+            System.out.println("\nWhile using symbol table:\n"+fc.print());
+            throw new AbortIntoConsole("Could not parse formula: "+s, s, fc);
         }
         return f;
     }
@@ -312,8 +311,7 @@ Formula fromStringMightFail(String s, SymbolTable fc)
         {
             System.out.print("Could not parse formula :\n    ");
             System.out.println(s);
-            System.out.println("\nWhile using symbol table:");
-            fc.print();
+            System.out.println("\nWhile using symbol table:\n"+fc.print());
         }
         return f;
     }

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

@@ -217,12 +217,12 @@ public Formula visitOperatorInfixExpression(EvBFormulaParser.OperatorInfixExpres
     @Override
     public Formula visitOperatorPrefixPredicate(EvBFormulaParser.OperatorPrefixPredicateContext ctx)
     {
-        EvBFormulaParser.ListOfPredicatesContext parameters = ctx.listOfPredicates();
+        EvBFormulaParser.ListOfExpressionsContext parameters = ctx.listOfExpressions();
 
         return FormulaFactory.newOperatorPrefixSymbol(ctx.operator.getText(),
                                                       OperatorNotationType.PREFIX,
                                                       OperatorType.PREDICATE,
-                                                      parameters != null ? visitListOfPredicates(parameters):null,
+                                                      parameters != null ? visitListOfExpressions(parameters):null,
                                                       visitOptionalMeta(ctx.meta()));
     }
 
@@ -345,17 +345,6 @@ public Formula visitListOfExpressions(EvBFormulaParser.ListOfExpressionsContext
         return FormulaFactory.newListOfExpressions(elements);
     }
 
-    @Override
-    public Formula visitListOfPredicates(EvBFormulaParser.ListOfPredicatesContext ctx)
-    {
-        List<Formula> elements = new LinkedList<>();
-        for (EvBFormulaParser.PredicateContext sec : ctx.predicate())
-        {
-            elements.add(this.visit(sec));
-        }
-        return FormulaFactory.newListOfPredicates(elements);
-    }
-
     @Override
     public Formula visitEnumeratedSet(EvBFormulaParser.EnumeratedSetContext ctx)
     {

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

@@ -152,6 +152,61 @@ public Set<String> polymorphicDataTypeSymbols()
         return polymorphic_data_type_symbols_;
     }
 
+    public boolean hasAnySymbols()
+    {
+        return any_symbols_.size() > 0;
+    }
+
+    public boolean hasConstantSymbols()
+    {
+        return constant_symbols_.size() > 0;
+    }
+
+    public boolean hasExpressionSymbols()
+    {
+        return expression_symbols_.size() > 0;
+    }
+
+    public boolean hasNumberSymbols()
+    {
+        return number_symbols_.size() > 0;
+    }
+
+    public boolean hasSetSymbols()
+    {
+        return set_symbols_.size() > 0;
+    }
+
+    public boolean hasPredicateSymbols()
+    {
+        return predicate_symbols_.size() > 0;
+    }
+
+    public boolean hasVariableSymbols()
+    {
+        return variable_symbols_.size() > 0;
+    }
+
+    public boolean hasPolymorphicDataTypeSymbols()
+    {
+        return polymorphic_data_type_symbols_.size() > 0;
+    }
+
+    public boolean hasConstructorSymbols()
+    {
+        return constructors_.size() > 0;
+    }
+
+    public boolean hasDestructorSymbols()
+    {
+        return destructors_.size() > 0;
+    }
+
+    public boolean hasOperatorSymbols()
+    {
+        return operators_.size() > 0;
+    }
+
     public PolymorphicDataType getPolymorphicDataType(Formula name)
     {
         return getPolymorphicDataType(name.symbol());
@@ -586,6 +641,7 @@ public boolean isPolymorphicDataTypeSymbol(String base_name)
         return false;
     }
 
+
     public void addOperator(Operator o)
     {
         operator_symbols_.add(o.name());
@@ -697,38 +753,78 @@ public String print()
         cnvs.setRenderTarget(RenderTarget.PLAIN);
         StringBuilder o = new StringBuilder();
 
-        for (SymbolTable p : parents_)
-        {
-            p.print();
-        }
         String title = "SymbolTable "+name_;
+        boolean need_line = false;
 
-        o.append("constants: "+Canvas.flow(80, printSyms(constant_symbols_)));
-        o.append("-\n");
-        o.append("expressions: "+Canvas.flow(80, printSyms(expression_symbols_)));
-        o.append("-\n");
-        o.append("numbers: "+Canvas.flow(80, printSyms(number_symbols_)));
-        o.append("-\n");
-        o.append("predicates: "+Canvas.flow(80, printSyms(predicate_symbols_)));
-        o.append("-\n");
-        o.append("sets: "+Canvas.flow(80, printSyms(set_symbols_)));
-        o.append("-\n");
-        o.append("variables: "+Canvas.flow(80, printSyms(variable_symbols_)));
-        o.append("-\n");
-        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("operators: "+Canvas.flow(80, printOperatorSyms(operator_symbols_)));
-
-        // The anys are special and used for wildcard matching. We only print these
-        // if there are any to print.
-        if (any_symbols_.size() > 0)
-        {
-            o.append("-\n");
+        if (hasConstantSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("constants: "+Canvas.flow(80, printSyms(constant_symbols_)));
+            need_line = true;
+        }
+        if (hasExpressionSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("expressions: "+Canvas.flow(80, printSyms(expression_symbols_)));
+            need_line = true;
+        }
+        if (hasNumberSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("numbers: "+Canvas.flow(80, printSyms(number_symbols_)));
+            need_line = true;
+        }
+        if (hasPredicateSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("predicates: "+Canvas.flow(80, printSyms(predicate_symbols_)));
+            need_line = true;
+        }
+        if (hasSetSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("sets: "+Canvas.flow(80, printSyms(set_symbols_)));
+            need_line = true;
+        }
+        if (hasVariableSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("variables: "+Canvas.flow(80, printSyms(variable_symbols_)));
+            need_line = true;
+        }
+        if (hasPolymorphicDataTypeSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("datatypes: "+Canvas.flow(80, printSyms(polymorphic_data_type_symbols_)));
+            need_line = true;
+        }
+        if (hasConstructorSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("constructors: "+Canvas.flow(80, printSyms(constructor_symbols_)));
+            need_line = true;
+        }
+        if (hasDestructorSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("destructors: "+Canvas.flow(80, printSyms(destructor_symbols_)));
+            need_line = true;
+        }
+        if (hasOperatorSymbols())
+        {
+            if (need_line) o.append("-\n");
+            o.append("operators: "+Canvas.flow(80, printOperatorSyms(operator_symbols_)));
+            need_line = true;
+        }
+        if (hasAnySymbols())
+        {
+            if (need_line) o.append("-\n");
             o.append("anys: "+Canvas.flow(80, printSyms(any_symbols_)));
+            need_line = true;
+        }
+        for (SymbolTable p : parents_)
+        {
+            o.append(p.print());
         }
         String f = cnvs.frame(title, o.toString(), Canvas.sline);
         return f;