auto completion and inline action bar

.gitignore

@@ -2,3 +2,6 @@ target/
 *.iml
 .idea
 website/site/
+*/build/
+*/out/
+.gradle

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java

@@ -26,7 +26,9 @@ package edu.kit.iti.formal.psdbg.parser;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import edu.kit.iti.formal.psdbg.parser.types.Type;
 
-import java.util.Map;
+import java.util.*;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 /**
  * {@link ASTTraversal} provides a visitor with a a default traversal of the given AST.
@@ -35,6 +37,41 @@ import java.util.Map;
  * @version 1 (29.04.17)
  */
 public interface ASTTraversal<T> extends Visitor<T> {
+
+    default Stream<T> allOf(Stream<ASTNode> nodes) {
+        return nodes.map(n -> (T) n.accept(this));
+    }
+
+    default List<T> allOf(Collection<ASTNode> nodes) {
+        if (nodes.size() == 0) return Collections.emptyList();
+        return allOf(nodes.stream()).collect(Collectors.toList());
+    }
+
+    default Stream<T> allOf(ASTNode... nodes) {
+        if (nodes.length == 0) return (Stream<T>) Collections.emptyList().stream();
+        return allOf(Arrays.stream(nodes));
+    }
+
+    default T oneOf(Stream<? extends ASTNode> nodes) {
+        return (T) nodes
+                .filter(Objects::nonNull)
+                .map(n -> (T) n.accept(this))
+                .filter(Objects::nonNull)
+                .findFirst()
+                .orElse((T) null);
+    }
+
+    default T oneOf(ASTNode... nodes) {
+        if (nodes.length == 0) return null;
+        return oneOf(Arrays.stream(nodes));
+    }
+
+    default T oneOf(Collection<ASTNode> nodes) {
+        if (nodes.size() == 0) return null;
+        return oneOf(nodes.stream());
+    }
+
+
     @Override
     default T visit(ProofScript proofScript) {
         proofScript.getSignature().accept(this);

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java

@@ -197,7 +197,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
     @Override
     public Void visit(TermLiteral termLiteral) {
-        String termLit = termLiteral.getText();
+        String termLit = termLiteral.getContent();
         if (termLit.contains("\n")) {
             termLit = termLit.trim();
         }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java

@@ -121,12 +121,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     @Override
     public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) {
         Signature signature = new Signature();
+        signature.setRuleContext(ctx);
         for (ScriptLanguageParser.VarDeclContext decl : ctx.varDecl()) {
             Variable key = new Variable(decl.name);
             key.setParent(signature);
             signature.put(key, TypeFacade.findType(decl.type.getText()));
         }
-        signature.setRuleContext(ctx);
         return signature;
     }
 
@@ -148,6 +148,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     @Override
     public Statements visitStmtList(ScriptLanguageParser.StmtListContext ctx) {
         Statements statements = new Statements();
+        statements.setRuleContext(ctx);
         for (ScriptLanguageParser.StatementContext stmt : ctx.statement()) {
             Statement<ParserRuleContext> statement = (Statement<ParserRuleContext>) stmt.accept(this);
             statement.setParent(statements);
@@ -333,7 +334,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
     @Override
     public Object visitLiteralTerm(ScriptLanguageParser.LiteralTermContext ctx) {
-        return new TermLiteral(ctx.getText());
+        return new TermLiteral(ctx.TERM_LITERAL().getSymbol());
     }
 
     @Override

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java

@@ -81,8 +81,8 @@ public abstract class ASTNode<T extends ParserRuleContext>
     }
 
     public void setRuleContext(T c) {
-        startPosition = Position.from(c.getStart());
-        endPosition = Position.from(c.getStop());
+        startPosition = Position.start(c);
+        endPosition = Position.end(c);
         ruleContext = c;
     }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/BooleanLiteral.java

@@ -51,7 +51,7 @@ public class BooleanLiteral extends Literal {
 
     public BooleanLiteral(boolean value, Token token) {
         this.value = value;
-        this.token = token;
+        setToken(token);
     }
 
     BooleanLiteral(boolean b) {
@@ -76,7 +76,7 @@ public class BooleanLiteral extends Literal {
      */
     @Override
     public BooleanLiteral copy() {
-        return new BooleanLiteral(value, token);
+        return new BooleanLiteral(value, getToken());
     }
 
     /**

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/IntegerLiteral.java

@@ -71,7 +71,7 @@ public class IntegerLiteral extends Literal {
      */
     @Override public IntegerLiteral copy() {
         IntegerLiteral il = new IntegerLiteral(value);
-        il.token = token;
+        il.setToken(getToken());
         return il;
     }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Literal.java

@@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  */
 
 
-
 import lombok.Getter;
 import lombok.Setter;
 import org.antlr.v4.runtime.ParserRuleContext;
@@ -38,7 +37,15 @@ import java.util.Optional;
 public abstract class Literal extends Expression<ParserRuleContext> {
     @Getter
     @Setter
-    protected Token token;
+    private Token token;
+
+    public void setToken(Token token) {
+        this.token = token;
+        if (token != null) {
+            startPosition = Position.start(token);
+            endPosition = Position.end(token);
+        }
+    }
 
     /**
      * {@inheritDoc}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Position.java

@@ -23,26 +23,51 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  */
 
 
-
-import lombok.*;
+import lombok.Data;
+import lombok.RequiredArgsConstructor;
+import lombok.Value;
+import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.Token;
 
 /**
  * @author Alexander Weigl
  */
-@Data @Value @RequiredArgsConstructor public class Position implements Copyable<Position> {
+@Data
+@Value
+@RequiredArgsConstructor
+public class Position implements Copyable<Position> {
+    private final int offset;
     private final int lineNumber;
     private final int charInLine;
 
     public Position() {
-        this(-1, -1);
+        this(-1, -1, -1);
+    }
+
+    public static Position start(Token token) {
+        return new Position(
+                token.getStartIndex(),
+                token.getLine(),
+                token.getCharPositionInLine());
+    }
+
+    public static Position end(Token token) {
+        return new Position(
+                token.getStopIndex(),
+                token.getLine(),
+                token.getCharPositionInLine());
+    }
+
+    public static Position start(ParserRuleContext token) {
+        return start(token.start);
     }
 
-    @Override public Position copy() {
-        return new Position(lineNumber, charInLine);
+    public static Position end(ParserRuleContext token) {
+        return end(token.stop);
     }
 
-    public static Position from(Token token) {
-        return new Position(token.getLine(), token.getCharPositionInLine());
+    @Override
+    public Position copy() {
+        return new Position(offset, lineNumber, charInLine);
     }
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TermLiteral.java

@@ -23,12 +23,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  */
 
 
-
 import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
 import edu.kit.iti.formal.psdbg.parser.Visitor;
 import edu.kit.iti.formal.psdbg.parser.types.Type;
 import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
 import lombok.Data;
+import org.antlr.v4.runtime.Token;
 
 /**
  * @author Alexander Weigl
@@ -36,16 +36,27 @@ import lombok.Data;
  */
 @Data
 public class TermLiteral extends Literal {
-    private final String text;
+    private final String content;
 
-    public TermLiteral(String text) {
+    public TermLiteral(Token token) {
+        setToken(token);
+        String text = token.getText();
         if (text.charAt(0) == '`')
             text = text.substring(1);
         if (text.charAt(text.length() - 1) == '`') //remove last backtick
             text = text.substring(0, text.length() - 1);
         if (text.charAt(0) == '`')
             text = text.substring(0, text.length() - 2);
-        this.text = text;
+        content = text;
+    }
+
+    private TermLiteral(String sfTerm) {
+        content = sfTerm;
+    }
+
+    public static TermLiteral from(String sfTerm) {
+        TermLiteral tl = new TermLiteral(sfTerm);
+        return tl;
     }
 
     /**
@@ -67,7 +78,7 @@ public class TermLiteral extends Literal {
 
     @Override
     public TermLiteral copy() {
-        return new TermLiteral(text);
+        return new TermLiteral(getToken());
     }
 
     /**
@@ -77,5 +88,4 @@ public class TermLiteral extends Literal {
     public Type getType(Signature signature) throws NotWelldefinedException {
         return TypeFacade.ANY_TERM;
     }
-
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Variable.java

@@ -61,7 +61,7 @@ public class Variable extends Literal implements Comparable<Variable> {
     @Override
     public Variable copy() {
         Variable v = new Variable(identifier);
-        v.token = token;
+        v.setToken(getToken());
         return v;
     }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/data/Value.java

@@ -57,7 +57,7 @@ public class Value<T> {
     }
 
     public static Value<String> from(TermLiteral term) {
-        return new Value<>(TypeFacade.ANY_TERM, term.getText());
+        return new Value<>(TypeFacade.ANY_TERM, term.getContent());
     }
 
     @Override

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

@@ -17,7 +17,6 @@ import jdk.nashorn.internal.objects.annotations.Getter;
 import jdk.nashorn.internal.objects.annotations.Setter;
 import lombok.RequiredArgsConstructor;
 import lombok.Value;
-import sun.security.jca.GetInstance;
 
 import java.io.StringReader;
 import java.lang.annotation.Retention;

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

@@ -142,7 +142,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
         eval.setTermValueFactory(new Function<TermLiteral, Value>() {
             @Override
             public Value apply(TermLiteral termLiteral) {
-                return  new Value(TypeFacade.ANY_TERM, new TermValue(termLiteral.getText()));
+                return  new Value(TypeFacade.ANY_TERM, new TermValue(termLiteral.getContent()));
             }
         });
         return eval;

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindLabelInGoalList.java

+package edu.kit.iti.formal.psdbg.gui.actions.inline;
+
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
+import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral;
+import javafx.event.ActionEvent;
+
+import java.util.Collection;
+import java.util.Collections;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (12.03.18)
+ */
+public class FindLabelInGoalList implements InlineActionSupplier {
+    @Override
+    public Collection<InlineAction> get(ASTNode node) {
+        if (node instanceof StringLiteral) {
+            return Collections.singletonList(new FindLabelInGoalListAction());
+        }
+        return Collections.emptyList();
+    }
+
+    public static class FindLabelInGoalListAction extends InlineAction {
+        public FindLabelInGoalListAction() {
+            setName(getClass().getSimpleName());
+            setGraphics(new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
+            setPriority(2);
+            setEventHandler(this::handle);
+        }
+
+        private void handle(ActionEvent event) {
+            System.out.println("FindLabelInGoalListAction.handle");
+        }
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindTermLiteralInSequence.java

+package edu.kit.iti.formal.psdbg.gui.actions.inline;
+
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
+import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
+import javafx.event.ActionEvent;
+
+import java.util.Collection;
+import java.util.Collections;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (12.03.18)
+ */
+public class FindTermLiteralInSequence implements InlineActionSupplier {
+    @Override
+    public Collection<InlineAction> get(ASTNode node) {
+        if (node instanceof TermLiteral) {
+            return Collections.singletonList(
+                    new FindTermLiteralInSequenceAction()
+            );
+        }
+        return Collections.emptyList();
+    }
+
+    public static class FindTermLiteralInSequenceAction extends InlineAction {
+        public FindTermLiteralInSequenceAction() {
+            setName(getClass().getSimpleName());
+            setGraphics(new MaterialDesignIconView(MaterialDesignIcon.MAGNIFY_PLUS));
+            setEventHandler(this::handle);
+        }
+
+        private void handle(ActionEvent event) {
+            System.out.println("FindTermLiteralInSequenceAction.handle");
+        }
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineAction.java

+package edu.kit.iti.formal.psdbg.gui.actions.inline;
+
+import javafx.beans.DefaultProperty;
+import javafx.event.ActionEvent;
+import javafx.event.EventHandler;
+import javafx.scene.Node;
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+
+@Data
+@AllArgsConstructor
+@NoArgsConstructor
+public class InlineAction implements Comparable<InlineAction> {
+    private String name;
+    private int priority;
+    private Node graphics;
+    private EventHandler<ActionEvent> eventHandler;
+
+    @Override
+    public int compareTo(InlineAction o) {
+        return priority - o.priority;
+    }
+}
\ No newline at end of file

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineActionSupplier.java

+package edu.kit.iti.formal.psdbg.gui.actions.inline;
+
+import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
+
+import java.util.Collection;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (12.03.18)
+ */
+public interface InlineActionSupplier {
+    Collection<InlineAction> get(ASTNode node);
+}

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

@@ -175,9 +175,9 @@ public class InteractiveModeController {
         int occ = rch.getOccurence(tap.getApp());
 
         Parameters callp = new Parameters();
-        callp.put(new Variable("formula"), new TermLiteral(sfTerm));
+        callp.put(new Variable("formula"), TermLiteral.from(sfTerm));
         callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ)));
-        callp.put(new Variable("on"), new TermLiteral(onTerm));
+        callp.put(new Variable("on"), TermLiteral.from(onTerm));
 
         VariableAssignment va = new VariableAssignment(null);
         CallStatement call = new CallStatement(tapName, callp);

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

+package edu.kit.iti.formal.psdbg.gui.controls;
+
+import com.google.common.collect.Streams;
+import edu.kit.iti.formal.psdbg.parser.ASTTraversal;
+import edu.kit.iti.formal.psdbg.parser.ast.*;
+import lombok.RequiredArgsConstructor;
+
+import java.util.*;
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (12.03.18)
+ */
+@RequiredArgsConstructor
+public class FindNearestASTNode implements ASTTraversal<ASTNode> {
+    private final int pos;
+
+    @Override
+    public ASTNode visit(ProofScript proofScript) {
+        return childOrMe(proofScript, proofScript.getSignature(), proofScript.getBody());
+    }
+
+    private ASTNode childOrMe(ASTNode me, Stream<? extends ASTNode> nodes) {
+        // range check
+        if (me == null) {
+            return null;
+        }
+
+        try {
+            int start = me.getStartPosition().getOffset();
+            int stop = me.getEndPosition().getOffset();
+            if (start <= pos && pos <= stop) {
+                ASTNode a = null;
+                try {
+                    a = oneOf(nodes);
+                } catch (NullPointerException e1) {
+                    e1.printStackTrace();
+                }
+                return a != null ? a : me;
+            }
+        } catch (NullPointerException e) {
+            System.err.println("No rule context set for instance " + me);
+            e.printStackTrace();
+        }
+        return null;
+    }
+
+    private ASTNode childOrMe(ASTNode me, Collection<? extends ASTNode> children) {
+        return childOrMe(me, children.stream());
+    }
+
+    private ASTNode childOrMe(ASTNode me, ASTNode... nodes) {
+        return childOrMe(me, Arrays.stream(nodes));
+    }
+
+    @Override
+    public ASTNode visit(AssignmentStatement assign) {
+        return childOrMe(assign, assign.getLhs(), assign.getRhs());
+    }
+
+    @Override
+    public ASTNode visit(BinaryExpression e) {
+        return childOrMe(e, e.getLeft(), e.getRight());
+    }
+
+    @Override
+    public ASTNode visit(MatchExpression match) {
+        return childOrMe(match, match.getSignature(), match.getDerivableTerm(), match.getPattern());
+    }
+
+    @Override
+    public ASTNode visit(TermLiteral term) {
+        return childOrMe(term);
+    }
+
+    @Override
+    public ASTNode visit(StringLiteral string) {
+        return childOrMe(string);
+    }
+
+    @Override
+    public ASTNode visit(Variable variable) {
+        return childOrMe(variable);
+    }
+
+    @Override
+    public ASTNode visit(BooleanLiteral bool) {
+        return childOrMe(bool);
+    }
+
+    @Override
+    public ASTNode visit(Statements statements) {
+        return childOrMe(statements, statements.stream());
+    }
+
+    @Override
+    public ASTNode visit(IntegerLiteral integer) {
+        return childOrMe(integer);
+    }
+
+    @Override
+    public ASTNode visit(CasesStatement casesStatement) {
+        return childOrMe(casesStatement,
+                Streams.concat(casesStatement.getCases().stream(),
+                        Stream.of(casesStatement.getDefCaseStmt())
+                ));
+    }
+
+    @Override
+    public ASTNode visit(CaseStatement caseStatement) {
+        return childOrMe(caseStatement, caseStatement.getBody());
+    }
+
+    @Override
+    public ASTNode visit(CallStatement call) {
+        return childOrMe(call, call.getParameters());
+    }
+
+    @Override
+    public ASTNode visit(TheOnlyStatement theOnly) {
+        return childOrMe(theOnly, theOnly.getBody());
+    }
+
+    @Override
+    public ASTNode visit(ForeachStatement foreach) {
+        return childOrMe(foreach, foreach.getBody());
+    }
+
+    @Override
+    public ASTNode visit(RepeatStatement repeatStatement) {
+        return childOrMe(repeatStatement, repeatStatement.getBody());
+    }
+
+    @Override
+    public ASTNode visit(Signature signature) {
+        return childOrMe(signature);
+    }
+
+    @Override
+    public ASTNode visit(Parameters parameters) {
+        return childOrMe(parameters, parameters.values());
+    }
+
+    @Override
+    public ASTNode visit(UnaryExpression e) {
+        return childOrMe(e, e.getExpression());
+    }
+
+    @Override
+    public ASTNode visit(TryCase tryCase) {
+        return childOrMe(tryCase, tryCase.getBody());
+    }
+
+    @Override
+    public ASTNode visit(GuardedCaseStatement guardedCaseStatement) {
+        return childOrMe(guardedCaseStatement,
+                guardedCaseStatement.getGuard(),
+                guardedCaseStatement.getBody());
+    }
+
+    @Override
+    public ASTNode visit(SubstituteExpression subst) {
+        return childOrMe(subst);
+    }
+
+    @Override
+    public ASTNode visit(ClosesCase closesCase) {
+        return null;
+    }
+
+    @Override
+    public ASTNode visit(DefaultCaseStatement defCase) {
+        return null;
+    }
+
+    @Override
+    public ASTNode visit(FunctionCall func) {
+        return null;
+    }
+
+    @Override
+    public ASTNode visit(WhileStatement ws) {
+        return null;
+    }
+
+    @Override
+    public ASTNode visit(IfStatement is) {
+        return null;
+    }
+
+    @Override
+    public ASTNode visit(StrictBlock strictBlock) {
+        return null;
+    }
+
+    @Override
+    public ASTNode visit(RelaxBlock relaxBlock) {
+        return null;
+    }
+
+    @Override
+    public ASTNode visit(NamespaceSetExpression nss) {
+        return null;
+    }
+
+    public Optional<ASTNode> find(List<ProofScript> ast) {
+        return ast.stream().map(a -> a.accept(this))
+                .filter(Objects::nonNull)
+                .findFirst();
+    }
+}

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

@@ -3,8 +3,13 @@ package edu.kit.iti.formal.psdbg.gui.controls;
 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.KeYApi;
+import edu.kit.iti.formal.psdbg.gui.actions.inline.FindLabelInGoalList;