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.logic.util;
009:
010: import de.uka.ilkd.key.java.Services;
011: import de.uka.ilkd.key.logic.Term;
012: import de.uka.ilkd.key.logic.op.*;
013: import de.uka.ilkd.key.logic.sort.Sort;
014:
015: /**
016: * Provides some helper methods used by classes outside the logic package
017: * Please be careful with putting things here. This class has been mainly created
018: * to give getMaxSort a home which is scheduled to become obsolete soon
019: * (see method comment)
020: */
021: public class TermHelper {
022:
023: private TermHelper() {
024: }
025:
026: /**
027: * helper function to determine the maximal sort the term
028: * tSub may have as <tt>i</tt> sub term
029: * This method will become obsolete in the near future as all operators
030: * will become a fixed signature. But currently there ar eto many chnages
031: * pending (new sort hierarchy for integers, new pos) that much of the work would be
032: * for made new. That is the reason for this HACK
033: * @param term the Term of which a part of the <tt>i</tt>-th sub term
034: * may be replaced
035: * @param i an int giving the position of sub term of which a part is to be replaced
036: * @param services the Services object
037: * @return the maximal sort allowed at the i-th position
038: */
039: public static Sort getMaxSort(Term term, int i, Services services) {
040: if (term.sub(i).sort() == Sort.FORMULA)
041: return Sort.FORMULA;
042:
043: if (term.op() instanceof IfThenElse && i > 0) {
044: return term.sort();
045: }
046: return getMaxSortHelper(term.op(), i, term.sub(i).sort(),
047: services);
048: }
049:
050: /**
051: * @param op the Operator whose argument sorts are to be determined
052: * @param i the arguments position
053: * @param maxSortDefault if argument sort cannot be determined
054: * @param services the Services object
055: * @return the maximal sort allowed at argument <tt>i</tt>
056: */
057: private static Sort getMaxSortHelper(final Operator op, int i,
058: Sort maxSortDefault, Services services) {
059: final Sort newMaxSort;
060: if (op instanceof Function) {
061: newMaxSort = ((Function) op).argSort(i);
062: } else if (i == 0 && op instanceof AttributeOp) {
063: newMaxSort = ((AttributeOp) op).getContainerType()
064: .getSort();
065: } else if (i == 0 && op instanceof ArrayOp) {
066: newMaxSort = ((ArrayOp) op).arraySort();
067: } else if (op instanceof AccessOp) {
068: newMaxSort = services.getTypeConverter().getIntegerLDT()
069: .targetSort();
070: } else if (op instanceof Equality) {
071: newMaxSort = ((Equality) op).argSort(i);
072: } else if (op instanceof IUpdateOperator) {
073: newMaxSort = maxSortIUpdate((IUpdateOperator) op, i,
074: maxSortDefault, services);
075: } else {
076: newMaxSort = maxSortDefault;
077: }
078: return newMaxSort;
079: }
080:
081: /**
082: *
083: * looks up if the given subterm position describes a value
084: */
085: private static Sort maxSortIUpdate(IUpdateOperator op, int pos,
086: Sort maxSortDefault, Services services) {
087: if (op.targetPos() != pos) {
088: for (int i = 0, locs = op.locationCount(); i < locs; i++) {
089: final int valuePos = op.valuePos(i);
090: if (valuePos == pos) {
091: return Sort.ANY; //op.location(i).sort() would be more precise
092: // but the current solution is also sound
093: // as the update application rules take care
094: // of inserting casts when necessary
095: } else if (pos < valuePos) {
096: if (op.locationSubtermsBegin(i) <= pos
097: && pos < op.locationSubtermsEnd(i)) {
098: return getMaxSortHelper(op.location(i), pos
099: - op.locationSubtermsBegin(i),
100: maxSortDefault, services);
101: }
102: }
103: }
104: }
105: return maxSortDefault;
106: }
107:
108: }
|