01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.proof.decproc.translation;
12:
13: import de.uka.ilkd.key.logic.op.Metavariable;
14: import de.uka.ilkd.key.logic.op.Operator;
15:
16: /** This class represents the translation rule for <tt>MetaVariable</tt>s.
17: * <p>
18: * They are currently not supported in the translation
19: *
20: * @author akuwertz
21: * @version 1.0, 01/28/2006
22: */
23:
24: public class TranslateMetavariable implements IOperatorTranslation {
25:
26: /* (non-Javadoc)
27: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
28: */
29: public boolean isApplicable(Operator op) {
30: return op instanceof Metavariable;
31: }
32:
33: /* (non-Javadoc)
34: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#translate(de.uka.ilkd.key.logic.op.Operator, de.uka.ilkd.key.proof.decproc.translation.TermTranslationVisitor)
35: */
36: public Object translate(Operator op,
37: TermTranslationVisitor ttVisitor) {
38: // Because MetaVariables are currently not translated, this method should not be called!
39: throw new UnsupportedOperationException();
40: }
41: }
|