Commit 2c4d4929 authored by Alexander Weigl's avatar Alexander Weigl

Removal of using clause in match expressions.

parent ef3ebf59
...@@ -59,10 +59,6 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> { ...@@ -59,10 +59,6 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
@Override @Override
public MatchExpression visit(MatchExpression match) { public MatchExpression visit(MatchExpression match) {
if (match.getSignature() != null)
match.setSignature((Signature)
match.getSignature().accept(this));
match.setPattern((Expression) match.getPattern().accept(this)); match.setPattern((Expression) match.getPattern().accept(this));
return match; return match;
} }
......
...@@ -22,9 +22,9 @@ public class NegatedMatchWithUsing extends AbstractLintRule { ...@@ -22,9 +22,9 @@ public class NegatedMatchWithUsing extends AbstractLintRule {
public Void visit(UnaryExpression ue) { public Void visit(UnaryExpression ue) {
if (ue.getExpression() instanceof MatchExpression) { if (ue.getExpression() instanceof MatchExpression) {
MatchExpression me = (MatchExpression) ue.getExpression(); MatchExpression me = (MatchExpression) ue.getExpression();
if (me.getSignature() != null && me.getSignature().size() > 0) { /*if (me.getSignature() != null && me.getSignature().size() > 0) {
problem(ISSUE, ue, me); problem(ISSUE, ue, me);
} }*/
} }
return super.visit(ue); return super.visit(ue);
} }
......
package edu.kit.iti.formal.psdbg.interpreter.functions; package edu.kit.iti.formal.psdbg.interpreter.functions;
import edu.kit.iti.formal.psdbg.interpreter.Evaluator; import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
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.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher;
import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException; import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.FunctionCall; import edu.kit.iti.formal.psdbg.parser.ast.FunctionCall;
import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression; import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression;
import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.ast.Variable; import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import edu.kit.iti.formal.psdbg.parser.data.Value; import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.function.ScriptFunction; import edu.kit.iti.formal.psdbg.parser.function.ScriptFunction;
...@@ -52,12 +51,11 @@ public class FindInSequence implements ScriptFunction { ...@@ -52,12 +51,11 @@ public class FindInSequence implements ScriptFunction {
Evaluator<KeyData> e = (Evaluator<KeyData>) val; Evaluator<KeyData> e = (Evaluator<KeyData>) val;
try { try {
MatchExpression match = (MatchExpression) call.getArguments().get(0); MatchExpression match = (MatchExpression) call.getArguments().get(0);
Signature sig = match.getSignature(); //Signature sig = match.getSignature();
Value pattern = e.eval(match.getPattern()); Value pattern = e.eval(match.getPattern());
KeYMatcher matcher = (KeYMatcher) e.getMatcher(); KeYMatcher matcher = (KeYMatcher) e.getMatcher();
if (TypeFacade.isTerm(pattern.getType())) { if (TypeFacade.isTerm(pattern.getType())) {
List<VariableAssignment> va = matcher.matchSeq(e.getGoal(), List<VariableAssignment> va = matcher.matchSeq(e.getGoal(), (String) pattern.getData());
(String) pattern.getData(), sig);
if (va.isEmpty()) { if (va.isEmpty()) {
throw new IllegalArgumentException("No match found for " + match.getPattern()); throw new IllegalArgumentException("No match found for " + match.getPattern());
} else { } else {
......
...@@ -182,11 +182,11 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -182,11 +182,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
} }
@Override @Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String pattern, Signature sig) { public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String pattern) {
KeyMatcherFacade kmf = new KeyMatcherFacade(currentState.getData().getEnv(), currentState.getData().getNode().sequent()); 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("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + pattern);
//System.out.println("Signature " + sig.toString()); //System.out.println("Signature " + sig.toString());
Matchings m = kmf.matches(pattern, sig); Matchings m = kmf.matches(pattern);
if (m.isNoMatch()) { if (m.isNoMatch()) {
LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent()); LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent());
......
...@@ -30,16 +30,16 @@ public class KeyMatcherFacade { ...@@ -30,16 +30,16 @@ public class KeyMatcherFacade {
private final Sequent sequent; private final Sequent sequent;
public Matchings matches(String pattern, Signature sig) { public Matchings matches(String pattern) {
if(pattern.contains("==>")) { if(pattern.contains("==>")) {
return matchesSequent(pattern, sig); return matchesSequent(pattern);
} else { } else {
return matchesTerm(pattern, sig); return matchesTerm(pattern);
} }
} }
private Matchings matchesTerm(String pattern, Signature sig) { private Matchings matchesTerm(String pattern) {
List<Term> positions = new ArrayList<>(); List<Term> positions = new ArrayList<>();
for (String patternTerm : hasToplevelComma(pattern)) { for (String patternTerm : hasToplevelComma(pattern)) {
try { try {
...@@ -76,7 +76,7 @@ public class KeyMatcherFacade { ...@@ -76,7 +76,7 @@ public class KeyMatcherFacade {
return rt; return rt;
} }
private Matchings matchesSequent(String pattern, Signature sig) { private Matchings matchesSequent(String pattern) {
Sequent seq = null; Sequent seq = null;
try { try {
......
...@@ -71,9 +71,6 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser ...@@ -71,9 +71,6 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
@Override @Override
public Value visit(MatchExpression match) { public Value visit(MatchExpression match) {
enterScope(match); enterScope(match);
if (match.getSignature() != null && !match.getSignature().isEmpty()) {
throw new IllegalStateException("not supported");
}
List<VariableAssignment> va = null; List<VariableAssignment> va = null;
Value pattern = (Value) match.getPattern().accept(this); Value pattern = (Value) match.getPattern().accept(this);
if (match.isDerivable()) { if (match.isDerivable()) {
...@@ -81,7 +78,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser ...@@ -81,7 +78,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
if (pattern.getType() == SimpleType.STRING) { if (pattern.getType() == SimpleType.STRING) {
va = matcher.matchLabel(goal, (String) pattern.getData()); va = matcher.matchLabel(goal, (String) pattern.getData());
} else if (TypeFacade.isTerm(pattern.getType())) { } else if (TypeFacade.isTerm(pattern.getType())) {
va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature()); va = matcher.matchSeq(goal, (String) pattern.getData());
} }
} }
......
...@@ -157,8 +157,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -157,8 +157,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
*/ */
@Override @Override
public List<VariableAssignment> visit(MatchExpression match) { public List<VariableAssignment> visit(MatchExpression match) {
//Signature sig = match.getSignature();
Signature sig = match.getSignature();
Value pattern = eval.eval(match.getPattern()); Value pattern = eval.eval(match.getPattern());
// Value pattern = (Value) match.getPattern().accept(this); // Value pattern = (Value) match.getPattern().accept(this);
...@@ -167,7 +166,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -167,7 +166,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
va = getMatcher().matchLabel(goal, (String) pattern.getData()); va = getMatcher().matchLabel(goal, (String) pattern.getData());
//TODO extract the results form the matcher in order to retrieve the selection results //TODO extract the results form the matcher in order to retrieve the selection results
} else if (TypeFacade.isTerm(pattern.getType())) { } else if (TypeFacade.isTerm(pattern.getType())) {
va = getMatcher().matchSeq(goal, (String) pattern.getData(), sig); va = getMatcher().matchSeq(goal, (String) pattern.getData());
// System.out.println("va = " + va); // System.out.println("va = " + va);
} }
return va != null ? va : Collections.emptyList(); return va != null ? va : Collections.emptyList();
......
...@@ -12,6 +12,6 @@ import java.util.List; ...@@ -12,6 +12,6 @@ import java.util.List;
*/ */
public interface MatcherApi<T> { public interface MatcherApi<T> {
List<VariableAssignment> matchLabel(GoalNode<T> currentState, String label); List<VariableAssignment> matchLabel(GoalNode<T> currentState, String label);
List<VariableAssignment> matchSeq(GoalNode<T> currentState, String data, Signature sig); List<VariableAssignment> matchSeq(GoalNode<T> currentState, String data);
} }
...@@ -25,19 +25,13 @@ public class PseudoMatcher implements MatcherApi<String> { ...@@ -25,19 +25,13 @@ public class PseudoMatcher implements MatcherApi<String> {
} }
@Override @Override
public List<VariableAssignment> matchSeq(GoalNode<String> currentState, String data, Signature sig) { public List<VariableAssignment> matchSeq(GoalNode<String> currentState, String data) {
Pattern p = Pattern.compile(data, Pattern.CASE_INSENSITIVE); Pattern p = Pattern.compile(data, Pattern.CASE_INSENSITIVE);
Matcher m = p.matcher(currentState.getData()); Matcher m = p.matcher(currentState.getData());
if (!m.matches()) if (!m.matches())
return Collections.emptyList(); return Collections.emptyList();
VariableAssignment va = new VariableAssignment(); VariableAssignment va = new VariableAssignment();
for (Map.Entry<Variable, Type> s : sig.entrySet()) {
va.declare(s.getKey(), s.getValue());
va.assign(s.getKey(),
Value.from(m.group(s.getKey().getIdentifier())));
}
return Collections.singletonList(va); return Collections.singletonList(va);
} }
} }
...@@ -66,7 +66,7 @@ public class FindNearestASTNode implements ASTTraversal<ASTNode> { ...@@ -66,7 +66,7 @@ public class FindNearestASTNode implements ASTTraversal<ASTNode> {
@Override @Override
public ASTNode visit(MatchExpression match) { public ASTNode visit(MatchExpression match) {
return childOrMe(match, match.getSignature(), match.getDerivableTerm(), match.getPattern()); return childOrMe(match, match.getDerivableTerm(), match.getPattern());
} }
@Override @Override
......
...@@ -127,7 +127,7 @@ public class SequentMatcher extends BorderPane { ...@@ -127,7 +127,7 @@ public class SequentMatcher extends BorderPane {
public void startMatch() { public void startMatch() {
sequentView.clearHighlight(); sequentView.clearHighlight();
KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(getSelectedGoalNodeToShow().getData().getEnv()).sequent(getSelectedGoalNodeToShow().getData().getNode().sequent()).build(); KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(getSelectedGoalNodeToShow().getData().getEnv()).sequent(getSelectedGoalNodeToShow().getData().getNode().sequent()).build();
Matchings matchings = kmf.matches(matchpattern.getText(), null); Matchings matchings = kmf.matches(matchpattern.getText());
//MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true, //MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true,
//services); //services);
......
...@@ -209,7 +209,7 @@ public class SequentView extends CodeArea { ...@@ -209,7 +209,7 @@ public class SequentView extends CodeArea {
if (node.get().sequent() != null) { if (node.get().sequent() != null) {
KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(this.getKeYProofFacade().getEnvironment()) KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(this.getKeYProofFacade().getEnvironment())
.sequent(node.get().sequent()).build(); .sequent(node.get().sequent()).build();
Matchings m = kmf.matches(pattern, null); Matchings m = kmf.matches(pattern);
// Matchings m = // Matchings m =
//MatcherFacade.matches(pattern, node.get().sequent(), true, services); //MatcherFacade.matches(pattern, node.get().sequent(), true, services);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment