01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.rule;
12:
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.sort.Sort;
15:
16: /** class builds SuccTaclet objects.*/
17: public class SuccTacletBuilder extends FindTacletBuilder {
18:
19: /** sets the <I>find</I> of the Taclet that is to build to the given
20: * term, if the sort of the given term is of Sort.FORMULA otherwise
21: * nothing happens.
22: * @return this SuccTacletBuilder
23: */
24: public SuccTacletBuilder setFind(Term findTerm) {
25: if (findTerm.sort() == Sort.FORMULA)
26: find = findTerm;
27: checkContainsFreeVarSV(findTerm, this .getName(), "find term");
28: return this ;
29: }
30:
31: /** adds a new goal descriptions to the goal descriptions of the Taclet.
32: * the TacletGoalTemplate must not be an RewriteTacletGoalTemplate,
33: * otherwise an illegal argument exception is thrown.
34: */
35: public void addTacletGoalTemplate(TacletGoalTemplate goal) {
36: if (goal instanceof RewriteTacletGoalTemplate) {
37: throw new TacletBuilderException(this ,
38: "Tried to add a RewriteTaclet"
39: + "GoalTemplate to a Succ" + "Taclet");
40: }
41: goals = goals.prepend(goal);
42: }
43:
44: /** builds and returns the SuccTaclet that is specified by
45: * former set... / add... methods. If no name is specified then
46: * an Taclet with an empty string name is build. No specifications
47: * for variable conditions, goals or heuristics imply that the
48: * corresponding parts of the Taclet are empty. No specification for
49: * the if-sequence is represented as a sequent with two empty
50: * semisequents. No specification for the interactive or
51: * recursive flags imply that the flags are not set.
52: * No specified find part causes an IllegalStateException.
53: * Throws an
54: * TacletBuilderException if a bound SchemaVariable occurs more than once in if
55: * and find or an InvalidPrefixException if the building of the Taclet
56: * Prefix fails.
57: */
58: public SuccTaclet getSuccTaclet() {
59: if (find == null) {
60: throw new TacletBuilderException(this ,
61: "No find part specified");
62:
63: }
64: checkBoundInIfAndFind();
65: final TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(
66: this );
67: prefixBuilder.build();
68: return new SuccTaclet(name, new TacletApplPart(ifseq, varsNew,
69: varsNotFreeIn, varsNewDependingOn, variableConditions),
70: goals, ruleSets, constraint, attrs, find, prefixBuilder
71: .getPrefixMap(), choices);
72: }
73:
74: /** builds and returns the Taclet that is specified by
75: * former set... / add... methods. If no name is specified then
76: * an Taclet with an empty string name is build. No specifications
77: * for variable conditions, goals or heuristics imply that the
78: * corresponding parts of the Taclet are empty. No specification for
79: * the if-sequence is represented as a sequent with two empty
80: * semisequences. No specification for the interactive or
81: * recursive flags imply that the flags are not set.
82: * No specified find part causes an IllegalStateException.
83: */
84: public Taclet getTaclet() {
85: return getSuccTaclet();
86: }
87:
88: }
|