Binary operation done right interim

src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4

@@ -20,30 +20,28 @@ sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? | anywhere=sem
 semiSeqPattern : termPattern (',' termPattern)*;
 
 termPattern :
-	   DONTCARE      #dontCare
+      termPattern MUL termPattern                               #mult
+    | <assoc=right> termPattern op=(DIV|MOD) termPattern        #divMod
+    | termPattern op=(PLUS|MINUS) termPattern                   #plusMinus
+    | termPattern op=(LE|GE|LEQ|GEQ) termPattern                #comparison
+    | termPattern op=(NEQ|EQ) termPattern                       #equality
+    | termPattern AND termPattern                               #and
+    | termPattern OR termPattern                                #or
+    | termPattern IMP termPattern                               #impl
+    | termPattern XOR termPattern                               #xor
+    //|   termPattern EQUIV termPattern already covered by EQ/NEQ
+    | MINUS termPattern                                         #exprNegate
+    | NOT termPattern                                           #exprNot
+    | '(' termPattern ')'                                       #exprParen
+    | func=ID ( '(' termPattern (',' termPattern)* ')')?        #function
+    |  DONTCARE                                                 #dontCare
     //| STARDONTCARE  #starDontCare
     | SID                                                       #schemaVar
     | STARDONTCARE termPattern STARDONTCARE                     #anywhere
     | DIGITS                                                    #number
-	 | func=ID ( '(' termPattern (',' termPattern)* ')')? #function
-	 | left=termPattern op=(PLUS|MINUS|MUL|LE|GE|LEQ|GEQ|NEQ|EQ| AND|OR|IMP) right=termPattern #binaryOperation
+    // not working because of ambigue | left=termPattern op=(PLUS|MINUS|MUL|LE|GE|LEQ|GEQ|NEQ|EQ| AND|OR|IMP) right=termPattern #binaryOperation
     ;
 
-	 /*
-	       expression MUL expression #exprMultiplication
-         | <assoc=right> expression DIV expression #exprDivision
-         | expression op=(PLUS|MINUS) expression #exprLineOperators
-         | expression op=(LE|GE|LEQ|GEQ) expression #exprComparison
-         | expression op=(NEQ|EQ) expression  #exprEquality
-         | expression AND expression   #exprAnd
-         | expression OR expression    #exprOr
-         | expression IMP expression   #exprIMP
-         //|   expression EQUIV expression already covered by EQ/NEQ
-         | expression LBRACKET substExpressionList RBRACKET #exprSubst
-         | MINUS expression   #exprNegate
-         | NOT expression  #exprNot
-         | '(' expression ')' #exprParen
-	 */
 /*
 f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...)
 */
@@ -52,12 +50,6 @@ f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f
 ARROW : '⇒' | '==>';
 DONTCARE: '?' | '_' | '█';
 STARDONTCARE: '...' | '…';
-DIGITS : DIGIT+ ;
-fragment DIGIT : [0-9] ;
-SID: '?' [_a-zA-Z0-9\\]+ ;
-ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*;
-
-
 PLUS : '+' ;
 MINUS : '-' ;
 MUL : '*' ;
@@ -71,6 +63,13 @@ LE : '<' ;
 AND : '&' ;
 OR: '|' ;
 IMP: '->';
+MOD:'%';
+XOR:'^';
+
+DIGITS : DIGIT+ ;
+fragment DIGIT : [0-9] ;
+SID: '?' [_a-zA-Z0-9\\]+ ;
+ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*;
 
 COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
 WS: [\n\f\r\t ] -> channel(HIDDEN);

src/main/java/edu/kit/formal/psdb/termmatcher/MatchPatternDualVisitor.java

@@ -55,11 +55,6 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
         return visitFunction(ctx, stack.peek());
     }
 
