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 java.util.HashMap;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.util.Service;
019:
020: /**
021: * <p>
022: * Stores the mapping from operators to {@link Notation}s. Each
023: * {@link Notation} represents the concrete syntax for some
024: * {@link de.uka.ilkd.key.logic.op.Operator}. The {@link LogicPrinter}
025: * asks the NotationInfo to find out which Notation to use for a given term.
026: * <p>
027: * The Notation associated with an operator might change. New Notations can
028: * be added.
029: *
030: * Support for infix notations in case of function symbols like
031: * <code>+, -, *, /, <, >, </code>
032: * etc. is added by class {@link de.uka.ilkd.key.pp.PresentationFeatures} (that has
033: * historical reasons)
034: * <p>
035: * The next lines describe a general rule how to determine priorities and
036: * associativities:
037: *
038: * One thing we need to know from the pretty printer:
039: * Given a term <tt>t</tt> containg <tt>s</tt> as proper subterm.
040: * Then <tt>s</tt> is printed in parentheses when the priority of the
041: * top level symbol of <tt>s</tt> is strict less than the associativity of the
042: * position where <tt>s</tt> occurs. For example:
043: * <p>
044: * Let the priority of <tt>AND</tt> be <tt>30</tt> and the associativities for each
045: * of its subterms be 40; <tt>OR</tt>s priority is <tt>20</tt> and the associativites are
046: * both <tt>30</tt> then
047: * <ul> <li> formula <tt>(p & q) | r</tt> is pretty printed as <tt>p & q | r</tt>
048: * as the priority of & is 30 which is (greater or) equal than the
049: * associativity of <tt>OR</tt>s left subterm which is 30.</li>
050: * <li> In contrast the formula <tt>p & (q | r)</tt> is pretty printed as
051: * <tt>p & (q | r)</tt> as the priority of <tt>OR</tt> is 20 which is less than
052: * the associativity of <tt>AND</tt>s left subterm, which is 40.</li>
053: * </ul>
054: *
055: * A general rule to determine the correct priority and associativity is to use:
056: *
057: * Grammar rules whose derivation delivers a syntactical correct logic term should follow
058: * a standard numbering scheme, which is used as indicator for priorities and associativites,
059: * e.g.
060: * by simply reading the grammar rule
061: * <blockquote><tt>term60 ::= term70 (IMP term70)?</tt></blockquote>
062: * we get the priority of <tt>IMP</tt>, which is <tt>60</tt>. The associativities
063: * of <tt>IMP</tt>s subterms are not much more difficult to determine, namely
064: * the left subterm has associativity <tt>70</tt> and in this case its the same
065: * for the right subterm (<tt>70</tt>).
066: * <p>
067: * There are exceptional cases for
068: * <ul>
069: * <li> <em>infix function</em> symbols that are left associative e.g.
070: * <code>-, +</code>
071: * <blockquote>
072: * <tt> term90 ::= term100 (PLUS term100)* </tt>
073: * </blockquote>
074: * then the associative for the right subterm is increased by <tt>1</tt>,
075: * i.e. here we have a priority of <tt>90</tt> for <tt>PLUS</tt> as infix operator,
076: * a left associativity of <tt>100</tt> <em>and</em> a right associativity of <tt>101</tt>
077: * </li>
078: * <li> update and substituition terms: for them their associativity is
079: * determined dynamically by the pretty printer depending if it is applied on a
080: * formula or term. In principal there should be two different
081: * rules in the parser as then we could reuse the general rule from above, but
082: * there are technical reasons which causes this exception.
083: * </li>
084: * <li> some very few rules do not follow the usual parser design
085: * e.g. like
086: * <blockquote><tt>R_PRIO ::= SubRule_ASS1 | SubRule_ASS2 </tt></blockquote>
087: * where
088: * <blockquote><tt>SubRule_ASS2 ::= OP SubRule_ASS1</tt></blockquote>
089: * Most of these few rules could in general be rewritten to fit the usual scheme
090: * e.g. as
091: * <blockquote><tt> R_PRIO ::= (OP)? SubRule_ASS1</tt></blockquote>
092: * using the priorities and associativities of the so rewritten rules
093: * (instead of rewriting them actually) is a way to cope with them.
094: * </li>
095: * </ul>
096: */
097: public class NotationInfo {
098:
099: /** Factory method: creates a new NotationInfo instance. The
100: * actual implementation depends on system properties or service
101: * entries. */
102: public static final NotationInfo createInstance() {
103: return (NotationInfo) Service.find(
104: NotationInfo.class.getName(), NotationInfo.class
105: .getName());
106: }
107:
108: /** This maps operators and classes of operators to {@link
109: * Notation}s. The idea is that we first look wether the operator has
110: * a Notation registered. Otherwise, we see if there is one for the
111: * <em>class</em> of the operator.
112: */
113: private HashMap tbl;
114:
115: /**
116: * Maps terms to abbreviations and reverse.
117: */
118: private AbbrevMap scm;
119:
120: /** Create a new NotationInfo. Do not call this constructor
121: * directly. Use the factory method {@link createInstance}
122: * instead. */
123: public NotationInfo() {
124: createDefaultNotationTable();
125: }
126:
127: /** Set all notations back to default. */
128: public void setBackToDefault() {
129: createDefaultNotationTable();
130: }
131:
132: /** Register the standard set of notations. This means no
133: * abbreviations, and a set of Notations for the built-in operators
134: * which corresponds to the parser syntax.
135: */
136: private void createDefaultNotationTable() {
137: tbl = new HashMap();
138: createDefaultOpNotation();
139: createDefaultTermSymbolNotation();
140: scm = new AbbrevMap();
141: }
142:
143: /**
144: * Registers notations for the built-in operators. The priorities
145: * and associativities correspond to the parser syntax.
146: */
147: private void createDefaultOpNotation() {
148: tbl.put(Op.TRUE, new Notation.Constant("true", 130));
149: tbl.put(Op.FALSE, new Notation.Constant("false", 130));
150: tbl.put(Op.NOT, new Notation.Prefix("!", 60, 60));
151: tbl.put(Op.AND, new Notation.Infix("&", 50, 50, 60));
152: tbl.put(Op.OR, new Notation.Infix("|", 40, 40, 50));
153: tbl.put(Op.IMP, new Notation.Infix("->", 30, 40, 30));
154: tbl.put(Op.EQV, new Notation.Infix("<->", 20, 20, 30));
155:
156: tbl.put(Op.ALL, new Notation.Quantifier("\\forall", 60, 60));
157: tbl.put(Op.EX, new Notation.Quantifier("\\exists", 60, 60));
158: tbl.put(Op.DIA, new Notation.Modality("\\<", "\\>", 60, 60));
159: tbl.put(Op.BOX, new Notation.Modality("\\[", "\\]", 60, 60));
160: tbl.put(Op.TOUT, new Notation.Modality("\\[[", "\\]]", 60, 60));
161: Modality modalities[] = { Op.DIATRC, Op.BOXTRC, Op.TOUTTRC,
162: Op.DIATRA, Op.BOXTRA, Op.TOUTTRA, Op.DIASUSP,
163: Op.BOXSUSP, Op.TOUTSUSP };
164: for (int i = 0; i < modalities.length; i++)
165: tbl.put(modalities[i], new Notation.Modality("\\"
166: + modalities[i].name().toString(), "\\endmodality",
167: 60, 60));
168: tbl.put(Op.IF_THEN_ELSE, new Notation.IfThenElse(130, "\\if"));
169: tbl.put(Op.IF_EX_THEN_ELSE, new Notation.IfThenElse(130,
170: "\\ifEx"));
171:
172: tbl.put(Op.COMPUTE_SPEC_OP, new Notation.Prefix("^", 60, 60));
173:
174: //createNumLitNotation(IntegerLDT.getStaticNumberSymbol());
175:
176: tbl.put(Op.SUBST, new Notation.Subst());
177: }
178:
179: /**
180: * Register notations for standard classes of operators. This
181: * includes Function operators, all kinds of variables, etc.
182: */
183: /**
184: * Register notations for standard classes of operators. This
185: * includes Function operators, all kinds of variables, etc.
186: */
187: private void createDefaultTermSymbolNotation() {
188: tbl.put(Function.class, new Notation.Function());
189: tbl.put(LogicVariable.class, new Notation.VariableNotation());
190: //tbl.put(SchemaVariable.class, new Notation.Variable());
191: tbl
192: .put(Metavariable.class,
193: new Notation.MetavariableNotation());
194: tbl
195: .put(LocationVariable.class,
196: new Notation.VariableNotation());
197: tbl.put(ProgramConstant.class, new Notation.VariableNotation());
198: tbl.put(ProgramMethod.class, new Notation.ProgramMethod(121));
199: tbl.put(Equality.class, new Notation.Infix("=", 70, 80, 80));
200: tbl.put(QuanUpdateOperator.class, new Notation.QuanUpdate());
201: tbl.put(AnonymousUpdate.class, new Notation.AnonymousUpdate());
202: tbl.put(ShadowAttributeOp.class, new Notation.ShadowAttribute(
203: 121, 121));
204: tbl.put(AttributeOp.class, new Notation.Attribute(121, 121));
205: tbl.put(ShadowArrayOp.class, new Notation.ArrayNot(
206: new String[] { "[", "]", "" }, 130, new int[] { 121, 0,
207: 0 }));
208: tbl.put(ArrayOp.class, new Notation.ArrayNot(new String[] {
209: "[", "]" }, 130, new int[] { 121, 0 }));
210: tbl.put(CastFunctionSymbol.class, new Notation.CastFunction(
211: "(", ")", 120, 140));
212: tbl.put(NRFunctionWithExplicitDependencies.class,
213: new Notation.NRFunctionWithDependenciesNotation());
214: tbl.put(ModalOperatorSV.class, new Notation.ModalSVNotation(60,
215: 60));
216: tbl.put(SortedSchemaVariable.class,
217: new Notation.SortedSchemaVariableNotation());
218: }
219:
220: public AbbrevMap getAbbrevMap() {
221: return scm;
222: }
223:
224: public void setAbbrevMap(AbbrevMap am) {
225: scm = am;
226: }
227:
228: /** Get the Notation for a given Operator.
229: * If no notation is registered, a Function notation is returned.
230: */
231: public Notation getNotation(Operator op, Services services) {
232: if (services != null) {
233: IntegerLDT integerLDT = services.getTypeConverter()
234: .getIntegerLDT();
235: if (integerLDT != null) {
236: createNumLitNotation(integerLDT.getNumberSymbol());
237: createCharLitNotation(integerLDT.getCharSymbol());
238: }
239: }
240: createStringLitNotation(
241: de.uka.ilkd.key.java.TypeConverter.stringConverter
242: .getStringSymbol(), null);
243:
244: //For OCL Simplification
245: if (tbl.containsKey(op.name().toString())) {
246: return (Notation) tbl.get(op.name().toString());
247: }
248: //
249: else if (tbl.containsKey(op)) {
250: return (Notation) tbl.get(op);
251: } else if (tbl.containsKey(op.getClass())) {
252: return (Notation) tbl.get(op.getClass());
253: } else if (op instanceof SortedSchemaVariable) {
254: return (Notation) tbl.get(SortedSchemaVariable.class);
255: } else {
256: return new Notation.Function();
257: }
258: }
259:
260: /** Registers an infix notation for a given operator
261: * @param op the operator
262: * @param token the string representing the operator
263: */
264: public void createInfixNotation(Operator op, String token) {
265: tbl.put(op, new Notation.Infix(token, 120, 130, 130));
266: }
267:
268: /** Registers an infix notation for a given operator
269: * with given priority and associativity
270: * @param op the operator
271: * @param token the string representing the operator
272: */
273: public void createInfixNotation(Operator op, String token,
274: int prio, int lass, int rass) {
275: tbl.put(op, new Notation.Infix(token, prio, lass, rass));
276: }
277:
278: /** Registers a prefix notation for a given operator
279: * @param op the operator
280: * @param token the string representing the operator
281: */
282: public void createPrefixNotation(Operator op, String token) {
283: tbl.put(op, new Notation.Prefix(token, 140, 130));
284: }
285:
286: /** Registers a number literal notation for a given operator.
287: * This is done for the `Z' operator which marks number literals.
288: * A term <code>Z(3(2(#)))</code> gets printed simply as
289: * <code>23</code>.
290: * @param op the operator */
291: public void createNumLitNotation(Operator op) {
292: tbl.put(op, new Notation.NumLiteral());
293: }
294:
295: /** Registers a character literal notation for a given operator.
296: * This is done for the `C' operator which marks character literals.
297: * A term <code>C(3(2(#)))</code> gets printed simply as
298: * the character corresponding to the unicode value 23 (really 23
299: * and not 32, see integer literals)
300: * @param op the operator */
301: public void createCharLitNotation(Operator op) {
302: tbl.put(op, new Notation.CharLiteral());
303: }
304:
305: public void createStringLitNotation(Operator op, Operator eps) {
306: Notation.StringLiteral stringLiteral = new Notation.StringLiteral();
307: tbl.put(op, stringLiteral);
308: tbl.put(eps, stringLiteral);
309: }
310:
311: /**
312: * Used for OCL Simplification.
313: * Syntax for iterate().
314: */
315: public void createOCLIterateNotation(String token) {
316: tbl.put("$" + token, new Notation.OCLIterate());
317: }
318:
319: /**
320: * Used for OCL Simplification.
321: * Syntax for forAll(), exists(), etc.
322: */
323: public void createOCLCollOpBoundVarNotation(String token) {
324: tbl.put("$" + token, new Notation.OCLCollOpBoundVar(token));
325: }
326:
327: /**
328: * Used for OCL Simplification.
329: * Syntax for size(), includes(), etc.
330: */
331: public void createOCLCollOpNotation(String token) {
332: tbl.put("$" + token, new Notation.OCLCollOp(token));
333: }
334:
335: /**
336: * Used for OCL Simplification.
337: * Syntax for supertypes(), oclIsNew(), etc.
338: */
339: public void createOCLDotOpNotation(String token) {
340: tbl.put("$" + token, new Notation.OCLDotOp(token, 121));
341: }
342:
343: /**
344: * Used for OCL Simplification.
345: */
346: public void createOCLWrapperNotation(String token) {
347: tbl.put("$" + token, new Notation.OCLWrapper());
348: }
349:
350: /**
351: * Used for OCL Simplification.
352: * Syntax for Set{...}, Bag{...}, and Sequence{...}.
353: */
354: public void createOCLCollectionNotation(String internalName,
355: String token) {
356: tbl.put("$" + internalName, new Notation.OCLCollection(token));
357: }
358:
359: /**
360: * Used for OCL Simplification.
361: * Syntax for self, true, false, Set{}, etc.
362: */
363: public void createConstantNotation(String internalName, String token) {
364: tbl.put("$" + internalName, new Notation.Constant(token, 100));
365: }
366:
367: /**
368: * Used for OCL Simplification.
369: * Syntax for if-then-else-endif.
370: */
371: public void createOCLIfNotation(String token) {
372: tbl.put("$" + token, new Notation.OCLIf());
373: }
374:
375: /**
376: * Used for OCL Simplification.
377: * Syntax for "not" and "-".
378: */
379: public void createOCLPrefixNotation(String internalName,
380: String token, int prio, int ass) {
381: tbl.put("$" + internalName, new Notation.Prefix(token, prio,
382: ass));
383: }
384:
385: /**
386: * Used for OCL Simplification.
387: * Syntax for "and", "or", "+", "<", etc.
388: */
389: public void createOCLInfixNotation(String internalName,
390: String token, int prio, int assLeft, int assRight) {
391: tbl.put("$" + internalName, new Notation.Infix(token, prio,
392: assLeft, assRight));
393: }
394:
395: /**
396: * Used for OCL Simplification.
397: */
398: public void createOCLInvariantNotation(String token) {
399: tbl.put("$" + token, new Notation.OCLInvariant());
400: }
401:
402: /**
403: * Used for OCL Simplification.
404: */
405: public void createOCLListOfInvariantsNotation(String token) {
406: tbl.put("$" + token, new Notation.OCLListOfInvariants());
407: }
408: }
|