partly working matcher

matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java

@@ -4,6 +4,8 @@ import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Semisequent;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.parser.DefaultTermParser;
+import de.uka.ilkd.key.parser.ParserException;
 import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternLexer;
 import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser;
 import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade;
@@ -13,6 +15,8 @@ import org.antlr.v4.runtime.CommonTokenStream;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
+import java.io.StringReader;
+
 /**
  * A facade for capturing everything we want to do with matchers.
  *
@@ -25,6 +29,8 @@ public class MatcherFacade {
     public static Matchings matches(String pattern, Term keyTerm, Services services) {
         MatcherImpl matcher = new MatcherImpl(services);
         matcher.setCatchAll(false);
+
+
         MatchPatternParser mpp = getParser(pattern);
         MatchPatternParser.TermPatternContext ctx = mpp.termPattern();
         return matcher.accept(ctx, MatchPathFacade.createRoot(keyTerm));

rt-key/build.gradle

@@ -3,5 +3,5 @@ description = ''
 dependencies {
   compile project(':rt')
   compile project(':keydeps')
-  compile project(':matcher')
+//  compile project(':matcher')
 }

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java

@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.interpreter;
 
 import de.uka.ilkd.key.api.KeYApi;
 import de.uka.ilkd.key.api.ProofApi;
-import de.uka.ilkd.key.api.ScriptApi;
 import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
@@ -14,6 +13,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.interpreter.funchdl.*;
+import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher;
 import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.Visitor;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/functions/FindInSequence.java

 package edu.kit.iti.formal.psdbg.interpreter.functions;
 
 import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
-import edu.kit.iti.formal.psdbg.interpreter.KeYMatcher;
+import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/DispatchOn.java

+package edu.kit.iti.formal.psdbg.interpreter.matcher;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+@Retention(RetentionPolicy.RUNTIME)
+public @interface DispatchOn {
+    Class<?> value();
+}

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java → rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java

-package edu.kit.iti.formal.psdbg.interpreter;
+package edu.kit.iti.formal.psdbg.interpreter.matcher;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Name;
@@ -12,6 +12,7 @@ import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.TacletApp;
+import edu.kit.iti.formal.psdbg.interpreter.MatcherApi;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.SortType;
@@ -20,9 +21,6 @@ import edu.kit.iti.formal.psdbg.parser.ast.Signature;
 import edu.kit.iti.formal.psdbg.parser.data.Value;
 import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
 import edu.kit.iti.formal.psdbg.parser.types.TermType;
-import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
-import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
-import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
 import lombok.Getter;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -170,14 +168,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
     }
 
     @Override
-    public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState,
-                                             String data,
-                                             Signature sig) {
-        //System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
+    public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String pattern, Signature sig) {
+        KeyMatcherFacade kmf = new KeyMatcherFacade(currentState.getData().getEnv(), currentState.getData().getNode().sequent());
+        //System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + pattern);
         //System.out.println("Signature " + sig.toString());
-
-        Matchings m = MatcherFacade.matches(data,
-                currentState.getData().getNode().sequent(), false, currentState.getData().getProof().getServices());
+         Matchings m = kmf.matches(pattern, sig);
 
         if (m.isEmpty()) {
             LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent());

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java

+package edu.kit.iti.formal.psdbg.interpreter.matcher;
+
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.parser.DefaultTermParser;
+import de.uka.ilkd.key.parser.ParserException;
+import edu.kit.iti.formal.psdbg.parser.ast.Signature;
+import lombok.Builder;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
+
+import java.io.Reader;
+import java.io.StringReader;
+import java.util.ArrayList;
+import java.util.List;
+
+@Builder
+public class KeyMatcherFacade {
+    private static Logger logger = LogManager.getLogger(KeyMatcherFacade.class);
+
+    private final DefaultTermParser dtp = new DefaultTermParser();
+    private final KeYEnvironment environment;
+    private final Sequent sequent;
+
+    public Matchings matches(String pattern, Signature sig) {
+        if(pattern.contains("==>")) {
+            return matchesSequent(pattern, sig);
+        } else {
+            return matchesTerm(pattern, sig);
+        }
+
+    }
+
+    private Matchings matchesTerm(String pattern, Signature sig) {
+        List<Term> positions = new ArrayList<>();
+        for (String patternTerm : hasToplevelComma(pattern)) {
+            try {
+               Term t = dtp.parse(createReader(patternTerm), null, environment.getServices(), environment.getServices().getNamespaces(), null, true);
+               positions.add(t);
+            } catch (ParserException e) {
+                e.printStackTrace();
+            }
+        }
+
+        KeyTermMatcher keyTermMatcher = new KeyTermMatcher();
+        return keyTermMatcher.matchesToplevel(sequent, positions);
+    }
+
+
+    static List<String> hasToplevelComma(String pattern) {
+        ArrayList<String> rt = new ArrayList<>();
+        char[] c = pattern.toCharArray();
+        int level = 0;
+        int lastPosition = 0;
+        for (int i = 0; i < c.length; i++) {
+            if(c[i]==',' && level==0){
+                rt.add(pattern.substring(lastPosition, i));
+                lastPosition=i;
+            }
+            if(c[i]=='(' || c[i]=='{')
+                level++;
+            if(c[i]==')' || c[i]=='}')
+                level--;
+        }
+        if(rt.isEmpty())
+            rt.add(pattern);
+        return rt;
+    }
+
+    private Matchings matchesSequent(String pattern, Signature sig) {
+
+        Sequent seq = null;
+        try {
+            seq = dtp.parseSeq(createReader(pattern), environment.getServices(), environment.getServices().getNamespaces(), null,true);
+        } catch (ParserException e) {
+            e.printStackTrace();
+        }
+        KeyTermMatcher keyTermMatcher = new KeyTermMatcher();
+        return keyTermMatcher.matchesSequent(sequent, seq);
+    }
+
+    private Reader createReader(String pattern) {
+        StringReader sr = new StringReader(pattern);
+        return sr;
+    }
+}

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermBaseVisitor.java

+package edu.kit.iti.formal.psdbg.interpreter.matcher;
+
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.op.Operator;
+import de.uka.ilkd.key.logic.op.SchemaVariable;
+
+import javax.xml.validation.Schema;
+import java.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
+import java.util.HashMap;
+import java.util.Map;
+
+public abstract class KeyTermBaseVisitor<T,S> {
+    private Map<Class<?>, TermAcceptor<T,S>> dispatchMap = new HashMap<>();
+
+    public KeyTermBaseVisitor() {
+        populateMap();
+    }
+
+    protected void populateMap() {
+        Class me = getClass();
+        for (Method m: me.getMethods()) {
+            DispatchOn anno = m.getAnnotation(DispatchOn.class);
+            if(anno!=null){
+                dispatchMap.put(anno.value(),
+                        (term,arg) -> (T) m.invoke(this, term,arg));
+            }
+        }
+    }
+
+    public T visit(Term term, S arg) {
+        Class<? extends Operator> opClazz = term.op().getClass();
+        if(!dispatchMap.containsKey(opClazz)) {
+            return defaultVisit(term, arg);
+        }
+        try {
+            return dispatchMap.get(opClazz).visit(term, arg);
+        } catch (InvocationTargetException | IllegalAccessException e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    protected T defaultVisit(Term term, S arg) {
+        throw new RuntimeException("Visiting of " +term.getClass() + " not handled by visitor: "
+                + getClass().getSimpleName());
+    }
+
+    interface TermAcceptor<T, S> {
+        T visit(Term term, S arg) throws InvocationTargetException, IllegalAccessException;
+    }
+}

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java

+package edu.kit.iti.formal.psdbg.interpreter.matcher;
+
+import com.google.common.collect.Sets;
+import de.uka.ilkd.key.logic.*;
+import de.uka.ilkd.key.logic.op.*;
+import org.antlr.v4.runtime.Token;
+
+import java.util.*;
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+import java.util.stream.Stream;
+
+public class KeyTermMatcher extends  KeyTermBaseVisitor<Matchings, MatchPath> {
+    static final Matchings NO_MATCH = new Matchings();
+
+    static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
+
+    static final Map<String, MatchPath> EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first();
+
+    private String randomName;
+
+    MatchPath peek;
+
+    private List<Integer> currentposition = new ArrayList<>();
+
+    private boolean catchAll = false;
+
+    public Matchings matchesToplevel(Sequent sequent, List<Term> patternTerms) {
+        MatchPath.MPSequent seq = MatchPathFacade.create(sequent);
+
+        Matchings ret = new Matchings();
+        Matchings antecMatches = matchesSemisequent(MatchPathFacade.createAntecedent(seq), patternTerms);
+        Matchings succMatches = matchesSemisequent(MatchPathFacade.createSuccedent(seq), patternTerms);
+
+        //if(!antecMatches.equals(EMPTY_MATCH))
+        ret.addAll(antecMatches);
+        //if(!succMatches.equals(EMPTY_MATCH))
+        ret.addAll(succMatches);
+        return ret;
+    }
+
+
+    public Matchings matchesSequent(Sequent sequent, Sequent pattern) {
+        MatchPath.MPSequent mps = MatchPathFacade.create(sequent);
+//        MatchPath.MPSequent mps = new MatchPath.MPSequent(sequent);
+
+        Matchings ms = matchesSemisequent(
+                // new MatchPath.MPSemiSequent(mps, sequent.succedent(), false),
+                MatchPathFacade.createSuccedent(mps),
+                pattern.succedent());
+
+        //peek = new MatchPath.MPSemiSequent(mps, sequent.succedent(), true);
+
+        Matchings ma = matchesSemisequent(
+                MatchPathFacade.createAntecedent(mps),
+//                new MatchPath.MPSemiSequent(mps, sequent.antecedent(), true),
+                pattern.antecedent());
+
+        return reduceConform(ms, ma);
+    }
+
+    private Matchings matchesSemisequent(MatchPath.MPSemiSequent peek, Semisequent pattern) {
+        List<Term> patterns = pattern.asList().stream().map(SequentFormula::formula).collect(Collectors.toList());
+        return matchesSemisequent(peek, patterns);
+
+    }
+
+
+    private Matchings matchesSemisequent(MatchPath.MPSemiSequent peek, List<Term> patterns) {
+
+        Semisequent semiSeq = peek.getUnit();
+        if (semiSeq.isEmpty()) {
+            return patterns.isEmpty()
+                    ? EMPTY_MATCH
+                    : NO_MATCH;
+        }
+        HashMap<Term, Map<SequentFormula, Matchings>> map = new HashMap<>();
+        List<MatchPath.MPSequentFormula> sequentFormulas =
+                IntStream.range(0, semiSeq.size())
+                        .mapToObj(pos -> MatchPathFacade.create(peek, pos))
+                        .collect(Collectors.toList());
+
+        //cartesic product of pattern and top-level terms
+        for (Term subPatternTerm : patterns) {
+            map.put(subPatternTerm, new HashMap<>());
+            for (MatchPath.MPSequentFormula sf : sequentFormulas) {
+                Matchings temp = visit(subPatternTerm, MatchPathFacade.create(sf));
+                if (!temp.equals(NO_MATCH))
+                    map.get(subPatternTerm).put(sf.getUnit(), temp);
+            }
+        }
+
+        List<Matchings> matchings = new ArrayList<>();
+        reduceDisjoint(map, patterns, matchings);
+        Matchings ret = new Matchings();
+        //.filter(x -> !x.equals(EMPTY_MATCH))
+        matchings.forEach(ret::addAll);
+        return ret;
+    }
+
+    /*  private MatchPath.MPTerm create(MatchPath.MPSequentFormula sf) {
+          return new MatchPath.MPTerm(sf, sf.getUnit().formula(), MatchPath.SEQUENT_FORMULA_ROOT);
+      }
+
+      private MatchPath.MPSequentFormula create(MatchPath.MPSemiSequent peek, int pos) {
+          return new MatchPath.MPSequentFormula(peek, peek.getUnit().get(pos), pos);
+      }
+  */
+
+    /**
+     * Visit a '...'MatchPath'...' structure
+     * @param pattern
+     * @param subject
+     * @return
+     */
+    @DispatchOn(EllipsisOp.class)
+    public Matchings visitEllipsisOp(Term pattern, MatchPath subject) {
+        Matchings matchings = new Matchings();
+        subTerms((MatchPath.MPTerm) peek).forEach(sub -> {
+            Matchings s = visit(pattern.sub(0), sub);
+            matchings.addAll(s);
+        });
+        return matchings;
+    }
+
+
+    /**
+     * Visit a MatchIdentifierOP e.g., ?X or ?
+     * @param pattern
+     * @param subject
+     * @return
+     */
+    @DispatchOn(MatchIdentifierOp.class)
+    public Matchings visitMatchIdentifierOp(Term pattern, MatchPath subject) {
+        if(subject != null) {
+            String name = pattern.op().name().toString();
+            if (name.equalsIgnoreCase("?")) {
+                name = getRandomName();
+            }
+            Matchings mSingleton = Matchings.singleton(name, subject);
+            return mSingleton;
+        } else {
+            return NO_MATCH;
+        }
+
+    }
+
+
+    @DispatchOn(Quantifier.class)
+    public Matchings visitQuantifier(Term pattern, MatchPath subject) {
+        Term toMatch = (Term) subject.getUnit();
+        if (!toMatch.op().equals(pattern.op())) {
+            return NO_MATCH;
+        }
+        if (toMatch.boundVars().size() != pattern.boundVars().size()) {
+            return NO_MATCH;
+        }
+
+        Matchings match = EMPTY_MATCH;
+
+     /*   for (int i = 0; i < pattern.boundVars().size(); i++) {
+
+            QuantifiableVariable qfPattern = pattern.boundVars().get(i);
+            QuantifiableVariable qv = toMatch.boundVars().get(i);
+
+           if (qfPattern.getType() == MatchPatternLexer.DONTCARE) {
+                //match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
+                match = reduceConform(match, EMPTY_MATCH);
+                continue;
+            }
+            if (qfPattern.getType() == MatchPatternLexer.SID) {
+                TermFactory tf = new TermFactory(new HashMap<>());
+                TermBuilder tb = new TermBuilder(tf, services);
+                Term termQVariable = tb.var(qv);
+
+                match = reduceConform(match, Matchings.singleton(qfPattern.getText(),
+                        new MatchPath.MPTerm(peek, termQVariable, -i)));
+            } else {
+                if (!qv.name().toString().equals(qfPattern.getText())) {
+                    return NO_MATCH;
+                }
+                match = reduceConform(match, EMPTY_MATCH);
+            }
+        }
+
+
+        Matchings fromTerm = accept(ctx.skope, create(peek, 0));
+        Matchings retM = reduceConform(fromTerm, match);
+        retM.forEach(stringMatchPathMap -> {
+            stringMatchPathMap.forEach((s, matchPath) -> {
+                        if (matchPath instanceof MatchPath.MPQuantifiableVariable) {
+
+                            //create term from variablename and put instead into map
+                        }
+                    }
+
+            );
+        });
+        return handleBindClause(ctx.bindClause(), peek, retM);
+
+      /*  // Decision: Order of bounded vars
+        Matchings mm = new Matchings();
+        if (term.getUnit().boundVars().size() != pattern.boundVars().size()) {
+            return NO_MATCH;
+        }
+
+        Map<String, MatchPath> mPaths = new HashMap<>();
+        mm.add(mPaths);
+
+        for (int i = 0; i < term.getUnit().boundVars().size(); i++) {
+            QuantifiableVariable bv = term.getUnit().boundVars().get(i);
+            QuantifiableVariable pv = pattern.boundVars().get(i);
+
+            if (pv instanceof MatchIdentifierOp) {
+                //Namensbehandlung
+                String name;
+                if (pv.name().toString().equalsIgnoreCase("?")) {
+                    name = getRandomName();
+                } else {
+                    name = getBindingName(pv.name());
+                }
+
+                mPaths.put(name, term);
+            } else if (!pv.equals(bv)) {
+                return NO_MATCH;
+            }
+        }
+        return mm;*/
+      return null;
+
+    }
+
+    @DispatchOn(MatchBinderOp.class)
+    public Matchings visitMatchBinderOp(Term pattern, MatchPath subject) {
+        Matchings matchings = visit(pattern.sub(1), subject);
+        if (matchings != NO_MATCH) {
+            String name = pattern.sub(0).op().name().toString();
+            for (Map<String, MatchPath> a : matchings) {
+                a.put(name, peek);
+            }
+        }
+        return matchings;
+    }
+
+
+
+    @Override
+    protected Matchings defaultVisit(Term pattern, MatchPath subject1) {
+        Matchings m = new Matchings();
+        MatchPath<Term, Object> subject = (MatchPath<Term, Object>) subject1;
+        if (subject.getUnit().subs().size() != pattern.subs().size()) {
+            return NO_MATCH;
+        }
+
+        for (int i = 0; i < subject.getUnit().subs().size(); i++) {
+            Term tt = subject.getUnit().sub(i);
+            Term pt = pattern.sub(i);
+            Matchings msub = visit(pt, MatchPathFacade.create(subject, i));
+
+            if (msub.equals(NO_MATCH)) {
+                return NO_MATCH;
+            }
+            m = reduceConform(m, msub);
+        }
+
+        return m;
+    }
+
+    //region helper
+    private String getBindingName(Name name) {
+        if (name.toString().equals("?"))
+            return getRandomName();
+        return name.toString();
+    }
+
+    public String getRandomName() {
+        return randomName;
+    }
+
+    private Stream<MatchPath.MPTerm> subTerms(MatchPath.MPTerm peek) {
+        ArrayList<MatchPath.MPTerm> list = new ArrayList<>();
+        subTerms(list, peek);
+        return list.stream();
+    }
+
+    private void subTerms(ArrayList<MatchPath.MPTerm> list, MatchPath.MPTerm peek) {
+        list.add(peek);
+        for (int i = 0; i < peek.getUnit().arity(); i++) {
+            subTerms(list, MatchPathFacade.create(peek, i));
+        }
+    }
+    //endregion
+
+    //region Reductions
+
+
+    /**
+     * Reduce the matchings by eliminating non-compatible matchings.
+     * For example:
+     * m1: <X, f(y)>, <Y,g> and m2: <X, g> <Y, f(x)>
+     *
+     * @param m1
+     * @param m2
+     * @return
+     */