Context Menu for ProofTree, Formatting,

* Menu entries for debugging

.gitlab-ci.yml

@@ -45,6 +45,12 @@ deploy:
       - "*/target/*.jar"
   allow_failure: true
 
+sonar:
+  stage: deploy
+  script:
+    - ""
+  allow_failure: true
+
 site:
   stage: deploy
   script:

lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4

@@ -9,16 +9,16 @@ start
     ;
 
 script
-    : SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT
+    : SCRIPT name=ID LPAREN signature=argList? RPAREN INDENT body=stmtList DEDENT
     ;
 
 
 argList
-    :   varDecl (',' varDecl)*
+    :   varDecl (COMMA varDecl)*
     ;
 
 varDecl
-    :   name=ID ':' type=ID
+    :   name=ID COLON type=ID
     ;
 
 stmtList
@@ -59,18 +59,18 @@ expression
     | expression IMP expression   #exprIMP
     //|   expression EQUIV expression already covered by EQ/NEQ
     | expression LBRACKET substExpressionList RBRACKET #exprSubst
-    | MINUS expression   #exprNegate
-    | NOT expression  #exprNot
-    | '(' expression ')' #exprParen
-    | literals             #exprLiterals
-    | matchPattern         #exprMatch
+    | MINUS expression         #exprNegate
+    | NOT expression           #exprNot
+    | LPAREN expression RPAREN #exprParen
+    | literals                 #exprLiterals
+    | matchPattern             #exprMatch
 ;
 
 
 substExpressionList
     :
