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;
012:
013: import de.uka.ilkd.key.logic.BoundVarsVisitor;
014: import de.uka.ilkd.key.logic.Sequent;
015: import de.uka.ilkd.key.logic.op.*;
016:
017: /**
018: * this class contains the goals of the schematic theory specific
019: * rules (Taclet). There are new sequents that have to be added, new
020: * rules and rule variables. The replacewith-goal is implemented in
021: * subclasses
022: */
023: public class TacletGoalTemplate {
024:
025: /** stores sequent that is one of the new goals */
026: private Sequent addedSeq = Sequent.EMPTY_SEQUENT;
027:
028: /** stores list of Taclet which are introduced*/
029: private ListOfTaclet addedRules = SLListOfTaclet.EMPTY_LIST;
030:
031: /** program variables added by this taclet to the namespace */
032: private SetOfSchemaVariable addedProgVars = SetAsListOfSchemaVariable.EMPTY_SET;
033:
034: private String name = null;
035:
036: /** creates new Goaldescription
037: *@param addedSeq new Sequent to be added
038: *@param addedRules ListOfTaclet contains the new allowed rules
039: * at this branch
040: *@param addedProgVars a SetOfSchemaVariable which will be instantiated with
041: * a application time unused (new) program variables that are introduced by
042: * an application of this template
043: */
044: public TacletGoalTemplate(Sequent addedSeq,
045: ListOfTaclet addedRules, SetOfSchemaVariable addedProgVars) {
046: TacletBuilder.checkContainsFreeVarSV(addedSeq, null,
047: "add sequent");
048:
049: this .addedRules = addedRules;
050: this .addedSeq = addedSeq;
051: this .addedProgVars = addedProgVars;
052: }
053:
054: /**
055: * creates new Goaldescription
056: * same effect as <code>new TacletGoalTemplate(addedSeq,
057: * addedRules,
058: * SetAsListOfSchemaVariable.EMPTY_SET)
059: * </code>
060: *
061: * @param addedSeq new Sequent to be added
062: * @param addedRules ListOfTaclet contains the new allowed rules
063: * at this branch
064: */
065: public TacletGoalTemplate(Sequent addedSeq, ListOfTaclet addedRules) {
066: this (addedSeq, addedRules, SetAsListOfSchemaVariable.EMPTY_SET);
067: }
068:
069: /** a Taclet may replace parts of sequent.
070: * @return term (or sequent) to be placed instead of the findexp-term.
071: * REMARK: returns 'null' if there is no replace-with part !
072: * Overwritten in subclasses !
073: */
074: Object replaceWithExpressionAsObject() {
075: return null;
076: }
077:
078: /** a Taclet may add a new Sequent as Goal. Use this method to get
079: * this Sequent
080: * @return Sequent to be added as Goal or Sequent.EMPTY_SEQUENT if
081: * no such Sequent exists
082: */
083: public Sequent sequent() {
084: return addedSeq;
085: }
086:
087: /** the goal of a Taclet may introduce new rules. Call this method
088: * to get them
089: * @return ListOfTaclet contains new introduced rules
090: */
091: public ListOfTaclet rules() {
092: return addedRules;
093: }
094:
095: /** returns the set of schemavaroable whos einstantiations will be
096: * added to the sequent namespace */
097: public SetOfSchemaVariable addedProgVars() {
098: return addedProgVars;
099: }
100:
101: /**
102: * rertieves and returns all variables that are bound in the
103: * goal template
104: * @return all variables that occur bound in this goal template
105: */
106: protected SetOfQuantifiableVariable getBoundVariables() {
107: SetOfQuantifiableVariable result = SetAsListOfQuantifiableVariable.EMPTY_SET;
108:
109: final IteratorOfTaclet tacletIt = rules().iterator();
110:
111: while (tacletIt.hasNext()) {
112: result = result.union(tacletIt.next().getBoundVariables());
113: }
114:
115: final BoundVarsVisitor bvv = new BoundVarsVisitor();
116: bvv.visit(sequent());
117:
118: return result.union(bvv.getBoundVariables());
119: }
120:
121: public void setName(String s) {
122: name = s;
123: }
124:
125: public String name() {
126: return name;
127: }
128:
129: public boolean equals(Object o) {
130: if (!(o instanceof TacletGoalTemplate))
131: return false;
132:
133: TacletGoalTemplate other = (TacletGoalTemplate) o;
134:
135: return addedSeq.equals(other.addedSeq)
136: && addedRules.equals(other.addedRules);
137: }
138:
139: public int hashCode() {
140: int result = 17;
141: result = 37 * result + addedSeq.hashCode();
142: result = 37 * result + addedRules.hashCode();
143: return result;
144: }
145:
146: /** toString */
147: public String toString() {
148: String result = "";
149: if (sequent() != Sequent.EMPTY_SEQUENT)
150: result += "\\add " + sequent() + " ";
151: if (rules() != SLListOfTaclet.EMPTY_LIST)
152: result += "\\addrules " + rules() + " ";
153: if (addedProgVars().size() > 0)
154: result += "\\addprogvars " + addedProgVars() + " ";
155: return result;
156: }
157:
158: }
|