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.logic.op;
012:
013: import de.uka.ilkd.key.java.NameAbstractionTable;
014: import de.uka.ilkd.key.java.SourceElement;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.sort.Sort;
018:
019: /**
020: * This class represents the root of a schema variable hierarchy to be
021: * express termstructures that match on logical terms. Schema variables
022: * are used in Taclets where they act as placeholders for other
023: * TermSymbols. The TermSymbols a SchemaVariable is allowed to match
024: * is specified by their type and sort. If a match fits these
025: * conditions can be checked using the method isCompatible(TermSymbol t)
026: */
027: public abstract class SchemaVariableAdapter extends TermSymbol
028: implements SchemaVariable {
029:
030: /**
031: * SchemaVariables are used as placeholder for other
032: * TermSymbols. The allowed type of the symbols is stored here.
033: */
034: private final Class matchType;
035:
036: /**
037: * this flag indicates if the schemavariable matches a list of syntactical
038: * elements
039: */
040: private final boolean listSV;
041:
042: /**
043: * creates a new SchemaVariable. That is used as placeholder for
044: * TermSymbols of a certain type.
045: * @param name the Name of the SchemaVariable
046: * @param matchType Class representing the type of symbols that
047: * can be matched
048: * @param sort the Sort of the SchemaVariable and the matched type
049: * @param listSV a boolean which is true iff the schemavariable is allowed
050: * to match a list of syntactical elements
051: */
052: protected SchemaVariableAdapter(Name name, Class matchType,
053: Sort sort, boolean listSV) {
054: super (name, sort);
055: this .matchType = matchType;
056: this .listSV = listSV;
057: }
058:
059: protected SchemaVariableAdapter(Name name, Class matchType) {
060: this (name, matchType, null, false);
061: }
062:
063: /**
064: * this method tests on object identity
065: */
066: public boolean equalsModRenaming(SourceElement se,
067: NameAbstractionTable nat) {
068: return se == this ;
069: }
070:
071: public Class matchType() {
072: return matchType;
073: }
074:
075: /** returns true iff this SchemaVariable is used to match
076: * bound (quantifiable) variables
077: * @return true iff this SchemaVariable is used to match
078: * bound (quantifiable) variables
079: */
080: public boolean isVariableSV() {
081: return false;
082: }
083:
084: /** returns true iff this SchemaVariable is used to match
085: * a term but not a formula
086: * @return true iff this SchemaVariable is used to match
087: * a term but not a formula
088: */
089: public boolean isTermSV() {
090: return false;
091: }
092:
093: /** returns true iff this SchemaVariable is used to match
094: * a formula
095: * @return true iff this SchemaVariable is used to match
096: * a formula
097: */
098: public boolean isFormulaSV() {
099: return false;
100: }
101:
102: /** returns true iff this SchemaVariable is used to match
103: * a part of a program
104: * @return true iff this SchemaVariable is used to match
105: * a part of a program
106: */
107: public boolean isProgramSV() {
108: return false;
109: }
110:
111: /**
112: * returns true if the schemavariable can match a list of syntactical
113: * elements
114: * @return true if the schemavariable can match a list of syntactical
115: * elements
116: */
117: public boolean isListSV() {
118: return listSV;
119: }
120:
121: /**
122: * @return true iff this SchemaVariable is used to match
123: * modal operators
124: */
125: public boolean isOperatorSV() {
126: return false;
127: }
128:
129: /** returns true iff this SchemaVariable is used to match (create)
130: * a skolem term
131: * @return true iff this SchemaVariable is used to match (create)
132: * a skolem term
133: */
134: public boolean isSkolemTermSV() {
135: return false;
136: }
137:
138: public boolean isNameSV() {
139: return false;
140: }
141:
142: /**
143: * @return true if the schemavariable has the strict modifier
144: * which forces the instantiation to have exact the same sort
145: * as the schemavariable (or if the sv is of generic sort -
146: * the instantiation of the generic sort)
147: */
148: public boolean isStrict() {
149: return true;
150: }
151:
152: /** @return arity of the Variable as int */
153: public int arity() {
154: return 0;
155: }
156:
157: /**
158: * @return true if the value of "term" having this operator as
159: * top-level operator and may not be changed by modalities
160: */
161: public boolean isRigid(Term term) {
162: return isRigid();
163: }
164:
165: public boolean isRigid() {
166: return false;
167: }
168:
169: /** toString */
170: public String toString(String sortSpec) {
171: return name() + " (" + sortSpec + ")";
172: }
173:
174: /* default toString for schema variables witho sortSpec, e.g. ModifiesSV */
175: public String toString() {
176: return name().toString();
177: }
178: }
|