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: /* Generated by Together */
12:
13: /**
14: * Only for use in the generation of the translation of an OCL constaint !!!
15: *
16: * Creates a mapping of the names of functions (as strings) to the
17: * corresponding functionsymbol (object) ...
18: */package de.uka.ilkd.key.logic;
19:
20: import java.util.HashMap;
21: import java.util.Map;
22:
23: import de.uka.ilkd.key.logic.op.Function;
24: import de.uka.ilkd.key.logic.op.Operator;
25:
26: public class FunctionNameFunctionSymbolMapper extends Visitor {
27:
28: private Map funcNameSymbolMap;
29:
30: public FunctionNameFunctionSymbolMapper() {
31: funcNameSymbolMap = new HashMap();
32: }
33:
34: public void visit(Term visited) {
35:
36: if ((visited instanceof OpTerm)) {
37: // we possibly have a functionterm as the current subterm ...
38: Operator currentOp = visited.op();
39: if (currentOp instanceof Function) {
40: String funcName = currentOp.name().toString();
41: if (!funcNameSymbolMap.containsKey(funcName)) {
42: funcNameSymbolMap.put(funcName, currentOp);
43: }
44: }
45:
46: }
47: }
48:
49: public Map getNameSymbolMapping() {
50: return funcNameSymbolMap;
51: }
52:
53: }
|