Commit 1bfc2b02 authored by Sarah Grebing's avatar Sarah Grebing

Merge branch 'master' into gradle

parents 5376686a 0f340c93
......@@ -23,16 +23,16 @@ public class Utils {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") -> (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Junctor.AND)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") && (" + toPrettyTerm(formula.sub(1)) + ")");
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") & (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Junctor.OR)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") || (" + toPrettyTerm(formula.sub(1)) + ")");
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") | (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Equality.EQV)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") <-> (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Equality.EQUALS)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") == (" + toPrettyTerm(formula.sub(1)) + ")");
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") = (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Junctor.NOT)) {
sb.append("(!" + toPrettyTerm(formula.sub(0)) + ")");
......
......@@ -85,11 +85,29 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
}
//initialize environment variables
for (VariableAssignmentHook<T> hook : variableHooks) {
VariableAssignment va = hook.getStartAssignment(getSelectedNode().getData());
getSelectedNode().setAssignments(
getSelectedNode().getAssignments().push(va));
if(getSelectedNode() != null) {
//initialize environment variables
for (VariableAssignmentHook<T> hook : variableHooks) {
VariableAssignment va = hook.getStartAssignment(getSelectedNode().getData());
getSelectedNode().setAssignments(
getSelectedNode().getAssignments().push(va));
}
} else {
List<GoalNode<T>> currentgoals = getCurrentGoals();
logger.info("Loaded Proof with multiple Open Goals");
if (currentgoals.size() == 0) {
logger.debug("Current Goals empty");
return;
}
for (GoalNode<T> goal : currentgoals) {
for (VariableAssignmentHook<T> hook : variableHooks) {
VariableAssignment va = hook.getStartAssignment(goal.getData());
goal.setAssignments(
goal.getAssignments().push(va));
}
}
}
script.accept(this);
//exitScope(script);
......@@ -641,10 +659,26 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
@Override
public Object visit(Signature signature) {
// enterScope(signature);
GoalNode<T> node = getSelectedNode();
node.enterScope();
signature.forEach(node::declareVariable);
// exitScope(signature);
// TODO: quickfix
List<GoalNode<T>> currentGoals = getCurrentGoals();
if(getCurrentGoals().size() > 1) {
if(getSelectedNode() == null) {
for(GoalNode<T> goal: currentGoals) {
goal.enterScope();
signature.forEach(goal::declareVariable);
// exitScope(signature);
}
}
} else {
GoalNode<T> node = getSelectedNode();
node.enterScope();
signature.forEach(node::declareVariable);
// exitScope(signature);
}
return null;
}
......
......@@ -155,7 +155,7 @@ public class InteractiveModeController {
LOGGER.debug("Handling {}", tap);
moreThanOneMatch = false;
String tapName = tap.getApp().taclet().displayName();
String tapName = tap.getApp().taclet().name().toString();
Goal g = tap.getCurrentGoal();
SequentFormula seqForm = tap.getPio().sequentFormula();
......@@ -283,6 +283,7 @@ public class InteractiveModeController {
if (ngoals.size() > 1) {
cases.get(findRoot(ngoals.get(0).node())).add(call);
CasesStatement inner = new CasesStatement();
cases.get(findRoot(ngoals.get(0).node())).add(inner);
......@@ -301,7 +302,7 @@ public class InteractiveModeController {
}
} else {
if (ngoals.size() == 0) {
cases.get(g).add(call);
cases.get(findRoot(expandedNode.getData().getNode())).add(call);
} else {
KeyData kdn = new KeyData(kd, ngoals.get(0).node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
......
......@@ -136,6 +136,7 @@ public class SequentView extends CodeArea {
filter.setSequent(sequent);
ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter());
this.backend = new LogicPrinter.PosTableStringBackend(80);
......
......@@ -21,12 +21,15 @@ script interactive(){
script interactive_with_match(){
impRight;
impRight;
impLeft;
cases{
case match `?X -> ?Y ==> not(?Z)`:
notLeft;
default:
case match `==> not(?Z), ?Z`:
notRight;
default:
notLeft;
}
}
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