introducing lombok and type safety

pom.xml

@@ -89,5 +89,11 @@
             <artifactId>antlr4</artifactId>
             <version>4.7</version>
         </dependency>
+        <dependency>
+            <groupId>org.projectlombok</groupId>
+            <artifactId>lombok</artifactId>
+            <version>1.16.16</version>
+            <scope>provided</scope>
+        </dependency>
     </dependencies>
 </project>

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

@@ -157,7 +157,7 @@ GE : '>' ;
 LE : '<' ;
 AND : '&' ;
 OR: '|' ;
-IMP : '->' ;
+IMP : '==>' ;
 EQUIV : '<=>' ;
 NEGATE: 'not';
 

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

@@ -3,6 +3,8 @@ 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).
@@ -81,4 +83,42 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
         call.setParameters((Parameters) call.getParameters().accept(this));
         return call;
     }
+
+    @Override public ASTNode visit(TheOnlyStatement theOnly) {
+        theOnly.setBody((Statements) theOnly.getBody().accept(this));
+        return theOnly;
+    }
+
+    @Override public ASTNode visit(ForeachStatement foreach) {
+        foreach.setBody((Statements) foreach.getBody().accept(this));
+        return foreach;
+    }
+
+    @Override public ASTNode visit(RepeatStatement repeat) {
+        repeat.setBody((Statements) repeat.getBody().accept(this));
+        return repeat;
+    }
+
+    @Override public ASTNode visit(Signature signature) {
+        Set<Map.Entry<Variable, Type>> entries = signature.entrySet();
+        signature.clear();
+        for (Map.Entry<Variable, Type> e : entries) {
+            signature.put((Variable) e.getKey().accept(this), e.getValue());
+        }
+        return signature;
+    }
+
+    @Override public ASTNode visit(Parameters parameters) {
+        Set<Map.Entry<Variable, Expression>> entries = parameters.entrySet();
+        parameters.clear();
+        for (Map.Entry<Variable, Expression> e : entries) {
+            parameters.put((Variable) e.getKey().accept(this), e.getValue());
+        }
+        return parameters;
+    }
+
+    @Override public ASTNode visit(UnaryExpression e) {
+        e.setExpression((Expression) e.getExpression().accept(this));
+        return e;
+    }
 }

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

