diff --git a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 index ec883067804edf346a666c5e897d69d768c8354e..05201921fd8062b0aca403ba59419b329f15c8f3 100644 --- a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 +++ b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 @@ -49,19 +49,19 @@ assignment expression : - MINUS expression #exprNegate - | NOT expression #exprNot - | expression '[' substExpressionList ']' #exprSubst - | expression MUL expression #exprMultiplication - | expression DIV expression #exprDivision - | expression op=(PLUS|MINUS) expression #exprLineOperators - | expression op=(LE|GE|LEQ|GEQ) expression #exprComparison - | expression op=(NEQ|EQ) expression #exprEquality - | expression AND expression #exprAnd - | expression OR expression #exprOr - | expression IMP expression #exprIMP + expression MUL expression #exprMultiplication + | expression DIV expression #exprDivision + | expression op=(PLUS|MINUS) expression #exprLineOperators + | expression op=(LE|GE|LEQ|GEQ) expression #exprComparison + | expression op=(NEQ|EQ) expression #exprEquality + | expression AND expression #exprAnd + | expression OR expression #exprOr + | expression IMP expression #exprIMP //| expression EQUIV expression already covered by EQ/NEQ - | '(' expression ')' #exprParen + | expression LBRACKET substExpressionList RBRACKET #exprSubst + | MINUS expression #exprNegate + | NOT expression #exprNot + | '(' expression ')' #exprParen | literals #exprLiterals | matchPattern #exprMatch ; @@ -69,7 +69,9 @@ expression substExpressionList : - scriptVar '/' expression (',' substExpressionList)* + (scriptVar '/' expression + (',' scriptVar '/' expression)* + )? ; literals : @@ -205,4 +207,4 @@ EXE_MARKER: '\u2316' -> channel(HIDDEN); DIGITS : DIGIT+ ; fragment DIGIT : [0-9] ; -ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]' | '-')* ; +ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\')*; \ No newline at end of file diff --git a/src/main/java/edu/kit/formal/interpreter/Evaluator.java b/src/main/java/edu/kit/formal/interpreter/Evaluator.java index 4dabdaad40bece610edd89f67a6c77b0d00fae97..520633559e52e476b618918f71ce84164157c689 100644 --- a/src/main/java/edu/kit/formal/interpreter/Evaluator.java +++ b/src/main/java/edu/kit/formal/interpreter/Evaluator.java @@ -6,11 +6,16 @@ import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.TermType; +import edu.kit.formal.proofscriptparser.types.TypeFacade; import lombok.Getter; import lombok.Setter; import java.util.ArrayList; import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; /** * Class handling evaluation of expressions (visitor for expressions) @@ -68,9 +73,9 @@ public class Evaluator extends DefaultASTVisitor implements ScopeObser Value pattern = (Value) match.getPattern().accept(this); if (match.isDerivable()) { } else { - if (pattern.getType() == Type.STRING) { + if (pattern.getType() == SimpleType.STRING) { va = matcher.matchLabel(goal, (String) pattern.getData()); - } else if (pattern.getType() == Type.TERM) { + } else if (TypeFacade.isTerm(pattern.getType())) { va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature()); } } @@ -127,5 +132,29 @@ public class Evaluator extends DefaultASTVisitor implements ScopeObser return op.evaluate(exValue); } - + public Value visit(SubstituteExpression expr) { + Value term = (Value) expr.getSub().accept(this); + if (term.getType() instanceof TermType) { + Pattern pattern = Pattern.compile("\\?[a-zA-Z_]+"); + String termstr = term.getData().toString(); + Matcher m = pattern.matcher(termstr); + StringBuffer newTerm = new StringBuffer(); + while (m.find()) { + String name = m.group().substring(1); // remove trailing '?' + Expression t = expr.getSubstitution().get(m.group()); + + //either evalute the substitent or find ?X in the + String newVal = ""; + if (t != null) + newVal = ((Value) t.accept(this)).getData().toString(); + else + newVal = state.getValue(new Variable(name)).getData().toString(); + m.appendReplacement(newTerm, newVal); + } + m.appendTail(newTerm); + return new Value<>(TypeFacade.ANY_TERM, newTerm.toString()); + } else { + throw new IllegalStateException("Try to apply substitute on a non-term value."); + } + } } diff --git a/src/main/java/edu/kit/formal/interpreter/Interpreter.java b/src/main/java/edu/kit/formal/interpreter/Interpreter.java index d73bc9ae47111034f983af07d1bac4dd3f37962e..6445d8b3bcbe0c7b85be9fa09d9de4afb94dfca0 100644 --- a/src/main/java/edu/kit/formal/interpreter/Interpreter.java +++ b/src/main/java/edu/kit/formal/interpreter/Interpreter.java @@ -14,6 +14,8 @@ import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Getter; import lombok.Setter; import org.key_project.util.collection.ImmutableList; @@ -33,15 +35,15 @@ public class Interpreter extends DefaultASTVisitor implements ScopeObservable { private static final int MAX_ITERATIONS = 5; @Getter - private static final BiMap typeConversionBiMap = - new ImmutableBiMap.Builder() - .put(Type.ANY, VariableAssignments.VarType.ANY) - .put(Type.BOOL, VariableAssignments.VarType.BOOL) - .put(Type.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms - .put(Type.INT, VariableAssignments.VarType.INT) - .put(Type.STRING, VariableAssignments.VarType.OBJECT) - .put(Type.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY) - .put(Type.SEQ, VariableAssignments.VarType.SEQ) + private static final BiMap typeConversionBiMap = + new ImmutableBiMap.Builder() + .put(SimpleType.ANY, VariableAssignments.VarType.ANY) + .put(SimpleType.BOOL, VariableAssignments.VarType.BOOL) + //.put(SimpleType.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms + .put(SimpleType.INT, VariableAssignments.VarType.INT) + .put(SimpleType.STRING, VariableAssignments.VarType.OBJECT) + .put(SimpleType.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY) + .put(SimpleType.SEQ, VariableAssignments.VarType.SEQ) .build(); private static Logger logger = Logger.getLogger("interpreter"); //TODO later also include information about source line for each state (for debugging purposes and rewind purposes) @@ -114,7 +116,7 @@ public class Interpreter extends DefaultASTVisitor if (expr != null) { Type type = node.getVariableType(var); if (type == null) { - throw new RuntimeException("Type of Variable " + var + " is not declared yet"); + throw new RuntimeException("SimpleType of Variable " + var + " is not declared yet"); } else { Value v = evaluate(expr); node.setVariableValue(var, v); diff --git a/src/main/java/edu/kit/formal/interpreter/KeYMatcher.java b/src/main/java/edu/kit/formal/interpreter/KeYMatcher.java index ea27ee06cf6cfeaafd580612d354ffa4ffe9a41e..f87636ecf4c91b1746a3ebe320216ce6fc491bf7 100644 --- a/src/main/java/edu/kit/formal/interpreter/KeYMatcher.java +++ b/src/main/java/edu/kit/formal/interpreter/KeYMatcher.java @@ -18,8 +18,9 @@ import edu.kit.formal.interpreter.data.Value; import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.proofscriptparser.ast.Signature; import edu.kit.formal.proofscriptparser.ast.TermLiteral; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import edu.kit.formal.proofscriptparser.ast.Variable; +import edu.kit.formal.proofscriptparser.types.Type; import org.key_project.util.collection.ImmutableList; import java.util.ArrayList; @@ -114,7 +115,7 @@ public class KeYMatcher implements MatcherApi { if (branchLabelMatcher.matches()) { VariableAssignment va = new VariableAssignment(null); - va.declare("$$branchLabel_", Type.STRING); + va.declare("$$branchLabel_", SimpleType.STRING); va.assign("$$branchLabel_", Value.from(branchLabelMatcher.group())); assignments.add(va); resultsFromLabelMatch.add(branchLabelMatcher.toMatchResult()); @@ -124,7 +125,7 @@ public class KeYMatcher implements MatcherApi { Matcher linesMatcher = regexpForLabel.matcher(controlFlowLines); if (linesMatcher.matches()) { VariableAssignment va = new VariableAssignment(null); - va.declare("$$CtrlLinesLabel_", Type.STRING); + va.declare("$$CtrlLinesLabel_", SimpleType.STRING); va.assign("$$CtrlLinesLabel_", Value.from(linesMatcher.group())); assignments.add(va); resultsFromLabelMatch.add(linesMatcher.toMatchResult()); @@ -134,7 +135,7 @@ public class KeYMatcher implements MatcherApi { Matcher flowStmtsMatcher = regexpForLabel.matcher(controlFlowLines); if (flowStmtsMatcher.matches()) { VariableAssignment va = new VariableAssignment(null); - va.declare("$$FlowStmtsLabel_", Type.STRING); + va.declare("$$FlowStmtsLabel_", SimpleType.STRING); va.assign("$$FlowStmtsLabel_", Value.from(flowStmtsMatcher.group())); assignments.add(va); resultsFromLabelMatch.add(flowStmtsMatcher.toMatchResult()); @@ -144,7 +145,7 @@ public class KeYMatcher implements MatcherApi { Matcher ruleMatcher = regexpForLabel.matcher(ruleLabel); if (ruleMatcher.matches()) { VariableAssignment va = new VariableAssignment(null); - va.declare("$$RuleLabel_", Type.STRING); + va.declare("$$RuleLabel_", SimpleType.STRING); va.assign("$$RuleLabel_", Value.from(ruleMatcher.group())); assignments.add(va); resultsFromLabelMatch.add(ruleMatcher.toMatchResult()); diff --git a/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java b/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java index b1d602d33d74e4d7e905a342f0b24176f8077ded..3c407ea15e83c185bdd2755042c53261b8060512 100644 --- a/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java +++ b/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java @@ -6,6 +6,8 @@ import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.TypeFacade; import lombok.Getter; import org.apache.commons.lang.NotImplementedException; @@ -156,10 +158,10 @@ public class MatchEvaluator extends DefaultASTVisitor> // Value pattern = (Value) match.getPattern().accept(this); List va = null; - if (pattern.getType() == Type.STRING) { + if (pattern.getType() == SimpleType.STRING) { va = getMatcher().matchLabel(goal, (String) pattern.getData()); //TODO extract the results form the matcher in order to retrieve the selection results - } else if (pattern.getType() == Type.TERM) { + } else if (TypeFacade.isTerm(pattern.getType())) { va = getMatcher().matchSeq(goal, (String) pattern.getData(), sig); } return va != null ? va : Collections.emptyList(); @@ -203,7 +205,7 @@ public class MatchEvaluator extends DefaultASTVisitor> */ public List transformTruthValue(Value v) { - if (v.getType().equals(Type.BOOL)) { + if (v.getType().equals(SimpleType.BOOL)) { List transformedValue = new ArrayList<>(); if (v.getData().equals(Value.TRUE)) { transformedValue.add(new VariableAssignment(null)); diff --git a/src/main/java/edu/kit/formal/interpreter/data/GoalNode.java b/src/main/java/edu/kit/formal/interpreter/data/GoalNode.java index 866e78d66348f7a66927bd8a30280fcbea17d5bd..bb51ab4eff9ac85f0fc6730c68db631416e5c8f2 100644 --- a/src/main/java/edu/kit/formal/interpreter/data/GoalNode.java +++ b/src/main/java/edu/kit/formal/interpreter/data/GoalNode.java @@ -1,7 +1,8 @@ package edu.kit.formal.interpreter.data; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import edu.kit.formal.proofscriptparser.ast.Variable; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Getter; import lombok.ToString; diff --git a/src/main/java/edu/kit/formal/interpreter/data/Value.java b/src/main/java/edu/kit/formal/interpreter/data/Value.java index cbd61ca3ffc4cd3fcc458979d4df8874721cf1fd..fa4acd4f02412133ecea4e6e7a66ab949f2ea65d 100644 --- a/src/main/java/edu/kit/formal/interpreter/data/Value.java +++ b/src/main/java/edu/kit/formal/interpreter/data/Value.java @@ -1,6 +1,9 @@ package edu.kit.formal.interpreter.data; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; +import edu.kit.formal.proofscriptparser.types.TypeFacade; import lombok.Getter; import lombok.RequiredArgsConstructor; @@ -15,8 +18,8 @@ import java.math.BigInteger; */ @RequiredArgsConstructor public class Value { - public static final Value TRUE = new Value<>(Type.BOOL, true); - public static final Value FALSE = new Value<>(Type.BOOL, false); + public static final Value TRUE = new Value<>(SimpleType.BOOL, true); + public static final Value FALSE = new Value<>(SimpleType.BOOL, false); @Getter private final Type type; @@ -25,35 +28,35 @@ public class Value { public static Value from(IntegerLiteral i) { - return new Value<>(Type.INT, i.getValue()); + return new Value<>(SimpleType.INT, i.getValue()); } public static Value from(Integer i) { - return new Value<>(Type.INT, BigInteger.valueOf(i)); + return new Value<>(SimpleType.INT, BigInteger.valueOf(i)); } public static Value from(StringLiteral s) { - return new Value<>(Type.STRING, s.getText()); + return new Value<>(SimpleType.STRING, s.getText()); } public static Value from(BooleanLiteral b) { - return new Value(Type.BOOL, b.isValue()); + return new Value<>(SimpleType.BOOL, b.isValue()); } public static Value from(boolean equals) { - return new Value(Type.BOOL, equals); + return new Value<>(SimpleType.BOOL, equals); } public static Value from(BigInteger apply) { - return new Value<>(Type.INT, apply); + return new Value<>(SimpleType.INT, apply); } public static Value from(String s) { - return new Value<>(Type.STRING, s); + return new Value<>(SimpleType.STRING, s); } public static Value from(TermLiteral term) { - return new Value<>(Type.TERM, term.getText()); + return new Value<>(TypeFacade.ANY_TERM, term.getText()); } @Override diff --git a/src/main/java/edu/kit/formal/interpreter/data/VariableAssignment.java b/src/main/java/edu/kit/formal/interpreter/data/VariableAssignment.java index 93deeea67813bcc5887ff4194b24c7909911e0d6..0aa3de03456167335424a824fc995b3dbb5ffed0 100644 --- a/src/main/java/edu/kit/formal/interpreter/data/VariableAssignment.java +++ b/src/main/java/edu/kit/formal/interpreter/data/VariableAssignment.java @@ -1,8 +1,9 @@ package edu.kit.formal.interpreter.data; import edu.kit.formal.interpreter.exceptions.VariableNotDefinedException; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import edu.kit.formal.proofscriptparser.ast.Variable; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.ToString; import java.util.HashMap; diff --git a/src/main/java/edu/kit/formal/interpreter/dbg/PseudoMatcher.java b/src/main/java/edu/kit/formal/interpreter/dbg/PseudoMatcher.java index 8450f11b685ba0a8ae828b232ec4359a7fd81407..8e08c00abf50a1dff0f88ba3a558b7659e98c20c 100644 --- a/src/main/java/edu/kit/formal/interpreter/dbg/PseudoMatcher.java +++ b/src/main/java/edu/kit/formal/interpreter/dbg/PseudoMatcher.java @@ -5,8 +5,9 @@ import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.Value; import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.proofscriptparser.ast.Signature; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import edu.kit.formal.proofscriptparser.ast.Variable; +import edu.kit.formal.proofscriptparser.types.Type; import java.util.Collections; import java.util.List; diff --git a/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java b/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java index 727babbf287587159f57295c05d79b1e85f69376..48fcf8b32555d8078ed171038cecd163edabe20d 100644 --- a/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java +++ b/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java @@ -5,6 +5,7 @@ import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.data.Value; import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.SimpleType; import lombok.Getter; import lombok.RequiredArgsConstructor; @@ -39,7 +40,7 @@ public class MacroCommandHandler implements CommandHandler { CallStatement macroCall = new CallStatement("macro", p); macroCall.setRuleContext(call.getRuleContext()); VariableAssignment newParam = new VariableAssignment(null); - newParam.declare("#2", Type.STRING); + newParam.declare("#2", SimpleType.STRING); newParam.assign("#2", Value.from(call.getCommand())); //macro proofscript command interpreter.getFunctionLookup().callCommand(interpreter, macroCall, newParam); diff --git a/src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java b/src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java index 14f657bac8b5791afda0a5b7ae5d7c31e5e7903c..807c6f568d1af8b4847c968d64a2e321e485b757 100644 --- a/src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java @@ -1,7 +1,7 @@ package edu.kit.formal.interpreter.graphs; /** - * Edge Types a state graph and control flow graph may have + * Edge Type a state graph and control flow graph may have */ public enum EdgeTypes { STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN, STEP_OVER_COND, STATE_FLOW; diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java b/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java index 86c468284f666256dcd90e4cf8b58b76c61d47e2..0298935fb1477f1bc807a040aefb572e51fb5786 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java @@ -24,6 +24,8 @@ package edu.kit.formal.proofscriptparser; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import java.util.ArrayList; import java.util.Map; diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java b/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java index 6557c4258b919d34457aa025e79540f802e278dc..ec7db374a951e6ad30554b6757d4d97a5401e5ff 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java @@ -24,6 +24,7 @@ package edu.kit.formal.proofscriptparser; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.Type; import java.util.Map; @@ -146,7 +147,7 @@ public interface ASTTraversal extends Visitor { @Override default T visit(Parameters parameters) { for (Map.Entry e : - parameters.entrySet()) { + parameters.entrySet()) { e.getKey().accept(this); e.getValue().accept(this); } @@ -171,4 +172,13 @@ public interface ASTTraversal extends Visitor { simpleCaseStatement.getBody().accept(this); return null; } + + @Override + default T visit(SubstituteExpression subst) { + subst.getSub().accept(this); + for (Expression e : subst.getSubstitution().values()) { + e.accept(this); + } + return null; + } } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java b/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java index 3f4aecf4156ed4bd4f9a002a11bb20586fc4836e..72b02611def2d6c8755f8b22f9f8e58369435f7e 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java @@ -94,6 +94,11 @@ public class DefaultASTVisitor implements Visitor { return defaultVisit(caseStatement); } + @Override + public T visit(SubstituteExpression subst) { + return defaultVisit(subst); + } + @Override public T visit(CallStatement call) { return defaultVisit(call); @@ -138,5 +143,6 @@ public class DefaultASTVisitor implements Visitor { public T visit(SimpleCaseStatement simpleCaseStatement) { return defaultVisit(simpleCaseStatement); } + } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java b/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java index 1b4b72381066f0ab8a048337ad6fc529d919d271..2fa6614f336f9326c1d289a7b95f7599fb34a51f 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java @@ -24,6 +24,8 @@ package edu.kit.formal.proofscriptparser; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Getter; import lombok.Setter; diff --git a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java index ece815e0b2992b8ffa9b541a7a5da2915e30fd59..49dff1fee4365f4836b5273af6276237507e73ca 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java @@ -24,6 +24,7 @@ package edu.kit.formal.proofscriptparser; import edu.kit.formal.proofscriptparser.ast.*; +import edu.kit.formal.proofscriptparser.types.TypeFacade; import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.tree.ErrorNode; import org.antlr.v4.runtime.tree.ParseTree; @@ -31,7 +32,9 @@ import org.antlr.v4.runtime.tree.RuleNode; import org.antlr.v4.runtime.tree.TerminalNode; import java.util.ArrayList; +import java.util.LinkedHashMap; import java.util.List; +import java.util.Map; /** * @author Alexander Weigl @@ -66,7 +69,8 @@ public class TransformAst implements ScriptLanguageVisitor { public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) { Signature signature = new Signature(); for (ScriptLanguageParser.VarDeclContext decl : ctx.varDecl()) { - signature.put(new Variable(decl.name), Type.findType(decl.type.getText())); + signature.put(new Variable(decl.name), + TypeFacade.findType(decl.type.getText())); } return signature; } @@ -80,7 +84,7 @@ public class TransformAst implements ScriptLanguageVisitor { public Object visitVarDecl(ScriptLanguageParser.VarDeclContext ctx) { /* VariableDeclaration varDecl = new VariableDeclaration(); varDecl.setIdentifier(new Variable(ctx.name)); - varDecl.setType(Type.findType(ctx.type.getText())); + varDecl.setType(SimpleType.findType(ctx.type.getText())); return varDecl;*/ return null; @@ -90,7 +94,7 @@ public class TransformAst implements ScriptLanguageVisitor { public Statements visitStmtList(ScriptLanguageParser.StmtListContext ctx) { Statements statements = new Statements(); for (ScriptLanguageParser.StatementContext stmt : ctx.statement()) { - statements.add((Statement) stmt.accept(this)); + statements.add((Statement) stmt.accept(this)); } return statements; } @@ -107,10 +111,10 @@ public class TransformAst implements ScriptLanguageVisitor { assign.setRuleContext(ctx); assign.setLhs(new Variable(ctx.variable)); if (ctx.type != null) { - assign.setType(Type.findType(ctx.type.getText())); + assign.setType(TypeFacade.findType(ctx.type.getText())); } if (ctx.expression() != null) { - assign.setRhs((Expression) ctx.expression().accept(this)); + assign.setRhs((Expression) ctx.expression().accept(this)); } return assign; } @@ -123,8 +127,8 @@ public class TransformAst implements ScriptLanguageVisitor { private BinaryExpression createBinaryExpression(ParserRuleContext ctx, List expression, Operator op) { BinaryExpression be = new BinaryExpression(); - be.setLeft((Expression) expression.get(0).accept(this)); - be.setRight((Expression) expression.get(1).accept(this)); + be.setLeft((Expression) expression.get(0).accept(this)); + be.setRight((Expression) expression.get(1).accept(this)); be.setOperator(op); return be; } @@ -132,7 +136,7 @@ public class TransformAst implements ScriptLanguageVisitor { private UnaryExpression createUnaryExpression(ParserRuleContext ctx, ScriptLanguageParser.ExpressionContext expression, Operator op) { UnaryExpression ue = new UnaryExpression(); ue.setRuleContext(ctx); - ue.setExpression((Expression) expression.accept(this)); + ue.setExpression((Expression) expression.accept(this)); ue.setOperator(op); return ue; } @@ -153,7 +157,6 @@ public class TransformAst implements ScriptLanguageVisitor { } - private Operator findOperator(String n) { return findOperator(n, 2); } @@ -222,12 +225,21 @@ public class TransformAst implements ScriptLanguageVisitor { @Override public Object visitExprSubst(ScriptLanguageParser.ExprSubstContext ctx) { - return null; + SubstituteExpression se = new SubstituteExpression(); + se.setSub((Expression) ctx.expression().accept(this)); + se.setSubstitution( + (Map) ctx.substExpressionList().accept(this)); + return se; } @Override - public Object visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) { - return null; + public Map visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) { + Map map = new LinkedHashMap<>(); + for (int i = 0; i < ctx.scriptVar().size(); i++) { + map.put(ctx.scriptVar(i).getText(), + (Expression) ctx.expression(i).accept(this)); + } + return map; } @Override @@ -267,11 +279,11 @@ public class TransformAst implements ScriptLanguageVisitor { if (ctx.derivable != null) { match.setDerivable(true); - match.setDerivableTerm((Expression) ctx.derivableExpression.accept(this)); + match.setDerivableTerm((Expression) ctx.derivableExpression.accept(this)); } else { if (ctx.argList() != null) match.setSignature((Signature) ctx.argList().accept(this)); - match.setPattern((Expression) ctx.pattern.accept(this)); + match.setPattern((Expression) ctx.pattern.accept(this)); } return match; @@ -314,7 +326,7 @@ public class TransformAst implements ScriptLanguageVisitor { } else { SimpleCaseStatement caseStatement = new SimpleCaseStatement(); caseStatement.setRuleContext(ctx); - caseStatement.setGuard((Expression) ctx.expression().accept(this)); + caseStatement.setGuard((Expression) ctx.expression().accept(this)); caseStatement.setBody((Statements) ctx.stmtList().accept(this)); return caseStatement; } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java b/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java index b96612a7eedbecd077e4ef5a60a379ac4efcbc5f..507fd474afadb285a0526e91f81a34923bfa198b 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java @@ -75,4 +75,6 @@ public interface Visitor { T visit(SimpleCaseStatement simpleCaseStatement); T visit(CaseStatement caseStatement); + + T visit(SubstituteExpression subst); } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/AssignmentStatement.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/AssignmentStatement.java index 62be715baafb2cdbfa3d1873c623c745ad7afd3f..6a51f20d3f2ada3983ce911618bed8d8a0c1e5f6 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/AssignmentStatement.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/AssignmentStatement.java @@ -26,6 +26,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.ScriptLanguageParser; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.*; /** diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java index 021a9a5b9f8e9c7f35855663ba05eb0f7f2cf277..268f3edce4846298036cdccc09aab6b26982ee0e 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java @@ -25,6 +25,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Data; import org.antlr.v4.runtime.ParserRuleContext; diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java index b1bd3fea0783b4fb48f5f46c4ce10069ea6b8af8..ee2cb748c753dc445037c35593280e6d54e38d9f 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java @@ -26,6 +26,7 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; import lombok.Data; import lombok.EqualsAndHashCode; import lombok.Getter; @@ -82,7 +83,7 @@ public class BooleanLiteral extends Literal { * {@inheritDoc} */ @Override - public Type getType(Signature signature) throws NotWelldefinedException { - return Type.BOOL; + public SimpleType getType(Signature signature) throws NotWelldefinedException { + return SimpleType.BOOL; } } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java index f559e4720c474faea2d4bb19b8a3bfd2eb9135e2..e71d8dfb9f40f8ad05b47a13f34778c7872fc8ea 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java @@ -25,6 +25,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import org.antlr.v4.runtime.ParserRuleContext; /** diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java index 1edb994f4fcc68402c6021096f74e4eba0abc920..9d56600a229ffdb4ed32ec00f9b21deaf3075e95 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java @@ -26,6 +26,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Data; import org.antlr.v4.runtime.Token; @@ -78,7 +80,7 @@ public class IntegerLiteral extends Literal { */ @Override public Type getType(Signature signature) throws NotWelldefinedException { - return Type.INT; + return SimpleType.INT; } 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 abc52cac832fe54436dde9b40ad4abb791374e58..24206ee77bee4d02d11fe1cf438d1d0390b7c927 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java @@ -26,6 +26,9 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.ScriptLanguageParser; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.TermType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Data; import lombok.Getter; import lombok.Setter; @@ -73,15 +76,10 @@ public class MatchExpression extends Expression", "[]", 10, TypeFacade.ANY_TERM, TypeFacade.ANY_TERM) { + @Override + public Value evaluate(Value[] v) { + return null;// see SubstituteExpression for handling + } + }, /** * */ @@ -176,6 +189,7 @@ public enum Operator { }; + private final String symbol; private final String unicode; private final int precedence; diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/Signature.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/Signature.java index 0e93a27b8fa47590bf8482a1bee7f9e859b2ffbd..85bb4f2ddf8dd96a73196d06c22ae39277dbd2e9 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/Signature.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/Signature.java @@ -26,6 +26,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.ScriptLanguageParser; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.Type; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.EqualsAndHashCode; import lombok.ToString; @@ -142,17 +144,17 @@ public class Signature extends ASTNode impl } public Type computeIfPresent(Variable key, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return sig.computeIfPresent(key, remappingFunction); } public Type compute(Variable key, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return sig.compute(key, remappingFunction); } public Type merge(Variable key, Type value, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return sig.merge(key, value, remappingFunction); } } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/StringLiteral.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/StringLiteral.java index ea8bd2cfaf2025c5ecb5771481efc51cb2873f73..e1eb1821a5a775edf0ad5b430be5af2531d12b30 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/StringLiteral.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/StringLiteral.java @@ -25,6 +25,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Data; /** @@ -69,6 +71,6 @@ public class StringLiteral extends Literal { */ @Override public Type getType(Signature signature) throws NotWelldefinedException { - return Type.STRING; + return SimpleType.STRING; } } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/SubstituteExpression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/SubstituteExpression.java new file mode 100644 index 0000000000000000000000000000000000000000..5dea80c62aa16b01c57eedc9cabc34e5bf1f6ecc --- /dev/null +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/SubstituteExpression.java @@ -0,0 +1,53 @@ +package edu.kit.formal.proofscriptparser.ast; + +import edu.kit.formal.proofscriptparser.NotWelldefinedException; +import edu.kit.formal.proofscriptparser.ScriptLanguageParser; +import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.Type; +import edu.kit.formal.proofscriptparser.types.TypeFacade; +import lombok.Data; + +import java.util.LinkedHashMap; +import java.util.Map; + +/** + * @author Alexander Weigl + * @version 1 (15.08.17) + */ +@Data +public class SubstituteExpression extends Expression { + private Expression sub; + private Map substitution = new LinkedHashMap<>(); + + @Override + public boolean hasMatchExpression() { + return sub.hasMatchExpression(); + } + + @Override + public int getPrecedence() { + return Operator.SUBST.precedence(); + } + + @Override + public T accept(Visitor visitor) { + return visitor.visit(this); + } + + @Override + public Expression copy() { + SubstituteExpression se = new SubstituteExpression(); + se.sub = sub.copy(); + se.substitution = new LinkedHashMap<>(substitution); + return se; + } + + @Override + public Type getType(Signature signature) throws NotWelldefinedException { + Type t = sub.getType(signature); + if(!TypeFacade.isTerm(t)){ + throw new NotWelldefinedException("Term expected, got " + t.symbol(), this); + } + return TypeFacade.ANY_TERM; + } +} diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/TermLiteral.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/TermLiteral.java index ef11b1b73ccca3dd6ed8b4c44a8ffaf228b20323..66f85bcd165ed247acbfda341234785ad9c669f5 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/TermLiteral.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/TermLiteral.java @@ -26,6 +26,9 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; +import edu.kit.formal.proofscriptparser.types.TypeFacade; import lombok.Data; /** @@ -73,6 +76,7 @@ public class TermLiteral extends Literal { */ @Override public Type getType(Signature signature) throws NotWelldefinedException { - return Type.TERM; + return TypeFacade.ANY_TERM; } + } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/UnaryExpression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/UnaryExpression.java index 6282bdf0e0097d81280fe5232489509797b3e2ff..355748d94ab284136eb49dd5e8ba3d2c10d00d5e 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/UnaryExpression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/UnaryExpression.java @@ -26,6 +26,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.AllArgsConstructor; import lombok.Data; import lombok.NoArgsConstructor; diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java index 0be2fa368fec67f384a079b02434addb7236deea..814bda39d40ed1a915e76a3b8210448b96ef0cb3 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java @@ -26,6 +26,8 @@ package edu.kit.formal.proofscriptparser.ast; import edu.kit.formal.proofscriptparser.NotWelldefinedException; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import lombok.Data; import lombok.EqualsAndHashCode; import lombok.NonNull; diff --git a/src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/VariableDeclarationCheck.java b/src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/VariableDeclarationCheck.java index 728324bb940abc3aebb5fee8fc1f3c3c5f33549a..c6613392d8d3739bb8242fcf18ef632e1da8e966 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/VariableDeclarationCheck.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/VariableDeclarationCheck.java @@ -4,6 +4,8 @@ import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.lint.Issue; import edu.kit.formal.proofscriptparser.lint.IssuesRepository; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import edu.kit.formal.proofscriptparser.types.Type; import org.antlr.v4.runtime.Token; import java.util.HashMap; @@ -59,6 +61,11 @@ public class VariableDeclarationCheck extends AbstractLintRule { return null; } + @Override + public Void visit(SubstituteExpression subst) { + return null; + } + private void declare(Variable var, Type type) { if (current.getType(var) != null) { problem(REDECLARE_VARIABLE).tokens(var.getToken()); diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/Type.java b/src/main/java/edu/kit/formal/proofscriptparser/types/SimpleType.java similarity index 72% rename from src/main/java/edu/kit/formal/proofscriptparser/ast/Type.java rename to src/main/java/edu/kit/formal/proofscriptparser/types/SimpleType.java index 6f44d23d5fd10a53700871f99f2a427fe044f8d4..a173cee688a595b4344f3d2ad4789ad39b7e8225 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/Type.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/types/SimpleType.java @@ -1,4 +1,4 @@ -package edu.kit.formal.proofscriptparser.ast; +package edu.kit.formal.proofscriptparser.types; /*- * #%L @@ -23,34 +23,24 @@ package edu.kit.formal.proofscriptparser.ast; */ - -import java.util.Arrays; - /** * Represents the possible types (including scriptVarTypes). * * Created at 30.04.2017 * @author Sarah Grebing */ -public enum Type { - STRING("string"), TERM("term"), ANY("any"), +public enum SimpleType implements Type { + STRING("string"), ANY("any"), INT("int"), BOOL("bool"), INT_ARRAY("int[]"), OBJECT("object"), HEAP("heap"), FIELD("field"), LOCSET("locset"), NULL("null"), FORMULA("formula"), SEQ("Seq"); private final String symbol; - Type(String symbol) { + SimpleType(String symbol) { this.symbol = symbol; } - public static Type findType(String n) { - for (Type t : Type.values()) { - if (t.symbol().equals(n)) - return t; - } - throw new IllegalStateException("Type " + n + " is not defined. Valid types are: " + Arrays.toString(values())); - } - + @Override public String symbol() { return symbol; } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/types/TermType.java b/src/main/java/edu/kit/formal/proofscriptparser/types/TermType.java new file mode 100644 index 0000000000000000000000000000000000000000..088250da0235c83586e5b92a202ef235870ef894 --- /dev/null +++ b/src/main/java/edu/kit/formal/proofscriptparser/types/TermType.java @@ -0,0 +1,27 @@ +package edu.kit.formal.proofscriptparser.types; + +import lombok.AllArgsConstructor; +import lombok.Data; +import lombok.NoArgsConstructor; + +import java.util.ArrayList; +import java.util.List; + +/** + * @author Alexander Weigl + * @version 1 (15.08.17) + */ +@AllArgsConstructor +@NoArgsConstructor +@Data +public class TermType implements Type { + private List argTypes = new ArrayList<>(); + + @Override + public String symbol() { + return "Term<" + + argTypes.stream().map(Type::symbol).reduce((a, b) -> (a + "," + b)).orElse("") + + ">"; + } + +} diff --git a/src/main/java/edu/kit/formal/proofscriptparser/types/Type.java b/src/main/java/edu/kit/formal/proofscriptparser/types/Type.java new file mode 100644 index 0000000000000000000000000000000000000000..96d133e6b7a5eb6402d153860af0745dbfc42688 --- /dev/null +++ b/src/main/java/edu/kit/formal/proofscriptparser/types/Type.java @@ -0,0 +1,9 @@ +package edu.kit.formal.proofscriptparser.types; + +/** + * @author Alexander Weigl + * @version 1 (15.08.17) + */ +public interface Type { + String symbol(); +} diff --git a/src/main/java/edu/kit/formal/proofscriptparser/types/TypeFacade.java b/src/main/java/edu/kit/formal/proofscriptparser/types/TypeFacade.java new file mode 100644 index 0000000000000000000000000000000000000000..4a2250a557c9832e9639e8141f4d8f1d2a4c87af --- /dev/null +++ b/src/main/java/edu/kit/formal/proofscriptparser/types/TypeFacade.java @@ -0,0 +1,41 @@ +package edu.kit.formal.proofscriptparser.types; + +import java.util.Arrays; + +/** + * @author Alexander Weigl + * @version 1 (15.08.17) + */ +public final class TypeFacade { + public static final Type ANY_TERM = new TermType(); + + public static TermType getTermType(String symbol) { + if (symbol.startsWith("Term<") && symbol.endsWith(">")) { + TermType tt = new TermType(); + String n = symbol.substring(6, symbol.length() - 2); + for (String term : n.split(",")) { + tt.getArgTypes().add(findType(term)); + } + return tt; + } + return null; + } + + public static Type findType(String n) { + TermType tt = getTermType(n); + if (tt != null) return tt; + return getSimpleType(n); + } + + public static SimpleType getSimpleType(String n) { + for (SimpleType t : SimpleType.values()) { + if (t.symbol().equals(n)) + return t; + } + throw new IllegalStateException("SimpleType " + n + " is not defined. Valid types are: " + Arrays.toString(SimpleType.values())); + } + + public static boolean isTerm(Type type) { + return type instanceof TermType; + } +} diff --git a/src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java b/src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java index 5007c4bd72b280aa5cde6ec3173e512e7d6d9f4b..dfe40246ebddb04ea99fd5ed7ea23c06b59ea2e7 100644 --- a/src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java +++ b/src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java @@ -5,7 +5,7 @@ import edu.kit.formal.interpreter.data.Value; import edu.kit.formal.interpreter.dbg.PseudoMatcher; import edu.kit.formal.proofscriptparser.TestHelper; import edu.kit.formal.proofscriptparser.ast.Expression; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import org.junit.Assert; import org.junit.Before; import org.junit.Test; @@ -37,8 +37,8 @@ public class EvaluatorTest { public void setup() { GoalNode parent = new GoalNode<>(null, "pa", false); parent.getAssignments() - .declare("a", Type.INT) - .declare("b", Type.INT) + .declare("a", SimpleType.INT) + .declare("b", SimpleType.INT) .assign("a", Value.from(1)) .assign("b", Value.from(1)); GoalNode selected = new GoalNode<>(parent, "selg", false); diff --git a/src/test/java/edu/kit/formal/interpreter/MatchEvaluatorTest.java b/src/test/java/edu/kit/formal/interpreter/MatchEvaluatorTest.java index 9ffefb10e5ce35ae58ed8e9cf12c934ed9d69aed..13193d103a46c05a52b0abdcb3d55aa5f6a05716 100644 --- a/src/test/java/edu/kit/formal/interpreter/MatchEvaluatorTest.java +++ b/src/test/java/edu/kit/formal/interpreter/MatchEvaluatorTest.java @@ -4,7 +4,7 @@ import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.Value; import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.interpreter.dbg.PseudoMatcher; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import edu.kit.formal.proofscriptparser.ast.Variable; import org.junit.Before; @@ -23,8 +23,8 @@ public class MatchEvaluatorTest { @Before public void setup() { GoalNode parent = new GoalNode<>(null, "pa", false); - parent.declareVariable(new Variable("a"), Type.INT); - parent.declareVariable(new Variable("b"), Type.INT); + parent.declareVariable(new Variable("a"), SimpleType.INT); + parent.declareVariable(new Variable("b"), SimpleType.INT); VariableAssignment va = parent.getAssignments(); va.assign(new Variable("a"), Value.from(1)); va.assign(new Variable("b"), Value.from(1)); diff --git a/src/test/java/edu/kit/formal/interpreter/VariableAssignmentTest.java b/src/test/java/edu/kit/formal/interpreter/VariableAssignmentTest.java index 42acb32a7cdc958b41651cd6051d255250bb6e6e..67370a77acd87b2a646603ce2710943e9b409dc7 100644 --- a/src/test/java/edu/kit/formal/interpreter/VariableAssignmentTest.java +++ b/src/test/java/edu/kit/formal/interpreter/VariableAssignmentTest.java @@ -2,7 +2,7 @@ package edu.kit.formal.interpreter; import edu.kit.formal.interpreter.data.Value; import edu.kit.formal.interpreter.data.VariableAssignment; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import org.junit.Assert; import org.junit.Before; import org.junit.Test; @@ -18,25 +18,25 @@ public class VariableAssignmentTest { @Before public void setup() { va1 = new VariableAssignment(null); - va1.declare("a", Type.INT); - va1.declare("b", Type.INT); - va1.declare("c", Type.INT); + va1.declare("a", SimpleType.INT); + va1.declare("b", SimpleType.INT); + va1.declare("c", SimpleType.INT); va1.assign("a", Value.from(1)); va1.assign("b", Value.from(2)); va1.assign("c", Value.from(3)); va2 = new VariableAssignment(null); - va2.declare("d", Type.INT); - va2.declare("e", Type.INT); - va2.declare("f", Type.INT); + va2.declare("d", SimpleType.INT); + va2.declare("e", SimpleType.INT); + va2.declare("f", SimpleType.INT); va2.assign("d", Value.from(1)); va2.assign("e", Value.from(2)); va2.assign("f", Value.from(3)); va3 = new VariableAssignment(null); - va3.declare("a", Type.INT); - va3.declare("b", Type.INT); - va3.declare("c", Type.INT); + va3.declare("a", SimpleType.INT); + va3.declare("b", SimpleType.INT); + va3.declare("c", SimpleType.INT); va3.assign("a", Value.from(1)); va3.assign("b", Value.from(3)); va3.assign("c", Value.from(3)); diff --git a/src/test/java/edu/kit/formal/proofscriptparser/EvalTest.java b/src/test/java/edu/kit/formal/proofscriptparser/EvalTest.java new file mode 100644 index 0000000000000000000000000000000000000000..374771b892acdb1215cba9dc61c7373f141347bc --- /dev/null +++ b/src/test/java/edu/kit/formal/proofscriptparser/EvalTest.java @@ -0,0 +1,85 @@ +package edu.kit.formal.proofscriptparser; + +/*- + * #%L + * ProofScriptParser + * %% + * Copyright (C) 2017 Application-oriented Formal Verification + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public + * License along with this program. If not, see + * . + * #L% + */ + + +import edu.kit.formal.interpreter.Evaluator; +import edu.kit.formal.interpreter.data.GoalNode; +import edu.kit.formal.interpreter.data.Value; +import edu.kit.formal.interpreter.data.VariableAssignment; +import edu.kit.formal.proofscriptparser.ast.Expression; +import edu.kit.formal.proofscriptparser.ast.Signature; +import edu.kit.formal.proofscriptparser.ast.Variable; +import edu.kit.formal.proofscriptparser.types.SimpleType; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.IOException; + +@RunWith(Parameterized.class) +public class EvalTest { + @Parameterized.Parameters(name = "{0}") + public static Iterable getGoodExpressions() throws IOException { + return TestHelper.loadLines("eval.txt", 2); + } + + @Parameterized.Parameter(0) + public String testExpression; + + @Parameterized.Parameter(1) + public String expResult; + + + @Test + public void test() throws IOException, NotWelldefinedException { + Expression e_is = TestHelper.toExpr(testExpression); + Expression e_exp = TestHelper.toExpr(expResult); + + VariableAssignment s = createAssignments(); + Evaluator evaluator = new Evaluator(s, new GoalNode(null, null, true)); + + Value is = evaluator.eval(e_is); + Value exp = evaluator.eval(e_exp); + + Assert.assertEquals(exp,is); + } + + public static VariableAssignment createAssignments() { + VariableAssignment va = new VariableAssignment(); + va.declare("a", SimpleType.INT); + va.assign("a", Value.from(10)); + va.declare("b", SimpleType.INT); + va.assign("b", Value.from(2)); + + va.declare("c", SimpleType.INT); + va.assign("c", Value.from(10)); + + va.declare("d", SimpleType.INT); + va.assign("d", Value.from(10)); + + return va; + } + +} diff --git a/src/test/java/edu/kit/formal/proofscriptparser/GoodExpressionTest.java b/src/test/java/edu/kit/formal/proofscriptparser/GoodExpressionTest.java index f10526d12a4cdba9b88505e72bce430351e96b34..ccef7a77da2d2d7d9ec834a307a06f4e31971fc6 100644 --- a/src/test/java/edu/kit/formal/proofscriptparser/GoodExpressionTest.java +++ b/src/test/java/edu/kit/formal/proofscriptparser/GoodExpressionTest.java @@ -26,7 +26,7 @@ package edu.kit.formal.proofscriptparser; import edu.kit.formal.proofscriptparser.ast.Expression; import edu.kit.formal.proofscriptparser.ast.Signature; -import edu.kit.formal.proofscriptparser.ast.Type; +import edu.kit.formal.proofscriptparser.types.SimpleType; import edu.kit.formal.proofscriptparser.ast.Variable; import org.junit.Assert; import org.junit.Test; @@ -59,12 +59,12 @@ public class GoodExpressionTest { public static Signature createSignature() { Signature s = new Signature(); - s.put(new Variable("a"), Type.BOOL); - s.put(new Variable("b"), Type.BOOL); - s.put(new Variable("c"), Type.BOOL); - s.put(new Variable("i"), Type.INT); - s.put(new Variable("j"), Type.INT); - s.put(new Variable("k"), Type.INT); + s.put(new Variable("a"), SimpleType.BOOL); + s.put(new Variable("b"), SimpleType.BOOL); + s.put(new Variable("c"), SimpleType.BOOL); + s.put(new Variable("i"), SimpleType.INT); + s.put(new Variable("j"), SimpleType.INT); + s.put(new Variable("k"), SimpleType.INT); return s; } diff --git a/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt b/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt index 333770133c3f38fa62915621dbbdd3b735f42b87..8f631536a2c77f3dbcbed871256b421716f960fe 100644 --- a/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt +++ b/src/test/resources/edu/kit/formal/proofscriptparser/eval.txt @@ -24,3 +24,6 @@ a + b >>> 2 1=2 | 3=3 >>> true 1=2 >>> false b=a&3=3|a=b >>> true +`f(x)`[] >>> `f(x)` +`f(?X)`[?X/`g(x)`] >>> `f(g(x))` +5+3*2 >>> 11 \ No newline at end of file diff --git a/src/test/resources/edu/kit/formal/proofscriptparser/goodexpr.txt b/src/test/resources/edu/kit/formal/proofscriptparser/goodexpr.txt index 2aef8aff15f41851d11d100ca90eb9f694146827..d09359b868795aefb79bc32f07a02c275807f0dd 100644 --- a/src/test/resources/edu/kit/formal/proofscriptparser/goodexpr.txt +++ b/src/test/resources/edu/kit/formal/proofscriptparser/goodexpr.txt @@ -3,6 +3,7 @@ true false (true | false) & true <=> a | b `f(x)` +`f(x)`[X/2,y/x] 'abc\'abc' 'blubber' 1+1