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.*;
014: import de.uka.ilkd.key.logic.op.*;
015:
016: /**
017: * This visitor is used to collect information about schema variable
018: * pairs occurring within the same substitution operator within a
019: * taclet. This information is used to choose names of metavariables
020: * or skolem functions.
021: */
022:
023: public class SVNameCorrespondenceCollector extends Visitor {
024:
025: /**
026: * This map contains (a, b) if there is a substitution {b a}
027: * somewhere in the taclet
028: */
029: private MapFromSchemaVariableToSchemaVariable nameCorrespondences = MapAsListFromSchemaVariableToSchemaVariable.EMPTY_MAP;
030:
031: /** is called by the execPostOrder-method of a term
032: * @param Term if the toplevel operator of this term is a
033: * substitution of schema variables, then this pair is added to
034: * the map "nameCorrespondences"
035: */
036: public void visit(Term t) {
037:
038: final Operator top = t.op();
039:
040: if (top instanceof SubstOp) {
041: final Operator substTermOp = t.sub(0).op();
042: final QuantifiableVariable substVar = t.varsBoundHere(1)
043: .getQuantifiableVariable(0);
044: if (substTermOp instanceof SchemaVariable
045: && substVar instanceof SchemaVariable)
046: addNameCorrespondence((SchemaVariable) substTermOp,
047: (SchemaVariable) substVar);
048: }
049:
050: }
051:
052: private void addNameCorrespondence(SchemaVariable nameReceiver,
053: SchemaVariable nameProvider) {
054: nameCorrespondences = nameCorrespondences.put(nameReceiver,
055: nameProvider);
056: }
057:
058: /**
059: * @return the found correspondences as a map, mapping schema variable a
060: * onto schema variables b if b is replaced with a somewhere in this
061: * taclet
062: */
063: public MapFromSchemaVariableToSchemaVariable getCorrespondences() {
064: return nameCorrespondences;
065: }
066:
067: /** collects all correspondences in a semisequent
068: * @param semiseq the Semisequent to visit
069: */
070: private void visit(Semisequent semiseq) {
071: IteratorOfConstrainedFormula it = semiseq.iterator();
072: while (it.hasNext()) {
073: it.next().formula().execPostOrder(this );
074: }
075: }
076:
077: /** collects all correspondences in a sequent
078: * @param seq the Sequent to visit
079: */
080: public void visit(Sequent seq) {
081: visit(seq.antecedent());
082: visit(seq.succedent());
083: }
084:
085: /** collects all correspondences in a taclet
086: * @param taclet the Taclet where the correspondences have to be
087: * collected
088: * @param visitAddRules a boolean that contols if the addrule sections are
089: * to be ignored (iff false) or if the visitor descends into them (iff true)
090: */
091: public void visit(Taclet taclet, boolean visitAddrules) {
092: SchemaVariable findSV = null;
093: visit(taclet.ifSequent());
094: if (taclet instanceof FindTaclet) {
095: final Term findTerm = ((FindTaclet) taclet).find();
096: findTerm.execPostOrder(this );
097: if (findTerm.op() instanceof SchemaVariable)
098: findSV = (SchemaVariable) findTerm.op();
099: }
100: IteratorOfTacletGoalTemplate it = taclet.goalTemplates()
101: .iterator();
102: while (it.hasNext()) {
103: TacletGoalTemplate gt = it.next();
104: visit(gt.sequent());
105: if (gt instanceof RewriteTacletGoalTemplate) {
106: final Term replaceWithTerm = ((RewriteTacletGoalTemplate) gt)
107: .replaceWith();
108: replaceWithTerm.execPostOrder(this );
109: if (findSV != null
110: && replaceWithTerm.op() instanceof SchemaVariable)
111: addNameCorrespondence(
112: (SchemaVariable) replaceWithTerm.op(),
113: findSV);
114: } else {
115: if (gt instanceof AntecSuccTacletGoalTemplate) {
116: visit(((AntecSuccTacletGoalTemplate) gt)
117: .replaceWith());
118: }
119: }
120: if (visitAddrules) {
121: IteratorOfTaclet addruleIt = gt.rules().iterator();
122: while (addruleIt.hasNext()) {
123: visit(addruleIt.next(), true);
124: }
125: }
126: }
127: }
128:
129: }
|