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 Schematic Theory Specific Rules (Taclets) with find part
17: * int antecedent.
18: */
19: public class AntecTacletBuilder extends FindTacletBuilder {
20:
21: /** sets the <I>find</I> of the Taclet that is to build to the given
22: * term, if the sort of the given term is of Sort.FORMULA otherwise
23: * nothing happens.
24: * @return this AntecTacletBuilder
25: */
26: public AntecTacletBuilder setFind(Term findTerm) {
27: if (findTerm.sort() == Sort.FORMULA) {
28: find = findTerm;
29: }
30: checkContainsFreeVarSV(findTerm, getName(), "find term");
31: return this ;
32: }
33:
34: /** adds a new goal descriptions to the goal descriptions of the Taclet.
35: * the TacletGoalTemplate must not be a RewriteTacletGoalTemplate,
36: * otherwise an illegal argument exception is thrown.
37: */
38: public void addTacletGoalTemplate(TacletGoalTemplate goal) {
39: if (goal instanceof RewriteTacletGoalTemplate) {
40: throw new TacletBuilderException(this ,
41: "Tried to add a RewriteTaclet"
42: + "GoalTemplate to a Antec" + "Taclet");
43: }
44: goals = goals.prepend(goal);
45: }
46:
47: /** builds and returns the Taclet that is specified by
48: * former set... / add... methods. If no name is specified then
49: * an Taclet with an empty string name is build. No specifications
50: * for variable conditions, goals or heuristics imply that the
51: * corresponding parts of the Taclet are empty. No specification for
52: * the if-sequent is represented as a sequent with two empty
53: * semisequents. No specification for the interactive or
54: * recursive flags imply that the flags are not set.
55: * No specified find part causes an IllegalStateException.
56: */
57: public Taclet getTaclet() {
58: return getAntecTaclet();
59: }
60:
61: /** builds and returns the AntecTaclet that is specified by
62: * former set... / add... methods. If no name is specified then
63: * a taclet with an empty string name is build. No specifications
64: * for variable conditions, goals or heuristics imply that the
65: * corresponding parts of the Taclet are empty. No specification for
66: * the if-sequence is represented as a sequent with two empty
67: * semisequences. No specification for the interactive or
68: * recursive flags imply that the flags are not set.
69: * No specified find part causes an IllegalStateException.
70: * Throws an
71: * TacletBuilderException if a bound SchemaVariable occurs more than once in if
72: * and find or an InvalidPrefixException if the building of the Taclet
73: * Prefix fails.
74: */
75: public AntecTaclet getAntecTaclet() {
76: if (find == null) {
77: throw new TacletBuilderException(this ,
78: "No find part specified");
79:
80: }
81: checkBoundInIfAndFind();
82:
83: TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(
84: this );
85:
86: prefixBuilder.build();
87:
88: return new AntecTaclet(name, new TacletApplPart(ifseq, varsNew,
89: varsNotFreeIn, varsNewDependingOn, variableConditions),
90: goals, ruleSets, constraint, attrs, find, prefixBuilder
91: .getPrefixMap(), choices);
92: }
93:
94: }
|