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 15.03.2005
10: */
11: package de.uka.ilkd.key.logic.op;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
16: import de.uka.ilkd.key.logic.sort.Sort;
17:
18: /**
19: * "S::ExactInstanceof" is a function symbol parameterised with sort <code>S</code>
20: * testing if a given argument has sort <code>S</code> as
21: * exact type (dynamic type)
22: */
23: public class ExactInstanceSymbol extends SortDependingFunction {
24:
25: public static final Name NAME = new Name("exactInstance");
26:
27: public ExactInstanceSymbol(Sort p_sort, Sort booleanSort) {
28: super (new Name("" + p_sort.name() + "::" + NAME), booleanSort,
29: new Sort[] { Sort.ANY }, NAME, p_sort);
30: }
31:
32: /**
33: * This operator can be used with arbitrary arguments
34: * (only mixing primitive and reference sorts is not allowed)
35: */
36: public boolean possibleSub(int at, Term possibleSub) {
37: if (possibleSub.op() instanceof SchemaVariable) {
38: return true;
39: }
40: return (possibleSub.sort() instanceof PrimitiveSort) == (getSortDependingOn() instanceof PrimitiveSort);
41:
42: }
43: }
|