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.Constraint;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.Sequent;
017: import de.uka.ilkd.key.logic.SetOfChoice;
018: import de.uka.ilkd.key.logic.op.MapFromSchemaVariableToTacletPrefix;
019: import de.uka.ilkd.key.logic.op.SetAsListOfQuantifiableVariable;
020: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
021: import de.uka.ilkd.key.logic.op.SetOfSchemaVariable;
022: import de.uka.ilkd.key.proof.Goal;
023: import de.uka.ilkd.key.proof.IteratorOfGoal;
024: import de.uka.ilkd.key.proof.ListOfGoal;
025:
026: /**
027: * Used to implement a Taclet that has no <I>find</I> part. This kind of taclet
028: * is not attached to term or formula, but to a complete sequent. A typical
029: * representant is the <code>cut</code> rule.
030: */
031: public class NoFindTaclet extends Taclet {
032:
033: /**
034: * creates a Schematic Theory Specific Rule (Taclet) with the given
035: * parameters.
036: * @param name the name of the Taclet
037: * @param applPart contains the application part of an Taclet that is
038: * the if-sequent, the variable conditions
039: * @param goalTemplates the ListOfTacletGoalTemplate containg all goal descriptions of the taclet to be created
040: * @param ruleSets a list of rule sets for the Taclet
041: * @param constraint the Constraint under which the Taclet is valid
042: * @param attrs attributes for the Taclet; these are boolean values
043: * @param prefixMap a MapFromSchemaVariableToTacletPrefix that contains the
044: * prefix for each SchemaVariable in the Taclet
045: * @param choices the SetOfChoices to which this taclet belongs to
046: */
047: public NoFindTaclet(Name name, TacletApplPart applPart,
048: ListOfTacletGoalTemplate goalTemplates,
049: ListOfRuleSet ruleSets, Constraint constraint,
050: TacletAttributes attrs,
051: MapFromSchemaVariableToTacletPrefix prefixMap,
052: SetOfChoice choices) {
053: super (name, applPart, goalTemplates, ruleSets, constraint,
054: attrs, prefixMap, choices);
055: cacheMatchInfo();
056: }
057:
058: /**
059: * adds the sequent of the add part of the Taclet to the goal sequent
060: * @param add the Sequent to be added
061: * @param goal the Goal to be updated
062: * @param services the Services encapsulating all java information
063: * @param matchCond the MatchConditions with all required instantiations
064: */
065: protected void applyAdd(Sequent add, Goal goal, Services services,
066: MatchConditions matchCond) {
067: addToAntec(add.antecedent(), goal, null, services, matchCond);
068: addToSucc(add.succedent(), goal, null, services, matchCond);
069: }
070:
071: /**
072: * the rule is applied on the given goal using the
073: * information of rule application.
074: * @param goal the goal that the rule application should refer to.
075: * @param services the Services encapsulating all java information
076: * @param ruleApp the taclet application that is executed
077: */
078: public ListOfGoal apply(Goal goal, Services services,
079: RuleApp ruleApp) {
080:
081: // Number without the if-goal eventually needed
082: int numberOfNewGoals = goalTemplates().size();
083:
084: TacletApp tacletApp = (TacletApp) ruleApp;
085: MatchConditions mc = tacletApp.matchConditions();
086:
087: // Restrict introduced metavariables to the subtree
088: setRestrictedMetavariables(goal, mc);
089:
090: ListOfGoal newGoals = checkIfGoals(goal, tacletApp
091: .ifFormulaInstantiations(), mc, numberOfNewGoals);
092:
093: IteratorOfTacletGoalTemplate it = goalTemplates().iterator();
094: IteratorOfGoal goalIt = newGoals.iterator();
095:
096: while (it.hasNext()) {
097: TacletGoalTemplate gt = it.next();
098: Goal currentGoal = goalIt.next();
099: // add first because we want to use pos information that
100: // is lost applying replacewith
101: applyAdd(gt.sequent(), currentGoal, services, mc);
102:
103: applyAddrule(gt.rules(), currentGoal, services, mc);
104:
105: applyAddProgVars(gt.addedProgVars(), currentGoal, tacletApp
106: .posInOccurrence(), services, mc);
107:
108: currentGoal.setBranchLabel(gt.name());
109: }
110:
111: return newGoals;
112: }
113:
114: protected Taclet setName(String s) {
115: NoFindTacletBuilder b = new NoFindTacletBuilder();
116: return super .setName(s, b);
117: }
118:
119: /**
120: * @return Set of schemavariables of the if and the (optional)
121: * find part
122: */
123: public SetOfSchemaVariable getIfFindVariables() {
124: return getIfVariables();
125: }
126:
127: /**
128: * the empty set as a no find taclet has no other entities where
129: * variables cann occur bound than in the goal templates
130: * @return empty set
131: */
132: protected SetOfQuantifiableVariable getBoundVariablesHelper() {
133: return SetAsListOfQuantifiableVariable.EMPTY_SET;
134: }
135:
136: }
|