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: package de.uka.ilkd.key.rule.conditions;
009:
010: import de.uka.ilkd.key.java.Expression;
011: import de.uka.ilkd.key.java.ProgramElement;
012: import de.uka.ilkd.key.java.Services;
013: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.logic.sort.GenericSort;
017: import de.uka.ilkd.key.logic.sort.Sort;
018: import de.uka.ilkd.key.rule.inst.SVInstantiations;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * Several variable conditions deal with types. The type resolver provides a
023: * unique interface to access types, e.g. the type of a schemavariable instantiation,
024: * the instantiated type of a generic sort or the type an attribut eis declared in.
025: *
026: */
027: public abstract class TypeResolver {
028:
029: public static TypeResolver createContainerTypeResolver(
030: SchemaVariable s) {
031: return new ContainerTypeResolver(s);
032: }
033:
034: public static TypeResolver createElementTypeResolver(
035: SchemaVariable s) {
036: return new ElementTypeResolverForSV(s);
037: }
038:
039: public static TypeResolver createGenericSortResolver(GenericSort gs) {
040: return new GenericSortResolver(gs);
041: }
042:
043: public static class GenericSortResolver extends TypeResolver {
044:
045: private final GenericSort gs;
046:
047: public GenericSortResolver(GenericSort gs) {
048: this .gs = gs;
049: }
050:
051: public boolean isComplete(SchemaVariable sv,
052: SVSubstitute instCandidate, SVInstantiations instMap,
053: Services services) {
054: return instMap.getGenericSortInstantiations()
055: .getInstantiation(gs) != null;
056: }
057:
058: public Sort resolveSort(SchemaVariable sv,
059: SVSubstitute instCandidate, SVInstantiations instMap,
060: Services services) {
061: return instMap.getGenericSortInstantiations()
062: .getInstantiation(gs);
063: }
064:
065: public KeYJavaType resolveType(SchemaVariable sv,
066: SVSubstitute instCandidate, SVInstantiations instMap,
067: Services services) {
068: final Sort s = resolveSort(sv, instCandidate, instMap,
069: services);
070: return services.getJavaInfo().getKeYJavaType(s);
071: }
072:
073: public String toString() {
074: return gs.toString();
075: }
076: }
077:
078: public static class ElementTypeResolverForSV extends TypeResolver {
079:
080: private final SortedSchemaVariable resolveSV;
081:
082: public ElementTypeResolverForSV(SchemaVariable sv) {
083: if (!(sv instanceof SortedSchemaVariable)) {
084: throw new IllegalArgumentException(
085: "Expected a SortedSchemaVariable," + " but is "
086: + sv);
087: }
088: this .resolveSV = (SortedSchemaVariable) sv;
089: }
090:
091: public boolean isComplete(SchemaVariable sv,
092: SVSubstitute instCandidate, SVInstantiations instMap,
093: Services services) {
094: return resolveSV == sv
095: || instMap.getInstantiation(resolveSV) != null;
096: }
097:
098: public Sort resolveSort(SchemaVariable sv,
099: SVSubstitute instCandidate, SVInstantiations instMap,
100: Services services) {
101:
102: final Sort s;
103:
104: final SVSubstitute inst = (SVSubstitute) (resolveSV == sv ? instCandidate
105: : instMap.getInstantiation(resolveSV));
106:
107: if (inst instanceof ProgramVariable) {
108: s = ((ProgramVariable) inst).sort();
109: } else {
110: Term gsTerm = null;
111: if (inst instanceof Term) {
112: gsTerm = (Term) inst;
113: } else if (inst instanceof ProgramElement) {
114: gsTerm = services.getTypeConverter()
115: .convertToLogicElement(
116: (ProgramElement) inst,
117: instMap.getExecutionContext());
118: } else {
119: Debug.fail("Unexpected substitution for sv "
120: + resolveSV + ":" + inst);
121: return null;
122: }
123: s = gsTerm.sort();
124: }
125: return s;
126: }
127:
128: public KeYJavaType resolveType(SchemaVariable sv,
129: SVSubstitute instCandidate, SVInstantiations instMap,
130: Services services) {
131: final Sort s = resolveSort(sv, instCandidate, instMap,
132: services);
133: return services.getJavaInfo().getKeYJavaType(s);
134: }
135:
136: public String toString() {
137: return "\\typeof(" + resolveSV + ")";
138: }
139: }
140:
141: public static class ContainerTypeResolver extends TypeResolver {
142:
143: private final SchemaVariable memberSV;
144:
145: public ContainerTypeResolver(SchemaVariable sv) {
146: this .memberSV = sv;
147: }
148:
149: public boolean isComplete(SchemaVariable sv,
150: SVSubstitute instCandidate, SVInstantiations instMap,
151: Services services) {
152:
153: return sv == memberSV
154: || instMap.getInstantiation(memberSV) != null;
155: }
156:
157: public Sort resolveSort(SchemaVariable sv,
158: SVSubstitute instCandidate, SVInstantiations instMap,
159: Services services) {
160: return resolveType(sv, instCandidate, instMap, services)
161: .getSort();
162: }
163:
164: public KeYJavaType resolveType(SchemaVariable sv,
165: SVSubstitute instCandidate, SVInstantiations instMap,
166: Services services) {
167:
168: final KeYJavaType resolvedType;
169:
170: final SVSubstitute inst = (SVSubstitute) (memberSV == sv ? instCandidate
171: : instMap.getInstantiation(memberSV));
172:
173: if (inst instanceof Operator) {
174: resolvedType = getContainerType(inst);
175: } else {
176: if (inst instanceof Expression) {
177: resolvedType = getContainerType(services
178: .getTypeConverter().convertToLogicElement(
179: (Expression) inst,
180: instMap.getExecutionContext()).op());
181: } else if (inst instanceof Term) {
182: resolvedType = getContainerType(((Term) inst).op());
183: } else {
184: Debug.fail("Unexpected instantiation for SV "
185: + memberSV + ":" + inst);
186: resolvedType = null;
187: }
188: }
189: return resolvedType;
190: }
191:
192: private KeYJavaType getContainerType(SVSubstitute inst) {
193: KeYJavaType resolvedType = null;
194: if (inst instanceof ProgramVariable) {
195: resolvedType = ((ProgramVariable) inst)
196: .getContainerType();
197: } else if (inst instanceof AttributeOp) {
198: resolvedType = ((AttributeOp) inst).getContainerType();
199: } else {
200: Debug.fail("Unknown member type: ", inst);
201: }
202: return resolvedType;
203: }
204:
205: public String toString() {
206: return "\\containerType(" + memberSV + ")";
207: }
208: }
209:
210: public abstract boolean isComplete(SchemaVariable sv,
211: SVSubstitute instCandidate, SVInstantiations instMap,
212: Services services);
213:
214: public abstract Sort resolveSort(SchemaVariable sv,
215: SVSubstitute instCandidate, SVInstantiations instMap,
216: Services services);
217:
218: public abstract KeYJavaType resolveType(SchemaVariable sv,
219: SVSubstitute instCandidate, SVInstantiations instMap,
220: Services services);
221:
222: }
|