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