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: //
009: //
010:
011: package de.uka.ilkd.key.proof.proofevent;
012:
013: import de.uka.ilkd.key.logic.*;
014: import de.uka.ilkd.key.proof.Node;
015:
016: /** Information about a node replacing its parent after a rule
017: * application, currently giving information about added and removed
018: * formulas */
019: public class NodeReplacement {
020:
021: Node node;
022: Node parent;
023: ListOfSequentChangeInfo rawChanges;
024: ListOfNodeChange changes = null;
025:
026: /**
027: * @param p_node the node this object reports about
028: * @param p_parent the parent node
029: * @param p_changes the complete list of changes made to the
030: * original node, with the most recent change being the first
031: * element of the list
032: */
033: public NodeReplacement(Node p_node, Node p_parent,
034: ListOfSequentChangeInfo p_changes) {
035: node = p_node;
036: parent = p_parent;
037: rawChanges = p_changes;
038: }
039:
040: private void addNodeChanges() {
041: if (rawChanges != SLListOfSequentChangeInfo.EMPTY_LIST) {
042: SequentChangeInfo sci = rawChanges.head();
043: rawChanges = rawChanges.tail();
044:
045: addNodeChanges();
046:
047: addNodeChange(sci);
048: }
049: }
050:
051: private void addNodeChange(SequentChangeInfo p_sci) {
052: IteratorOfConstrainedFormula it;
053: IteratorOfFormulaChangeInfo it2;
054:
055: //---
056: it = p_sci.removedFormulas(true).iterator();
057: while (it.hasNext())
058: addRemovedChange(it.next(), true);
059:
060: it = p_sci.removedFormulas(false).iterator();
061: while (it.hasNext())
062: addRemovedChange(it.next(), false);
063:
064: // Information about modified formulas is currently not used
065: it2 = p_sci.modifiedFormulas(true).iterator();
066: while (it2.hasNext())
067: addRemovedChange(it2.next().getPositionOfModification()
068: .constrainedFormula(), true);
069:
070: // Information about modified formulas is currently not used
071: it2 = p_sci.modifiedFormulas(false).iterator();
072: while (it2.hasNext())
073: addRemovedChange(it2.next().getPositionOfModification()
074: .constrainedFormula(), false);
075:
076: it = p_sci.addedFormulas(true).iterator();
077: while (it.hasNext())
078: addAddedChange(it.next(), true);
079:
080: it = p_sci.addedFormulas(false).iterator();
081: while (it.hasNext())
082: addAddedChange(it.next(), false);
083:
084: // Information about modified formulas is currently not used
085: it2 = p_sci.modifiedFormulas(true).iterator();
086: while (it2.hasNext())
087: addAddedChange(it2.next().getNewFormula(), true);
088:
089: // Information about modified formulas is currently not used
090: it2 = p_sci.modifiedFormulas(false).iterator();
091: while (it2.hasNext())
092: addAddedChange(it2.next().getNewFormula(), false);
093:
094: // Information about formulas that have not been added as equal or more general
095: // formulas are already on the sequent
096: it = p_sci.rejectedFormulas(true).iterator();
097: while (it.hasNext())
098: addAddedRedundantChange(it.next(), true);
099:
100: it = p_sci.rejectedFormulas(false).iterator();
101: while (it.hasNext())
102: addAddedRedundantChange(it.next(), false);
103:
104: }
105:
106: private void addAddedChange(ConstrainedFormula p_cf,
107: boolean p_inAntec) {
108: Sequent oldS = parent.sequent();
109: Semisequent oldSS = (p_inAntec ? oldS.antecedent() : oldS
110: .succedent());
111: Sequent newS = node.sequent();
112: Semisequent newSS = (p_inAntec ? newS.antecedent() : newS
113: .succedent());
114:
115: removeNodeChanges(p_cf, p_inAntec);
116:
117: if (!oldSS.contains(p_cf) && newSS.contains(p_cf)) {
118: PosInOccurrence pio = new PosInOccurrence(p_cf,
119: PosInTerm.TOP_LEVEL, p_inAntec);
120: addNodeChange(new NodeChangeAddFormula(pio));
121: }
122: }
123:
124: /** TODO comment
125: *
126: * @param p_cf
127: * @param p_inAntec
128: */
129: private void addAddedRedundantChange(ConstrainedFormula p_cf,
130: boolean p_inAntec) {
131:
132: final PosInOccurrence pio = new PosInOccurrence(p_cf,
133: PosInTerm.TOP_LEVEL, p_inAntec);
134: addNodeChange(new NodeRedundantAddChange(pio));
135:
136: }
137:
138: private void addRemovedChange(ConstrainedFormula p_cf,
139: boolean p_inAntec) {
140: Sequent oldS = parent.sequent();
141: Semisequent oldSS = (p_inAntec ? oldS.antecedent() : oldS
142: .succedent());
143:
144: removeNodeChanges(p_cf, p_inAntec);
145:
146: if (oldSS.contains(p_cf)) {
147: PosInOccurrence pio = new PosInOccurrence(p_cf,
148: PosInTerm.TOP_LEVEL, p_inAntec);
149: addNodeChange(new NodeChangeRemoveFormula(pio));
150: }
151: }
152:
153: private void addNodeChange(NodeChange p_nc) {
154: changes = changes.prepend(p_nc);
155: }
156:
157: private void removeNodeChanges(ConstrainedFormula p_cf,
158: boolean p_inAntec) {
159: IteratorOfNodeChange it = changes.iterator();
160: changes = SLListOfNodeChange.EMPTY_LIST;
161: NodeChange oldNC;
162: PosInOccurrence oldPio;
163:
164: while (it.hasNext()) {
165: oldNC = it.next();
166:
167: if (oldNC instanceof NodeChangeARFormula) {
168: oldPio = ((NodeChangeARFormula) oldNC).getPos();
169: if (oldPio.isInAntec() == p_inAntec
170: && oldPio.constrainedFormula().equals(p_cf))
171: continue;
172: }
173:
174: addNodeChange(oldNC);
175: }
176: }
177:
178: public Node getNode() {
179: return node;
180: }
181:
182: /**
183: * @return Modifications that have been made to node
184: */
185: public IteratorOfNodeChange getNodeChanges() {
186: if (changes == null) {
187: changes = SLListOfNodeChange.EMPTY_LIST;
188: addNodeChanges();
189: }
190: return changes.iterator();
191: }
192:
193: public String toString() {
194: getNodeChanges();
195: return "Changes: " + changes;
196: }
197: }
|