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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.parser.ocl;
019:
020: import de.uka.ilkd.key.java.JavaInfo;
021: import de.uka.ilkd.key.java.Services;
022: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
023: import de.uka.ilkd.key.logic.*;
024: import de.uka.ilkd.key.logic.op.IteratorOfLogicVariable;
025: import de.uka.ilkd.key.logic.op.IteratorOfParsableVariable;
026: import de.uka.ilkd.key.logic.op.ListOfLogicVariable;
027: import de.uka.ilkd.key.logic.op.ListOfParsableVariable;
028: import de.uka.ilkd.key.logic.op.ParsableVariable;
029: import de.uka.ilkd.key.logic.sort.ObjectSort;
030:
031: /**
032: * Resolves property calls of any kind.
033: * Keeps a stack of namespaces to deal with several levels of local variables
034: * (e.g. "self", or iterator variables in forall() or select() subtrees).
035: */
036: class PropertyManager {
037:
038: private static final TermBuilder tb = TermBuilder.DF;
039:
040: private final JavaInfo javaInfo;
041: private final ListOfPropertyResolver resolvers;
042:
043: private ListOfNamespace /*ParsableVariable*/
044: localVariablesNamespaces = SLListOfNamespace.EMPTY_LIST;
045:
046: public PropertyManager(Services services, FormulaBoolConverter fbc,
047: ParsableVariable excVar) {
048: this .javaInfo = services.getJavaInfo();
049: ListOfPropertyResolver list = SLListOfPropertyResolver.EMPTY_LIST;
050: list = list.prepend(new AssociationResolver(services));
051: list = list.prepend(new BuiltInPropertyResolver(services,
052: excVar));
053: list = list.prepend(new MethodResolver(services, fbc));
054: list = list.prepend(new AttributeResolver(services));
055: resolvers = list;
056: }
057:
058: /**
059: * Tries to resolve a name as a property call on an explicit receiver.
060: * @throws OCLTranslationError
061: */
062: private OCLEntity resolveExplicit(OCLEntity receiver, String name,
063: OCLParameters parameters) throws OCLTranslationError {
064: IteratorOfPropertyResolver it = resolvers.iterator();
065: while (it.hasNext()) {
066: OCLEntity result = it.next().resolve(receiver, name,
067: parameters);
068: if (result != null) {
069: return result;
070: }
071: }
072: return null;
073: }
074:
075: /**
076: * Tries to resolve a name as a type.
077: */
078: private OCLEntity resolveType(String name) {
079: try {
080: KeYJavaType kjt = javaInfo.getTypeByClassName(name);
081: if (kjt != null) {
082: return new OCLEntity(kjt);
083: }
084: } catch (RuntimeException e) {
085: // do nothing
086: }
087: return null;
088: }
089:
090: /**
091: * Tries to resolve a name as a local variable.
092: */
093: private OCLEntity resolveLocal(String name) {
094: Name n = new Name(name);
095: IteratorOfNamespace it = localVariablesNamespaces.iterator();
096: while (it.hasNext()) {
097: ParsableVariable localVar = (ParsableVariable) it.next()
098: .lookup(n);
099: if (localVar != null) {
100: Term varTerm = tb.var(localVar);
101: return new OCLEntity(varTerm);
102: }
103: }
104:
105: return null;
106: }
107:
108: /**
109: * Tries to resolve a name as a property call on any available implicit
110: * receiver.
111: * @throws OCLTranslationError
112: */
113: private OCLEntity resolveImplicit(String name,
114: OCLParameters parameters) throws OCLTranslationError {
115: IteratorOfNamespace it = localVariablesNamespaces.iterator();
116: while (it.hasNext()) {
117: Namespace ns = it.next();
118: ListOfNamed elements = ns.elements();
119:
120: IteratorOfNamed it2 = elements.iterator();
121: while (it2.hasNext()) {
122: ParsableVariable localVar = (ParsableVariable) it2
123: .next();
124: if (localVar.sort() instanceof ObjectSort) {
125: Term recTerm = tb.var(localVar);
126: OCLEntity result = resolveExplicit(new OCLEntity(
127: recTerm), name, parameters);
128: if (result != null) {
129: return result;
130: }
131: }
132: }
133: }
134:
135: return null;
136: }
137:
138: /**
139: * Pushes a new, empty namespace onto the stack.
140: */
141: public void pushLocalVariablesNamespace() {
142: Namespace ns = new Namespace();
143: localVariablesNamespaces = localVariablesNamespaces.prepend(ns);
144: }
145:
146: /**
147: * Puts a local variable into the topmost namespace on the stack
148: */
149: public void putIntoTopLocalVariablesNamespace(ParsableVariable pv) {
150: localVariablesNamespaces.head().addSafely(pv);
151: }
152:
153: /**
154: * Puts a list of local variables into the topmost namespace on the stack.
155: */
156: public void putIntoTopLocalVariablesNamespace(
157: ListOfLogicVariable pvs) {
158: IteratorOfLogicVariable it = pvs.iterator();
159: while (it.hasNext()) {
160: localVariablesNamespaces.head().addSafely(it.next());
161: }
162: }
163:
164: /**
165: * Throws away the topmost namespace on the stack.
166: */
167: public void popLocalVariablesNamespace() {
168: localVariablesNamespaces = localVariablesNamespaces.tail();
169: }
170:
171: /**
172: * Determines whether a variable has to be put into localVariableNamespace
173: * @param propertyName name of the propertyCall
174: * @return true, if propertyName needs a variable to be put into
175: * localVariableNamespace
176: */
177: public boolean needVarDeclaration(String propertyName) {
178: IteratorOfPropertyResolver it = resolvers.iterator();
179: while (it.hasNext()) {
180: if (it.next().needVarDeclaration(propertyName)) {
181: return true;
182: }
183: }
184: return false;
185: }
186:
187: /**
188: * Resolves arbitrary property calls.
189: * @param receiver the specified explicit receiver, or null
190: * @param name name of the property
191: * @param parameters actual parameters of the property call, or null
192: * @return corresponding term, type or collection if successful, null
193: * otherwise
194: * @throws OCLTranslationError
195: */
196: public OCLEntity resolve(OCLEntity receiver, String name,
197: OCLParameters parameters) throws OCLTranslationError {
198: OCLEntity result = null;
199:
200: if (receiver != null) {
201: result = resolveExplicit(receiver, name, parameters);
202: } else {
203: result = resolveType(name);
204: if (result == null) {
205: result = resolveLocal(name);
206: if (result == null) {
207: result = resolveImplicit(name, parameters);
208: }
209: }
210: }
211:
212: return result;
213: }
214: }
|