argument completion

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

@@ -4,6 +4,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.macros.scripts.EngineState;
 import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
+import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import edu.kit.iti.formal.psdbg.ValueInjector;
@@ -15,7 +16,6 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
-import lombok.Value;
 import org.apache.commons.io.IOUtils;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -25,10 +25,8 @@ import java.io.IOException;
 import java.lang.reflect.Method;
 import java.net.URISyntaxException;
 import java.net.URL;
-import java.util.Collection;
-import java.util.HashMap;
-import java.util.Iterator;
-import java.util.Map;
+import java.util.*;
+import java.util.stream.Stream;
 
 /**
  * This class handles the call of key's proof script commands, e.g. select or auto;
@@ -114,6 +112,17 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
         return (T) rtclazz.newInstance();
     }
 
+    @Override
+    public Stream<String> getArguments(String name) {
+        if (commands.containsKey(name)) {
+            ProofScriptCommand cmd = commands.get(name);
+            List<ProofScriptArgument<?>> seq = (List<ProofScriptArgument<?>>) cmd.getArguments();
+            return seq.stream()
+                    .map((ProofScriptArgument arg) -> arg.getName());//+ " " + arg.getType());
+        }
+        return Stream.of();
+    }
+
     @Override
     public String getHelp(CallStatement call) {
         ProofScriptCommand c = commands.get(call.getCommand());

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/CommandHandler.java

@@ -5,6 +5,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 
 import javax.annotation.Nullable;
+import java.util.Collections;
+import java.util.stream.Stream;
 
 /**
  * @author Alexander Weigl
@@ -44,4 +46,7 @@ public interface CommandHandler<T> {
         return "Help is not implemented for " + getClass().getCanonicalName();
     }
 
+    default Stream<String> getArguments(String name) {
+        return Stream.of();
+    }
 }

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptHandler.java

@@ -14,6 +14,7 @@ import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.stream.Stream;
 
 /**
  * @author Alexander Weigl
@@ -40,6 +41,7 @@ public class ProofScriptHandler implements CommandHandler<Object> {
     public ProofScript getScript(String name) {
         return scripts.get(name);
     }
+
     /**
      * lib/test.test
      *
@@ -104,4 +106,16 @@ public class ProofScriptHandler implements CommandHandler<Object> {
     public void addScripts(List<ProofScript> ast) {
         ast.forEach(script -> scripts.put(script.getName(), script));
     }
+
+    @Override
+    public Stream<String> getArguments(String name) {
+        try {
+            ProofScript ps = find(name);
+            return ps.getSignature().values().stream().map(
+                    arg -> arg.symbol() + ":" + arg.interpreterSort()
+            );
+        } catch (IOException e) {
+            return Stream.of();
+        }
+    }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/ArgumentCompleter.java

 package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
 
+import de.uka.ilkd.key.api.KeYApi;
+import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.exceptions.NoCallHandlerException;
+import edu.kit.iti.formal.psdbg.interpreter.funchdl.*;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
+import lombok.AllArgsConstructor;
+import lombok.Getter;
+import lombok.NoArgsConstructor;
+
 import java.util.stream.Stream;
 
 /**
  * @author Alexander Weigl
  * @version 1 (13.03.18)
  */
