Commit ac4ea814 authored by Sarah Grebing's avatar Sarah Grebing

First part of fix for isDerivable

parent 07477085
Pipeline #29176 passed with stages
in 3 minutes and 46 seconds
...@@ -373,6 +373,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -373,6 +373,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
if (ctx.derivable != null) { if (ctx.derivable != null) {
match.setDerivable(true); match.setDerivable(true);
Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.derivableExpression.accept(this); Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.derivableExpression.accept(this);
match.setPattern(e);
e.setParent(match); e.setParent(match);
match.setDerivableTerm(e); match.setDerivableTerm(e);
} else { } else {
......
...@@ -30,6 +30,8 @@ import edu.kit.iti.formal.psdbg.parser.types.SimpleType; ...@@ -30,6 +30,8 @@ import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import edu.kit.iti.formal.psdbg.parser.types.TermType; import edu.kit.iti.formal.psdbg.parser.types.TermType;
import edu.kit.iti.formal.psdbg.parser.types.Type; import edu.kit.iti.formal.psdbg.parser.types.Type;
import lombok.Data; import lombok.Data;
import lombok.Getter;
import lombok.Setter;
/** /**
* A match expression contains an argument and a uses clause. * A match expression contains an argument and a uses clause.
...@@ -41,6 +43,7 @@ import lombok.Data; ...@@ -41,6 +43,7 @@ import lombok.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 @Setter
private boolean isDerivable = false; private boolean isDerivable = false;
@Deprecated @Deprecated
private Expression derivableTerm; private Expression derivableTerm;
......
...@@ -3,11 +3,16 @@ package edu.kit.iti.formal.psdbg.interpreter; ...@@ -3,11 +3,16 @@ package edu.kit.iti.formal.psdbg.interpreter;
import com.google.common.collect.BiMap; import com.google.common.collect.BiMap;
import com.google.common.collect.ImmutableBiMap; import com.google.common.collect.ImmutableBiMap;
import de.uka.ilkd.key.api.VariableAssignments; import de.uka.ilkd.key.api.VariableAssignments;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.parser.ParserException;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.interpreter.data.*; import edu.kit.iti.formal.psdbg.interpreter.data.*;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.InvalidTypeException; import edu.kit.iti.formal.psdbg.interpreter.exceptions.InvalidTypeException;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup; import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher;
import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value; import edu.kit.iti.formal.psdbg.parser.data.Value;
...@@ -16,6 +21,7 @@ import edu.kit.iti.formal.psdbg.parser.types.TermType; ...@@ -16,6 +21,7 @@ import edu.kit.iti.formal.psdbg.parser.types.TermType;
import edu.kit.iti.formal.psdbg.parser.types.TypeFacade; import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
import lombok.Getter; import lombok.Getter;
import java.util.Collections;
import java.util.List; import java.util.List;
import java.util.function.Function; import java.util.function.Function;
...@@ -24,6 +30,8 @@ import java.util.function.Function; ...@@ -24,6 +30,8 @@ import java.util.function.Function;
* @version 1 (28.08.17) * @version 1 (28.08.17)
*/ */
public class KeyInterpreter extends Interpreter<KeyData> { public class KeyInterpreter extends Interpreter<KeyData> {
@Getter @Getter
private static final BiMap<SimpleType, VariableAssignments.VarType> typeConversionBiMap = private static final BiMap<SimpleType, VariableAssignments.VarType> typeConversionBiMap =
new ImmutableBiMap.Builder<SimpleType, VariableAssignments.VarType>() new ImmutableBiMap.Builder<SimpleType, VariableAssignments.VarType>()
...@@ -140,6 +148,64 @@ public class KeyInterpreter extends Interpreter<KeyData> { ...@@ -140,6 +148,64 @@ public class KeyInterpreter extends Interpreter<KeyData> {
return eval; return eval;
} }
@Override
public Object visit(GuardedCaseStatement guardedCaseStatement) {
Expression matchExpression = guardedCaseStatement.getGuard();
State<KeyData> currentStateToMatch = peekState();
GoalNode<KeyData> selectedGoal = currentStateToMatch.getSelectedGoalNode();
assert currentStateToMatch.getGoals().contains(selectedGoal);
if(matchExpression.hasMatchExpression()){
MatchExpression me = (MatchExpression) matchExpression;
if(me.isDerivable()){
enterScope(matchExpression);
Evaluator eval = new Evaluator<>(selectedGoal.getAssignments(), selectedGoal);
eval.getEntryListeners().addAll(getEntryListeners());
eval.getExitListeners().addAll(getExitListeners());
Value eval1 = eval.eval(me.getPattern());
Term term = null;
Services services = selectedGoal.getData().getProof().getServices();
if(eval1.getType() == TypeFacade.ANY_TERM){
if(eval1.getData() instanceof String){
try {
term = new TermBuilder(services.getTermFactory(), services).parseTerm(eval1.getData().toString());
} catch (ParserException e) {
throw new RuntimeException(e);
}
} else {
TermValue tv = (TermValue) eval1.getData();
term = tv.getTerm();
}
} else {
new RuntimeException("The parameter for a derivable expression has to be a term. Got "+ eval1.getType());
}
KeYMatcher.isDerivable(selectedGoal.getData().getProof(), selectedGoal, term);
exitScope(matchExpression);
} else {
return super.visit(guardedCaseStatement);
}
}
// VariableAssignment va = super.evaluateMatchInGoal(matchExpression, selectedGoal);
VariableAssignment va = null;
try {
enterScope(guardedCaseStatement);
if (va != null) {
executeBody(guardedCaseStatement.getBody(), selectedGoal, va);
return true;
} else {
return false;
}
} finally {
exitScope(guardedCaseStatement);
}
}
@Override @Override
public Object visit(LetStatement let) { public Object visit(LetStatement let) {
......
...@@ -47,6 +47,9 @@ public class KeyMatcherFacadeTest { ...@@ -47,6 +47,9 @@ public class KeyMatcherFacadeTest {
*/ */
@Test @Test
public void matchTerms() throws Exception { public void matchTerms() throws Exception {
System.out.println(shouldMatchT("f(a)", "...f(a)..."));
System.out.println(shouldMatchT("h(a,a)", "...h(?X,?Y)..."));
System.out.println(shouldMatchT("f(a)", "?")); System.out.println(shouldMatchT("f(a)", "?"));
System.out.println(shouldMatchT("f(a)", "f(a)")); System.out.println(shouldMatchT("f(a)", "f(a)"));
...@@ -59,6 +62,9 @@ public class KeyMatcherFacadeTest { ...@@ -59,6 +62,9 @@ public class KeyMatcherFacadeTest {
@Test @Test
public void matchSeq() throws Exception { public void matchSeq() throws Exception {
//atm missing is catching the toplevel formula //atm missing is catching the toplevel formula
shouldMatch("pred(a), pred(b), a=b, a=c ==> pred(c)", "pred(?X), ?X=?Y ==> ", "[?X=a, ?Y=b}, {?X=a, ?Y=c}]");
shouldMatch("pred(a), pred(b), a=b, a=c ==> pred(c)", "pred(?X), ?X=?Y ==> pred(?Y)", "[{?X=a, ?Y=c}]");
shouldMatch("!q==>p,!p","!q ==> p", "[{}]"); shouldMatch("!q==>p,!p","!q ==> p", "[{}]");
shouldMatch("!p ,p ==> q", "!p ==> q", "[{}]"); shouldMatch("!p ,p ==> q", "!p ==> q", "[{}]");
shouldMatch("!q ,p ==> q", "!p ==> q", "{NOMATCH}"); shouldMatch("!q ,p ==> q", "!p ==> q", "{NOMATCH}");
......
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