Commit a8009ced authored by Sarah Grebing's avatar Sarah Grebing

Interim

parent 0f0c3f8c
package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.ProjectedNode;
import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.api.VariableAssignments;
import edu.kit.formal.proofscriptparser.ast.Type;
import java.util.List;
import java.util.Map;
/**
* Interface to KeY Matcher Api
*
* @author S. Grebing
*/
public class KeYMatcher implements MatcherApi {
ScriptApi scrapi;
public KeYMatcher(ScriptApi scrapi) {
this.scrapi = scrapi;
}
@Override
public List<VariableAssignment> matchLabel(GoalNode currentState, String label) {
return null;
}
@Override
public List<VariableAssignment> matchSeq(GoalNode currentState, String data) {
VariableAssignment assignments = currentState.getAssignments();
ProjectedNode pNode = currentState.getActualKeYGoalNode();
//Gemeinsame VariableAssignments
//scrapi.matchPattern(data, pNode.getSequent(), assignments);
return null;
}
/**
* Transforms a KeY Variable Assignment into an assignment for the interpreter
*
* @param keyAssignments
* @return
*/
public VariableAssignment from(VariableAssignments keyAssignments) {
VariableAssignment interpreterAssignments = new VariableAssignment(null);
Map<String, VariableAssignments.VarType> keyTypeMap = keyAssignments.getTypeMap();
//find type needs to be rewritten
keyTypeMap.forEach((k, v) -> interpreterAssignments.addVarDecl(k, Type.findType(v.getKeYDeclarationPrefix())));
interpreterAssignments.getTypes().forEach((k, v) -> {
try {
//TODO cast is not valid
interpreterAssignments.setVarValue(k, (Value) keyAssignments.getVarValue(k));
} catch (Exception e) {
e.printStackTrace();
}
});
return interpreterAssignments;
}
}
package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.VariableAssignments;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter;
import java.util.ArrayList;
import java.util.List;
/**
* Evaluator specially for Expressions in a case "declaration".
* Created by sarah on 5/22/17.
*/
public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> implements ScopeObservable {
@Getter
private final GoalNode goal;
private final VariableAssignment state;
@Getter
private MatcherApi matcher;
@Getter
private List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>();
private Evaluator eval;
public MatchEvaluator(VariableAssignment assignment, GoalNode node, MatcherApi matcher) {
state = new VariableAssignment(assignment); // unmodifiable version of assignment
goal = node;
this.matcher = matcher;
this.eval = new Evaluator(assignment, node);
}
/**
* Evaluation of an expression.
*
* @param truth
* @return
*/
public List<VariableAssignment> eval(Expression truth) {
return (List<VariableAssignment>) truth.accept(this);
}
@Override
public List<VariableAssignment> visit(BinaryExpression e) {
List<VariableAssignment> left = decideEvaluatorAndEvaluate(e.getLeft());
List<VariableAssignment> right = decideEvaluatorAndEvaluate(e.getRight());
Operator op = e.getOperator();
return evaluateExpression(op, left, right);
}
/**
* Decide whether to evaluate using the MatchEvaluator or the standard evaluator depending on the content of the expression
*
* @param e
* @return
*/
private List<VariableAssignment> decideEvaluatorAndEvaluate(Expression e) {
List<VariableAssignment> evaluatedExpression;
if (!e.hasMatchExpression()) {
Value v = (Value) eval(e);
evaluatedExpression = transformTruthValue(v);
} else {
evaluatedExpression = (List<VariableAssignment>) e.accept(this);
}
return evaluatedExpression;
}
private List<VariableAssignment> evaluateExpression(Operator op, List<VariableAssignment> v1, List<VariableAssignment> v2) {
switch (op) {
case AND:
return joinLists(v1, v2);
default:
System.out.println("Need to be installed");
}
return null;
}
/**
* If two matching results are conjunctively joined only variable assignments that are compatible with each other can be chosen.
*
* @param v1
* @param v2
* @return an empty list means false, a list with an assignment means true
*/
private List<VariableAssignment> joinLists(List<VariableAssignment> v1, List<VariableAssignment> v2) {
if (v1.isEmpty() || v2.isEmpty()) {
return v1;
}
List<VariableAssignment> compatible = new ArrayList<>();
for (VariableAssignment variableAssignment1 : v1) {
List<VariableAssignment> compatibleAssignment = checkForCompatibleAssignment(variableAssignment1, v2);
if (!compatibleAssignment.isEmpty()) {
compatible.addAll(compatibleAssignment);
}
}
return compatible;
}
private List<VariableAssignment> checkForCompatibleAssignment(VariableAssignment variableAssignment1, List<VariableAssignment> v2) {
List<VariableAssignment> compatibleAssignments = new ArrayList<>();
for (VariableAssignment variableAssignment2 : v2) {
VariableAssignment assignment = variableAssignment1.joinWithCheck(variableAssignment2);
//check whether an empty assignment was returned, then the join was unsuccessful
if (!assignment.isEmpty()) {
compatibleAssignments.add(assignment);
}
}
return compatibleAssignments;
}
/**
* @param match
* @return
*/
@Override
public List<VariableAssignment> visit(MatchExpression match) {
List<VariableAssignments> resultOfMatch;
//TODO transform assignments
Value pattern = (Value) match.getPattern().accept(this);
List<VariableAssignment> va = null;
if (pattern.getType() == Type.STRING) {
va = getMatcher().matchLabel(goal, (String) pattern.getData());
} else if (pattern.getType() == Type.TERM) {
va = getMatcher().matchSeq(goal, (String) pattern.getData());
}
return va != null ? va : new ArrayList<>();
}
/**
* @param
* @return
*/
/* @Override
public List<VariableAssignment> visit(TermLiteral term) {
return null;
}*/
/* @Override
public List<VariableAssignment> visit(StringLiteral string) {
return Value.from(string);
}*/
@Override
public List<VariableAssignment> visit(Variable variable) {
//get variable value
String id = variable.getIdentifier();
Value v = state.lookupVarValue(id);
if (v != null) {
// return v;
return null;
} else {
throw new RuntimeException("Variable " + variable + " was not initialized");
}
}
/* @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
public List<VariableAssignment> visit(UnaryExpression e) {
Operator op = e.getOperator();
Expression expr = e.getExpression();
Value exValue = (Value) expr.accept(this);
Value ret = op.evaluate(exValue);
return null;
}
// public List<VariableAssignment> getMatchedVariables() {
// return null;
// }
/**
* Transforms a truth value to its representation as list:
* If the value is true this method returns a list with an empty assignment
* If the value is false this method returns an empty list
*
* @param v
* @return
*/
public List<VariableAssignment> transformTruthValue(Value v) {
if (v.getType().equals(Type.BOOL)) {
List<VariableAssignment> transformedValue = new ArrayList<>();
if (v.getData().equals(Value.TRUE)) {
transformedValue.add(new VariableAssignment(null));
}
return transformedValue;
} else {
throw new RuntimeException("This type " + v.getType() + " can not be transformed into a truth value");
}
}
}
......@@ -49,20 +49,6 @@ public class VariableAssignment {
}
}
/* public VariableAssignment copy() {
VariableAssignment copy;
if (parent != null) {
copy = new VariableAssignment(this.parent.copy());
} else {
copy = new VariableAssignment(null);
}
//TODO
//copy.setValues(deepcopy of values);
//deepcopy types
return copy;
}
*/
/**
* Lookup value of variable also in parent assignments
......@@ -160,7 +146,8 @@ public class VariableAssignment {
/**
* @param assignment
* @return empty variable assignment if not possible to join conflictfree (i.e., if a variable name is present in both assignments with different types or dfferent values)
* @return empty variable assignment if not possible to join conflictfree (i.e., if a variable name is present
* in both assignments with different types or dfferent values) the join otherwise
* @throws RuntimeException
*/
public VariableAssignment joinWithCheck(VariableAssignment assignment) throws RuntimeException {
......@@ -180,6 +167,11 @@ public class VariableAssignment {
return this.joinWithoutCheck(assignment);
}
/**
* checks whether an assignment is empty i.e. does not contain type declarations and values
*
* @return
*/
public boolean isEmpty() {
if (this.getValues().isEmpty() && this.parent != null) {
return this.getParent().isEmpty();
......
package edu.kit.formal.interpreter;
import edu.kit.formal.ScopeLogger;
import edu.kit.formal.dbg.Debugger;
import edu.kit.formal.interpreter.funchdl.BuiltinCommands;
import edu.kit.formal.interpreter.funchdl.CommandLookup;
......@@ -53,6 +52,11 @@ public class InterpreterTest {
Assert.assertEquals(10, i.getCurrentState().getGoals().size());
}
@Test
public void testSimple2() throws IOException {
Interpreter inter = execute(getClass().getResourceAsStream("testSimple2.txt"));
// Assert.assertSame(0, ((BigInteger) inter.getCurrentState().getGoals().get(0).getAssignments().lookupVarValue("j").getData()).intValue());
}
@Test
public void testInclude() throws IOException {
......
package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.ast.Type;
import org.junit.Before;
import java.util.Collections;
import java.util.List;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
/**
* Created by sarah on 5/23/17.
*/
public class MatchEvaluatorTest {
MatchEvaluator mEval;
public MatchEvaluatorTest() {
}
@Before
public void setup() {
GoalNode parent = new GoalNode(null, "pa");
parent.addVarDecl("a", Type.INT);
parent.addVarDecl("b", Type.INT);
VariableAssignment va = parent.getAssignments();
va.setVarValue("a", Value.from(1));
va.setVarValue("b", Value.from(1));
GoalNode selected = new GoalNode(parent, "selg");
mEval = new MatchEvaluator(va, selected, new PseudoMatcher());
//eval = new Evaluator(selected.getAssignments(), selected);
//eval.setMatcher(new PseudoMatcher());
}
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();
}
}
}
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