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.op;
009:
010: import java.util.Collections;
011: import java.util.HashSet;
012: import java.util.Set;
013:
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.sort.Sort;
018: import de.uka.ilkd.key.rule.MatchConditions;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * Creates an operator schemavariable that matches a given set of operators.
023: * All operators to be matched must have the same arity like this
024: * schema variable.
025: */
026: public class OperatorSV extends SchemaVariableAdapter {
027:
028: /** the arity of the operators this sv can be instantiated to */
029: private final int arity;
030:
031: /** the set of operators this sv can match */
032: private final Set operators;
033:
034: /**
035: * creates an instance of this schemavariable kind that can match any
036: * operator occuring in the set as long as the arities are the same
037: * @param name the Name of the schema variable
038: * @param sort the Sort the schema variable shall have
039: * @param arity the int with the arity
040: * @param set the set of operators to be matched by this schemavariable kind
041: *
042: */
043: OperatorSV(Name name, Sort sort, int arity, HashSet set) {
044:
045: super (name, Operator.class, sort, false);
046: this .arity = arity;
047: this .operators = (HashSet) set.clone();
048: }
049:
050: /**
051: * creates an instance of this schemavariable kind that can match any
052: * operator occuring in the set as long as the arities are the same as long
053: * as it is an instance of the given matching type
054: * @param name the Name of the schema variable
055: * @param matchingType the Class whose instances (including subtypes) can be matched
056: * @param sort the Sort the schema variable shall have
057: * @param arity the int with the arity
058: * @param set the set of operators to be matched by this schemavariable kind
059: *
060: */
061: protected OperatorSV(Name name, Class matchingType, Sort sort,
062: int arity, HashSet set) {
063:
064: super (name, matchingType, sort, false);
065: this .arity = arity;
066: this .operators = (HashSet) set.clone();
067: }
068:
069: /**
070: * checks whether the top level structure of the given @link Term
071: * is syntactically valid, given the assumption that the top level
072: * operator of the term is the same as this Operator. The
073: * assumption that the top level operator and the term are equal
074: * is NOT checked.
075: * @return true iff the top level structure of
076: * the {@link Term} is valid.
077: */
078: public boolean validTopLevel(Term term) {
079: if (term.arity() != this .arity())
080: return false;
081: return true;
082: }
083:
084: /** returns the arity of this operator */
085: public int arity() {
086: return arity;
087: }
088:
089: /**
090: * returns true if the schemavariable is an operator sv
091: */
092: public boolean isOperatorSV() {
093: return true;
094: }
095:
096: /**
097: * returns an unmodifiacle set of operators this schemavariable can match
098: */
099: public Set operators() {
100: return Collections.unmodifiableSet(operators);
101: }
102:
103: /**
104: * (non-Javadoc)
105: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
106: */
107: public MatchConditions match(SVSubstitute subst,
108: MatchConditions mc, Services services) {
109:
110: if (!(subst instanceof Operator)) {
111: Debug.out(
112: "FAILED. ArithmeticOperatorSC matches only operators "
113: + "(template, orig)", this , subst);
114: return null;
115: }
116:
117: final Operator op = (Operator) subst;
118: if (operators.contains(op)) {
119: Operator o = (Operator) mc.getInstantiations()
120: .getInstantiation(this );
121: if (o == null) {
122: return mc.setInstantiations(mc.getInstantiations().add(
123: this , op));
124: } else {
125: if (o != op) {
126: Debug
127: .out("FAILED. Already instantiated with a different operator.");
128: return null;
129: }
130: }
131: }
132: Debug.out("FAILED. template is a schema operator,"
133: + " term is an operator, but not a matching one");
134: return null;
135: }
136:
137: /** toString */
138: public String toString() {
139: return toString(" (operator sv)");
140: }
141:
142: }
|