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.rule.conditions;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.op.SVSubstitute;
015: import de.uka.ilkd.key.logic.op.SchemaVariable;
016: import de.uka.ilkd.key.logic.sort.Sort;
017: import de.uka.ilkd.key.rule.VariableConditionAdapter;
018: import de.uka.ilkd.key.rule.inst.SVInstantiations;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * ensures that the types where the variables are declared are not the same
023: */
024: public class TypeComparisionCondition extends VariableConditionAdapter {
025:
026: /** checks if sorts are not same */
027: public final static int NOT_SAME = 0;
028: /** checks if sorts are not compatible */
029: public final static int NOT_COMPATIBLE = 1;
030: /** checks subtype relationship */
031: public final static int IS_SUBTYPE = 2;
032: /** checks subtype relationship */
033: public final static int NOT_IS_SUBTYPE = 3;
034: /** check for strict subtype */
035: public static final int STRICT_SUBTYPE = 4;
036: /** checks if sorts are same */
037: public final static int SAME = 5;
038:
039: private final int mode;
040: private final TypeResolver fst;
041: private final TypeResolver snd;
042:
043: /**
044: * creates a condition that checks if the declaration types of the
045: * schemavariable's instantiations are unequal
046: * @param fstType one of the SchemaVariable whose type is checked
047: * @param sndType one of the SchemaVariable whose type is checked
048: * @param mode an int encoding if testing of not same or not compatible
049: */
050: public TypeComparisionCondition(TypeResolver fst, TypeResolver snd,
051: int mode) {
052: this .fst = fst;
053: this .snd = snd;
054: this .mode = mode;
055: }
056:
057: /**
058: * tests if the instantiations for both schema variables have a
059: * different type
060: * @param var the template Variable to be instantiated
061: * @param subst the SVSubstitute to be mapped to var
062: * @param svInst the SVInstantiations that are already known to be
063: * needed
064: * @return true iff condition is fulfilled
065: */
066: public boolean check(SchemaVariable var, SVSubstitute subst,
067: SVInstantiations svInst, Services services) {
068:
069: if (!fst.isComplete(var, subst, svInst, services)
070: || !snd.isComplete(var, subst, svInst, services)) {
071: // not yet complete
072: return true;
073: }
074:
075: return checkSorts(
076: fst.resolveSort(var, subst, svInst, services), snd
077: .resolveSort(var, subst, svInst, services));
078: }
079:
080: private boolean checkSorts(final Sort fstSort, final Sort sndSort) {
081: switch (mode) {
082: case SAME:
083: return fstSort == sndSort;
084: case NOT_SAME:
085: return fstSort != sndSort;
086: case NOT_COMPATIBLE:
087: return !(fstSort.extendsTrans(sndSort) || sndSort
088: .extendsTrans(fstSort));
089: case IS_SUBTYPE:
090: return fstSort.extendsTrans(sndSort);
091: case STRICT_SUBTYPE:
092: return fstSort != sndSort && fstSort.extendsTrans(sndSort);
093: case NOT_IS_SUBTYPE:
094: return !fstSort.extendsTrans(sndSort);
095: default:
096: Debug.fail("TypeComparisionCondition: " + "Unknown mode.");
097: return false;
098: }
099: }
100:
101: public String toString() {
102: switch (mode) {
103: case SAME:
104: return "\\same(" + fst + ", " + snd + ")";
105: case NOT_COMPATIBLE:
106: return "\\not\\compatible(" + fst + ", " + snd + ")";
107: case NOT_SAME:
108: return "\\not\\same(" + fst + ", " + snd + ")";
109: case IS_SUBTYPE:
110: return "\\sub(" + fst + ", " + snd + ")";
111: case STRICT_SUBTYPE:
112: return "\\strict\\sub(" + fst + ", " + snd + ")";
113: case NOT_IS_SUBTYPE:
114: return "\\not\\sub(" + fst + ", " + snd + ")";
115: default:
116: return "invalid type copmparision mode";
117: }
118: }
119:
120: }
|