Userinteraction Draft

rt-key/src/main/java/edu/kit/iti/formal/psdbg/ValueInjector.java

@@ -13,17 +13,17 @@ import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import edu.kit.iti.formal.psdbg.interpreter.data.TermValue;
+import javafx.scene.Scene;
+import javafx.stage.Stage;
 import lombok.RequiredArgsConstructor;
 import lombok.Value;
 
 import java.io.StringReader;
 import java.lang.annotation.Retention;
+import java.lang.reflect.Field;
 import java.lang.reflect.Method;
 import java.math.BigInteger;
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
 
 /**
  * @author Alexander Weigl
@@ -86,8 +86,8 @@ public class ValueInjector {
         vi.addConverter(Long.TYPE, Long::parseLong);
         vi.addConverter(Double.TYPE, Double::parseDouble);
         vi.addConverter(Float.TYPE, Float::parseFloat);
-        vi.addConverter(BigInteger.class,Integer.class, (BigInteger b) -> b.intValue());
-        vi.addConverter(BigInteger.class,Integer.TYPE, (BigInteger b) -> b.intValue());
+        vi.addConverter(BigInteger.class, Integer.class, (BigInteger b) -> b.intValue());
+        vi.addConverter(BigInteger.class, Integer.TYPE, (BigInteger b) -> b.intValue());
 
         return vi;
     }
@@ -111,7 +111,7 @@ public class ValueInjector {
                 return s.getTerm();
             } else {
                 NamespaceSet nss = null;
-                if(s.getNs() !=null) {
+                if (s.getNs() != null) {
                     nss = s.getNs();
 
                 }
@@ -149,7 +149,7 @@ public class ValueInjector {
                 ns = node.proof().getNamespaces();
             }
 
-            if(additionalNamespace!=null) {
+            if (additionalNamespace != null) {
                 ns = ns.copy();
                 ns.add(additionalNamespace);
             }
@@ -160,7 +160,8 @@ public class ValueInjector {
         }
     }
 
-    @Value public static class SortConverter implements Converter<String, Sort>{
+    @Value
+    public static class SortConverter implements Converter<String, Sort> {
         private Proof proof;
 
         @Override
@@ -241,12 +242,43 @@ public class ValueInjector {
         final Object val = args.get(meta.getName());
         if (val == null) {
             if (meta.isRequired()) {
-                throw new ArgumentRequiredException(
-                        String.format("Argument %s:%s is required, but %s was given. " +
-                                        "For comamnd class: '%s'",
-                                meta.getName(), meta.getField().getType(), val,
-                                meta.getCommand().getClass()), meta);
+
+                //TODO MissingInstWindow:
+                String userinput = "p -> q";
+                DefaultTermParser dtp = new DefaultTermParser();
+                TermConverter tc = (TermConverter) getConverter(String.class, Term.class);
+                Term t;
+                try {
+                    t = tc.convert(userinput);
+                } catch (ParserException pe) {
+                    System.out.println("edu/kit/iti/formal/psdbg/ValueInjector.java:250 ParserException");
+                    throw new ArgumentRequiredException(
+                            String.format("Argument %s:%s is required, but %s was given. " +
+                                            "For comamnd class: '%s'",
+                                    meta.getName(), meta.getField().getType(), val,
+                                    meta.getCommand().getClass()), meta);
+                }
+
+                //TODO: inject t into meta?
+                meta.setRequired(false);
+                args.put("#2", t);
+                Object valnew = args.get(meta.getName());
+
+                Object value = convert(meta, valnew);
+                try {
+                    //if (meta.getType() != value.getClass())
+                    //    throw new ConversionException("The typed returned '" + val.getClass()
+                    //            + "' from the converter mismtached with the
+                    // type of the field " + meta.getType(), meta);
+                    meta.getField().set(obj, value);
+
+                } catch (IllegalAccessException e) {
+                    throw new InjectionReflectionException("Could not inject values via reflection",
+                            e, meta);
+                }
             }
+
+
         } else {
             Object value = convert(meta, val);
             try {
@@ -255,6 +287,7 @@ public class ValueInjector {
                 //            + "' from the converter mismtached with the
                 // type of the field " + meta.getType(), meta);
                 meta.getField().set(obj, value);
+
             } catch (IllegalAccessException e) {
                 throw new InjectionReflectionException("Could not inject values via reflection",
                         e, meta);
@@ -282,24 +315,24 @@ public class ValueInjector {
     /**
      * Registers the given converter for the specified class.
      *
-     * @param conv  a converter for the given class
-     * @param <T>   an arbitrary type
+     * @param conv a converter for the given class
+     * @param <T>  an arbitrary type
      */
