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.pp;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.Namespace;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.Function;
017: import de.uka.ilkd.key.proof.Proof;
018:
019: public class PresentationFeatures {
020:
021: private PresentationFeatures() {
022: }
023:
024: private static void putInfixNotation(NotationInfo notInfo,
025: Namespace functions, String op, String token) {
026: notInfo.createInfixNotation((Function) functions
027: .lookup(new Name(op)), token);
028: }
029:
030: private static void putInfixNotation(NotationInfo notInfo,
031: Namespace functions, String op, String token, int prio,
032: int lass, int rass) {
033: notInfo.createInfixNotation((Function) functions
034: .lookup(new Name(op)), token, prio, lass, rass);
035: }
036:
037: private static void putPrefixNotation(NotationInfo notInfo,
038: Namespace functions, String op, String token) {
039: notInfo.createPrefixNotation((Function) functions
040: .lookup(new Name(op)), token);
041: }
042:
043: public static boolean ENABLED = false;
044:
045: public static void modifyNotationInfo(NotationInfo notInfo,
046: Namespace functions) {
047: if (ENABLED) {
048: putInfixNotation(notInfo, functions, "lt", "< ", 80, 90, 90);
049: putInfixNotation(notInfo, functions, "gt", "> ", 80, 90, 90);
050: putInfixNotation(notInfo, functions, "leq", "<=", 80, 90,
051: 90);
052: putInfixNotation(notInfo, functions, "geq", ">=", 80, 90,
053: 90);
054:
055: putInfixNotation(notInfo, functions, "sub", "-", 90, 90, 91);
056: putInfixNotation(notInfo, functions, "add", "+", 90, 90, 91);
057:
058: putInfixNotation(notInfo, functions, "mul", "*", 100, 100,
059: 101);
060: putInfixNotation(notInfo, functions, "div", "/", 100, 100,
061: 101);
062: putInfixNotation(notInfo, functions, "mod", "%", 100, 100,
063: 101);
064: putPrefixNotation(notInfo, functions, "neg", "-");
065: notInfo.createNumLitNotation((Function) functions
066: .lookup(new Name("Z")));
067: putPrefixNotation(notInfo, functions, "neglit", "-");
068:
069: // ******** For OCL Simplification ************
070: //iterate
071: notInfo.createOCLIterateNotation("iterate");
072:
073: //collection operations with one iteration variable
074: notInfo.createOCLCollOpBoundVarNotation("forAll");
075: notInfo.createOCLCollOpBoundVarNotation("exists");
076: notInfo.createOCLCollOpBoundVarNotation("select");
077: notInfo.createOCLCollOpBoundVarNotation("collect");
078: notInfo.createOCLCollOpBoundVarNotation("reject");
079: notInfo.createOCLCollOpBoundVarNotation("isUnique");
080: notInfo.createOCLCollOpBoundVarNotation("sortedBy");
081: notInfo.createOCLCollOpBoundVarNotation("any");
082: notInfo.createOCLCollOpBoundVarNotation("one");
083:
084: //other collection operations
085: notInfo.createOCLCollOpNotation("asSet");
086: notInfo.createOCLCollOpNotation("includes");
087: notInfo.createOCLCollOpNotation("excludes");
088: notInfo.createOCLCollOpNotation("count");
089: notInfo.createOCLCollOpNotation("includesAll");
090: notInfo.createOCLCollOpNotation("excludesAll");
091: notInfo.createOCLCollOpNotation("isEmpty");
092: notInfo.createOCLCollOpNotation("notEmpty");
093: notInfo.createOCLCollOpNotation("sum");
094: notInfo.createOCLCollOpNotation("union");
095: notInfo.createOCLCollOpNotation("intersection");
096: notInfo.createOCLCollOpNotation("including");
097: notInfo.createOCLCollOpNotation("excluding");
098: notInfo.createOCLCollOpNotation("symmetricDifference");
099: notInfo.createOCLCollOpNotation("asSequence");
100: notInfo.createOCLCollOpNotation("asBag");
101: notInfo.createOCLCollOpNotation("append");
102: notInfo.createOCLCollOpNotation("prepend");
103: notInfo.createOCLCollOpNotation("subSequence");
104: notInfo.createOCLCollOpNotation("at");
105: notInfo.createOCLCollOpNotation("first");
106: notInfo.createOCLCollOpNotation("last");
107: notInfo.createOCLCollOpNotation("size");
108:
109: //non-infix operations on OclType, OclAny, Real, Integer, String
110: notInfo.createOCLDotOpNotation("allSubtypes");
111: notInfo.createOCLDotOpNotation("allInstances");
112: notInfo.createOCLDotOpNotation("name");
113: notInfo.createOCLDotOpNotation("attributes");
114: notInfo.createOCLDotOpNotation("associationEnds");
115: notInfo.createOCLDotOpNotation("operations");
116: notInfo.createOCLDotOpNotation("supertypes");
117: notInfo.createOCLDotOpNotation("allSupertypes");
118: notInfo.createOCLDotOpNotation("oclIsKindOf");
119: notInfo.createOCLDotOpNotation("oclIsTypeOf");
120: notInfo.createOCLDotOpNotation("oclAsType");
121: notInfo.createOCLDotOpNotation("oclIsNew");
122: notInfo.createOCLDotOpNotation("evaluationType");
123: notInfo.createOCLDotOpNotation("abs");
124: notInfo.createOCLDotOpNotation("floor");
125: notInfo.createOCLDotOpNotation("round");
126: notInfo.createOCLDotOpNotation("max");
127: notInfo.createOCLDotOpNotation("min");
128: notInfo.createOCLDotOpNotation("div");
129: notInfo.createOCLDotOpNotation("mod");
130: notInfo.createOCLDotOpNotation("concat");
131: notInfo.createOCLDotOpNotation("toUpper");
132: notInfo.createOCLDotOpNotation("toLower");
133: notInfo.createOCLDotOpNotation("substring");
134:
135: //prefix
136: notInfo.createOCLPrefixNotation("not", "not ", 80, 80);
137: notInfo.createOCLPrefixNotation("minusPrefix", "-", 80, 80);
138:
139: //infix
140: notInfo.createOCLInfixNotation("times", "*", 70, 70, 80);
141: notInfo.createOCLInfixNotation("divInfix", "/", 70, 70, 80);
142: notInfo.createOCLInfixNotation("plus", "+", 60, 60, 70);
143: notInfo.createOCLInfixNotation("minus", "-", 60, 60, 70);
144: notInfo.createOCLInfixNotation("lessThan", "<", 50, 50, 60);
145: notInfo.createOCLInfixNotation("lessThanEq", "<=", 50, 50,
146: 60);
147: notInfo.createOCLInfixNotation("greaterThan", ">", 50, 50,
148: 60);
149: notInfo.createOCLInfixNotation("greaterThanEq", ">=", 50,
150: 50, 60);
151: notInfo.createOCLInfixNotation("equals", "=", 40, 40, 50);
152: notInfo.createOCLInfixNotation("notEquals", "<>", 40, 40,
153: 50);
154: notInfo.createOCLInfixNotation("and", "and", 30, 30, 40);
155: notInfo.createOCLInfixNotation("or", "or", 30, 30, 40);
156: notInfo.createOCLInfixNotation("xor", "xor", 30, 30, 40);
157: notInfo.createOCLInfixNotation("implies", "implies", 20,
158: 20, 30);
159:
160: //others
161: notInfo.createOCLWrapperNotation("OclWrapper");
162: notInfo.createOCLCollectionNotation("insert_collection",
163: "Collection");
164: notInfo.createOCLCollectionNotation("insert_set", "Set");
165: notInfo.createOCLCollectionNotation("insert_bag", "Bag");
166: notInfo.createOCLCollectionNotation("insert_sequence",
167: "Sequence");
168: notInfo.createConstantNotation("empty_collection",
169: "Collection{}");
170: notInfo.createConstantNotation("empty_set", "Set{}");
171: notInfo.createConstantNotation("empty_bag", "Bag{}");
172: notInfo.createConstantNotation("empty_sequence",
173: "Sequence{}");
174: notInfo.createConstantNotation("self", "self");
175: notInfo.createConstantNotation("true", "true");
176: notInfo.createConstantNotation("false", "false");
177: notInfo.createOCLIfNotation("if");
178: notInfo.createOCLInvariantNotation("invariant");
179: notInfo.createOCLListOfInvariantsNotation("cons_inv");
180: //
181: }
182: }
183:
184: private static StringBuffer printlastfirst(Term t) {
185: if (t.op().arity() == 0) {
186: return new StringBuffer();
187: } else {
188: return printlastfirst(t.sub(0)).append(
189: t.op().name().toString());
190: }
191: }
192:
193: public static String printNumberTerm(Term t) {
194: StringBuffer sb = new StringBuffer();
195: if (t.sub(0).op().name().toString().equals("neglit")) {
196: return "-" + printlastfirst(t.sub(0).sub(0)).toString();
197: } else {
198: return printlastfirst(t.sub(0)).toString();
199: }
200: }
201:
202: public static void initialize(Namespace funcns, NotationInfo ni,
203: Proof p) {
204: if (ENABLED) {
205: modifyNotationInfo(ni, funcns);
206: if (p != null)
207: p.updateProof();
208: }
209: }
210:
211: }
|