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 java.util.HashMap;
014:
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
017: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
018: import de.uka.ilkd.key.logic.op.SchemaVariable;
019: import de.uka.ilkd.key.logic.sort.Sort;
020:
021: /** subclasss build Schematic Theory Specific Rules (Taclets) */
022: public abstract class TacletBuilder {
023:
024: protected final static Name NONAME = new Name("unnamed");
025:
026: protected Taclet taclet;
027:
028: protected Name name = NONAME;
029: protected Sequent ifseq = Sequent.EMPTY_SEQUENT;
030: protected ListOfNewVarcond varsNew = SLListOfNewVarcond.EMPTY_LIST;
031: protected ListOfNotFreeIn varsNotFreeIn = SLListOfNotFreeIn.EMPTY_LIST;
032: protected ListOfNewDependingOn varsNewDependingOn = SLListOfNewDependingOn.EMPTY_LIST;
033: protected ListOfTacletGoalTemplate goals = SLListOfTacletGoalTemplate.EMPTY_LIST;
034: protected ListOfRuleSet ruleSets = SLListOfRuleSet.EMPTY_LIST;
035: protected TacletAttributes attrs = new TacletAttributes();
036: protected Constraint constraint = Constraint.BOTTOM;
037: /** List of additional generic conditions on the instantiations of
038: * schema variables. */
039: protected ListOfVariableCondition variableConditions = SLListOfVariableCondition.EMPTY_LIST;
040: protected HashMap goal2Choices = null;
041: protected SetOfChoice choices = SetAsListOfChoice.EMPTY_SET;
042:
043: private static boolean containsFreeVarSV(Term t) {
044:
045: IteratorOfQuantifiableVariable it = t.freeVars().iterator();
046: while (it.hasNext()) {
047: QuantifiableVariable var = it.next();
048: if (var instanceof SchemaVariable
049: && ((SchemaVariable) var).isVariableSV()) {
050: return true;
051: }
052: }
053: return false;
054: }
055:
056: private static boolean containsFreeVarSV(Sequent s) {
057: IteratorOfConstrainedFormula it = s.iterator();
058: while (it.hasNext()) {
059: if (containsFreeVarSV(it.next().formula())) {
060: return true;
061: }
062: }
063: return false;
064: }
065:
066: static void checkContainsFreeVarSV(Sequent seq, Name tacletName,
067: String str) {
068: if (containsFreeVarSV(seq)) {
069: throw new TacletBuilderException(tacletName,
070: "Free Variable in " + str
071: + " in Taclet / sequent: " + seq);
072: }
073: }
074:
075: static void checkContainsFreeVarSV(Term t, Name tacletName,
076: String str) {
077: if (containsFreeVarSV(t)) {
078: throw new TacletBuilderException(tacletName,
079: "Free Variable found in " + str
080: + " in Taclet / Term: " + t);
081: }
082: }
083:
084: /**
085: * returns the name of the Taclet to be built
086: */
087: public Name getName() {
088: return this .name;
089: }
090:
091: /** sets the name of the Taclet to be built
092: */
093: public void setName(Name name) {
094: this .name = name;
095: }
096:
097: /** sets an optional display name (presented to the user)
098: */
099: public void setDisplayName(String s) {
100: attrs.setDisplayName(s);
101: }
102:
103: /** adds an old name to the list of old names
104: */
105: public void addOldName(String s) {
106: attrs.addOldName(s);
107: }
108:
109: public void setHelpText(String s) {
110: attrs.setHelpText(s);
111: }
112:
113: /** sets the ifseq of the Taclet to be built
114: */
115: public void setIfSequent(Sequent seq) {
116: checkContainsFreeVarSV(seq, getName(), "sequent");
117: this .ifseq = seq;
118: }
119:
120: /** sets the constraint that has to be satisfied if the Taclet
121: * should be valid */
122: public void setConstraint(Constraint constraint) {
123: this .constraint = constraint;
124: }
125:
126: /**
127: * adds a mapping from GoalTemplate <code>gt</code> to SetOfChoice
128: * <code>soc</code>
129: */
130: public void addGoal2ChoicesMapping(TacletGoalTemplate gt,
131: SetOfChoice soc) {
132: if (goal2Choices == null) {
133: goal2Choices = new HashMap();
134: }
135: goal2Choices.put(gt, soc);
136: }
137:
138: public HashMap getGoal2Choices() {
139: return goal2Choices;
140: }
141:
142: public void setChoices(SetOfChoice choices) {
143: this .choices = choices;
144: }
145:
146: public SetOfChoice getChoices() {
147: return choices;
148: }
149:
150: /** adds a new <I>new</I> variable to the variable conditions of
151: * the Taclet: v is new and has the sort as asSort if elementsort=false and the
152: * sort of the elements of asSort if elementsort=true and asSort is a program
153: * array SV.
154: */
155: public void addVarsNew(SchemaVariable v, SchemaVariable asSort,
156: boolean elementsort) {
157: addVarsNew(new NewVarcond(v, asSort, elementsort));
158: }
159:
160: /** adds a new <I>new</I> variable to the variable conditions of
161: * the Taclet: v is new and has the sort as asSort
162: */
163: public void addVarsNew(SchemaVariable v, SchemaVariable asSort) {
164: addVarsNew(new NewVarcond(v, asSort));
165: }
166:
167: /** adds a new <I>new</I> variable to the variable conditions of
168: * the Taclet: v is new and has type sort
169: */
170: public void addVarsNew(SchemaVariable v, Sort sort) {
171: addVarsNew(new NewVarcond(v, sort));
172: }
173:
174: /** adds a new <I>new</I> variable to the variable conditions of
175: * the Taclet: v is new.
176: */
177: public void addVarsNew(NewVarcond nv) {
178: if (!nv.getSchemaVariable().isProgramSV()) {
179: throw new TacletBuilderException(this ,
180: "Tried to add condition:" + nv
181: + "to new vars-list. That can"
182: + "match more than program" + " variables.");
183: }
184: varsNew = varsNew.prepend(nv);
185: }
186:
187: /** adds a list of <I>new</I> variables to the variable conditions of
188: * the Taclet: v is new for all v's in the given list
189: */
190: public void addVarsNew(ListOfNewVarcond list) {
191: IteratorOfNewVarcond it = list.iterator();
192: while (it.hasNext()) {
193: addVarsNew(it.next());
194: }
195: }
196:
197: /** adds a new <I>NotFreeIn</I> variable pair to the variable conditions of
198: * the Taclet: v0 is not free in v1.
199: */
200: public void addVarsNotFreeIn(SchemaVariable v0, SchemaVariable v1) {
201: varsNotFreeIn = varsNotFreeIn.prepend(new NotFreeIn(v0, v1));
202: }
203:
204: /** adds a list of <I>NotFreeIn</I> variable pairs to the variable
205: *conditions of
206: * the Taclet: v0 is not free in v1 for all entries (v0,v1) in the given list.
207: */
208: public void addVarsNotFreeIn(ListOfNotFreeIn list) {
209: varsNotFreeIn = varsNotFreeIn.prepend(list);
210: }
211:
212: /**
213: * Add a "v0 depending on v1"-statement. "v0" may not occur within
214: * the if sequent or the find formula/term, however, this is not
215: * checked
216: */
217: public void addVarsNewDependingOn(SchemaVariable v0,
218: SchemaVariable v1) {
219: varsNewDependingOn = varsNewDependingOn
220: .prepend(new NewDependingOn(v0, v1));
221: }
222:
223: /** Add an additional generic condition on the instatiation of
224: * schema variables. */
225: public void addVariableCondition(VariableCondition vc) {
226: variableConditions = variableConditions.append(vc);
227: }
228:
229: /** adds a new goal descriptions to the goal descriptions of the Taclet.
230: * The TacletGoalTemplate must be of
231: * the appropriate kind (Rewrite/Ante/Succ),
232: * otherwise an IllegalArgumentException is thrown.
233: */
234: public abstract void addTacletGoalTemplate(TacletGoalTemplate goal);
235:
236: /** adds a new rule set to the rule sets of the Taclet.
237: */
238: public void addRuleSet(RuleSet rs) {
239: ruleSets = ruleSets.prepend(rs);
240: }
241:
242: public void setRuleSets(ListOfRuleSet rs) {
243: ruleSets = rs;
244: }
245:
246: /** sets the noninteractive flag to the given value.
247: */
248: public void setNoninteractive(boolean ni) {
249: attrs.setNoninteractive(ni);
250: }
251:
252: public Sequent ifSequent() {
253: return ifseq;
254: }
255:
256: public ListOfTacletGoalTemplate goalTemplates() {
257: return goals;
258: }
259:
260: public IteratorOfNotFreeIn varsNotFreeIn() {
261: return varsNotFreeIn.iterator();
262: }
263:
264: public void setTacletGoalTemplates(ListOfTacletGoalTemplate g) {
265: goals = g;
266: }
267:
268: /** builds and returns the Taclet that is specified by
269: * former set... / add... methods. If no name is specified then
270: * an Taclet with an empty string name is build. No specifications
271: * for variable conditions, goals or rule sets imply that the
272: * corresponding parts of the Taclet are empty. No specification for
273: * the if-sequence is represented as a sequent with two empty
274: * semisequences. No specification for the interactive or
275: * recursive flags imply that the flags are not set.
276: * No specified find part for Taclets that require a find part
277: * causes an IllegalStateException.
278: */
279: public abstract Taclet getTaclet();
280:
281: public Taclet getTacletWithoutInactiveGoalTemplates(
282: SetOfChoice active) {
283: if (goal2Choices == null
284: || goals == SLListOfTacletGoalTemplate.EMPTY_LIST) {
285: return getTaclet();
286: } else {
287: ListOfTacletGoalTemplate oldGoals = goals;
288: IteratorOfTacletGoalTemplate it = oldGoals.iterator();
289: Taclet result;
290: while (it.hasNext()) {
291: TacletGoalTemplate goal = it.next();
292: if (goal2Choices.get(goal) != null
293: && !((SetOfChoice) goal2Choices.get(goal))
294: .subset(active)) {
295: goals = goals.removeAll(goal);
296: }
297: }
298: if (goals == SLListOfTacletGoalTemplate.EMPTY_LIST) {
299: result = null;
300: } else {
301: result = getTaclet();
302: }
303: goals = oldGoals;
304: return result;
305: }
306: }
307:
308: static class TacletBuilderException extends
309: IllegalArgumentException {
310:
311: private Name tacletname;
312: private String errorMessage;
313:
314: TacletBuilderException(Name tacletname, String errorMessage) {
315: this .tacletname = tacletname;
316: this .errorMessage = errorMessage;
317: }
318:
319: TacletBuilderException(TacletBuilder tb, String errorMessage) {
320: this (tb.getName(), errorMessage);
321: }
322:
323: public String getMessage() {
324: String message = (tacletname == null ? "(unknown taclet name)"
325: : tacletname.toString());
326: return message + ": " + errorMessage;
327: }
328:
329: }
330:
331: }
|