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.io.IOException;
014:
015: import org.apache.log4j.Logger;
016:
017: import de.uka.ilkd.key.java.ProgramElement;
018: import de.uka.ilkd.key.logic.ProgramElementName;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT;
021: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.rule.IteratorOfObject;
025: import de.uka.ilkd.key.rule.ListOfObject;
026: import de.uka.ilkd.key.util.Debug;
027:
028: /**
029: * Encapsulate the concrete syntax used to print a term. The {@link
030: * NotationInfo} class associates a Notation with every {@link
031: * de.uka.ilkd.key.logic.op.Operator}. The various inner classes of this class
032: * represent different kinds of concrete syntax, like prefix, infix, postfix,
033: * function style, attribute style, etc.
034: */
035: public abstract class Notation {
036:
037: /**
038: * The priority of this operator in the given concrete syntax. This is
039: * used to determine whether parentheses are required around a subterm.
040: */
041: protected int priority;
042:
043: /** Create a Notation with a given priority. */
044: protected Notation(int priority) {
045: this .priority = priority;
046: }
047:
048: /** get the priority of the term */
049: public int getPriority() {
050: return priority;
051: }
052:
053: /**
054: * Print a term to a {@link LogicPrinter}. Concrete subclasses override
055: * this to call one of the <code>printXYZTerm</code> of
056: * {@link LogicPrinter}, which do the layout.
057: */
058: public void print(Term t, LogicPrinter sp) throws IOException {
059: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
060: sp.printTerm(t);
061: } else {
062: sp.printConstant(t.toString());
063: System.err.println("There is no registered Notation "
064: + "for the operator\n" + t.op());
065: }
066: }
067:
068: /**
069: * Print a term without beginning a new block. See
070: * {@link LogicPrinter#printTermContinuingBlock(Term)}for the idea
071: * behind this. The standard implementation just delegates to
072: * {@link #print(Term,LogicPrinter)}
073: */
074: public void printContinuingBlock(Term t, LogicPrinter sp)
075: throws IOException {
076: print(t, sp);
077: }
078:
079: /**
080: * The standard concrete syntax for constants like true and false.
081: */
082: public static class Constant extends Notation {
083: String name;
084:
085: public Constant(String name, int prio) {
086: super (prio);
087: this .name = name;
088: }
089:
090: public void print(Term t, LogicPrinter sp) throws IOException {
091: sp.printConstant(name);
092: }
093: }
094:
095: /**
096: * The standard concrete syntax for prefix operators.
097: */
098: public static class Prefix extends Notation {
099: String name;
100:
101: int ass;
102:
103: public Prefix(String name, int prio, int ass) {
104: super (prio);
105: this .name = name;
106: this .ass = ass;
107: }
108:
109: public void print(Term t, LogicPrinter sp) throws IOException {
110: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
111: sp.printTerm(t);
112: } else {
113: sp.printPrefixTerm(name, t.sub(0), ass);
114: }
115: }
116:
117: }
118:
119: /**
120: * The standard concrete syntax for infix operators.
121: */
122: public static class Infix extends Notation {
123: String name;
124:
125: int assLeft, assRight;
126:
127: public Infix(String name, int prio, int assLeft, int assRight) {
128: super (prio);
129: this .name = name;
130: this .assLeft = assLeft;
131: this .assRight = assRight;
132: }
133:
134: public void print(Term t, LogicPrinter sp) throws IOException {
135: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
136: sp.printTerm(t);
137: } else {
138: sp.printInfixTerm(t.sub(0), assLeft, name, t.sub(1),
139: assRight);
140: }
141: }
142:
143: /**
144: * Print a term without beginning a new block. This calls the
145: * {@link LogicPrinter#printTermContinuingBlock(Term)} method.
146: */
147: public void printContinuingBlock(Term t, LogicPrinter sp)
148: throws IOException {
149: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
150: sp.printTerm(t);
151: } else {
152: sp.printInfixTermContinuingBlock(t.sub(0), assLeft,
153: name, t.sub(1), assRight);
154: }
155: }
156:
157: }
158:
159: /**
160: * The standard concrete syntax for arrays.
161: */
162: public static class ArrayNot extends Notation {
163:
164: final private String[] arraySeparators;
165:
166: private final int[] ass;
167:
168: public ArrayNot(String[] arraySeparators, int prio, int[] ass) {
169: super (prio);
170: this .arraySeparators = arraySeparators;
171: this .ass = ass;
172: }
173:
174: public void print(Term t, LogicPrinter sp) throws IOException {
175: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
176: sp.printTerm(t);
177: } else {
178: sp.printArray(arraySeparators, t, ass);
179: }
180: }
181: }
182:
183: /**
184: * The standard concrete syntax for quantifiers.
185: */
186: public static class Quantifier extends Notation {
187: String name;
188:
189: int ass;
190:
191: public Quantifier(String name, int prio, int ass) {
192: super (prio);
193: this .name = name;
194: this .ass = ass;
195: }
196:
197: public void print(Term t, LogicPrinter sp) throws IOException {
198: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
199: sp.printTerm(t);
200: } else {
201: sp.printQuantifierTerm(name, t.varsBoundHere(0), t
202: .sub(0), ass);
203: }
204: }
205:
206: }
207:
208: /**
209: * The standard concrete syntax for DL modalities box and diamond.
210: */
211: public static class Modality extends Notation {
212: String left, right;
213:
214: int ass;
215:
216: public Modality(String left, String right, int prio, int ass) {
217: super (prio);
218: this .left = left;
219: this .right = right;
220: this .ass = ass;
221: }
222:
223: public void print(Term t, LogicPrinter sp) throws IOException {
224: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
225: sp.printTerm(t);
226: } else {
227: sp
228: .printModalityTerm(left, t.javaBlock(), right,
229: t, ass);
230: }
231: }
232: }
233:
234: /**
235: * The concrete syntax for DL modalities represented with a
236: * SchemaVariable.
237: */
238: public static class ModalSVNotation extends Notation {
239: int ass;
240:
241: public ModalSVNotation(int prio, int ass) {
242: super (prio);
243: this .ass = ass;
244: }
245:
246: public void print(Term t, LogicPrinter sp) throws IOException {
247: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
248: sp.printTerm(t);
249: } else {
250: sp.printModalityTerm("\\modality{"
251: + t.op().name().toString() + "}",
252: t.javaBlock(), "\\endmodality", t, ass);
253: }
254: }
255: }
256:
257: /**
258: * The standard concrete syntax for terms with updates.
259: */
260: public static class AnonymousUpdate extends Notation {
261:
262: public AnonymousUpdate() {
263: super (115);
264: }
265:
266: public void print(Term t, LogicPrinter sp) throws IOException {
267: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
268: sp.printTerm(t);
269: } else {
270: final int assTarget = (t.sort() == Sort.FORMULA ? (((IUpdateOperator) t
271: .op()).target(t).op() == Op.EQUALS ? 75 : 60)
272: : 110);
273: sp.printAnonymousUpdate(t, assTarget);
274: }
275: }
276: }
277:
278: /**
279: * The standard concrete syntax for terms with updates.
280: */
281: public static class QuanUpdate extends Notation {
282:
283: public QuanUpdate() {
284: super (115);
285: }
286:
287: public void print(Term t, LogicPrinter sp) throws IOException {
288: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
289: sp.printTerm(t);
290: } else {
291: final Operator targetOp = ((IUpdateOperator) t.op())
292: .target(t).op();
293: final int assTarget = (t.sort() == Sort.FORMULA ? (targetOp
294: .arity() == 1 ? 60 : 85)
295: : 110);
296: if (t.op() instanceof AnonymousUpdate) {
297: sp.printAnonymousUpdate(t, assTarget);
298: } else {
299: sp.printQuanUpdateTerm("{", ":=", "}", t, 80, 0,
300: assTarget);
301: }
302: }
303: }
304: }
305:
306: /**
307: * The standard concrete syntax for substitution terms.
308: */
309: public static class Subst extends Notation {
310: public Subst() {
311: super (120);
312: }
313:
314: public void print(Term t, LogicPrinter sp) throws IOException {
315: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
316: sp.printTerm(t);
317: } else {
318: QuantifiableVariable v = instQV(t, sp, 1);
319: final int assTarget = (t.sort() == Sort.FORMULA ? (t
320: .sub(1).op() == Op.EQUALS ? 75 : 60) : 110);
321: sp.printSubstTerm("{\\subst ", v, t.sub(0), 0, "}", t
322: .sub(1), assTarget);
323: }
324: }
325: }
326:
327: /**
328: * The standard concrete syntax for function and predicate terms.
329: */
330: static class Function extends Notation {
331:
332: public Function() {
333: super (130);
334: }
335:
336: public void print(Term t, LogicPrinter sp) throws IOException {
337: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
338: sp.printTerm(t);
339: } else {
340: sp.printFunctionTerm(t.op().name().toString(), t);
341: }
342: }
343: }
344:
345: /**
346: * The standard concrete syntax for a non rigid function with explicit
347: * known dependencies.
348: */
349: static class NRFunctionWithDependenciesNotation extends Notation {
350:
351: public NRFunctionWithDependenciesNotation() {
352: super (130);
353: }
354:
355: public void print(Term t, LogicPrinter sp) throws IOException {
356: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
357: sp.printTerm(t);
358: } else {
359: final NRFunctionWithExplicitDependencies func = (NRFunctionWithExplicitDependencies) t
360: .op();
361: StringBuffer name = new StringBuffer(func.classifier());
362: name
363: .append(NRFunctionWithExplicitDependencies.DEPENDENCY_LIST_STARTER);
364:
365: final int depSize = func.dependencies().size();
366: for (int i = 0; i < depSize; i++) {
367:
368: Location loc = func.dependencies().getLocation(i);
369: if (loc instanceof ProgramVariable
370: && ((ProgramVariable) loc).isMember()) {
371: loc = AttributeOp
372: .getAttributeOp((ProgramVariable) loc);
373: }
374:
375: if (loc instanceof AttributeOp) {
376: name.append(Attribute.printName(
377: (AttributeOp) loc, null, null)
378: .substring(1));
379: } else {
380: name.append(loc.name());
381: }
382: name
383: .append(NRFunctionWithExplicitDependencies.DEPENDENCY_LIST_SEPARATOR);
384: }
385: if (depSize == 0) {
386: name
387: .append(NRFunctionWithExplicitDependencies.DEPENDENCY_LIST_SEPARATOR);
388: }
389: name
390: .append(NRFunctionWithExplicitDependencies.DEPENDENCY_LIST_END);
391: sp.printFunctionTerm(name.toString(), t);
392: }
393: }
394: }
395:
396: /**
397: * The standard concrete syntax for arrays.
398: */
399: public static class CastFunction extends Notation {
400:
401: final String pre, post;
402:
403: final int ass;
404:
405: public CastFunction(String pre, String post, int prio, int ass) {
406: super (prio);
407: this .pre = pre;
408: this .post = post;
409: this .ass = ass;
410: }
411:
412: public void print(Term t, LogicPrinter sp) throws IOException {
413: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
414: sp.printTerm(t);
415: } else {
416: sp.printCast(pre, post, t, ass);
417: }
418: }
419: }
420:
421: /**
422: * The standard concrete syntax for query terms <code>o.q(x)</code>.
423: */
424: static class ProgramMethod extends Notation {
425: private final int ass;
426:
427: public ProgramMethod(int ass) {
428: super (130);
429: this .ass = ass;
430: }
431:
432: public void print(Term t, LogicPrinter sp) throws IOException {
433: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
434: sp.printTerm(t);
435: } else if (((de.uka.ilkd.key.logic.op.ProgramMethod) t.op())
436: .isStatic()) {
437:
438: sp.printFunctionTerm(t.op().name().toString()
439: .replaceAll("::", "."), t);
440: } else {
441: final ProgramElementName name = (ProgramElementName) t
442: .op().name();
443: sp.printQueryTerm(name.getProgramName() + "@("
444: + name.getQualifier() + ")", t, ass);
445: }
446: }
447: }
448:
449: /**
450: * The standard concrete syntax for attribute terms <code>o.a</code>.
451: */
452: static class Attribute extends Notation {
453:
454: private int associativity;
455:
456: public Attribute(int priority, int associativity) {
457: super (priority);
458: this .associativity = associativity;
459: }
460:
461: /**
462: * prints an attribute operator
463: */
464: public static String printName(AttributeOp op, Term refPrefix,
465: LogicPrinter sp) {
466: final IProgramVariable ivar = op.attribute();
467: if (!(ivar instanceof ProgramVariable)) {
468: return op.toString();
469: }
470: final ProgramVariable pvar = ((ProgramVariable) ivar);
471:
472: final String qualifier = pvar.getProgramElementName()
473: .getQualifier();
474: final String programName = pvar.getProgramElementName()
475: .getProgramName();
476:
477: if (qualifier.length() == 0
478: || (refPrefix != null && sp != null && sp
479: .printInShortForm(programName, refPrefix))) {
480: return "." + programName;
481: }
482:
483: return "." + programName + "@(" + qualifier + ")";
484:
485: }
486:
487: public void print(Term t, LogicPrinter sp) throws IOException {
488: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
489: sp.printTerm(t);
490: } else {
491: if (t.op() instanceof AttributeOp) {
492: sp.printPostfixTerm(t.sub(0), associativity,
493: printName((AttributeOp) t.op(), t.sub(0),
494: sp));
495: } else {
496: sp.printPostfixTerm(t.sub(0), associativity, "."
497: + t.op().name());
498: }
499: }
500: }
501: }
502:
503: /**
504: * The standard concrete syntax for attribute terms <code>o.a</code>.
505: */
506: static class ShadowAttribute extends Notation {
507:
508: private int associativity;
509:
510: public ShadowAttribute(int priority, int associativity) {
511: super (priority);
512: this .associativity = associativity;
513: }
514:
515: public void print(Term t, LogicPrinter sp) throws IOException {
516: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
517: sp.printTerm(t);
518: } else {
519: sp.printShadowedAttribute(t.sub(0), associativity,
520: Attribute.printName(((AttributeOp) t.op()), t
521: .sub(0), sp), t.sub(1));
522: }
523: }
524: }
525:
526: /**
527: * The standard concrete syntax for conditional terms
528: * <code>if (phi) (t1) (t2)</code>.
529: */
530: static class IfThenElse extends Notation {
531:
532: private final String keyword;
533:
534: public IfThenElse(int priority, String keyw) {
535: super (priority);
536: keyword = keyw;
537: }
538:
539: public void print(Term t, LogicPrinter sp) throws IOException {
540: if (sp.getNotationInfo().getAbbrevMap().isEnabled(t)) {
541: sp.printTerm(t);
542: } else {
543: sp.printIfThenElseTerm(t, keyword);
544: }
545: }
546: }
547:
548: /**
549: * The standard concrete syntax for all kinds of variables.
550: */
551: static class VariableNotation extends Notation {
552: public VariableNotation() {
553: super (1000);
554: }
555:
556: public void print(Term t, LogicPrinter sp) throws IOException {
557: if (t.op() instanceof ProgramVariable) {
558: sp.printConstant(t.op().name().toString().replaceAll(
559: "::", "."));
560: } else {
561: Debug.out("Unknown variable type");
562: sp.printConstant(t.op().name().toString());
563: }
564: }
565: }
566:
567: static class SortedSchemaVariableNotation extends VariableNotation {
568: static Logger logger = Logger.getLogger(Notation.class
569: .getName());
570:
571: public void print(Term t, LogicPrinter sp) throws IOException {
572: // logger.debug("SSV: " + t+ " [" + t.op() + "]");
573: Debug.assertTrue(t.op() instanceof SchemaVariable);
574: Object o = sp.getInstantiations().getInstantiation(
575: (SchemaVariable) (t.op()));
576: if (o == null) {
577: // logger.debug("Instantiation of " + t+ " [" + t.op() + "]" + "
578: // not known.");
579: sp.printConstant(t.op().name().toString());
580: } else {
581: if (o instanceof ProgramElement) {
582: // logger.debug(t.toString() + " [" + t.op() + "]" + "
583: // is a ProgramElement.");
584: sp.printProgramElement((ProgramElement) o);
585: } else {
586: // logger.debug("Instantiation of " + t+ " [" + t.op() +
587: // "]" + " known.");
588: if (o instanceof ListOfObject) {
589: final IteratorOfObject it = ((ListOfObject) o)
590: .iterator();
591: sp.getLayouter().print("{");
592: while (it.hasNext()) {
593: final Object next = it.next();
594: if (next instanceof Term) {
595: sp.printTerm((Term) o);
596: } else {
597: sp.printConstant(o.toString());
598: }
599: if (it.hasNext()) {
600: sp.getLayouter().print(",");
601: }
602: }
603: sp.getLayouter().print("}");
604: } else {
605: Debug.assertTrue(o instanceof Term);
606: sp.printTerm((Term) o);
607: }
608: }
609: }
610: }
611: }
612:
613: static class MetavariableNotation extends Notation {
614: public MetavariableNotation() {
615: super (1000);
616: }
617:
618: public void print(Term t, LogicPrinter sp) throws IOException {
619: sp
620: .printMetavariable((de.uka.ilkd.key.logic.op.Metavariable) t
621: .op());
622: }
623: }
624:
625: /**
626: * The standard concrete syntax for the number literal indicator `Z'.
627: * This is only used in the `Pretty&Untrue' syntax.
628: */
629: static class NumLiteral extends Notation {
630: public NumLiteral() {
631: super (120);
632: }
633:
634: public static String printNumberTerm(Term numberTerm) {
635: Term t = numberTerm;
636:
637: // skip number symbol /as this method may be called
638: // e.g. by char literal we do not fail if the first is
639: // not the number symbol
640: if (t.op().name().equals(AbstractIntegerLDT.NUMBERS_NAME)) {
641: t = t.sub(0);
642: }
643:
644: final StringBuffer number = new StringBuffer();
645: int offset = 0;
646:
647: if (t.op().name().toString().equals(
648: IntegerLDT.NEGATIVE_LITERAL_STRING)) {
649: number.append("-");
650: t = t.sub(0);
651: offset = 1;
652: }
653:
654: do {
655: final String opName = t.op().name() + "";
656:
657: if (t.arity() != 1
658: || (opName.length() != 1 || !Character
659: .isDigit(opName.charAt(0)))) {
660: return null; // not a number
661: } else {
662: number.insert(offset, opName);
663: }
664: t = t.sub(0);
665: } while (t.arity() != 0);
666:
667: return number.toString();
668: }
669:
670: public void print(Term t, LogicPrinter sp) throws IOException {
671: final String number = printNumberTerm(t);
672: if (number != null) {
673: sp.printConstant(number);
674: } else {
675: sp.printFunctionTerm(t.op().name().toString(), t);
676: }
677: }
678: }
679:
680: /**
681: * The standard concrete syntax for the character literal indicator `C'.
682: */
683: static class CharLiteral extends Notation {
684: public CharLiteral() {
685: super (1000);
686: }
687:
688: private static String printCharTerm(Term t) {
689:
690: char charVal = 0;
691: int intVal = 0;
692:
693: String result = NumLiteral.printNumberTerm(t.sub(0));
694:
695: if (result == null) {
696: return null;
697: }
698:
699: try {
700: intVal = Integer.parseInt(result);
701: charVal = (char) intVal;
702: if (intVal - charVal != 0)
703: throw new NumberFormatException(); // overflow!
704:
705: } catch (NumberFormatException ex) {
706: System.out.println("Oops. " + result
707: + " is not of type char");
708: return null;
709: }
710:
711: return ("'" + new Character(charVal)).toString() + "'";
712: }
713:
714: public void print(Term t, LogicPrinter sp) throws IOException {
715: final String charString = printCharTerm(t);
716: if (charString != null) {
717: sp.printConstant(charString);
718: } else {
719: sp.printFunctionTerm(t.op().name().toString(), t);
720: }
721: }
722: }
723:
724: /**
725: * The standard concrete syntax for the string literal indicator `cat'
726: * or `epsilon'.
727: */
728: static class StringLiteral extends Notation {
729:
730: public StringLiteral() {
731: super (1000);
732: }
733:
734: public static String printStringTerm(Term t) {
735: String result = "\"";
736: Term term = t;
737: while (term.op().arity() != 0) {
738: result = result
739: + CharLiteral.printCharTerm(term.sub(0))
740: .charAt(1);
741: term = term.sub(1);
742: }
743: return (result + "\"");
744: }
745:
746: public void print(Term t, LogicPrinter sp) throws IOException {
747: sp.printConstant(printStringTerm(t));
748: }
749: }
750:
751: /**
752: * Used for OCL Simplification. The standard concrete syntax for the OCL
753: * "iterate" operation.
754: */
755: public static class OCLIterate extends Notation {
756:
757: public OCLIterate() {
758: super (130);
759: }
760:
761: public void print(Term t, LogicPrinter sp) throws IOException {
762: QuantifiableVariable iterVar = t.varsBoundHere(2)
763: .getQuantifiableVariable(0);
764: QuantifiableVariable accVar = t.varsBoundHere(2)
765: .getQuantifiableVariable(1);
766: sp.printOCLIterateTerm(t.sub(0), "->", "iterate", "(", ""
767: + iterVar.name() + ":" + iterVar.sort().name(),
768: "; ", "" + accVar.name() + ":"
769: + accVar.sort().name(), "=", t.sub(1),
770: " | ", t.sub(2), ")");
771: }
772: }
773:
774: /**
775: * Used for OCL Simplification. The standard concrete syntax for the OCL
776: * collection operations with one iteration variable.
777: */
778: public static class OCLCollOpBoundVar extends Notation {
779: String name;
780:
781: public OCLCollOpBoundVar(String name) {
782: super (130);
783: this .name = name;
784: }
785:
786: public void print(Term t, LogicPrinter sp) throws IOException {
787: QuantifiableVariable iterVar = t.varsBoundHere(1)
788: .getQuantifiableVariable(0);
789: sp.printOCLCollOpBoundVarTerm(t.sub(0), "->", name, "(", ""
790: + iterVar.name() + ":" + iterVar.sort().name(),
791: " | ", t.sub(1), ")");
792: }
793: }
794:
795: /**
796: * Used for OCL Simplification. The standard concrete syntax for the OCL
797: * collection operations without iteration variables.
798: */
799: public static class OCLCollOp extends Notation {
800: String name;
801:
802: public OCLCollOp(String name) {
803: super (130);
804: this .name = name;
805: }
806:
807: public void print(Term t, LogicPrinter sp) throws IOException {
808: sp.printOCLCollOpTerm(name, t);
809: }
810: }
811:
812: /**
813: * Used for OCL Simplification. The standard concrete syntax for the OCL
814: * "dot" operations.
815: */
816: public static class OCLDotOp extends Notation {
817: String name;
818:
819: int ass;
820:
821: public OCLDotOp(String name, int ass) {
822: super (130);
823: this .name = name;
824: this .ass = ass;
825: }
826:
827: public void print(Term t, LogicPrinter sp) throws IOException {
828: sp.printQueryTerm(name, t, ass);
829: }
830: }
831:
832: /**
833: * Used for OCL Simplification. The standard concrete syntax for the OCL
834: * if-then-else-endif operation.
835: */
836: public static class OCLIf extends Notation {
837:
838: public OCLIf() {
839: super (125);
840: }
841:
842: public void print(Term t, LogicPrinter sp) throws IOException {
843: sp.printOCLIfTerm("if ", t.sub(0), "then ", t.sub(1),
844: "else ", t.sub(2), "endif");
845: }
846: }
847:
848: /**
849: * Used for OCL Simplification. The standard concrete syntax for OCL
850: * collections.
851: */
852: public static class OCLCollection extends Notation {
853: String name;
854:
855: public OCLCollection(String name) {
856: super (130);
857: this .name = name;
858: }
859:
860: public void print(Term t, LogicPrinter sp) throws IOException {
861: sp.layouter.beginI(0);
862: sp.layouter.print(name + "{");
863: sp.printOCLCollectionTerm(t);
864: sp.layouter.print("}").end();
865: }
866: }
867:
868: /**
869: * Used for OCL Simplification. The standard concrete syntax for the OCL
870: * wrapper predicate.
871: */
872: public static class OCLWrapper extends Notation {
873:
874: public OCLWrapper() {
875: super (130);
876: }
877:
878: public void print(Term t, LogicPrinter sp) throws IOException {
879: sp.printOCLWrapperTerm(t);
880: }
881: }
882:
883: /**
884: * Used for OCL Simplification. The standard concrete syntax for an OCL
885: * invariant.
886: */
887: public static class OCLInvariant extends Notation {
888:
889: public OCLInvariant() {
890: super (130);
891: }
892:
893: public void print(Term t, LogicPrinter sp) throws IOException {
894: sp.printOCLInvariantTerm(t.sub(0), t.sub(1));
895: }
896: }
897:
898: /**
899: * Used for OCL Simplification. The concrete syntax for a list of OCL
900: * invariants.
901: */
902: public static class OCLListOfInvariants extends Notation {
903:
904: public OCLListOfInvariants() {
905: super (130);
906: }
907:
908: public void print(Term t, LogicPrinter sp) throws IOException {
909: sp.layouter.beginI(0);
910: sp.layouter.brk(0, -1).print("[\n");
911: sp.printOCLListOfInvariantsTerm(t);
912: sp.layouter.print("\n]").end();
913: }
914: }
915:
916: /**
917: * @param t
918: * @param sp
919: * @param subTerm
920: * TODO
921: * @return
922: */
923: protected QuantifiableVariable instQV(Term t, LogicPrinter sp,
924: int subTerm) {
925: QuantifiableVariable v = t.varsBoundHere(subTerm)
926: .getQuantifiableVariable(0);
927:
928: if (v instanceof SchemaVariable) {
929: Object object = (sp.getInstantiations()
930: .getInstantiation((SchemaVariable) v));
931: if (object != null) {
932: Debug.assertTrue(object instanceof Term);
933: Debug
934: .assertTrue(((Term) object).op() instanceof QuantifiableVariable);
935: v = (QuantifiableVariable) (((Term) object).op());
936: }
937: }
938: return v;
939: }
940: }
|