-    (scriptVar '\\' expression
-        (',' scriptVar '\\' expression)*
+    (scriptVar SUBST_TO expression
+        (COMMA scriptVar SUBST_TO expression)*
     )?
     ;
 
@@ -97,9 +97,10 @@ matchPattern
     ;
 
 scriptVar
-    :   '?' ID
+    :   QUESTION_MARK ID
     ;
 
+
 repeatStmt
     :   REPEAT INDENT stmtList DEDENT
     ;
@@ -138,7 +139,7 @@ scriptCommand
     ;
 
 parameters: parameter+;
-parameter :  ((pname=ID '=')? expr=expression);
+parameter :  ((pname=ID EQ)? expr=expression);
 
 /*
 callStmt
@@ -179,6 +180,7 @@ DEDENT : '}' ;
 SEMICOLON : ';' ;
 COLON : ':' ;
 HEAPSIMP:'heap-simp';
+SUBST_TO: '\\';
 
 
 STRING_LITERAL
@@ -204,8 +206,11 @@ OR: '|' ;
 IMP : '==>' ;
 EQUIV : '<=>' ;
 NOT: 'not';
-
+COMMA: ',';
+LPAREN: '(';
+RPAREN: ')';
 EXE_MARKER: '\u2316' -> channel(HIDDEN);
+QUESTION_MARK: '?';
 
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;

lint/pom.xml

@@ -44,6 +44,19 @@
             <version>0.9.5</version>
         </dependency>
 
+        <dependency>
+            <groupId>it.unibo.alice.tuprolog</groupId>
+            <artifactId>tuprolog</artifactId>
+            <version>3.2.1</version>
+        </dependency>
+
+        <!--
+        <dependency>
+            <groupId>com.thesett</groupId>
+            <artifactId>prolog</artifactId>
+            <version>0.9.117</version>
+        </dependency>-->
+
         <dependency>
             <groupId>edu.kit.iti.formal.psdbg</groupId>
             <artifactId>lang</artifactId>
@@ -52,7 +65,7 @@
 
         <dependency>
             <groupId>edu.kit.iti.formal.psdbg</groupId>
-            <artifactId>runtime</artifactId>
+            <artifactId>rt</artifactId>
             <version>0.1-SNAPSHOT</version>
         </dependency>
 

lint/src/main/java/edu/kit/iti/formal/psdbg/fmt/DefaultFormatter.java

+package edu.kit.iti.formal.psdbg.fmt;
+
+
+import alice.tuprolog.*;
+import com.google.common.base.Strings;
+import edu.kit.iti.formal.psdbg.parser.ScriptLanguageLexer;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.Lexer;
+import org.antlr.v4.runtime.Token;
+
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.util.Arrays;
+import java.util.List;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public class DefaultFormatter implements Formatter {
+    private final Prolog prolog;
+
+    private final Theory formattingTheory;
+
+    private boolean inExpression = false;
+
+    private List<? extends Token> tokens;
+
+    private int nested;
+
+    private int pos;
+
+    private List<String> types;
+
+    public DefaultFormatter() throws InvalidLibraryException, IOException, InvalidTheoryException {
+        this.prolog = new Prolog();
+        //formattingTheory = new Theory(getClass().getResourceAsStream("fmt.pl"));
+        formattingTheory = new Theory(new FileInputStream("C:/Users/weigl/IdeaProjects/ProofScriptParser/lint/src/main/resources/fmt.pl"));
+        prolog.addTheory(formattingTheory);
+        //prolog.loadLibrary();
+        //new String[]{"lint/src/main/resources/fmt.pl"}
+
+    }
+
+    @Override
+    public String format(String code) {
+        ScriptLanguageLexer lexer = new ScriptLanguageLexer(CharStreams.fromString(code));
+        StringBuilder sb = new StringBuilder();
+
+        tokens = lexer.getAllTokens().stream()
+                .filter(t -> t.getChannel() != Lexer.HIDDEN)
+                .collect(Collectors.toList());
+
+        types = tokens.stream()
+                .map(Token::getType)
+                .map(lexer.getVocabulary()::getSymbolicName)
+                //.map(String::toLowerCase)
+                .map(s -> String.valueOf(s).toLowerCase())
+                .collect(Collectors.toList());
+
+
+        //System.out.println(types);
+        for (pos = 0; pos < tokens.size() - 1; pos++) {
+            Token token = tokens.get(pos);
+
+            nested += askForNumber("level", 2);
+
+            int nlCount = 0;
+            if ((nlCount = clearLinesBefore()) > 0)
+                clearLine(sb, nlCount);
+            else {
+                int numSpace = 0;
+                if ((numSpace = spaceBefore()) > 0)
+                    whitespaces(sb, numSpace);
+            }
+            sb.append(token.getText());
+
+            int numSpace = 0;
+            if ((numSpace = spaceAfter()) > 0)
+                whitespaces(sb, numSpace);
+            else {
+                int nlAfter = 0;
+                if ((nlAfter = newlineAfter()) > 0) {
+                    sb.append(Strings.repeat("\n", nlAfter))
+                            .append(Strings.repeat(" ", nested * 4));
+                }
+            }
+
+
+        }
+        sb.append(tokens.get(pos).getText());
+        sb.append("\n");
+        return sb.toString();
+    }
+
+    private void whitespaces(StringBuilder sb, int numSpace) {
+        int i = 0;
+        for (i = 0; i < sb.length(); i++) {
+            if (sb.charAt(sb.length() - 1 - i) != ' ') {
+                break;
+            }
+        }
+        if (i < numSpace)
+            sb.append(Strings.repeat(" ", numSpace - i));
+    }
+
+    private void clearLine(StringBuilder sb, int nlCount) {
+        int i = 0;
+        for (i = sb.length() - 1; i >= 0; i--) {
+            if (!Character.isWhitespace(sb.charAt(i))) {
+                break;
+            }
+        }
+        sb.setLength(i + 1);
+        sb.append(Strings.repeat("\n", nlCount))
+                .append(Strings.repeat(" ", 4 * nested));
+    }
+
+    private int newlineAfter() {
+        return askForNumber("nlafter", 2);
+    }
+
+    private int spaceBefore() {
+        return askForNumber("wsbefore", 2);
+    }
+
+    private int spaceAfter() {
+        return askForNumber("wsafter", 2);
+    }
+
+    private int askForNumber(String name, int numContext) {
+        try {
+            SolveInfo si = callProlog(name, numContext, 1);
+            Term x = si.getVarValue("X");
+            if (x instanceof Int)
+                return ((Int) x).intValue();
+            else
+                return 0;
+        } catch (MalformedGoalException | NoSolutionException e) {
+            // e.printStackTrace();
+            return 0;
+        }
+    }
+
+    private int clearLinesBefore() {
+        return askForNumber("onclearline", 5);
+    }
+
+    private SolveInfo callProlog(String name, int numContext, int retArgs) throws MalformedGoalException {
+        String pctx = getContext(numContext, i -> pos - i - 1);
+        String nctx = getContext(numContext, i -> pos + i + 1);
+
+        String query = String.format(
+                "%s( [%s], %s, [%s] ,X ).", name, pctx, this.types.get(pos), nctx);
+        System.err.format("q: %s%n", query);
+        SolveInfo si = prolog.solve(query);
+        System.err.format("got %s%n", si);
+
+        return si;
+    }
+
+    private String getContext(int numContext, Function<Integer, Integer> access) {
+        String[] next = new String[numContext];
+        Arrays.fill(next, "empty");
+        for (int i = 0; i < numContext; i++) {
+            int val = access.apply(i);
+            if (0 <= val && val < types.size())
+                next[i] = this.types.get(val);
+            else break;
+        }
+        return Arrays.stream(next).reduce((a, b) -> a + ',' + b).orElse("");
+    }
+}

lint/src/main/java/edu/kit/iti/formal/psdbg/fmt/Formatter.java

+package edu.kit.iti.formal.psdbg.fmt;
+
+public interface Formatter {
+    public String format(String code);
+}

lint/src/main/java/edu/kit/iti/formal/psdbg/fmt/FormatterMain.java

+package edu.kit.iti.formal.psdbg.fmt;
+
+import alice.tuprolog.InvalidLibraryException;
+import alice.tuprolog.InvalidTheoryException;
+import org.apache.commons.io.FileUtils;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.charset.Charset;
+
+public class FormatterMain {
+    public static final void main(String[] args) throws InvalidLibraryException, IOException, InvalidTheoryException {
+        DefaultFormatter df = new DefaultFormatter();
+        String code = FileUtils.readFileToString(new File(args[0]), Charset.defaultCharset());
+        String newCode = df.format(code);
+        System.out.flush();
+        System.err.flush();
+        System.out.println(newCode);
+    }
+}

lint/src/main/resources/fmt.pl

+level(dedent,-1).
+level(indent,1).
+level(X,0).
+level(Prev, colon, [indent,T],0).
+level(colon,1).
+level(Prev, Cur, Next, X) :- level(Cur,X).
+
+onclearline(dedent,1).
+onclearline(script, 2).
+onclearline(cases, 1).
+onclearline(foreach, 1).
+onclearline(repeat, 2).
+onclearline(comment, 1).
+onclearline(Prev, Cur, Next, X) :- onclearline(Cur,X).
+
+nlafter(Prev, colon, [H | T], 1) :- H \= indent .
+nlafter(indent,1).
+nlafter(dedent,1).
+nlafter(semicolon,1).
+nlafter(Prev, Cur, Next, X) :- nlafter(Cur,X).
+
+wsbefore(Prev, Cur, Next, X) :- wsafter(Cur,X).
+wsbefore(id,1).
+
+
+wsafter(Prev, id, [semicolon | T], 0).
+wsafter(id,1).
+wsafter(cases,1).
+wsafter(case,1).
+wsafter(default,1).
+wsafter(Prev, Cur, Next, X) :- wsafter(Cur,X).

rt-key/pom.xml

@@ -16,7 +16,7 @@
 	<dependencies>
 		<dependency>
 			<groupId>edu.kit.iti.formal.psdbg</groupId>
-			<artifactId>runtime</artifactId>
+			<artifactId>rt</artifactId>
 			<version>0.1-SNAPSHOT</version>
 		</dependency>
 		<dependency>

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

+package edu.kit.iti.formal.psdbg;
+
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+import org.apache.commons.lang.ArrayUtils;
+import org.key_project.util.collection.ImmutableList;
+
+import java.util.Collections;
+import java.util.List;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+/**
+ * Utillities for producing labels of KeY proof nodes
+ *
+ * @author Alexander Weigl
+ * @see edu.kit.iti.formal.psdbg.interpreter.data.KeyData
+ * @see Node
+ */
+public class LabelFactory {
+    public static String SEPARATOR = " // ";
+
+    public static String RANGE_SEPARATOR = " -- ";
+
+
+    /**
+     * Create Label for goalview according to function that is passed.
+     * The following functions can be given:
+     * <ul>
+     * <li>@see  #Method getRuleLabel()</li>
+     * <li>@see  #Method getBranchingLabel()</li>
+     * <li>@see  #Method getNameLabel()</li>
+     * <li>@see  #Method getProgramLinesLabel()</li>
+     * <li>@see  #Method getProgramStatementsLabel()</li>
+     * </ul>
+     *
+     * @param projection function determining which kind of label to construct
+     * @return Label from this node to parent
+     */
+    private static String constructLabel(Node cur, Function<Node, String> projection) {
+        StringBuilder sb = new StringBuilder();
+        do {
+            try {
+                String section = projection.apply(cur);
+                //filter null elements and -1 elements
+                if (section != null && !(section.equals(Integer.toString(-1)))) {
+                    sb.append(section);
+                    sb.append(SEPARATOR);
+
+                }
+            } catch (Exception e) {
+            }
+            cur = cur.parent();
+        } while (cur != null);
+        sb.append("$$");
+        return sb.toString();
+    }
+
+    public static String getBranchingLabel(Node node) {
+        return constructLabel(node, n -> n.getNodeInfo().getBranchLabel());
+    }
+
+    public static String getNameLabel(Node node) {
+        return constructLabel(node, Node::name);
+    }
+
+    public static String getRuleLabel(Node node) {
+        return constructLabel(node, (n) -> n.getAppliedRuleApp().rule().name().toString());
+    }
+
+    public static String getProgramLines(Node node) {
+        return constructLabel(node, n -> {
+            int startPos = n.getNodeInfo().getActiveStatement().getPositionInfo().getStartPosition().getLine();
+            int endPos = n.getNodeInfo().getActiveStatement().getPositionInfo().getEndPosition().getLine();
+            if (startPos == endPos) {
+                return Integer.toString(startPos);
+            } else {
+                String start = Integer.toString(startPos);
+                String end = Integer.toString(endPos);
+                return start + RANGE_SEPARATOR + end;
+            }
+        });
+    }
+
+    public static String getProgramStatmentLabel(Node node) {
+        return constructLabel(node, n ->
+                n.getNodeInfo().getFirstStatementString());
+    }
+
+    public static List<String[]> getLabelOfOpenGoals(Proof root, Function<Node, String> func) {
+        if (root.closed())
+            return Collections.emptyList();
+        ImmutableList<Goal> open = root.getSubtreeGoals(root.root());
+        return open.stream()
+                .map(Goal::node)
+                .map(func)
+                .map(s -> s.split(SEPARATOR))
+                .map(a -> {
+                    ArrayUtils.reverse(a);
+                    return a;
+                })
+                .collect(Collectors.toList());
+    }
+}

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

 package edu.kit.iti.formal.psdbg.interpreter.data;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.java.Label;
 import de.uka.ilkd.key.java.SourceElement;
 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.LabelFactory;
 import lombok.*;
 
 import java.util.HashSet;
@@ -22,8 +24,6 @@ import java.util.function.Function;
 @EqualsAndHashCode
 @RequiredArgsConstructor
 public class KeyData {
-    private static final String SEPARATOR = " // ";
-    private static final String RANGE_SEPARATOR = " -- ";
     private final KeYEnvironment env;
     private final Proof proof;
     private Node node;
@@ -71,43 +71,12 @@ public class KeyData {
      */
     public String getRuleLabel() {
         if (ruleLabel == null) {
-            ruleLabel = constructLabel((Node n) -> n.getAppliedRuleApp().rule().name().toString());
+            ruleLabel =  LabelFactory.getRuleLabel(getNode());
         }
         return ruleLabel;
     }
 
-    /**
-     * Create Label for goalview according to function that is passed.
-     * The following functions can be given:
-     * <ul>
-     *     <li>@see  #Method getRuleLabel()</li>
-     *     <li>@see  #Method getBranchingLabel()</li>
-     *     <li>@see  #Method getNameLabel()</li>
-     *     <li>@see  #Method getProgramLinesLabel()</li>
-     *     <li>@see  #Method getProgramStatementsLabel()</li>
-     * </ul>
-     * @param projection function determining which kind of label to construct
-     * @return Label from this node to parent
-     */
-    private String constructLabel(Function<Node, String> projection) {
-        StringBuilder sb = new StringBuilder();
-        Node cur = getNode();
-        do {
-            try {
-                String section = projection.apply(cur);
-                //filter null elements and -1 elements
-                if (section != null && !(section.equals(Integer.toString(-1)))) {
-                    sb.append(section);
-                    sb.append(SEPARATOR);
 
-                }
-            } catch (Exception e) {
-            }
-            cur = cur.parent();
-        } while (cur != null);
-        sb.append("$$");
-        return sb.toString();
-    }
 
     /**
      * Get branching label of node from KeY
@@ -115,7 +84,7 @@ public class KeyData {
      */
     public String getBranchingLabel() {
         if (branchingLabel == null) {
-            branchingLabel = constructLabel(n -> n.getNodeInfo().getBranchLabel());
+            branchingLabel = LabelFactory.getBranchingLabel(getNode());
         }
         return branchingLabel;
     }
@@ -126,7 +95,7 @@ public class KeyData {
      */
     public String getNameLabel() {
         if (nameLabel == null) {
-            nameLabel = constructLabel(Node::name);
+            nameLabel = LabelFactory.getNameLabel(getNode());
         }
         return nameLabel;
     }
@@ -137,17 +106,7 @@ public class KeyData {
      */
     public String getProgramLinesLabel() {
         if (programLinesLabel == null) {
-            programLinesLabel = constructLabel(n -> {
-                int startPos = n.getNodeInfo().getActiveStatement().getPositionInfo().getStartPosition().getLine();
-                int endPos = n.getNodeInfo().getActiveStatement().getPositionInfo().getEndPosition().getLine();
-                if (startPos == endPos) {
-                    return Integer.toString(startPos);
-                } else {
-                    String start = Integer.toString(startPos);
-                    String end = Integer.toString(endPos);
-                    return start + RANGE_SEPARATOR + end;
-                }
-            });
+            programLinesLabel = LabelFactory.getProgramLines(getNode());
         }
         return programLinesLabel;
     }
@@ -158,10 +117,8 @@ public class KeyData {
      */
     public String getProgramStatementsLabel() {
         if (programStatementsLabel == null) {
-            programStatementsLabel = constructLabel(n ->
-                    n.getNodeInfo().getFirstStatementString());
+            programStatementsLabel = LabelFactory.getProgramStatmentLabel(getNode());
         }
-
         return programStatementsLabel;
     }
 

rt/pom.xml

@@ -9,7 +9,7 @@
 		<relativePath>..</relativePath>
 	</parent>
 
-	<artifactId>runtime</artifactId>
+	<artifactId>rt</artifactId>
 	<packaging>jar</packaging>
 
 	<dependencies>

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

 package edu.kit.iti.formal.psdbg.gui.controller;
 
+import alice.tuprolog.InvalidLibraryException;
+import alice.tuprolog.InvalidTheoryException;
 import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
@@ -10,6 +12,7 @@ import de.uka.ilkd.key.speclang.Contract;
 import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
 import edu.kit.iti.formal.psdbg.StepIntoCommand;
 import edu.kit.iti.formal.psdbg.examples.Examples;
+import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
 import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
 import edu.kit.iti.formal.psdbg.gui.controls.*;
 import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
@@ -145,6 +148,15 @@ public class DebuggerMain implements Initializable {
 
     private Timer interpreterThreadTimer;
 
+    @Subscribe
+    public void handle(Events.ShowSequent ss) {
+        SequentView sv = new SequentView();
+        sv.setKeYProofFacade(FACADE);
+        sv.setNode(ss.getNode());
+        DockNode node = new DockNode(sv, "Sequent Viewer " + ss.getNode().serialNr());
+        node.dock(dockStation, DockPos.CENTER);
+    }
+
     @Subscribe
     public void handle(Events.PublishMessage message) {
         if (message.getFlash() == 0)
@@ -876,6 +888,19 @@ public class DebuggerMain implements Initializable {
         return scriptController;
     }
 
+    @FXML
+    public void reformatCurrentEditor(ActionEvent event) {
+        scriptController.getOpenScripts().values().forEach(ed -> {
+            try {
+                DefaultFormatter df = new DefaultFormatter();
+                ((ScriptArea) ed.getContents()).setText(
+                        df.format(((ScriptArea) ed.getContents()).getText()));
+            } catch (InvalidLibraryException | IOException | InvalidTheoryException e) {
+                LOGGER.debug(e);
+            }
+        });
+    }
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected void succeeded() {

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

@@ -89,19 +89,44 @@ public class Events {
         private final List<GoalNode> openNodes;
     }
 
-
+    /**
+     *
+     */
     @Data
     @RequiredArgsConstructor
     public static class SelectNodeInGoalList {
         private final Node node;
     }
 
+    /**
+     * @author weigl
+     */
     @Data
     @RequiredArgsConstructor
     @AllArgsConstructor
     public static class PublishMessage {
-        private String message;
+        private final String message;
 
         private int flash = 0;
     }
+
+    /**
+     *
+     */
+    @Data
+    @RequiredArgsConstructor
+    public static class ShowSequent {
+        private final Node node;
+    }
+
+    /**
+     * Der Gipfel an doofen Eventnamen
+     *
+     * @author weigl
+     */
+    @Data
+    @RequiredArgsConstructor
+    public static class InsertAtTheEndOfMainScript {