more work done

* PrettyPrinter feature complete
* AST fully created
* small changes on Grammar

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

@@ -5,7 +5,7 @@ start
     ;
 
 argList
-    :   varDecl (',' varDecl)+
+    :   varDecl (',' varDecl)*
     ;
 
 varDecl
@@ -76,12 +76,16 @@ repeatStmt
     ;
 
 casesStmt
-    :   CASES INDENT casesList+ DEDENT
+    :   CASES INDENT
+            casesList*
+        (DEFAULT  COLON? INDENT
+            defList=stmtList
+          DEDENT)?
+        DEDENT
     ;
 
 casesList
-    :   CASE expression COLON? INDENT stmtList DEDENT casesList*
-    |   DEFAULT  COLON? INDENT stmtList DEDENT
+    :   CASE expression COLON? INDENT stmtList DEDENT
     ;
 
 forEachStmt

src/main/java/edu/kit/formatl/proofscriptparser/ASTChanger.java

@@ -3,8 +3,6 @@ package edu.kit.formatl.proofscriptparser;
 import edu.kit.formatl.proofscriptparser.ast.*;
 
 import java.util.ArrayList;
-import java.util.Map;
-import java.util.Set;
 
 /**
  * {@link ASTChanger} provides a visitor with for replacing or substiting nodes (in situ).
@@ -79,12 +77,8 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
         return caseStatement;
     }
 
-    @Override public ScriptCallStatement visit(ScriptCallStatement call) {
-        Map<String, Expression> p = call.getParameters();
-        Set<Map.Entry<String, Expression>> entries = call.getParameters().entrySet();
-        for (Map.Entry<String, Expression> e : entries) {
-            p.put(e.getKey(), (Expression) e.getValue().accept(this));
-        }
+    @Override public CallStatement visit(CallStatement call) {
+        call.setParameters((Parameters) call.getParameters().accept(this));
         return call;
     }
 }

src/main/java/edu/kit/formatl/proofscriptparser/ASTTraversal.java

@@ -73,7 +73,7 @@ public class ASTTraversal<T> implements Visitor<T> {
         return null;
     }
 
-    @Override public T visit(ScriptCallStatement call) {
+    @Override public T visit(CallStatement call) {
         for (Expression e : call.getParameters().values()) {
             e.accept(this);
         }
@@ -99,4 +99,8 @@ public class ASTTraversal<T> implements Visitor<T> {
     @Override public T visit(Parameters parameters) {
         return null;
     }
+
+    @Override public T visit(UnaryExpression e) {
+        return null;
+    }
 }

src/main/java/edu/kit/formatl/proofscriptparser/ast/DefaultASTVisitor.java → src/main/java/edu/kit/formatl/proofscriptparser/DefaultASTVisitor.java

-package edu.kit.formatl.proofscriptparser.ast;
+package edu.kit.formatl.proofscriptparser;
 
 import edu.kit.formatl.proofscriptparser.Visitor;
+import edu.kit.formatl.proofscriptparser.ast.*;
 
 /**
  * @author Alexander Weigl
@@ -55,7 +56,7 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
         return null;
     }
 
-    @Override public T visit(ScriptCallStatement call) {
+    @Override public T visit(CallStatement call) {
         return null;
     }
 
@@ -78,4 +79,8 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     @Override public T visit(Parameters parameters) {
         return null;
     }
+
+    @Override public T visit(UnaryExpression unaryExpression) {
+        return null;
+    }
 }

src/main/java/edu/kit/formatl/proofscriptparser/PrettyPrinter.java

@@ -10,8 +10,10 @@ import java.util.Map;
  * @version 1 (28.04.17)
  */
 public class PrettyPrinter extends DefaultASTVisitor<Void> {
+    private static final int MAX_WIDTH = 80;
     private final StringBuilder s = new StringBuilder();
     private int indentation = 0;
+    private int currentLineLength;
 
     @Override public String toString() {
         return s.toString();
@@ -50,14 +52,52 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
     }
 
     @Override public Void visit(BinaryExpression e) {
+        boolean left = e.getPrecedence() < e.getLeft().getPrecedence();
+        boolean right = e.getPrecedence() < e.getRight().getPrecedence();
+
+        if (left) {
+            s.append("(");
+        }
         e.getLeft().accept(this);
+        if (left) {
+            s.append(")");
+        }
+
         s.append(e.getOperator().symbol());
+
+        if (right) {
+            s.append("(");
+        }
         e.getRight().accept(this);
+        if (right) {
+            s.append(")");
+        }
+
         return super.visit(e);
     }
 
-    @Override public Void visit(MatchExpression matchExpression) {
-        return super.visit(matchExpression);
+    @Override public Void visit(MatchExpression match) {
+        s.append("match ");
+        String prefix = getWhitespacePrefix();
+        if (match.getTerm() != null) {
+            match.getTerm().accept(this);
+        }
+
+        if (!match.getSignature().isEmpty()) {
+
+            if (getCurrentLineLength() > MAX_WIDTH) {
+                s.append("\n").append(prefix);
+            }
+            else {
+                s.append(" ");
+            }
+
+            s.append("using [");
+            match.getSignature().accept(this);
+            s.append("]");
+        }
+
+        return null;
     }
 
     @Override public Void visit(CasesStatement casesStatement) {
@@ -68,6 +108,12 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
             c.accept(this);
             nl();
         }
+        if(casesStatement.getDefaultCase()!=null) {
+            s.append("default {");
+            casesStatement.getDefaultCase().accept(this);
+            cl();
+            s.append("}");
+        }
         decrementIndent();
         cl();
         s.append("}");
@@ -95,13 +141,9 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         return super.visit(caseStatement);
     }
 
-    @Override public Void visit(ScriptCallStatement call) {
+    @Override public Void visit(CallStatement call) {
         s.append(call.getCommand()).append(' ');
-        call.getParameters().forEach((k, v) -> {
-            s.append(k).append(" = ");
-            v.accept(this);
-            s.append(" ");
-        });
+        call.getParameters().accept(this);
         s.append(";");
         return null;
     }
@@ -127,6 +169,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
     }
 
     @Override public Void visit(Statements statements) {
+        if (statements.size() == 0)
+            return null;
         incrementIndent();
         for (Statement s : statements) {
             nl();
@@ -141,6 +185,71 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         return null;
     }
 
+    @Override public Void visit(TheOnlyStatement theOnly) {
+        s.append("theonly {");
+        theOnly.getBody().accept(this);
+        cl();
+        s.append("}");
+        return null;
+    }
+
+    @Override public Void visit(ForeachStatement foreach) {
+        s.append("foreach {");
+        foreach.getBody().accept(this);
+        cl();
+        s.append("}");
+        return null;
+    }
+
+    @Override public Void visit(RepeatStatement repeat) {
+        s.append("repeat");
+        s.append("{");
+        repeat.getBody().accept(this);
+        cl();
+        s.append("}");
+        return null;
+
+    }
+
+    @Override public Void visit(Parameters parameters) {
+        int nl = getLastNewline();
+        String indention = getWhitespacePrefix();
+        Iterator<Map.Entry<Variable, Expression>> iter = parameters.entrySet().iterator();
+
+        while (iter.hasNext()) {
+            Map.Entry<Variable, Expression> entry = iter.next();
+            entry.getKey().accept(this);
+            s.append("=");
+            entry.getValue().accept(this);
+            if (iter.hasNext()) {
+                int currentLineLength = getCurrentLineLength();
+                if (currentLineLength > 80) {
+                    s.append("\n").append(indention);
+                }
+                else {
+                    s.append(" ");
+                }
+            }
+        }
+        return null;
+    }
+
+    private int getLastNewline() {
+        int posnewline = s.length() - 1;
+        while (s.charAt(posnewline) != '\n') {
+            posnewline--;
+        }
+        return posnewline;
+    }
+
+    private String getWhitespacePrefix() {
+        return s.substring(getLastNewline() + 1).replaceAll("\\w", " ");
+    }
+
+    @Override public Void visit(UnaryExpression unaryExpression) {
+        return super.visit(unaryExpression);
+    }
+
     private void nl() {
         s.append('\n');
         for (int i = 0; i < indentation; i++)
@@ -155,4 +264,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         indentation++;
     }
 
+    public int getCurrentLineLength() {
+        return s.length() - getLastNewline();
+    }
 }

src/main/java/edu/kit/formatl/proofscriptparser/TransformAst.java

@@ -50,6 +50,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         }
         throw new IllegalStateException("Type " + n + " not defined");
     }
