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: //
012:
013: package de.uka.ilkd.key.logic.sort;
014:
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.Namespace;
017: import de.uka.ilkd.key.logic.op.ListOfSortDependingSymbol;
018: import de.uka.ilkd.key.logic.op.SLListOfSortDependingSymbol;
019: import de.uka.ilkd.key.logic.op.SortDependingFunction;
020:
021: public class BagSort extends
022: de.uka.ilkd.key.logic.sort.AbstractCollectionSort {
023:
024: /** creates a Sort (with a new equality symbol for this sort) */
025: protected BagSort(de.uka.ilkd.key.logic.sort.Sort elemSort) {
026: super ("Bag" + "Of" + elemSort.name(), elemSort);
027: }
028:
029: /**
030: * @return an object of this class with elementSort().equals(p),
031: * or null if such an object cannot be constructed (as p is an
032: * incompatible sort)
033: */
034: public Sort cloneFor(Sort p) {
035: if (p instanceof AbstractNonCollectionSort)
036: return ((AbstractNonCollectionSort) p).getBagSort();
037: else
038: return null;
039: }
040:
041: protected void createSymbols(Namespace p_func_ns, Namespace sort_ns) {
042: if (!symbolsCreated) {
043: super .createSymbols(p_func_ns, sort_ns);
044:
045: ListOfSortDependingSymbol res = SLListOfSortDependingSymbol.EMPTY_LIST;
046:
047: final Sort intSort = (Sort) sort_ns.lookup(new Name("int"));
048: if (intSort == null) {
049: return;
050: }
051:
052: res = createSymbol(res, "size", intSort,
053: new Sort[] { this });
054:
055: if (elementSort() == intSort) {
056: res = createSymbol(res, "sum", intSort,
057: new Sort[] { this });
058: }
059: res = createSymbol(res, "count", intSort, new Sort[] {
060: this , elementSort() });
061: res = createSymbol(res, "union", this , new Sort[] { this ,
062: this });
063: res = createSymbol(res, "intersection", this , new Sort[] {
064: this , this });
065: res = createSymbol(res, "without", this , new Sort[] { this ,
066: this });
067: res = createSymbol(res, "symmetricDifference", this ,
068: new Sort[] { this , this });
069: res = createSymbol(res, "including", this , new Sort[] {
070: this , elementSort() });
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, "emptyBag", 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("Bag::" + p_name);
093: Name fullname = new Name("Bag" + "Of" + 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: }
|