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: * An AntecTaclet represents a taclet whose find part has to match a top level
020: * formula in the antecedent of the sequent.
021: */
022: public class AntecTaclet extends FindTaclet {
023:
024: /**
025: * creates a Schematic Theory Specific Rule (Taclet) with the given
026: * parameters.
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 AntecTaclet(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: final Sequent replWith = ((AntecSuccTacletGoalTemplate) gt)
072: .replaceWith();
073:
074: if (createCopies(goal, posOfFind, matchCond)) {
075: addToAntec(replWith.antecedent(), goal, posOfFind,
076: services, matchCond);
077: } else {
078: replaceAtPos(replWith.antecedent(), goal, posOfFind,
079: services, matchCond);
080: }
081: addToSucc(replWith.succedent(), goal, null, services,
082: matchCond);
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 services the Services encapsulating all java information
096: * @param matchCond the MatchConditions with all required instantiations
097: */
098: protected void applyAdd(Sequent add, Goal goal,
099: PosInOccurrence posOfFind, Services services,
100: MatchConditions matchCond) {
101: addToAntec(add.antecedent(), goal, posOfFind, services,
102: matchCond);
103: addToSucc(add.succedent(), goal, null, services, matchCond);
104: }
105:
106: /** toString for the find part */
107: StringBuffer toStringFind(StringBuffer sb) {
108: return sb.append("\\find(").append(find().toString()).append(
109: "==>)\n");
110: }
111:
112: protected Taclet setName(String s) {
113: AntecTacletBuilder b = new AntecTacletBuilder();
114: b.setFind(find());
115: return super.setName(s, b);
116: }
117:
118: }
|