Skip to content

GitLab

Commit 92266590 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Further implemenmtation for interactive macros

parent 8b850649
Pipeline #23338 passed with stages
in 3 minutes and 23 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 141 additions and 41 deletions
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/exceptions/ScriptCommandNotApplicableException.java
View file @ 92266590
package edu.kit.iti.formal.psdbg.interpreter.exceptions;
import de.uka.ilkd.key.macros.scripts.AbstractCommand;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import java.util.Map;
......@@ -13,6 +14,9 @@ public class ScriptCommandNotApplicableException extends InterpreterRuntimeExcep
public ScriptCommandNotApplicableException(Exception e, RuleCommand c) {
System.out.println("Call " + c.getName() + " was not applicable");
}
public ScriptCommandNotApplicableException(Exception e, AbstractCommand c) {
System.out.println("Call " + c.getName() + " was not applicable");
}
public ScriptCommandNotApplicableException(Exception e, RuleCommand c, Map<String, Object> params) {
super(createMessage(c, params), e);
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
View file @ 92266590
......@@ -6,9 +6,8 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.*;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
......@@ -27,6 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.MacroCommandHandler;
import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
......@@ -47,6 +47,7 @@ import java.math.BigInteger;
import java.util.*;
import java.util.stream.Collectors;
@Getter
@Setter
@RequiredArgsConstructor
......@@ -202,7 +203,7 @@ public class InteractiveModeController {
try {
applyRule(call, g);
applyRuleHelper(call, g, Type.RULE);
// Insert into the right cases
// Node currentNode = g.node();
// cases.get(findRoot(currentNode)).add(call);
......@@ -234,58 +235,148 @@ public class InteractiveModeController {
@Subscribe
public void handle(Events.MacroApplicationEvent map) {
/* LOGGER.debug("Handling {}", map);
moreThanOneMatch = false;
String tapName = map.getApp().taclet().name().toString();
Goal g = tap.getCurrentGoal();
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
Sequent seq = g.sequent();
String sfTerm = Utils.printParsableTerm(seqForm.formula(), keYServices);
String onTerm = Utils.printParsableTerm(tap.getPio().subTerm(), keYServices);
RuleCommand.Parameters params = new RuleCommand.Parameters();
params.formula = seqForm.formula();
params.rulename = tap.getApp().taclet().name().toString();
params.on = tap.getPio().subTerm();
RuleCommandHelper rch = new RuleCommandHelper(g, params);
int occ = rch.getOccurence(tap.getApp());
LOGGER.debug("Handling {}", map);
Goal g = map.getGoal();
MacroCommand.Parameters params = new MacroCommand.Parameters();
Parameters callp = new Parameters();
callp.put(new Variable("formula"), TermLiteral.from(sfTerm));
callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ)));
callp.put(new Variable("on"), TermLiteral.from(onTerm));
VariableAssignment va = new VariableAssignment(null);
CallStatement call = new CallStatement(tapName, callp);
CallStatement call = new CallStatement(map.getMacroName().getScriptCommandName(), callp);
try {
applyRule(call, g);
applyRuleHelper(call, g, Type.MACRO);
String c = getCasesAsString();
scriptArea.setText("" +
"//Preview \n" + c);
} catch (ScriptCommandNotApplicableException e) {
StringBuilder sb = new StringBuilder("The script command ");
StringBuilder sb = new StringBuilder("The macro command ");
sb.append(call.getCommand()).append(" was not applicable.");
sb.append("\nSequent Formula: formula=").append(sfTerm);
sb.append("\nOn Sub Term: on=").append(onTerm);
System.out.println("e = " + e);
//sb.append("\nSequent Formula: formula=").append(sfTerm);
//sb.append("\nOn Sub Term: on=").append(onTerm);
Utils.showWarningDialog("Proof Command was not applicable",
"Proof Command was not applicable.",
sb.toString(), e);
}
*/
}
private void applyRuleHelper(CallStatement call, Goal g, Type t) throws ScriptCommandNotApplicableException {
savepointslist.add(g.node());
savepointsstatement.add(call);
ObservableList<GoalNode<KeyData>> goals = model.getGoals();
GoalNode<KeyData> expandedNode;
List<GoalNode<KeyData>> collect = goals.stream().filter(keyDataGoalNode -> keyDataGoalNode.getData().getGoal().equals(g)).collect(Collectors.toList());
if (collect.isEmpty() || collect.size() > 1) {
throw new RuntimeException("Interactive Rule can not be applied, can not find goal in goal list");
} else {
expandedNode = collect.get(0);
}
// KeyData kd = g.getData();
Evaluator eval = new Evaluator(expandedNode.getAssignments(), expandedNode);
Map<String, Object> map = new HashMap<>();
call.getParameters().forEach((variable, expression) -> {
Value exp = eval.eval(expression);
map.put(variable.getIdentifier(), exp.getData());
});
LOGGER.info("Execute {} with {}", call, map);
try {
KeyData kd = expandedNode.getData();
map.put("#2", call.getCommand());
EngineState estate = new EngineState(g.proof());
estate.setGoal(g);
//System.out.println("on = " + map.get("on"));
//System.out.println("formula = " + map.get("formula"));
//System.out.println("occ = " + map.get("occ"));
ValueInjector valueInjector = ValueInjector.createDefault(kd.getNode());
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
switch (t){
case MACRO:
MacroCommand.Parameters cc = new MacroCommand.Parameters();
MacroCommand c = new MacroCommand();
cc = valueInjector.inject(c, cc, map);
c.execute(uiControl, cc, estate);
postStateHandler(call, g, goals, expandedNode, kd);
break;
case RULE:
RuleCommand.Parameters ccR = new RuleCommand.Parameters();
RuleCommand cR = new RuleCommand();
ccR = valueInjector.inject(cR, ccR, map);
cR.execute(uiControl, ccR, estate);
postStateHandler(call, g, goals, expandedNode, kd);
break;
case SCRIPT_COMMAND:
ScriptCommand.Parameters ccS = new ScriptCommand.Parameters();
ScriptCommand cS = new ScriptCommand();
ccS = valueInjector.inject(cS, ccS, map);
cS.execute(uiControl, ccS, estate);
postStateHandler(call, g, goals, expandedNode, kd);
break;
default:
throw new Exception("Command not found");
}
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, null, map);
} else {
throw new RuntimeException(e);
}
}
}
private void postStateHandler(CallStatement call, Goal g, ObservableList<GoalNode<KeyData>> goals, GoalNode<KeyData> expandedNode, KeyData kd) {
ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(expandedNode.getData().getNode());
goals.remove(expandedNode);
GoalNode<KeyData> last = null;
if (ngoals.size() > 1) {
cases.get(findRoot(ngoals.get(0).node())).add(call);
CasesStatement inner = new CasesStatement();
cases.get(findRoot(ngoals.get(0).node())).add(inner);
for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
val caseForSubNode = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(newGoalNode.node()))
));
caseForSubNode.setGuard(m);
inner.getCases().add(caseForSubNode);
cases.put(last.getData().getNode(), caseForSubNode.getBody());
}
} else {
if (ngoals.size() == 0) {
cases.get(findRoot(expandedNode.getData().getNode())).add(call);
} else {
KeyData kdn = new KeyData(kd, ngoals.get(0).node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
Node currentNode = last.getData().getNode();
cases.get(findRoot(currentNode)).add(call);
}
}
if (last != null)
model.setSelectedGoalNodeToShow(last);
}
private Node findRoot(Node cur) {
while (cur != null) {
......@@ -301,7 +392,7 @@ public class InteractiveModeController {
casesStatement.accept(pp);
return pp.toString();
}
/*
private void applyRule(CallStatement call, Goal g) throws ScriptCommandNotApplicableException {
savepointslist.add(g.node());
savepointsstatement.add(call);
......@@ -338,6 +429,7 @@ public class InteractiveModeController {
//System.out.println("formula = " + map.get("formula"));
//System.out.println("occ = " + map.get("occ"));
ValueInjector valueInjector = ValueInjector.createDefault(kd.getNode());
RuleCommand.Parameters cc = new RuleCommand.Parameters();
cc = valueInjector.inject(c, cc, map);
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
......@@ -389,7 +481,7 @@ public class InteractiveModeController {
}
}
}
}*/
private String format(String branchingLabel) {
// System.out.println("branchingLabel = " + branchingLabel);
......@@ -419,4 +511,8 @@ public class InteractiveModeController {
}
static enum Type {
MACRO, RULE, SCRIPT_COMMAND;
}
}
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