Commit 9398d9ba authored by LULUDBR\Lulu's avatar LULUDBR\Lulu

contraposition skript angepasst

multiple Open Goals Fix
parent ef5271b4
......@@ -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;
}
......
......@@ -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);
......
......@@ -136,6 +136,7 @@ public class SequentView extends CodeArea {
filter.setSequent(sequent);
ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter());
this.backend = new LogicPrinter.PosTableStringBackend(80);
......
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