01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic.op;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Name;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.TermFactory;
17: import de.uka.ilkd.key.logic.sort.Sort;
18: import de.uka.ilkd.key.rule.MatchConditions;
19: import de.uka.ilkd.key.util.Debug;
20:
21: class VariableSV extends SortedSchemaVariable {
22:
23: /** creates a new SchemaVariable. That is used as placeholder for
24: * bound(quantified) variables.
25: * @param name the Name of the SchemaVariable
26: * @param sort the Sort of the SchemaVariable and the matched type
27: * @param listSV a boolean which is true iff the schemavariable is allowed
28: * to match a list of quantified variables
29: * @param strictSV boolean indicating if the schemavariable is declared as strict
30: * forcing exact type match*/
31: VariableSV(Name name, Sort sort, boolean listSV) {
32: super (name, QuantifiableVariable.class, sort, listSV);
33: }
34:
35: /** returns true iff this SchemaVariable is used to match
36: * bound (quantifiable) variables
37: * @return true iff this SchemaVariable is used to match
38: * bound (quantifiable) variables
39: */
40: public boolean isVariableSV() {
41: return true;
42: }
43:
44: public boolean isRigid() {
45: return true;
46: }
47:
48: /* (non-Javadoc)
49: * @see de.uka.ilkd.key.logic.op.Operator#match(de.uka.ilkd.key.logic.op.SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
50: */
51: public MatchConditions match(SVSubstitute substitute,
52: MatchConditions mc, Services services) {
53: final Term subst;
54: if (substitute instanceof LogicVariable) {
55: subst = TermFactory.DEFAULT
56: .createVariableTerm((LogicVariable) substitute);
57: } else if (substitute instanceof Term
58: && ((Term) substitute).op() instanceof QuantifiableVariable) {
59: subst = (Term) substitute;
60: } else {
61: Debug
62: .out("Strange Exit of match in VariableSV. Check for bug");
63: return null;
64: }
65: final Term foundMapping = (Term) mc.getInstantiations()
66: .getInstantiation(this );
67: if (foundMapping == null) {
68: return addInstantiation(subst, mc, services);
69: } else if (((QuantifiableVariable) foundMapping.op()) != subst
70: .op()) {
71: return null; //FAILED;
72: }
73: return mc;
74: }
75:
76: /** toString */
77: public String toString() {
78: return toString("variable");
79: }
80:
81: }
|