-    public <T,R> void addConverter(Class<T> from, Class<R> to, Converter<T,R> conv) {
-        converters.add(new ConverterWrapper<T,R>(from, to, conv));
+    public <T, R> void addConverter(Class<T> from, Class<R> to, Converter<T, R> conv) {
+        converters.add(new ConverterWrapper<T, R>(from, to, conv));
     }
 
-    public <R> void addConverter(Class<R> to, Converter<String,R> conv) {
+    public <R> void addConverter(Class<R> to, Converter<String, R> conv) {
         addConverter(String.class, to, conv);
     }
 
-    public <T,R> void addConverter(Converter<T,R> conv) {
+    public <T, R> void addConverter(Converter<T, R> conv) {
         Method[] ms = conv.getClass().getMethods();
         for (Method m : ms) {
             if (m.getParameterCount() == 1) {
                 Class<T> t = (Class<T>) m.getParameterTypes()[0];
                 Class<R> c = (Class<R>) m.getReturnType();
-                addConverter(t,c, conv);
+                addConverter(t, c, conv);
             }
         }
 
@@ -307,26 +340,27 @@ public class ValueInjector {
 
     /**
      * Finds a converter for the given class.
+     *
      * @return null or a suitable converter (registered) converter for the requested class.
      */
     @SuppressWarnings("unchecked")
-    public <T,R> Converter<T,R> getConverter(Class<T> from, Class<R> to) {
-        for (ConverterWrapper c: converters) {
-                if(c.getFrom().equals(from) && c.getTo().equals(to))
-                    return c.getConverter();
-       }
+    public <T, R> Converter<T, R> getConverter(Class<T> from, Class<R> to) {
+        for (ConverterWrapper c : converters) {
+            if (c.getFrom().equals(from) && c.getTo().equals(to))
+                return c.getConverter();
+        }
         throw new RuntimeException("Could not find a suitable converter for types " + from + " to " + to);
     }
 
 
     @Value
-    private static class ConverterWrapper<T,R> {
+    private static class ConverterWrapper<T, R> {
         Class<T> from;
         Class<R> to;
-        Converter<T,R> converter;
+        Converter<T, R> converter;
     }
 
-    interface  Converter<T, R> {
+    interface Converter<T, R> {
         R convert(T o) throws Exception;
     }
 }

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java

@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.interpreter.funchdl;
 
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
+import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.PosInTerm;
@@ -12,6 +13,7 @@ import de.uka.ilkd.key.macros.scripts.ScriptException;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.RuleAppIndex;
+import de.uka.ilkd.key.proof.SVInstantiationException;
 import de.uka.ilkd.key.proof.rulefilter.TacletFilter;
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.Taclet;
@@ -26,14 +28,30 @@ 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.VariableNotDefinedException;
 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 javafx.collections.FXCollections;
+import javafx.event.ActionEvent;
+import javafx.event.EventHandler;
+import javafx.geometry.Pos;
+import javafx.scene.Scene;
+import javafx.scene.control.Button;
+import javafx.scene.control.ListView;
+import javafx.scene.control.TextField;
+import javafx.scene.layout.VBox;
+import javafx.stage.Modality;
+import javafx.stage.Stage;
+import javafx.stage.StageStyle;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
 
+import java.io.IOException;
 import java.util.*;
+import java.util.concurrent.ConcurrentMap;
+import java.util.concurrent.TimeUnit;
 
 /**
  * @author Alexander Weigl
@@ -49,6 +67,8 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
     @Getter
     private final Map<String, Rule> rules;
 
+    private Scanner scanner = new Scanner(System.in);
+
     public RuleCommandHandler() {
         this(new HashMap<>());
     }
@@ -140,36 +160,52 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
             }
         } catch (ScriptException e) {
 
-            //TODO: adding UserinteractionWindow
-            /*TODO: possible cases not applicable, because
-                command not recognized (can be ignored)
+            boolean exceptionsolved = false;
 
-                command multiple matches -> need more specification with on + formula
-                    if(e.getMessage().equals("More than one applicable occurrence")) {
-                    //TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 121)
+            if (e instanceof ScriptException.IndistinctFormula) {
+                List<TacletApp> matchingapps = ((ScriptException.IndistinctFormula) e).getMatchingApps();
 
-                ImmutableList<TacletApp> allApps = c.findAllTacletApps(cc, state);
-                List<TacletApp> matchingApps = c.filterList(cc, allApps);
+                //IndistinctPrompt prompt = new IndistinctPrompt(matchingapps);
+                //TacletApp chosen = prompt.getChosen();
 
-                    //TODO: (re)apply completed TacletApp
+                int inputindex = -1;
 
-                    //TODO: insert into script
+                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 = System.in.read(new byte[System.in.available()]);
 
+                    } catch (IOException ioe) {
+                        System.out.println("No valid input");
+                        continue;
+                    }
+                    if (0 <= inputindex && inputindex <= matchingapps.size() - 1) {
+                        System.out.println("Acceptable inputindex = " + inputindex);
+                        break;
+                    } else {
+                        System.out.println("No valid input");
+                    }
                 }
+                TacletApp chosenApp = matchingapps.get(inputindex);
 
+                TacletInstantiationModel tim = new TacletInstantiationModel(chosenApp, data.getGoal().sequent(), data.getGoal().getLocalNamespaces(), null, data.getGoal());
+                try {
+                    TacletApp newTA = tim.createTacletApp();
+                    newTA.execute(data.getGoal(), data.getProof().getServices());
 
-                command not complete -> missig parameters
-                solution:
-                if(e.getMessage().equals("Not a unique \\assumes instantiation")) {
-                    //TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 56)
-                    ImmutableList<TacletApp> assumesCandidates = theApp.findIfFormulaInstantiations(state.getFirstOpenGoal().sequent(), proof.getServices());
+                    int linenr = call.getStartPosition().getLineNumber();
+                    exceptionsolved = true;
+                } catch (SVInstantiationException svie) {
 
-                    //TODO: (re)apply completed TacletApp
+                }
+            }
+            if (exceptionsolved) return;
 
-                    //TODO: insert into script
 
-                }
-             */
             if (interpreter.isStrictMode()) {
                 throw new ScriptCommandNotApplicableException(e, c, map);
             } else {
@@ -195,4 +231,66 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
         return params;
     }
 
+    private class IndistinctPrompt {
+        private final TacletApp chosen = null;
+
+        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;
+                    }
+
+                }
+            });
+
+            final VBox layout = new VBox(10);
+            layout.setAlignment(Pos.CENTER_RIGHT);
+            layout.setStyle("-fx-background-color: azure; -fx-padding: 10;");
+            layout.getChildren().setAll(
+                    listView,
+                    textField,
+                    submitButton
+            );
+
+            dialog.setScene(new Scene(layout));
+            dialog.showAndWait();
+
+        }
+
+        private TacletApp getChosen() {
+            return chosen;
+        }
+    }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/VariableAssignmentWindow.java

@@ -31,6 +31,9 @@ public class VariableAssignmentWindow extends BorderPane {
     @FXML
     TableView special_tableView;
 
+    @FXML
+    TableView history;
+
     @FXML
     TextArea match_variables;
 
@@ -49,6 +52,7 @@ public class VariableAssignmentWindow extends BorderPane {
 
     private List<VariableModel> matchlist_declarative = new ArrayList<>();
     private List<VariableModel> matchlist_special = new ArrayList<>();
+    private List<VariableModel> historylist = new ArrayList<>();
 
     private Evaluator evaluator;
 
@@ -177,11 +181,14 @@ public class VariableAssignmentWindow extends BorderPane {
         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_special = getVariableMatches(specialModel);
@@ -195,6 +202,20 @@ public class VariableAssignmentWindow extends BorderPane {
         if (matchlist_special != null) System.out.println("matchlist_special = " + matchlist_special.size());
     }
 
+
+    @FXML
+    private void evaluate() {
+        matchexp = match_variables.getText();
+        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)));
+    }
+
     /**
      * Highlight all varlist items in the view
      *

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/userinteraction/IndistinctWindow.java

+package edu.kit.iti.formal.psdbg.gui.controls.userinteraction;
+
+import de.uka.ilkd.key.rule.TacletApp;
+import edu.kit.iti.formal.psdbg.gui.controls.Utils;
+import javafx.collections.FXCollections;
+import javafx.fxml.FXML;
+import javafx.scene.control.ListView;
+import javafx.scene.control.TextField;
+import javafx.scene.layout.BorderPane;
+import javafx.stage.Stage;
+import lombok.Getter;
+
+import java.io.IOException;
+import java.util.InputMismatchException;
+import java.util.List;
+
+public class IndistinctWindow extends BorderPane {
+
+    @Getter
+    private TacletApp chosen;
+    private List<TacletApp> matchingapps;
+    @FXML
+    ListView listView;
+
+    @FXML
+    TextField input;
+
+    public IndistinctWindow(List<TacletApp> matchingapps) {
+        Utils.createWithFXML(this);
+        this.matchingapps = matchingapps;
+        listView = new ListView(FXCollections.observableArrayList(matchingapps));
+    }
+
+    @FXML
+    private void accept() {
+        String userinput = input.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()) {
+            chosen = matchingapps.get(index);
+        } else {
+            System.out.println("Invalid input!");
+            return;
+        }
+
+    }
+
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/userinteraction/MissingInstWindow.java

+package edu.kit.iti.formal.psdbg.gui.controls.userinteraction;
+
+import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
+import de.uka.ilkd.key.parser.DefaultTermParser;
+import javafx.fxml.FXML;
+import javafx.scene.control.TextField;
+import javafx.scene.text.Text;
+
+
+public class MissingInstWindow {
+    @FXML
+    Text commandname;
+
+    @FXML
+    Text requiredInput;
+
+    @FXML
+    TextField input;
+
+    private ProofScriptArgument meta;
+
+    public MissingInstWindow(ProofScriptArgument meta) {
+        this.meta = meta;
+        commandname.setText(meta.getCommand().getClass().toString());
+        requiredInput.setText(meta.getField().getType().toString());
+    }
+
+    public void accept() {
+        DefaultTermParser parser = new DefaultTermParser();
+
+
+    }
+}

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/applyEq/script.kps

-script interaction() {
+script mock_interaction() {
     impRight;
     andLeft;
     andLeft;
-    // apply 'applyEq' on 'a' in 'a = d'
+    applyEq;
 }
 
-script mock_interaction() {
+script interaction() {
     impRight;
     andLeft;
     andLeft;
-    applyEq;
+    // apply 'applyEq' on 'a' in 'a = d'
 }
 
+
+
 script mock_interaction_1() {
     impRight;
     andLeft;

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps

+script interaction() {
+    impRight;
+    cut;
+}
+
 script empty(){
 
 }

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/VariableAssignmentWindow.fxml

@@ -4,6 +4,7 @@
 <?import javafx.scene.control.*?>
 
 <?import javafx.scene.layout.BorderPane?>
+<?import javafx.scene.layout.HBox?>
 <fx:root xmlns="http://javafx.com/javafx"
          xmlns:fx="http://javafx.com/fxml"
          type="edu.kit.iti.formal.psdbg.gui.controls.VariableAssignmentWindow"
@@ -19,13 +20,18 @@
                 />
             </center>
             <bottom>
-                <Button mnemonicParsing="false" text="Start Matching"
-                        onMouseClicked="#startMatch"/>
+                <HBox>
+                    <Button mnemonicParsing="false" text="Start Matching"
+                            onMouseClicked="#startMatch"/>
+                    <Button mnemonicParsing="false" text="Evaluate"
+                            onMouseClicked="#evaluate"/>
+                </HBox>
+
             </bottom>
         </BorderPane>
     </top>
     <center>
-        <TabPane>
+        <TabPane tabClosingPolicy="UNAVAILABLE">
             <tabs>
                 <Tab text="Script Variables">
                     <TableView fx:id="declarative_tableView"></TableView>
@@ -33,6 +39,9 @@
                 <Tab text="KeY Control Variables">
                     <TableView fx:id="special_tableView"></TableView>
                 </Tab>
+                <Tab text="History">
+                    <TableView fx:id="history_tableView"></TableView>
+                </Tab>
             </tabs>
         </TabPane>
     </center>

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/userinteraction/IndistinctWindow.fxml

+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import java.lang.*?>
+<?import java.util.*?>
+<?import javafx.scene.*?>
+<?import javafx.scene.control.*?>
+<?import javafx.scene.layout.*?>
+
+<?import javafx.scene.text.Text?>
+<fx:root type="javafx.scene.layout.BorderPane" xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane"
+         xmlns="http://javafx.com/javafx/8.0.112">
+    <top>
+        <ListView fx:id="listview"></ListView>
+    </top>
+
+    <center>
+        <TextField fx:id="input"></TextField>
+    </center>
+    <bottom>
+        <Button text="Apply" onAction="#accept"></Button>
+    </bottom>
+</fx:root>
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/userinteraction/MissingInstWindow.fxml

+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import java.lang.*?>
+<?import java.util.*?>
+<?import javafx.scene.*?>
+<?import javafx.scene.control.*?>
+<?import javafx.scene.layout.*?>
+
+<?import javafx.scene.text.Text?>
+<?import javafx.geometry.Insets?>
+<fx:root type="javafx.scene.layout.BorderPane" xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane"
+         xmlns="http://javafx.com/javafx/8.0.112">
+    <top>
+        <Text fx:id="commandname"></Text>
+    </top>
+
+    <center>
+        <GridPane alignment="center" hgap="10" vgap="10">
+            <padding>
+                <Insets top="25" right="25" bottom="25" left="25"/>
+            </padding>
+            <Text fx:id="requiredInput" GridPane.columnIndex="0"
+                  GridPane.rowIndex="0"></Text>
+
+
+            <TextField fx:id="input" GridPane.columnIndex="1"
+                       GridPane.rowIndex="0"></TextField>
+
+        </GridPane>
+    </center>
+    <bottom>
+        <Button text="Apply" onAction="#accept"></Button>
+    </bottom>
+</fx:root>