001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.pp;
012:
013: import java.util.HashMap;
014:
015: import de.uka.ilkd.key.logic.Term;
016:
017: public class AbbrevMap {
018:
019: /**
020: * HashMaps used to store the mappings from Term to String, String to Term
021: * and Term to Enabled. Enabled is set true if a abbreviation should be used when
022: * printing the term.
023: */
024: protected HashMap termstring, stringterm, termenabled;
025: protected Boolean TRUE = new Boolean(true);
026: protected Boolean FALSE = new Boolean(false);
027:
028: /**
029: * Creates a AbbrevMap.
030: */
031: public AbbrevMap() {
032: termstring = new HashMap();
033: stringterm = new HashMap();
034: termenabled = new HashMap();
035: }
036:
037: /**
038: * Associates a Term and its abbreviation in this map.
039: * @param t a term
040: * @param abbreviation the abbreviation for of this term
041: * @param enabled true if the abbreviation should be used
042: * (e.g. when printing the term), false otherwise.
043: */
044: public void put(Term t, String abbreviation, boolean enabled)
045: throws AbbrevException {
046: AbbrevWrapper scw;
047: if (containsTerm(t)) {
048: throw new AbbrevException("A abbreviation for " + t
049: + " already exists", true);
050: }
051: if (containsAbbreviation(abbreviation)) {
052: throw new AbbrevException("The abbreviation "
053: + abbreviation + " is already" + " in use for: "
054: + getTerm(abbreviation), false);
055: }
056: scw = new AbbrevWrapper(t);
057: termstring.put(scw, abbreviation);
058: stringterm.put(abbreviation, scw);
059: termenabled.put(scw, enabled ? TRUE : FALSE);
060: }
061:
062: /**
063: * Changes the abbreviation of t to abbreviation. If the AbbrevMap doesn't
064: * contain t nothing happens.
065: */
066: public void changeAbbrev(Term t, String abbreviation)
067: throws AbbrevException {
068: if (containsTerm(t)) {
069: AbbrevWrapper scw;
070: if (containsAbbreviation(abbreviation)) {
071: throw new AbbrevException("The abbreviation "
072: + abbreviation + " is already"
073: + " in use for: " + getTerm(abbreviation),
074: false);
075: }
076: scw = new AbbrevWrapper(t);
077: stringterm.remove(termstring.get(scw));
078: termstring.put(scw, abbreviation);
079: stringterm.put(abbreviation, scw);
080: }
081: }
082:
083: /**
084: * Returns true if the map contains the abbreviation s.
085: */
086: public boolean containsAbbreviation(String s) {
087: return stringterm.containsKey(s);
088: }
089:
090: /**
091: * Returns true if the map contains the term t.
092: */
093: public boolean containsTerm(Term t) {
094: return termstring.containsKey(new AbbrevWrapper(t));
095: }
096:
097: /**
098: * Returns the term which is mapped to the abbreviation s, null if no term
099: * is mapped to the abbreviation.
100: */
101: public Term getTerm(String s) {
102: return ((AbbrevWrapper) stringterm.get(s)).getTerm();
103: }
104:
105: /**
106: * Returns the abbreviation mapped to the term t. Returns null if no abbreviation
107: * is mapped to t.
108: */
109: public String getAbbrev(Term t) {
110: return "@" + (String) termstring.get(new AbbrevWrapper(t));
111: }
112:
113: /**
114: * Returns true if the mapping is enabled, which means that the abbreviation may
115: * be used.
116: */
117: public boolean isEnabled(Term t) {
118: Boolean b = (Boolean) termenabled.get(new AbbrevWrapper(t));
119: if (b != null)
120: return b.booleanValue();
121: return false;
122: }
123:
124: /**
125: * Sets the mapping of the term t to its abbreviation enabled or disabled
126: * @param t a Term
127: * @param enabled true if the abbreviation of t may be used.
128: */
129: public void setEnabled(Term t, boolean enabled) {
130: termenabled.put(new AbbrevWrapper(t), enabled ? TRUE : FALSE);
131: }
132:
133: }
134:
135: class AbbrevWrapper {
136:
137: private Term t;
138:
139: public AbbrevWrapper(Term t) {
140: this .t = t;
141: }
142:
143: public int hashCode() {
144: return t.hashCode();
145: }
146:
147: public boolean equals(Object o) {
148: if (!(o instanceof AbbrevWrapper))
149: return false;
150: AbbrevWrapper scw = (AbbrevWrapper) o;
151: if (scw.getTerm() == t)
152: return true;
153: return t.equals(scw.getTerm());
154: }
155:
156: public Term getTerm() {
157: return t;
158: }
159: }
|