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.rule.inst;
012:
013: import de.uka.ilkd.key.logic.op.SortDependingSymbol;
014: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
015: import de.uka.ilkd.key.logic.sort.CollectionSort;
016: import de.uka.ilkd.key.logic.sort.GenericSort;
017: import de.uka.ilkd.key.logic.sort.Sort;
018:
019: /**
020: * Abstract superclass for conditions controlling the instantiations
021: * of generic sorts
022: */
023: public abstract class GenericSortCondition {
024:
025: private GenericSort gs;
026:
027: /**
028: * Create the condition that needs to be fulfilled for the given
029: * instantiation of a metavariable to be correct, i.e. if the
030: * schemavariable is of generic sort, the instantiation of that
031: * sort has to match the sort of the schemavariable's
032: * instantiation
033: * @return the resulting condition, if the schemavariable is of
034: * generic sort; null, if the sorts are either always compatible
035: * (no generic sorts) or never compatible (non generic sorts that
036: * don't match)
037: */
038: public static GenericSortCondition createCondition(
039: InstantiationEntry p_entry) {
040:
041: if (!(p_entry instanceof TermInstantiation))
042: return null;
043:
044: final TermInstantiation ti = (TermInstantiation) p_entry;
045: final SortedSchemaVariable ssv = (SortedSchemaVariable) p_entry
046: .getSchemaVariable();
047:
048: return createCondition(ssv.sort(), ti.getTerm().sort(),
049: !subSortsAllowed(ssv));
050: }
051:
052: /**
053: * Create a condition ensuring that the two given symbols become
054: * identical; "p0" may be of generic sort, "p1" not
055: * @return the resulting condition; null if the symbols are either
056: * incompatible or equal
057: */
058: public static GenericSortCondition createCondition(
059: SortDependingSymbol p0, SortDependingSymbol p1) {
060:
061: if (!p0.isSimilar(p1))
062: return null;
063:
064: return createCondition(p0.getSortDependingOn(), p1
065: .getSortDependingOn(), true);
066: }
067:
068: /**
069: * @return <code>true</code> iff the variable <code>p_sv</code> is
070: * allowed to be instantiated with expressions that have a real
071: * subtype of the type of <code>p_sv</code>. Otherwise the sorts
072: * have to match exactly
073: */
074: static boolean subSortsAllowed(SortedSchemaVariable p_sv) {
075: return p_sv.isTermSV() && !p_sv.isStrict();
076: }
077:
078: /**
079: * Create the condition to make a generic sort (s0) (or a
080: * collection sort of a generic sort) and a concrete sort (s1)
081: * equal
082: * @param p_identity true iff an identity condition should be
083: * generated (otherwise: a supersort condition is generated)
084: * @return the resulting condition, if "s0" is of generic sort;
085: * null, if the sorts are either always compatible (no generic
086: * sorts) or never compatible (e.g. non generic sorts that don't
087: * match)
088: */
089: protected static GenericSortCondition createCondition(Sort s0,
090: Sort s1, boolean p_identity) {
091: while (s0 instanceof CollectionSort) {
092: // Currently the sort hierarchy is not inherited by
093: // collection sorts; therefore identity has to be ensured
094: p_identity = true;
095:
096: if (!s0.getClass().equals(s1.getClass()))
097: return null;
098:
099: s0 = ((CollectionSort) s0).elementSort();
100: s1 = ((CollectionSort) s1).elementSort();
101: }
102:
103: if (!(s0 instanceof GenericSort) || s1 == Sort.FORMULA)
104: return null;
105:
106: final GenericSort gs = (GenericSort) s0;
107:
108: if (p_identity) {
109: return createIdentityCondition(gs, s1);
110: } else {
111: return createSupersortCondition(gs, s1);
112: }
113: }
114:
115: /**
116: * Create the condition to force the instantiation of a given
117: * (possibly generic) sort
118: * @param p_maximum hint whether the generic sort should be
119: * instantiated with the maximum or mimimum possible concrete sort
120: * (this hint is currently not used by GenericSortInstantiations)
121: * @return the resulting condition, or null if "p_s" is not
122: * generic
123: */
124: public static GenericSortCondition forceInstantiation(Sort p_s,
125: boolean p_maximum) {
126:
127: if (p_s instanceof GenericSort)
128: return createForceInstantiationCondition((GenericSort) p_s,
129: p_maximum);
130: else if (p_s instanceof CollectionSort)
131: return forceInstantiation(((CollectionSort) p_s)
132: .elementSort(), p_maximum);
133:
134: return null;
135: }
136:
137: /**
138: * @return a condition that specifies the given generic sort to be
139: * instantiated with a supersort of the given concrete sort
140: */
141: public static GenericSortCondition createSupersortCondition(
142: GenericSort p_gs, Sort p_s) {
143: return new GSCSupersort(p_gs, p_s);
144: }
145:
146: /**
147: * @return a condition that specifies the given generic sort to be
148: * instantiated (exactly) with the given concrete sort
149: */
150: public static GenericSortCondition createIdentityCondition(
151: GenericSort p_gs, Sort p_s) {
152: return new GSCIdentity(p_gs, p_s);
153: }
154:
155: /**
156: * @return a condition that specifies the given generic sort to be
157: * instantiated
158: * @param p_maximum hint whether the generic sort should be
159: * instantiated with the maximum or mimimum possible concrete sort
160: * (this hint is currently not used by GenericSortInstantiations)
161: */
162: public static GenericSortCondition createForceInstantiationCondition(
163: GenericSort p_gs, boolean p_maximum) {
164: return new GSCForceInstantiation(p_gs, p_maximum);
165: }
166:
167: public GenericSort getGenericSort() {
168: return gs;
169: }
170:
171: protected GenericSortCondition(GenericSort p_gs) {
172: gs = p_gs;
173: }
174:
175: /**
176: * returns true if the given sort <code>s</code> satisfies this generic sort
177: * condition
178: * @param s the Sort to check
179: * @param insts a map containing already found instantiations
180: * @return true if the given sort <code>s</code> satisfies this generic sort
181: * condition
182: */
183: public abstract boolean check(Sort s,
184: GenericSortInstantiations insts);
185:
186: static class GSCSupersort extends GenericSortCondition {
187: Sort s;
188:
189: protected GSCSupersort(GenericSort p_gs, Sort p_s) {
190: super (p_gs);
191: s = p_s;
192: }
193:
194: public Sort getSubsort() {
195: return s;
196: }
197:
198: /**
199: * checks if sort <code>p_s</code> is a supersort of
200: * the <code>getSubsort</code>
201: */
202: public boolean check(Sort p_s, GenericSortInstantiations insts) {
203: return getSubsort().extendsTrans(p_s);
204: }
205:
206: /** toString */
207: public String toString() {
208: return "Supersort condition: " + getGenericSort() + " >= "
209: + getSubsort();
210: }
211:
212: }
213:
214: static class GSCIdentity extends GenericSortCondition {
215: Sort s;
216:
217: protected GSCIdentity(GenericSort p_gs, Sort p_s) {
218: super (p_gs);
219: s = p_s;
220: }
221:
222: public Sort getSort() {
223: return s;
224: }
225:
226: /**
227: * tests if <code>p_s</code> is identical to @link GSCIdentity#getSort()
228: */
229: public boolean check(Sort p_s, GenericSortInstantiations insts) {
230: return p_s == getSort();
231: }
232:
233: /** toString */
234: public String toString() {
235: return "Sort Identity: " + getGenericSort() + " = "
236: + getSort();
237: }
238: }
239:
240: static class GSCForceInstantiation extends GenericSortCondition {
241: boolean maximum;
242:
243: protected GSCForceInstantiation(GenericSort p_gs,
244: boolean p_maximum) {
245: super (p_gs);
246: maximum = p_maximum;
247: }
248:
249: public boolean getMaximum() {
250: return maximum;
251: }
252:
253: /**
254: * checks if @link GenericSortcondition#getgenericSort()
255: * has been already instantiated by some sort
256: * (maximum, minimum is currently not checked)
257: */
258: public boolean check(Sort p_s, GenericSortInstantiations insts) {
259: return insts.isInstantiated(getGenericSort());
260: }
261:
262: /** toString */
263: public String toString() {
264: return "Force instantiation: " + getGenericSort() + ", "
265: + (getMaximum() ? "maximum" : "minimum");
266: }
267:
268: }
269: }
|