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.java.Services;
014: import de.uka.ilkd.key.logic.*;
015: import de.uka.ilkd.key.logic.op.MapFromSchemaVariableToTacletPrefix;
016: import de.uka.ilkd.key.proof.Goal;
017:
018: /**
019: * A SuccTaclet represents a taclet whose find part has to match a top level
020: * formula in the succedent of the sequent.
021: */
022: public class SuccTaclet extends FindTaclet {
023:
024: /**
025: * creates a Schematic Theory Specific Rule (Taclet) with the given
026: * parameters that works on the succedent.
027: * @param name the name of the Taclet
028: * @param applPart contains the application part of an Taclet that is
029: * the if-sequent, the variable conditions
030: * @param goalTemplates a list of goal descriptions.
031: * @param heuristics a list of heurisics for the Taclet
032: * @param constraint the Constraint under which the Taclet is valid
033: * @param attrs attributes for the Taclet; these are boolean values
034: * indicating a noninteractive or recursive use of the Taclet.
035: * @param find the find term of the Taclet
036: * @param prefixMap a MapFromSchemaVariableToTacletPrefix that contains the
037: * prefix for each SchemaVariable in the Taclet
038: */
039: public SuccTaclet(Name name, TacletApplPart applPart,
040: ListOfTacletGoalTemplate goalTemplates,
041: ListOfRuleSet heuristics, Constraint constraint,
042: TacletAttributes attrs, Term find,
043: MapFromSchemaVariableToTacletPrefix prefixMap,
044: SetOfChoice choices) {
045: super (name, applPart, goalTemplates, heuristics, constraint,
046: attrs, find, prefixMap, choices);
047: cacheMatchInfo();
048: }
049:
050: /** this method is used to determine if top level updates are
051: * allowed to be ignored. This is the case if we have an Antec or
052: * SuccTaclet but not for a RewriteTaclet
053: * @return true if top level updates shall be ignored
054: */
055: protected boolean ignoreTopLevelUpdates() {
056: return true;
057: }
058:
059: /** CONSTRAINT NOT USED
060: * applies the replacewith part of Taclets
061: * @param gt TacletGoalTemplate used to get the replaceexpression in the Taclet
062: * @param goal the Goal where the rule is applied
063: * @param posOfFind the PosInOccurrence belonging to the find expression
064: * @param services the Services encapsulating all java information
065: * @param matchCond the MatchConditions with all required instantiations
066: */
067: protected void applyReplacewith(TacletGoalTemplate gt, Goal goal,
068: PosInOccurrence posOfFind, Services services,
069: MatchConditions matchCond) {
070: if (gt instanceof AntecSuccTacletGoalTemplate) {
071: Sequent replWith = ((AntecSuccTacletGoalTemplate) gt)
072: .replaceWith();
073:
074: addToAntec(replWith.antecedent(), goal, null, services,
075: matchCond);
076: if (createCopies(goal, posOfFind, matchCond)) {
077: addToSucc(replWith.succedent(), goal, posOfFind,
078: services, matchCond);
079: } else {
080: replaceAtPos(replWith.succedent(), goal, posOfFind,
081: services, matchCond);
082: }
083:
084: } else {
085: // Then there was no replacewith...
086: }
087: }
088:
089: /**
090: * adds the sequent of the add part of the Taclet to the goal sequent
091: * @param add the Sequent to be added
092: * @param goal the Goal to be updated
093: * @param posOfFind the PosInOccurrence describes the place where to add
094: * the semisequent
095: * @param matchCond the MatchConditions with all required instantiations
096: */
097: protected void applyAdd(Sequent add, Goal goal,
098: PosInOccurrence posOfFind, Services services,
099: MatchConditions matchCond) {
100: addToAntec(add.antecedent(), goal, null, services, matchCond);
101: addToSucc(add.succedent(), goal, posOfFind, services, matchCond);
102: }
103:
104: /** toString for the find part */
105: StringBuffer toStringFind(StringBuffer sb) {
106: return sb.append("\\find(==>").append(find().toString())
107: .append(")\n");
108: }
109:
110: protected Taclet setName(String s) {
111: SuccTacletBuilder b = new SuccTacletBuilder();
112: b.setFind(find());
113: return super.setName(s, b);
114: }
115:
116: }
|