Commit feec8b4b authored by Sarah Grebing's avatar Sarah Grebing

Fixed Matching bugs!

parent 53a01a49
Pipeline #10732 failed with stage
in 1 minute and 29 seconds
...@@ -18,6 +18,7 @@ import java.io.InputStreamReader; ...@@ -18,6 +18,7 @@ import java.io.InputStreamReader;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.Collections; import java.util.Collections;
import java.util.List; import java.util.List;
import java.util.Map;
import java.util.function.BiConsumer; import java.util.function.BiConsumer;
import java.util.regex.Matcher; import java.util.regex.Matcher;
import java.util.regex.Pattern; import java.util.regex.Pattern;
...@@ -190,6 +191,35 @@ public class Debugger { ...@@ -190,6 +191,35 @@ public class Debugger {
} }
public static class PseudoMatcher implements MatcherApi {
@Override
public List<VariableAssignment> 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<VariableAssignment> matchSeq(GoalNode currentState, String data, Signature sig) {
Pattern p = Pattern.compile(data, Pattern.CASE_INSENSITIVE);
Matcher m = p.matcher(currentState.getSequent());
p.pattern();
if (!m.matches())
return Collections.emptyList();
VariableAssignment va = new VariableAssignment();
for (Map.Entry<Variable, Type> s : sig.entrySet()) {
va.addVarDecl(s.getKey().getIdentifier(), s.getValue());
va.setVarValue(
s.getKey().getIdentifier(),
Value.from(m.group(s.getKey().getIdentifier())));
}
return Collections.singletonList(va);
}
}
private class CommandLogger extends DefaultASTVisitor<Void> { private class CommandLogger extends DefaultASTVisitor<Void> {
public void suffix(ASTNode node) { public void suffix(ASTNode node) {
...@@ -255,21 +285,4 @@ public class Debugger { ...@@ -255,21 +285,4 @@ public class Debugger {
return super.visit(repeatStatement); return super.visit(repeatStatement);
} }
} }
public static class PseudoMatcher implements MatcherApi {
@Override
public List<VariableAssignment> 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<VariableAssignment> matchSeq(GoalNode currentState, String data) {
return Collections.emptyList();
}
}
} }
...@@ -7,7 +7,6 @@ import lombok.Getter; ...@@ -7,7 +7,6 @@ import lombok.Getter;
import lombok.Setter; import lombok.Setter;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.Collections;
import java.util.List; import java.util.List;
/** /**
...@@ -19,18 +18,15 @@ import java.util.List; ...@@ -19,18 +18,15 @@ import java.util.List;
public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservable { public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservable {
@Getter @Getter
private final List<VariableAssignment> matchedVariables = new ArrayList<>(); private final List<VariableAssignment> matchedVariables = new ArrayList<>();
private final GoalNode goal;
private final VariableAssignment state;
@Getter @Getter
@Setter @Setter
private MatcherApi matcher; private MatcherApi matcher;
@Getter @Getter
private List<Visitor> entryListeners = new ArrayList<>(), private List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>(); exitListeners = new ArrayList<>();
private final GoalNode goal;
private final VariableAssignment state;
public Evaluator(VariableAssignment assignment, GoalNode node) { public Evaluator(VariableAssignment assignment, GoalNode node) {
state = new VariableAssignment(assignment); // unmodifiable version of assignment state = new VariableAssignment(assignment); // unmodifiable version of assignment
goal = node; goal = node;
...@@ -68,7 +64,7 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab ...@@ -68,7 +64,7 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab
if (pattern.getType() == Type.STRING) { if (pattern.getType() == Type.STRING) {
va = matcher.matchLabel(goal, (String) pattern.getData()); va = matcher.matchLabel(goal, (String) pattern.getData());
} else if (pattern.getType() == Type.TERM) { } else if (pattern.getType() == Type.TERM) {
va = matcher.matchSeq(goal, (String) pattern.getData()); va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
} }
return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE; return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE;
...@@ -76,13 +72,13 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab ...@@ -76,13 +72,13 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab
/** /**
* TODO Connect with KeY * TODO Connect with KeY
* * TODO remove return
* @param term * @param term
* @return * @return
*/ */
@Override @Override
public Value visit(TermLiteral term) { public Value visit(TermLiteral term) {
return null; return Value.from(term);
} }
@Override @Override
......
...@@ -126,6 +126,7 @@ public class GoalNode { ...@@ -126,6 +126,7 @@ public class GoalNode {
return assignments; return assignments;
} }
public VariableAssignment exitNewVarScope() { public VariableAssignment exitNewVarScope() {
this.assignments = this.assignments.pop(); this.assignments = this.assignments.pop();
return assignments; return assignments;
......
...@@ -153,51 +153,28 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -153,51 +153,28 @@ public class Interpreter extends DefaultASTVisitor<Void>
//global List after all Case Statements //global List after all Case Statements
List<GoalNode> goalsAfterCases = new ArrayList<>(); List<GoalNode> goalsAfterCases = new ArrayList<>();
//copy the list of goal nodes for keeping track of goals //copy the list of goal nodes for keeping track of goals
Set<GoalNode> copiedList = new HashSet<>(allGoalsBeforeCases); Set<GoalNode> remainingGoalsSet = new HashSet<>(allGoalsBeforeCases);
//handle cases //handle cases
List<CaseStatement> cases = casesStatement.getCases(); List<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) { for (CaseStatement aCase : cases) {
Map<GoalNode, VariableAssignment> matchedGoals = matchGoal(copiedList, aCase); Map<GoalNode, VariableAssignment> matchedGoals = matchGoal(remainingGoalsSet, aCase);
if (matchedGoals != null) { if (matchedGoals != null) {
copiedList.removeAll(matchedGoals.entrySet()); remainingGoalsSet.removeAll(matchedGoals.keySet());
goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals.keySet())); goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
} }
} }
/* Iterator<CaseStatement> casesIter = cases.iterator();
while (casesIter.hasNext()) {
//get information for case
CaseStatement currentCase = casesIter.next();
Expression guard = currentCase.getGuard();
Statements body = currentCase.getBody();
Iterator<GoalNode> goalIter = copiedList.iterator();
Set<GoalNode> forCase = new HashSet<>();
//iterate over all available goals and select those that evaluate to true with the guard
//assumption, matchpattern handles varAssignments
while (goalIter.hasNext()) {
GoalNode g = goalIter.next();
Value eval = evaluate(g, guard);
if (eval.getData().equals(true)) {
forCase.add(g);
}
}
copiedList.removeAll(forCase);
goalsAfterCases.addAll(executeCase(body, forCase));
}
*/
//for all remaining goals execute default //for all remaining goals execute default
if (!copiedList.isEmpty()) { if (!remainingGoalsSet.isEmpty()) {
VariableAssignment va = new VariableAssignment();
Statements defaultCase = casesStatement.getDefaultCase(); Statements defaultCase = casesStatement.getDefaultCase();
goalsAfterCases.addAll(executeCase(defaultCase, copiedList)); for (GoalNode goal : remainingGoalsSet) {
goalsAfterCases.addAll(executeBody(defaultCase, goal, va).getGoals());
}
} }
...@@ -205,7 +182,7 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -205,7 +182,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
State newStateAfterCases; State newStateAfterCases;
if (!goalsAfterCases.isEmpty()) { if (!goalsAfterCases.isEmpty()) {
goalsAfterCases.forEach(node -> node.exitNewVarScope()); //goalsAfterCases.forEach(node -> node.exitNewVarScope());
if (goalsAfterCases.size() == 1) { if (goalsAfterCases.size() == 1) {
newStateAfterCases = new State(goalsAfterCases, goalsAfterCases.get(0)); newStateAfterCases = new State(goalsAfterCases, goalsAfterCases.get(0));
...@@ -226,7 +203,7 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -226,7 +203,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
* @param aCase * @param aCase
* @return * @return
*/ */
private Map<GoalNode, VariableAssignment> matchGoal(Set<GoalNode> allGoalsBeforeCases, CaseStatement aCase) { private Map<GoalNode, VariableAssignment> matchGoal(Collection<GoalNode> allGoalsBeforeCases, CaseStatement aCase) {
HashMap<GoalNode, VariableAssignment> matchedGoals = new HashMap<>(); HashMap<GoalNode, VariableAssignment> matchedGoals = new HashMap<>();
Expression matchExpression = aCase.getGuard(); Expression matchExpression = aCase.getGuard();
...@@ -281,23 +258,18 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -281,23 +258,18 @@ public class Interpreter extends DefaultASTVisitor<Void>
/** /**
* For each selected goal put a state onto the stack and visit the body of the case * For each selected goal put a state onto the stack and visit the body of the case
* * @param
* @param
* @param caseStmts * @param caseStmts
* @param goalsToApply @return * @param goalsToApply @return
*/ */
private List<GoalNode> executeCase(Statements caseStmts, Set<GoalNode> goalsToApply) { private List<GoalNode> executeCase(Statements caseStmts, Map<GoalNode, VariableAssignment> goalsToApply) {
enterScope(caseStmts); enterScope(caseStmts);
List<GoalNode> goalsAfterCases = new ArrayList<>(); List<GoalNode> goalsAfterCases = new ArrayList<>();
for (GoalNode next : goalsToApply) { for (Map.Entry<GoalNode, VariableAssignment> next : goalsToApply.entrySet()) {
List<GoalNode> goalList = new ArrayList<>();
goalList.add(next); AbstractState s = executeBody(caseStmts, next.getKey(), next.getValue());
State s = new State(goalList, next); goalsAfterCases.addAll(s.getGoals());
stateStack.push(s);
caseStmts.accept(this);
State aftercase = (State) stateStack.pop();
goalsAfterCases.addAll(aftercase.getGoals());
} }
exitScope(caseStmts); exitScope(caseStmts);
return goalsAfterCases; return goalsAfterCases;
...@@ -305,6 +277,15 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -305,6 +277,15 @@ public class Interpreter extends DefaultASTVisitor<Void>
} }
private AbstractState executeBody(Statements caseStmts, GoalNode goalNode, VariableAssignment va) {
goalNode.enterNewVarScope(va);
AbstractState s = newState(goalNode);
caseStmts.accept(this);
popState(s);
return s;
}
/** /**
* @param caseStatement * @param caseStatement
* @return * @return
......
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.*; import de.uka.ilkd.key.api.ProofManagementApi;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import edu.kit.formal.interpreter.funchdl.BuiltinCommands; import edu.kit.formal.interpreter.funchdl.BuiltinCommands;
import edu.kit.formal.interpreter.funchdl.DefaultLookup; import edu.kit.formal.interpreter.funchdl.DefaultLookup;
import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.Facade;
...@@ -10,9 +8,7 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript; ...@@ -10,9 +8,7 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.util.HashMap;
import java.util.List; import java.util.List;
import java.util.Map;
/** /**
* Test Main, will be replaced * Test Main, will be replaced
...@@ -24,13 +20,15 @@ public class Main { ...@@ -24,13 +20,15 @@ public class Main {
private static File testFile1 = new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/proofscriptparser/scripts/contraposition.key"); private static File testFile1 = new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/proofscriptparser/scripts/contraposition.key");
public static void main(String[] args) { public static void main(String[] args) {
try { /*try {
System.out.println(testFile1.exists()); System.out.println(testFile1.exists());
api = KeYApi.loadFromKeyFile(testFile1); api = KeYApi.loadFromKeyFile(testFile1);
ProofApi papi = api.getLoadedProof(); ProofApi papi = api.getLoadedProof();
ScriptApi scrapi = papi.getScriptApi(); ScriptApi scrapi = papi.getScriptApi();
System.out.println(papi.getFirstOpenGoal().getSequent().toString()); */
/*System.out.println(papi.getFirstOpenGoal().getSequent().toString());
ProjectedNode openGoal = papi.getFirstOpenGoal(); ProjectedNode openGoal = papi.getFirstOpenGoal();
RuleCommand rc = (RuleCommand) KeYApi.getScriptCommandApi().getScriptCommands("rule"); RuleCommand rc = (RuleCommand) KeYApi.getScriptCommandApi().getScriptCommands("rule");
Map cArgs = new HashMap(); Map cArgs = new HashMap();
...@@ -51,13 +49,13 @@ public class Main { ...@@ -51,13 +49,13 @@ public class Main {
} else { } else {
List<VariableAssignments> matches2 = scrapi.matchPattern("==> X -> Y", openGoal.getSequent(), va2); List<VariableAssignments> matches2 = scrapi.matchPattern("==> X -> Y", openGoal.getSequent(), va2);
} }*/
} catch (ProblemLoaderException e) { /* } catch (ProblemLoaderException e) {
System.out.println("Could not load file"); System.out.println("Could not load file");
e.printStackTrace(); e.printStackTrace();
} catch (Exception e) { } catch (Exception e) {
e.printStackTrace(); e.printStackTrace();
} }*/
//Erzeuge Parser //Erzeuge Parser
//lese P ein //lese P ein
//Erzeuge Interpreter //Erzeuge Interpreter
......
...@@ -7,6 +7,7 @@ import edu.kit.formal.proofscriptparser.ast.*; ...@@ -7,6 +7,7 @@ import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter; import lombok.Getter;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.Collections;
import java.util.List; import java.util.List;
/** /**
...@@ -68,16 +69,43 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -68,16 +69,43 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
return evaluatedExpression; return evaluatedExpression;
} }
/**
* TODO rethink
*
* @param op
* @param v1
* @param v2
* @return
*/
private List<VariableAssignment> evaluateExpression(Operator op, List<VariableAssignment> v1, List<VariableAssignment> v2) { private List<VariableAssignment> evaluateExpression(Operator op, List<VariableAssignment> v1, List<VariableAssignment> v2) {
switch (op) { switch (op) {
case AND: case AND:
return joinLists(v1, v2); return joinLists(v1, v2);
case OR:
return orList(v1, v2);
case EQ:
return joinLists(v1, v2);
case NEQ:
return null;
default: default:
System.out.println("Need to be installed"); System.out.println("Need to be implemented");
} }
return null; return null;
} }
/**
* TODO rethink decision: atm. if the first list is true/not empty (but may contain amepty assignment) this is returned
* This decision also results that if a binary expression without a match is printed first, it is the winning assignment
* Importance of match is decreased with this decision
*
* @param v1
* @param v2
* @return
*/
private List<VariableAssignment> orList(List<VariableAssignment> v1, List<VariableAssignment> v2) {
return (v1.isEmpty()) ? v2 : v1;
}
/** /**
* If two matching results are conjunctively joined only variable assignments that are compatible with each other can be chosen. * If two matching results are conjunctively joined only variable assignments that are compatible with each other can be chosen.
* *
...@@ -121,30 +149,18 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -121,30 +149,18 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
public List<VariableAssignment> visit(MatchExpression match) { public List<VariableAssignment> visit(MatchExpression match) {
List<VariableAssignments> resultOfMatch; List<VariableAssignments> resultOfMatch;
//TODO transform assignments //TODO transform assignments
Value pattern = (Value) match.getPattern().accept(this); Value pattern = (Value) eval.eval(match.getPattern());
// Value pattern = (Value) match.getPattern().accept(this);
List<VariableAssignment> va = null; List<VariableAssignment> va = null;
if (pattern.getType() == Type.STRING) { if (pattern.getType() == Type.STRING) {
va = getMatcher().matchLabel(goal, (String) pattern.getData()); va = getMatcher().matchLabel(goal, (String) pattern.getData());
} else if (pattern.getType() == Type.TERM) { } else if (pattern.getType() == Type.TERM) {
va = getMatcher().matchSeq(goal, (String) pattern.getData()); va = getMatcher().matchSeq(goal, (String) pattern.getData(), match.getSignature());
} }
return va != null ? va : new ArrayList<>(); return va != null ? va : Collections.emptyList();
} }
/**
* @param
* @return
*/
/* @Override
public List<VariableAssignment> visit(TermLiteral term) {
return null;
}*/
/* @Override
public List<VariableAssignment> visit(StringLiteral string) {
return Value.from(string);
}*/
@Override @Override
public List<VariableAssignment> visit(Variable variable) { public List<VariableAssignment> visit(Variable variable) {
//get variable value //get variable value
...@@ -159,17 +175,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -159,17 +175,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
} }
/* @Override
public List<VariableAssignment> visit(BooleanLiteral bool) {
return bool.isValue() ? Value.TRUE : Value.FALSE;
}
@Override
public List<VariableAssignment> visit(IntegerLiteral integer) {
return Value.from(integer);
}
*/
@Override @Override
public List<VariableAssignment> visit(UnaryExpression e) { public List<VariableAssignment> visit(UnaryExpression e) {
Operator op = e.getOperator(); Operator op = e.getOperator();
......
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.ast.Signature;
import java.util.List; import java.util.List;
/** /**
...@@ -8,5 +10,6 @@ import java.util.List; ...@@ -8,5 +10,6 @@ import java.util.List;
*/ */
public interface MatcherApi { public interface MatcherApi {
List<VariableAssignment> matchLabel(GoalNode currentState, String label); List<VariableAssignment> matchLabel(GoalNode currentState, String label);
List<VariableAssignment> matchSeq(GoalNode currentState, String data);
List<VariableAssignment> matchSeq(GoalNode currentState, String data, Signature sig);
} }
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.ast.BooleanLiteral; import edu.kit.formal.proofscriptparser.ast.*;
import edu.kit.formal.proofscriptparser.ast.IntegerLiteral;
import edu.kit.formal.proofscriptparser.ast.StringLiteral;
import edu.kit.formal.proofscriptparser.ast.Type;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
...@@ -51,6 +48,14 @@ public class Value<T> { ...@@ -51,6 +48,14 @@ public class Value<T> {
return new Value<>(Type.INT, apply); return new Value<>(Type.INT, apply);
} }
public static Value<String> from(String s) {
return new Value<>(Type.STRING, s);
}
public static Value<String> from(TermLiteral term) {
return new Value<>(Type.TERM, term.getText());
}
@Override @Override
public boolean equals(Object o) { public boolean equals(Object o) {
if (this == o) return true; if (this == o) return true;
...@@ -73,8 +78,4 @@ public class Value<T> { ...@@ -73,8 +78,4 @@ public class Value<T> {
public String toString() { public String toString() {
return data + ":" + type; return data + ":" + type;
} }
public static Value<String> from(String s) {
return new Value<>(Type.STRING, s);
}
}