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:
11: package de.uka.ilkd.key.logic.op;
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.sort.Sort;
17: import de.uka.ilkd.key.rule.MatchConditions;
18: import de.uka.ilkd.key.util.Debug;
19:
20: /**
21: * The abstract class term symbol implements common features of several
22: * symbols occuring as part of a term (formula). For example common getters for
23: * name and sort of the symbol.
24: */
25: public abstract class TermSymbol implements Operator {
26:
27: /** name of this symbol */
28: private final Name name;
29:
30: /**
31: * sort of the term symbol
32: */
33: private final Sort sort;
34:
35: /**
36: * creates a new term symbol of the given name and sort
37: * @param name the Name of the symbol
38: * @param sort the Sort of the symbol
39: */
40: protected TermSymbol(Name name, Sort sort) {
41: this .name = name;
42: this .sort = sort;
43: }
44:
45: /** @return Sort of the TermSymbol */
46: public Sort sort(Term[] term) {
47: return sort;
48: }
49:
50: /** @return true iff number of subterms of term is equal to its own arity
51: */
52: public boolean validTopLevel(Term term) {
53: return term.arity() == this .arity();
54: }
55:
56: /** @return name of the TermSymbol */
57: public Name name() {
58: return name;
59: }
60:
61: /** @return Sort of this */
62: public Sort sort() {
63: return sort;
64: }
65:
66: /**
67: * @return true if the value of "term" having this operator as
68: * top-level operator and may not be changed by modalities
69: */
70: public boolean isRigid(Term term) {
71: return term.hasRigidSubterms();
72: }
73:
74: /**
75: * implements the default operator matching rule which means
76: * that the compared object have to be equal otherwise
77: * matching fails
78: */
79: public MatchConditions match(SVSubstitute subst,
80: MatchConditions mc, Services services) {
81: if (subst == this ) {
82: return mc;
83: }
84: Debug.out("Operators are different(template, candidate)", this,
85: subst);
86: return null;
87: }
88: }
|