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: package de.uka.ilkd.key.proof;
09:
10: import java.util.Map;
11:
12: import de.uka.ilkd.key.logic.JavaBlock;
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.TermFactory;
15: import de.uka.ilkd.key.logic.op.*;
16:
17: public class SymbolReplacer extends ProgVarReplacer {
18:
19: public SymbolReplacer(Map m) {
20: super (m);
21: }
22:
23: /**
24: * replaces in a term
25: */
26: public Term replace(Term t) {
27: if (t.op() instanceof RigidFunction && map.containsKey(t.op())) {
28: return replaceRigidFunction(t);
29: } else {
30: return super .replace(t);
31: }
32: }
33:
34: private Term replaceRigidFunction(Term t) {
35: assert t.op() instanceof RigidFunction;
36: assert t.javaBlock().isEmpty();
37:
38: RigidFunction rf = (RigidFunction) map.get(t.op());
39:
40: if (rf != t.op()) {
41: final Term newSubTerms[] = new Term[t.arity()];
42: final ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[t
43: .arity()];
44:
45: for (int i = 0, ar = t.arity(); i < ar; i++) {
46: newSubTerms[i] = replace(t.sub(i));
47: boundVars[i] = t.varsBoundHere(i);
48: }
49:
50: return TermFactory.DEFAULT.createTerm(rf, newSubTerms,
51: boundVars, JavaBlock.EMPTY_JAVABLOCK);
52:
53: } else {
54: return standardReplace(t);
55: }
56: }
57:
58: }
|