diff --git a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 index 53eb54c31461d34ac5b0a29ec6e20cc782815172..baa2aacc808b019d8a8b37085beacad06c6fa398 100644 --- a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 +++ b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 @@ -75,7 +75,7 @@ literals : */ matchPattern - : MATCH ( TERM_LITERAL | ID) + : MATCH pattern=expression (USING LBRACKET argList RBRACKET)? ; diff --git a/src/main/java/edu/kit/formal/interpreter/Evaluator.java b/src/main/java/edu/kit/formal/interpreter/Evaluator.java index 473b4a0d180c76e4f7de5b3d9fa60ad6875d1460..c7c8c099130d9dccf8ecfb159394b5fe40787d78 100644 --- a/src/main/java/edu/kit/formal/interpreter/Evaluator.java +++ b/src/main/java/edu/kit/formal/interpreter/Evaluator.java @@ -2,9 +2,11 @@ package edu.kit.formal.interpreter; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.*; +import lombok.Getter; +import lombok.Setter; +import java.util.ArrayList; import java.util.List; -import java.util.Stack; /** * Class handling evaluation of expressions (visitor for expressions) @@ -12,11 +14,13 @@ import java.util.Stack; * @author S.Grebing */ public class Evaluator extends DefaultASTVisitor { - private State currentState; - private Stack> matchedGoals = new Stack<>(); - private EvaluatorABI abi; + private GoalNode currentState; + private List matchedVariables = new ArrayList<>(); + @Getter + @Setter + private MatcherApi matcher; - public Evaluator(State s) { + public Evaluator(GoalNode s) { this.currentState = s; } @@ -46,9 +50,16 @@ public class Evaluator extends DefaultASTVisitor { */ @Override public Value visit(MatchExpression match) { + Value pattern = (Value) match.getPattern().accept(this); + List va = null; + if (pattern.getType() == Type.STRING) { + va = matcher.matchLabel(currentState, (String) pattern.getData()); + } else if (pattern.getType() == Type.TERM) { + va = matcher.matchSeq(currentState, (String) pattern.getData()); + } - return Value.TRUE; + return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE; } /** @@ -71,8 +82,7 @@ public class Evaluator extends DefaultASTVisitor { public Value visit(Variable variable) { //get variable value String id = variable.getIdentifier(); - GoalNode n = currentState.getSelectedGoalNode(); - Value v = n.lookupVarValue(id); + Value v = currentState.lookupVarValue(id); if (v != null) { return v; } else { diff --git a/src/main/java/edu/kit/formal/interpreter/EvaluatorABI.java b/src/main/java/edu/kit/formal/interpreter/EvaluatorABI.java deleted file mode 100644 index b7304a1af5742f509292693f0189570ad8825984..0000000000000000000000000000000000000000 --- a/src/main/java/edu/kit/formal/interpreter/EvaluatorABI.java +++ /dev/null @@ -1,8 +0,0 @@ -package edu.kit.formal.interpreter; - -/** - * @author Alexander Weigl - * @version 1 (16.05.17) - */ -public interface EvaluatorABI { -} diff --git a/src/main/java/edu/kit/formal/interpreter/GoalNode.java b/src/main/java/edu/kit/formal/interpreter/GoalNode.java index e1c3ec684f45c267d299e71c2349f2cf7fd60eeb..764d7d947e9c7826ed2b5e242391b101ca9edd85 100644 --- a/src/main/java/edu/kit/formal/interpreter/GoalNode.java +++ b/src/main/java/edu/kit/formal/interpreter/GoalNode.java @@ -1,6 +1,7 @@ package edu.kit.formal.interpreter; import edu.kit.formal.proofscriptparser.ast.Type; +import lombok.Getter; /** * Objects of this class represent a GoalNode in a script state @@ -9,8 +10,8 @@ import edu.kit.formal.proofscriptparser.ast.Type; * @author S.Grebing */ public class GoalNode { - //TODO this is only for testing, later Sequent object or similar + @Getter private String sequent; private VariableAssignment assignments; @@ -18,9 +19,7 @@ public class GoalNode { private GoalNode parent; public GoalNode(GoalNode parent, String seq) { - if (parent == null) { - this.assignments = new VariableAssignment(null); - } + this.assignments = new VariableAssignment(parent == null ? null : parent.assignments); this.parent = parent; this.sequent = seq; } @@ -29,11 +28,6 @@ public class GoalNode { return assignments; } - public GoalNode setAssignments(VariableAssignment assignments) { - this.assignments = assignments; - return this; - } - public GoalNode getParent() { return parent; } @@ -47,7 +41,6 @@ public class GoalNode { * @return value of variable if it exists */ public Value lookupVarValue(String varname) { - Value v = assignments.getValue(varname); if (v != null) { return v; @@ -85,8 +78,7 @@ public class GoalNode { * @param t */ public void addVarDecl(String name, Type t) { - this.assignments = getAssignments().addVariable(name, t); - + getAssignments().addVariable(name, t); } /** @@ -107,16 +99,13 @@ public class GoalNode { /** * Enter new variable scope and push onto stack */ - public void enterNewVarScope() { - this.assignments = this.assignments.push(); + public VariableAssignment enterNewVarScope() { + assignments = assignments.push(); + return assignments; } - public void exitNewVarScope() { + public VariableAssignment exitNewVarScope() { this.assignments = this.assignments.pop(); + return assignments; } - - public VariableAssignment peek() { - return null; - } - } diff --git a/src/main/java/edu/kit/formal/interpreter/Interpreter.java b/src/main/java/edu/kit/formal/interpreter/Interpreter.java index 4aa836c0fea55e5801d568aedf40b62f9e99e908..5c44719dc5bb67603fcd3a854f6887d112bb1fbf 100644 --- a/src/main/java/edu/kit/formal/interpreter/Interpreter.java +++ b/src/main/java/edu/kit/formal/interpreter/Interpreter.java @@ -60,7 +60,7 @@ public class Interpreter extends DefaultASTVisitor { if (node != null) { Type t = node.lookUpType(var.getIdentifier()); if (t != null) { - Evaluator eval = new Evaluator((State) state); + Evaluator eval = new Evaluator(state.getSelectedGoalNode()); Value v = (Value) expr.accept(eval); node.getAssignments().setVar(var.getIdentifier(), v); } else { diff --git a/src/main/java/edu/kit/formal/interpreter/MatcherApi.java b/src/main/java/edu/kit/formal/interpreter/MatcherApi.java new file mode 100644 index 0000000000000000000000000000000000000000..dfbd8264efd1e2cabf616fa9a3c575b6b46070c8 --- /dev/null +++ b/src/main/java/edu/kit/formal/interpreter/MatcherApi.java @@ -0,0 +1,12 @@ +package edu.kit.formal.interpreter; + +import java.util.List; + +/** + * @author Alexander Weigl + * @version 1 (16.05.17) + */ +public interface MatcherApi { + List matchLabel(GoalNode currentState, String label); + List matchSeq(GoalNode currentState, String data); +} diff --git a/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java b/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java index 573fc97fbac89e65531b335853ffc3745bafcc69..82821f532329d5922a47bea83891ffc7741da16e 100644 --- a/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java +++ b/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java @@ -22,6 +22,10 @@ public class VariableAssignment { this.parent = parent; } + public VariableAssignment() { + this(null); + } + public VariableAssignment getParent() { return parent; } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java b/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java index 16ad9731d8ed54d79284b7f6f566144fef7b1504..5783b53c1c2ebeed880f5cfe95a5fb897818629d 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java @@ -23,7 +23,6 @@ package edu.kit.formal.proofscriptparser; */ - import edu.kit.formal.proofscriptparser.ast.*; import java.util.ArrayList; @@ -37,46 +36,58 @@ import java.util.Set; * @version 1 (29.04.17) */ public class ASTChanger extends DefaultASTVisitor { - @Override public ProofScript visit(ProofScript proofScript) { + @Override + public ProofScript visit(ProofScript proofScript) { proofScript.setBody((Statements) proofScript.getBody().accept(this)); return proofScript; } - @Override public AssignmentStatement visit(AssignmentStatement assign) { + @Override + public AssignmentStatement visit(AssignmentStatement assign) { assign.setRhs((Expression) assign.getRhs().accept(this)); assign.setLhs((Variable) assign.getLhs().accept(this)); return assign; } - @Override public Expression visit(BinaryExpression e) { + @Override + public Expression visit(BinaryExpression e) { e.setLeft((Expression) e.getLeft().accept(this)); e.setRight((Expression) e.getRight().accept(this)); return e; } - @Override public MatchExpression visit(MatchExpression match) { - if (match.getTerm() != null) - match.setTerm((TermLiteral) match.getTerm().accept(this)); + @Override + public MatchExpression visit(MatchExpression match) { + if (match.getSignature() != null) + match.setSignature((Signature) + match.getSignature().accept(this)); + + match.setPattern((Expression) match.getPattern().accept(this)); return match; } - @Override public TermLiteral visit(TermLiteral term) { + @Override + public TermLiteral visit(TermLiteral term) { return term; } - @Override public StringLiteral visit(StringLiteral string) { + @Override + public StringLiteral visit(StringLiteral string) { return string; } - @Override public Variable visit(Variable variable) { + @Override + public Variable visit(Variable variable) { return variable; } - @Override public BooleanLiteral visit(BooleanLiteral bool) { + @Override + public BooleanLiteral visit(BooleanLiteral bool) { return bool; } - @Override public Statements visit(Statements statements) { + @Override + public Statements visit(Statements statements) { ArrayList copy = new ArrayList<>(statements.size()); for (Statement statement : statements) { copy.add(statement.accept(this)); @@ -86,44 +97,52 @@ public class ASTChanger extends DefaultASTVisitor { return statements; } - @Override public IntegerLiteral visit(IntegerLiteral integer) { + @Override + public IntegerLiteral visit(IntegerLiteral integer) { return integer; } - @Override public CasesStatement visit(CasesStatement casesStatement) { + @Override + public CasesStatement visit(CasesStatement casesStatement) { for (CaseStatement c : casesStatement.getCases()) { c.accept(this); } return casesStatement; } - @Override public CaseStatement visit(CaseStatement caseStatement) { + @Override + public CaseStatement visit(CaseStatement caseStatement) { caseStatement.getGuard().accept(this); caseStatement.getBody().accept(this); return caseStatement; } - @Override public CallStatement visit(CallStatement call) { + @Override + public CallStatement visit(CallStatement call) { call.setParameters((Parameters) call.getParameters().accept(this)); return call; } - @Override public ASTNode visit(TheOnlyStatement theOnly) { + @Override + public ASTNode visit(TheOnlyStatement theOnly) { theOnly.setBody((Statements) theOnly.getBody().accept(this)); return theOnly; } - @Override public ASTNode visit(ForeachStatement foreach) { + @Override + public ASTNode visit(ForeachStatement foreach) { foreach.setBody((Statements) foreach.getBody().accept(this)); return foreach; } - @Override public ASTNode visit(RepeatStatement repeat) { + @Override + public ASTNode visit(RepeatStatement repeat) { repeat.setBody((Statements) repeat.getBody().accept(this)); return repeat; } - @Override public ASTNode visit(Signature signature) { + @Override + public ASTNode visit(Signature signature) { Set> entries = signature.entrySet(); signature.clear(); for (Map.Entry e : entries) { @@ -132,7 +151,8 @@ public class ASTChanger extends DefaultASTVisitor { return signature; } - @Override public ASTNode visit(Parameters parameters) { + @Override + public ASTNode visit(Parameters parameters) { Set> entries = parameters.entrySet(); parameters.clear(); for (Map.Entry e : entries) { @@ -141,7 +161,8 @@ public class ASTChanger extends DefaultASTVisitor { return parameters; } - @Override public ASTNode visit(UnaryExpression e) { + @Override + public ASTNode visit(UnaryExpression e) { e.setExpression((Expression) e.getExpression().accept(this)); return e; } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java b/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java index 3da7a7c8754884bd48ac8b64b34becdb3c018487..c8392a08b3010801278f907cd62059b6b1667a90 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java @@ -50,9 +50,8 @@ public class ASTTraversal implements Visitor { } @Override public T visit(MatchExpression match) { - if (match.getTerm() != null) - match.getTerm().accept(this); - + match.getPattern().accept(this); + match.getSignature().accept(this); return null; } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java b/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java index 7102e4df0f294ec6cb2a09269ea15dce11f2b197..6515f5a989f6262abc1745a69f3b6fd1f1fd5d96 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java @@ -119,10 +119,7 @@ public class PrettyPrinter extends DefaultASTVisitor { public Void visit(MatchExpression match) { s.append("match "); String prefix = getWhitespacePrefix(); - if (match.getTerm() != null) { - match.getTerm().accept(this); - } - + match.getPattern().accept(this); if (!match.getSignature().isEmpty()) { if (getCurrentLineLength() > maxWidth) { diff --git a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java index eb5b9db474932eb91cb19c7744b91c4edf8048bd..ae988dd6c1c19a6d5e922800d7ad690e8aaed2d3 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java @@ -239,11 +239,7 @@ public class TransformAst implements ScriptLanguageVisitor { match.setRuleContext(ctx); if (ctx.argList() != null) match.setSignature((Signature) ctx.argList().accept(this)); - if (ctx.TERM_LITERAL() != null) { - match.setTerm(new TermLiteral(ctx.TERM_LITERAL().getText())); - } else { - match.setVariable(new Variable(ctx.ID().getSymbol())); - } + match.setPattern((Expression) ctx.pattern.accept(this)); return match; } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java index 7f587279ddb69b47087a494d08d8a164623c440e..7b269bb6cc44c32f15fd150680780e135001b7ef 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java @@ -23,9 +23,8 @@ package edu.kit.formal.proofscriptparser.ast; */ - -import edu.kit.formal.proofscriptparser.ScriptLanguageParser; import edu.kit.formal.proofscriptparser.NotWelldefinedException; +import edu.kit.formal.proofscriptparser.ScriptLanguageParser; import edu.kit.formal.proofscriptparser.Visitor; import lombok.Data; @@ -38,27 +37,25 @@ import lombok.Data; @Data public class MatchExpression extends Expression { private Signature signature; - private TermLiteral term; - private Variable variable; + private Expression pattern; /** * {@inheritDoc} */ - @Override public T accept(Visitor visitor) { + @Override + public T accept(Visitor visitor) { return visitor.visit(this); } /** * {@inheritDoc} */ - @Override public MatchExpression copy() { + @Override + public MatchExpression copy() { MatchExpression me = new MatchExpression(); - if(signature!=null) - me.signature=signature.copy(); - if(term!=null) - me.term = term.copy(); - if(variable!=null) - me.variable = variable.copy(); + if (signature != null) + me.signature = signature.copy(); + me.pattern = pattern.copy(); return me; } @@ -67,15 +64,27 @@ public class MatchExpression extends Expression goals = Arrays.asList(g1,g2,selected); - State state = new State(goals, selected); - eval = new Evaluator(state); + parent.addVarDecl("a", Type.INT); + parent.addVarDecl("b", Type.INT); + VariableAssignment va = parent.getAssignments(); + va.setVar("a", Value.from(1)); + va.setVar("b", Value.from(1)); + GoalNode selected = new GoalNode(parent, "selg"); + eval = new Evaluator(selected); + eval.setMatcher(new PseudoMatcher()); } @Test @@ -48,4 +54,20 @@ public class EvaluatorTest { System.out.println(expr); Assert.assertEquals(truthValue, result); } + + class PseudoMatcher implements MatcherApi { + @Override + public List matchLabel(GoalNode currentState, String label) { + Pattern p = Pattern.compile(label,Pattern.CASE_INSENSITIVE); + Matcher m = p.matcher(currentState.getSequent()); + return m.matches() + ? Collections.singletonList(new VariableAssignment()) + : Collections.emptyList(); + } + + @Override + public List matchSeq(GoalNode currentState, String data) { + return Collections.emptyList(); + } + } } \ No newline at end of file diff --git a/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt b/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt index 5eef3f0b3c63adffe6604f771c5c217dca46b94e..297bd6e96561c5b83a7c53b6cbc47d973eaac886 100644 --- a/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt +++ b/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt @@ -5,7 +5,7 @@ 2*(8) >>> 16 (5+3) >>> 8 16163542361*1612316161341421+2+56+2+2+2+2+2+2 >>> 26060740573166968917435051 -match `.*g.*` >>> true +match '.*g.*' >>> true true >>> true false >>> false true & false >>> false @@ -13,4 +13,6 @@ false & true >>> false false | true >>> true true | false >>> true not true >>> false -not false >>> true \ No newline at end of file +not false >>> true +a + b >>> 2 +(a+a+a+a+a+a+a)*(b+b+b+b+a+a+a) >>> 49 \ No newline at end of file