Commit 7b0417c6 authored by Sarah Grebing's avatar Sarah Grebing

scriptcommand

parent d91bd463
Pipeline #28107 passed with stages
in 3 minutes and 49 seconds
package edu.kit.iti.formal.psdbg.gui.controller; package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.Subscribe; import com.google.common.eventbus.Subscribe;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.Services;
...@@ -27,6 +28,7 @@ import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework; ...@@ -27,6 +28,7 @@ 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.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException; import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.MacroCommandHandler; import edu.kit.iti.formal.psdbg.interpreter.funchdl.MacroCommandHandler;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.ProofScriptCommandBuilder;
import edu.kit.iti.formal.psdbg.parser.PrettyPrinter; import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
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;
...@@ -43,6 +45,7 @@ import org.key_project.util.collection.ImmutableList; ...@@ -43,6 +45,7 @@ import org.key_project.util.collection.ImmutableList;
import recoder.util.Debug; import recoder.util.Debug;
import javax.annotation.Nullable; import javax.annotation.Nullable;
import java.lang.reflect.Method;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.util.stream.Collectors; import java.util.stream.Collectors;
...@@ -340,10 +343,11 @@ public class InteractiveModeController { ...@@ -340,10 +343,11 @@ public class InteractiveModeController {
postStateHandler(call, g, goals, expandedNode, kd); postStateHandler(call, g, goals, expandedNode, kd);
break; break;
case SCRIPT_COMMAND: case SCRIPT_COMMAND:
ScriptCommand.Parameters ccS = new ScriptCommand.Parameters(); ProofScriptCommandBuilder psb = new ProofScriptCommandBuilder(KeYApi.getScriptCommandApi().getScriptCommands());
ScriptCommand cS = new ScriptCommand(); ProofScriptCommand ps = psb.getCommands().get(call.getCommand());
ccS = valueInjector.inject(cS, ccS, map);
cS.execute(uiControl, ccS, estate); Object temp = valueInjector.inject(ps, getParameterInstance(ps), map);
ps.execute(uiControl, temp, estate);
postStateHandler(call, g, goals, expandedNode, kd); postStateHandler(call, g, goals, expandedNode, kd);
break; break;
default: default:
...@@ -363,6 +367,12 @@ public class InteractiveModeController { ...@@ -363,6 +367,12 @@ public class InteractiveModeController {
} }
private <T> T getParameterInstance(ProofScriptCommand c) throws NoSuchMethodException, IllegalAccessException,
InstantiationException {
Method method = c.getClass().getMethod("evaluateArguments", EngineState.class, Map.class);
Class rtclazz = method.getReturnType();
return (T) rtclazz.newInstance();
}
private void postStateHandler(CallStatement call, Goal g, ObservableList<GoalNode<KeyData>> goals, GoalNode<KeyData> expandedNode, KeyData kd) { 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()); ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(expandedNode.getData().getNode());
......
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