Commit db98546f authored by Alexander Weigl's avatar Alexander Weigl

Fixing a lot of errors found by EvaluatorTest

* BUG: Operator `not` hidden by `ID` in ScriptLanguage.g4
* BUG: Evaluator evaluation of binary
* BUG: TransformAst.java copy paste, BooleanLiteral for TRUE
* IMPROVE: Facade new method for creating parser
* BUG: Value equals/hashcode, wrong type for STRING
* IMPROVE: add test cases for Evaluator.java
parent 3476df23
Pipeline #10518 passed with stage
in 1 minute and 59 seconds
...@@ -146,9 +146,6 @@ BOOL: 'bool' ; ...@@ -146,9 +146,6 @@ BOOL: 'bool' ;
TERMTYPE : 'term' ;*/ TERMTYPE : 'term' ;*/
FOREACH : 'foreach' ; FOREACH : 'foreach' ;
THEONLY : 'theonly' ; THEONLY : 'theonly' ;
ID : [a-zA-Z] [_a-zA-Z0-9]* ;
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
INDENT : '{' ; INDENT : '{' ;
DEDENT : '}' ; DEDENT : '}' ;
SEMICOLON : ';' ; SEMICOLON : ';' ;
...@@ -178,8 +175,6 @@ IMP : '==>' ; ...@@ -178,8 +175,6 @@ IMP : '==>' ;
EQUIV : '<=>' ; EQUIV : '<=>' ;
NOT: 'not'; NOT: 'not';
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
ID : [a-zA-Z] [_a-zA-Z0-9]* ;
\ No newline at end of file
...@@ -3,26 +3,39 @@ package edu.kit.formal.interpreter; ...@@ -3,26 +3,39 @@ package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
import java.util.List;
import java.util.Stack;
/** /**
* Class handling evaluation of expressions (visitor for expressions) * Class handling evaluation of expressions (visitor for expressions)
* *
* @author S.Grebing * @author S.Grebing
*/ */
public class Evaluator extends DefaultASTVisitor<Value> { public class Evaluator extends DefaultASTVisitor<Value> {
State currentState; private State currentState;
private Stack<List<GoalNode>> matchedGoals = new Stack<>();
private EvaluatorABI abi;
public Evaluator(State s) { public Evaluator(State s) {
this.currentState = s; this.currentState = s;
} }
/**
* Evaluation of an expression.
*
* @param truth
* @return
*/
public Value eval(Expression truth) {
return (Value) truth.accept(this);
}
@Override @Override
public Value visit(BinaryExpression e) { public Value visit(BinaryExpression e) {
Value v1 = (Value) e.getLeft().accept(this); Value v1 = (Value) e.getLeft().accept(this);
Value v2 = (Value) e.getLeft().accept(this); Value v2 = (Value) e.getRight().accept(this);
Operator op = e.getOperator(); Operator op = e.getOperator();
return op.evaluate(v1, v2); return op.evaluate(v1, v2);
} }
/** /**
...@@ -33,7 +46,9 @@ public class Evaluator extends DefaultASTVisitor<Value> { ...@@ -33,7 +46,9 @@ public class Evaluator extends DefaultASTVisitor<Value> {
*/ */
@Override @Override
public Value visit(MatchExpression match) { public Value visit(MatchExpression match) {
return null;
return Value.TRUE;
} }
/** /**
...@@ -68,7 +83,7 @@ public class Evaluator extends DefaultASTVisitor<Value> { ...@@ -68,7 +83,7 @@ public class Evaluator extends DefaultASTVisitor<Value> {
@Override @Override
public Value visit(BooleanLiteral bool) { public Value visit(BooleanLiteral bool) {
return Value.from(bool); return bool.isValue() ? Value.TRUE : Value.FALSE;
} }
......
package edu.kit.formal.interpreter;
/**
* @author Alexander Weigl
* @version 1 (16.05.17)
*/
public interface EvaluatorABI {
}
...@@ -17,6 +17,9 @@ import java.math.BigInteger; ...@@ -17,6 +17,9 @@ import java.math.BigInteger;
*/ */
@RequiredArgsConstructor @RequiredArgsConstructor
public class Value<T> { public class Value<T> {
public static final Value TRUE = new Value<>(Type.BOOL, true);
public static final Value FALSE = new Value<>(Type.BOOL, false);
@Getter @Getter
private final Type type; private final Type type;
@Getter @Getter
...@@ -32,7 +35,7 @@ public class Value<T> { ...@@ -32,7 +35,7 @@ public class Value<T> {
} }
public static Value<String> from(StringLiteral s) { public static Value<String> from(StringLiteral s) {
return new Value<>(Type.INT, s.getText()); return new Value<>(Type.STRING, s.getText());
} }
public static Value<Boolean> from(BooleanLiteral b) { public static Value<Boolean> from(BooleanLiteral b) {
...@@ -47,6 +50,24 @@ public class Value<T> { ...@@ -47,6 +50,24 @@ public class Value<T> {
return new Value<>(Type.INT, apply); return new Value<>(Type.INT, apply);
} }
@Override
public boolean equals(Object o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
Value<?> value = (Value<?>) o;
if (getType() != value.getType()) return false;
return getData().equals(value.getData());
}
@Override
public int hashCode() {
int result = getType().hashCode();
result = 31 * result + getData().hashCode();
return result;
}
@Override @Override
public String toString() { public String toString() {
return "Value{" + return "Value{" +
......
...@@ -23,10 +23,12 @@ package edu.kit.formal.proofscriptparser; ...@@ -23,10 +23,12 @@ package edu.kit.formal.proofscriptparser;
*/ */
import edu.kit.formal.proofscriptparser.ast.ASTNode; import edu.kit.formal.proofscriptparser.ast.ASTNode;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
import org.antlr.v4.runtime.*; import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.ParserRuleContext;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
...@@ -45,9 +47,20 @@ public final class Facade { ...@@ -45,9 +47,20 @@ public final class Facade {
* @param stream containing the proof script * @param stream containing the proof script
* @return * @return
*/ */
public static ScriptLanguageParser.StartContext parseStream(CharStream stream) { public static ScriptLanguageParser getParser(CharStream stream) {
ScriptLanguageParser slp = new ScriptLanguageParser(new CommonTokenStream(new ScriptLanguageLexer(stream))); ScriptLanguageParser slp = new ScriptLanguageParser(new CommonTokenStream(new ScriptLanguageLexer(stream)));
return slp.start(); return slp;
}
/**
* Parses the given {@link CharStream} and returns the {@link ParserRuleContext}.
*
* @param stream containing the proof script
* @return
*/
public static ScriptLanguageParser.StartContext parseStream(CharStream stream) {
return getParser(stream).start();
} }
/** /**
......
...@@ -23,7 +23,6 @@ package edu.kit.formal.proofscriptparser; ...@@ -23,7 +23,6 @@ package edu.kit.formal.proofscriptparser;
*/ */
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.ParserRuleContext;
import org.antlr.v4.runtime.tree.ErrorNode; import org.antlr.v4.runtime.tree.ErrorNode;
...@@ -183,7 +182,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -183,7 +182,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override @Override
public Object visitExprLineOperators(ScriptLanguageParser.ExprLineOperatorsContext ctx) { public Object visitExprLineOperators(ScriptLanguageParser.ExprLineOperatorsContext ctx) {
return createBinaryExpression(ctx, ctx.expression(), findOperator(ctx.op.getText())); return createBinaryExpression(ctx, ctx.expression(), findOperator(ctx.op.getText()));
} }
...@@ -226,7 +225,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -226,7 +225,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override @Override
public Object visitLiteralTrue(ScriptLanguageParser.LiteralTrueContext ctx) { public Object visitLiteralTrue(ScriptLanguageParser.LiteralTrueContext ctx) {
return new BooleanLiteral(false, ctx.TRUE().getSymbol()); return new BooleanLiteral(true, ctx.TRUE().getSymbol());
} }
@Override @Override
...@@ -238,7 +237,8 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -238,7 +237,8 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
public Object visitMatchPattern(ScriptLanguageParser.MatchPatternContext ctx) { public Object visitMatchPattern(ScriptLanguageParser.MatchPatternContext ctx) {
MatchExpression match = new MatchExpression(); MatchExpression match = new MatchExpression();
match.setRuleContext(ctx); match.setRuleContext(ctx);
match.setSignature((Signature) ctx.argList().accept(this)); if (ctx.argList() != null)
match.setSignature((Signature) ctx.argList().accept(this));
if (ctx.TERM_LITERAL() != null) { if (ctx.TERM_LITERAL() != null) {
match.setTerm(new TermLiteral(ctx.TERM_LITERAL().getText())); match.setTerm(new TermLiteral(ctx.TERM_LITERAL().getText()));
} else { } else {
......
package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.TestHelper;
import edu.kit.formal.proofscriptparser.ast.Expression;
import org.junit.Assert;
import org.junit.Before;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
import java.io.IOException;
import java.util.Arrays;
import java.util.List;
/**
* @author Alexander Weigl
* @version 1 (16.05.17)
*/
@RunWith(Parameterized.class)
public class EvaluatorTest {
private final Expression expr, truth;
private Evaluator eval;
public EvaluatorTest(String e, String r) {
expr = TestHelper.toExpr(e);
truth = TestHelper.toExpr(r);
}
@Parameterized.Parameters(name = "{0} => {1}")
public static Iterable<Object[]> expr() throws IOException {
return TestHelper.loadLines("eval.txt", 2);
}
@Before public void setup() {
GoalNode parent = new GoalNode(null, "pa");
GoalNode selected = new GoalNode(parent,"sel");
GoalNode g1 = new GoalNode(parent,"g1");
GoalNode g2 = new GoalNode(parent,"g2");
List<GoalNode> goals = Arrays.asList(g1,g2,selected);
State state = new State(goals, selected);
eval = new Evaluator(state);
}
@Test
public void testEval() {
Value result = eval.eval(expr);
Value truthValue = eval.eval(truth);
System.out.println(expr);
Assert.assertEquals(truthValue, result);
}
}
\ No newline at end of file
...@@ -24,7 +24,6 @@ package edu.kit.formal.proofscriptparser; ...@@ -24,7 +24,6 @@ package edu.kit.formal.proofscriptparser;
import edu.kit.formal.proofscriptparser.ast.Expression;
import org.junit.Assert; import org.junit.Assert;
import org.junit.Test; import org.junit.Test;
import org.junit.runner.RunWith; import org.junit.runner.RunWith;
...@@ -36,7 +35,7 @@ import java.io.IOException; ...@@ -36,7 +35,7 @@ import java.io.IOException;
public class BadExpressionTest { public class BadExpressionTest {
@Parameterized.Parameters(name = "{0}") @Parameterized.Parameters(name = "{0}")
public static Iterable<Object[]> getBadExpressions() throws IOException { public static Iterable<Object[]> getBadExpressions() throws IOException {
return TestHelper.loadLines("badexpr.txt"); return TestHelper.loadLines("badexpr.txt", 1);
} }
@Parameterized.Parameter @Parameterized.Parameter
......
...@@ -40,7 +40,7 @@ import java.io.IOException; ...@@ -40,7 +40,7 @@ import java.io.IOException;
public class BadlyTypedExpression { public class BadlyTypedExpression {
@Parameterized.Parameters(name = "{0}") @Parameterized.Parameters(name = "{0}")
public static Iterable<Object[]> getBadExpressions() throws IOException { public static Iterable<Object[]> getBadExpressions() throws IOException {
return TestHelper.loadLines("badlytypedexpr.txt"); return TestHelper.loadLines("badlytypedexpr.txt", 1);
} }
@Parameterized.Parameter @Parameterized.Parameter
......
...@@ -39,7 +39,7 @@ import java.io.IOException; ...@@ -39,7 +39,7 @@ import java.io.IOException;
public class GoodExpressionTest { public class GoodExpressionTest {
@Parameterized.Parameters(name = "{0}") @Parameterized.Parameters(name = "{0}")
public static Iterable<Object[]> getGoodExpressions() throws IOException { public static Iterable<Object[]> getGoodExpressions() throws IOException {
return TestHelper.loadLines("goodexpr.txt"); return TestHelper.loadLines("goodexpr.txt", 1);
} }
@Parameterized.Parameter @Parameterized.Parameter
......
...@@ -23,12 +23,8 @@ package edu.kit.formal.proofscriptparser; ...@@ -23,12 +23,8 @@ package edu.kit.formal.proofscriptparser;
*/ */
import edu.kit.formal.proofscriptparser.ast.Expression;
import org.antlr.runtime.ANTLRInputStream;
import org.antlr.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
import org.junit.AssumptionViolatedException;
import java.io.*; import java.io.*;
import java.net.URL; import java.net.URL;
...@@ -46,7 +42,7 @@ public class TestHelper { ...@@ -46,7 +42,7 @@ public class TestHelper {
public static Iterable<Object[]> getResourcesAsParameters(String folder) { public static Iterable<Object[]> getResourcesAsParameters(String folder) {
File[] files = getResources(folder); File[] files = getResources(folder);
return Arrays.stream(files).map(f -> new Object[] { f }).collect(Collectors.toList()); return Arrays.stream(files).map(f -> new Object[]{f}).collect(Collectors.toList());
} }
public static final File[] getResources(String folder) { public static final File[] getResources(String folder) {
...@@ -59,7 +55,7 @@ public class TestHelper { ...@@ -59,7 +55,7 @@ public class TestHelper {
return file.listFiles(); return file.listFiles();
} }
public static Iterable<Object[]> loadLines(String filename) throws IOException { public static Iterable<Object[]> loadLines(String filename, int expectedArgs) throws IOException {
List<Object[]> validExpression = new ArrayList<>(4096); List<Object[]> validExpression = new ArrayList<>(4096);
InputStream ve = TestHelper.class.getResourceAsStream(filename); InputStream ve = TestHelper.class.getResourceAsStream(filename);
...@@ -71,9 +67,15 @@ public class TestHelper { ...@@ -71,9 +67,15 @@ public class TestHelper {
BufferedReader stream = new BufferedReader(new InputStreamReader(ve)); BufferedReader stream = new BufferedReader(new InputStreamReader(ve));
String tmp = ""; String tmp = "";
while ((tmp = stream.readLine()) != null) { while ((tmp = stream.readLine()) != null) {
if (tmp.startsWith("#")) if (tmp.startsWith("#") || tmp.isEmpty())
continue;
String[] split = tmp.split(">>>");
if (split.length != expectedArgs) {
System.err.format("Line %s has %d arguments, expected %d. SKIPPED%n",
tmp, split.length, expectedArgs);
continue; continue;
validExpression.add(new Object[] { tmp }); }
validExpression.add(split);
} }
System.out.println("Found: " + filename + " with " + validExpression.size() + " lines!"); System.out.println("Found: " + filename + " with " + validExpression.size() + " lines!");
...@@ -81,17 +83,22 @@ public class TestHelper { ...@@ -81,17 +83,22 @@ public class TestHelper {
return validExpression; return validExpression;
} }
public static Collection<Object[]> asParameters(String[] cases) { public static Collection<Object[]> asParameters(String[] cases) {
return Arrays.stream(cases).map(s -> new Object[] { s }).collect(Collectors.toList()); return Arrays.stream(cases).map(s -> new Object[]{s}).collect(Collectors.toList());
} }
public static ScriptLanguageParser getParser(String input) { public static ScriptLanguageParser getParser(String input) {
return new ScriptLanguageParser(new CommonTokenStream(new ScriptLanguageLexer(CharStreams.fromString(input)))); return Facade.getParser(CharStreams.fromString(input));
} }
public static ScriptLanguageParser getParser(File f) throws IOException { public static ScriptLanguageParser getParser(File f) throws IOException {
org.antlr.v4.runtime.CharStream stream = CharStreams.fromFileName(f.getAbsolutePath()); return Facade.getParser(CharStreams.fromFileName(f.getAbsolutePath()));
ScriptLanguageLexer lexer = new ScriptLanguageLexer(stream); }
return new ScriptLanguageParser(new CommonTokenStream(lexer));
public static Expression toExpr(String s) {
TransformAst v = new TransformAst();
Expression e = (Expression) getParser(s).expression().accept(v);
return e;
} }
} }
2+2 >>> 4
'abc' >>> 'abc'
`f(x)` >>> `f(x)`
2*(5+3) >>> 16
2*(8) >>> 16
(5+3) >>> 8
16163542361*1612316161341421+2+56+2+2+2+2+2+2 >>> 26060740573166968917435051
match `.*g.*` >>> true
true >>> true
false >>> false
true & false >>> false
false & true >>> false
false | true >>> true
true | false >>> true
not true >>> false
not false >>> true
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment