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: /** this class contains the prefix for an Taclet according to M.Gieses paper
012: * "Taclet mit Schemavariablen und lokalen Deklarationen"
013: * It is used as a data container for the set of all variables bound above the
014: * appearance of a SchemaVariable v in a Taclet without all those x not free
015: * in v variables
016: */package de.uka.ilkd.key.rule;
017:
018: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
019: import de.uka.ilkd.key.logic.op.SchemaVariable;
020: import de.uka.ilkd.key.logic.op.SetOfSchemaVariable;
021:
022: public class TacletPrefix {
023:
024: /** the prefix of the taclet */
025: private SetOfSchemaVariable prefix;
026: /** used by rewrite taclets to mark the context */
027: private boolean context;
028:
029: /** creates the prefix
030: * @param prefix the SetOfSchemaVariable that is the prefix of a termsv or
031: * formulasv
032: * @param context a boolean marker
033: */
034: public TacletPrefix(SetOfSchemaVariable prefix, boolean context) {
035: this .prefix = prefix;
036: this .context = context;
037: }
038:
039: /** returns the prefix
040: * @return the prefix
041: */
042: public SetOfSchemaVariable prefix() {
043: return prefix;
044: }
045:
046: public IteratorOfSchemaVariable iterator() {
047: return prefix().iterator();
048: }
049:
050: /** returns the context marker
051: * @return the context marker
052: */
053: public boolean context() {
054: return context;
055: }
056:
057: /**
058: * returns a new TacletPrefix with the context flag set to the given
059: * boolean value
060: * @param setTo the boolean to which the TacletPrefix is set to
061: * @return a newly created TacletPrefix
062: */
063: public TacletPrefix setContext(boolean setTo) {
064: return new TacletPrefix(prefix, setTo);
065: }
066:
067: /** creates a new TacletPrefix with a new prefix entry
068: * @param var the SchemaVariable to be added
069: * @return the new prefix
070: */
071: public TacletPrefix put(SchemaVariable var) {
072: if (!var.isVariableSV()) {
073: throw new RuntimeException("var can match more than "
074: + "bound variables");
075: }
076: return new TacletPrefix(prefix.add(var), context);
077: }
078:
079: /** removes a SchemaVariable from the prefix
080: * @param var the SchemaVariable to be removed
081: * @return the new prefix
082: */
083: public TacletPrefix remove(SchemaVariable var) {
084: return new TacletPrefix(prefix.remove(var), context);
085: }
086:
087: public boolean equals(Object o) {
088: if (o == this ) {
089: return true;
090: }
091: if (!(o instanceof TacletPrefix)) {
092: return false;
093: }
094: TacletPrefix other = (TacletPrefix) o;
095: return (other.prefix().equals(prefix()))
096: && (other.context() == context());
097: }
098:
099: public int hashCode() {
100: int result = 17;
101: result = 37 * result + prefix().hashCode();
102: result = 37 * result + (context() ? 0 : 1);
103: return result;
104: }
105:
106: public String toString() {
107: return "TacletPrefix: " + prefix + (context() ? "+ { K }" : "");
108: }
109: }
|