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.rule;
12:
13: import de.uka.ilkd.key.logic.BoundVarsVisitor;
14: import de.uka.ilkd.key.logic.Sequent;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.SetAsListOfSchemaVariable;
17: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
18: import de.uka.ilkd.key.logic.op.SetOfSchemaVariable;
19:
20: /** this class inherits from TacletGoalTemplate. It is used if there is a
21: * replacewith in the ruleGoals that replaces a term by another
22: * term. For a sequent {@see de.uka.ilkd.key.proof.AnteSuccTacletGoalTemplate}
23: */
24: public class RewriteTacletGoalTemplate extends TacletGoalTemplate {
25:
26: /** term that replaces another one */
27: private Term replacewith;
28:
29: /** creates new Goaldescription
30: *@param addedSeq new Sequent to be added
31: *@param addedRules ListOfTaclet contains the new allowed rules
32: * at this branch
33: *@param ruleVars ListOfRulevariable contains used rulevariables
34: *@param replacewith the Term that replaces another one
35: */
36: public RewriteTacletGoalTemplate(Sequent addedSeq,
37: ListOfTaclet addedRules, Term replacewith,
38: SetOfSchemaVariable pvs) {
39: super (addedSeq, addedRules, pvs);
40: TacletBuilder.checkContainsFreeVarSV(replacewith, null,
41: "replacewith term");
42: this .replacewith = replacewith;
43: }
44:
45: public RewriteTacletGoalTemplate(Sequent addedSeq,
46: ListOfTaclet addedRules, Term replacewith) {
47: this (addedSeq, addedRules, replacewith,
48: SetAsListOfSchemaVariable.EMPTY_SET);
49: }
50:
51: /** a Taclet may replace a Term by another. The new Term is returned.
52: * @return Term being paramter in the rule goal replacewith(Seq)
53: */
54: public Term replaceWith() {
55: return replacewith;
56: }
57:
58: /**
59: * rertieves and returns all variables that are bound in the
60: * goal template
61: * @return all variables that occur bound in this goal template
62: */
63: protected SetOfQuantifiableVariable getBoundVariables() {
64: final BoundVarsVisitor bvv = new BoundVarsVisitor();
65: bvv.visit(replaceWith());
66: return bvv.getBoundVariables().union(super .getBoundVariables());
67: }
68:
69: /**
70: * @return Term being paramter in the rule goal replacewith(term)
71: */
72: Object replaceWithExpressionAsObject() {
73: return replacewith;
74: }
75:
76: public boolean equals(Object o) {
77: if (!(o instanceof RewriteTacletGoalTemplate))
78: return false;
79: RewriteTacletGoalTemplate other = (RewriteTacletGoalTemplate) o;
80:
81: return super .equals(other)
82: && replacewith.equals(other.replacewith);
83: }
84:
85: public int hashCode() {
86: int result = 17;
87: result = 37 * result * super .hashCode();
88: result = 37 * result * replacewith.hashCode();
89: return result;
90: }
91:
92: /** toString */
93: public String toString() {
94: String result = super .toString();
95: result += "\\replacewith(" + replaceWith() + ") ";
96: return result;
97: }
98:
99: }
|