Commit 62844d6d authored by Lulu Luong's avatar Lulu Luong

+ tacletapp as scriptcommand

+ evaluator in Varas + History
parent 58e94ba2
Pipeline #39066 passed with stages
in 2 minutes and 39 seconds
...@@ -4,20 +4,24 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; ...@@ -4,20 +4,24 @@ 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.control.instantiation_model.TacletInstantiationModel; import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel;
import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.PosInTerm;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand; import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException; import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.pp.NotationInfo;
import de.uka.ilkd.key.pp.ProgramPrinter;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.RuleAppIndex; import de.uka.ilkd.key.proof.RuleAppIndex;
import de.uka.ilkd.key.proof.SVInstantiationException; import de.uka.ilkd.key.proof.SVInstantiationException;
import de.uka.ilkd.key.proof.rulefilter.TacletFilter; import de.uka.ilkd.key.proof.rulefilter.TacletFilter;
import de.uka.ilkd.key.rule.IfFormulaInstantiation;
import de.uka.ilkd.key.rule.Rule; 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 de.uka.ilkd.key.rule.inst.SVInstantiations;
import edu.kit.iti.formal.psdbg.RuleCommandHelper;
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.IndistinctWindow;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
...@@ -29,8 +33,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; ...@@ -29,8 +33,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
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.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.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.Variable; import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.collections.FXCollections; import javafx.collections.FXCollections;
import javafx.collections.ObservableList; import javafx.collections.ObservableList;
import javafx.event.ActionEvent; import javafx.event.ActionEvent;
...@@ -51,6 +55,8 @@ import org.apache.logging.log4j.LogManager; ...@@ -51,6 +55,8 @@ 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.math.BigInteger;
import java.util.*; import java.util.*;
/** /**
...@@ -158,48 +164,18 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -158,48 +164,18 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
boolean exceptionsolved = false; boolean exceptionsolved = false;
//Exception thown when multiple TacletApp possible
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(); ObservableList<String> obsMatchApps = FXCollections.observableArrayList();
matchingapps.forEach(k -> obsMatchApps.add(k.toString())); int linenr = call.getStartPosition().getLineNumber();
matchingapps.forEach(k -> obsMatchApps.add(tacletAppIntoString(k, kd.getGoal(), linenr)));
//TODO: open window here //TODO: open window here
IndistinctWindow indistinctWindow = new IndistinctWindow(obsMatchApps); IndistinctWindow indistinctWindow = new IndistinctWindow(obsMatchApps);
tacletAppSelectionDialogService.setPane(indistinctWindow); tacletAppSelectionDialogService.setPane(indistinctWindow);
tacletAppSelectionDialogService.showDialog(); tacletAppSelectionDialogService.showDialog();
//IndistinctPrompt prompt = new IndistinctPrompt(matchingapps);
//TacletApp chosen = prompt.getChosen();
/*
int inputindex = -1;
while (true) {
System.out.println("Taclet " + matchingapps.get(0).taclet().displayName() + " is applicable on multiple formulas, " +
"please choose one of the following by entering a number from 0 to " + (matchingapps.size() - 1) + " :");
matchingapps.forEach(k -> System.out.println(k));
System.out.flush();
// User input
try {
inputindex = scanner.nextInt(); //System.in.read();
} catch (InputMismatchException ime) {
System.out.println("InputMismatchException thrown: edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java:176");
continue;
}
if (0 <= inputindex && inputindex <= matchingapps.size() - 1) {
System.out.println("Acceptable inputindex = " + inputindex);
break;
} else {
System.out.println("No valid input");
}
}
*/
try {
tacletAppSelectionDialogService.latch.await();
} catch (InterruptedException ie) {
System.out.println("latch await got interrupted");
}
TacletApp chosenApp = matchingapps.get(tacletAppSelectionDialogService.getUserIndexInput()); TacletApp chosenApp = matchingapps.get(tacletAppSelectionDialogService.getUserIndexInput());
TacletInstantiationModel tim = new TacletInstantiationModel(chosenApp, kd.getGoal().sequent(), kd.getGoal().getLocalNamespaces(), null, kd.getGoal()); TacletInstantiationModel tim = new TacletInstantiationModel(chosenApp, kd.getGoal().sequent(), kd.getGoal().getLocalNamespaces(), null, kd.getGoal());
...@@ -207,7 +183,6 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -207,7 +183,6 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
TacletApp newTA = tim.createTacletApp(); TacletApp newTA = tim.createTacletApp();
newTA.execute(kd.getGoal(), kd.getProof().getServices()); newTA.execute(kd.getGoal(), kd.getProof().getServices());
int linenr = call.getStartPosition().getLineNumber();
exceptionsolved = true; exceptionsolved = true;
} catch (SVInstantiationException svie) { } catch (SVInstantiationException svie) {
...@@ -253,66 +228,57 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -253,66 +228,57 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
return params; return params;
} }
private class IndistinctPrompt { private String tacletAppIntoString(TacletApp tacletApp, Goal g, int linenumber) {
private final TacletApp chosen = null; String tacletAppString = "";
IndistinctPrompt(List<TacletApp> matchingapps) {
final Stage dialog = new Stage();
dialog.setTitle("Select a Tacletapp");
dialog.initStyle(StageStyle.UTILITY);
dialog.initModality(Modality.WINDOW_MODAL);
ListView listView = new ListView(FXCollections.observableArrayList(matchingapps));
final TextField textField = new TextField();
final Button submitButton = new Button("Submit");
submitButton.setDefaultButton(true);
submitButton.setOnAction(new EventHandler<ActionEvent>() {
@Override
public void handle(ActionEvent t) {
String userinput = textField.getText();
if (userinput.equals("")) {
System.out.println("Invalid input!");
return;
}
int index;
try {
index = Integer.parseInt(userinput);
} catch (NumberFormatException e) {
System.out.println("Invalid input!");
return;
}
if (0 < index && index < matchingapps.size()) {
final TacletApp chosen = matchingapps.get(index);
dialog.close();
} else {
System.out.println("Invalid input!");
return;
}
} String tapName = tacletApp.taclet().name().toString();
}); PosInOccurrence pio = tacletApp.posInOccurrence();
SequentFormula seqForm = pio.sequentFormula();
Services keYServices = g.proof().getServices();
Sequent seq = g.sequent();
String sfTerm = printParsableTerm(seqForm.formula(), keYServices);
String onTerm = printParsableTerm(pio.subTerm(), keYServices);
RuleCommand.Parameters params = new RuleCommand.Parameters();
params.formula = seqForm.formula();
params.rulename = tacletApp.taclet().name().toString();
params.on = pio.subTerm();
final VBox layout = new VBox(10); RuleCommandHelper rch = new RuleCommandHelper(g, params);
layout.setAlignment(Pos.CENTER_RIGHT); int occ = rch.getOccurence(tacletApp);
layout.setStyle("-fx-background-color: azure; -fx-padding: 10;");
layout.getChildren().setAll(
listView,
textField,
submitButton
);
dialog.setScene(new Scene(layout));
dialog.showAndWait();
tacletAppString = String.format("%s formula=' %s ' on=' %s ' occ=%d;",
tapName,
sfTerm.trim(),
onTerm.trim(),
occ);
// add missing instantiations
if (!tacletApp.ifInstsComplete()) {
SVInstantiations sv = tacletApp.instantiations();
//TODO:
} }
private TacletApp getChosen() { tacletAppString += String.format("(linenumber = %d)", linenumber);
return chosen;
return tacletAppString;
}
public static String printParsableTerm(Term term, Services services) {
NotationInfo ni = new NotationInfo();
LogicPrinter p = new LogicPrinter(new ProgramPrinter(), ni, services);
ni.refresh(services, false, false);
String termString = "";
try {
p.printTerm(term);
} catch (IOException ioe) {
// t.toString();
} }
termString = p.toString();
return termString;
} }
} }
...@@ -28,7 +28,7 @@ public abstract class TacletAppSelectionDialogService { ...@@ -28,7 +28,7 @@ public abstract class TacletAppSelectionDialogService {
@Getter @Getter
int userIndexInput; int userIndexInput;
public CountDownLatch latch = new CountDownLatch(1); private CountDownLatch latch = new CountDownLatch(1);
public void showDialog() { public void showDialog() {
Platform.runLater(new Runnable() { Platform.runLater(new Runnable() {
...@@ -50,8 +50,6 @@ public abstract class TacletAppSelectionDialogService { ...@@ -50,8 +50,6 @@ public abstract class TacletAppSelectionDialogService {
} }
}); });
stage.showAndWait(); stage.showAndWait();
latch.countDown(); latch.countDown();
} }
}); });
...@@ -62,4 +60,5 @@ public abstract class TacletAppSelectionDialogService { ...@@ -62,4 +60,5 @@ public abstract class TacletAppSelectionDialogService {
userIndexInput = ((IndistinctWindow) pane).getIndexOfSelected(); userIndexInput = ((IndistinctWindow) pane).getIndexOfSelected();
} }
} }
package edu.kit.iti.formal.psdbg.gui.controls; package edu.kit.iti.formal.psdbg.gui.controls;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import edu.kit.iti.formal.psdbg.interpreter.Evaluator; import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException; import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDefinedException;
import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.Expression;
import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral; import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral;
import edu.kit.iti.formal.psdbg.parser.data.Value; import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.Type;
import javafx.collections.FXCollections; import javafx.collections.FXCollections;
import javafx.collections.ObservableList; import javafx.collections.ObservableList;
import javafx.fxml.FXML; import javafx.fxml.FXML;
...@@ -32,7 +28,7 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -32,7 +28,7 @@ public class VariableAssignmentWindow extends BorderPane {
TableView special_tableView; TableView special_tableView;
@FXML @FXML
TableView history; TableView history_tableView;
@FXML @FXML
TextArea match_variables; TextArea match_variables;
...@@ -45,6 +41,8 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -45,6 +41,8 @@ public class VariableAssignmentWindow extends BorderPane {
/** Variables that start with __ **/ /** Variables that start with __ **/
private ObservableList<VariableModel> specialModel; private ObservableList<VariableModel> specialModel;
private ObservableList<VariableModel> historyModel = FXCollections.observableArrayList();
private String matchexp; private String matchexp;
private ScriptEngineManager mgr = new ScriptEngineManager(); private ScriptEngineManager mgr = new ScriptEngineManager();
...@@ -52,7 +50,6 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -52,7 +50,6 @@ public class VariableAssignmentWindow extends BorderPane {
private List<VariableModel> matchlist_declarative = new ArrayList<>(); private List<VariableModel> matchlist_declarative = new ArrayList<>();
private List<VariableModel> matchlist_special = new ArrayList<>(); private List<VariableModel> matchlist_special = new ArrayList<>();
private List<VariableModel> historylist = new ArrayList<>();
private Evaluator evaluator; private Evaluator evaluator;
...@@ -67,6 +64,7 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -67,6 +64,7 @@ public class VariableAssignmentWindow extends BorderPane {
declarative_tableView.setEditable(false); declarative_tableView.setEditable(false);
special_tableView.setEditable(false); special_tableView.setEditable(false);
history_tableView.setEditable(false);
//Table Colums for declarative_tableView //Table Colums for declarative_tableView
TableColumn decl_varCol = new TableColumn("Variable"); TableColumn decl_varCol = new TableColumn("Variable");
...@@ -114,6 +112,30 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -114,6 +112,30 @@ public class VariableAssignmentWindow extends BorderPane {
special_tableView.setItems(specialModel); special_tableView.setItems(specialModel);
special_tableView.getColumns().addAll(spec_varCol, spec_typeCol, spec_valCol); special_tableView.getColumns().addAll(spec_varCol, spec_typeCol, spec_valCol);
//Table Colums for history_tableView
TableColumn hist_varCol = new TableColumn("Variable");
TableColumn hist_typeCol = new TableColumn("Type");
TableColumn hist_valCol = new TableColumn("Value");
//Set Colums width proportional to windows with
hist_varCol.prefWidthProperty().bind(history_tableView.widthProperty().divide(3));
hist_typeCol.prefWidthProperty().bind(history_tableView.widthProperty().divide(3));
hist_valCol.prefWidthProperty().bind(history_tableView.widthProperty().divide(3));
hist_varCol.setCellValueFactory(
new PropertyValueFactory<VariableModel, String>("varname")
);
hist_typeCol.setCellValueFactory(
new PropertyValueFactory<VariableModel, String>("vartype")
);
hist_valCol.setCellValueFactory(
new PropertyValueFactory<VariableModel, String>("varval")
);
history_tableView.setItems(historyModel);
history_tableView.getColumns().addAll(hist_varCol, hist_typeCol, hist_valCol);
//Row factory added //Row factory added
declarative_tableView.setRowFactory(tv -> new TableRow<VariableModel>() { declarative_tableView.setRowFactory(tv -> new TableRow<VariableModel>() {
@Override @Override
...@@ -180,19 +202,9 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -180,19 +202,9 @@ public class VariableAssignmentWindow extends BorderPane {
matchexp = match_variables.getText(); matchexp = match_variables.getText();
if (matchexp.equals("")) return; if (matchexp.equals("")) return;
Value value = evaluator.visit(new StringLiteral(matchexp));
new StringLiteral(matchexp).accept(evaluator);
System.out.println("Value of Evaluator: " + value);
System.out.println("Visit " + new StringLiteral(matchexp).accept(evaluator));
System.out.println("Eval: " + evaluator.eval(new StringLiteral(matchexp)));
/*
matchlist_declarative = getVariableMatches(declarativeModel); matchlist_declarative = getVariableMatches(declarativeModel);
matchlist_special = getVariableMatches(specialModel); matchlist_special = getVariableMatches(specialModel);
*/
highlight(matchlist_declarative); highlight(matchlist_declarative);
highlight(matchlist_special); highlight(matchlist_special);
...@@ -207,13 +219,20 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -207,13 +219,20 @@ public class VariableAssignmentWindow extends BorderPane {
private void evaluate() { private void evaluate() {
matchexp = match_variables.getText(); matchexp = match_variables.getText();
if (matchexp.equals("")) return; if (matchexp.equals("")) return;
Value value;
try {
value = evaluator.eval(Facade.parseExpression(matchexp));
Value value = evaluator.visit(new StringLiteral(matchexp)); VariableModel vm = new VariableModel(matchexp,
value.getType().toString(),
value.getData().toString());
new StringLiteral(matchexp).accept(evaluator); historyModel.add(vm);
System.out.println("Value of Evaluator: " + value); history_tableView.refresh();
System.out.println("Visit " + new StringLiteral(matchexp).accept(evaluator));
System.out.println("Eval: " + evaluator.eval(new StringLiteral(matchexp))); } catch (Exception e) {
System.out.println("No evaluable expression");
}
} }
/** /**
...@@ -269,34 +288,19 @@ public class VariableAssignmentWindow extends BorderPane { ...@@ -269,34 +288,19 @@ public class VariableAssignmentWindow extends BorderPane {
* @return list of matching VariableModels * @return list of matching VariableModels
* *
*/ */
/*
private List<VariableModel> getVariableMatches(ObservableList<VariableModel> varlist) {
private List<VariableModel> getVariableMatches(ObservableList<VariableModel> varlist) {
//Contains numbers
if (!Pattern.compile("[0-9]+").matcher(matchexp).find()) return null;
List<VariableModel> matchlist = new ArrayList<>(); List<VariableModel> matchlist = new ArrayList<>();
//append with \\ to escape '?' of variable declaration -> e.g.: \\?X
String new_var = "\\" + var;
for (VariableModel vm : varlist) { for (VariableModel vm : varlist) {
String boolexpression = matchexp.replaceAll(new_var, vm.getVarval()); if (vm.getVarname().matches(matchexp)) {
try { matchlist.add(vm);
if (vm.getVartype().equals("int")) {
if ((Boolean) engine.eval(boolexpression.toLowerCase())) {
matchlist.add(vm);
}
}
} catch (ScriptException e) {
continue;
} }
} }
return matchlist; return matchlist;
} }
*/
public static class VariableModel { public static class VariableModel {
......
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