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.logic.op;
11:
12: import de.uka.ilkd.key.logic.Name;
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.sort.Sort;
15:
16: public class Metavariable extends TermSymbol implements
17: ParsableVariable, Comparable {
18:
19: // Used to define an alternative order of all existing
20: // metavariables
21: private static int maxSerial = 0;
22: private int serial;
23:
24: private final boolean isTemporaryVariable;
25:
26: private synchronized void setSerial() {
27: serial = maxSerial++;
28: }
29:
30: private Metavariable(Name name, Sort sort,
31: boolean isTemporaryVariable) {
32: super (name, sort);
33: if (sort == Sort.FORMULA) {
34: throw new RuntimeException(
35: "Attempt to create metavariable of type formula");
36: }
37: this .isTemporaryVariable = isTemporaryVariable;
38: setSerial();
39: }
40:
41: public Metavariable(Name name, Sort sort) {
42: this (name, sort, false);
43: }
44:
45: public static Metavariable createTemporaryVariable(Name name,
46: Sort sort) {
47: return new Metavariable(name, sort, true);
48: }
49:
50: /** @return true iff number of subterms of term is 0
51: */
52: public boolean validTopLevel(Term term) {
53: return term.arity() == 0;
54: }
55:
56: public String toString() {
57: return name() + ":" + sort();
58: }
59:
60: /** @return arity of the Metavariable as int */
61: public int arity() {
62: return 0;
63: }
64:
65: public int compareTo(Object p) {
66: if (p == this )
67: return 0;
68: if (p == null)
69: throw new NullPointerException();
70:
71: // throws a ClassCastException on error
72: final Metavariable cmp = (Metavariable) p;
73:
74: // temporary variables are the greatest ones
75: if (isTemporaryVariable()) {
76: if (!cmp.isTemporaryVariable())
77: return 1;
78: } else {
79: if (cmp.isTemporaryVariable())
80: return -1;
81: }
82:
83: int t = name().toString().compareTo(cmp.name().toString());
84: if (t == 0)
85: return serial < (cmp).serial ? -1 : 1;
86: return t;
87: }
88:
89: /**
90: * @return Returns the isTemporaryVariable.
91: */
92: public boolean isTemporaryVariable() {
93: return isTemporaryVariable;
94: }
95: }
|