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.recoderext.ImplicitFieldAdder;
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.SVSubstitute;
18: import de.uka.ilkd.key.rule.MatchConditions;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: /** this class implements the interface for
22: * MetaAdderators. MetaAdderators are used to do complex term
23: * transformation when applying a taclet. Often these transformation
24: * caanot be described with the taclet scheme (or trying to do so would
25: * result in a huge number of rules)
26: */
27: public class MetaTransient extends AbstractMetaOperator {
28:
29: public MetaTransient() {
30: super (new Name("#transient"), 1);
31: }
32:
33: public boolean isRigid(Term t) {
34: return false;
35: }
36:
37: /**
38: * checks whether the top level structure of the given @link Term
39: * is syntactically valid, given the assumption that the top level
40: * operator of the term is the same as this Operator. The
41: * assumption that the top level operator and the term are equal
42: * is NOT checked.
43: * @return true iff the top level structure of
44: * the @link Term is valid.
45: */
46: public boolean validTopLevel(Term term) {
47: // a meta operator accepts almost everything
48: return term.arity() == arity();
49: }
50:
51: /** calculates the resulting term. */
52: public Term calculate(Term term, SVInstantiations svInst,
53: Services services) {
54: return termFactory.createAttributeTerm(services.getJavaInfo()
55: .getAttribute(ImplicitFieldAdder.IMPLICIT_TRANSIENT,
56: services.getJavaInfo().getJavaLangObject()),
57: term.sub(0));
58: }
59:
60: /** (non-Javadoc)
61: * by default meta operators do not match anything
62: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
63: */
64: public MatchConditions match(SVSubstitute subst,
65: MatchConditions mc, Services services) {
66: return null;
67: }
68: }
|