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: * Created on Apr 14, 2005
10: */
11: package de.uka.ilkd.key.rule.metaconstruct;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Name;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.TermFactory;
17: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
18: import de.uka.ilkd.key.logic.op.ExactInstanceSymbol;
19: import de.uka.ilkd.key.logic.op.Function;
20: import de.uka.ilkd.key.logic.sort.ArraySort;
21: import de.uka.ilkd.key.logic.sort.ObjectSort;
22: import de.uka.ilkd.key.logic.sort.Sort;
23: import de.uka.ilkd.key.logic.sort.SortDefiningSymbols;
24: import de.uka.ilkd.key.rule.inst.SVInstantiations;
25: import de.uka.ilkd.key.util.Debug;
26:
27: /**
28: * Creates an <tt>Type::instance(..)</tt> term for the component type of the
29: * array. The component type has to be a reference type.
30: */
31: public class ArrayBaseInstanceOf extends AbstractMetaOperator {
32:
33: public ArrayBaseInstanceOf() {
34: super (new Name("#arrayBaseInstanceOf"), 2);
35: }
36:
37: /**
38: * returns an <tt>G::instance(term.sub(1))</tt> term for the element sort of
39: * the given array . It is assumed that <tt>term.sub(0)</tt> is either a term of
40: * reference array sort or a term with an <tt>exactInstance</tt> symbol as top level
41: * depending on a reference array sort.
42: */
43: public Term calculate(Term term, SVInstantiations svInst,
44: Services services) {
45: final Term array = term.sub(0);
46: final Term element = term.sub(1);
47:
48: final Sort arraySort;
49: if (array.op() instanceof ExactInstanceSymbol) {
50: arraySort = ((ExactInstanceSymbol) array.op())
51: .getSortDependingOn();
52: } else {
53: arraySort = array.sort();
54: }
55:
56: assert arraySort instanceof ArraySort;
57:
58: final Sort arrayElementSort = ((ArraySort) arraySort)
59: .elementSort();
60:
61: Function instanceof Symbol = null;
62: if (arrayElementSort instanceof SortDefiningSymbols) {
63: assert arrayElementSort instanceof ArraySort
64: || arrayElementSort instanceof ObjectSort;
65: instanceof Symbol = (Function) ((SortDefiningSymbols) arrayElementSort)
66: .lookupSymbol(new Name("instance"));
67: }
68: Debug.assertTrue(instanceof Symbol != null,
69: "Instanceof symbol not found for ", arrayElementSort);
70:
71: return TermFactory.DEFAULT.createFunctionTerm(instanceofSymbol,
72: element);
73: }
74:
75: }
|