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.logic.op;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.Name;
015: import de.uka.ilkd.key.logic.sort.*;
016: import de.uka.ilkd.key.rule.MatchConditions;
017: import de.uka.ilkd.key.rule.inst.GenericSortCondition;
018: import de.uka.ilkd.key.rule.inst.SortException;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * A sort depending function is a function symbol.
023: * The following invariant has to hold:<br>
024: * given two sort depending functions f1 and f2 then</br>
025: * from f1.isSimilar(f2) and f1.getSortDependingOn() == f2.getSortDependingOn() <br/>
026: * follows f1 == f2
027: */
028: public class SortDependingFunction extends RigidFunction implements
029: SortDependingSymbol {
030:
031: private final Name kind;
032: private final Sort sortDependingOn;
033:
034: /** creates a Function
035: * @param name String with name of the function
036: * @param sort the Sort of the function (result type)
037: * @param kind name of the kind this object belongs to
038: * @param sortDependingOn sort this object is depending on, this
039: * is the difference between various objects of the same kind
040: */
041: public SortDependingFunction(Name name, Sort sort, Sort[] argSorts,
042: Name kind, Sort sortDependingOn) {
043: super (name, sort, argSorts);
044: this .kind = kind;
045: this .sortDependingOn = sortDependingOn;
046: }
047:
048: public SortDependingFunction(Name name, Sort sort,
049: ArrayOfSort argSorts, Name kind, Sort sortDependingOn) {
050: super (name, sort, argSorts);
051: this .kind = kind;
052: this .sortDependingOn = sortDependingOn;
053: }
054:
055: /**
056: * @return the sort this object has been instantiated for
057: */
058: public Sort getSortDependingOn() {
059: return sortDependingOn;
060: }
061:
062: /**
063: * Compares "this" and "p"
064: * @param p object to compare
065: * @return true iff this and p are instances of the same kind of
066: * symbol, but possibly instantiated for different sorts
067: */
068: public boolean isSimilar(SortDependingSymbol p) {
069: return getKind().equals(p.getKind());
070: }
071:
072: /**
073: * Assign a name to this term symbol, independant of concrete
074: * instantiations for different sorts
075: * @return the kind of term symbol this object is an instantiation
076: * for
077: */
078: public Name getKind() {
079: return kind;
080: }
081:
082: /**
083: * Get the instance of this term symbol defined by the given sort
084: * "p_sort"
085: * @return a term symbol similar to this one, or null if this
086: * symbol is not defined by "p_sort"
087: *
088: * POSTCONDITION: result==null || (this.isSimilar(result) &&
089: * result.getSortDependingOn()==p_sort)
090: */
091: public SortDependingSymbol getInstanceFor(SortDefiningSymbols p_sort) {
092: return p_sort.lookupSymbol(getKind());
093: }
094:
095: /**
096: * tries to match sort <code>s1</code> to fit sort <code>s2</code>
097: * @param s1 Sort tried to matched (maybe concrete or (contain) generic)
098: * @param s2 concrete Sort
099: * @param mc the MatchConditions up to now
100: * @return <code>null</code> if failed the resulting match conditions otherwise
101: */
102: private MatchConditions matchSorts(Sort s1, Sort s2,
103: MatchConditions mc) {
104: Debug
105: .assertFalse(s2 instanceof GenericSort,
106: "Internal Error. Sort s2 is not allowed to be of type generic.");
107: if (!(s1 instanceof GenericSort)) {
108: if (s1.getClass() != s2.getClass()) {
109: Debug.out("Not unifiable sorts.", s1, s2);
110: return null;
111: }
112: if (s1 instanceof IntersectionSort) {
113: final IntersectionSort intersect1 = (IntersectionSort) s1;
114: final IntersectionSort intersect2 = (IntersectionSort) s2;
115:
116: if (intersect1.memberCount() != intersect2
117: .memberCount()) {
118: Debug
119: .out("Should not happen as intersection sorts should always "
120: + "have member count = 2");
121: return null;
122: }
123: for (int i = 0, sz = intersect1.memberCount(); i < sz; i++) {
124: mc = matchSorts(intersect1.getComponent(i),
125: intersect2.getComponent(i), mc);
126: if (mc == null) {
127: Debug.out("Failed matching ", intersect1,
128: intersect2);
129: return null;
130: }
131: }
132: }
133: if (s1 == s2) {
134: return mc;
135: } else {
136: Debug.out("FAIL. Sorts not identical.", s1, s2);
137: return null;
138: }
139: } else {
140: final GenericSort gs = (GenericSort) s1;
141: final GenericSortCondition c = GenericSortCondition
142: .createIdentityCondition(gs, s2);
143: if (c == null) {
144: Debug.out("FAILED. Generic sort condition");
145: return null; //FAILED;
146: } else {
147: try {
148: mc = mc.setInstantiations(mc.getInstantiations()
149: .add(c));
150: } catch (SortException e) {
151: Debug.out("FAILED. Sort mismatch.", s1, s2);
152: return null; //FAILED;
153: }
154: }
155: }
156: return mc;
157: }
158:
159: /**
160: * Taking this sortdepending function as template to be matched against <code>op</code>,
161: * the necessary conditions are returned or null if not unifiable (matchable).
162: * A sortdepending function is matched successfull against another sortdepending function
163: * if the sorts can be matched and they are of same kind.
164: */
165: public MatchConditions match(SVSubstitute subst,
166: MatchConditions mc, Services services) {
167: if (this .getClass() != subst.getClass()) {
168: Debug.out(
169: "FAILED. Given operator cannot be matched by a sort"
170: + "depending function (template, orig)",
171: this , subst);
172: return null;
173: }
174: final SortDependingFunction sdp = (SortDependingFunction) subst;
175: final MatchConditions result = matchSorts(getSortDependingOn(),
176: sdp.getSortDependingOn(), mc);
177:
178: if (result == null) {
179: Debug
180: .out(
181: "Failed. Sorts of depending function not unifiable.",
182: this, subst);
183: return null;
184: }
185:
186: return isSimilar(sdp) ? result : null;
187: }
188: }
|