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.ProgramElement;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.Constraint;
016: import de.uka.ilkd.key.logic.Name;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.sort.Sort;
019: import de.uka.ilkd.key.rule.MatchConditions;
020: import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
021: import de.uka.ilkd.key.rule.inst.SVInstantiations;
022: import de.uka.ilkd.key.util.Debug;
023:
024: /**
025: * This class represents the root of a schema variable hierarchy to be express
026: * termstructures that match on logical terms. Schema variables are used in
027: * Taclets where they act as placeholders for other TermSymbols. The TermSymbols
028: * a SchemaVariable is allowed to match is specified by their type and sort. If
029: * a match fits these conditions can be checked using the method
030: * isCompatible(TermSymbol t)
031: */
032: public abstract class SortedSchemaVariable extends
033: SchemaVariableAdapter implements ParsableVariable,
034: QuantifiableVariable, Location {
035:
036: /**
037: * creates a new SchemaVariable. That is used as placeholder for TermSymbols
038: * of a certain type.
039: *
040: * @param name
041: * the Name of the SchemaVariable
042: * @param matchType
043: * Class representing the type of symbols that can be matched
044: * @param sort
045: * the Sort of the SchemaVariable and the matched type
046: * @param listSV
047: * a boolean which is true iff the schemavariable is allowed to
048: * match a list of syntactical elements
049: */
050: protected SortedSchemaVariable(Name name, Class matchType,
051: Sort sort, boolean listSV) {
052: super (name, matchType, sort, listSV);
053: }
054:
055: /**
056: * tries to add the pair <tt>(this,pe)</tt> to the match conditions. If
057: * possible the resulting match conditions are returned, otherwise
058: * <tt>null</tt>. Such an addition can fail, e.g. if already a pair
059: * <tt>(this,x)</tt> exists where <tt>x<>pe</tt>
060: */
061: protected MatchConditions addInstantiation(ProgramElement pe,
062: MatchConditions matchCond, Services services) {
063:
064: final SVInstantiations instantiations = matchCond
065: .getInstantiations();
066: final SVSubstitute inMap = (SVSubstitute) instantiations
067: .getInstantiation(this );
068:
069: if (inMap == null) {
070: try {
071: return matchCond.setInstantiations(instantiations.add(
072: this , pe));
073: } catch (IllegalInstantiationException e) {
074: Debug
075: .out("Exception thrown by class Taclet at setInstantiations");
076: }
077: } else {
078: Object peForCompare = pe;
079: if (inMap instanceof Term) {
080: try {
081: peForCompare = services.getTypeConverter()
082: .convertToLogicElement(
083: pe,
084: matchCond.getInstantiations()
085: .getExecutionContext());
086: } catch (RuntimeException re) {
087: Debug.out(
088: "Cannot convert program element to term.",
089: this , pe);
090: return null;
091: }
092: }
093: if (inMap.equals(peForCompare)) {
094: return matchCond;
095: }
096: }
097: Debug.out("FAILED. Illegal Instantiation.", this , pe);
098: return null;
099: }
100:
101: /**
102: * tries to add the pair <tt>(this,term)</tt> to the match conditions. If
103: * successful the resulting conditions are returned, otherwise null. Failure
104: * is possible e.g. if this schemavariable has been already matched to a
105: * term <tt>t2</tt> which is not unifiable with the given term.
106: */
107: protected MatchConditions addInstantiation(Term term,
108: MatchConditions matchCond, Services services) {
109:
110: if (this .isRigid() && !term.isRigid()) {
111: Debug.out("FAILED. Illegal Instantiation");
112: return null;
113: }
114:
115: final SVInstantiations inst = matchCond.getInstantiations();
116:
117: final Term t = inst.getTermInstantiation(this , inst
118: .getExecutionContext(), services);
119: if (t != null) {
120: final Constraint c = matchCond.getConstraint().unify(t,
121: term, services);
122: if (!c.isSatisfiable()) {
123: Debug.out(
124: "FAILED. Adding instantiations leads to unsatisfiable"
125: + " constraint.", this , term);
126: return null; // FAILED;
127: } else {
128: return matchCond.setConstraint(c);
129: }
130: }
131:
132: try {
133: return matchCond.setInstantiations(inst.add(this , term));
134: } catch (IllegalInstantiationException e) {
135: Debug
136: .out(
137: "FAILED. Exception thrown at sorted schema variable",
138: e);
139: }
140:
141: Debug.out("FAILED. Illegal Instantiation");
142: return null;
143: }
144:
145: /**
146: * @return true if the schemavariable has the strict modifier which forces
147: * the instantiation to have exact the same sort as the
148: * schemavariable (or if the sv is of generic sort - the
149: * instantiation of the generic sort)
150: */
151: public boolean isStrict() {
152: return true;
153: }
154:
155: /**
156: * checks if this schemavariable matches element <code>subst</code> with
157: * respect to the given conditions and returns the resulting match
158: * conditions (or null if the match is not possible)
159: *
160: * @param subst
161: * the SVSubstitute to be matched
162: * @param mc
163: * the MatchConditions posing restrictions on the variables to be
164: * matched
165: * @param services
166: * the Services with additional information about the context
167: * (e.g. type hierarchy)
168: * @return the resulting MatchConditions
169: */
170: public MatchConditions match(SVSubstitute subst,
171: MatchConditions mc, Services services) {
172: if (subst instanceof Term) {
173: return addInstantiation((Term) subst, mc, services);
174: }
175: // overwritten in variable sv to match logic variables
176: Debug
177: .out("FAILED. Schemavariable of this kind only match terms.");
178: return null;
179: }
180:
181: public boolean mayBeAliasedBy(Location loc) {
182: return true;
183: }
184:
185: }
|