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.proof.decproc.translation;
012:
013: import org.apache.log4j.Logger;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.Visitor;
016:
017: /** This class representing a visitor intended to be used for the translation of KeY <tt>Term</tt>s.
018: * <p>
019: * The translate a <tt>Term</tt>, a <tt>TranslationVisitor</tt> instance will be passed to either
020: * the <tt>execPostOrder</tt> or the <tt>execPreOrder</tt> method of the given <tt>Term</tt>.
021: * These methods then call the <tt>visit</tt> method of the passed <tt>TranslationVisitor</tt>
022: * recursively, with the appropriate subterms of the given <tt>Term</tt> as arguments
023: *
024: * @author akuwertz
025: * @version 1.0, 12/10/2006
026: */
027:
028: public abstract class TranslationVisitor extends Visitor {
029:
030: /* Additional fields */
031:
032: /** The array of translation rules represented by exactly one instance of an
033: * <tt>IOperatorTranslation</tt> subclass per rule. */
034: protected IOperatorTranslation[] translationRules = null;
035:
036: /** A counter indicating the level in the AST of the top level <tt>Term</tt> on which the
037: * currently translated subterms occurs */
038: private int level = -1;
039:
040: /** A <tt>Logger</tt> for logging and debugging the translation process */
041: protected static final Logger logger = Logger
042: .getLogger(TranslationVisitor.class.getName());
043:
044: /** A short <tt>String</tt> identifying the implementing <tt>TranslationVisitor</tt> subclass
045: * which has produced the current log statement */
046: protected String loggingSubclass;
047:
048: /* String constants for failures during translation process */
049: private static final String nothingTranslatedException = "No translation has been initiated up to now!";
050: protected static final String translationNotFinishedException = "The translation of the current Term has not finished yet!";
051: protected static final String NoReuseStateException = "Previous translation didn't finish successfully or result has not been fetched yet!";
052:
053: /* Public method implementation */
054:
055: /** A factory method for returning an instance of a <tt>TranslationVisitor</tt> implementing
056: * subclass. It therefore must be implemented in that subclass.
057: * <p>
058: * This method intends the reuse of already created subclass instances. Subclasses overriding
059: * this method should therefore use the Singleton pattern, enabling time and memory savings.
060: * <p>
061: * To reuse <tt>TranslationVisitor</tt> instances, they have to be in a well-defined, resuable
062: * state. To ensure this state, the <tt>isReusable</tt> should be called by an overriding
063: * implementation.<br>
064: * To reset an instance to a reusable state, the <tt>reset</tt> method should be used
065: *
066: * @return a <tt>TranslationVisitor</tt> instance
067: *
068: * @see #isReusable()
069: * @see #reset()
070: */
071: public synchronized static TranslationVisitor getInstance() {
072: throw new UnsupportedOperationException();
073: }
074:
075: /** The visit method of this <tt>TranslationVisitor</tt>. Takes a KeY <tt>Term</tt> and tries
076: * to translate it
077: * <p>
078: * Has to be implemented by a specific subclass
079: *
080: * @see de.uka.ilkd.key.logic.Visitor#visit(de.uka.ilkd.key.logic.Term)
081: */
082: abstract public void visit(Term t);
083:
084: /** This method is intended to be called only by the <tt>execPostOrder</tt> method of
085: * class <tt>de.uka.ilkd.key.logic.Term</tt>
086: *
087: * @see de.uka.ilkd.key.logic.Visitor#subtreeEntered(de.uka.ilkd.key.logic.Term)
088: */
089: public final void subtreeEntered(Term subtreeRoot) {
090: logger.info(logThis("->Subtree entered!"));
091: if (level == -1) {
092: level = 1;
093: } else {
094: level++;
095: }
096: }
097:
098: /** This method is intended to be called only by the <tt>execPostOrder</tt> method of
099: * class <tt>de.uka.ilkd.key.logic.Term</tt>
100: *
101: * @see de.uka.ilkd.key.logic.Visitor#subtreeLeft(de.uka.ilkd.key.logic.Term)
102: */
103: public final void subtreeLeft(Term subtreeRoot) {
104: logger.info(logThis("<-Subtree left!"));
105: level--;
106: }
107:
108: /** Returns the result of the translation process and resets this <tt>TranslationVisitor</tt>
109: * for reuse.
110: * <p>
111: * The result is actually fetched by calling the <tt>getResult</tt> method of the implementing
112: * subclass.
113: * <p>
114: * After calling this method, this <tt>TranslationVisitor</tt> instance is in reusable state.
115: *
116: * @return the <tt>Object</tt> resulting from current <tt>Term</tt> translation
117: *
118: * @throws IllegalStateException if this method is called during an unfinished translation
119: * process or before any translation was initiated
120: * @see #getResult()
121: */
122: public final Object getTranslationResult() {
123: // A positive level value indicates an unfinished translation
124: if (level > 0)
125: throw new IllegalStateException(
126: translationNotFinishedException);
127: // A negative level value indicates that no translation was initiated
128: if (level < 0)
129: throw new IllegalStateException(nothingTranslatedException);
130:
131: level = -1; // Reset visitor for reuse
132:
133: logger
134: .debug(logThis("Visitor state is reusable, fetching result from subclass..."));
135: return getResult(); // Provide a hook for subclasses
136: }
137:
138: /** Resets this <tt>TranslationVisitor</tt> for reuse.<br>
139: * After execution of this method, the state of this <tt>TranslationVisistor</tt> is equal
140: * to that of a newly created <tt>TranslationVisitor</tt>
141: */
142: public void reset() {
143: logger.info(logThis("Reseted visitor!"));
144: level = -1;
145: }
146:
147: /* Protected (subclass) methods */
148:
149: /** Sets the translation rules by converting <tt>rules</tt> to an
150: * <tt>IOperatorTranslation</tt> array
151: *
152: * @param rules the rules to be set
153: */
154: protected final void setTranslationRules(
155: ListOfIOperatorTranslation rules) {
156: translationRules = rules.toArray();
157: }
158:
159: /** Returns true if this <tt>TranslationVisitor</tt> is ready for the next translation process
160: *
161: * @return true if this <tt>TranslationVisitor</tt> is ready to be reused; otherwise false
162: */
163: protected boolean isReusable() {
164: // A level value of -1 indicates that the previous translation process has completed
165: return level == -1;
166: }
167:
168: /** This methods provides a hook for implementing subclasses to forward their translation
169: * results.
170: * <p>
171: * It is intended to be called exclusively by the <tt>getTranslationResult</tt> method
172: * <p>
173: * After calling this method on a <tt>TranslationVisitor</tt> subclass instance, the instance
174: * has to be in the reusable state
175: *
176: * @return the translation result provided by an implementing subclass
177: *
178: * @see #getTranslationResult()
179: */
180: abstract protected Object getResult();
181:
182: /** Take a <tt>String</tt> which should be logged and adds a subclass identifying tag to it
183: *
184: * @param toLog the <tt>String</tt> to be logged
185: * @return the given <tt>String</tt> extended by a subclass tag
186: */
187: protected final String logThis(String toLog) {
188: return "(" + loggingSubclass + ") " + toLog;
189: }
190:
191: }
|