Commit 90c10929 authored by Alexander Weigl's avatar Alexander Weigl

matcher api and bugfixes

parent db98546f
Pipeline #10521 passed with stage
in 1 minute and 54 seconds
...@@ -75,7 +75,7 @@ literals : ...@@ -75,7 +75,7 @@ literals :
</pre>*/ </pre>*/
matchPattern matchPattern
: MATCH ( TERM_LITERAL | ID) : MATCH pattern=expression
(USING LBRACKET argList RBRACKET)? (USING LBRACKET argList RBRACKET)?
; ;
......
...@@ -2,9 +2,11 @@ package edu.kit.formal.interpreter; ...@@ -2,9 +2,11 @@ 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 lombok.Getter;
import lombok.Setter;
import java.util.ArrayList;
import java.util.List; import java.util.List;
import java.util.Stack;
/** /**
* Class handling evaluation of expressions (visitor for expressions) * Class handling evaluation of expressions (visitor for expressions)
...@@ -12,11 +14,13 @@ import java.util.Stack; ...@@ -12,11 +14,13 @@ import java.util.Stack;
* @author S.Grebing * @author S.Grebing
*/ */
public class Evaluator extends DefaultASTVisitor<Value> { public class Evaluator extends DefaultASTVisitor<Value> {
private State currentState; private GoalNode currentState;
private Stack<List<GoalNode>> matchedGoals = new Stack<>(); private List<VariableAssignment> matchedVariables = new ArrayList<>();
private EvaluatorABI abi; @Getter
@Setter
private MatcherApi matcher;
public Evaluator(State s) { public Evaluator(GoalNode s) {
this.currentState = s; this.currentState = s;
} }
...@@ -46,9 +50,16 @@ public class Evaluator extends DefaultASTVisitor<Value> { ...@@ -46,9 +50,16 @@ public class Evaluator extends DefaultASTVisitor<Value> {
*/ */
@Override @Override
public Value visit(MatchExpression match) { public Value visit(MatchExpression match) {
Value pattern = (Value) match.getPattern().accept(this);
List<VariableAssignment> 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<Value> { ...@@ -71,8 +82,7 @@ public class Evaluator extends DefaultASTVisitor<Value> {
public Value visit(Variable variable) { public Value visit(Variable variable) {
//get variable value //get variable value
String id = variable.getIdentifier(); String id = variable.getIdentifier();
GoalNode n = currentState.getSelectedGoalNode(); Value v = currentState.lookupVarValue(id);
Value v = n.lookupVarValue(id);
if (v != null) { if (v != null) {
return v; return v;
} else { } else {
......
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.ast.Type; import edu.kit.formal.proofscriptparser.ast.Type;
import lombok.Getter;
/** /**
* Objects of this class represent a GoalNode in a script state * Objects of this class represent a GoalNode in a script state
...@@ -9,8 +10,8 @@ import edu.kit.formal.proofscriptparser.ast.Type; ...@@ -9,8 +10,8 @@ import edu.kit.formal.proofscriptparser.ast.Type;
* @author S.Grebing * @author S.Grebing
*/ */
public class GoalNode { public class GoalNode {
//TODO this is only for testing, later Sequent object or similar //TODO this is only for testing, later Sequent object or similar
@Getter
private String sequent; private String sequent;
private VariableAssignment assignments; private VariableAssignment assignments;
...@@ -18,9 +19,7 @@ public class GoalNode { ...@@ -18,9 +19,7 @@ public class GoalNode {
private GoalNode parent; private GoalNode parent;
public GoalNode(GoalNode parent, String seq) { public GoalNode(GoalNode parent, String seq) {
if (parent == null) { this.assignments = new VariableAssignment(parent == null ? null : parent.assignments);
this.assignments = new VariableAssignment(null);
}
this.parent = parent; this.parent = parent;
this.sequent = seq; this.sequent = seq;
} }
...@@ -29,11 +28,6 @@ public class GoalNode { ...@@ -29,11 +28,6 @@ public class GoalNode {
return assignments; return assignments;
} }
public GoalNode setAssignments(VariableAssignment assignments) {
this.assignments = assignments;
return this;
}
public GoalNode getParent() { public GoalNode getParent() {
return parent; return parent;
} }
...@@ -47,7 +41,6 @@ public class GoalNode { ...@@ -47,7 +41,6 @@ public class GoalNode {
* @return value of variable if it exists * @return value of variable if it exists
*/ */
public Value lookupVarValue(String varname) { public Value lookupVarValue(String varname) {
Value v = assignments.getValue(varname); Value v = assignments.getValue(varname);
if (v != null) { if (v != null) {
return v; return v;
...@@ -85,8 +78,7 @@ public class GoalNode { ...@@ -85,8 +78,7 @@ public class GoalNode {
* @param t * @param t
*/ */
public void addVarDecl(String name, Type 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 { ...@@ -107,16 +99,13 @@ public class GoalNode {
/** /**
* Enter new variable scope and push onto stack * Enter new variable scope and push onto stack
*/ */
public void enterNewVarScope() { public VariableAssignment enterNewVarScope() {
this.assignments = this.assignments.push(); assignments = assignments.push();
return assignments;
} }
public void exitNewVarScope() { public VariableAssignment exitNewVarScope() {
this.assignments = this.assignments.pop(); this.assignments = this.assignments.pop();
return assignments;
} }
public VariableAssignment peek() {
return null;
}
} }
...@@ -60,7 +60,7 @@ public class Interpreter<T> extends DefaultASTVisitor<T> { ...@@ -60,7 +60,7 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
if (node != null) { if (node != null) {
Type t = node.lookUpType(var.getIdentifier()); Type t = node.lookUpType(var.getIdentifier());
if (t != null) { if (t != null) {
Evaluator eval = new Evaluator((State) state); Evaluator eval = new Evaluator(state.getSelectedGoalNode());
Value v = (Value) expr.accept(eval); Value v = (Value) expr.accept(eval);
node.getAssignments().setVar(var.getIdentifier(), v); node.getAssignments().setVar(var.getIdentifier(), v);
} else { } else {
......
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import java.util.List;
/** /**
* @author Alexander Weigl * @author Alexander Weigl
* @version 1 (16.05.17) * @version 1 (16.05.17)
*/ */
public interface EvaluatorABI { public interface MatcherApi {
List<VariableAssignment> matchLabel(GoalNode currentState, String label);
List<VariableAssignment> matchSeq(GoalNode currentState, String data);
} }
...@@ -22,6 +22,10 @@ public class VariableAssignment { ...@@ -22,6 +22,10 @@ public class VariableAssignment {
this.parent = parent; this.parent = parent;
} }
public VariableAssignment() {
this(null);
}
public VariableAssignment getParent() { public VariableAssignment getParent() {
return parent; return parent;
} }
......
...@@ -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 java.util.ArrayList; import java.util.ArrayList;
...@@ -37,46 +36,58 @@ import java.util.Set; ...@@ -37,46 +36,58 @@ import java.util.Set;
* @version 1 (29.04.17) * @version 1 (29.04.17)
*/ */
public class ASTChanger extends DefaultASTVisitor<ASTNode> { public class ASTChanger extends DefaultASTVisitor<ASTNode> {
@Override public ProofScript visit(ProofScript proofScript) { @Override
public ProofScript visit(ProofScript proofScript) {
proofScript.setBody((Statements) proofScript.getBody().accept(this)); proofScript.setBody((Statements) proofScript.getBody().accept(this));
return proofScript; return proofScript;
} }
@Override public AssignmentStatement visit(AssignmentStatement assign) { @Override
public AssignmentStatement visit(AssignmentStatement assign) {
assign.setRhs((Expression) assign.getRhs().accept(this)); assign.setRhs((Expression) assign.getRhs().accept(this));
assign.setLhs((Variable) assign.getLhs().accept(this)); assign.setLhs((Variable) assign.getLhs().accept(this));
return assign; return assign;
} }
@Override public Expression visit(BinaryExpression e) { @Override
public Expression visit(BinaryExpression e) {
e.setLeft((Expression) e.getLeft().accept(this)); e.setLeft((Expression) e.getLeft().accept(this));
e.setRight((Expression) e.getRight().accept(this)); e.setRight((Expression) e.getRight().accept(this));
return e; return e;
} }
@Override public MatchExpression visit(MatchExpression match) { @Override
if (match.getTerm() != null) public MatchExpression visit(MatchExpression match) {
match.setTerm((TermLiteral) match.getTerm().accept(this)); if (match.getSignature() != null)
match.setSignature((Signature)
match.getSignature().accept(this));
match.setPattern((Expression) match.getPattern().accept(this));
return match; return match;
} }
@Override public TermLiteral visit(TermLiteral term) { @Override
public TermLiteral visit(TermLiteral term) {
return term; return term;
} }
@Override public StringLiteral visit(StringLiteral string) { @Override
public StringLiteral visit(StringLiteral string) {
return string; return string;
} }
@Override public Variable visit(Variable variable) { @Override
public Variable visit(Variable variable) {
return variable; return variable;
} }
@Override public BooleanLiteral visit(BooleanLiteral bool) { @Override
public BooleanLiteral visit(BooleanLiteral bool) {
return bool; return bool;
} }
@Override public Statements visit(Statements statements) { @Override
public Statements visit(Statements statements) {
ArrayList copy = new ArrayList<>(statements.size()); ArrayList copy = new ArrayList<>(statements.size());
for (Statement statement : statements) { for (Statement statement : statements) {
copy.add(statement.accept(this)); copy.add(statement.accept(this));
...@@ -86,44 +97,52 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> { ...@@ -86,44 +97,52 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
return statements; return statements;
} }
@Override public IntegerLiteral visit(IntegerLiteral integer) { @Override
public IntegerLiteral visit(IntegerLiteral integer) {
return integer; return integer;
} }
@Override public CasesStatement visit(CasesStatement casesStatement) { @Override
public CasesStatement visit(CasesStatement casesStatement) {
for (CaseStatement c : casesStatement.getCases()) { for (CaseStatement c : casesStatement.getCases()) {
c.accept(this); c.accept(this);
} }
return casesStatement; return casesStatement;
} }
@Override public CaseStatement visit(CaseStatement caseStatement) { @Override
public CaseStatement visit(CaseStatement caseStatement) {
caseStatement.getGuard().accept(this); caseStatement.getGuard().accept(this);
caseStatement.getBody().accept(this); caseStatement.getBody().accept(this);
return caseStatement; return caseStatement;
} }
@Override public CallStatement visit(CallStatement call) { @Override
public CallStatement visit(CallStatement call) {
call.setParameters((Parameters) call.getParameters().accept(this)); call.setParameters((Parameters) call.getParameters().accept(this));
return call; return call;
} }
@Override public ASTNode visit(TheOnlyStatement theOnly) { @Override
public ASTNode visit(TheOnlyStatement theOnly) {
theOnly.setBody((Statements) theOnly.getBody().accept(this)); theOnly.setBody((Statements) theOnly.getBody().accept(this));
return theOnly; return theOnly;
} }
@Override public ASTNode visit(ForeachStatement foreach) { @Override
public ASTNode visit(ForeachStatement foreach) {
foreach.setBody((Statements) foreach.getBody().accept(this)); foreach.setBody((Statements) foreach.getBody().accept(this));
return foreach; return foreach;
} }
@Override public ASTNode visit(RepeatStatement repeat) { @Override
public ASTNode visit(RepeatStatement repeat) {
repeat.setBody((Statements) repeat.getBody().accept(this)); repeat.setBody((Statements) repeat.getBody().accept(this));
return repeat; return repeat;
} }
@Override public ASTNode visit(Signature signature) { @Override
public ASTNode visit(Signature signature) {
Set<Map.Entry<Variable, Type>> entries = signature.entrySet(); Set<Map.Entry<Variable, Type>> entries = signature.entrySet();
signature.clear(); signature.clear();
for (Map.Entry<Variable, Type> e : entries) { for (Map.Entry<Variable, Type> e : entries) {
...@@ -132,7 +151,8 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> { ...@@ -132,7 +151,8 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
return signature; return signature;
} }
@Override public ASTNode visit(Parameters parameters) { @Override
public ASTNode visit(Parameters parameters) {
Set<Map.Entry<Variable, Expression>> entries = parameters.entrySet(); Set<Map.Entry<Variable, Expression>> entries = parameters.entrySet();
parameters.clear(); parameters.clear();
for (Map.Entry<Variable, Expression> e : entries) { for (Map.Entry<Variable, Expression> e : entries) {
...@@ -141,7 +161,8 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> { ...@@ -141,7 +161,8 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
return parameters; return parameters;
} }
@Override public ASTNode visit(UnaryExpression e) { @Override
public ASTNode visit(UnaryExpression e) {
e.setExpression((Expression) e.getExpression().accept(this)); e.setExpression((Expression) e.getExpression().accept(this));
return e; return e;
} }
......
...@@ -50,9 +50,8 @@ public class ASTTraversal<T> implements Visitor<T> { ...@@ -50,9 +50,8 @@ public class ASTTraversal<T> implements Visitor<T> {
} }
@Override public T visit(MatchExpression match) { @Override public T visit(MatchExpression match) {
if (match.getTerm() != null) match.getPattern().accept(this);
match.getTerm().accept(this); match.getSignature().accept(this);
return null; return null;
} }
......
...@@ -119,10 +119,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> { ...@@ -119,10 +119,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
public Void visit(MatchExpression match) { public Void visit(MatchExpression match) {
s.append("match "); s.append("match ");
String prefix = getWhitespacePrefix(); String prefix = getWhitespacePrefix();
if (match.getTerm() != null) { match.getPattern().accept(this);
match.getTerm().accept(this);
}
if (!match.getSignature().isEmpty()) { if (!match.getSignature().isEmpty()) {
if (getCurrentLineLength() > maxWidth) { if (getCurrentLineLength() > maxWidth) {
......
...@@ -239,11 +239,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -239,11 +239,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
match.setRuleContext(ctx); match.setRuleContext(ctx);
if (ctx.argList() != null) if (ctx.argList() != null)
match.setSignature((Signature) ctx.argList().accept(this)); match.setSignature((Signature) ctx.argList().accept(this));
if (ctx.TERM_LITERAL() != null) { match.setPattern((Expression) ctx.pattern.accept(this));
match.setTerm(new TermLiteral(ctx.TERM_LITERAL().getText()));
} else {
match.setVariable(new Variable(ctx.ID().getSymbol()));
}
return match; return match;
} }
......
...@@ -23,9 +23,8 @@ package edu.kit.formal.proofscriptparser.ast; ...@@ -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.NotWelldefinedException;
import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.Visitor;
import lombok.Data; import lombok.Data;
...@@ -38,27 +37,25 @@ import lombok.Data; ...@@ -38,27 +37,25 @@ import lombok.Data;
@Data @Data
public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> { public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
private Signature signature; private Signature signature;
private TermLiteral term; private Expression pattern;
private Variable variable;
/** /**
* {@inheritDoc} * {@inheritDoc}
*/ */
@Override public <T> T accept(Visitor<T> visitor) { @Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this); return visitor.visit(this);
} }
/** /**
* {@inheritDoc} * {@inheritDoc}
*/ */
@Override public MatchExpression copy() { @Override
public MatchExpression copy() {
MatchExpression me = new MatchExpression(); MatchExpression me = new MatchExpression();
if(signature!=null) if (signature != null)
me.signature=signature.copy(); me.signature = signature.copy();
if(term!=null) me.pattern = pattern.copy();
me.term = term.copy();
if(variable!=null)
me.variable = variable.copy();
return me; return me;
} }
...@@ -67,15 +64,27 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter ...@@ -67,15 +64,27 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter
*/ */
@Override @Override
public Type getType(Signature signature) throws NotWelldefinedException { public Type getType(Signature signature) throws NotWelldefinedException {
if(term==null && variable==null) Type patternType = pattern.getType(signature);
throw new NotWelldefinedException("Missing parameter", this);