-    @Override
-    public T visitBinaryOperation(MatchPatternParser.BinaryOperationContext ctx) {
-        return visitBinaryOperation(ctx, stack.peek());
-    }
-
     @Override
     public final T visitAnywhere(MatchPatternParser.AnywhereContext ctx) {
         return visitAnywhere(ctx, stack.peek());
@@ -67,11 +62,94 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
 
     protected abstract T visitAnywhere(MatchPatternParser.AnywhereContext ctx, S peek);
 
-    protected abstract T visitBinaryOperation(MatchPatternParser.BinaryOperationContext ctx, S peek);
-
     protected abstract T visitFunction(MatchPatternParser.FunctionContext ctx, S peek);
 
     protected abstract T visitNumber(MatchPatternParser.NumberContext ctx, S peek);
 
     protected abstract T visitSequentPattern(MatchPatternParser.SequentPatternContext ctx, S peek);
+
+    @Override
+    public T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx) {
+        return visitPlusMinus(ctx, stack.peek());
+    }
+
+    protected abstract T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx, S peek);
+
+    @Override
+    public T visitMult(MatchPatternParser.MultContext ctx) {
+        return visitMult(ctx, stack.peek());
+    }
+
+    protected abstract T visitMult(MatchPatternParser.MultContext ctx, S peek);
+
+    @Override
+    public T visitComparison(MatchPatternParser.ComparisonContext ctx) {
+        return visitComparison(ctx, stack.peek());
+    }
+
+    protected abstract T visitComparison(MatchPatternParser.ComparisonContext ctx, S peek);
+
+    @Override
+    public T visitOr(MatchPatternParser.OrContext ctx) {
+        return visitOr(ctx, stack.peek());
+    }
+
+    protected abstract T visitOr(MatchPatternParser.OrContext ctx, S peek);
+
+    @Override
+    public T visitExprNot(MatchPatternParser.ExprNotContext ctx) {
+        return visitExprNot(ctx, stack.peek());
+    }
+
+    public abstract T visitExprNot(MatchPatternParser.ExprNotContext ctx, S peek);
+
+    @Override
+    public T visitExprNegate(MatchPatternParser.ExprNegateContext ctx) {
+        return visitExprNegate(ctx, stack.peek());
+    }
+
+    public abstract T visitExprNegate(MatchPatternParser.ExprNegateContext ctx, S peek);
+
+    @Override
+    public T visitExprParen(MatchPatternParser.ExprParenContext ctx) {
+        return accept(ctx.termPattern(), stack.peek());
+    }
+
+    @Override
+    public T visitImpl(MatchPatternParser.ImplContext ctx) {
+        return visitImpl(ctx, stack.peek());
+    }
+
+    protected abstract T visitImpl(MatchPatternParser.ImplContext ctx, S peek);
+
+    @Override
+    public T visitDivMod(MatchPatternParser.DivModContext ctx) {
+        return visitDivMod(ctx, stack.peek());
+    }
+
+    protected abstract T visitDivMod(MatchPatternParser.DivModContext ctx, S peek);
+
+    @Override
+    public T visitAnd(MatchPatternParser.AndContext ctx) {
+        return visitAnd(ctx, stack.peek());
+    }
+
+    protected abstract T visitAnd(MatchPatternParser.AndContext ctx, S peek);
+
+    @Override
+    public T visitXor(MatchPatternParser.XorContext ctx) {
+        return visitXor(ctx, stack.peek());
+    }
+
+    protected abstract T visitXor(MatchPatternParser.XorContext ctx, S peek);
+
+    @Override
+    public T visitEquality(MatchPatternParser.EqualityContext ctx) {
+        return visitEquality(ctx, stack.peek());
+    }
+
+    protected abstract T visitEquality(MatchPatternParser.EqualityContext ctx, S peek);
 }
+    
+
+

src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java

@@ -2,6 +2,9 @@ package edu.kit.formal.psdb.termmatcher;
 
 import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
+import org.antlr.v4.runtime.CommonToken;
+import org.antlr.v4.runtime.Lexer;
+import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.Token;
 
 import java.util.*;
@@ -10,6 +13,7 @@ import java.util.stream.Stream;
 
 /**
  * Matchpattern visitor visits the matchpatterns of case-statements
+ *
  * @author Alexander Weigl
  * @author S. Grebing
  */
@@ -17,8 +21,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
     static final Matchings NO_MATCH = new Matchings();
     static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
 
