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.Term;
15: import de.uka.ilkd.key.logic.op.Location;
16: import de.uka.ilkd.key.logic.sort.ObjectSort;
17: import de.uka.ilkd.key.logic.sort.Sort;
18: import de.uka.ilkd.key.parser.KeYSemanticException;
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 MetaNextToCreate extends MetaField implements Location {
28:
29: public MetaNextToCreate() {
30: super ("#nextToCreate", false);
31: }
32:
33: /** calculates the resulting term.
34: * @throws KeYSemanticException */
35: public Term calculate(Term term, SVInstantiations svInst,
36: Services services) {
37:
38: final Term t = term.sub(0);
39:
40: final Sort s = t.sort();
41:
42: if (!(s instanceof ObjectSort)) {
43: throw new RuntimeException("Wrong usage of meta operator "
44: + this
45: + ". Sort of subterm is not an ObjectSort, but "
46: + s);
47: }
48:
49: return termFactory.createVariableTerm(services.getJavaInfo()
50: .getAttribute(
51: ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE,
52: (ObjectSort) s));
53: }
54:
55: public boolean mayBeAliasedBy(Location loc) {
56: return true;
57: }
58:
59: public Sort sort() {
60: return METASORT;
61: }
62:
63: }
|