+
     //TODO check
     @Override public Object visitVarDecl(ScriptLanguageParser.VarDeclContext ctx) {
         VariableDeclaration varDecl = new VariableDeclaration();
@@ -98,13 +99,20 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         ue.setOperator(op);
         return ue;
     }
+
     @Override public Object visitExprMinus(ScriptLanguageParser.ExprMinusContext ctx) {
-       return createUnaryExpression(ctx, ctx.expression(), Operator.MINUS);
+        UnaryExpression ue = new UnaryExpression();
+ue.setRuleContext(...);
+        ue.setOperator(Operator.MINUS);
+        ue.setExpression((Expression) ctx.expression().accept(this));
+        return ue;
     }
 
     @Override public Object visitExprNegate(ScriptLanguageParser.ExprNegateContext ctx) {
-        return createUnaryExpression(ctx, ctx.expression(), Operator.NEG);
-
+        UnaryExpression ue = new UnaryExpression();
+        ue.setOperator(Operator.NOT);
+        ue.setExpression((Expression) ctx.expression().accept(this));
+        return ue;
     }
 
     @Override public Object visitExprComparison(ScriptLanguageParser.ExprComparisonContext ctx) {
@@ -188,7 +196,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     @Override public Object visitMatchPattern(ScriptLanguageParser.MatchPatternContext ctx) {
         MatchExpression match = new MatchExpression();
         match.setRuleContext(ctx);
-        match.setSignature((Map<String, String>) ctx.argList().accept(this));
+        match.setSignature((Signature) ctx.argList().accept(this));
         if (ctx.TERM_LITERAL() != null) {
             match.setTerm(new TermLiteral(ctx.TERM_LITERAL().getText()));
         }
@@ -212,6 +220,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     @Override public Object visitCasesStmt(ScriptLanguageParser.CasesStmtContext ctx) {
         CasesStatement cases = new CasesStatement();
         ctx.casesList().forEach(c -> cases.getCases().add((CaseStatement) c.accept(this)));
+        if (ctx.DEFAULT() != null) {
+            cases.setDefaultCase((Statements)
+                ctx.defList.accept(this)
+            );
+        }
+
         return cases;
     }
 
@@ -238,12 +252,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     }
 
     @Override public Object visitScriptCommand(ScriptLanguageParser.ScriptCommandContext ctx) {
-        ScriptCallStatement scs = new ScriptCallStatement();
+        CallStatement scs = new CallStatement();
         scs.setRuleContext(ctx);
         scs.setCommand(ctx.cmd.getText());
-        int i = 1;
         if (ctx.parameters() != null) {
-            ctx.parameters().accept(this);
+            scs.setParameters((Parameters) ctx.parameters().accept(this));
         }
         return scs;
     }

src/main/java/edu/kit/formatl/proofscriptparser/Visitor.java

@@ -31,19 +31,17 @@ public interface Visitor<T> {
 
     T visit(CaseStatement case_);
 
-    T visit(ScriptCallStatement call);
+    T visit(CallStatement call);
 
     T visit(TheOnlyStatement theOnly);
 
     T visit(ForeachStatement foreach);
 
-    T visit(RepeatStatement repeatStatement);
+    T visit(RepeatStatement repeat);
 
     T visit(Signature signature);
 
     T visit(Parameters parameters);
 
-    T visit(UnaryExpression unaryExpression);
-
-    T visit(VariableDeclaration variableDeclaration);
+    T visit(UnaryExpression e);
 }

src/main/java/edu/kit/formatl/proofscriptparser/ast/BinaryExpression.java

@@ -49,4 +49,8 @@ public class BinaryExpression extends Expression<ParserRuleContext> {
     public Expression getRight() {
         return right;
     }
+
+    @Override public int getPrecedence() {
+        return operator.precedence();
+    }
 }

src/main/java/edu/kit/formatl/proofscriptparser/ast/ScriptCallStatement.java → src/main/java/edu/kit/formatl/proofscriptparser/ast/CallStatement.java

@@ -3,16 +3,13 @@ package edu.kit.formatl.proofscriptparser.ast;
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formatl.proofscriptparser.Visitor;
 
-import java.util.LinkedHashMap;
-import java.util.Map;
-
 /**
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
-public class ScriptCallStatement extends Statement<ScriptLanguageParser.ScriptCommandContext> {
+public class CallStatement extends Statement<ScriptLanguageParser.ScriptCommandContext> {
     private String command;
-    private Map<String, Expression> parameters = new LinkedHashMap<>();
+    private Parameters parameters = new Parameters();
 
     @Override public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
@@ -30,12 +27,12 @@ public class ScriptCallStatement extends Statement<ScriptLanguageParser.ScriptCo
         return command;
     }
 
-    public ScriptCallStatement setParameters(Map<String, Expression> parameters) {
+    public CallStatement setParameters(Parameters parameters) {
         this.parameters = parameters;
         return this;
     }
 
-    public Map<String, Expression> getParameters() {
+    public Parameters getParameters() {
         return parameters;
     }
 

src/main/java/edu/kit/formatl/proofscriptparser/ast/CasesStatement.java

@@ -12,11 +12,21 @@ import java.util.List;
  */
 public class CasesStatement extends Statement<ScriptLanguageParser.CasesListContext> {
     private List<CaseStatement> cases = new ArrayList<>();
+    private Statements defaultCase = null;
 
     public List<CaseStatement> getCases() {
         return cases;
     }
 
+    public Statements getDefaultCase() {
+        return defaultCase;
+    }
+
+    public CasesStatement setDefaultCase(Statements defaultCase) {
+        this.defaultCase = defaultCase;
+        return this;
+    }
+
     @Override public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }

src/main/java/edu/kit/formatl/proofscriptparser/ast/Expression.java

@@ -7,4 +7,5 @@ import org.antlr.v4.runtime.ParserRuleContext;
  * @version 1 (28.04.17)
  */
 public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T> {
+    public abstract int getPrecedence();
 }

src/main/java/edu/kit/formatl/proofscriptparser/ast/GoalSelector.java

@@ -6,7 +6,7 @@ import org.antlr.v4.runtime.ParserRuleContext;
  * @author Alexander Weigl
  * @version 1 (29.04.17)
  */
-public abstract class GoalSelector<T extends ParserRuleContext> extends ASTNode<T> {
+public abstract class GoalSelector<T extends ParserRuleContext> extends Statement<T> {
     private Statements body;
 
     public Statements getBody() {

src/main/java/edu/kit/formatl/proofscriptparser/ast/Literal.java

@@ -21,6 +21,10 @@ public abstract class Literal extends Expression<ParserRuleContext> {
         return this;
     }
 
+    @Override public int getPrecedence() {
+        return 0;
+    }
+
     @Override public Optional<ParserRuleContext> getRuleContext() {
         return Optional.empty();
     }

src/main/java/edu/kit/formatl/proofscriptparser/ast/MatchExpression.java

@@ -3,14 +3,12 @@ package edu.kit.formatl.proofscriptparser.ast;
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formatl.proofscriptparser.Visitor;
 
-import java.util.Map;
-
 /**
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
 public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
-    private Map<String, String> signature;
+    private Signature signature;
     private TermLiteral term;
     private String variable;
 
@@ -22,11 +20,11 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter
         return null;
     }
 
-    public void setSignature(Map<String, String> signature) {
+    public void setSignature(Signature signature) {
         this.signature = signature;
     }
 
-    public Map<String, String> getSignature() {
+    public Signature getSignature() {
         return signature;
     }
 
@@ -41,4 +39,8 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter
     public TermLiteral getTerm() {
         return term;
     }
+
+    @Override public int getPrecedence() {
+        return Operator.MATCH.precedence();
+    }
 }

src/main/java/edu/kit/formatl/proofscriptparser/ast/Operator.java

 package edu.kit.formatl.proofscriptparser.ast;
 
 /**
+ * Precedence: zero is preserved for literals!
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
 public enum Operator {
-    MULTIPLY("*"), DIVISION("/"), AND("&&"), OR("||"), IMPLICATION("==>"),
-    PLUS("+"), MINUS("-"), EQ("="), NEQ("<>"), NEG("!");
+    /**
+     * special entry for marking match as an atomic expression.
+     */
+    MATCH("match", 1000),
+    NOT("not", "¬", 10),
+    MULTIPLY("*", "×", 20),
+    DIVISION("/", "÷", 20),
+    PLUS("+",  30),
+    MINUS("-", 30),
+    LE("<",40),
+    GE(">",40),
+    LEQ("<=", "≤",40),
+    GEQ(">=", "≥",40),
+    EQ("=", "≡", 50),
+    NEQ("<>","≢", 50),
+    AND("&&", "∧", 60),
+    OR("||", "∨", 70),
+    IMPLICATION("==>", "⇒", 80),
+    EQUIVALENCE("<=>", "⇔", 90);
 
     private final String symbol;
+    private final String unicode;
+    private final int precedence;
 
-    Operator(String symbol) {
+    Operator(String symbol, int precedence) {
+        this(symbol, symbol, precedence);
+    }
+
+    Operator(String symbol, String unicode, int precedence) {
         this.symbol = symbol;
+        this.unicode = unicode;
+        this.precedence = precedence;
+    }
+
+    public String unicode() {
+        return unicode;
     }
 
-    public  String symbol() {
+    public String symbol() {
         return symbol;
     }
 
+    public int precedence() {
+        return precedence;
+    }
+
 }

src/main/java/edu/kit/formatl/proofscriptparser/ast/UnaryExpression.java

@@ -2,34 +2,42 @@ package edu.kit.formatl.proofscriptparser.ast;
 
 import edu.kit.formatl.proofscriptparser.Visitor;
 import org.antlr.v4.runtime.ParserRuleContext;
+import org.antlr.v4.runtime.tree.TerminalNode;
 
 /**
- * Created by S.Grebing
+ * @author Alexander Weigl
+ * @author Sarah Grebing
+ * @version 1 (30.04.17)
  */
-public class UnaryExpression extends Expression<ParserRuleContext>{
-    private Operator operator;
+public class UnaryExpression extends Expression<ParserRuleContext> {
     private Expression expression;
+    private Operator