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.logic.sort;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.Namespace;
15: import de.uka.ilkd.key.logic.op.SortDependingSymbol;
16:
17: public abstract class AbstractNonCollectionSort extends AbstractSort
18: implements NonCollectionSort {
19:
20: protected AbstractCollectionSort setSort;
21:
22: protected AbstractCollectionSort bagSort;
23:
24: protected AbstractCollectionSort sequenceSort;
25:
26: /** creates a Sort (with a new equality symbol for this sort) */
27: public AbstractNonCollectionSort(Name name) {
28: super (name);
29: setSort = new SetSort(this );
30: bagSort = new BagSort(this );
31: sequenceSort = new SequenceSort(this );
32: }
33:
34: public CollectionSort getSetSort() {
35: return setSort;
36: }
37:
38: public CollectionSort getBagSort() {
39: return bagSort;
40: }
41:
42: public CollectionSort getSequenceSort() {
43: return sequenceSort;
44: }
45:
46: public SortDependingSymbol lookupSymbol(Name p_name) {
47: SortDependingSymbol result = super .lookupSymbol(p_name);
48: if (result == null) {
49: result = setSort.lookupSymbol(p_name);
50: }
51: if (result == null) {
52: result = bagSort.lookupSymbol(p_name);
53: }
54: if (result == null) {
55: result = sequenceSort.lookupSymbol(p_name);
56: }
57: return result;
58: }
59:
60: public void addDefinedSymbols(Namespace functions, Namespace sorts) {
61: super.addDefinedSymbols(functions, sorts);
62: setSort.addDefinedSymbols(functions, sorts);
63: bagSort.addDefinedSymbols(functions, sorts);
64: sequenceSort.addDefinedSymbols(functions, sorts);
65: }
66: }
|