001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic.sort;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.Namespace;
015: import de.uka.ilkd.key.logic.op.ListOfSortDependingSymbol;
016: import de.uka.ilkd.key.logic.op.SLListOfSortDependingSymbol;
017: import de.uka.ilkd.key.logic.op.SortDependingFunction;
018:
019: public class SetSort extends AbstractCollectionSort {
020:
021: /** creates a Sort (with a new equality symbol for this sort) */
022: protected SetSort(de.uka.ilkd.key.logic.sort.Sort elemSort) {
023: super (elemSort.name() + "{}", elemSort);
024: }
025:
026: /**
027: * @return an object of this class with elementSort().equals(p),
028: * or null if such an object cannot be constructed (as p is an
029: * incompatible sort)
030: */
031: public Sort cloneFor(Sort p) {
032: if (p instanceof AbstractNonCollectionSort)
033: return ((AbstractNonCollectionSort) p).getSetSort();
034: else
035: return null;
036: }
037:
038: protected void createSymbols(Namespace p_func_ns, Namespace sort_ns) {
039: if (!symbolsCreated) {
040: super .createSymbols(p_func_ns, sort_ns);
041:
042: ListOfSortDependingSymbol res = SLListOfSortDependingSymbol.EMPTY_LIST;
043:
044: final Sort intSort = (Sort) sort_ns.lookup(new Name("int"));
045: if (intSort == null) {
046: return;
047: }
048:
049: res = createSymbol(res, "size", intSort,
050: new Sort[] { this });
051:
052: if (elementSort() == intSort) {
053: res = createSymbol(res, "sum", intSort,
054: new Sort[] { this });
055: }
056:
057: res = createSymbol(res, "count", intSort, new Sort[] {
058: this , elementSort() });
059:
060: res = createSymbol(res, "union", this , new Sort[] { this ,
061: this });
062: res = createSymbol(res, "intersection", this , new Sort[] {
063: this , this });
064: res = createSymbol(res, "without", this , new Sort[] { this ,
065: this });
066: res = createSymbol(res, "symmetricDifference", this ,
067: new Sort[] { this , this });
068: res = createSymbol(res, "including", this , new Sort[] {
069: this , elementSort() });
070:
071: res = createSymbol(res, "excluding", this , new Sort[] {
072: this , elementSort() });
073:
074: res = createSymbol(res, "includes", Sort.FORMULA,
075: new Sort[] { this , elementSort() });
076: res = createSymbol(res, "excludes", Sort.FORMULA,
077: new Sort[] { this , elementSort() });
078: res = createSymbol(res, "isEmpty", Sort.FORMULA,
079: new Sort[] { this });
080: res = createSymbol(res, "notEmpty", Sort.FORMULA,
081: new Sort[] { this });
082: res = createSymbol(res, "emptySet", this , new Sort[0]);
083:
084: addSymbols(res);
085: }
086: }
087:
088: private ListOfSortDependingSymbol createSymbol(
089: ListOfSortDependingSymbol p_list, String p_name,
090: Sort p_valueSort, Sort[] p_argSorts) {
091:
092: Name kind = new Name("Set::" + p_name);
093: Name fullname = new Name(elementSort().name() + "{}" + "::"
094: + p_name);
095:
096: SortDependingFunction f = new SortDependingFunction(fullname,
097: p_valueSort, p_argSorts, kind, elementSort());
098:
099: return p_list.prepend(f);
100: }
101:
102: }
|