Commit 28943f4a authored by Sarah Grebing's avatar Sarah Grebing

Merge remote-tracking branch 'origin/master'

parents d8ebcb2c 9117eb2d
Pipeline #16587 passed with stages
in 10 minutes and 23 seconds
Subproject commit 294f2fe61188314a0e50fe80ce2de2070df85599
...@@ -33,3 +33,7 @@ mvn install:install-file -Dfile=$COMPONENTS/../libs/recoderKey.jar\ ...@@ -33,3 +33,7 @@ mvn install:install-file -Dfile=$COMPONENTS/../libs/recoderKey.jar\
-DartifactId=recoder \ -DartifactId=recoder \
-Dversion=2.7\ -Dversion=2.7\
-Dpackaging=jar \ -Dpackaging=jar \
//insgesamt efach in der Kommandozeile das eingeben
package edu.kit.iti.formal.psdbg.interpreter; package edu.kit.iti.formal.psdbg.interpreter;
import de.uka.ilkd.key.api.KeYApi; import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProjectedNode;
import de.uka.ilkd.key.api.ProofApi; import de.uka.ilkd.key.api.ProofApi;
import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.interpreter.assignhook.InterpreterOptionsHook; import edu.kit.iti.formal.psdbg.interpreter.assignhook.InterpreterOptionsHook;
import edu.kit.iti.formal.psdbg.interpreter.assignhook.KeyAssignmentHook; import edu.kit.iti.formal.psdbg.interpreter.assignhook.KeyAssignmentHook;
...@@ -19,14 +19,15 @@ import edu.kit.iti.formal.psdbg.parser.Visitor; ...@@ -19,14 +19,15 @@ 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 org.key_project.util.collection.ImmutableList;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.security.Key;
import java.util.Arrays; import java.util.Arrays;
import java.util.Collection; import java.util.Collection;
import java.util.List; import java.util.List;
import java.util.Set; import java.util.Set;
import java.util.stream.Collectors;
/** /**
* @author Alexander Weigl * @author Alexander Weigl
...@@ -202,11 +203,13 @@ public class InterpreterBuilder { ...@@ -202,11 +203,13 @@ public class InterpreterBuilder {
if (proof == null || keyEnvironment == null) if (proof == null || keyEnvironment == null)
throw new IllegalStateException("Call proof(..) before startState"); throw new IllegalStateException("Call proof(..) before startState");
final ProofApi pa = new ProofApi(proof, keyEnvironment); ImmutableList<Goal> openGoals = proof.getSubtreeGoals(proof.root());
final ProjectedNode root = pa.getFirstOpenGoal(); List<GoalNode<KeyData>> goals = openGoals.stream().map(g ->
final KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof()); new GoalNode<>(null, new KeyData(g, keyEnvironment, proof), false))
final GoalNode<KeyData> startGoal = new GoalNode<>(null, keyData, keyData.isClosedNode()); .collect(Collectors.toList());
return startState(startGoal); interpreter.newState(goals);
return this;
} }
private InterpreterBuilder startState(GoalNode<KeyData> startGoal) { private InterpreterBuilder startState(GoalNode<KeyData> startGoal) {
......
...@@ -37,6 +37,7 @@ public class InspectionView extends BorderPane { ...@@ -37,6 +37,7 @@ public class InspectionView extends BorderPane {
); );
public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu(); public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
public SequentOptionsMenu sequentOptionsMenu = new SequentOptionsMenu(model.get());
@FXML @Getter @FXML @Getter
private ComboBox<PTreeNode<KeyData>> frames; private ComboBox<PTreeNode<KeyData>> frames;
...@@ -160,6 +161,11 @@ public class InspectionView extends BorderPane { ...@@ -160,6 +161,11 @@ public class InspectionView extends BorderPane {
goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY()); goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
} }
public void showSequentOptions(MouseEvent actionEvent) {
Node n = (Node) actionEvent.getTarget();
sequentOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
}
public InspectionModel getModel() { public InspectionModel getModel() {
return model.get(); return model.get();
} }
......
package edu.kit.iti.formal.psdbg.gui.controls;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.pp.*;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
import javafx.beans.Observable;
import javafx.beans.property.*;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.fxml.FXML;
import javafx.scene.Node;
import javafx.scene.control.Label;
import javafx.scene.control.ListCell;
import javafx.scene.control.ListView;
import javafx.scene.control.TextArea;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.scene.layout.Pane;
import java.util.Collections;
import java.util.HashMap;
import java.util.Map;
public class SequentMatcher extends BorderPane {
public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
@FXML
private SequentView sequentView;
@FXML
private ListView<GoalNode<KeyData>> goalView;
@FXML
private TextArea matchpattern;
@FXML
private ListView<Map<String, MatchPath>> matchingsView;
@FXML
private Label nomatchings; //only shown when no matchings found, else always hidden
private Map<PosInOccurrence, Range> cursorPosition = new HashMap<>();
public SequentMatcher() {
Utils.createWithFXML(this);
selectedGoalNodeToShow.addListener((observable, oldValue, newValue) -> {
sequentView.setGoal(newValue.getData().getGoal());
sequentView.setNode(newValue.getData().getNode());
calculateLookupTable();
}
);
goalView.getSelectionModel().selectedItemProperty().addListener((prop, old, nnew) ->
selectedGoalNodeToShow.setValue(nnew)
);
goalView.setCellFactory(GoalNodeListCell::new);
goals.addListener((observable, oldValue, newValue) -> goalView.setItems(newValue));
matchingsView.getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
if (newValue != null) {
newValue.forEach((name, mp) -> {
PosInOccurrence pio = mp.pio();
Range r = cursorPosition.get(pio);
sequentView.setStyleClass(r.start(),r.end(), "sequent-highlight");
System.out.println("Highlight " + r.start() + " " + r.end());
});
}
});
}
private void calculateLookupTable() {
sequentView.update(null);
cursorPosition.clear();
LogicPrinter.PosTableStringBackend backend = sequentView.getBackend();
SequentPrintFilter filter = new IdentitySequentPrintFilter();
filter.setSequent(selectedGoalNodeToShow.get().getData().getNode().sequent());
for (int i = 0; i < sequentView.getText().length(); i++) {
try {
Range range = backend.getPositionTable().rangeForIndex(i, sequentView.getLength());
PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(i, filter);
if (pis != null && pis.getPosInOccurrence() != null) {
Term term = pis.getPosInOccurrence().subTerm();
cursorPosition.put(pis.getPosInOccurrence(), range);
}
} catch (NullPointerException e) {
e.printStackTrace();
}
}
}
public void showGoalOptions(MouseEvent actionEvent) {
Node n = (Node) actionEvent.getTarget();
goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
}
public void startMatch() {
Matchings matchings = MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true);
ObservableList<Map<String, MatchPath>> resultlist = FXCollections.observableArrayList(matchings);
//If no matchings found, add "No matchings found"
if (resultlist.isEmpty()) {
matchingsView.setVisible(false);
nomatchings.setVisible(true);
} else {
nomatchings.setVisible(false);
matchingsView.setItems(resultlist);
matchingsView.setVisible(true);
}
}
//alle aktuellen nicht geschlossene Ziele -> alle leaves später (open+closed)
private final ListProperty<GoalNode<KeyData>> goals = new SimpleListProperty<>(this, "goals", FXCollections.observableArrayList());
private final ListProperty<GoalNode<KeyData>> matchingresults = new SimpleListProperty<>(this, "matchingresults", FXCollections.observableArrayList());
public ObservableList<GoalNode<KeyData>> getMatchingresults() {
return matchingresults.get();
}
public ObservableList<Map<String, MatchPath>> getResults() {
return results.get();
}
public ListProperty<Map<String, MatchPath>> resultsProperty() {
return results;
}
public void setResults(ObservableList<Map<String, MatchPath>> results) {
this.results.set(results);
}
private final ListProperty<Map<String, MatchPath>> results = new SimpleListProperty<>(this, "results", FXCollections.observableArrayList());
//sicht user selected
private final ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShow = new SimpleObjectProperty<>(this, "selectedGoalNodeToShow");
public ObservableList<GoalNode<KeyData>> getGoals() {
return goals.get();
}
public ListProperty<GoalNode<KeyData>> goalsProperty() {
return goals;
}
public void setGoals(ObservableList<GoalNode<KeyData>> goals) {
this.goals.set(goals);
}
public GoalNode<KeyData> getSelectedGoalNodeToShow() {
return selectedGoalNodeToShow.get();
}
public ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShowProperty() {
return selectedGoalNodeToShow;
}
public void setSelectedGoalNodeToShow(GoalNode<KeyData> selectedGoalNodeToShow) {
this.selectedGoalNodeToShow.set(selectedGoalNodeToShow);
}
public ListView<Map<String, MatchPath>> getMatchingsView() {
return matchingsView;
}
public void setMatchingsView(ListView<Map<String, MatchPath>> matchingsView) {
this.matchingsView = matchingsView;
}
public ListProperty<GoalNode<KeyData>> matchingresultsProperty() {
return matchingresults;
}
public void setMatchingresults(ObservableList<GoalNode<KeyData>> matchingresults) {
this.matchingresults.set(matchingresults);
}
/**
* Cells for GoalView
*/
private class GoalNodeListCell extends ListCell<GoalNode<KeyData>> {
public GoalNodeListCell(ListView<GoalNode<KeyData>> goalNodeListView) {
itemProperty().addListener(this::update);
goalOptionsMenu.selectedViewOptionProperty().addListener(this::update);
}
private void update(Observable observable) {
if (getItem() == null) {
setText("");
return;
}
KeyData item = getItem().getData();
String text = "n/a";
if (goalOptionsMenu.getSelectedViewOption() != null) {
text = goalOptionsMenu.getSelectedViewOption().getText(item);
}
//setStyle("-fx-font-size: 12pt;");
setText(text);
}
}
}
package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.collect.BiMap;
import com.google.common.collect.HashBiMap;
import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader;
import javafx.scene.Parent;
import javafx.scene.Scene;
import javafx.scene.control.*;
import javafx.stage.Modality;
import javafx.stage.Stage;
import javafx.stage.StageStyle;
import org.dockfx.DockNode;
import java.util.function.Function;
public class SequentOptionsMenu extends ContextMenu {
private final InspectionModel model;
@FXML
private MenuItem openSequentMatcher;
public SequentOptionsMenu(InspectionModel model) {
Utils.createWithFXML(this);
this.model = model;
openSequentMatcher.setOnAction(new EventHandler<ActionEvent>() {
@Override
public void handle(ActionEvent event) {
try {
SequentMatcher root1 = new SequentMatcher();
root1.setGoals(model.getGoals());
root1.setSelectedGoalNodeToShow(model.getSelectedGoalNodeToShow());
root1.getStyleClass().add("sequent-view");
Stage stage = new Stage();
stage.setTitle("Sequent Matcher");
Scene scene = new Scene(root1);
scene.getStylesheets().addAll(
// ProofScriptDebugger.class.getClass().getResource("debugger-ui.css").toExternalForm()
getClass().getResource("/edu/kit/iti/formal/psdbg/gui/debugger-ui.css")
.toExternalForm());
stage.setScene(scene);
stage.show();
} catch (Exception e) {
e.printStackTrace();
System.out.println(e);
}
}
});
}
}
\ No newline at end of file
...@@ -66,6 +66,7 @@ public class SequentView extends CodeArea { ...@@ -66,6 +66,7 @@ public class SequentView extends CodeArea {
int insertionPoint = hit.getInsertionIndex(); int insertionPoint = hit.getInsertionIndex();
try { try {
PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter); PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
if (pis != null) { if (pis != null) {
Range r = backend.getPositionTable().rangeForIndex(insertionPoint, getLength()); Range r = backend.getPositionTable().rangeForIndex(insertionPoint, getLength());
hightlightRange(r.start(), r.end()); hightlightRange(r.start(), r.end());
...@@ -134,6 +135,7 @@ public class SequentView extends CodeArea { ...@@ -134,6 +135,7 @@ public class SequentView extends CodeArea {
filter = new IdentitySequentPrintFilter(); filter = new IdentitySequentPrintFilter();
filter.setSequent(sequent); filter.setSequent(sequent);
ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter()); ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter());
this.backend = new LogicPrinter.PosTableStringBackend(80); this.backend = new LogicPrinter.PosTableStringBackend(80);
...@@ -208,7 +210,7 @@ public class SequentView extends CodeArea { ...@@ -208,7 +210,7 @@ public class SequentView extends CodeArea {
Matchings m = MatcherFacade.matches(pattern, node.get().sequent(), true); Matchings m = MatcherFacade.matches(pattern, node.get().sequent(), true);
if (m.size() == 0) return false; if (m.size() == 0) return false;
Map<String, MatchPath> va = m.first(); Map<String, MatchPath> va = m.first();
System.out.println(va);//TODO remove //System.out.println(va);//TODO remove
for (MatchPath mp : va.values()) { for (MatchPath mp : va.values()) {
System.out.println(mp.pio()); System.out.println(mp.pio());
highlightTerm(mp.pio()); highlightTerm(mp.pio());
...@@ -226,4 +228,8 @@ public class SequentView extends CodeArea { ...@@ -226,4 +228,8 @@ public class SequentView extends CodeArea {
Range r = backend.getInitialPositionTable().rangeForPath(path); Range r = backend.getInitialPositionTable().rangeForPath(path);
setStyle(r.start(), r.end(), Collections.singleton("search-highlight")); setStyle(r.start(), r.end(), Collections.singleton("search-highlight"));
} }
public LogicPrinter.PosTableStringBackend getBackend() {
return backend;
}
} }
...@@ -34,7 +34,7 @@ ...@@ -34,7 +34,7 @@
<SectionPane title="Sequent"> <SectionPane title="Sequent">
<headerRight> <headerRight>
<Button> <Button onMouseClicked="#showSequentOptions">
<graphic> <graphic>
<MaterialDesignIconView glyphName="WRENCH"/> <MaterialDesignIconView glyphName="WRENCH"/>
</graphic> </graphic>
......
<?xml version="1.0" encoding="UTF-8"?>
<?import javafx.geometry.Insets?>
<?import javafx.scene.control.Button?>
<?import javafx.scene.control.Label?>
<?import javafx.scene.control.ListView?>
<?import javafx.scene.control.SplitPane?>
<?import javafx.scene.control.TextArea?>
<?import javafx.scene.layout.VBox?>
<?import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView?>
<?import edu.kit.iti.formal.psdbg.gui.controls.SectionPane?>
<?import javafx.scene.layout.Pane?>
<?import edu.kit.iti.formal.psdbg.gui.controls.SequentView?>
<fx:root xmlns="http://javafx.com/javafx/8.0.121" xmlns:fx="http://javafx.com/fxml/1"
type="edu.kit.iti.formal.psdbg.gui.controls.SequentMatcher">
<center>
<SplitPane orientation="VERTICAL">
<SectionPane title="Current Goals">
<headerRight>
<Button onMouseClicked="#showGoalOptions">
<graphic>
<MaterialDesignIconView glyphName="WRENCH"/>
</graphic>
</Button>
</headerRight>
<center>
<VBox prefHeight="5" prefWidth="1150.0">
<ListView fx:id="goalView"/>
</VBox>
</center>
</SectionPane>
<SplitPane dividerPositions="0.4189895470383275" prefHeight="500" prefWidth="800">
<SectionPane title="Sequent" minHeight="0.0" minWidth="0.0" prefHeight="633.0"
prefWidth="341.0">
<center>
<SequentView fx:id="sequentView"/>
</center>
</SectionPane>
<SplitPane dividerPositions="0.28551136363636365" layoutX="11.0" layoutY="12.0"
orientation="VERTICAL" prefHeight="706.0" prefWidth="641.0">
<VBox prefHeight="293.0">
<Label text="Matching Pattern"/>
<TextArea fx:id="matchpattern" minHeight="0.0" minWidth="0.0" prefHeight="159.0"
prefWidth="639.0"
/>
<Button mnemonicParsing="false" text="Start Matching"
onMouseClicked="#startMatch"/>
</VBox>
<VBox prefHeight="349.0">
<Label text="Matches"/>
<Pane>
<Label fx:id ="nomatchings" text="No matchings found" visible="false"/>
<ListView fx:id="matchingsView" prefWidth="800"/>
</Pane>
</VBox>
</SplitPane>
</SplitPane>
</SplitPane>
</center>
<padding>
<Insets bottom="25.0" left="25.0" right="25.0" top="25.0"/>
</padding>
</fx:root>
<?xml version="1.0" encoding="UTF-8"?>
<?import javafx.scene.control.*?>
<fx:root xmlns="http://javafx.com/javafx"
xmlns:fx="http://javafx.com/fxml"
prefHeight="400.0" prefWidth="600.0" type="javafx.scene.control.ContextMenu">
<items>
<MenuItem fx:id="openSequentMatcher" text="Open Sequent Matcher"/>
</items>
</fx:root>
\ No newline at end of file
...@@ -242,9 +242,28 @@ ...@@ -242,9 +242,28 @@
-fx-fill: black; -fx-fill: black;
.sequent-highlight { .sequent-highlight {
-rtfx-background-color: @base0; -rtfx-background-color: @base1;
-fx-fill: black; -fx-fill: black;
} }
.search-highlight {
-rtfx-background-color: @base02;
-fx-underline: true;
-rtfx-underline: true;
-fx-fill: darkred;
}
}
.sequent-highlight {
-rtfx-background-color: @base1;
-fx-fill: black;
}
.search-highlight {
-rtfx-background-color: @base02;
-fx-underline: true;
-rtfx-underline: true;
-fx-fill: darkred;
} }
.closed-sequent-view { .closed-sequent-view {
......
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