Commit b56fc44e authored by Alexander Weigl's avatar Alexander Weigl

Persistence of interpreter state

parent 32c3a995
...@@ -95,7 +95,7 @@ public interface ASTTraversal<T> extends Visitor<T> { ...@@ -95,7 +95,7 @@ public interface ASTTraversal<T> extends Visitor<T> {
@Override @Override
default T visit(MatchExpression match) { default T visit(MatchExpression match) {
match.getPattern().accept(this); match.getPattern().accept(this);
match.getSignature().accept(this); //match.getSignature().accept(this);
return null; return null;
} }
......
...@@ -123,7 +123,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> { ...@@ -123,7 +123,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
s.append("match "); s.append("match ");
String prefix = getWhitespacePrefix(); String prefix = getWhitespacePrefix();
match.getPattern().accept(this); match.getPattern().accept(this);
if (!match.getSignature().isEmpty()) { /*if (!match.getSignature().isEmpty()) {
if (getCurrentLineLength() > maxWidth) { if (getCurrentLineLength() > maxWidth) {
s.append("\n").append(prefix); s.append("\n").append(prefix);
...@@ -134,7 +134,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> { ...@@ -134,7 +134,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
s.append("using ["); s.append("using [");
match.getSignature().accept(this); match.getSignature().accept(this);
s.append("]"); s.append("]");
} }*/
return null; return null;
} }
......
...@@ -363,11 +363,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -363,11 +363,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
e.setParent(match); e.setParent(match);
match.setDerivableTerm(e); match.setDerivableTerm(e);
} else { } else {
if (ctx.argList() != null) { /*if (ctx.argList() != null) {
Signature signature = (Signature) ctx.argList().accept(this); Signature signature = (Signature) ctx.argList().accept(this);
match.setSignature(signature); match.setSignature(signature);
signature.setParent(match); signature.setParent(match);
} }*/
Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.pattern.accept(this); Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.pattern.accept(this);
match.setPattern(e); match.setPattern(e);
e.setParent(match); e.setParent(match);
......
...@@ -41,7 +41,7 @@ import lombok.Setter; ...@@ -41,7 +41,7 @@ import lombok.Setter;
*/ */
@Data @Data
public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> { public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
private Signature signature = new Signature(); //private Signature signature = new Signature();
private Expression pattern; private Expression pattern;
@Getter @Getter
@Setter @Setter
...@@ -64,8 +64,8 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter ...@@ -64,8 +64,8 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter
@Override @Override
public MatchExpression copy() { public MatchExpression copy() {
MatchExpression me = new MatchExpression(); MatchExpression me = new MatchExpression();
if (signature != null) //if (signature != null)
me.signature = signature.copy(); // me.signature = signature.copy();
me.pattern = pattern.copy(); me.pattern = pattern.copy();
me.setRuleContext(this.ruleContext); me.setRuleContext(this.ruleContext);
return me; return me;
......
...@@ -4,7 +4,6 @@ import de.uka.ilkd.key.java.Services; ...@@ -4,7 +4,6 @@ import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.LogicVariable; import de.uka.ilkd.key.logic.op.LogicVariable;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.ApplyStrategy; import de.uka.ilkd.key.proof.ApplyStrategy;
...@@ -28,7 +27,10 @@ import org.apache.logging.log4j.LogManager; ...@@ -28,7 +27,10 @@ import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import java.util.*; import java.util.ArrayList;
import java.util.Collections;
import java.util.LinkedList;
import java.util.List;
import java.util.regex.MatchResult; import java.util.regex.MatchResult;
import java.util.regex.Matcher; import java.util.regex.Matcher;
import java.util.regex.Pattern; import java.util.regex.Pattern;
...@@ -40,8 +42,8 @@ import java.util.regex.Pattern; ...@@ -40,8 +42,8 @@ import java.util.regex.Pattern;
*/ */
public class KeYMatcher implements MatcherApi<KeyData> { public class KeYMatcher implements MatcherApi<KeyData> {
private static final Logger LOGGER = LogManager.getLogger(KeYMatcher.class); private static final Logger LOGGER = LogManager.getLogger(KeYMatcher.class);
private static final Name CUT_TACLET_NAME = new Name("cut"); private static final Name CUT_TACLET_NAME = new Name("cut");
private List<MatchResult> resultsFromLabelMatch; private List<MatchResult> resultsFromLabelMatch;
@Getter @Getter
...@@ -89,6 +91,17 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -89,6 +91,17 @@ public class KeYMatcher implements MatcherApi<KeyData> {
} }
} }
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 * If teh label matcher was successful the list contains all match results
* *
...@@ -116,16 +129,15 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -116,16 +129,15 @@ public class KeYMatcher implements MatcherApi<KeyData> {
String branchLabel = currentState.getData().getBranchingLabel(); String branchLabel = currentState.getData().getBranchingLabel();
String cleanBranchLabel = branchLabel.replaceAll(" ", ""); 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(Pattern.quote(cleanBranchLabel));
//Matcher branchLabelMatcher = regexpForLabel.matcher(cleanBranchLabel); //Matcher branchLabelMatcher = regexpForLabel.matcher(cleanBranchLabel);
if (branchLabelMatcher.matches()) { if (branchLabelMatcher.matches()) {
VariableAssignment va = new VariableAssignment(null); VariableAssignment va = new VariableAssignment(null);
va.declare("$$branchLabel_", SimpleType.STRING); va.declare("$$branchLabel_", SimpleType.STRING);
...@@ -166,7 +178,7 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -166,7 +178,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
// assignments.forEach(variableAssignment -> System.out.println(variableAssignment)); // assignments.forEach(variableAssignment -> System.out.println(variableAssignment));
return assignments.isEmpty()? null: assignments; return assignments.isEmpty() ? null : assignments;
} }
@Override @Override
...@@ -174,13 +186,13 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -174,13 +186,13 @@ public class KeYMatcher implements MatcherApi<KeyData> {
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, sig);
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());
return Collections.emptyList(); return Collections.emptyList();
} else { } else {
Match firstMatch = m.getMatchings().iterator().next() ; Match firstMatch = m.getMatchings().iterator().next();
VariableAssignment va = new VariableAssignment(null); VariableAssignment va = new VariableAssignment(null);
for (String s : firstMatch.keySet()) { for (String s : firstMatch.keySet()) {
MatchPath matchPath = firstMatch.get(s); MatchPath matchPath = firstMatch.get(s);
...@@ -197,7 +209,7 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -197,7 +209,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
va.declare(s, value.getType()); va.declare(s, value.getType());
va.assign(s, value); va.assign(s, value);
} catch (ClassCastException e){ } catch (ClassCastException e) {
LogicVariable var = (LogicVariable) matchPath.getUnit(); LogicVariable var = (LogicVariable) matchPath.getUnit();
String reprTerm = var.name().toString(); String reprTerm = var.name().toString();
Value<String> value = new Value<>( Value<String> value = new Value<>(
...@@ -211,7 +223,7 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -211,7 +223,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
} }
//LOGGER.info("Variables to match " + s + " : " + value); //LOGGER.info("Variables to match " + s + " : " + value);
//} //}
} }
List<VariableAssignment> retList = new LinkedList(); List<VariableAssignment> retList = new LinkedList();
...@@ -232,18 +244,6 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -232,18 +244,6 @@ public class KeYMatcher implements MatcherApi<KeyData> {
); );
} }
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) { //private TermLiteral from(SequentFormula sf) {
// return new TermLiteral(sf.toString()); // return new TermLiteral(sf.toString());
//} //}
......
...@@ -43,7 +43,8 @@ public class KeyMatcherFacade { ...@@ -43,7 +43,8 @@ public class KeyMatcherFacade {
List<Term> positions = new ArrayList<>(); List<Term> positions = new ArrayList<>();
for (String patternTerm : hasToplevelComma(pattern)) { for (String patternTerm : hasToplevelComma(pattern)) {
try { 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); positions.add(t);
} catch (ParserException e) { } catch (ParserException e) {
e.printStackTrace(); e.printStackTrace();
......
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