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.Term;
014:
015: /** class builds RewriteTaclet objects.*/
016: public class RewriteTacletBuilder extends FindTacletBuilder {
017:
018: /**
019: * encodes restrictions on the state where a rewrite taclet is applicable
020: * If the value is equal to
021: * <ul>
022: * <li> {@link RewriteTaclet#NONE} no state restrictions are posed</li>
023: * <li> {@link RewriteTaclet#SAME_UPDATE_LEVEL} then <code>\assumes</code>
024: * must match on a formula within the same state as <code>\find</code>
025: * rsp. <code>\add</code>. For efficiency no modalities are allowed above
026: * the <code>\find</code> position </li>
027: * <li> {@link RewriteTaclet#IN_SEQUENT_STATE} the <code>\find</code> part is
028: * only allowed to match on formulas which are evaulated in the same state as
029: * the sequent</li>
030: *</ul>
031: */
032: private int stateRestriction;
033:
034: public RewriteTacletBuilder setStateRestriction(
035: int p_stateRestriction) {
036: stateRestriction = p_stateRestriction;
037: return this ;
038: }
039:
040: /** sets the <I>find</I> of the Taclet that is to build to the given
041: * term.
042: * @return this RewriteTacletBuilder
043: */
044: public RewriteTacletBuilder setFind(Term findTerm) {
045: checkContainsFreeVarSV(findTerm, this .getName(), "find term");
046: find = findTerm;
047: return this ;
048: }
049:
050: /** builds and returns the RewriteTaclet that is specified by
051: * former set... / add... methods. If no name is specified then
052: * an Taclet with an empty string name is build. No specifications
053: * for variable conditions, goals or heuristics imply that the
054: * corresponding parts of the Taclet are empty. No specification for
055: * the if-sequent is represented as a sequent with two empty
056: * semisequents. No specification for the interactive or
057: * recursive flags imply that the flags are not set.
058: * No specified find part causes an TacletBuilderException.
059: * Throws an
060: * TacletBuilderException if a bound SchemaVariable occurs more than once in if
061: * and find or an InvalidPrefixException if the building of the Taclet
062: * Prefix fails.
063: */
064: public RewriteTaclet getRewriteTaclet() {
065: if (find == null) {
066: throw new TacletBuilderException(this ,
067: "No find part specified");
068:
069: }
070: checkBoundInIfAndFind();
071: TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(
072: this );
073: prefixBuilder.build();
074: return new RewriteTaclet(name, new TacletApplPart(ifseq,
075: varsNew, varsNotFreeIn, varsNewDependingOn,
076: variableConditions), goals, ruleSets, constraint,
077: attrs, find, prefixBuilder.getPrefixMap(),
078: stateRestriction, choices);
079: }
080:
081: /**
082: * adds a new goal descriptions to the goal descriptions of the Taclet.
083: * the TacletGoalTemplate must not be an AntecSuccTacletGoalTemplate,
084: * otherwise an illegal argument exception is thrown.
085: */
086: public void addTacletGoalTemplate(TacletGoalTemplate goal) {
087: if (goal instanceof AntecSuccTacletGoalTemplate) {
088: throw new IllegalArgumentException(
089: "Tried to add a AntecSucc"
090: + "GoalTemplate to a Rewrite" + "Taclet");
091: }
092:
093: goals = goals.prepend(goal);
094: }
095:
096: /** builds and returns the Taclet that is specified by
097: * former set... / add... methods. If no name is specified then
098: * an Taclet with an empty string name is build. No specifications
099: * for variable conditions, goals or heuristics imply that the
100: * corresponding parts of the Taclet are empty. No specification for
101: * the if-sequence is represented as a sequent with two empty
102: * semisequences. No specification for the interactive or
103: * recursive flags imply that the flags are not set.
104: * No specified find part causes an IllegalStateException.
105: */
106: public Taclet getTaclet() {
107: return getRewriteTaclet();
108: }
109: }
|