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: package de.uka.ilkd.key.visualdebugger;
009:
010: import java.io.IOException;
011: import java.util.HashMap;
012: import java.util.Iterator;
013: import java.util.LinkedList;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.IteratorOfTerm;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.op.CastFunctionSymbol;
019: import de.uka.ilkd.key.logic.op.SortDependingFunction;
020: import de.uka.ilkd.key.pp.*;
021: import de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObject;
022:
023: public class DebuggerLP extends LogicPrinter {
024: Abb abb = new Abb();
025:
026: NotationInfo info;
027:
028: HashMap inputValues;
029:
030: LinkedList objects = new LinkedList();
031:
032: Services services;
033:
034: SymbolicObject this Object;
035:
036: final VisualDebugger vd = VisualDebugger.getVisualDebugger();
037:
038: public DebuggerLP(ProgramPrinter prgPrinter,
039: NotationInfo notationInfo, Services services,
040: HashMap inputValues) {
041: super (prgPrinter, notationInfo, services);
042: // TODO Auto-generated constructor stub
043: notationInfo.setAbbrevMap(new AbbrevMap());
044: info = notationInfo;
045: this .inputValues = inputValues;
046: this .services = services;
047:
048: }
049:
050: public DebuggerLP(ProgramPrinter prgPrinter,
051: NotationInfo notationInfo, Services services,
052: HashMap inputValues, LinkedList objects,
053: SymbolicObject this Object) {
054: super (prgPrinter, notationInfo, services);
055: info = notationInfo;
056: this .objects = objects;
057: this .this Object = this Object;
058: this .inputValues = inputValues;
059: this .services = services;
060: this .createAb();
061: }
062:
063: private void createAb() {
064: Iterator it = objects.iterator();
065: // info.set
066: // System.out.println(t);
067: while (it.hasNext()) {
068:
069: SymbolicObject so = (SymbolicObject) it.next();
070: // System.out.println(so.getName());
071: // if (so.getTerms().contains(t))
072: for (IteratorOfTerm tit = so.getTerms().iterator(); tit
073: .hasNext();)
074: try {
075: Term t = tit.next();
076: if (so != this Object) {
077: if (!abb.containsTerm(t))
078: abb.put(t, so.getInstanceName(), true);
079: } else if (!abb.containsTerm(t))
080: abb.put(t, "this", true);
081: } catch (AbbrevException e) {
082: e.printStackTrace();
083: }
084:
085: }
086: // abb.put(thisObject., abbreviation, enabled)
087: info.setAbbrevMap(abb);
088: }
089:
090: private String getName(Term t) {
091: Iterator it = objects.iterator();
092:
093: while (it.hasNext()) {
094:
095: SymbolicObject so = (SymbolicObject) it.next();
096:
097: if (so.getTerms().contains(t))
098: return so.getInstanceName();
099: }
100:
101: return null;
102: }
103:
104: public void printCast(String pre, String post, Term t, int ass)
105: throws IOException {
106: final CastFunctionSymbol cast = (CastFunctionSymbol) t.op();
107: // startTerm(t.arity());
108: // layouter.print(pre);
109: // System.out.println("PRE: "+pre);
110: // System.out.println("Post: "+post);
111: //
112: // System.out.println("csat "+cast.getSortDependingOn().toString());
113: // layouter.print(cast.getSortDependingOn().toString());
114: // layouter.print(post);
115: // maybeParens(t.sub(0), ass);
116: printTerm(t.sub(0));
117: }
118:
119: public void printFunctionTerm(String name, Term t)
120: throws IOException {
121: String s = null;// = this.getName(t);
122: // System.out.println("PF "+ t);
123: if (s != null) {
124: startTerm(0);
125: layouter.print(s);
126: } else
127: super .printFunctionTerm(name, t);
128:
129: }
130:
131: public void printTerm(Term t) throws IOException {
132: if (getNotationInfo().getAbbrevMap().isEnabled(t)) {
133: startTerm(0);
134: layouter.print(getNotationInfo().getAbbrevMap()
135: .getAbbrev(t));
136: } else {
137: String s = this .getName(t);
138: if (s != null) {
139: startTerm(0);
140: layouter.print(s);
141: } else
142:
143: if (inputValues.containsKey(t)) {
144: startTerm(0);
145: final Term it = (Term) inputValues.get(t);
146:
147: if ((!vd.isStaticMethod() && !vd.getSelfTerm().equals(
148: it))
149: || vd.isStaticMethod())
150: layouter.print(it.toString() + "_i");
151: // else if (vd.isStaticMethod());
152: else
153: layouter.print(it.toString());
154: } else {
155: if (t.op() instanceof SortDependingFunction
156: && ((SortDependingFunction) t.op()).name()
157: .toString().endsWith("<get>")) {
158: Term sub = t.sub(0);
159: if (sub.arity() > 1)
160: layouter.print("new" + t.sort()
161: + sub.sub(0).toString());
162: else
163: layouter.print("new" + t.sort() + "0");
164: } else
165:
166: getNotationInfo().getNotation(t.op(), services)
167: .print(t, this );
168: }
169: }
170: }
171:
172: class Abb extends AbbrevMap {
173:
174: // public String getAbbrev(Term t){
175: // return super.getAbbrev(t).substring(1);
176: // }
177:
178: /**
179: * Changes the abbreviation of t to abbreviation. If the AbbrevMap
180: * doesn't contain t nothing happens.
181: */
182: public void changeAbbrev(Term t, String abbreviation)
183: throws AbbrevException {
184: if (containsTerm(t)) {
185: AbbrevWrapper scw;
186: // if(containsAbbreviation(abbreviation)){
187: // throw new AbbrevException("The abbreviation "+abbreviation+"
188: // is already"+
189: // " in use for: "+getTerm(abbreviation),false);
190: // }
191: scw = new AbbrevWrapper(t);
192: stringterm.remove(termstring.get(scw));
193: termstring.put(scw, abbreviation);
194: stringterm.put(abbreviation, scw);
195: }
196: }
197:
198: /**
199: * Returns true if the map contains the abbreviation s.
200: */
201: public boolean containsAbbreviation(String s) {
202: return stringterm.containsKey(s);
203: }
204:
205: /**
206: * Returns true if the map contains the term t.
207: */
208: public boolean containsTerm(Term t) {
209: return termstring.containsKey(new AbbrevWrapper(t));
210: }
211:
212: /**
213: * Returns the abbreviation mapped to the term t. Returns null if no
214: * abbreviation is mapped to t.
215: */
216: public String getAbbrev(Term t) {
217: return (String) termstring.get(new AbbrevWrapper(t));
218: }
219:
220: /**
221: * Returns the term which is mapped to the abbreviation s, null if no
222: * term is mapped to the abbreviation.
223: */
224: public Term getTerm(String s) {
225: return ((AbbrevWrapper) stringterm.get(s)).getTerm();
226: }
227:
228: /**
229: * Returns true if the mapping is enabled, which means that the
230: * abbreviation may be used.
231: */
232: public boolean isEnabled(Term t) {
233: Boolean b = (Boolean) termenabled.get(new AbbrevWrapper(t));
234: if (b != null)
235: return b.booleanValue();
236: return false;
237: }
238:
239: /**
240: * Associates a Term and its abbreviation in this map.
241: *
242: * @param t
243: * a term
244: * @param abbreviation
245: * the abbreviation for of this term
246: * @param enabled
247: * true if the abbreviation should be used (e.g. when
248: * printing the term), false otherwise.
249: */
250: public void put(Term t, String abbreviation, boolean enabled)
251: throws AbbrevException {
252: AbbrevWrapper scw;
253: if (containsTerm(t)) {
254: throw new AbbrevException("A abbreviation for " + t
255: + " already exists", true);
256: }
257: // if(containsAbbreviation(abbreviation)){
258: // throw new AbbrevException("The abbreviation "+abbreviation+" is
259: // already"+
260: // " in use for: "+getTerm(abbreviation),false);
261: // }
262: scw = new AbbrevWrapper(t);
263: termstring.put(scw, abbreviation);
264: stringterm.put(abbreviation, scw);
265: termenabled.put(scw, enabled ? TRUE : FALSE);
266: }
267:
268: /**
269: * Sets the mapping of the term t to its abbreviation enabled or
270: * disabled
271: *
272: * @param t
273: * a Term
274: * @param enabled
275: * true if the abbreviation of t may be used.
276: */
277: public void setEnabled(Term t, boolean enabled) {
278: termenabled.put(new AbbrevWrapper(t), enabled ? TRUE
279: : FALSE);
280: }
281:
282: }
283:
284: class AbbrevWrapper {
285:
286: private Term t;
287:
288: public AbbrevWrapper(Term t) {
289: this .t = t;
290: }
291:
292: public boolean equals(Object o) {
293: if (!(o instanceof AbbrevWrapper))
294: return false;
295: AbbrevWrapper scw = (AbbrevWrapper) o;
296: if (scw.getTerm() == t)
297: return true;
298: return t.equals(scw.getTerm());
299: }
300:
301: public Term getTerm() {
302: return t;
303: }
304:
305: public int hashCode() {
306: return t.hashCode();
307: }
308:
309: }
310:
311: }
|