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.Expression;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.reference.TypeReference;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.op.SVSubstitute;
018: import de.uka.ilkd.key.logic.op.SchemaVariable;
019: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
020: import de.uka.ilkd.key.logic.sort.GenericSort;
021: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
022: import de.uka.ilkd.key.logic.sort.Sort;
023: import de.uka.ilkd.key.rule.MatchConditions;
024: import de.uka.ilkd.key.rule.VariableCondition;
025: import de.uka.ilkd.key.rule.inst.GenericSortCondition;
026: import de.uka.ilkd.key.rule.inst.SVInstantiations;
027: import de.uka.ilkd.key.rule.inst.SortException;
028: import de.uka.ilkd.key.util.Debug;
029:
030: /**
031: * Variable condition that enforces a given generic sort to be instantiated with
032: * the sort of a program expression a schema variable is instantiated with
033: * (currently only schema variables <code>ProgramSVSort.EXPRESSION</code> are
034: * supported)
035: */
036: public class JavaTypeToSortCondition implements VariableCondition {
037:
038: private final SchemaVariable exprOrTypeSV;
039: private final GenericSort sort;
040:
041: public JavaTypeToSortCondition(final SchemaVariable exprOrTypeSV,
042: final GenericSort sort) {
043: this .exprOrTypeSV = exprOrTypeSV;
044: this .sort = sort;
045:
046: if (!checkSortedSV(exprOrTypeSV)) {
047: throw new RuntimeException(
048: "Expected a program schemavariable for expressions");
049: }
050: }
051:
052: public static boolean checkSortedSV(
053: final SchemaVariable exprOrTypeSV) {
054: if (!(exprOrTypeSV instanceof SortedSchemaVariable)
055: && !exprOrTypeSV.isTermSV()) {
056: final Sort svSort = ((SortedSchemaVariable) exprOrTypeSV)
057: .sort();
058: if ((svSort == ProgramSVSort.EXPRESSION || svSort == ProgramSVSort.TYPE)) {
059: return false;
060: }
061: }
062: return true;
063: }
064:
065: /**
066: * checks if the condition for a correct instantiation is fulfilled
067: *
068: * @param var
069: * the template Variable to be instantiated
070: * @param matchCond
071: * the MatchCondition with the current matching state and in
072: * particular the SVInstantiations that are already known to be
073: * needed
074: * @param services
075: * the program information object
076: * @return modified match results if the condition can be satisfied, or
077: * <code>null</code> otherwise
078: */
079: public MatchConditions check(SchemaVariable var,
080: SVSubstitute svSubst, MatchConditions matchCond,
081: Services services) {
082: if (var != exprOrTypeSV) {
083: return matchCond;
084: }
085:
086: Debug.assertTrue(svSubst instanceof Expression
087: || svSubst instanceof TypeReference
088: || svSubst instanceof Term);
089:
090: final SVInstantiations inst = matchCond.getInstantiations();
091: final Sort type;
092: if (svSubst instanceof Term) {
093: type = ((Term) svSubst).sort();
094: } else if (svSubst instanceof TypeReference) {
095: type = ((TypeReference) svSubst).getKeYJavaType().getSort();
096: } else {
097: final Expression expr = (Expression) svSubst;
098: type = expr.getKeYJavaType(services,
099: inst.getExecutionContext()).getSort();
100: }
101: try {
102: return matchCond.setInstantiations(inst
103: .add(GenericSortCondition.createIdentityCondition(
104: sort, type)));
105: } catch (SortException e) {
106: return null;
107: }
108: }
109:
110: public String toString() {
111: return "\\hasSort(" + exprOrTypeSV + ", " + sort + ")";
112: }
113: }
|