001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.visualdebugger;
009:
010: import de.uka.ilkd.key.gui.RuleAppListener;
011: import de.uka.ilkd.key.java.ProgramElement;
012: import de.uka.ilkd.key.java.SourceElement;
013: import de.uka.ilkd.key.logic.*;
014: import de.uka.ilkd.key.logic.op.*;
015: import de.uka.ilkd.key.proof.Node;
016: import de.uka.ilkd.key.proof.ProofEvent;
017: import de.uka.ilkd.key.proof.proofevent.*;
018: import de.uka.ilkd.key.rule.*;
019:
020: public class UpdateLabelListener implements RuleAppListener {
021:
022: public UpdateLabelListener() {
023: }
024:
025: private void analyseNodeChanges(NodeReplacement nr, int id,
026: boolean looking, HashMapFromPosInOccurrenceToLabel labels) {
027: final IteratorOfNodeChange it = nr.getNodeChanges();
028: while (it.hasNext()) {
029: NodeChange nc = it.next();
030: if (nc instanceof NodeChangeAddFormula) {
031: labels.put(((NodeChangeAddFormula) nc).getPos(),
032: new PCLabel(id, looking));
033: } else if (nc instanceof NodeRedundantAddChange) {
034: labels.put(((NodeRedundantAddChange) nc).getPos(),
035: new PCLabel(id, looking));
036: } else if (nc instanceof NodeChangeRemoveFormula) {
037: labels.remove(((NodeChangeRemoveFormula) nc).getPos());
038: }
039:
040: }
041: }
042:
043: private boolean containsIfTerm(Term t) {
044: final OpCollector col = new OpCollector();
045: t.execPreOrder(col);
046: return col.contains(Op.IF_THEN_ELSE);
047: }
048:
049: private boolean inUpdate(PosInOccurrence pio2) {
050: PosInOccurrence pio = pio2;
051: while (!pio.isTopLevel()) {
052: pio = pio.up();
053: if (pio.subTerm().op() instanceof QuanUpdateOperator) {
054: return true;
055: }
056: }
057: return false;
058: }
059:
060: // FIXME: What is a BC Taclet and this broke because of a test of taclets
061: // starting with
062: // inst_ after we have renamed taclets this set of rules changed so that a
063: // replacement
064: // with inst is not possible! Workaround by assumption ...
065: private boolean isBCTaclet(PosTacletApp tap, Node n) {
066:
067: return !(tap.taclet().name().toString().startsWith("instAll") || tap
068: .taclet().name().toString().startsWith("instEx"));
069: }
070:
071: // TODO duplication in prooflistner
072: private boolean isLiteral(PosInOccurrence pio) {
073: Term f = pio.constrainedFormula().formula();
074: Operator op = f.op();
075: if (this .modalityTopLevel(pio)
076: && !this .containsIfTerm(pio.constrainedFormula()
077: .formula()))
078: return true;
079: if (op == Op.AND || op == Op.OR || op == Op.IF_THEN_ELSE
080: || op == Op.IF_EX_THEN_ELSE || op == Op.EQV
081: || op == Op.IMP || op == Op.AND
082: || (op instanceof IUpdateOperator/*
083: * &&
084: * !containsJavaBlock(pio.constrainedFormula().formula()
085: */))
086: return false;
087: final OpCollector col = new OpCollector();
088: f.execPostOrder(col);
089: return !(col.contains(Op.IF_EX_THEN_ELSE) || col
090: .contains(Op.IF_THEN_ELSE));
091: }
092:
093: // TODO in program mod!
094: private boolean modalityTopLevel(PosInOccurrence pio) {
095: Term f = pio.constrainedFormula().formula();
096: if (f.arity() > 0) {
097: Term sub = f.sub(f.arity() - 1);
098: if (sub.op() instanceof Modality)
099: return true;
100: }
101: return false;
102: }
103:
104: public void ruleApplied(ProofEvent e) {
105: RuleAppInfo info = e.getRuleAppInfo();
106: setStepInfos(info);
107: if (info != null) {
108: Node parent = info.getOriginalNode();
109: IteratorOfNodeReplacement it = info.getReplacementNodes();
110: while (it.hasNext()) {
111: NodeReplacement nr = it.next();
112: updateLabels(parent, nr, false);
113: }
114: }
115: }
116:
117: private HashMapFromPosInOccurrenceToLabel setAssumeLabel(
118: HashMapFromPosInOccurrenceToLabel labels, Node n,
119: ListOfIfFormulaInstantiation inst) {
120: HashMapFromPosInOccurrenceToLabel l = labels;
121: if (inst == null) {
122: return l;
123: }
124: IteratorOfIfFormulaInstantiation it = inst.iterator();
125: while (it.hasNext()) {
126: // TODO case assume=find
127: IfFormulaInstantiation next = it.next();
128: if (next instanceof IfFormulaInstSeq) {
129: IfFormulaInstSeq i = (IfFormulaInstSeq) next;
130: PosInOccurrence pio = new PosInOccurrence(i
131: .getConstrainedFormula(), PosInTerm.TOP_LEVEL,
132: i.inAntec());
133:
134: l.put(pio, new PCLabel(-1, false));
135:
136: }
137: }
138: return l;
139: }
140:
141: private void setStepInfos(RuleAppInfo info) {
142: final Node originalNode = info.getOriginalNode();
143: SourceElement actSt = // this.getActStatement(originalNode);
144: VisualDebugger.getVisualDebugger()
145: .determineFirstAndActiveStatement(originalNode);
146: final VisualDebuggerState originalNodeVDS = originalNode
147: .getNodeInfo().getVisualDebuggerState();
148:
149: int newCount = originalNodeVDS.getStatementIdcount();
150: if (VisualDebugger.getVisualDebugger().isSepStatement(
151: (ProgramElement) (actSt))) {
152: newCount--;
153: }
154:
155: final IteratorOfNodeReplacement repl = info
156: .getReplacementNodes();
157: while (repl.hasNext()) {
158: NodeReplacement nr = repl.next();
159: final VisualDebuggerState visualDebuggerState = nr
160: .getNode().getNodeInfo().getVisualDebuggerState();
161: visualDebuggerState.setStatementIdcount(newCount);
162: visualDebuggerState.setStepOver(originalNodeVDS
163: .getStepOver());
164: visualDebuggerState.setStepOverFrom(originalNodeVDS
165: .getStepOverFrom());
166: }
167: }
168:
169: private void updateLabels(Node parent, NodeReplacement nr,
170: boolean impl) {
171: Node n = nr.getNode();
172: int id = -1;
173: boolean looking = false;
174:
175: HashMapFromPosInOccurrenceToLabel labels = (HashMapFromPosInOccurrenceToLabel) parent
176: .getNodeInfo().getVisualDebuggerState().getLabels()
177: .clone();
178:
179: RuleApp app = parent.getAppliedRuleApp();
180:
181: if (app instanceof PosTacletApp) {
182:
183: final PosTacletApp tapp = (PosTacletApp) app;
184: final PosInOccurrence pio = tapp.posInOccurrence()
185: .topLevel();
186:
187: if (labels.containsKey(pio) && isBCTaclet(tapp, parent)) {
188: labels = setAssumeLabel(labels, n, tapp
189: .ifFormulaInstantiations());
190:
191: if (modalityTopLevel(pio) && !inUpdate(pio)) {
192: id = nr.getNode().serialNr();
193: looking = true;
194: } else {
195: id = ((PCLabel) labels.get(pio)).getId();
196: looking = ((PCLabel) labels.get(pio)).isLooking();
197: }
198: analyseNodeChanges(nr, id, looking, labels);
199: }
200: } else {
201: // build in rule
202: if (app.posInOccurrence() != null) {
203: PosInOccurrence pio = app.posInOccurrence().topLevel();
204: if (labels.containsKey(pio)) {
205: id = ((PCLabel) labels.get(pio)).getId();
206: boolean isl = ((PCLabel) labels.get(pio))
207: .isLooking();
208: analyseNodeChanges(nr, id, isl, labels);
209: }
210:
211: }
212: }
213: updateLooking(labels);
214: n.getNodeInfo().getVisualDebuggerState().setLabels(labels);
215: }
216:
217: private void updateLooking(HashMapFromPosInOccurrenceToLabel labels) {
218: boolean removelooking = true;
219:
220: for (IteratorOfPosInOccurrence it = labels.keyIterator(); it
221: .hasNext();) {
222: PosInOccurrence pio = it.next();
223: PCLabel l = (PCLabel) labels.get(pio);
224: if (l.isLooking()) {
225: if (!isLiteral(pio)) {
226: removelooking = false;
227: }
228: }
229: }
230:
231: if (removelooking) {
232: for (IteratorOfPosInOccurrence it = labels.keyIterator(); it
233: .hasNext();) {
234: PosInOccurrence pio = it.next();
235: PCLabel l = (PCLabel) labels.get(pio);
236: l.setLooking(false);
237: }
238: }
239: }
240: }
|