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: package de.uka.ilkd.key.rule.metaconstruct;
11:
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.java.expression.Literal;
14: import de.uka.ilkd.key.logic.Name;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
17: import de.uka.ilkd.key.logic.op.Operator;
18: import de.uka.ilkd.key.logic.op.ProgramConstant;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: /**
22: * Replace a program variable that is a compile-time constant with the
23: * value of the initializer
24: */
25: public class ConstantValue extends AbstractMetaOperator {
26:
27: public ConstantValue() {
28: super (new Name("#constantvalue"), 1);
29: }
30:
31: /**
32: * checks whether the top level structure of the given @link Term
33: * is syntactically valid, given the assumption that the top level
34: * operator of the term is the same as this Operator. The
35: * assumption that the top level operator and the term are equal
36: * is NOT checked.
37: * @return true iff the top level structure of
38: * the @link Term is valid.
39: */
40: public boolean validTopLevel(Term term) {
41: // a meta operator accepts almost everything
42: return term.arity() == arity();
43: }
44:
45: /** calculates the resulting term. */
46: public Term calculate(Term term, SVInstantiations svInst,
47: Services services) {
48: term = term.sub(0);
49: Operator op = term.op();
50:
51: if (op instanceof ProgramConstant) {
52: Literal lit = ((ProgramConstant) op)
53: .getCompileTimeConstant();
54: if (lit != null)
55: term = services.getTypeConverter()
56: .convertToLogicElement(lit);
57: }
58:
59: return term;
60: }
61:
62: }
|