Skip to content

GitLab

Commit 90be741d authored by Sarah Grebing's avatar Sarah Grebing
Browse files

added first idea for label matcher

parent bc05d208
Pipeline #12404 failed with stage
in 1 minute and 38 seconds
Hide whitespace changes
Inline Side-by-side
src/main/java/edu/kit/formal/interpreter/Interpreter.java
View file @ 90be741d
......@@ -38,6 +38,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
.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)
.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)
......@@ -236,7 +237,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
}
//remove state from stack
State<T> stateAfterCase = popState();
System.out.println("State after Case " + stateAfterCase.getSelectedGoalNode().toCellTextForKeYData());
// System.out.println("State after Case " + stateAfterCase.getSelectedGoalNode().toCellTextForKeYData());
if (result && stateAfterCase.getGoals() != null) {
goalsAfterCases.addAll(stateAfterCase.getGoals());
}
......@@ -280,6 +281,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
if (goalsAfterCases.size() == 1) {
newStateAfterCases = new State<T>(goalsAfterCases, 0);
} else {
//TODO check for closed goals?
newStateAfterCases = new State<T>(goalsAfterCases, null);
}
stateStack.push(newStateAfterCases);
......@@ -319,6 +321,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
*/
private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode<T> goal) {
enterScope(matchExpression);
System.out.println("Goal to match " + goal.toCellTextForKeYData());
MatchEvaluator mEval = new MatchEvaluator(goal.getAssignments(), goal, matcherApi);
mEval.getEntryListeners().addAll(entryListeners);
mEval.getExitListeners().addAll(exitListeners);
......
src/main/java/edu/kit/formal/interpreter/KeYMatcher.java
View file @ 90be741d
......@@ -26,6 +26,9 @@ import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.regex.MatchResult;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
/**
* Interface to KeY Matcher Api
......@@ -36,6 +39,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
private static final Name CUT_TACLET_NAME = new Name("cut");
private ScriptApi scrapi;
private Interpreter<KeyData> interpreter;
private List<MatchResult> resultsFromLabelMatch;
public KeYMatcher(ScriptApi scrapi, Interpreter<KeyData> interpreter) {
this.scrapi = scrapi;
......@@ -79,13 +83,84 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
}
/**
* If teh label matcher was successful the list contains all match results
*
* @return
*/
public List<MatchResult> getResultsFromLabelMatch() {
return resultsFromLabelMatch;
}
/**
* Match the label of a goal node
*
* @param currentState goal node as possible match cancidate
* @param label String representation for regualr expression for label to match
* @return List of matches if match was sucessful, empty list otherwise
*/
@Override
public List<VariableAssignment> matchLabel(GoalNode<KeyData> currentState,
String label) {
List<VariableAssignment> assignments = new ArrayList<>();
resultsFromLabelMatch = new ArrayList<>();
//compile pattern
Pattern regexpForLabel = Pattern.compile(label);
String branchLabel = currentState.getData().getBranchingLabel();
Matcher branchLabelMatcher = regexpForLabel.matcher(branchLabel);
if (branchLabelMatcher.matches()) {
VariableAssignment va = new VariableAssignment(null);
va.declare("$$branchLabel_", Type.STRING);
va.assign("$$branchLabel_", Value.from(branchLabelMatcher.group()));
assignments.add(va);
resultsFromLabelMatch.add(branchLabelMatcher.toMatchResult());
}
return null;
String controlFlowLines = currentState.getData().getProgramLinesLabel();
Matcher linesMatcher = regexpForLabel.matcher(controlFlowLines);
if (linesMatcher.matches()) {
VariableAssignment va = new VariableAssignment(null);
va.declare("$$CtrlLinesLabel_", Type.STRING);
va.assign("$$CtrlLinesLabel_", Value.from(linesMatcher.group()));
assignments.add(va);
resultsFromLabelMatch.add(linesMatcher.toMatchResult());
}
String controlFlowStmts = currentState.getData().getProgramStatementsLabel();
Matcher flowStmtsMatcher = regexpForLabel.matcher(controlFlowLines);
if (flowStmtsMatcher.matches()) {
VariableAssignment va = new VariableAssignment(null);
va.declare("$$FlowStmtsLabel_", Type.STRING);
va.assign("$$FlowStmtsLabel_", Value.from(flowStmtsMatcher.group()));
assignments.add(va);
resultsFromLabelMatch.add(flowStmtsMatcher.toMatchResult());
}
String ruleLabel = currentState.getData().getRuleLabel();
Matcher ruleMatcher = regexpForLabel.matcher(ruleLabel);
if (ruleMatcher.matches()) {
VariableAssignment va = new VariableAssignment(null);
va.declare("$$RuleLabel_", Type.STRING);
va.assign("$$RuleLabel_", Value.from(ruleMatcher.group()));
assignments.add(va);
resultsFromLabelMatch.add(ruleMatcher.toMatchResult());
}
assignments.forEach(variableAssignment -> System.out.println(variableAssignment));
return assignments.isEmpty()? null: assignments;
}
/**
* Match against a sequent of a goal node
* @param currentState
* @param term
* @param signature
* @return
*/
@Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState,
String term,
......@@ -110,10 +185,10 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
});
// System.out.println("Matching: "+term.toString()+"\n================\n"+currentState.getData().getNode().sequent()+"\n================\n");
List<VariableAssignments> keyMatchResult = scrapi.matchPattern(term, currentState.getData().getNode().sequent(), keyAssignments);
//empty keyassigmnments
System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term);
//empty keyassignments
// System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term);
List<VariableAssignment> transformedMatchResults = new ArrayList<>();
for (VariableAssignments mResult : keyMatchResult) {
transformedMatchResults.add(from(mResult));
......
src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java
View file @ 90be741d
......@@ -144,6 +144,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
/**
* Visit a match expression and decide which matcher to use. currently working is a matcher for sequents and a matcher for labels.
* @param match
* @return
*/
......@@ -157,6 +158,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
List<VariableAssignment> va = null;
if (pattern.getType() == Type.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) {
va = getMatcher().matchSeq(goal, (String) pattern.getData(), sig);
}
......
src/main/java/edu/kit/formal/proofscriptparser/ast/Type.java
View file @ 90be741d
......@@ -35,7 +35,7 @@ import java.util.Arrays;
public enum Type {
STRING("string"), TERM("term"), ANY("any"),
INT("int"), BOOL("bool"), INT_ARRAY("int[]"), OBJECT("object"),
HEAP("heap"), FIELD("field"), LOCSET("locset"), NULL("null"), FORMULA("formula");
HEAP("heap"), FIELD("field"), LOCSET("locset"), NULL("null"), FORMULA("formula"), SEQ("Seq");
private final String symbol;
......
src/test/resources/edu/kit/formal/interpreter/javaExample/test.kps
View file @ 90be741d
script t1(){
symbex;
cases{
case match '.*x.*':{
auto;
}
// case match `T >= 0 ==> ` using[ ?T:int]:{
// auto;
// }
default{
auto;
}
}
}
src/test/resources/edu/kit/formal/interpreter/paperExample/script.kps 0 → 100644
View file @ 90be741d
script prove_transitive(){
symbex;
cases{
case match
'seqPerm(?Res0Copy, ?Arr),
seqPerm(?Res0Sort, ?Res0Copy),
seqPerm(?Res1Copy0, ?Res0Sort),
seqPerm(?Res2Copy1, ?Res0Sort) ==>
seqPerm(?Res2Copy1, ?Arr)' using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res2Copy1: Seq, ?Res0Sort: Seq ]:
{SeqPermSym on='seqPerm(?Res0Copy, ?Arr) ==>';
SeqPermSym on='seqPerm(?Res0Sort, ?Res0Copy) ==>';
SeqPermSym on='seqPerm(?Res1Copy0, ?Res0Sort)==>';
SeqPermSym on='seqPerm(?Res2Copy1, ?Res0Sort) ==>';
SeqPermTrans on='seqPerm(?Res0Copy, ?Arr) ==>';
SeqPermTrans on='seqPerm(?Arr, ?Res0Sort) ==>'
with='seqPerm(?Arr,?Res2Copy1)';
SeqPermSym on='seqPerm(?Arr,?Res2Copy1)';
auto;
}
case match
'seqPerm(?Res0Copy, ?Arr),
seqPerm(?Res0Sort, ?Res0Copy),
seqPerm(?Res1Copy0, ?Res0Sort) ==>
seqPerm(?Res1Copy0, ?Arr)' using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res0Sort: Seq ]:
{SeqPermSym on='seqPerm(?Res0Copy, ?Arr)';
SeqPermSym on='seqPerm(?Res0Sort, ?Res0Copy)';
SeqPermSym on='seqPerm(?Res1Copy0, ?Res0Sort)';
SeqPermTrans on='seqPerm(?Res0Copy, ?Arr)';
SeqPermTrans on='seqPerm(?Arr, ?Res0Sort)'
SeqPermSym on='==> seqPerm(?Res1Copy0, ?Arr)';
auto;
}
default:{
auto;
}
}
}
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