Commit 58e94ba2 authored by Sarah Grebing's avatar Sarah Grebing

Merge remote-tracking branch 'origin/grebing_luong_workbranch' into grebing_luong_workbranch

parents 54952861 d9989cfc
Pipeline #38445 passed with stages
in 2 minutes and 35 seconds
...@@ -19,6 +19,7 @@ import edu.kit.iti.formal.psdbg.parser.Visitor; ...@@ -19,6 +19,7 @@ import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import lombok.Getter; import lombok.Getter;
import lombok.Setter;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import java.io.File; import java.io.File;
...@@ -42,6 +43,11 @@ public class InterpreterBuilder { ...@@ -42,6 +43,11 @@ public class InterpreterBuilder {
private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder(); private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder();
@Getter @Getter
private BuiltInCommandHandler bich = new BuiltInCommandHandler(); private BuiltInCommandHandler bich = new BuiltInCommandHandler();
@Getter
@Setter
private TacletAppSelectionDialogService tacletappSelectionDialogService;
@Getter @Getter
private ProofScript entryPoint; private ProofScript entryPoint;
@Getter @Getter
...@@ -82,6 +88,8 @@ public class InterpreterBuilder { ...@@ -82,6 +88,8 @@ public class InterpreterBuilder {
public KeyInterpreter build() { public KeyInterpreter build() {
interpreter.getVariableHooks().add(keyHooks); interpreter.getVariableHooks().add(keyHooks);
interpreter.getVariableHooks().add(optionsHook); interpreter.getVariableHooks().add(optionsHook);
interpreter.setTacletAppSelectionDialogService(tacletappSelectionDialogService);
pmr.setTacletAppSelectionDialogService(tacletappSelectionDialogService);
return interpreter; return interpreter;
} }
......
...@@ -17,6 +17,8 @@ import javafx.beans.binding.BooleanBinding; ...@@ -17,6 +17,8 @@ import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.SimpleBooleanProperty; import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty; import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Task; import javafx.concurrent.Task;
import lombok.Getter;
import lombok.Setter;
import org.apache.logging.log4j.LogManager; 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;
...@@ -73,6 +75,9 @@ public class KeYProofFacade { ...@@ -73,6 +75,9 @@ public class KeYProofFacade {
private File filepath; private File filepath;
@Getter
@Setter
private TacletAppSelectionDialogService tacletAppSelectionDialogService;
/** /**
* *
*/ */
...@@ -204,6 +209,7 @@ public class KeYProofFacade { ...@@ -204,6 +209,7 @@ public class KeYProofFacade {
.scriptSearchPath(new File(".")); .scriptSearchPath(new File("."));
//getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false); //getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
interpreterBuilder.setTacletappSelectionDialogService(tacletAppSelectionDialogService);
return interpreterBuilder; return interpreterBuilder;
} }
//endregion //endregion
......
...@@ -43,6 +43,10 @@ public class KeyInterpreter extends Interpreter<KeyData> { ...@@ -43,6 +43,10 @@ public class KeyInterpreter extends Interpreter<KeyData> {
// .put(SimpleType.SEQ, VariableAssignments.VarType.SEQ) // .put(SimpleType.SEQ, VariableAssignments.VarType.SEQ)
.build(); .build();
@Getter
@Setter
private TacletAppSelectionDialogService tacletAppSelectionDialogService;
public KeyInterpreter(CommandLookup lookup) { public KeyInterpreter(CommandLookup lookup) {
super(lookup); super(lookup);
......
...@@ -19,7 +19,9 @@ import de.uka.ilkd.key.rule.Rule; ...@@ -19,7 +19,9 @@ import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.ValueInjector; import edu.kit.iti.formal.psdbg.ValueInjector;
import edu.kit.iti.formal.psdbg.interpreter.IndistinctWindow;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.TacletAppSelectionDialogService;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; 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.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State; import edu.kit.iti.formal.psdbg.interpreter.data.State;
...@@ -28,9 +30,9 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicabl ...@@ -28,9 +30,9 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicabl
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDeclaredException; import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDeclaredException;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDefinedException; import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDefinedException;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.Statement;
import edu.kit.iti.formal.psdbg.parser.ast.Variable; import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import javafx.collections.FXCollections; import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.event.ActionEvent; import javafx.event.ActionEvent;
import javafx.event.EventHandler; import javafx.event.EventHandler;
import javafx.geometry.Pos; import javafx.geometry.Pos;
...@@ -44,14 +46,12 @@ import javafx.stage.Stage; ...@@ -44,14 +46,12 @@ import javafx.stage.Stage;
import javafx.stage.StageStyle; import javafx.stage.StageStyle;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import lombok.Setter;
import org.apache.logging.log4j.LogManager; 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.io.IOException;
import java.util.*; import java.util.*;
import java.util.concurrent.ConcurrentMap;
import java.util.concurrent.TimeUnit;
/** /**
* @author Alexander Weigl * @author Alexander Weigl
...@@ -69,6 +69,10 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -69,6 +69,10 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
private Scanner scanner = new Scanner(System.in); private Scanner scanner = new Scanner(System.in);
@Getter
@Setter
private TacletAppSelectionDialogService tacletAppSelectionDialogService;
public RuleCommandHandler() { public RuleCommandHandler() {
this(new HashMap<>()); this(new HashMap<>());
} }
...@@ -150,26 +154,24 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -150,26 +154,24 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
c.execute(uiControl, cc, estate); c.execute(uiControl, cc, estate);
//TODO auslagern / finally
ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
state.getGoals().remove(expandedNode);
if (state.getSelectedGoalNode().equals(expandedNode)) {
state.setSelectedGoalNode(null);
}
for (Goal g : ngoals) {
KeyData kdn = new KeyData(kd, g.node());
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
}
} catch (ScriptException e) { } catch (ScriptException e) {
boolean exceptionsolved = false; boolean exceptionsolved = false;
if (e instanceof ScriptException.IndistinctFormula) { if (e instanceof ScriptException.IndistinctFormula) {
List<TacletApp> matchingapps = ((ScriptException.IndistinctFormula) e).getMatchingApps(); List<TacletApp> matchingapps = ((ScriptException.IndistinctFormula) e).getMatchingApps();
ObservableList<String> obsMatchApps = FXCollections.observableArrayList();
matchingapps.forEach(k -> obsMatchApps.add(k.toString()));
//TODO: open window here
IndistinctWindow indistinctWindow = new IndistinctWindow(obsMatchApps);
tacletAppSelectionDialogService.setPane(indistinctWindow);
tacletAppSelectionDialogService.showDialog();
//IndistinctPrompt prompt = new IndistinctPrompt(matchingapps); //IndistinctPrompt prompt = new IndistinctPrompt(matchingapps);
//TacletApp chosen = prompt.getChosen(); //TacletApp chosen = prompt.getChosen();
/*
int inputindex = -1; int inputindex = -1;
while (true) { while (true) {
...@@ -179,10 +181,10 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -179,10 +181,10 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
System.out.flush(); System.out.flush();
// User input // User input
try { try {
inputindex = System.in.read(); inputindex = scanner.nextInt(); //System.in.read();
} catch (IOException ioe) { } catch (InputMismatchException ime) {
System.out.println("No valid input"); System.out.println("InputMismatchException thrown: edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java:176");
continue; continue;
} }
if (0 <= inputindex && inputindex <= matchingapps.size() - 1) { if (0 <= inputindex && inputindex <= matchingapps.size() - 1) {
...@@ -192,12 +194,18 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -192,12 +194,18 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
System.out.println("No valid input"); System.out.println("No valid input");
} }
} }
TacletApp chosenApp = matchingapps.get(inputindex); */
try {
tacletAppSelectionDialogService.latch.await();
} catch (InterruptedException ie) {
System.out.println("latch await got interrupted");
}
TacletApp chosenApp = matchingapps.get(tacletAppSelectionDialogService.getUserIndexInput());
TacletInstantiationModel tim = new TacletInstantiationModel(chosenApp, data.getGoal().sequent(), data.getGoal().getLocalNamespaces(), null, data.getGoal()); TacletInstantiationModel tim = new TacletInstantiationModel(chosenApp, kd.getGoal().sequent(), kd.getGoal().getLocalNamespaces(), null, kd.getGoal());
try { try {
TacletApp newTA = tim.createTacletApp(); TacletApp newTA = tim.createTacletApp();
newTA.execute(data.getGoal(), data.getProof().getServices()); newTA.execute(kd.getGoal(), kd.getProof().getServices());
int linenr = call.getStartPosition().getLineNumber(); int linenr = call.getStartPosition().getLineNumber();
exceptionsolved = true; exceptionsolved = true;
...@@ -205,20 +213,32 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -205,20 +213,32 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
} }
} }
if (exceptionsolved) return;
if (!exceptionsolved) {
if (interpreter.isStrictMode()) { if (interpreter.isStrictMode()) {
throw new ScriptCommandNotApplicableException(e, c, map); throw new ScriptCommandNotApplicableException(e, c, map);
} else { } else {
//Utils necessary oder schmeißen //Utils necessary oder schmeißen
LOGGER.error("Command " + call.getCommand() + " is not applicable in line " + call.getRuleContext().getStart().getLine()); LOGGER.error("Command " + call.getCommand() + " is not applicable in line " + call.getRuleContext().getStart().getLine());
} }
}
} catch (InterruptedException e) { } catch (InterruptedException e) {
e.printStackTrace(); e.printStackTrace();
} catch (Exception e) { } catch (Exception e) {
e.printStackTrace(); e.printStackTrace();
} }
//refreshes Debuggermainmodel
ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
state.getGoals().remove(expandedNode);
if (state.getSelectedGoalNode().equals(expandedNode)) {
state.setSelectedGoalNode(null);
}
for (Goal g : ngoals) {
KeyData kdn = new KeyData(kd, g.node());
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
}
} }
private Map<String, Object> createParameters(VariableAssignment assignments) { private Map<String, Object> createParameters(VariableAssignment assignments) {
......
package edu.kit.iti.formal.psdbg.interpreter;
import javafx.collections.ObservableList;
import javafx.event.EventHandler;
import javafx.fxml.FXMLLoader;
import javafx.scene.control.Button;
import javafx.scene.control.ListView;
import javafx.scene.control.ScrollPane;
import javafx.scene.control.TextField;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.scene.layout.HBox;
import javafx.scene.text.Text;
import lombok.Getter;
import java.util.List;
public class IndistinctWindow extends BorderPane {
@Getter
int indexOfSelected = -1;
public Button accept;
public IndistinctWindow(ObservableList<String> matchApps) {
//Top
ScrollPane scrollPane = new ScrollPane();
ListView<String> listView = new ListView<String>(matchApps);
scrollPane.setContent(listView);
this.setTop(scrollPane);
listView.setOnMouseClicked(new EventHandler<MouseEvent>() {
@Override
public void handle(MouseEvent event) {
indexOfSelected = listView.getSelectionModel().getSelectedIndex();
}
});
//Center
/*
HBox hbox = new HBox();
Text inputlabel = new Text("Enter a number:");
TextField textField = new TextField();
hbox.getChildren().addAll(inputlabel, textField);
this.setCenter(hbox);
*/
//Bottom
accept = new Button();
accept.setText("Accept");
this.setBottom(accept);
}
}
package edu.kit.iti.formal.psdbg.interpreter;
import javafx.application.Platform;
import javafx.concurrent.Service;
import javafx.concurrent.Task;
import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader;
import javafx.scene.Scene;
import javafx.scene.control.Button;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.scene.layout.Pane;
import javafx.stage.Stage;
import lombok.Getter;
import lombok.Setter;
import java.util.List;
import java.util.concurrent.Callable;
import java.util.concurrent.CountDownLatch;
import java.util.concurrent.FutureTask;
public abstract class TacletAppSelectionDialogService {
@Setter
Pane pane;
@Getter
int userIndexInput;
public CountDownLatch latch = new CountDownLatch(1);
public void showDialog() {
Platform.runLater(new Runnable() {
@Override
public void run() {
Stage stage = new Stage();
stage.setTitle("TacletAppSelectionDialog");
if (pane != null) {
Scene scene = new Scene(pane);
stage.setScene(scene);
}
((IndistinctWindow) pane).accept.setOnMouseClicked(new EventHandler<MouseEvent>() {
@Override
public void handle(MouseEvent event) {
getIndex();
if (userIndexInput != -1) {
stage.close();
}
}
});
stage.showAndWait();
latch.countDown();
}
});
}
private void getIndex() {
userIndexInput = ((IndistinctWindow) pane).getIndexOfSelected();
}
}
...@@ -30,6 +30,7 @@ import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier; ...@@ -30,6 +30,7 @@ import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder; import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter; import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.TacletAppSelectionDialogService;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; 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.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint; import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
...@@ -179,6 +180,9 @@ public class DebuggerMain implements Initializable { ...@@ -179,6 +180,9 @@ public class DebuggerMain implements Initializable {
private InteractiveModeController interactiveModeController; private InteractiveModeController interactiveModeController;
private ScriptExecutionController scriptExecutionController; private ScriptExecutionController scriptExecutionController;
private TacletAppSelectionDialogService tacletAppSelectionDialogService = new TacletAppSelectionDialogService() {
};
private ViewSettings viewSettings; private ViewSettings viewSettings;
@FXML @FXML
...@@ -417,6 +421,8 @@ public class DebuggerMain implements Initializable { ...@@ -417,6 +421,8 @@ public class DebuggerMain implements Initializable {
viewSettings = new ViewSettings(this); viewSettings = new ViewSettings(this);
FACADE.setTacletAppSelectionDialogService(tacletAppSelectionDialogService);
} }
/** /**
......
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