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: package de.uka.ilkd.key.java;
011:
012: import java.util.HashMap;
013: import java.util.Set;
014:
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.util.Debug;
017:
018: public class KeYRecoderMapping {
019:
020: /** have special classes been parsed in */
021: private boolean parsedSpecial = false;
022:
023: /** maps a recoder programelement (or something similar, e.g. Type)
024: * to the KeY-equivalent
025: */
026: private HashMap map;
027:
028: /** maps a KeY programelement to the Recoder-equivalent */
029: private HashMap revMap;
030:
031: /** a pseudo super class for all arrays used to declare length */
032: private KeYJavaType super ArrayType = null;
033:
034: public KeYRecoderMapping() {
035: this .map = new HashMap();
036: this .revMap = new HashMap();
037: }
038:
039: /**
040: * creates a KeYRecoderMapping object
041: * @param map a HashMap mapping ProgramElements in Recoder to
042: * ProgramElements in KeY
043: * @param revMap the reverse map (KeY->Recoder)
044: * @param parsedSpecial boolean indicating if the special classes have been parsed in
045: */
046: public KeYRecoderMapping(HashMap map, HashMap revMap,
047: KeYJavaType super ArrayType, boolean parsedSpecial) {
048: this .map = map;
049: this .revMap = revMap;
050: this .super ArrayType = super ArrayType;
051: this .parsedSpecial = parsedSpecial;
052: }
053:
054: /**
055: * returns a matching ProgramElement (KeY) to a given
056: * ProgramElement (Recoder)
057: * @param pe a recoder.java.ProgramElement
058: */
059: public ProgramElement toKeY(recoder.java.ProgramElement pe) {
060: return (ProgramElement) map.get(pe);
061: }
062:
063: /**
064: * returns a matching ModelElement (KeY) to a given recoder.ModelElement
065: * @param pe a recoder.ModelElement
066: */
067: public ModelElement toKeY(recoder.ModelElement pe) {
068: return (ModelElement) map.get(pe);
069: }
070:
071: /**
072: * returns the Recoder-equivalent to a given ProgramElement (KeY).
073: * If there's no RecodeR equivalent to program element pe, an
074: * assertion failure "Program Element <pe> not known" is emitted.
075: * @param pe a JavaProgramElement
076: */
077: public recoder.java.ProgramElement toRecoder(ProgramElement pe) {
078: Object res = revMap.get(pe);
079: Debug.assertTrue(res != null, "Program Element not known", pe);
080: return (recoder.java.ProgramElement) res;
081: }
082:
083: /**
084: * returns the Recoder-equivalent to a given ModelElement (KeY).
085: * If there's no Recoder-equivalent to the ModelElement pe a
086: * debug message "Model Element <pe> not known" is printed.
087: * @param pe a ModelElement
088: */
089: public recoder.ModelElement toRecoder(ModelElement pe) {
090: Object res = revMap.get(pe);
091: if (res == null) {
092: //System.out.println(revMap);
093: }
094: Debug.assertTrue(res != null, "Model Element not known", pe);
095:
096: return (recoder.ModelElement) res;
097: }
098:
099: public void put(Object rec, Object key) {
100: Object formerValue = map.put(rec, key);
101: Debug.assertTrue(formerValue == null,
102: "keyrecodermapping: duplicate registration of type:",
103: key);
104: revMap.put(key, rec);
105: }
106:
107: public boolean mapped(Object rec) {
108: return map.containsKey(rec);
109: }
110:
111: public Set elemsKeY() {
112: return revMap.keySet();
113: }
114:
115: public Set elemsRec() {
116: return map.keySet();
117: }
118:
119: public void setSuperArrayType(KeYJavaType super ArrayType) {
120: this .super ArrayType = super ArrayType;
121: }
122:
123: public KeYJavaType getSuperArrayType() {
124: return this .super ArrayType;
125: }
126:
127: public KeYRecoderMapping copy() {
128: return new KeYRecoderMapping((HashMap) map.clone(),
129: (HashMap) revMap.clone(), super ArrayType, parsedSpecial);
130: }
131:
132: /**
133: * As long as we do not support lemmata we need the source code of
134: * some 'java.lang' classes. These are parsed in using method
135: * parseSpecial of {@link Recoder2KeY}. To avoid multiple readings
136: * this method indicates whether the special have been parsed in or
137: * not.
138: * @return true if special classes have been parsed in
139: */
140: public boolean parsedSpecial() {
141: return parsedSpecial;
142: }
143:
144: public int size() {
145: return map.size();
146: }
147:
148: /**
149: * As long as we do not support lemmata we need the source code of
150: * some 'java.lang' classes. These are parsed in using method
151: * parseSpecial of {@link Recoder2KeY}. To avoid multiple readings
152: * this method sets a flag whether the special have been parsed in or
153: * not
154: * @param b boolean indicating if the special classes have been
155: * parsed in
156: */
157: public void parsedSpecial(boolean b) {
158: parsedSpecial = b;
159: }
160:
161: }
|