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.ListOfSortDependingSymbol;
16: import de.uka.ilkd.key.logic.op.SLListOfSortDependingSymbol;
17: import de.uka.ilkd.key.logic.op.SortDependingFunction;
18:
19: public class SequenceSort extends AbstractCollectionSort {
20:
21: /** creates a Sort (with a new equality symbol for this sort) */
22: protected SequenceSort(Sort elemSort) {
23: super ("Sequence" + "Of" + elemSort.name(), elemSort);
24: }
25:
26: /**
27: * @return an object of this class with elementSort().equals(p),
28: * or null if such an object cannot be constructed (as p is an
29: * incompatible sort)
30: */
31: public Sort cloneFor(Sort p) {
32: if (p instanceof AbstractNonCollectionSort)
33: return ((AbstractNonCollectionSort) p).getSequenceSort();
34: else
35: return null;
36: }
37:
38: public void createSymbols(Namespace p_func_ns, Namespace sort_ns) {
39: if (!symbolsCreated) {
40: super .createSymbols(p_func_ns, sort_ns);
41:
42: ListOfSortDependingSymbol res = SLListOfSortDependingSymbol.EMPTY_LIST;
43:
44: final Sort intSort = (Sort) sort_ns.lookup(new Name("int"));
45: if (intSort == null) {
46: return;
47: }
48:
49: res = createSymbol(res, "size", intSort,
50: new Sort[] { this });
51:
52: if (elementSort() == intSort) {
53: res = createSymbol(res, "sum", intSort,
54: new Sort[] { this });
55: }
56: res = createSymbol(res, "count", intSort, new Sort[] {
57: this , elementSort() });
58: res = createSymbol(res, "union", this , new Sort[] { this ,
59: this });
60: res = createSymbol(res, "add", this , new Sort[] { this ,
61: elementSort() });
62:
63: res = createSymbol(res, "includes", Sort.FORMULA,
64: new Sort[] { this , elementSort() });
65: res = createSymbol(res, "excludes", Sort.FORMULA,
66: new Sort[] { this , elementSort() });
67: res = createSymbol(res, "isEmpty", Sort.FORMULA,
68: new Sort[] { this });
69: res = createSymbol(res, "notEmpty", Sort.FORMULA,
70: new Sort[] { this });
71: res = createSymbol(res, "emptySequence", this , new Sort[0]);
72:
73: res = createSymbol(res, "at", elementSort(), new Sort[] {
74: this , intSort });
75:
76: addSymbols(res);
77: }
78: }
79:
80: private ListOfSortDependingSymbol createSymbol(
81: ListOfSortDependingSymbol p_list, String p_name,
82: Sort p_valueSort, Sort[] p_argSorts) {
83:
84: Name kind = new Name("Sequence::" + p_name);
85: Name fullname = new Name("Sequence" + "Of"
86: + elementSort().name() + "::" + p_name);
87:
88: SortDependingFunction f = new SortDependingFunction(fullname,
89: p_valueSort, p_argSorts, kind, elementSort());
90:
91: return p_list.prepend(f);
92: }
93:
94: }
|