Skip to content

GitLab

Commit eef68b1a authored by Alexander Weigl's avatar Alexander Weigl
Browse files
Options

make MatchPath return PosInOccurrence 

* but PositionTable is incompatible
parent 2bb44850
Pipeline #13112 failed with stage
    in 2 minutes and 55 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 318 additions and 191 deletions
    src/main/java/edu/kit/formal/psdb/gui/controls/SequentView.java
    View file @ eef68b1a
    ......@@ -2,13 +2,14 @@ package edu.kit.formal.psdb.gui.controls;
    import de.uka.ilkd.key.java.Services;
    import de.uka.ilkd.key.logic.NamespaceSet;
    import de.uka.ilkd.key.logic.PosInOccurrence;
    import de.uka.ilkd.key.logic.Sequent;
    import de.uka.ilkd.key.pp.*;
    import de.uka.ilkd.key.proof.Goal;
    import de.uka.ilkd.key.proof.Node;
    import de.uka.ilkd.key.settings.ProofIndependentSettings;
    import edu.kit.formal.psdb.interpreter.KeYProofFacade;
    import edu.kit.formal.psdb.termmatcher.MatchPath;
    import edu.kit.formal.psdb.termmatcher.mp.MatchPath;
    import edu.kit.formal.psdb.termmatcher.MatcherFacade;
    import edu.kit.formal.psdb.termmatcher.Matchings;
    import javafx.beans.Observable;
    ......@@ -21,6 +22,7 @@ import javafx.scene.paint.Color;
    import org.fxmisc.richtext.CharacterHit;
    import org.fxmisc.richtext.CodeArea;
    import org.key_project.util.collection.ImmutableList;
    import org.key_project.util.collection.ImmutableSLList;
    import java.io.StringWriter;
    import java.util.Collections;
    ......@@ -193,19 +195,22 @@ public class SequentView extends CodeArea {
    if (node.get().sequent() != null) {
    Matchings m = MatcherFacade.matches(pattern, node.get().sequent(), true);
    if (m.size() == 0) return false;
    for (Map<String, MatchPath> va : m) {
    MatchPath<?> complete = va.get("?COMPLETE");
    highlightTerm(complete.getPos());
    Map<String, MatchPath> va = m.first();
    System.out.println(va);//TODO remove
    for (MatchPath mp : va.values()) {
    System.out.println(mp.pio());
    highlightTerm(mp.pio());
    }
    }
    return true;
    }
    private void highlightTerm(ImmutableList<Integer> complete) {
    private void highlightTerm(PosInOccurrence complete) {
    if (backend == null) {
    return;
    }
    Range r = backend.getInitialPositionTable().rangeForPath(complete);
    ImmutableList<Integer> path = ImmutableSLList.singleton(1);
    Range r = backend.getInitialPositionTable().rangeForPath(path);
    setStyle(r.start(), r.end(), Collections.singleton("search-highlight"));
    }
    }
    src/main/java/edu/kit/formal/psdb/gui/controls/Utils.java
    View file @ eef68b1a
    ......@@ -122,10 +122,13 @@ public class Utils {
    private Utils() {
    }
    public static String getRandomName(String suffx) {
    return getRandomName() + suffx;
    }
    public static String getRandomName() {
    Random r = new Random();
    return (ADJECTIVES[r.nextInt(ADJECTIVES.length)] + "_" + ANIMALS[r.nextInt(ANIMALS.length)] + ".kps").toLowerCase();
    return (ADJECTIVES[r.nextInt(ADJECTIVES.length)] + "_" + ANIMALS[r.nextInt(ANIMALS.length)]).toLowerCase();
    }
    public static void createWithFXML(Object node) {
    ......
    src/main/java/edu/kit/formal/psdb/termmatcher/MatchPath.java deleted 100644 → 0
    View file @ 2bb44850
    package edu.kit.formal.psdb.termmatcher;
    import de.uka.ilkd.key.logic.Semisequent;
    import de.uka.ilkd.key.logic.Sequent;
    import de.uka.ilkd.key.logic.Term;
    import lombok.Data;
    import lombok.EqualsAndHashCode;
    import org.key_project.util.collection.ImmutableList;
    import org.key_project.util.collection.ImmutableSLList;
    /**
    * @author Alexander Weigl
    * @version 1 (24.08.17)
    */
    @Data
    @EqualsAndHashCode(of = {"term"})
    public abstract class MatchPath<T> {
    public static final int ROOT = -1;
    public static final int POSITION_ANTECEDENT = -2;
    public static final int POSITION_SUCCEDENT = -3;
    private final MatchPath<?> parent;
    private final T term;
    private final int posInParent;
    public MatchPath(MatchPath<?> parent, T unit, int pos) {
    posInParent = pos;
    term = unit;
    this.parent = parent;
    }
    public static MatchPath<Term> createTermPath(MatchPath<Term> path, int i) {
    return new MatchPathTerm(path, path.getTerm().sub(i), i);
    }
    public ImmutableList<Integer> getPos() {
    if (parent == null) {
    return ImmutableSLList.singleton(posInParent);
    } else {
    return parent.getPos().append(posInParent);
    }
    }
    public static MatchPath<Term> createRoot(Term keyTerm) {
    return new MatchPathTerm(null, keyTerm, -1);
    }
    public String toString() {
    return term.toString();
    }
    public static MatchPathSemiSequent createSemiSequent(Sequent s, boolean antec) {
    MatchPathSemiSequent mp = new MatchPathSemiSequent(
    createSequent(s), antec ? s.antecedent() : s.succedent(), antec);
    return mp;
    }
    private static MatchPathSequent createSequent(Sequent s) {
    return new MatchPathSequent(s);
    }
    public static MatchPathSemiSequent createSuccedent(Sequent sequent) {
    return createSemiSequent(sequent, false);
    }
    public static MatchPathSemiSequent createAntecedent(Sequent sequent) {
    return createSemiSequent(sequent, true);
    }
    public abstract int depth();
    public static class MatchPathTerm extends MatchPath<Term> {
    public MatchPathTerm(MatchPath<?> parent, Term unit, int pos) {
    super(parent, unit, pos);
    }
    @Override
    public int depth() {
    return getTerm().depth();
    }
    }
    public static class MatchPathSequent extends MatchPath<Sequent> {
    public MatchPathSequent(Sequent unit) {
    super(null, unit, ROOT);
    }
    @Override
    public int depth() {
    return 0;
    }
    }
    public static class MatchPathSemiSequent extends MatchPath<Semisequent> {
    public MatchPathSemiSequent(MatchPathSequent parent, Semisequent unit, boolean antec) {
    super(parent, unit, antec ? POSITION_ANTECEDENT : POSITION_SUCCEDENT);
    }
    @Override
    public int depth() {
    return 1;
    }
    }
    }
    src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java
    View file @ eef68b1a
    ......@@ -4,9 +4,12 @@ import de.uka.ilkd.key.logic.Semisequent;
    import de.uka.ilkd.key.logic.Sequent;
    import de.uka.ilkd.key.logic.Term;
    import edu.kit.formal.psdb.termmatcher.MatchPatternParser.SemiSeqPatternContext;
    import edu.kit.formal.psdb.termmatcher.mp.MatchPathFacade;
    import org.antlr.v4.runtime.CharStream;
    import org.antlr.v4.runtime.CharStreams;
    import org.antlr.v4.runtime.CommonTokenStream;
    import org.apache.logging.log4j.LogManager;
    import org.apache.logging.log4j.Logger;
    import static edu.kit.formal.psdb.termmatcher.MatchPatternParser.SequentPatternContext;
    import static edu.kit.formal.psdb.termmatcher.MatchPatternParser.TermPatternContext;
    ......@@ -18,12 +21,14 @@ import static edu.kit.formal.psdb.termmatcher.MatchPatternParser.TermPatternCont
    * @author S.Grebing
    */
    public class MatcherFacade {
    private static Logger logger = LogManager.getLogger(MatcherFacade.class);
    public static Matchings matches(String pattern, Term keyTerm) {
    MatcherImpl matcher = new MatcherImpl();
    matcher.setCatchAll(false);
    MatchPatternParser mpp = getParser(pattern);
    TermPatternContext ctx = mpp.termPattern();
    return matcher.accept(ctx, MatchPath.createRoot(keyTerm));
    return matcher.accept(ctx, MatchPathFacade.createRoot(keyTerm));
    }
    ......@@ -44,8 +49,8 @@ public class MatcherFacade {
    /**
    * Match a semisequent against a sequent
    *
    * @param pattern Semisequent pattern e.g. f(x), f(x)
    * @param semiSeq Concrete KeY Semisequent
    * @param pattern Semisequent pattern e.g. f(x), f(x)
    * @param semiSeq Concrete KeY Semisequent
    * @param catchAll
    * @return Matchings
    */
    ......@@ -54,7 +59,7 @@ public class MatcherFacade {
    SemiSeqPatternContext ctx = mpp.semiSeqPattern();
    MatcherImpl matcher = new MatcherImpl();
    matcher.setCatchAll(catchAll);
    Matchings m = matcher.accept(ctx, new MatchPath.MatchPathSemiSequent(null, semiSeq, true));
    Matchings m = matcher.accept(ctx, MatchPathFacade.createRoot(semiSeq));
    return m;
    }
    ......@@ -69,9 +74,14 @@ public class MatcherFacade {
    public static Matchings matches(String pattern, Sequent sequent, boolean catchAll) {
    MatchPatternParser mpp = getParser(pattern);
    SequentPatternContext ctx = mpp.sequentPattern();
    if (mpp.getNumberOfSyntaxErrors() != 0) {
    logger.info("Invalid pattern syntax '{}' no matches returned.", pattern);
    return new Matchings();
    }
    MatcherImpl matcher = new MatcherImpl();
    matcher.setCatchAll(catchAll);
    Matchings m = matcher.accept(ctx, new MatchPath.MatchPathSequent(sequent));
    Matchings m = matcher.accept(ctx, MatchPathFacade.create(sequent));
    return m;
    }
    ......@@ -84,6 +94,6 @@ public class MatcherFacade {
    * @return
    */
    public static Matchings matches(String pattern, Sequent sequent) {
    return matches(pattern, sequent,false);
    return matches(pattern, sequent, false);
    }
    }
    src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java
    View file @ eef68b1a
    ......@@ -2,20 +2,22 @@ package edu.kit.formal.psdb.termmatcher;
    import com.google.common.collect.Sets;
    import de.uka.ilkd.key.logic.Semisequent;
    import de.uka.ilkd.key.logic.Sequent;
    import de.uka.ilkd.key.logic.SequentFormula;
    import de.uka.ilkd.key.logic.Term;
    import edu.kit.formal.psdb.gui.controls.Utils;
    import edu.kit.formal.psdb.termmatcher.mp.MatchPath;
    import lombok.Getter;
    import lombok.Setter;
    import org.antlr.v4.runtime.CommonToken;
    import org.key_project.util.collection.ImmutableArray;
    import org.key_project.util.collection.ImmutableList;
    import java.util.*;
    import java.util.stream.Collectors;
    import java.util.stream.IntStream;
    import java.util.stream.Stream;
    import static edu.kit.formal.psdb.termmatcher.mp.MatchPathFacade.*;
    /**
    * Matchpattern visitor visits the matchpatterns of case-statements
    *
    ......@@ -27,18 +29,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
    static final Map<String, MatchPath> EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first();
    private List<Integer> currentPosition = new ArrayList<>();
    /**
    * If true, we assume every term in the pattern has a binder.
    * The binding names are generated.
    *
    * @see #handleBindClause(MatchPatternParser.BindClauseContext, MatchPath, Matchings)
    */
    @Getter
    @Setter
    private boolean catchAll = false;
    /*
    * Reduce two matchinfos
    ......@@ -71,6 +61,16 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    return oneMatch ? res : null;
    }
    */
    private List<Integer> currentPosition = new ArrayList<>();
    /**
    * If true, we assume every term in the pattern has a binder.
    * The binding names are generated.
    *
    * @see #handleBindClause(MatchPatternParser.BindClauseContext, MatchPath, Matchings)
    */
    @Getter
    @Setter
    private boolean catchAll = false;
    private static HashMap<String, MatchPath> reduceConform(Map<String, MatchPath> h1, Map<String, MatchPath> h2) {
    ......@@ -86,7 +86,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    return h3;
    }
    /**
    * Reduce the matchings by eliminating non-compatible matchings.
    * For example:
    ......@@ -117,6 +116,35 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    return oneMatch ? m3 : NO_MATCH;
    }
    /**
    * Transform a number term into an int value.
    * <p>
    * i.e. Z(1(2(3(#)))) ==> 123
    *
    * @param zTerm
    * @return
    */
    public static int transformToNumber(Term zTerm) {
    List<Integer> integ = MatcherImpl.transformHelper(new ArrayList<>(), zTerm);
    int dec = 10;
    int output = integ.get(0);
    for (int i = 1; i < integ.size(); i++) {
    Integer integer = integ.get(i);
    output += integer * dec;
    dec = dec * 10;
    }
    return output;
    }
    private static List<Integer> transformHelper(List<Integer> l, Term sub) {
    if (sub.op().name().toString().equals("#")) {
    return l;
    } else {
    l.add(Integer.parseUnsignedInt(sub.op().name().toString()));
    return transformHelper(l, sub.sub(0));
    }
    }
    /**
    * Visit '_'
    *
    ......@@ -159,14 +187,13 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    @Override
    protected Matchings visitAnywhere(MatchPatternParser.AnywhereContext ctx, MatchPath peek) {
    Matchings m = new Matchings();
    subTerms(peek).forEach(sub -> {
    subTerms((MatchPath.MPTerm) peek).forEach(sub -> {
    Matchings s = accept(ctx.termPattern(), sub);
    m.addAll(s);
    });
    return m;
    }
    /**
    * Visit a function and predicate symbol without a sequent arrow
    *
    ......@@ -178,14 +205,13 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    protected Matchings visitFunction(MatchPatternParser.FunctionContext ctx, MatchPath path) {
    //System.out.format("Match: %25s with %s %n", peek, ctx.toInfoString(new MatchPatternParser(null)));
    String expectedFunction = ctx.func.getText();
    Term peek = ((MatchPath<Term>) path).getTerm();
    Term peek = ((MatchPath.MPTerm) path).getUnit();
    if (peek.op().name().toString().equals(expectedFunction) // same name
    && ctx.termPattern().size() == peek.arity() // same arity
    ) {
    Matchings m = IntStream.range(0, peek.arity())
    .mapToObj(i -> (Matchings)
    accept(ctx.termPattern(i),
    MatchPath.createTermPath(path, i)))
    accept(ctx.termPattern(i), create(path, i)))
    .reduce(MatcherImpl::reduceConform)
    .orElse(EMPTY_MATCH);
    return handleBindClause(ctx.bindClause(), path, m);
    ......@@ -217,39 +243,10 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    return this.reduceConform(m, mNew);
    }
    /**
    * Transform a number term into an int value.
    * <p>
    * i.e. Z(1(2(3(#)))) ==> 123
    *
    * @param zTerm
    * @return
    */
    public static int transformToNumber(Term zTerm) {
    List<Integer> integ = MatcherImpl.transformHelper(new ArrayList<>(), zTerm);
    int dec = 10;
    int output = integ.get(0);
    for (int i = 1; i < integ.size(); i++) {
    Integer integer = integ.get(i);
    output += integer * dec;
    dec = dec * 10;
    }
    return output;
    }
    private static List<Integer> transformHelper(List<Integer> l, Term sub) {
    if (sub.op().name().toString().equals("#")) {
    return l;
    } else {
    l.add(Integer.parseUnsignedInt(sub.op().name().toString()));
    return transformHelper(l, sub.sub(0));
    }
    }
    @Override
    protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, MatchPath path) {
    //we are at a number
    Term peek = ((MatchPath<Term>) path).getTerm();
    Term peek = ((MatchPath.MPTerm) path).getUnit();
    if (peek.op().name().toString().equals("Z")) {
    ImmutableArray<Term> subs = peek.subs();
    int transformedString = transformToNumber(peek.sub(0));
    ......@@ -274,13 +271,12 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    */
    @Override
    public Matchings visitSequentAnywhere(MatchPatternParser.SequentAnywhereContext ctx, MatchPath peek) {
    MatchPath<Sequent> seq = peek;
    Sequent sequent = seq.getTerm();
    MatchPath.MPSequent seq = (MatchPath.MPSequent) peek;
    MatchPatternParser.SemiSeqPatternContext patternCtx = ctx.anywhere;
    Matchings ret = new Matchings();
    Matchings antecMatches = accept(patternCtx, MatchPath.createAntecedent(sequent));
    Matchings succMatches = accept(patternCtx, MatchPath.createSuccedent(sequent));
    Matchings antecMatches = accept(patternCtx, createAntecedent(seq));
    Matchings succMatches = accept(patternCtx, createSuccedent(seq));
    //if(!antecMatches.equals(EMPTY_MATCH))
    ret.addAll(antecMatches);
    ......@@ -295,16 +291,15 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    @Override
    public Matchings visitSequentArrow(MatchPatternParser.SequentArrowContext ctx, MatchPath peek) {
    MatchPath<Sequent> seq = peek;
    Sequent sequent = seq.getTerm();
    MatchPath.MPSequent seq = (MatchPath.MPSequent) peek;
    //NPE
    Matchings mAntec = ctx.antec != null
    ? accept(ctx.antec, MatchPath.createSemiSequent(sequent, true))
    ? accept(ctx.antec, createAntecedent(seq))
    : EMPTY_MATCH;
    Matchings mSucc = ctx.succ != null
    ? accept(ctx.succ, MatchPath.createSemiSequent(sequent, false))
    ? accept(ctx.succ, createSuccedent(seq))
    : EMPTY_MATCH;
    return MatcherImpl.reduceConform(mAntec, mSucc);
    ......@@ -319,14 +314,19 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    */
    @Override
    protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, MatchPath peek) {
    Semisequent ss = (Semisequent) peek.getTerm();
    MatchPath.MPSemiSequent sseq = (MatchPath.MPSemiSequent) peek;
    Semisequent ss = (Semisequent) peek.getUnit();
    if (ss.isEmpty()) {
    return ctx.termPattern().size() == 0
    ? EMPTY_MATCH
    : NO_MATCH;
    }
    ImmutableList<SequentFormula> allSequentFormulas = ss.asList();
    List<MatchPath.MPSequentFormula> sequentFormulas =
    IntStream.range(0, ss.size())
    .mapToObj(pos -> create(sseq, pos))
    .collect(Collectors.toList());
    List<MatchPatternParser.TermPatternContext> patterns = ctx.termPattern();
    HashMap<MatchPatternParser.TermPatternContext, Map<SequentFormula, Matchings>>
    ......@@ -334,22 +334,20 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    //cartesic product of pattern and top-level terms
    for (MatchPatternParser.TermPatternContext tctx : patterns) {
    int i = 0;
    map.put(tctx, new HashMap<>());
    for (SequentFormula form : allSequentFormulas) {
    Matchings temp = accept(tctx, new MatchPath.MatchPathTerm(peek, form.formula(), i++));
    for (MatchPath.MPSequentFormula sf : sequentFormulas) {
    Matchings temp = accept(tctx, create(sf));
    if (!temp.equals(NO_MATCH))
    map.get(tctx).put(form, temp);
    map.get(tctx).put(sf.getUnit(), temp);
    }
    }
    List<Matchings> matchings = new ArrayList<>();
    reduceDisjoint(map, patterns, matchings);
    Matchings ret = new Matchings();
    matchings.stream()//.filter(x -> !x.equals(EMPTY_MATCH))
    .forEach(ret::addAll);
    //.filter(x -> !x.equals(EMPTY_MATCH))
    matchings.forEach(ret::addAll);
    return ret;
    }
    /**
    ......@@ -524,17 +522,16 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
    return visitBinaryOperation("eq", ctx.termPattern(0), ctx.termPattern(1), peek);
    }
    private Stream<MatchPath<Term>> subTerms(MatchPath peek) {
    ArrayList<MatchPath<Term>> list = new ArrayList<>();
    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<Term>> list, MatchPath<Term> peek) {
    private void subTerms(ArrayList<MatchPath.MPTerm> list, MatchPath.MPTerm peek) {
    list.add(peek);
    for (int i = 0; i < peek.getTerm().arity(); i++) {
    subTerms(list,
    MatchPath.createTermPath(peek, i));
    for (int i = 0; i < peek.getUnit().arity(); i++) {
    subTerms(list, create(peek, i));
    }
    }
    ......
    src/main/java/edu/kit/formal/psdb/termmatcher/Matchings.java
    View file @ eef68b1a
    package edu.kit.formal.psdb.termmatcher;
    import com.google.common.collect.Sets;
    import edu.kit.formal.psdb.termmatcher.mp.MatchPath;
    import java.util.*;
    ......
    src/main/java/edu/kit/formal/psdb/termmatcher/mp/MatchPath.java 0 → 100644
    View file @ eef68b1a
    package edu.kit.formal.psdb.termmatcher.mp;
    import de.uka.ilkd.key.logic.*;
    import lombok.Data;
    import lombok.EqualsAndHashCode;
    /**
    * @author Alexander Weigl
    * @version 1 (24.08.17)
    */
    @Data
    @EqualsAndHashCode(of = {"unit"})
    public abstract class MatchPath<T, P> {
    public static final int SEQUENT_FORMULA_ROOT = -1;
    public static final int POSITION_ANTECEDENT = -2;
    public static final int POSITION_SUCCEDENT = -3;
    private final MatchPath<? extends P, ?> parent;
    private final T unit;
    private final int posInParent;
    private MatchPath(MatchPath<? extends P, ?> parent, T unit, int pos) {
    posInParent = pos;
    this.unit = unit;
    this.parent = parent;
    }
    public abstract PosInOccurrence pio();
    public abstract Sequent getSequent();
    public abstract SequentFormula getSequentFormula();
    public abstract int depth();
    public String toString() {
    return unit.toString();
    }
    public static class MPTerm extends MatchPath<Term, Object> {
    MPTerm(MatchPath<? extends Object, ?> parent, Term unit, int pos) {
    super(parent, unit, pos);
    }
    @Override
    public PosInOccurrence pio() {