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.soundness;
12:
13: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
14: import de.uka.ilkd.key.logic.Semisequent;
15: import de.uka.ilkd.key.logic.Sequent;
16: import de.uka.ilkd.key.logic.Visitor;
17: import de.uka.ilkd.key.rule.*;
18:
19: public abstract class TacletVisitor extends Visitor {
20:
21: /** collects all variables in a Semisequent
22: * @param semiseq the Semisequent to visit
23: */
24: private void visit(Semisequent semiseq) {
25: IteratorOfConstrainedFormula it = semiseq.iterator();
26: while (it.hasNext()) {
27: it.next().formula().execPostOrder(this );
28: }
29: }
30:
31: /** goes through the given sequent an collects all vars found
32: * @param seq the Sequent to visit
33: */
34: public void visit(Sequent seq) {
35: visit(seq.antecedent());
36: visit(seq.succedent());
37: }
38:
39: /** collects all variables in a Taclet
40: * @param taclet the Taclet where the variables have to be collected to
41: * @param visitAddRules a boolean that contols if the addrule sections are
42: * to be ignored (iff false) or if the visitor descends into them (iff true)
43: */
44: public void visit(Taclet taclet, boolean visitAddrules) {
45: visit(taclet.ifSequent());
46: if (taclet instanceof FindTaclet) {
47: (((FindTaclet) taclet).find()).execPostOrder(this );
48: }
49: IteratorOfTacletGoalTemplate it = taclet.goalTemplates()
50: .iterator();
51: while (it.hasNext()) {
52: TacletGoalTemplate gt = it.next();
53: visit(gt.sequent());
54: if (gt instanceof RewriteTacletGoalTemplate) {
55: ((RewriteTacletGoalTemplate) gt).replaceWith()
56: .execPostOrder(this );
57: } else {
58: if (gt instanceof AntecSuccTacletGoalTemplate) {
59: visit(((AntecSuccTacletGoalTemplate) gt)
60: .replaceWith());
61: }
62: }
63: if (visitAddrules) {
64: IteratorOfTaclet addruleIt = gt.rules().iterator();
65: while (addruleIt.hasNext()) {
66: visit(addruleIt.next(), true);
67: }
68: }
69: }
70: }
71:
72: }
|