Properly parse formulas with theory operators that are infix/prefix a…

…nd predicate/expression.

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

@@ -21,6 +21,8 @@ import com.viklauverk.eventbtools.core.SymbolTable;
 
 @parser::header{
 import com.viklauverk.eventbtools.core.SymbolTable;
+import com.viklauverk.eventbtools.core.OperatorNotationType;
+import com.viklauverk.eventbtools.core.OperatorType;
 
 import java.util.List;
 import java.util.LinkedList;
@@ -231,13 +233,15 @@ predicate
    | { symbol_table.isAnySymbol(_input.LT(1).getText()) }?  sym=SYMBOL meta? # AnyPredicateSymbol
    | { symbol_table.isPredicateSymbol(_input.LT(1).getText()) }? sym=SYMBOL meta? # PredicateSymbol
    | '(' inner=predicate ')'                        # PredicateParentheses
+   | left=predicate { symbol_table.isOperatorSymbol(OperatorNotationType.INFIX, OperatorType.PREDICATE, _input.LT(1).getText()) }? operator=SYMBOL meta? right=predicate # OperatorInfixPredicate
    | left=expression IN meta? right=expression            # SetMembership
    | left=expression NOTIN meta? right=expression         # SetNotMembership
    | left=predicate operator=AND meta? right=predicate    # Conjunction
    | left=predicate operator=IMP meta? right=predicate    # Implication
    | 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
    | ALL meta? left=listOfNonFreeSymbols
      { pushFrame(((UniversalContext)_localctx).left); }
      QDOT right=predicate
@@ -274,7 +278,8 @@ expression
    | { 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.isOperatorSymbol(OperatorNotationType.PREFIX, OperatorType.EXPRESSION, _input.LT(1).getText()) }? operator=SYMBOL
+      meta? ( '(' parameters=listOfExpressions ')' )? # OperatorPrefixExpression
    | { 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
@@ -287,6 +292,7 @@ expression
    | left=expression operator=DIV meta? right=expression  # Division
    | left=expression operator=ADD meta? right=expression  # Addition
    | left=expression operator=MINUS meta? right=expression  # Subtraction
+   | left=expression { symbol_table.isOperatorSymbol(OperatorNotationType.INFIX, OperatorType.EXPRESSION, _input.LT(1).getText()) }? operator=SYMBOL meta? right=expression # OperatorInfixExpression
    | operator=MINUS right=expression                  # UnaryMinus
    | left=expression operator=MOD meta? right=expression  # Modulo
    | left=expression operator=EXP meta? right=expression  # Exponentiation
@@ -395,6 +401,10 @@ listOfExpressions
    : expression (',' expression)*
    ;
 
+listOfPredicates
+   : predicate (',' predicate)*
+   ;
+
 meta
    : '«' ( substitution | predicate | expression ) '»' #MetaFormula
    ;

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

@@ -18,6 +18,7 @@
 package com.viklauverk.eventbtools.core;
 
 import org.jline.reader.impl.completer.ArgumentCompleter;
+import org.jline.reader.impl.completer.NullCompleter;
 import org.jline.reader.impl.completer.StringsCompleter;
 import org.jline.reader.impl.completer.AggregateCompleter;
 import org.jline.builtins.Completers.TreeCompleter;
@@ -67,6 +68,7 @@ public static Completer addCompleters(Sys sys) {
              new ArgumentCompleter(new StringsCompleter("eb.show.formula")),
              new ArgumentCompleter(
                  new StringsCompleter("eb.show.part"),
+                 new StringsCompleter("--frame", "--tex"),
                  new SysCompleter(sys, false, false, false, true)
                  ),
              new ArgumentCompleter(
@@ -78,8 +80,8 @@ public static Completer addCompleters(Sys sys) {
              new ArgumentCompleter(new StringsCompleter("yms.add.constants")),
              new ArgumentCompleter(new StringsCompleter("yms.add.expressions")),
              new ArgumentCompleter(new StringsCompleter("yms.add.numbers")),
-             new ArgumentCompleter(new StringsCompleter("yms.add.polytypes")),
-             new ArgumentCompleter(new StringsCompleter("yms.add.polyops")),
+             new ArgumentCompleter(new StringsCompleter("yms.add.datatypes")),
+             new ArgumentCompleter(new StringsCompleter("yms.add.operators")),
              new ArgumentCompleter(new StringsCompleter("yms.add.predicates")),
              new ArgumentCompleter(new StringsCompleter("yms.add.sets")),
              new ArgumentCompleter(new StringsCompleter("yms.add.variables")),

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

@@ -246,6 +246,19 @@ public Formula right()
         meta_ = meta;
     }
 
+    Formula(Node node, int v, Formula left, Formula right, Formula meta)
+    {
+        assert (node != null && left != null && right != null) : "Internal error when creating formula, args must be non-null.";
+
+        node_ = node;
+        data_ = new int[1];
+        data_[0] = v;
+        children_ = new Formula[2];
+        children_[0] = left;
+        children_[1] = right;
+        meta_ = meta;
+    }
+
     Formula(Node node, Formula vars, Formula pred, Formula expr, Formula meta)
     {
         assert (node != null && vars != null && pred!= null && expr!= null) : "Internal error when creating formula, args must be non-null.";

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

@@ -187,9 +187,55 @@ public Formula visitDestructor(EvBFormulaParser.DestructorContext ctx)
     }
 
     @Override
-    public Formula visitOperator(EvBFormulaParser.OperatorContext ctx)
+    public Formula visitOperatorInfixPredicate(EvBFormulaParser.OperatorInfixPredicateContext ctx)
     {
-        return FormulaFactory.newOperatorSymbol(ctx.operator.getText(), visitOptionalMeta(ctx.meta()));
+        Formula left = this.visit(ctx.left);
+        Formula right = this.visit(ctx.right);
+
+        return FormulaFactory.newOperatorInfixSymbol(ctx.operator.getText(),
+                                                     OperatorNotationType.INFIX,
+                                                     OperatorType.PREDICATE,
+                                                     left,
+                                                     right,
+                                                     visitOptionalMeta(ctx.meta()));
+    }
+
+    @Override
+    public Formula visitOperatorInfixExpression(EvBFormulaParser.OperatorInfixExpressionContext ctx)
+    {
+        Formula left = this.visit(ctx.left);
+        Formula right = this.visit(ctx.right);
+
+        return FormulaFactory.newOperatorInfixSymbol(ctx.operator.getText(),
+                                                     OperatorNotationType.INFIX,
+                                                     OperatorType.EXPRESSION,
+                                                     left,
+                                                     right,
+                                                     visitOptionalMeta(ctx.meta()));
+    }
+
+    @Override
+    public Formula visitOperatorPrefixPredicate(EvBFormulaParser.OperatorPrefixPredicateContext ctx)
+    {
+        EvBFormulaParser.ListOfPredicatesContext parameters = ctx.listOfPredicates();
+
+        return FormulaFactory.newOperatorPrefixSymbol(ctx.operator.getText(),
+                                                      OperatorNotationType.PREFIX,
+                                                      OperatorType.PREDICATE,
+                                                      parameters != null ? visitListOfPredicates(parameters):null,
+                                                      visitOptionalMeta(ctx.meta()));
+    }
+
+    @Override
+    public Formula visitOperatorPrefixExpression(EvBFormulaParser.OperatorPrefixExpressionContext ctx)
+    {
+        EvBFormulaParser.ListOfExpressionsContext parameters = ctx.listOfExpressions();
+
+        return FormulaFactory.newOperatorPrefixSymbol(ctx.operator.getText(),
+                                                      OperatorNotationType.PREFIX,
+                                                      OperatorType.EXPRESSION,
+                                                      parameters != null ? visitListOfExpressions(parameters):null,
+                                                      visitOptionalMeta(ctx.meta()));
     }
 
     @Override
@@ -299,6 +345,17 @@ 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/FormulaFactory.java

@@ -148,9 +148,46 @@ Formula newDestructorSymbol (String s, Formula meta)
     }
 
     public static
-    Formula newOperatorSymbol (String s, Formula meta)
+    Formula newOperatorPrefixSymbol(String s, OperatorNotationType nt, OperatorType ot, Formula parameters, Formula meta)
     {
-        return new Formula(Node.OPERATOR_SYMBOL, Symbols.intern(s), meta);
+        Node n = null;
+        if (nt == OperatorNotationType.INFIX)
+        {
+            if (ot == OperatorType.PREDICATE) n = Node.OPERATOR_INFIX_PREDICATE_SYMBOL;
+            else n = Node.OPERATOR_INFIX_PREDICATE_SYMBOL;
+        }
+        else
+        {
+            if (ot == OperatorType.PREDICATE) n = Node.OPERATOR_PREFIX_PREDICATE_SYMBOL;
+            else n = Node.OPERATOR_PREFIX_PREDICATE_SYMBOL;
+        }
+
+        if (parameters != null)
+        {
+            return new Formula(n, Symbols.intern(s), parameters, meta);
+        }
+        else
+        {
+            return new Formula(n, Symbols.intern(s), meta);
+        }
+    }
+
+    public static
+    Formula newOperatorInfixSymbol(String s, OperatorNotationType nt, OperatorType ot,
+                                   Formula left, Formula right, Formula meta)
+    {
+        Node n = null;
+        if (nt == OperatorNotationType.INFIX)
+        {
+            if (ot == OperatorType.PREDICATE) n = Node.OPERATOR_INFIX_PREDICATE_SYMBOL;
+            else n = Node.OPERATOR_INFIX_PREDICATE_SYMBOL;
+        }
+        else
+        {
+            if (ot == OperatorType.PREDICATE) n = Node.OPERATOR_PREFIX_PREDICATE_SYMBOL;
+            else n = Node.OPERATOR_PREFIX_PREDICATE_SYMBOL;
+        }
+        return new Formula(n, Symbols.intern(s), left, right, meta);
     }
 
     public static
@@ -637,6 +674,12 @@ Formula newListOfExpressions(List<Formula> elements)
         return new Formula(Node.LIST_OF_EXPRESSIONS, elements, null);
     }
 
+    public static
+    Formula newListOfPredicates(List<Formula> elements)
+    {
+        return new Formula(Node.LIST_OF_PREDICATES, elements, null);
+    }
+
     public static
     Formula newEnumeratedSet(List<Formula> elements)
     {

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

@@ -40,7 +40,10 @@ public interface FormulaVisitor
     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_OPERATOR_INFIX_PREDICATE_SYMBOL(Formula i);
+    Formula visit_OPERATOR_INFIX_EXPRESSION_SYMBOL(Formula i);
+    Formula visit_OPERATOR_PREFIX_PREDICATE_SYMBOL(Formula i);
+    Formula visit_OPERATOR_PREFIX_EXPRESSION_SYMBOL(Formula i);
     Formula visit_APPLICATION(Formula i);
     Formula visit_PARENTHESISED_PREDICATE(Formula i);
     Formula visit_PARENTHESISED_EXPRESSION(Formula i);
@@ -111,6 +114,7 @@ public interface FormulaVisitor
     Formula visit_LIST_OF_VARIABLES(Formula i);
     Formula visit_LIST_OF_NONFREE_VARIABLES(Formula i);
     Formula visit_LIST_OF_EXPRESSIONS(Formula i);
+    Formula visit_LIST_OF_PREDICATES(Formula i);
     Formula visit_ADDITION(Formula i);
     Formula visit_SUBTRACTION(Formula i);
     Formula visit_MULTIPLICATION(Formula i);

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

@@ -41,11 +41,15 @@ public enum Node
     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
+    OPERATOR_INFIX_PREDICATE_SYMBOL(OPE.bit | SYM.bit), // An operator symbol: same lessThan
+    OPERATOR_INFIX_EXPRESSION_SYMBOL(OPE.bit | SYM.bit), // An operator symbol: merge minus
+    OPERATOR_PREFIX_PREDICATE_SYMBOL(OPE.bit | SYM.bit), // An operator symbol: same(a,b) lessThan(a,b)
+    OPERATOR_PREFIX_EXPRESSION_SYMBOL(OPE.bit | SYM.bit), // An operator symbol: merge(a,b) minus(a,b)
 
     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_EXPRESSIONS(0), // In a partition {a},{b},{c} is a list of expressions (sets).
+    LIST_OF_PREDICATES(0), // For an operator pp(P,Q,R) P,Q,R is a list of predicates.
     LIST_OF_TYPES(0), // In a DataType Seq(NAT) Map(NAT,INT)
 
     PARENTHESISED_PREDICATE(PRE.bit), // A predicate wrapped in parenthesis.

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

@@ -17,18 +17,23 @@
 
 package com.viklauverk.eventbtools.core;
 
+import com.viklauverk.eventbtools.core.OperatorNotationType;
+import com.viklauverk.eventbtools.core.OperatorType;
+
 public class Operator extends Typed
 {
     private String name_;
     private String comment_;
     private Formula definition_;
     private OperatorNotationType notation_type_;
+    private OperatorType operator_type_;
     private Theory theory_;
 
-    public Operator(String n, Theory t, OperatorNotationType s)
+    public Operator(String n, Theory t, OperatorNotationType nt, OperatorType ot)
     {
         name_ = n;
-        notation_type_ = s;
+        notation_type_ = nt;
+        operator_type_ = ot;
         theory_ = t;
     }
 
@@ -82,4 +87,22 @@ public boolean hasDefinition()
     {
         return definition_ != null;
     }
+
+    public OperatorNotationType notationType()
+    {
+        return notation_type_;
+    }
+
+    public OperatorType operatorType()
+    {
+        return operator_type_;
+    }
+
+    public boolean isOp(OperatorNotationType nt, OperatorType ot)
+    {
+        if (notation_type_ != nt) return false;
+        if (operator_type_ != ot) return false;
+
+        return true;
+    }
 }

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

@@ -227,7 +227,7 @@ private static boolean tryMatch(Formula f, Formula p, MatchResult mr)
             if (!tryMetaMatch(f, p, mr)) return false;
             return okToAdd(f, p, mr.destructors, "destructors");
         }
-        if (pt == Node.OPERATOR_SYMBOL)
+        if (pt.isOperator())
         {
             if (!f.isOperator()) return false;
             if (!tryMetaMatch(f, p, mr)) return false;

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

@@ -436,4 +436,9 @@ public RenderFormulaTeX(Canvas canvas)
         visitChildren(i, ()->{cnvs().append(",\\allowbreak "); }); return i;
     }
 
+    @Override public Formula visit_LIST_OF_PREDICATES(Formula i)
+    {
+        visitChildren(i, ()->{cnvs().append(",\\allowbreak "); }); return i;
+    }
+
 }