Commit 8346bfc8 authored by Lulu Luong's avatar Lulu Luong

merge with master

parent fbfe9ac5
Pipeline #33845 passed with stages
in 2 minutes and 17 seconds
......@@ -211,7 +211,7 @@ public interface ASTTraversal<T> extends Visitor<T> {
}
@Override
default T visit(DerivableCase derivableCase){
default T visit(DerivableCase derivableCase) {
derivableCase.getExpression().accept(this);
derivableCase.getBody().accept(this);
return null;
......
......@@ -414,8 +414,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
Expression pattern = (Expression) ctx.derivableExpression.accept(this);
((DerivableCase) cs).setExpression(pattern);
pattern.setParent(cs);
} else
{
} else {
cs = new GuardedCaseStatement();
Expression<ParserRuleContext> guard = (Expression<ParserRuleContext>) ctx.expression().accept(this);
((GuardedCaseStatement) cs).setGuard(guard);
......
......@@ -7,13 +7,13 @@ import lombok.NoArgsConstructor;
@Data
@NoArgsConstructor
public class DerivableCase extends CaseStatement{
public class DerivableCase extends CaseStatement {
private Expression expression;
public DerivableCase(Statements copy, Expression copy1) {
super(copy);
this.expression=copy1;
this.expression = copy1;
}
@Override
......
......@@ -43,7 +43,9 @@ import lombok.Setter;
public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
//private Signature signature = new Signature();
private Expression pattern;
@Deprecated @Getter @Setter
@Deprecated
@Getter
@Setter
private boolean isDerivable = false;
@Deprecated
private Expression derivableTerm;
......
......@@ -95,15 +95,15 @@ public class KeYProofFacade {
pma = KeYApi.loadFromKeyFile(problemFile);
List<Contract> contracts = pma.getProofContracts();
contracts.forEach(contract1 -> {
if(contract.get().getName().equals(contract1.getName())){
contractProperty().set(contract1);
if (contract.get().getName().equals(contract1.getName())) {
contractProperty().set(contract1);
}
});
if(contract.get() != null){
try{
if (contract.get() != null) {
try {
activateContract(contract.get());
}catch (ProofInputException pie){
} catch (ProofInputException pie) {
throw new ProofInputException("Contract not reloadable.", pie.getCause());
}
}
......
......@@ -14,6 +14,7 @@ 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");
}
......
......@@ -67,7 +67,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
State<KeyData> state = interpreter.getCurrentState();
//multiple goals exist
if(state.getGoals().size() > 1) {
if (state.getGoals().size() > 1) {
throw new IllegalStateException("Multiple open goals: Please use a selector.");
/*
//TODO: Utils showWarning
......
......@@ -62,7 +62,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
Proof proof = kd.getData().getProof();
TermValue tv = (TermValue) pattern.getData();
Term term = tv.getTerm();
if(term == null) {
if (term == null) {
Services services = kd.getData().getProof().getServices();
try {
term = new TermBuilder(services.getTermFactory(), services).parseTerm(tv.getTermRepr());
......@@ -96,10 +96,10 @@ public class KeYMatcher implements MatcherApi<KeyData> {
if (isDerivable) {
//find the open goal node
Goal toSet= null;
if(goalList.head().node().isClosed()){
Goal toSet = null;
if (goalList.head().node().isClosed()) {
toSet = goalList.tail().head();
} else{
} else {
toSet = goalList.head();
}
KeyData kdataNew = new KeyData(kd.getData(), toSet);
......
......@@ -34,7 +34,7 @@ public class KeyMatcherDerivableTest {
System.out.println(proof);
// Assert.assertNotNull(a);
// Assert.assertNotNull(a);
Assert.assertEquals(1, proof.getSubtreeGoals(proof.root()).size());
}
......
......@@ -218,8 +218,8 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
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);
if (v.getType() == TypeFacade.ANY_TERM) {
GoalNode<T> newGoalNode = matcherApi.isDerivable(selectedGoal, v);
try {
enterScope(derivableCase);
......@@ -236,7 +236,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
exitScope(derivableCase);
}
} else {
throw new RuntimeException("A derivable expression must contain a term. Received a"+v.getType());
throw new RuntimeException("A derivable expression must contain a term. Received a" + v.getType());
}
}
......
......@@ -191,9 +191,9 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
Operator op = e.getOperator();
Expression expr = e.getExpression();
List<VariableAssignment> exValue = (List<VariableAssignment>) expr.accept(this);
if(exValue.isEmpty()){
if (exValue.isEmpty()) {
return transformTruthValue(Value.TRUE);
}else{
} else {
return transformTruthValue(Value.FALSE);
}
......
......@@ -214,7 +214,7 @@ public class DebuggerMain implements Initializable {
if (stateAfterStmt.getSelectedGoalNode() != null) {
im.setSelectedGoalNodeToShow(stateAfterStmt.getSelectedGoalNode());
} else {
if(goals.size() > 0) {
if (goals.size() > 0) {
im.setSelectedGoalNodeToShow(goals.get(0));
} else {
im.setSelectedGoalNodeToShow(stateBeforeStmt.getSelectedGoalNode());
......@@ -570,7 +570,7 @@ public class DebuggerMain implements Initializable {
iModel.clearHighlightLines();
iModel.getGoals().clear();
iModel.setSelectedGoalNodeToShow(null);
if(chosen != null) {
if (chosen != null) {
FACADE.contractProperty().set(chosen);
}
try {
......@@ -1541,7 +1541,7 @@ public class DebuggerMain implements Initializable {
.stream()
.map(Goal::node)
.collect(Collectors.toSet());
if(sentinels.size() == 0){
if (sentinels.size() == 0) {
sentinels = new LinkedHashSet();
sentinels.add(pnode);
//sentinels.add(stateAfterStmt.get(0).getData().getNode());
......
......@@ -129,7 +129,7 @@ public class InteractiveModeController {
.filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal()))
.collect(Collectors.toList());
if(prunedChildren.size() == 0) {
if (prunedChildren.size() == 0) {
//TODO: add Utils.showInfoD
return;
}
......@@ -162,10 +162,10 @@ public class InteractiveModeController {
//TODO: buggy cuz allstatements of same node removed
//remove statement from cases / script
Statements statements = (cases.get(pruneNode.parent()) == null)? cases.get(pruneNode) : cases.get(pruneNode.parent());
int i = statements.size()-1;
Statements statements = (cases.get(pruneNode.parent()) == null) ? cases.get(pruneNode) : cases.get(pruneNode.parent());
int i = statements.size() - 1;
while(statements.get(i) != pruneStatement && i >= 0) {
while (statements.get(i) != pruneStatement && i >= 0) {
statements.remove(i);
i--;
}
......@@ -362,7 +362,7 @@ public class InteractiveModeController {
ValueInjector valueInjector = ValueInjector.createDefault(kd.getNode());
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
switch (t){
switch (t) {
case MACRO:
MacroCommand.Parameters cc = new MacroCommand.Parameters();
MacroCommand c = new MacroCommand();
......@@ -408,6 +408,7 @@ public class InteractiveModeController {
Class rtclazz = method.getReturnType();
return (T) rtclazz.newInstance();
}
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());
......
package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.Multimap;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.ProofTreeEvent;
import de.uka.ilkd.key.proof.ProofTreeListener;
import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import edu.kit.iti.formal.psdbg.gui.controller.Events;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.dbg.ProofTreeManager;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import javafx.application.Platform;
import javafx.beans.property.*;
import javafx.collections.FXCollections;
......@@ -27,6 +31,7 @@ import javafx.scene.layout.BorderPane;
import javafx.util.StringConverter;
import lombok.*;
import java.util.*;
import java.util.function.Consumer;
......@@ -102,18 +107,17 @@ public class ProofTree extends BorderPane {
}
};
private KeyProofTreeTransformation treeCreation;
private TreeTransformationKey treeCreation;
@Getter
private ScriptTreeTransformation treeScriptCreation;
public ProofTree(DebuggerMain main) {
Utils.createWithFXML(this);
//TODO remove this hack for a better solution
main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> {
treeScriptCreation = new ScriptTreeTransformation(m.getPtreeManager());
});
treeCreation = new KeyProofTreeTransformation(sentinels);
//main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> {
// treeCreation = new TreeTransformationScript(m.getPtreeManager());
//});
treeCreation = new TreeTransformationKey();
treeProof.setCellFactory(this::cellFactory);
......@@ -166,7 +170,7 @@ public class ProofTree extends BorderPane {
if (getTreeProof().getRoot() == null) {
if (root.get() != null) {
TreeItem<TreeNode> item;
if(sentinels.contains(root.get())){
if (sentinels.contains(root.get())) {
item = treeCreation.itemFactory(root.get());
} else {
item = treeCreation.populate("Proof", root.get());
......@@ -220,7 +224,7 @@ public class ProofTree extends BorderPane {
tftc.setConverter(stringConverter);
tftc.itemProperty().addListener((p, o, n) -> {
if (n != null )
if (n != null)
repaint(tftc);
});
return tftc;
......@@ -232,16 +236,16 @@ public class ProofTree extends BorderPane {
Node n = item.node;
tftc.setStyle("");
if (n != null) {
if (n.leaf() && !item.label.contains("CASE") ) {
if (n.isClosed()) {
colorOfNodes.putIfAbsent(n, "lightseagreen");
} else {
colorOfNodes.putIfAbsent(n, "indianred");
}
if (n.leaf() && !item.label.contains("CASE")) {
if (n.isClosed()) {
colorOfNodes.putIfAbsent(n, "lightseagreen");
} else {
colorOfNodes.putIfAbsent(n, "indianred");
}
if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
}
if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
}
}
}
//TODO for Screenshot tftc.setStyle("-fx-font-size: 18pt");
......@@ -350,18 +354,19 @@ public class ProofTree extends BorderPane {
treeProof.refresh();
}
private void expandTreeView(TreeItem<TreeNode> item){
if(item != null && !item.isLeaf()){
private void expandTreeView(TreeItem<TreeNode> item) {
if (item != null && !item.isLeaf()) {
item.setExpanded(true);
for(TreeItem<TreeNode> child:item.getChildren()){
for (TreeItem<TreeNode> child : item.getChildren()) {
expandTreeView(child);
}
}
}
private void collapseTreeView(TreeItem<TreeNode> item){
if(item != null && !item.isLeaf()){
private void collapseTreeView(TreeItem<TreeNode> item) {
if (item != null && !item.isLeaf()) {
item.setExpanded(false);
for(TreeItem<TreeNode> child:item.getChildren()){
for (TreeItem<TreeNode> child : item.getChildren()) {
collapseTreeView(child);
}
}
......@@ -385,8 +390,9 @@ public class ProofTree extends BorderPane {
return self1;
}
protected TreeItem<TreeNode> itemFactory(Node n, String label) {
if(label.equals("")){
if (label.equals("")) {
return itemFactory(n);
} else {
return new TreeItem<>(new TreeNode(label, n));
......@@ -440,10 +446,10 @@ public class ProofTree extends BorderPane {
Node node = n.child(0);
if (n.childrenCount() == 1) {
currentItem.getChildren().add(new TreeItem<>(new TreeNode(node.serialNr() + ": " + toString(node), node)));
while (node.childrenCount() == 1) {
node = node.child(0);
currentItem.getChildren().add(new TreeItem<>(new TreeNode(node.serialNr() + ": " + toString(node), node)));
}
while (node.childrenCount() == 1) {
node = node.child(0);
currentItem.getChildren().add(new TreeItem<>(new TreeNode(node.serialNr() + ": " + toString(node), node)));
}
/*do {
......@@ -481,7 +487,6 @@ public class ProofTree extends BorderPane {
}
@RequiredArgsConstructor
class TreeTransformationScript extends TreeTransformationKey {
final ProofTreeManager<KeyData> manager;
......@@ -544,7 +549,7 @@ public class ProofTree extends BorderPane {
//TODO: Reverse ArrayList in the end or nah?
@Deprecated
public ArrayList<String> getBranchLabels (TreeNode node) {
public ArrayList<String> getBranchLabels(TreeNode node) {
TreeItem<TreeNode> proofTree = create(proof.get());
ArrayList<String> branchlabels = new ArrayList<>();
......@@ -552,7 +557,7 @@ public class ProofTree extends BorderPane {
int i = 0;
branchlabels.set(0, node.label);
while (node != null) {
if(!branchlabels.get(i).equals(node.label)) {
if (!branchlabels.get(i).equals(node.label)) {
i++;
branchlabels.set(i, node.label);
}
......@@ -562,7 +567,7 @@ public class ProofTree extends BorderPane {
return branchlabels;
}
public ArrayList<String> getBranchLabels (Node node) {
public ArrayList<String> getBranchLabels(Node node) {
ArrayList<String> branchlabels = new ArrayList<>();
int i = 0;
......@@ -570,7 +575,7 @@ public class ProofTree extends BorderPane {
branchlabels.set(0, node.getNodeInfo().getBranchLabel());
Node n = node.parent();
while (n != null) {
if(!branchlabels.get(i).equals(n.getNodeInfo().getBranchLabel())) {
if (!branchlabels.get(i).equals(n.getNodeInfo().getBranchLabel())) {
i++;
branchlabels.set(i, n.getNodeInfo().getBranchLabel());
}
......
......@@ -62,7 +62,6 @@ public class TacletContextMenu extends ContextMenu {
FILTER_SCRIPT_COMMANDS.add("script");
}
static {
CLUTTER_RULES.add(new Name("cut_direct_r"));
......@@ -155,7 +154,7 @@ public class TacletContextMenu extends ContextMenu {
}
private void createMacroMenu(Collection<ProofScriptCommand> scriptCommandList, Collection<ProofMacro> macros) {
for(ProofMacro macro : macros){
for (ProofMacro macro : macros) {
final MenuItem item = new MenuItem(macro.getScriptCommandName());
item.setOnAction(event -> {
handleMacroCommandApplication(macro);
......@@ -164,8 +163,8 @@ public class TacletContextMenu extends ContextMenu {
this.scriptCommands.getItems().add(item);
}
for(ProofScriptCommand com : scriptCommandList){
if(!FILTER_SCRIPT_COMMANDS.contains(com.getName())) {
for (ProofScriptCommand com : scriptCommandList) {
if (!FILTER_SCRIPT_COMMANDS.contains(com.getName())) {
final MenuItem item = new MenuItem(com.getName());
item.setOnAction(event -> {
handleCommandApplication(com);
......@@ -288,9 +287,9 @@ public class TacletContextMenu extends ContextMenu {
List<TacletApp> toReturn = new ArrayList<>();
for (int i = 0; i < findTaclets.size(); i++) {
TacletApp tacletApp = findTaclets.get(i);
if(!tacletApp.rule().displayName().startsWith("cut")){
if (!tacletApp.rule().displayName().startsWith("cut")) {
//findTaclets.remove(tacletApp);
// foundCut = true;
// foundCut = true;
toReturn.add(tacletApp);
}
}
......@@ -419,6 +418,7 @@ public class TacletContextMenu extends ContextMenu {
//System.out.println("event = [" + event + "]");
Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence(), goal));
}
private void handleCommandApplication(ProofScriptCommand event) {
Events.fire(new Events.CommandApplicationEvent(event, pos.getPosInOccurrence(), goal));
......
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