-    private Stack<Term> termStack = new Stack<>();
-
     protected static List<MatchInfo> reduceConform(List<MatchInfo> m1, List<MatchInfo> m2) {
         if (m1 == null || m2 == null) return null; //"null" is equivalent to NO_MATCH
 
@@ -99,6 +101,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
 
     /**
      * Visit a '...'Term'...' structure
+     *
      * @param ctx
      * @param peek
      * @return
@@ -113,81 +116,42 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
         return m;
     }
 
-    @Override
-    protected Matchings visitBinaryOperation(MatchPatternParser.BinaryOperationContext ctx, Term peek) {
-        Token op = ctx.op;
-        String opToKeYName = convert(op.getType());
-
-        MatchPatternParser.TermPatternContext left = ctx.left;
-        MatchPatternParser.TermPatternContext right = ctx.right;
-
-        if (peek.op().name().toString().equals(opToKeYName)  // same name
-                && peek.arity() == 2   // we know that we are in binary term
-                ) {
-            Matchings lM = accept(left, peek.sub(0));
-            Matchings rM = accept(right, peek.sub(1));
-            Matchings ret = reduceConform(lM, rM);
-            return ret;
-            /*return IntStream.range(0, peek.arity())
-                    .mapToObj(i -> (Matchings) accept(ctx.termPattern(i), peek.sub(i)))
-                    .reduce(MatcherImpl::reduceConform)
-                    .orElse(NO_MATCH);*/
-        }
-        return NO_MATCH;
-
+    protected Matchings visitBinaryOperation(String keyOpName, MatchPatternParser.TermPatternContext ctx, Term peek) {
+        MatchPatternParser.FunctionContext func = new MatchPatternParser.FunctionContext(ctx);
+        func.func = new CommonToken(MatchPatternLexer.ID, keyOpName);
 
+        return accept(func, peek);
     }
 
     private String convert(int op) {
-
         switch (op) {
-
             case MatchPatternParser.PLUS:
                 return "add";
-
             case MatchPatternParser.MINUS:
                 return "sub";
-
             case MatchPatternParser.MUL:
                 return "mul";
-
-
             case MatchPatternParser.DIV:
                 return "div";
-
-
             case MatchPatternParser.LE:
                 return "lt";
-
-
             case MatchPatternParser.LEQ:
                 return "leq";
-
-
             case MatchPatternParser.EQ:
                 return "equals";
-
             case MatchPatternParser.GE:
                 return "gt";
-
             case MatchPatternParser.GEQ:
                 return "geq";
-
             case MatchPatternParser.IMP:
                 return "imp";
-
-
             case MatchPatternParser.AND:
                 return "and";
-
             case MatchPatternParser.OR:
                 return "or";
-
             default:
                 throw new UnsupportedOperationException("The operator " + op + "is not known");
         }
-
-
     }
 
     /**
@@ -221,6 +185,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
 
     /**
      * Visit a function and predicate symbol without a sequent arrow
+     *
      * @param ctx
      * @param peek
      * @return
@@ -241,6 +206,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
 
     /**
      * Visit a semisequent pattern f(x), f(y)
+     *
      * @param ctx
      * @param peek
      * @return
@@ -257,6 +223,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
 
     /**
      * Visit a sequent pattern 'f(x) ==> f(x)', 'f(x) ==>' or '==> f(x)'
+     *
      * @param ctx
      * @param peek
      * @return
@@ -266,6 +233,61 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
         return null;
     }
 
+    @Override
+    protected Matchings visitPlusMinus(MatchPatternParser.PlusMinusContext ctx, Term peek) {
+        return null;
+    }
+
+    @Override
+    protected Matchings visitMult(MatchPatternParser.MultContext ctx, Term peek) {
+        return visitBinaryOperation("mul", ctx, peek);
+    }
+
+    @Override
+    protected Matchings visitComparison(MatchPatternParser.ComparisonContext ctx, Term peek) {
+        return visitBinaryOperation(convert(ctx.op),ctx, peek);
+    }
+
+    @Override
+    protected Matchings visitOr(MatchPatternParser.OrContext ctx, Term peek) {
+        return visitBinaryOperation(convert(ctx.op),ctx, peek);
+    }
+
+    @Override
+    public Matchings visitExprNot(MatchPatternParser.ExprNotContext ctx, Term peek) {
+        return visitBinaryOperation("not",ctx, peek);
+    }
+
+    @Override
+    public Matchings visitExprNegate(MatchPatternParser.ExprNegateContext ctx, Term peek) {
+        return visitBinaryOperation("sub",ctx, peek);
+    }
+
+    @Override
+    protected Matchings visitImpl(MatchPatternParser.ImplContext ctx, Term peek) {
+        return visitBinaryOperation("imp",ctx, peek);
+    }
+
+    @Override
+    protected Matchings visitDivMod(MatchPatternParser.DivModContext ctx, Term peek) {
+        return visitBinaryOperation(convert(ctx.op), peek);
+    }
+
+    @Override
+    protected Matchings visitAnd(MatchPatternParser.AndContext ctx, Term peek) {
+        return visitBinaryOperation("and", peek);
+    }
+
+    @Override
+    protected Matchings visitXor(MatchPatternParser.XorContext ctx, Term peek) {
+        return visitBinaryOperation("xor", peek);
+    }
+
+    @Override
+    protected Matchings visitEquality(MatchPatternParser.EqualityContext ctx, Term peek) {
+        return visitBinaryOperation("eq", peek);
+    }
+
     private Stream<Term> subTerms(Term peek) {
         ArrayList<Term> list = new ArrayList<>();
         subTerms(list, peek);