@@ -11,25 +11,52 @@ import java.io.IOException;
 import java.util.List;
 
 /**
+ * This class captures high-level functions of this package.
+ *
  * @author Alexander Weigl
  * @version 1 (27.04.17)
  */
 public final class Facade {
+    /**
+     * Parses the given {@link CharStream} and returns the {@link ParserRuleContext}.
+     *
+     * @param stream containing the proof script
+     * @return
+     */
     public static ScriptLanguageParser.StartContext parseStream(CharStream stream) {
         ScriptLanguageParser slp = new ScriptLanguageParser(new CommonTokenStream(new ScriptLanguageLexer(stream)));
         return slp.start();
     }
 
+    /**
+     * Parses the given proof script from <code>stream</code> into an AST.
+     *
+     * @param stream
+     * @return
+     */
     public static List<ProofScript> getAST(CharStream stream) {
         TransformAst astt = new TransformAst();
         parseStream(stream).accept(astt);
         return astt.getScripts();
     }
 
+    /**
+     * Parses an AST from the given <code>inputfile</code>
+     *
+     * @param inputfile
+     * @return
+     * @throws IOException
+     */
     public static List<ProofScript> getAST(File inputfile) throws IOException {
         return getAST(CharStreams.fromPath(inputfile.toPath()));
     }
 
+    /**
+     * Returns a prettified output of the given AST.
+     *
+     * @param node
+     * @return
+     */
     public static String prettyPrint(ASTNode node) {
         PrettyPrinter prettyPrinter = new PrettyPrinter();
         node.accept(prettyPrinter);

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

+package edu.kit.formatl.proofscriptparser;
+
+import edu.kit.formatl.proofscriptparser.ast.Expression;
+import lombok.AllArgsConstructor;
+import lombok.Data;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (01.05.17)
+ */
+@Data
+@AllArgsConstructor
+public class NotWelldefinedException extends Exception {
+    private final Expression expr;
+
+    public NotWelldefinedException(String message, Expression expr) {
+        super(message);
+        this.expr = expr;
+    }
+}

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

@@ -11,9 +11,9 @@ import java.util.Map;
  */
 public class PrettyPrinter extends DefaultASTVisitor<Void> {
     private static final int MAX_WIDTH = 80;
+    private boolean unicode = true;
     private final StringBuilder s = new StringBuilder();
     private int indentation = 0;
-    private int currentLineLength;
 
     @Override public String toString() {
         return s.toString();
@@ -32,9 +32,9 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
     }
 
     @Override public Void visit(Signature sig) {
-        Iterator<Map.Entry<Variable, String>> iter = sig.entrySet().iterator();
+        Iterator<Map.Entry<Variable, Type>> iter = sig.entrySet().iterator();
         while (iter.hasNext()) {
-            Map.Entry<Variable, String> next = iter.next();
+            Map.Entry<Variable, Type> next = iter.next();
             next.getKey().accept(this);
             s.append(" : ").append(next.getValue());
             if (iter.hasNext())
@@ -63,8 +63,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
             s.append(")");
         }
 
-        s.append(e.getOperator().symbol());
-
+        s.append(' ').append(unicode ? e.getOperator().unicode() : e.getOperator().symbol()).append(' ');
         if (right) {
             s.append("(");
         }
@@ -108,7 +107,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
             c.accept(this);
             nl();
         }
-        if(casesStatement.getDefaultCase()!=null) {
+        if (casesStatement.getDefaultCase() != null) {
             s.append("default {");
             casesStatement.getDefaultCase().accept(this);
             cl();
@@ -163,9 +162,9 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         return super.visit(variable);
     }
 
-    @Override public Void visit(BooleanLiteral booleanLiteral) {
-        s.append(booleanLiteral.getValue());
-        return super.visit(booleanLiteral);
+    @Override public Void visit(BooleanLiteral bool) {
+        s.append(bool.isValue());
+        return super.visit(bool);
     }
 
     @Override public Void visit(Statements statements) {
@@ -223,7 +222,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
             entry.getValue().accept(this);
             if (iter.hasNext()) {
                 int currentLineLength = getCurrentLineLength();
-                if (currentLineLength > 80) {
+                if (currentLineLength > MAX_WIDTH) {
                     s.append("\n").append(indention);
                 }
                 else {
@@ -234,6 +233,18 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         return null;
     }
 
+    @Override public Void visit(UnaryExpression e) {
+        s.append(unicode ? e.getOperator().unicode() : e.getOperator().symbol());
+        if (e.getPrecedence() < e.getExpression().getPrecedence())
+            s.append("(");
+        e.getExpression().accept(this);
+        if (e.getPrecedence() < e.getExpression().getPrecedence())
+            s.append(")");
+        return null;
+    }
+
+    //region Printers little helper
+
     private int getLastNewline() {
         int posnewline = s.length() - 1;
         while (s.charAt(posnewline) != '\n') {
@@ -246,10 +257,6 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         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++)
@@ -267,4 +274,25 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
     public int getCurrentLineLength() {
         return s.length() - getLastNewline();
     }
+
+    //endregion
+
+    /**
+     * Flag for indicating, that the unicode operation symbols should be used.
+     *
+     * @return
+     */
+    public boolean isUnicode() {
+        return unicode;
+    }
+
+    /**
+     * @param unicode
+     * @return
+     * @see #isUnicode()
+     */
+    public PrettyPrinter setUnicode(boolean unicode) {
+        this.unicode = unicode;
+        return this;
+    }
 }

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

@@ -38,7 +38,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     @Override public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) {
         Signature signature = new Signature();
         for (ScriptLanguageParser.VarDeclContext decl : ctx.varDecl()) {
-            signature.put(new Variable(decl.name), decl.type.getText());
+            signature.put(new Variable(decl.name), Type.valueOf(decl.type.getText()));
         }
         return signature;
     }
@@ -201,7 +201,7 @@ ue.setRuleContext(...);
             match.setTerm(new TermLiteral(ctx.TERM_LITERAL().getText()));
         }
         else {
-            match.setVariable(ctx.ID().getText());
+            match.setVariable(new Variable(ctx.ID().getSymbol()));
         }
         return match;
     }

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

@@ -2,23 +2,25 @@ package edu.kit.formatl.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formatl.proofscriptparser.Visitor;
+import lombok.*;
 
 /**
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
-public class AssignmentStatement extends Statement<ScriptLanguageParser.AssignmentContext> {
-    private Variable rhs;
-    private Expression lhs;
-
-    //TODO type missing, if initialization
+@Data @ToString(includeFieldNames = true) @NoArgsConstructor @RequiredArgsConstructor() @AllArgsConstructor
+public class AssignmentStatement
+        extends Statement<ScriptLanguageParser.AssignmentContext> {
+    @NonNull private Variable rhs;
+    @NonNull private Expression lhs;
+    private Type type;
 
     @Override public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
-    @Override public ASTNode<ScriptLanguageParser.AssignmentContext> clone() {
-        return null;
+    @Override public AssignmentStatement clone() {
+        return new AssignmentStatement(rhs.clone(), lhs.clone());
     }
 
     public void setRhs(Variable rhs) {
@@ -37,7 +39,4 @@ public class AssignmentStatement extends Statement<ScriptLanguageParser.Assignme
         return lhs;
     }
 
-    @Override public String toString() {
-        return String.format("%s := %s", rhs, lhs);
-    }
 }

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

 package edu.kit.formatl.proofscriptparser.ast;
 
+import edu.kit.formatl.proofscriptparser.NotWelldefinedException;
 import edu.kit.formatl.proofscriptparser.Visitor;
+import lombok.Data;
 import org.antlr.v4.runtime.ParserRuleContext;
 
 /**
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
+@Data
 public class BinaryExpression extends Expression<ParserRuleContext> {
-    private Expression left,right;
+    private Expression left, right;
     private Operator operator;
 
-    public BinaryExpression setLeft(Expression left) {
-        this.left = left;
-        return this;
+    public BinaryExpression() {
     }
 
-    public BinaryExpression setRight(Expression right) {
+    public BinaryExpression(Expression left, Operator operator, Expression right) {
+        this.left = left;
+        this.operator = operator;
         this.right = right;
-        return this;
     }
 
-    @Override public <T> T accept(Visitor<T> visitor) {
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
-    @Override public ASTNode<ParserRuleContext> clone() {
-        return null;
+    @Override
+    public BinaryExpression clone() {
+        BinaryExpression be = new BinaryExpression(left.clone(), operator, right.clone());
+        return be;
     }
 
-    public void setOperator(Operator operator) {
-        this.operator = operator;
-    }
+    @Override
+    public Type getType(Signature signature) throws NotWelldefinedException {
+        if (operator.arity() != 2)
+            throw new NotWelldefinedException("Arity mismatch", this);
 
-    public Operator getOperator() {
-        return operator;
-    }
-
-
-    @Override public String toString() {
-        return "BinaryExpression{" + "left=" + left + ", right=" + right + ", operator=" + operator + '}';
-    }
-
-    public Expression getLeft() {
-        return left;
-    }
+        operator.type()[0].equals(left.getType(signature));
+        operator.type()[1].equals(right.getType(signature));
 
-    public Expression getRight() {
-        return right;
+        return operator.returnType();
     }
 
-    @Override public int getPrecedence() {
+    @Override
+    public int getPrecedence() {
         return operator.precedence();
     }
 }

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

 package edu.kit.formatl.proofscriptparser.ast;
 
+import edu.kit.formatl.proofscriptparser.NotWelldefinedException;
 import edu.kit.formatl.proofscriptparser.Visitor;
-import org.antlr.v4.runtime.ParserRuleContext;
+import lombok.*;
 import org.antlr.v4.runtime.Token;
 
 import java.util.Optional;
@@ -10,9 +11,13 @@ import java.util.Optional;
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
+@Data
+@EqualsAndHashCode(callSuper = false)
+@Getter
 public class BooleanLiteral extends Literal {
     public static final BooleanLiteral FALSE = new BooleanLiteral(false);
     public static final BooleanLiteral TRUE = new BooleanLiteral(true);
+
     private final boolean value;
 
     public BooleanLiteral(boolean value, Token token) {
@@ -28,19 +33,18 @@ public class BooleanLiteral extends Literal {
         this(b, null);
     }
 
-    @Override public <T> T accept(Visitor<T> visitor) {
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
-    @Override public ASTNode<ParserRuleContext> clone() {
-        return null;
-    }
-
-    @Override public String toString() {
-        return "BooleanLiteral{" + "value=" + value + '}';
+    @Override
+    public BooleanLiteral clone() {
+        return new BooleanLiteral(value, token.orElse(null));
     }
 
-    public boolean getValue() {
-        return value;
+    @Override
+    public Type getType(Signature signature) throws NotWelldefinedException {
+        return Type.bool;
     }
 }

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

@@ -2,38 +2,25 @@ package edu.kit.formatl.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formatl.proofscriptparser.Visitor;
+import lombok.*;
 
 /**
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
+@Data
+@NoArgsConstructor
+@RequiredArgsConstructor
+@AllArgsConstructor
 public class CallStatement extends Statement<ScriptLanguageParser.ScriptCommandContext> {
-    private String command;
+    @NonNull private String command;
     private Parameters parameters = new Parameters();
 
     @Override public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
-    @Override public ASTNode<ScriptLanguageParser.ScriptCommandContext> clone() {
-        return null;
+    @Override public CallStatement clone() {
+        return new CallStatement(command, parameters.clone());
     }
-
-    public void setCommand(String command) {
-        this.command = command;
-    }
-
-    public String getCommand() {
-        return command;
-    }
-
-    public CallStatement setParameters(Parameters parameters) {
-        this.parameters = parameters;
-        return this;
-    }
-
-    public Parameters getParameters() {
-        return parameters;
-    }
-
 }

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

@@ -2,38 +2,31 @@ package edu.kit.formatl.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formatl.proofscriptparser.Visitor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
 
 /**
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
+@Data
+@NoArgsConstructor
 public class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
     private Expression guard;
     private Statements body;
 
-    public Expression getGuard() {
-        return guard;
-    }
 
-    public CaseStatement setGuard(Expression guard) {
+    public CaseStatement(Expression guard, Statements body) {
         this.guard = guard;
-        return this;
-    }
-
-    public Statements getBody() {
-        return body;
-    }
-
-    public CaseStatement setBody(Statements body) {
         this.body = body;
-        return this;
     }
 
+
     @Override public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
-    @Override public ASTNode<ScriptLanguageParser.CasesListContext> clone() {
-        return null;
+    @Override public CaseStatement clone() {
+        return new CaseStatement(guard.clone(), body.clone());
     }
 }

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

@@ -2,6 +2,7 @@ package edu.kit.formatl.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formatl.proofscriptparser.Visitor;
+import lombok.Data;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -10,9 +11,10 @@ import java.util.List;
  * @author Alexander Weigl
  * @version 1 (28.04.17)
  */
+@Data
 public class CasesStatement extends Statement<ScriptLanguageParser.CasesListContext> {
     private List<CaseStatement> cases = new ArrayList<>();
-    private Statements defaultCase = null;
+    private Statements defaultCase = new Statements();
 
     public List<CaseStatement> getCases() {
         return cases;
@@ -31,7 +33,11 @@ public class CasesStatement extends Statement<ScriptLanguageParser.CasesListCont
         return visitor.visit(this);
     }
 
-    @Override public ASTNode<ScriptLanguageParser.CasesListContext> clone() {
-        return null;
+    @Override public CasesStatement clone() {
+        CasesStatement c = new CasesStatement();
+        cases.forEach(caseStatement -> c.cases.add(caseStatement.clone()));
+        if (defaultCase != null)
+            c.defaultCase = defaultCase.clone();
+        return c;
     }
 }

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

 package edu.kit.formatl.proofscriptparser.ast;
 
+import edu.kit.formatl.proofscriptparser.NotWelldefinedException;
 import org.antlr.v4.runtime.ParserRuleContext;
 
 /**
@@ -8,4 +9,10 @@ import org.antlr.v4.runtime.ParserRuleContext;
  */
 public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T> {
     public abstract int getPrecedence();
+
+    @Override public abstract Expression clone();
+
+    public abstract Type getType(Signature signature)
+            throws NotWelldefinedException;
+
 }

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

@@ -2,17 +2,26 @@ package edu.kit.formatl.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formatl.proofscriptparser.Visitor;
+import lombok.Data;
 
 /**
  * @author Alexander Weigl
  * @version 1 (29.04.17)
  */
+@Data
 public class ForeachStatement extends GoalSelector<ScriptLanguageParser.ForEachStmtContext> {
+    public ForeachStatement() {
+    }
+
+    public ForeachStatement(Statements statements) {
+        super(statements);
+    }
+
     @Override public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
-    @Override public ASTNode<ScriptLanguageParser.ForEachStmtContext> clone() {
-        return null;
+    @Override public ForeachStatement clone() {
+        return new ForeachStatement(getBody().clone());
     }
 }

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

 package edu.kit.formatl.proofscriptparser.ast;
 
+import lombok.*;
 import org.antlr.v4.runtime.ParserRuleContext;
 
 /**