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.logic.Term;
14: import de.uka.ilkd.key.logic.op.SVSubstitute;
15: import de.uka.ilkd.key.rule.MatchConditions;
16: import de.uka.ilkd.key.logic.op.MetaOperator;
17: import de.uka.ilkd.key.rule.inst.SVInstantiations;
18:
19: /** this class implements the interface for
20: * MetaAdderators. MetaAdderators are used to do complex term
21: * transformation when applying a taclet. Often these transformation
22: * caanot be described with the taclet scheme (or trying to do so would
23: * result in a huge number of rules)
24: */
25: public class MetaAttribute extends MetaField {
26:
27: private String attrName;
28:
29: public MetaAttribute() {
30: super ("#attribute");
31: }
32:
33: public MetaAttribute(String attrName) {
34: super ("#attribute" + attrName);
35: this .attrName = attrName;
36: }
37:
38: /** calculates the resulting term. */
39: public Term calculate(Term term, SVInstantiations svInst,
40: Services services) {
41: // This is still not really right, one would need something of the `@' notation thing
42: return termFactory.createAttributeTerm(services.getJavaInfo()
43: .getAllAttributes(
44: attrName,
45: services.getJavaInfo().getKeYJavaType(
46: term.sub(0).sort())).head(), term
47: .sub(0));
48: }
49:
50: /** (non-Javadoc)
51: * by default meta operators do not match anything
52: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
53: */
54: public MatchConditions match(SVSubstitute subst,
55: MatchConditions mc, Services services) {
56: return null;
57: }
58:
59: public MetaOperator getParamMetaOperator(String param) {
60: MetaOperator mop = name2metaop("#attribute_" + param);
61: if (mop != null)
62: return mop;
63: return new MetaAttribute(param);
64: }
65:
66: }
|