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.ShadowReplaceVisitor;
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.Location;
18: import de.uka.ilkd.key.logic.op.SVSubstitute;
19: import de.uka.ilkd.key.logic.sort.Sort;
20: import de.uka.ilkd.key.rule.MatchConditions;
21: import de.uka.ilkd.key.rule.inst.SVInstantiations;
22:
23: /** this class implements the interface for
24: * MetaAdderators. MetaAdderators are used to do complex term
25: * transformation when applying a taclet. Often these transformation
26: * caanot be described with the taclet scheme (or trying to do so would
27: * result in a huge number of rules)
28: */
29: public class MetaShadow extends AbstractMetaOperator implements
30: Location {
31:
32: public MetaShadow() {
33: super (new Name("#shadowed"), 1);
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: /** calculates the resulting term. */
55: public Term calculate(Term term, SVInstantiations svInst,
56: Services services) {
57: ShadowReplaceVisitor shadowreplace = new ShadowReplaceVisitor(
58: services);
59: term.sub(0).execPostOrder(shadowreplace);
60: return shadowreplace.getTerm();
61: // return term.sub(0); // don't do anything (i.e no shadowing for now)
62: // return termFactory.createAttributeTerm
63: // (javaInfo.getAttribute("length", javaInfo.getKeYJavaType(term.sub(0).sort())),
64: // term.sub(0));
65: }
66:
67: /**
68: */
69: public Sort sort() {
70: return METASORT;
71: }
72:
73: /* (non-Javadoc)
74: * @see de.uka.ilkd.key.logic.op.Location#mayBeAliasedBy(de.uka.ilkd.key.logic.op.Location)
75: */
76: public boolean mayBeAliasedBy(Location loc) {
77: return true;
78: }
79:
80: /** (non-Javadoc)
81: * by default meta operators do not match anything
82: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
83: */
84: public MatchConditions match(SVSubstitute subst,
85: MatchConditions mc, Services services) {
86: return null;
87: }
88:
89: }
|