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.logic.Name;
14: import de.uka.ilkd.key.logic.sort.Sort;
15:
16: class TermSV extends AbstractTermSV {
17:
18: /**
19: * this flag indicates if the instantiation of this schemavariable must have
20: * the same static type (sort) as this SV itself
21: */
22: private final boolean strictSV;
23:
24: /** creates a new SchemaVariable. That is used as placeholder for
25: * terms.
26: * @param name the Name of the SchemaVariable
27: * @param sort the Sort of the SchemaVariable and the matched type
28: * @param listSV a boolean which is true iff the schemavariable is allowed
29: * to match a list of terms
30: * @param rigidness true iff this SV may only match rigid
31: * terms/formulas
32: * @param strictSV boolean indicating if the schemavariable is declared as strict
33: * forcing exact type match
34: */
35: TermSV(Name name, Sort sort, boolean listSV, boolean rigidness,
36: boolean strictSV) {
37: super (name, sort, listSV, rigidness);
38: this .strictSV = strictSV;
39: if (sort == Sort.FORMULA) {
40: throw new RuntimeException("A TermSV is not allowed to"
41: + " have the sort " + sort);
42: }
43: }
44:
45: /** returns true iff this SchemaVariable is used to match
46: * a term but not a formula
47: * @return true iff this SchemaVariable is used to match
48: * a term but not a formula
49: */
50: public boolean isTermSV() {
51: return true;
52: }
53:
54: /**
55: * @return true if the schemavariable has the strict modifier
56: * which forces the instantiation to have exact the same sort
57: * as the schemavariable (or if the sv is of generic sort -
58: * the instantiation of the generic sort)
59: */
60: public boolean isStrict() {
61: return strictSV;
62: }
63:
64: /** toString */
65: public String toString() {
66: return toString(sort().toString() + " term");
67: }
68: }
|