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.pp;
012:
013: import de.uka.ilkd.key.logic.PosInOccurrence;
014:
015: /**
016: * describes a position in a sequent including the bounds within a string
017: * representation of the sequent. In contrast to PosInOccurrence and
018: * PosInTerm of package de.uka.ilkd.key.logic, this class is mutable,
019: * i.e the bounds may be set later in an already existing PosInSequent
020: * instance. Apart from the bounds, PosInSequent has the following kind
021: * of states: It marks the whole sequent, the whole antecedent, the whole
022: * succedent or includes a PosInOccurrence if a position within a
023: * constrained formula of the sequent is referred to. In the latter case
024: * it contains also information whether the whole constrained formula
025: * is referred to or the formula or the constraint.
026: */
027: public class PosInSequent {
028:
029: private Range bounds;
030: private boolean sequent;
031: private PosInOccurrence posInOcc = null;
032:
033: private Range firstJavaStatementRange = null;
034:
035: /**
036: * creates a PosInSequent that points to the whole sequent.
037: */
038: public static PosInSequent createSequentPos() {
039: return new PosInSequent(null, true);
040: }
041:
042: /**
043: * creates a PosInSequent that points to a ConstrainedFormula described by
044: * a PosInOccurrence. Additionally a boolean indicates whether the
045: * the whole ConstrainedFormula or just the formula is meant.
046: * @param posInOcc the PositionInOccurrence describing the
047: * ConstrainedFormula and maybe a subterm of its formula.
048: * @param cfma true iff the whole ConstrainedFormula (i.e. formula AND
049: * constraint) is meant.
050: */
051: public static PosInSequent createCfmaPos(PosInOccurrence posInOcc) {
052: return new PosInSequent(posInOcc, false);
053: }
054:
055: // use the create... above for getting instances of PosInSequent
056: private PosInSequent(PosInOccurrence posInOcc, boolean sequent) {
057: this .posInOcc = posInOcc;
058: this .sequent = sequent;
059: }
060:
061: /**
062: * sets the bounds, i.e. the start and end positions
063: * of the PosInSequent
064: * in a string representation of a sequent.
065: * @param r the range of character positions
066: */
067: public void setBounds(Range r) {
068: bounds = r;
069: }
070:
071: /**
072: * returns the bounds in a string representation of a sequent
073: * @return start position
074: */
075: public Range getBounds() {
076: return bounds;
077: }
078:
079: /**
080: * sets the bounds, i.e. the start and end positions of the first
081: * Java statement, of a corresponding Java program in a string
082: * representation of the sequent.
083: * @param r the range for the first statement in the corresponding program
084: */
085: public void setFirstJavaStatementRange(Range r) {
086: firstJavaStatementRange = r;
087: }
088:
089: /**
090: * returns the bounds, i.e. the start and end positions of the first Java statement,
091: * of a corresponding Java program in a string representation of the sequent.
092: * @return the range specifying the first statement in the corresponding program
093: */
094: public Range getFirstJavaStatementRange() {
095: return firstJavaStatementRange;
096: }
097:
098: /**
099: * returns the PosInOccurrence if the PosInSequent marks a
100: * ConstrainedFormula or parts of it, null otherwise.
101: */
102: public PosInOccurrence getPosInOccurrence() {
103: return posInOcc;
104: }
105:
106: /**
107: * returns true if the PosInSequent points to a whole Sequent
108: */
109: public boolean isSequent() {
110: return sequent;
111: }
112:
113: /**
114: * returns a string representation of this PosInSequent
115: */
116: public String toString() {
117: if (isSequent())
118: return "Whole Sequent";
119: return "" + posInOcc;
120: }
121:
122: }
|