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: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
11: // and Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16: package de.uka.ilkd.key.rule.metaconstruct;
17:
18: import de.uka.ilkd.key.gui.KeYMediator;
19: import de.uka.ilkd.key.gui.Main;
20: import de.uka.ilkd.key.java.JavaInfo;
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
23: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
24: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
25: import de.uka.ilkd.key.logic.Name;
26: import de.uka.ilkd.key.logic.Namespace;
27: import de.uka.ilkd.key.logic.Term;
28: import de.uka.ilkd.key.logic.TermFactory;
29: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
30: import de.uka.ilkd.key.logic.op.Function;
31: import de.uka.ilkd.key.logic.op.TermSymbol;
32: import de.uka.ilkd.key.rule.inst.SVInstantiations;
33:
34: /** Is used for OCL simplification.
35: * Extracts all subtypes of the given class from the
36: * current UML model.
37: */
38: public class MetaAllSubtypes extends AbstractMetaOperator {
39:
40: private TermFactory origTf = TermFactory.DEFAULT;
41:
42: public MetaAllSubtypes() {
43: super (new Name("#allSubtypes"), 1);
44: }
45:
46: /**
47: * checks whether the top level structure of the given @link Term
48: * is syntactically valid, given the assumption that the top level
49: * operator of the term is the same as this Operator. The
50: * assumption that the top level operator and the term are equal
51: * is NOT checked.
52: * @return true iff the top level structure of
53: * the @link Term is valid.
54: */
55: public boolean validTopLevel(Term term) {
56: return term.arity() == arity();
57: }
58:
59: /** calculates the resulting term. */
60: public Term calculate(Term term, SVInstantiations svInst,
61: Services services) {
62: Main main = Main.getInstance();
63: KeYMediator mediator = main.mediator();
64: Namespace namespace = mediator.func_ns();
65:
66: TermSymbol nil = (TermSymbol) namespace.lookup(new Name(
67: "$empty_set"));
68: TermSymbol cons = (TermSymbol) namespace.lookup(new Name(
69: "$insert_set"));
70: Term nilTerm = origTf.createFunctionTerm(nil);
71:
72: //Extract the subtypes in form of KeYJavaTypes
73: JavaInfo javaInfo = services.getJavaInfo();
74: String className = term.sub(0).op().name().toString();
75: KeYJavaType keyType = javaInfo
76: .getKeYJavaTypeByClassName(className);
77: ListOfKeYJavaType subtypes = javaInfo.getKeYProgModelInfo()
78: .getAllSubtypes(keyType);
79: subtypes = subtypes.append(keyType);
80:
81: //Build replacewith-term
82: IteratorOfKeYJavaType iter = subtypes.iterator();
83: Term result = nilTerm;
84: for (int i = 0; iter.hasNext(); i++) {
85: Name theName = new Name(iter.next().getFullName());
86: TermSymbol ts = (Function) namespace.lookup(theName);
87: Term t = origTf.createFunctionTerm(ts);
88: result = origTf.createFunctionTerm(cons, t, result);
89: }
90: return result;
91: }
92: }
|