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 de.uka.ilkd.key.java.expression.Literal;
013: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
014: import de.uka.ilkd.key.java.expression.literal.StringLiteral;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.Namespace;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.TermFactory;
019: import de.uka.ilkd.key.logic.ldt.LDT;
020: import de.uka.ilkd.key.logic.op.Function;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: public class StringConverter {
024:
025: /** used for the pretty printer*/
026: Function ppCat;
027: static final String EPSILON = "epsilon";
028: static final String CAT = "cat";
029:
030: /** translates a given literal to its logic counterpart.
031: * the string has to be enclosed by quotation marks.
032: */
033:
034: public Term translateLiteral(Literal lit, LDT intLDT, Services serv) {
035: Namespace funcNs = serv.getNamespaces().functions();
036: Function epsilon = (Function) funcNs.lookup(new Name(EPSILON));
037: assert epsilon != null;
038: Function cat = (Function) funcNs.lookup(new Name(CAT));
039: assert cat != null;
040: ppCat = cat;
041: Term term_epsilon = TermFactory.DEFAULT
042: .createFunctionTerm(epsilon);
043:
044: char[] charArray;
045: Term result = term_epsilon;
046:
047: if (lit instanceof StringLiteral)
048: charArray = ((StringLiteral) lit).getValue().toCharArray();
049: else
050: return null;
051: if (intLDT == null)
052: throw new IllegalArgumentException(
053: "IntLDT is needed for StringLiteral translation");//return term_epsilon;
054: for (int i = charArray.length - 2; i >= 1; i--) {
055: result = TermFactory.DEFAULT.createFunctionTerm(cat, intLDT
056: .translateLiteral(new IntLiteral(charArray[i])),
057: result);
058: }
059: return result;
060: }
061:
062: private StringBuffer printlastfirst(Term t) {
063: if (t.op().arity() == 0) {
064: return new StringBuffer();
065: } else {
066: return printlastfirst(t.sub(0)).append(
067: t.op().name().toString());
068: }
069: }
070:
071: private String translateCharTerm(Term t) {
072: char charVal = 0;
073: int intVal = 0;
074: String result = printlastfirst(t.sub(0)).toString();
075: try {
076: intVal = Integer.parseInt(result);
077: charVal = (char) intVal;
078: if (intVal - charVal != 0)
079: throw new NumberFormatException(); //overflow!
080:
081: } catch (NumberFormatException ex) {
082: throw new ConvertException(result + " is not of type char");
083: }
084: return new Character(charVal).toString();
085: }
086:
087: /** translates a term that represents a string into a string literal
088: * that is enclosed by quotation marks
089: */
090:
091: public Expression translateTerm(Term t, ExtList children) {
092: final StringBuffer result = new StringBuffer("");
093: Term term = t;
094: while (term.op().arity() != 0) {
095: result.append(translateCharTerm(term.sub(0)));
096: term = term.sub(1);
097: }
098: return new StringLiteral("\"" + result + "\"");
099: }
100:
101: /** @return the function symbol that is used to build strings*/
102: public Function getStringSymbol() {
103: return ppCat;
104: }
105:
106: }
|