diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java index 5be9db8a69e49536ff5f49e32b6b194920874f9b..9171f9e610c79260b9820077e904046d8a79314a 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java @@ -95,7 +95,7 @@ public interface ASTTraversal extends Visitor { @Override default T visit(MatchExpression match) { match.getPattern().accept(this); - match.getSignature().accept(this); + //match.getSignature().accept(this); return null; } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java index 5135a4b7d6f91a162763a8f36a3d63907f75dfa6..92af40c1de8fb104a0499698f91709fcf732eb9b 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java @@ -123,7 +123,7 @@ public class PrettyPrinter extends DefaultASTVisitor { s.append("match "); String prefix = getWhitespacePrefix(); match.getPattern().accept(this); - if (!match.getSignature().isEmpty()) { + /*if (!match.getSignature().isEmpty()) { if (getCurrentLineLength() > maxWidth) { s.append("\n").append(prefix); @@ -134,7 +134,7 @@ public class PrettyPrinter extends DefaultASTVisitor { s.append("using ["); match.getSignature().accept(this); s.append("]"); - } + }*/ return null; } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java index d6ca9e350f6955f9185f94fa1462a2712da532ce..be8e65b15d00da0dcfcd66f52816ccc9f749371d 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java @@ -363,11 +363,11 @@ public class TransformAst implements ScriptLanguageVisitor { e.setParent(match); match.setDerivableTerm(e); } else { - if (ctx.argList() != null) { + /*if (ctx.argList() != null) { Signature signature = (Signature) ctx.argList().accept(this); match.setSignature(signature); signature.setParent(match); - } + }*/ Expression e = (Expression) ctx.pattern.accept(this); match.setPattern(e); e.setParent(match); diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java index 3581d5d97a2762389abd110411b14217176ad211..fe0981dbc0826f29ea381b157b4c40706f052caf 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java @@ -41,7 +41,7 @@ import lombok.Setter; */ @Data public class MatchExpression extends Expression { - private Signature signature = new Signature(); + //private Signature signature = new Signature(); private Expression pattern; @Getter @Setter @@ -64,8 +64,8 @@ public class MatchExpression extends Expression { private static final Logger LOGGER = LogManager.getLogger(KeYMatcher.class); - private static final Name CUT_TACLET_NAME = new Name("cut"); + private List resultsFromLabelMatch; @Getter @@ -89,6 +91,17 @@ public class KeYMatcher implements MatcherApi { } } + private static String cleanLabel(String label) { + + String cleaned = label.replaceAll(" ", ""); + cleaned = cleaned.replaceAll("\\(", "\\\\("); + cleaned = cleaned.replaceAll("\\)", "\\\\)"); + cleaned = cleaned.replaceAll("\\[", "\\\\["); + cleaned = cleaned.replaceAll("\\]", "\\\\]"); + + return cleaned; + } + /** * If teh label matcher was successful the list contains all match results * @@ -116,16 +129,15 @@ public class KeYMatcher implements MatcherApi { String branchLabel = currentState.getData().getBranchingLabel(); String cleanBranchLabel = branchLabel.replaceAll(" ", ""); - //cleanLabel(branchLabel); + //cleanLabel(branchLabel); - Pattern regexpForLabel = Pattern.compile("\\\\Q"+cleanLabel+"\\\\E"); + Pattern regexpForLabel = Pattern.compile("\\\\Q" + cleanLabel + "\\\\E"); Matcher branchLabelMatcher = regexpForLabel.matcher(Pattern.quote(cleanBranchLabel)); //Matcher branchLabelMatcher = regexpForLabel.matcher(cleanBranchLabel); - if (branchLabelMatcher.matches()) { VariableAssignment va = new VariableAssignment(null); va.declare("$$branchLabel_", SimpleType.STRING); @@ -166,7 +178,7 @@ public class KeYMatcher implements MatcherApi { // assignments.forEach(variableAssignment -> System.out.println(variableAssignment)); - return assignments.isEmpty()? null: assignments; + return assignments.isEmpty() ? null : assignments; } @Override @@ -174,13 +186,13 @@ public class KeYMatcher implements MatcherApi { 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 = kmf.matches(pattern, sig); + Matchings m = kmf.matches(pattern, sig); if (m.isNoMatch()) { LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent()); return Collections.emptyList(); } else { - Match firstMatch = m.getMatchings().iterator().next() ; + Match firstMatch = m.getMatchings().iterator().next(); VariableAssignment va = new VariableAssignment(null); for (String s : firstMatch.keySet()) { MatchPath matchPath = firstMatch.get(s); @@ -197,7 +209,7 @@ public class KeYMatcher implements MatcherApi { va.declare(s, value.getType()); va.assign(s, value); - } catch (ClassCastException e){ + } catch (ClassCastException e) { LogicVariable var = (LogicVariable) matchPath.getUnit(); String reprTerm = var.name().toString(); Value value = new Value<>( @@ -211,7 +223,7 @@ public class KeYMatcher implements MatcherApi { } - //LOGGER.info("Variables to match " + s + " : " + value); + //LOGGER.info("Variables to match " + s + " : " + value); //} } List retList = new LinkedList(); @@ -232,18 +244,6 @@ public class KeYMatcher implements MatcherApi { ); } - private String cleanLabel(String label) { - - String cleaned = label.replaceAll(" ", ""); - cleaned = cleaned.replaceAll("\\(", "\\\\("); - cleaned = cleaned.replaceAll("\\)", "\\\\)"); - cleaned = cleaned.replaceAll("\\[", "\\\\["); - cleaned = cleaned.replaceAll("\\]", "\\\\]"); - - - return cleaned; - } - //private TermLiteral from(SequentFormula sf) { // return new TermLiteral(sf.toString()); //} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java index c04ef22a2c147c4cfa2fe41c8a42b464718b6919..b04328c97035623f695b0f672bb0142b6797375d 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java @@ -43,7 +43,8 @@ public class KeyMatcherFacade { List positions = new ArrayList<>(); for (String patternTerm : hasToplevelComma(pattern)) { try { - Term t = dtp.parse(createReader(patternTerm), null, environment.getServices(), environment.getServices().getNamespaces(), null, true); + Term t = dtp.parse(createReader(patternTerm), null, environment.getServices(), + environment.getServices().getNamespaces(), null, true); positions.add(t); } catch (ParserException e) { e.printStackTrace();