Commit 49abb804 authored by Sarah Grebing's avatar Sarah Grebing

Bugfix: DerivableCase

parent e81512f5
Pipeline #29423 passed with stages
in 2 minutes and 43 seconds
......@@ -100,9 +100,7 @@ literals :
</pre>*/
matchPattern
:
MATCH (
derivable=DERIVABLE derivableExpression=expression
| (pattern=expression (USING LBRACKET argList RBRACKET)?)
MATCH ((pattern=expression (USING LBRACKET argList RBRACKET)?)
)
;
......@@ -122,8 +120,9 @@ casesStmt
casesList
: (TRY |
(CASE (expression
| (CLOSES INDENT closesGuard=stmtList DEDENT) ) ) )
(CASE (expression
|(CLOSES INDENT closesGuard=stmtList DEDENT)
|(derivable=DERIVABLE derivableExpression=expression) ) ))
COLON INDENT? body=stmtList DEDENT?
;
......
......@@ -160,6 +160,7 @@ public interface ASTTraversal<T> extends Visitor<T> {
return null;
}
@Override
default T visit(ForeachStatement foreach) {
foreach.getBody().accept(this);
......@@ -209,6 +210,14 @@ public interface ASTTraversal<T> extends Visitor<T> {
return null;
}
@Override
default T visit(DerivableCase derivableCase){
derivableCase.getExpression().accept(this);
derivableCase.getBody().accept(this);
return null;
}
@Override
default T visit(SubstituteExpression subst) {
subst.getSub().accept(this);
......
......@@ -92,6 +92,11 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
return defaultVisit(defCase);
}
@Override
public T visit(DerivableCase derivableCase) {
return defaultVisit(derivableCase);
}
@Override
public T visit(CaseStatement caseStatement) {
return defaultVisit(caseStatement);
......
......@@ -370,17 +370,9 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
MatchExpression match = new MatchExpression();
match.setRuleContext(ctx);
if (ctx.derivable != null) {
match.setDerivable(true);
Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.derivableExpression.accept(this);
match.setPattern(e);
e.setParent(match);
match.setDerivableTerm(e);
} else {
Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.pattern.accept(this);
match.setPattern(e);
e.setParent(match);
}
Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.pattern.accept(this);
match.setPattern(e);
e.setParent(match);
return match;
}
......@@ -417,7 +409,13 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
Statements closes = (Statements) ctx.closesGuard.accept(this);
((ClosesCase) cs).setClosesGuard(closes);
closes.setParent(cs);
} else {
} else if (ctx.derivable != null) {
cs = new DerivableCase();
Expression pattern = (Expression) ctx.derivableExpression.accept(this);
((DerivableCase) cs).setExpression(pattern);
pattern.setParent(cs);
} else
{
cs = new GuardedCaseStatement();
Expression<ParserRuleContext> guard = (Expression<ParserRuleContext>) ctx.expression().accept(this);
((GuardedCaseStatement) cs).setGuard(guard);
......
......@@ -53,6 +53,8 @@ public interface Visitor<T> {
T visit(DefaultCaseStatement defCase);
T visit(DerivableCase derivableCase);
//T visit(CaseStatement case_);
T visit(CallStatement call);
......
package edu.kit.iti.formal.psdbg.parser.ast;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.Data;
import lombok.NoArgsConstructor;
@Data
@NoArgsConstructor
public class DerivableCase extends CaseStatement{
private Expression expression;
public DerivableCase(Statements copy, Expression copy1) {
super(copy);
this.expression=copy1;
}
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
}
@Override
public CaseStatement copy() {
DerivableCase dc = new DerivableCase(body.copy(), expression.copy());
dc.setRuleContext(this.getRuleContext());
return dc;
}
}
......@@ -43,7 +43,7 @@ import lombok.Setter;
public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
//private Signature signature = new Signature();
private Expression pattern;
@Getter @Setter
@Deprecated @Getter @Setter
private boolean isDerivable = false;
@Deprecated
private Expression derivableTerm;
......
......@@ -20,6 +20,7 @@ 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.TypeFacade;
import lombok.Getter;
import lombok.Setter;
import java.util.Collections;
import java.util.List;
......@@ -30,8 +31,6 @@ import java.util.function.Function;
* @version 1 (28.08.17)
*/
public class KeyInterpreter extends Interpreter<KeyData> {
@Getter
private static final BiMap<SimpleType, VariableAssignments.VarType> typeConversionBiMap =
new ImmutableBiMap.Builder<SimpleType, VariableAssignments.VarType>()
......@@ -148,63 +147,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
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
......
......@@ -42,6 +42,7 @@ public class TermValue {
}
}
public TermValue copy() {
TermValue tv = new TermValue();
......
......@@ -3,8 +3,10 @@ package edu.kit.iti.formal.psdbg.interpreter.matcher;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.op.LogicVariable;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.parser.ParserException;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.ApplyStrategy;
import de.uka.ilkd.key.proof.Goal;
......@@ -14,14 +16,12 @@ import de.uka.ilkd.key.rule.NoPosTacletApp;
import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.interpreter.MatcherApi;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.SortType;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.data.*;
import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.data.Value;
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.TypeFacade;
import lombok.Getter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
......@@ -54,12 +54,25 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
/**
* @param proof
* @param kd
* @param term
*
* @return null if the term is not derivable or the new state
*/
public static GoalNode<KeyData> isDerivable(Proof proof, GoalNode<KeyData> kd, Term term) {
public GoalNode<KeyData> isDerivable(GoalNode<KeyData> kd, Value pattern) {
Proof proof = kd.getData().getProof();
TermValue tv = (TermValue) pattern.getData();
Term term = tv.getTerm();
if(term == null) {
Services services = kd.getData().getProof().getServices();
try {
term = new TermBuilder(services.getTermFactory(), services).parseTerm(tv.getTermRepr());
} catch (ParserException e) {
throw new RuntimeException(e);
}
}
Taclet cut = proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(CUT_TACLET_NAME);
TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut);
SchemaVariable sv = (SchemaVariable) app.uninstantiatedVars().iterator().next();
......@@ -82,7 +95,14 @@ public class KeYMatcher implements MatcherApi<KeyData> {
boolean isDerivable = proof.getSubtreeGoals(toShow.node()).size() == 0;
if (isDerivable) {
KeyData kdataNew = new KeyData(kd.getData(), goalList.head());
//find the open goal node
Goal toSet= null;
if(goalList.head().node().isClosed()){
toSet = goalList.tail().head();
} else{
toSet = goalList.head();
}
KeyData kdataNew = new KeyData(kd.getData(), toSet);
GoalNode<KeyData> newGoalNode = new GoalNode<KeyData>(kd, kdataNew, kdataNew.isClosedNode());
return newGoalNode;
} else {
......
......@@ -12,7 +12,9 @@ import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
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.Type;
import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
import lombok.Getter;
import lombok.Setter;
import org.antlr.v4.runtime.ParserRuleContext;
......@@ -209,6 +211,35 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return null;
}
@Override
public Object visit(DerivableCase derivableCase) {
Expression pattern = derivableCase.getExpression();
State<T> currentStateToMatch = peekState();
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
assert currentStateToMatch.getGoals().contains(selectedGoal);
Value v = evaluate(pattern);
if(v.getType() == TypeFacade.ANY_TERM){
GoalNode<T> newGoalNode= matcherApi.isDerivable(selectedGoal, v);
try {
enterScope(derivableCase);
if (newGoalNode != null) {
currentStateToMatch.getGoals().remove(selectedGoal);
currentStateToMatch.getGoals().add(newGoalNode);
currentStateToMatch.setSelectedGoalNode(newGoalNode);
executeBody(derivableCase.getBody(), newGoalNode, new VariableAssignment());
return true;
} else {
return false;
}
} finally {
exitScope(derivableCase);
}
} else {
throw new RuntimeException("A derivable expression must contain a term. Received a"+v.getType());
}
}
/**
* @param casesStatement
* @return
......@@ -303,7 +334,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
assert currentStateToMatch.getGoals().contains(selectedGoal);
VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
try {
enterScope(guardedCaseStatement);
if (va != null) {
......
......@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import java.util.List;
......@@ -27,4 +28,6 @@ public interface MatcherApi<T> {
*/
List<VariableAssignment> matchSeq(GoalNode<T> currentState, String pattern);
GoalNode<T> isDerivable(GoalNode<T> currentState, Value v);
}
......@@ -49,6 +49,13 @@ public class PseudoMatcher implements MatcherApi<String> {
}
return Collections.singletonList(va);
}
@Override
public GoalNode<String> isDerivable(GoalNode<String> currentState, Value v) {
return null;
}
}
\ No newline at end of file
......@@ -7,7 +7,7 @@ script full(){
impRight;
impLeft;
cases {
case match derivable `p`:
case derivable `p`:
}
}
......
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