Commit 2442bfd7 authored by Alexander Weigl's avatar Alexander Weigl

Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser

* 'master' of git.scc.kit.edu:xt9634/ProofScriptParser:
  adderd flag for matchexpreesion
parents a46bfed6 8feff6db
Pipeline #10678 failed with stage
in 1 minute and 6 seconds
...@@ -97,41 +97,6 @@ ...@@ -97,41 +97,6 @@
<visitor>true</visitor> <visitor>true</visitor>
</configuration> </configuration>
</plugin> </plugin>
<!--<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-install-plugin</artifactId>
<version>2.5</version>
<executions>
<execution>
<id>keyinstall</id>
<phase>initialize</phase>
<goals>
<goal>install-file</goal>
</goals>
<configuration>
<groupId>org.key-project</groupId>
<artifactId>key.core</artifactId>
<version>2.7</version>
<packaging>jar</packaging>
<file>${basedir}/lib/key.core.jar</file>
</configuration>
</execution>
<execution>
<id>recoderinstall</id>
<phase>initialize</phase>
<goals>
<goal>install-file</goal>
</goals>
<configuration>
<groupId>org.key-project</groupId>
<artifactId>recoderKey</artifactId>
<version>1.0.0</version>
<packaging>jar</packaging>
<file>${basedir}/lib/recoderKey.jar</file>
</configuration>
</execution>
</executions>
</plugin>-->
</plugins> </plugins>
</build> </build>
......
...@@ -45,7 +45,6 @@ public class Debugger { ...@@ -45,7 +45,6 @@ public class Debugger {
interpreter.getEntryListeners().add(history); interpreter.getEntryListeners().add(history);
interpreter.getEntryListeners().add(blocker); interpreter.getEntryListeners().add(blocker);
interpreter.getEntryListeners().add(new CommandLogger()); interpreter.getEntryListeners().add(new CommandLogger());
//TODO install debugger functions
registerDebuggerFunction("step", this::step); registerDebuggerFunction("step", this::step);
registerDebuggerFunction("b", this::setBreakpoint); registerDebuggerFunction("b", this::setBreakpoint);
...@@ -56,6 +55,11 @@ public class Debugger { ...@@ -56,6 +55,11 @@ public class Debugger {
registerDebuggerFunction("status", this::status); registerDebuggerFunction("status", this::status);
} }
public static void main(String[] args) throws IOException {
Debugger d = new Debugger("src/test/resources/edu/kit/formal/interpreter/dbg.kps");
d.run();
}
private void registerDebuggerFunction(final String step, private void registerDebuggerFunction(final String step,
BiConsumer<CallStatement, VariableAssignment> func) { BiConsumer<CallStatement, VariableAssignment> func) {
debuggerFunctions.getBuilders().add(new CommandHandler() { debuggerFunctions.getBuilders().add(new CommandHandler() {
...@@ -71,11 +75,6 @@ public class Debugger { ...@@ -71,11 +75,6 @@ public class Debugger {
}); });
} }
public static void main(String[] args) throws IOException {
Debugger d = new Debugger("src/test/resources/edu/kit/formal/interpreter/dbg.kps");
d.run();
}
private void run() throws IOException { private void run() throws IOException {
blocker.stepUntilBlock.set(2); blocker.stepUntilBlock.set(2);
interpreterThread = new Thread(() -> { interpreterThread = new Thread(() -> {
......
...@@ -7,6 +7,7 @@ import lombok.Getter; ...@@ -7,6 +7,7 @@ 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;
/** /**
......
...@@ -10,21 +10,36 @@ import lombok.Getter; ...@@ -10,21 +10,36 @@ import lombok.Getter;
* @author S.Grebing * @author S.Grebing
*/ */
public class GoalNode { public class GoalNode {
//TODO this is only for testing, later Sequent object or similar
@Getter @Getter
private String sequent; private String sequent; //TODO this is only for testing, when connected with key using projectednode
private VariableAssignment assignments; private VariableAssignment assignments;
private GoalNode parent; private GoalNode parent;
@Getter
private ProjectedNode actualKeYGoalNode;
/**
* This conctructur will be replaced with concrete one that uses projectedNode
*
* @param parent
* @param seq
*/
public GoalNode(GoalNode parent, String seq) { public GoalNode(GoalNode parent, String seq) {
//BUG: Hier muesste deepcopy der assignments passieren //BUG: Hier muesste deepcopy der assignments passieren
this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments()); this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments());
this.parent = parent; this.parent = parent;
this.sequent = seq; this.sequent = seq;
actualKeYGoalNode = null;
} }
public GoalNode(GoalNode parent, String seq, ProjectedNode pNode) {
this.actualKeYGoalNode = pNode;
this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments());
this.parent = parent;
this.sequent = seq;
}
private VariableAssignment deepCopyAssignments() { private VariableAssignment deepCopyAssignments() {
return assignments.deepCopy(); return assignments.deepCopy();
} }
......
...@@ -4,7 +4,6 @@ import edu.kit.formal.proofscriptparser.DefaultASTVisitor; ...@@ -4,7 +4,6 @@ import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.ASTNode; import edu.kit.formal.proofscriptparser.ast.ASTNode;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import lombok.Setter;
import java.util.LinkedList; import java.util.LinkedList;
import java.util.List; import java.util.List;
...@@ -28,4 +27,6 @@ public class HistoryListener extends DefaultASTVisitor<Void> { ...@@ -28,4 +27,6 @@ public class HistoryListener extends DefaultASTVisitor<Void> {
queueNode.add(node); queueNode.add(node);
return null; return null;
} }
} }
...@@ -2,12 +2,14 @@ package edu.kit.formal.interpreter; ...@@ -2,12 +2,14 @@ package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.EngineState;
import edu.kit.formal.interpreter.funchdl.CommandCall;
import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.interpreter.funchdl.CommandLookup;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter; import lombok.Getter;
import lombok.Setter; import lombok.Setter;
import org.antlr.v4.runtime.ParserRuleContext;
import java.util.*; import java.util.*;
import java.util.logging.Logger; import java.util.logging.Logger;
...@@ -19,6 +21,7 @@ import java.util.logging.Logger; ...@@ -19,6 +21,7 @@ import java.util.logging.Logger;
*/ */
public class Interpreter extends DefaultASTVisitor<Void> public class Interpreter extends DefaultASTVisitor<Void>
implements ScopeObservable { implements ScopeObservable {
private static final int MAX_ITERATIONS = 5;
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes) //TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
private Stack<AbstractState> stateStack = new Stack<>(); private Stack<AbstractState> stateStack = new Stack<>();
private static Logger logger = Logger.getLogger("interpreter"); private static Logger logger = Logger.getLogger("interpreter");
...@@ -160,77 +163,80 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -160,77 +163,80 @@ public class Interpreter extends DefaultASTVisitor<Void>
@Override @Override
public Void visit(CasesStatement casesStatement) { public Void visit(CasesStatement casesStatement) {
enterScope(casesStatement); enterScope(casesStatement);
AbstractState beforeCases = stateStack.pop();
List<GoalNode> allGoalsBeforeCases = beforeCases.getGoals();
//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> currentGoals = new HashSet<>(getCurrentGoals()); Set<GoalNode> copiedList = new HashSet<>(allGoalsBeforeCases);
//List<Map<GoalNode, VariableAssignment>> matchedGoals = new ArrayList<>();
//handle cases
List<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) {
Map<GoalNode, VariableAssignment> matchedGoals = matchGoal(copiedList, aCase);
if (matchedGoals != null) {
copiedList.removeAll(matchedGoals.entrySet());
goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals.keySet()));
}
for (CaseStatement currentCase : casesStatement.getCases()) {
//calculate the goal nodes activations
Map<GoalNode, VariableAssignment> mg = getMatchedGoal(currentGoals, currentCase);
//matchedGoals.add(mg);
currentGoals.removeAll(mg.keySet());
// execute }
for (Map.Entry<GoalNode, VariableAssignment> s : mg.entrySet()) {
enterScope(currentCase); /* Iterator<CaseStatement> casesIter = cases.iterator();
executeStatements(currentCase.getBody(), s.getKey(), s.getValue()); while (casesIter.hasNext()) {
exitScope(currentCase);
//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
if (!copiedList.isEmpty()) {
Statements defaultCase = casesStatement.getDefaultCase();
goalsAfterCases.addAll(executeCase(defaultCase, copiedList));
// execute
for (GoalNode s : currentGoals) {
executeStatements(casesStatement.getDefaultCase(), s, new VariableAssignment());
} }
/*/exit scope and create a new state using the union of all newly created goals //exit scope and create a new state using the union of all newly created goals
State newStateAfterCases; State newStateAfterCases;
if (!goalsAfterCases.isEmpty()) { if (!goalsAfterCases.isEmpty()) {
for (GoalNode goalAfterCases : goalsAfterCases) { goalsAfterCases.forEach(node -> node.exitNewVarScope());
goalAfterCases.exitNewVarScope();
}
if (goalsAfterCases.size() == 1) { if (goalsAfterCases.size() == 1) {
newStateAfterCases = new State(goalsAfterCases, goalsAfterCases.get(0)); newStateAfterCases = new State(goalsAfterCases, goalsAfterCases.get(0));
} else { } else {
newStateAfterCases = new State(goalsAfterCases, null); newStateAfterCases = new State(goalsAfterCases, null);
} }
stateStack.push(newStateAfterCases); stateStack.push(newStateAfterCases);
}*/ }
exitScope(casesStatement); exitScope(casesStatement);
return null; return null;
} }
public void executeStatements(Statements currentCase, GoalNode gn, VariableAssignment va) {
enterScope(currentCase);
AbstractState ns = newState(gn);
ns.getSelectedGoalNode().enterNewVarScope(va);
currentCase.accept(this);
mergeGoalsAndPop(ns, gn);
exitScope(currentCase);
}
private void mergeGoalsAndPop(AbstractState ns, GoalNode toRemoved) {
AbstractState popped = popState();
assert popped == ns;
getCurrentState().getGoals().remove(toRemoved);
getCurrentState().getGoals().addAll(popped.getGoals());
}
private Map<GoalNode, VariableAssignment> getMatchedGoal(Collection<GoalNode> currentGoals,
CaseStatement currentCase) {
Map<GoalNode, VariableAssignment> map = new HashMap<>();
for (GoalNode gn : currentGoals) {
VariableAssignment va = evaluateWithAssignments(gn, currentCase.getGuard());
if (va != null)
map.put(gn, va);
}
return map;
}
/** /**
* @param caseStatement * @param caseStatement
...@@ -325,8 +331,10 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -325,8 +331,10 @@ public class Interpreter extends DefaultASTVisitor<Void>
@Override @Override
public Void visit(RepeatStatement repeatStatement) { public Void visit(RepeatStatement repeatStatement) {
enterScope(repeatStatement); enterScope(repeatStatement);
int counter = 0;
boolean b = false; boolean b = false;
do { do {
counter++;
AbstractState prev = getCurrentState(); AbstractState prev = getCurrentState();
repeatStatement.getBody().accept(this); repeatStatement.getBody().accept(this);
AbstractState end = getCurrentState(); AbstractState end = getCurrentState();
...@@ -334,6 +342,7 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -334,6 +342,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
Set<GoalNode> prevNodes = new HashSet<>(prev.getGoals()); Set<GoalNode> prevNodes = new HashSet<>(prev.getGoals());
Set<GoalNode> endNodes = new HashSet<>(end.getGoals()); Set<GoalNode> endNodes = new HashSet<>(end.getGoals());
b = prevNodes.equals(endNodes); b = prevNodes.equals(endNodes);
b = b && counter <= MAX_ITERATIONS;
} while (b); } while (b);
exitScope(repeatStatement); exitScope(repeatStatement);
return null; return null;
...@@ -363,6 +372,12 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -363,6 +372,12 @@ public class Interpreter extends DefaultASTVisitor<Void>
return getCurrentGoals().get(0); return getCurrentGoals().get(0);
} }
} }
/* @Override
public T visit(Parameters parameters) {
parameters.entrySet();
System.out.println("Params " + parameters.toString());
return null;
}*/
public AbstractState getCurrentState() { public AbstractState getCurrentState() {
return stateStack.peek(); return stateStack.peek();
......
...@@ -3,7 +3,10 @@ package edu.kit.formal.interpreter; ...@@ -3,7 +3,10 @@ package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.ast.Type; import edu.kit.formal.proofscriptparser.ast.Type;
import java.util.HashMap; import java.util.HashMap;
import java.util.HashSet;
import java.util.Map; import java.util.Map;
import java.util.Set;
import java.util.stream.Collectors;
/** /**
* Variable Assignments for each goal node * Variable Assignments for each goal node
...@@ -143,10 +146,43 @@ public class VariableAssignment { ...@@ -143,10 +146,43 @@ public class VariableAssignment {
return asMap(new HashMap<>()); return asMap(new HashMap<>());
} }
public VariableAssignment push(VariableAssignment va) { /**
VariableAssignment p = push(); * Method joins two variable assignments without checking their compatibility
p.values.putAll(va.values); *
p.types.putAll(va.types); * @param assignment
return p; * @return
*/
public VariableAssignment joinWithoutCheck(VariableAssignment assignment) {
this.getValues().putAll(assignment.getValues());
this.getTypes().putAll(assignment.getTypes());
return this;
}
/**
* @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)
* @throws RuntimeException
*/
public VariableAssignment joinWithCheck(VariableAssignment assignment) throws RuntimeException {
Set<String> namesV2 = assignment.getValues().keySet();
Set<String> nonConflicting = new HashSet<>();
Set<String> conflictingCand = new HashSet<>();
//subtract V2 from V1 and add the nonconflicting varNames into the nonconflicting set
nonConflicting = this.getValues().keySet().stream().filter(item -> !namesV2.contains(item)).collect(Collectors.toSet());
//subtract V1 from V2 and add the nonconflicting varNames into the nonconflicting set
nonConflicting.addAll(namesV2.stream().filter(item -> !this.getValues().keySet().contains(item)).collect(Collectors.toSet()));
//create intersection
conflictingCand = this.getValues().keySet().stream().filter(item -> namesV2.contains(item)).collect(Collectors.toSet());
if (!conflictingCand.isEmpty()) {
for (String s : conflictingCand) {
if (!this.lookupVarValue(s).equals(assignment.lookupVarValue(s))) {
return new VariableAssignment(null);
}
}
}
return this.joinWithoutCheck(assignment);
} }
} }
...@@ -75,6 +75,11 @@ public class BinaryExpression extends Expression<ParserRuleContext> { ...@@ -75,6 +75,11 @@ public class BinaryExpression extends Expression<ParserRuleContext> {
return operator.returnType(); return operator.returnType();
} }
@Override
public boolean hasMatchExpression() {
return left.hasMatchExpression() || right.hasMatchExpression();
}
/** /**
* {@inheritDoc} * {@inheritDoc}
*/ */
......
...@@ -65,6 +65,11 @@ public class BooleanLiteral extends Literal { ...@@ -65,6 +65,11 @@ public class BooleanLiteral extends Literal {
return visitor.visit(this); return visitor.visit(this);
} }
@Override
public boolean hasMatchExpression() {
return false;
}
/** /**
* {@inheritDoc} * {@inheritDoc}
*/ */
......
...@@ -34,6 +34,24 @@ import org.antlr.v4.runtime.ParserRuleContext; ...@@ -34,6 +34,24 @@ import org.antlr.v4.runtime.ParserRuleContext;
* @version 1 (28.04.17) * @version 1 (28.04.17)
*/ */
public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T> { public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T> {
/**
* @param type
* @param e
* @param signature
* @throws NotWelldefinedException
*/
public static final void checkType(Type type, Expression e, Signature signature) throws NotWelldefinedException {
Type got = e.getType(signature);
if (!type.equals(got)) {
throw new NotWelldefinedException("Typemismatch in expected " + type + ", got" + got, e);
}
}
/**
* @return returns true if a child expression contains a match expression
*/
public abstract boolean hasMatchExpression();
/** /**
* Returns the precedence of the operator expression. * Returns the precedence of the operator expression.
* <p> * <p>
...@@ -54,17 +72,4 @@ public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T> ...@@ -54,17 +72,4 @@ public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T>
*/ */
public abstract Type getType(Signature signature) public abstract Type getType(Signature signature)
throws NotWelldefinedException; throws NotWelldefinedException;
/**
* @param type
* @param e
* @param signature
* @throws NotWelldefinedException
*/
public static final void checkType(Type type, Expression e, Signature signature) throws NotWelldefinedException {
Type got = e.getType(signature);
if (!type.equals(got)) {
throw new NotWelldefinedException("Typemismatch in expected " + type + ", got" + got, e);
}
}
} }
...@@ -59,6 +59,11 @@ public class IntegerLiteral extends Literal { ...@@ -59,6 +59,11 @@ public class IntegerLiteral extends Literal {
return visitor.visit(this); return visitor.visit(this);
} }
@Override
public boolean hasMatchExpression() {
return false;
}
/** /**
* {@inheritDoc} * {@inheritDoc}
*/ */
......
...@@ -76,6 +76,11 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter ...@@ -76,6 +76,11 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter
return Type.BOOL; return Type.BOOL;
} }
@Override
public boolean hasMatchExpression() {
return true;
}
/** /**
* {@inheritDoc} * {@inheritDoc}
*/ */
......
...@@ -51,6 +51,11 @@ public class StringLiteral extends Literal { ...@@ -51,6 +51,11 @@ public class StringLiteral extends Literal {
return visitor.visit(this); return visitor.visit(this);
} }
@Override
public boolean hasMatchExpression() {