+@AllArgsConstructor
+
 public class ArgumentCompleter implements AutoCompleter {
+    @Getter
+    private final ProofScriptHandler psh = new ProofScriptHandler();
+    @Getter
+    private final MacroCommandHandler pmh = new MacroCommandHandler();
+    @Getter
+    private final RuleCommandHandler pmr = new RuleCommandHandler();
+    @Getter
+    private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder();
+    @Getter
+    private DefaultLookup<KeyData> lookup = new DefaultLookup(psh, pmh, pmr, pmc);
+    private KeyData keyData;
+
+    public ArgumentCompleter() {
+        KeYApi.getMacroApi().getMacros().forEach(m ->
+                pmh.getMacros().put(m.getScriptCommandName(), m));
+        KeYApi.getScriptCommandApi().getScriptCommands().forEach(m ->
+                pmc.getCommands().put(m.getName(), m));
+    }
+
+    public void setDefaultKeyData(KeyData data) {
+        this.keyData = data;
+    }
+
     @Override
     public Stream<Suggestion> get(CompletionPosition cp) {
-        return Stream.of(Suggestion.command("argument completer not implemented"));
+        String cmd = cp.getCommand();
+        if (!cmd.isEmpty()) {
+            CallStatement call = new CallStatement(cmd, new Parameters());
+            try {
+                return lookup.getBuilder(call, keyData).getArguments(cmd)
+                        .filter(s -> s.startsWith(cp.getPrefix()))
+                        .map(Suggestion::argument);
+            } catch (NoCallHandlerException e) {
+            }
+        }
+        return Stream.of();
     }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/CommandCompleter.java

@@ -14,7 +14,7 @@ public class CommandCompleter implements AutoCompleter {
     private static Collection<Suggestion> suggestions = new ArrayList<>();
     static {
         KeYApi.getScriptCommandApi().getScriptCommands().forEach(proofMacro -> {
-            suggestions.add(Suggestion.macro(proofMacro.getName()));
+            suggestions.add(Suggestion.command(proofMacro.getName()));
         });
     }
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/CompletionPosition.java

@@ -3,6 +3,8 @@ package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
 import lombok.Value;
 
 import java.util.Collection;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 import java.util.stream.Stream;
 
 /**
@@ -14,14 +16,45 @@ public class CompletionPosition {
     String text;
     int pos;
 
-    public String getPrefix() {
-        if (text.isEmpty()) return "";
-        int start = Math.min(text.length() - 1, pos - 1);
+    public static int indexOf(String subject, String stopChars, int pos) {
+        int start = Math.min(subject.length() - 1, pos);
+        char[] chars = subject.toCharArray();
+        for (; start < chars.length; start++) {
+            if (stopChars.indexOf(chars[start]) >= 0) {
+                return start;
+            }
+        }
+        return -1;
+    }
+
+    public static int lastIndexOf(String subject, String stopChars, int pos) {
+        int start = Math.min(subject.length() - 1, pos);
+        char[] chars = subject.toCharArray();
         for (; start >= 0; start--) {
-            if (Character.isWhitespace(text.charAt(start)))
-                break;
+            if (stopChars.indexOf(chars[start]) >= 0) {
+                return start + 1;
+            }
         }
-        return text.substring(Math.max(0, start), pos).trim();
+        if (start == -1 && stopChars.contains("^"))
+            return 0;
+
+        return -1;
+    }
+
+    public static String find(String subject, String regex, int start) {
+        Pattern p = Pattern.compile(regex + ".*", Pattern.MULTILINE | Pattern.DOTALL);
+        Matcher m = p.matcher(subject.substring(start));
+        if (m.matches())
+            return m.group(1);
+        return "";
+    }
+
+    public String getPrefix() {
+        if (text.isEmpty()) return "";
+        int start = lastIndexOf(text, "^\n \t\f", pos);
+        if (start == -1)
+            return "";
+        return text.substring(start, pos + 1).trim();
     }
 
     public boolean onLineBegin() {
@@ -37,4 +70,12 @@ public class CompletionPosition {
         String prefix = getPrefix();
         return list.stream().filter(s -> s.getText().startsWith(prefix));
     }
+
+    public String getCommand() {
+        int posNewline = lastIndexOf(text, "^{;", pos);
+        if (posNewline >= 0) {
+            return find(text, "\\s*(\\w+)\\s", posNewline);
+        }
+        return "";
+    }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/Suggestion.java

@@ -31,17 +31,22 @@ public class Suggestion implements Comparable<Suggestion> {
         return new Suggestion(name, Category.RULE, 5);
     }
 
+    public static Suggestion argument(String s) {
+        return new Suggestion(s, Category.ATTRIBUTE, 1);
+    }
+
     @Override
     public int compareTo(Suggestion o) {
         return Integer.compare(priority, o.priority);
     }
 
+
     @RequiredArgsConstructor
     public static enum Category {
         COMMAND((MaterialDesignIcon.APPLE_KEYBOARD_COMMAND)),
         RULE((MaterialDesignIcon.RULER)),
-        MACRO((MaterialDesignIcon.RULER)),
-        ATTRIBUTE((MaterialDesignIcon.RULER)),
+        MACRO((MaterialDesignIcon.PHARMACY)),
+        ATTRIBUTE((MaterialDesignIcon.ATTACHMENT)),
         KEYWORD((MaterialDesignIcon.KEY_VARIANT));
 
         @Getter

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -6,6 +6,7 @@ import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.api.ProofApi;
+import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
@@ -33,6 +34,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import javafx.application.Platform;
+import javafx.beans.InvalidationListener;
 import javafx.beans.binding.BooleanBinding;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableList;
@@ -58,6 +60,7 @@ import org.apache.logging.log4j.Logger;
 import org.dockfx.DockNode;
 import org.dockfx.DockPane;
 import org.dockfx.DockPos;
+import org.key_project.util.collection.ImmutableList;
 import org.reactfx.util.FxTimer;
 import org.reactfx.util.Timer;
 
@@ -204,6 +207,18 @@ public class DebuggerMain implements Initializable {
                     scriptController.getAutoCompleter().getRuleCompleter().setEnvironment(n);
                 });
 
+        InvalidationListener invalidationListener = observable -> {
+            Proof p = getFacade().getProof();
+            KeYEnvironment env = getFacade().getEnvironment();
+            if (p == null || env == null) return;
+            ImmutableList<Goal> openGoals = p.getSubtreeGoals(p.root());
+            KeyData kd = new KeyData(openGoals.get(0), env, p);
+            scriptController.getAutoCompleter().getArgumentCompleter().setDefaultKeyData(kd);
+        };
+        getFacade().environmentProperty().addListener(invalidationListener);
+        getFacade().proofProperty().addListener(invalidationListener);
+
+
         //marriage key proof facade to proof tree
         getFacade().proofProperty().addListener(
                 (prop, o, n) -> {

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

@@ -1865,7 +1865,7 @@ public class ScriptArea extends BorderPane {
 
         public void update() {
             popup = getPopup();
-            int end = codeArea.getCaretPosition();
+            int end = codeArea.getCaretPosition()-1;
             //int start = text.lastIndexOf(' ');
             //final String searchPrefix = text.substring(start).trim();
             //System.out.println("searchPrefix = " + searchPrefix);

ui/src/test/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/CompletionPositionTest.java

@@ -10,7 +10,33 @@ import static org.junit.Assert.*;
  * @version 1 (14.03.18)
  */
 public class CompletionPositionTest {
-    private CompletionPosition a, b, c, d, e;
+    private CompletionPosition a, b, c, d, e, f, g, h;
+
+    private static CompletionPosition create(String s) {
+        return new CompletionPosition(s.replace("|", ""), s.indexOf('|'));
+    }
+
+    @Test
+    public void find() throws Exception {
+        assertEquals("abc",
+                CompletionPosition.find("abc\na", "\\s*(\\w+)\\s", 0));
+        assertEquals("abc",
+                CompletionPosition.find("abc\ndef\n", "\\s*(\\w+)\\s", 0));
+        assertEquals("abc",
+                CompletionPosition.find("abc\ndef\n|\nghi\n", "\\s*(\\w+)\\s", 0));
+    }
+
+    @Test
+    public void getCommand() {
+        assertEquals("abc", a.getCommand());
+        assertEquals("abc", b.getCommand());
+        assertEquals("abc", c.getCommand());
+        assertEquals("", d.getCommand());
+        assertEquals("abc", e.getCommand());
+        assertEquals("multiLineRule", f.getCommand());
+        assertEquals("multiLineRule", g.getCommand());
+        assertEquals("multiLineRule", h.getCommand());
+    }
 
     @Before
     public void setup() {
@@ -19,10 +45,9 @@ public class CompletionPositionTest {
         c = create("abc\ndef\nghi\n|");
         d = new CompletionPosition("", 3);
         e = create("abc\ndef\n|\nghi\n");
-    }
-
-    private static CompletionPosition create(String s) {
-        return new CompletionPosition(s.replace("|", ""), s.indexOf('|'));
+        f = create("multiLineRule\nabc=1\ndef=2\n |;");
+        g = create("abc;\n\nmultiLineRule   a=\n2 abc  =  1|        \ndef=2\n;");
+        h = create("foreach{\n\nmultiLineRule   a=\n2 abc  =  1|       \ndef=2\n; }");
     }
 
     @Test
@@ -32,6 +57,9 @@ public class CompletionPositionTest {
         assertEquals("", c.getPrefix());
         assertEquals("", d.getPrefix());
         assertEquals("", e.getPrefix());
+        assertEquals("", f.getPrefix());
+        assertEquals("", g.getPrefix());
+        assertEquals("", h.getPrefix());
     }
 
     @Test
@@ -41,6 +69,9 @@ public class CompletionPositionTest {
         assertTrue(c.onLineBegin());
         assertTrue(d.onLineBegin());
         assertTrue(e.onLineBegin());
+        assertFalse(f.onLineBegin());//TODO off-by-one
+        assertFalse(g.onLineBegin());
+        assertFalse(h.onLineBegin());
     }
 
     @Test