0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
0009: // Universitaet Koblenz-Landau, Germany
0010: // Chalmers University of Technology, Sweden
0011: //
0012: // The KeY system is protected by the GNU General Public License.
0013: // See LICENSE.TXT for details.
0014: //
0015: //
0016:
0017: package de.uka.ilkd.key.pp;
0018:
0019: import java.io.IOException;
0020: import java.io.StringWriter;
0021: import java.util.*;
0022:
0023: import org.apache.log4j.Logger;
0024:
0025: import de.uka.ilkd.key.java.PrettyPrinter;
0026: import de.uka.ilkd.key.java.ProgramElement;
0027: import de.uka.ilkd.key.java.Services;
0028: import de.uka.ilkd.key.java.StatementBlock;
0029: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
0030: import de.uka.ilkd.key.logic.*;
0031: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
0032: import de.uka.ilkd.key.logic.op.*;
0033: import de.uka.ilkd.key.logic.op.oclop.OclOp;
0034: import de.uka.ilkd.key.logic.sort.ObjectSort;
0035: import de.uka.ilkd.key.logic.sort.Sort;
0036: import de.uka.ilkd.key.rule.*;
0037: import de.uka.ilkd.key.rule.inst.SVInstantiations;
0038: import de.uka.ilkd.key.util.Debug;
0039: import de.uka.ilkd.key.util.pp.Backend;
0040: import de.uka.ilkd.key.util.pp.Layouter;
0041: import de.uka.ilkd.key.util.pp.StringBackend;
0042: import de.uka.ilkd.key.util.pp.UnbalancedBlocksException;
0043:
0044: /**
0045: * The front end for the Sequent pretty-printer. It prints a sequent
0046: * and its parts and computes the PositionTable, which is needed for
0047: * highliting.
0048: *
0049: * <P>The actual layouting/formatting is done using the {@link
0050: * de.uka.ilkd.key.util.pp.Layouter} class. The concrete syntax for
0051: * operators is given by an instance of {@link NotationInfo}. The
0052: * LogicPrinter is responsible for the concrete <em>layout</em>,
0053: * e.g. how terms with infix operators are indented, and it binds the
0054: * various needed components together.
0055: *
0056: * @see NotationInfo
0057: * @see Notation
0058: * @see de.uka.ilkd.key.util.pp.Layouter
0059: *
0060: *
0061: */
0062: public class LogicPrinter {
0063:
0064: /**
0065: * The default and minimal value o fthe
0066: * max. number of characters to put in one line
0067: */
0068: public static final int DEFAULT_LINE_WIDTH = 55;
0069:
0070: /** The max. number of characters to put in one line */
0071: private int lineWidth = DEFAULT_LINE_WIDTH;
0072:
0073: /**
0074: * The ProgramPrinter used to pretty-print Java blocks in
0075: * formulae.
0076: */
0077: private ProgramPrinter prgPrinter;
0078:
0079: /** Contains information on the concrete syntax of operators. */
0080: private final NotationInfo notationInfo;
0081:
0082: /** the services object */
0083: private final Services services;
0084:
0085: /** The sequent we are pretty-printing */
0086: //private Sequent seq;
0087: //private SequentPrintFilter filter;
0088: /** This chooses the layout. */
0089: protected Layouter layouter;
0090:
0091: /** The backend <code>layouter</code> will write to. */
0092: private Backend backend;
0093:
0094: /** The constraint used for metavariable instantiations of the
0095: * current formula */
0096: Constraint formulaConstraint = null;
0097:
0098: /**If pure is true the PositionTable will not be calculated */
0099: private boolean pure = false;
0100:
0101: protected SVInstantiations instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS;
0102:
0103: /** For OCL Simplification. So that OCL/UML properties
0104: are pretty-printed the right way. */
0105: private boolean oclPrettyPrinting = false;
0106:
0107: static Logger logger = Logger.getLogger(LogicPrinter.class
0108: .getName());
0109:
0110: public static String quickPrintLocationDescriptors(
0111: SetOfLocationDescriptor locations, Services services) {
0112: LogicPrinter p = new LogicPrinter(null, NotationInfo
0113: .createInstance(), services);
0114: try {
0115: p.printLocationDescriptors(locations);
0116: } catch (IOException ioe) {
0117: return locations.toString();
0118: }
0119: return p.result().toString();
0120: }
0121:
0122: /**
0123: * Creates a LogicPrinter. Sets the sequent to be printed, as
0124: * well as a ProgramPrinter to print Java programs and a
0125: * NotationInfo which determines the concrete syntax.
0126: *
0127: * @param prgPrinter the ProgramPrinter that pretty-prints Java programs
0128: * @param notationInfo the NotationInfo for the concrete syntax
0129: * @param services The Services object
0130: */
0131: public LogicPrinter(ProgramPrinter prgPrinter,
0132: NotationInfo notationInfo, Services services) {
0133: backend = new PosTableStringBackend(lineWidth);
0134: layouter = new Layouter(backend, 2);
0135: this .prgPrinter = prgPrinter;
0136: this .notationInfo = notationInfo;
0137: this .services = services;
0138: }
0139:
0140: /**
0141: * Creates a LogicPrinter. Sets the sequent to be printed, as
0142: * well as a ProgramPrinter to print Java programs and a
0143: * NotationInfo which determines the concrete syntax.
0144: *
0145: * @param prgPrinter the ProgramPrinter that pretty-prints Java programs
0146: * @param notationInfo the NotationInfo for the concrete syntax
0147: * @param backend the Backend for the output
0148: * @param services the Services object
0149: */
0150:
0151: public LogicPrinter(ProgramPrinter prgPrinter,
0152: NotationInfo notationInfo, Backend backend,
0153: Services services) {
0154: this .backend = backend;
0155: layouter = new Layouter(backend, 2);
0156: this .prgPrinter = prgPrinter;
0157: this .notationInfo = notationInfo;
0158: this .services = services;
0159: }
0160:
0161: /**
0162: * Creates a LogicPrinter. Sets the sequent to be printed, as
0163: * well as a ProgramPrinter to print Java programs and a
0164: * NotationInfo which determines the concrete syntax.
0165: *
0166: * @param prgPrinter the ProgramPrinter that pretty-prints Java programs
0167: * @param notationInfo the NotationInfo for the concrete syntax
0168: * @param purePrint if true the PositionTable will not be calculated
0169: * (simulates the behaviour of the former PureSequentPrinter)
0170: * @param services the Services object
0171: */
0172: public LogicPrinter(ProgramPrinter prgPrinter,
0173: NotationInfo notationInfo, Services services,
0174: boolean purePrint) {
0175: backend = new PosTableStringBackend(lineWidth);
0176: layouter = new Layouter(backend, 2);
0177: this .prgPrinter = prgPrinter;
0178: this .notationInfo = notationInfo;
0179: this .services = services;
0180: pure = purePrint;
0181: }
0182:
0183: /**
0184: * Creates a LogicPrinter. Sets the sequent to be printed, as
0185: * well as a ProgramPrinter to print Java programs and a
0186: * NotationInfo which determines the concrete syntax.
0187: *
0188: * @param prgPrinter the ProgramPrinter that pretty-prints Java programs
0189: * @param notationInfo the NotationInfo for the concrete syntax
0190: * @param backend the Backend for the output
0191: * @param purePrint if true the PositionTable will not be calculated
0192: (simulates the behaviour of the former PureSequentPrinter)
0193: */
0194: public LogicPrinter(ProgramPrinter prgPrinter,
0195: NotationInfo notationInfo, Backend backend,
0196: Services services, boolean purePrint) {
0197: this .backend = backend;
0198: layouter = new Layouter(backend, 2);
0199: this .prgPrinter = prgPrinter;
0200: this .notationInfo = notationInfo;
0201: this .services = services;
0202: pure = purePrint;
0203: }
0204:
0205: /**
0206: * @return the notationInfo associated with this LogicPrinter
0207: */
0208: public NotationInfo getNotationInfo() {
0209: return notationInfo;
0210: }
0211:
0212: /**
0213: * Resets the Backend, the Layouter and (if applicable) the ProgramPrinter
0214: * of this Object.
0215: */
0216: public void reset() {
0217: backend = new PosTableStringBackend(lineWidth);
0218: layouter = new Layouter(backend, 2);
0219: if (prgPrinter != null) {
0220: prgPrinter.reset();
0221: }
0222: }
0223:
0224: /**
0225: * sets the line width to the new value but does <em>not</em>
0226: * reprint the sequent.
0227: * The actual set line width is the maximum of
0228: * {@link LogicPrinter#DEFAULT_LINE_WIDTH} and the given value
0229: * @param lineWidth the max. number of character to put on one line
0230: * @return the actual set line width
0231: */
0232: public int setLineWidth(int lineWidth) {
0233: this .lineWidth = lineWidth < DEFAULT_LINE_WIDTH ? DEFAULT_LINE_WIDTH
0234: : lineWidth;
0235: return this .lineWidth;
0236: }
0237:
0238: /** Reprints the sequent. This can be useful if settings like
0239: * PresentationFeatures or abbreviations have changed.
0240: * @param seq The Sequent to be reprinted
0241: * @param filter The SequentPrintFilter for seq
0242: * @param lineWidth the max. number of character to put on one line
0243: * (the actual taken linewidth is the max of
0244: * {@link LogicPrinter#DEFAULT_LINE_WIDTH} and the given value
0245: */
0246: public void update(Sequent seq, SequentPrintFilter filter,
0247: int lineWidth) {
0248: setLineWidth(lineWidth);
0249: reset();
0250: printSequent(seq, filter);
0251: }
0252:
0253: /**
0254: * sets instantiations of schema variables
0255: */
0256: public void setInstantiation(SVInstantiations instantiations) {
0257: this .instantiations = instantiations;
0258: }
0259:
0260: /**
0261: * Pretty-print a taclet. Line-breaks are taken care of.
0262: *
0263: * @param taclet
0264: * The Taclet to be pretty-printed.
0265: * @param sv
0266: * The instantiations of the SchemaVariables
0267: * @param showWholeTaclet
0268: * Should the find, varcond and heuristic part be pretty-printed?
0269: */
0270: public void printTaclet(Taclet taclet, SVInstantiations sv,
0271: boolean showWholeTaclet) {
0272: instantiations = sv;
0273: try {
0274: if (logger.isDebugEnabled()) {
0275: logger.debug(taclet.name().toString());
0276: }
0277: if (showWholeTaclet) {
0278: layouter.beginC(2).print(taclet.name().toString())
0279: .print(" {");
0280: } else {
0281: layouter.beginC();
0282: }
0283: if (!(taclet.ifSequent().isEmpty())) {
0284: printTextSequent(taclet.ifSequent(), "\\assumes", true);
0285: }
0286: if (showWholeTaclet) {
0287: printFind(taclet);
0288: if (taclet instanceof RewriteTaclet) {
0289: printRewriteAttributes((RewriteTaclet) taclet);
0290: }
0291: printVarCond(taclet);
0292: }
0293: printGoalTemplates(taclet);
0294: if (showWholeTaclet) {
0295: printHeuristics(taclet);
0296: }
0297: printAttribs(taclet);
0298: if (showWholeTaclet) {
0299: layouter.brk(1, -2).print("}");
0300: }
0301: layouter.end();
0302: } catch (java.io.IOException e) {
0303: logger.warn("xxx exception occurred during printTaclet");
0304: }
0305: instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS;
0306: }
0307:
0308: /**
0309: * Pretty-print a taclet. Line-breaks are taken care of. No instantiation is
0310: * applied.
0311: *
0312: * @param taclet
0313: * The Taclet to be pretty-printed.
0314: */
0315: public void printTaclet(Taclet taclet) {
0316: printTaclet(taclet, SVInstantiations.EMPTY_SVINSTANTIATIONS,
0317: true);
0318: }
0319:
0320: protected void printAttribs(Taclet taclet) throws IOException {
0321: if (taclet.noninteractive()) {
0322: layouter.brk().print("\\noninteractive");
0323: }
0324: }
0325:
0326: protected void printRewriteAttributes(RewriteTaclet taclet)
0327: throws IOException {
0328: final int stateRestriction = taclet.getStateRestriction();
0329: if (stateRestriction == RewriteTaclet.SAME_UPDATE_LEVEL) {
0330: layouter.brk().print("\\sameUpdateLevel");
0331: } else if (stateRestriction == RewriteTaclet.IN_SEQUENT_STATE) {
0332: layouter.brk().print("\\inSequentState");
0333: }
0334: }
0335:
0336: protected void printVarCond(Taclet taclet) throws IOException {
0337: IteratorOfNewVarcond itVarsNew = taclet.varsNew().iterator();
0338: IteratorOfNewDependingOn itVarsNewDepOn = taclet
0339: .varsNewDependingOn();
0340: IteratorOfNotFreeIn itVarsNotFreeIn = taclet.varsNotFreeIn();
0341: IteratorOfVariableCondition itVC = taclet
0342: .getVariableConditions();
0343:
0344: if (itVarsNew.hasNext() || itVarsNotFreeIn.hasNext()
0345: || itVC.hasNext() || itVarsNewDepOn.hasNext()) {
0346: layouter.brk().beginC(2).print("\\varcond (").brk();
0347: while (itVarsNewDepOn.hasNext()) {
0348: printNewVarDepOnCond(itVarsNewDepOn.next());
0349: if (itVarsNewDepOn.hasNext() || itVarsNew.hasNext()
0350: || itVarsNotFreeIn.hasNext() || itVC.hasNext()) {
0351: layouter.print(",").brk();
0352: }
0353: }
0354: while (itVarsNew.hasNext()) {
0355: printNewVarcond(itVarsNew.next());
0356: if (itVarsNew.hasNext() || itVarsNotFreeIn.hasNext()
0357: || itVC.hasNext()) {
0358: layouter.print(",").brk();
0359: }
0360: }
0361: while (itVarsNotFreeIn.hasNext()) {
0362: NotFreeIn pair = itVarsNotFreeIn.next();
0363: printNotFreeIn(pair);
0364: if (itVarsNotFreeIn.hasNext() || itVC.hasNext()) {
0365: layouter.print(",").brk();
0366: }
0367: }
0368: while (itVC.hasNext()) {
0369: printVariableCondition(itVC.next());
0370: if (itVC.hasNext()) {
0371: layouter.print(",").brk();
0372: }
0373: }
0374: layouter.brk(1, -2).print(")").end();
0375: }
0376: }
0377:
0378: private void printNewVarDepOnCond(NewDependingOn on)
0379: throws IOException {
0380: layouter.beginC(0);
0381: layouter.brk().print("\\new( ");
0382: printSchemaVariable(on.first());
0383: layouter.print(",").brk();
0384: layouter.print("\\dependingOn(");
0385: printSchemaVariable(on.second());
0386: layouter.brk(0, -2).print(")").brk();
0387: layouter.brk(0, -2).print(")").end();
0388: }
0389:
0390: protected void printNewVarcond(NewVarcond sv) throws IOException {
0391: layouter.beginC(0);
0392: layouter.brk().print("\\new(");
0393: printSchemaVariable(sv.getSchemaVariable());
0394: layouter.print(",").brk();
0395: if (sv.isDefinedByType()) {
0396: layouter.print(sv.getSort().toString());
0397: } else {
0398: if (sv.isDefinedByElementSort()) {
0399: layouter.print("\\elemTypeof (").brk();
0400: } else {
0401: layouter.print("\\typeof (").brk();
0402: }
0403: printSchemaVariable(sv.getPeerSchemaVariable());
0404: layouter.brk(0, -2).print(")").brk();
0405: }
0406: layouter.brk(0, -2).print(")").end();
0407: }
0408:
0409: protected void printNotFreeIn(NotFreeIn sv) throws IOException {
0410: layouter.beginI(0);
0411: layouter.brk().print("\\notFreeIn(").brk();
0412: printSchemaVariable(sv.first());
0413: layouter.print(",").brk();
0414: printSchemaVariable(sv.second());
0415: layouter.brk(0, -2).print(")").end();
0416: }
0417:
0418: protected void printVariableCondition(VariableCondition sv)
0419: throws IOException {
0420: layouter.print(sv.toString());
0421: }
0422:
0423: protected void printHeuristics(Taclet taclet) throws IOException {
0424: if (taclet.getRuleSets().size() == 0) {
0425: return;
0426: }
0427: layouter.brk().beginC(2).print("\\heuristics (");
0428: for (IteratorOfRuleSet it = taclet.getRuleSets().iterator(); it
0429: .hasNext();) {
0430: layouter.brk();
0431: RuleSet tgt = it.next();
0432: printHeuristic(tgt);
0433: if (it.hasNext()) {
0434: layouter.print(",");
0435: }
0436: }
0437: layouter.brk(1, -2).print(")").end();
0438: }
0439:
0440: protected void printHeuristic(RuleSet sv) throws IOException {
0441: layouter.print(sv.name().toString());
0442: }
0443:
0444: protected void printFind(Taclet taclet) throws IOException {
0445: if (!(taclet instanceof FindTaclet)) {
0446: return;
0447: }
0448: layouter.brk().beginC(2).print("\\find (").brk();
0449: if (taclet instanceof SuccTaclet) {
0450: layouter.print("==>").brk();
0451: }
0452: printTerm(((FindTaclet) taclet).find());
0453: if (taclet instanceof AntecTaclet) {
0454: layouter.brk().print("==>");
0455: }
0456: layouter.brk(1, -2).print(")").end();
0457: }
0458:
0459: protected void printTextSequent(Sequent seq, String text,
0460: boolean frontbreak) throws IOException {
0461:
0462: if (frontbreak) {
0463: layouter.brk();
0464: }
0465:
0466: layouter.beginC(2).print(text).print(" (");
0467: printSequent(seq, null, false);
0468: layouter.brk(1, -2).print(")").end();
0469: }
0470:
0471: protected void printGoalTemplates(Taclet taclet) throws IOException {
0472: //layouter.beginC(0);
0473: if (taclet.closeGoal()) {
0474: layouter.brk().print("\\closegoal").brk();
0475: }
0476:
0477: for (final IteratorOfTacletGoalTemplate it = taclet
0478: .goalTemplates().reverse().iterator(); it.hasNext();) {
0479: printGoalTemplate(it.next());
0480: if (it.hasNext()) {
0481: layouter.print(";");
0482: }
0483: }
0484: //layouter.end();
0485: }
0486:
0487: protected void printGoalTemplate(TacletGoalTemplate tgt)
0488: throws IOException {
0489: //layouter.beginC(0);
0490: if (tgt.name() != null) {
0491: if (tgt.name().length() > 0) {
0492: layouter.brk().beginC(2).print(tgt.name()).print(" {");
0493: }
0494:
0495: }
0496: if (!(tgt.sequent().isEmpty())) {
0497: printTextSequent(tgt.sequent(), "\\add", true);
0498: }
0499: if (tgt.rules() != SLListOfTaclet.EMPTY_LIST) {
0500: printRules(tgt.rules());
0501: }
0502: if (tgt.addedProgVars().size() > 0) {
0503: layouter.brk();
0504: printAddProgVars(tgt.addedProgVars());
0505: }
0506:
0507: if (tgt instanceof AntecSuccTacletGoalTemplate) {
0508: printTextSequent(((AntecSuccTacletGoalTemplate) tgt)
0509: .replaceWith(), "\\replacewith", true);
0510: }
0511: if (tgt instanceof RewriteTacletGoalTemplate) {
0512: layouter.brk();
0513: printRewrite(((RewriteTacletGoalTemplate) tgt)
0514: .replaceWith());
0515: }
0516: if (tgt.name() != null) {
0517: if (tgt.name().length() > 0) {
0518: layouter.brk(1, -2).print("}").end();
0519: }
0520: }
0521: //layouter.end();
0522: }
0523:
0524: protected void printRules(ListOfTaclet rules) throws IOException {
0525: layouter.brk().beginC(2).print("\\addrules (");
0526: SVInstantiations svi = instantiations;
0527: for (IteratorOfTaclet it = rules.iterator(); it.hasNext();) {
0528: layouter.brk();
0529: Taclet t = it.next();
0530: printTaclet(t, instantiations, true);
0531: instantiations = svi;
0532: }
0533: layouter.brk(1, -2).print(")").end();
0534: }
0535:
0536: protected void printAddProgVars(SetOfSchemaVariable apv)
0537: throws IOException {
0538: layouter.beginC(2).print("\\addprogvars (");
0539: for (IteratorOfSchemaVariable it = apv.iterator(); it.hasNext();) {
0540: layouter.brk();
0541: SchemaVariable tgt = it.next();
0542: printSchemaVariable(tgt);
0543: if (it.hasNext()) {
0544: layouter.print(",");
0545: }
0546: }
0547: layouter.brk(1, -2).print(")").end();
0548: }
0549:
0550: protected void printSchemaVariable(SchemaVariable sv)
0551: throws IOException {
0552: Object o = getInstantiations().getInstantiation(sv);
0553: if (o == null) {
0554: if (sv.isProgramSV()) {
0555: Debug.assertTrue(sv instanceof SortedSchemaVariable);
0556: printProgramSV((ProgramSV) sv);
0557: } else {
0558: printConstant(sv.name().toString());
0559: }
0560: } else {
0561: if (o instanceof Term) {
0562: printTerm((Term) o);
0563: } else if (o instanceof ProgramElement) {
0564: printProgramElement((ProgramElement) o);
0565: } else {
0566: logger.warn("Unknown instantiation type of " + o
0567: + "; class is " + o.getClass().getName());
0568: printConstant(sv.name().toString());
0569: }
0570: }
0571: }
0572:
0573: /**
0574: * Pretty-prints a ProgramElement.
0575: *
0576: * @param pe
0577: * You've guessed it, the ProgramElement to be pretty-printed
0578: * @throws IOException
0579: */
0580: public void printProgramElement(ProgramElement pe)
0581: throws IOException {
0582: if (pe instanceof ProgramVariable) {
0583: printProgramVariable((ProgramVariable) pe);
0584: } else {
0585: StringWriter w = new StringWriter();
0586: PrettyPrinter pp = new PrettyPrinter(w, true,
0587: instantiations);
0588: pe.prettyPrint(pp);
0589: layouter.pre(w.toString());
0590: }
0591: }
0592:
0593: /**
0594: * Pretty-Prints a ProgramVariable in the logic, not in Java blocks. Prints
0595: * out the full (logic) name, so if A.b is private, it becomes a.A::b .
0596: *
0597: * @param pv
0598: * The ProgramVariable in the logic
0599: * @throws IOException
0600: */
0601: public void printProgramVariable(ProgramVariable pv)
0602: throws IOException {
0603: if (logger.isDebugEnabled()) {
0604: logger.debug("PP PV " + pv.name());
0605: }
0606: layouter.beginC().print(pv.name().toString()).end();
0607: }
0608:
0609: /**
0610: * Pretty-prints a ProgramSV.
0611: *
0612: * @param pe
0613: * You've guessed it, the ProgramSV to be pretty-printed
0614: * @throws IOException
0615: */
0616: public void printProgramSV(ProgramSV pe) throws IOException {
0617: StringWriter w = new StringWriter();
0618: PrettyPrinter pp = new PrettyPrinter(w, true, instantiations);
0619: pe.prettyPrint(pp);
0620: layouter.pre(w.toString());
0621: }
0622:
0623: protected void printRewrite(Term t) throws IOException {
0624: layouter.beginC(2).print("\\replacewith (").brk();
0625: printTerm(t);
0626: layouter.brk(1, -2).print(")").end();
0627: }
0628:
0629: /**
0630: * Pretty-print a sequent.
0631: * The sequent arrow is rendered as <code>==></code>. If the
0632: * sequent doesn't fit in one line, a line break is inserted after each
0633: * formula, the sequent arrow is on a line of its own, and formulae
0634: * are indented w.r.t. the arrow.
0635: * @param seq The Sequent to be pretty-printed
0636: * @param filter The SequentPrintFilter for seq
0637: * @param finalbreak Print an additional line-break at the end of the sequent.
0638: */
0639: public void printSequent(Sequent seq, SequentPrintFilter filter,
0640: boolean finalbreak) {
0641: if (seq != null) {
0642: printSequent(seq, finalbreak);
0643: } else if (filter != null) {
0644: printSequent(filter, finalbreak);
0645: }
0646: }
0647:
0648: public void printSequent(SequentPrintFilter filter,
0649: boolean finalbreak) {
0650: try {
0651: ListOfSequentPrintFilterEntry antec = filter.getAntec();
0652: ListOfSequentPrintFilterEntry succ = filter.getSucc();
0653: markStartSub();
0654: startTerm(antec.size() + succ.size());
0655: layouter.beginC(1).ind();
0656: printSemisequent(antec);
0657: layouter.brk(1, -1).print("==>").brk(1);
0658: printSemisequent(succ);
0659: if (finalbreak) {
0660: layouter.brk(0);
0661: }
0662: markEndSub();
0663: layouter.end();
0664: } catch (IOException e) {
0665: throw new RuntimeException(
0666: "IO Exception in pretty printer:\n" + e);
0667: } catch (UnbalancedBlocksException e) {
0668: throw new RuntimeException(
0669: "Unbalanced blocks in pretty printer:\n" + e);
0670: }
0671: }
0672:
0673: public void printSequent(Sequent seq, boolean finalbreak) {
0674: try {
0675: Semisequent antec = seq.antecedent();
0676: Semisequent succ = seq.succedent();
0677: markStartSub();
0678: startTerm(antec.size() + succ.size());
0679: layouter.beginC(1).ind();
0680: printSemisequent(antec);
0681: layouter.brk(1, -1).print("==>").brk(1);
0682: printSemisequent(succ);
0683: if (finalbreak) {
0684: layouter.brk(0);
0685: }
0686: markEndSub();
0687: layouter.end();
0688: } catch (IOException e) {
0689: throw new RuntimeException(
0690: "IO Exception in pretty printer:\n" + e);
0691: } catch (UnbalancedBlocksException e) {
0692: throw new RuntimeException(
0693: "Unbalanced blocks in pretty printer:\n" + e);
0694: }
0695: }
0696:
0697: /**
0698: * Pretty-print a sequent.
0699: * The sequent arrow is rendered as <code>=></code>. If the
0700: * sequent doesn't fit in one line, a line break is inserted after each
0701: * formula, the sequent arrow is on a line of its own, and formulae
0702: * are indented w.r.t. the arrow.
0703: * A line-break is printed after the Sequent.
0704: * @param seq The Sequent to be pretty-printed
0705: * @param filter The SequentPrintFilter for seq
0706: */
0707: public void printSequent(Sequent seq, SequentPrintFilter filter) {
0708: printSequent(seq, filter, true);
0709: }
0710:
0711: /**
0712: * Pretty-print a sequent.
0713: * The sequent arrow is rendered as <code>=></code>. If the
0714: * sequent doesn't fit in one line, a line break is inserted after each
0715: * formula, the sequent arrow is on a line of its own, and formulae
0716: * are indented w.r.t. the arrow.
0717: * A line-break is printed after the Sequent.
0718: * No filtering is done.
0719: * @param seq The Sequent to be pretty-printed
0720: */
0721: public void printSequent(Sequent seq) {
0722: printSequent(seq, true);
0723: }
0724:
0725: /**
0726: * Pretty-prints a Semisequent. Formulae are separated by commas.
0727: *
0728: * @param semiseq the semisequent to be printed
0729: */
0730: public void printSemisequent(Semisequent semiseq)
0731: throws IOException {
0732: for (int i = 0; i < semiseq.size(); i++) {
0733: markStartSub();
0734: printConstrainedFormula(semiseq.get(i));
0735: markEndSub();
0736: if (i != semiseq.size() - 1) {
0737: layouter.print(",").brk(1);
0738: }
0739: }
0740: }
0741:
0742: public void printSemisequent(
0743: ListOfSequentPrintFilterEntry p_formulas)
0744: throws IOException {
0745: IteratorOfSequentPrintFilterEntry it = p_formulas.iterator();
0746: SequentPrintFilterEntry entry;
0747: int size = p_formulas.size();
0748: while (size-- != 0) {
0749: entry = it.next();
0750: markStartSub();
0751: formulaConstraint = entry.getDisplayConstraint();
0752: printConstrainedFormula(entry.getFilteredFormula());
0753: markEndSub();
0754: if (size != 0) {
0755: layouter.print(",").brk(1);
0756: }
0757: }
0758: formulaConstraint = null;
0759: }
0760:
0761: /**
0762: * Pretty-prints a constrained formula. The constraint
0763: * "Constraint.BOTTOM" is suppressed
0764: *
0765: * @param cfma the constrained formula to be printed
0766: */
0767: public void printConstrainedFormula(ConstrainedFormula cfma)
0768: throws IOException {
0769: if (cfma.constraint().isBottom()) {
0770: printTerm(cfma.formula());
0771: } else {
0772: layouter.beginC(0);
0773: layouter.ind();
0774: printTerm(cfma.formula());
0775: layouter.brk(1, 3).print("<<").ind(1, 6);
0776: printConstraint(cfma.constraint());
0777: layouter.end();
0778: }
0779: }
0780:
0781: /**
0782: * Pretty-prints a (shadowed) array expression
0783: *
0784: * @param arraySep usually a <code>[ </code> and a <code>] </code>
0785: * @param t the array expression as a whole
0786: * @param ass the associatives for the subterms
0787: */
0788: public void printArray(String[] arraySep, Term t, int[] ass)
0789: throws java.io.IOException {
0790: startTerm(t.arity());
0791: for (int i = 0; i < 2; i++) {
0792: maybeParens(t.sub(i), ass[i]);
0793: layouter.print(arraySep[i]);
0794: final Sort arraySortOfOperator = ((ArrayOp) t.op())
0795: .arraySort();
0796: if (i == 1 && t.sub(0).sort() != arraySortOfOperator) {
0797: layouter.print("@(");
0798: layouter.print(arraySortOfOperator.name().toString());
0799: layouter.print(")");
0800: }
0801: }
0802: if (t.op() instanceof ShadowedOperator) {
0803: printTransactionNumber(t.sub(2));
0804: }
0805: }
0806:
0807: /**
0808: * Pretty-prints a location descriptor.
0809: */
0810: public void printLocationDescriptor(LocationDescriptor loc)
0811: throws java.io.IOException {
0812:
0813: if (loc instanceof BasicLocationDescriptor) {
0814: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
0815: SetOfQuantifiableVariable boundVars = bloc.getLocTerm()
0816: .freeVars();
0817:
0818: if (boundVars.size() > 0) {
0819: layouter.print("\\for ").beginC();
0820: printVariables(new ArrayOfQuantifiableVariable(
0821: boundVars.toArray()));
0822: layouter.end();
0823: }
0824:
0825: if (bloc.getFormula().op() != Op.TRUE) {
0826: layouter.print("\\if (").beginC();
0827: printTerm(bloc.getFormula());
0828: layouter.print(") ").end();
0829: }
0830:
0831: printTerm(bloc.getLocTerm());
0832:
0833: } else {
0834: Debug
0835: .assertTrue(loc instanceof EverythingLocationDescriptor);
0836: layouter.print("*");
0837: }
0838: }
0839:
0840: /**
0841: * Pretty-prints a set of location descriptors.
0842: */
0843: public void printLocationDescriptors(
0844: SetOfLocationDescriptor locations)
0845: throws java.io.IOException {
0846: layouter.print("{").beginC();
0847: IteratorOfLocationDescriptor it = locations.iterator();
0848: while (it.hasNext()) {
0849: printLocationDescriptor(it.next());
0850: if (it.hasNext()) {
0851: layouter.print(", ").brk();
0852: }
0853: }
0854: layouter.print("}").end();
0855: }
0856:
0857: /**
0858: * Pretty-print a constraint
0859: *
0860: * This does currently only work well for "EqualityConstraint"s,
0861: * which are printed as a list of unifications. The bottom
0862: * constraint doesn't get special handling in here, i.e. this
0863: * method should not be called for p == Constraint.BOTTOM
0864: */
0865: public void printConstraint(Constraint p) throws IOException {
0866: createPositionTable = false;
0867: if (p instanceof EqualityConstraint) {
0868:
0869: // Within the constraint metavariables should not be
0870: // instantiated
0871: Constraint frmC = formulaConstraint;
0872: formulaConstraint = null;
0873:
0874: EqualityConstraint eqc = (EqualityConstraint) p;
0875: List vars = new ArrayList();
0876: {
0877: IteratorOfMetavariable it = eqc
0878: .restrictedMetavariables();
0879:
0880: while (it.hasNext())
0881: vars.add(it.next());
0882: }
0883:
0884: startTerm(vars.size());
0885: layouter.print("[ ").beginI(0);
0886:
0887: ListIterator it = vars.listIterator();
0888: Metavariable mv;
0889: Term inst;
0890: while (it.hasNext()) {
0891: mv = (Metavariable) it.next();
0892: inst = eqc.getDirectInstantiation(mv);
0893: if (inst == null)
0894: inst = TermFactory.DEFAULT.createFunctionTerm(mv);
0895:
0896: markStartSub();
0897: printInfixTerm(TermFactory.DEFAULT
0898: .createFunctionTerm(mv), 15, "=", inst, 10);
0899: markEndSub();
0900:
0901: if (it.hasNext()) {
0902: layouter.print(",").brk(1, 0);
0903: }
0904: }
0905: layouter.print(" ]").end();
0906:
0907: formulaConstraint = frmC;
0908:
0909: } else {
0910: // Don't know how to pretty-print this constraint class
0911: layouter.print(p.toString());
0912: }
0913: createPositionTable = true;
0914: }
0915:
0916: /**
0917: * Pretty-prints a term or formula. How it is rendered depends on
0918: * the NotationInfo given to the constructor.
0919: *
0920: * @param t the Term to be printed
0921: */
0922: public void printTerm(Term t) throws IOException {
0923: if (notationInfo.getAbbrevMap().isEnabled(t)) {
0924: startTerm(0);
0925: layouter.print(notationInfo.getAbbrevMap().getAbbrev(t));
0926: } else {
0927: notationInfo.getNotation(t.op(), services).print(t, this );
0928: }
0929: }
0930:
0931: /**
0932: * Pretty-prints a list of terms.
0933: * @param terms the terms to be printed
0934: */
0935: public void printTerm(ListOfTerm terms) throws IOException {
0936: getLayouter().print("{");
0937: IteratorOfTerm it = terms.iterator();
0938: while (it.hasNext()) {
0939: printTerm(it.next());
0940: if (it.hasNext())
0941: getLayouter().print(", ");
0942: }
0943: getLayouter().print("}");
0944: }
0945:
0946: /**
0947: * Pretty-prints a term or formula in the same block. How it is
0948: * rendered depends on the NotationInfo given to the constructor.
0949: * `In the same block' means that no extra indentation will be
0950: * added if line breaks are necessary. A formula <code>a & (b
0951: * & c)</code> would print <code>a & b & c</code>, omitting
0952: * the redundant parentheses. The subformula <code>b & c</code>
0953: * is printed using this method to get a layout of
0954: *
0955: * <pre>
0956: * a
0957: * & b
0958: * & c
0959: * </pre>
0960: * instead of
0961: * <pre>
0962: * a
0963: * & b
0964: * & c
0965: * </pre>
0966: *
0967: *
0968: * @param t the Term to be printed */
0969: public void printTermContinuingBlock(Term t) throws IOException {
0970: notationInfo.getNotation(t.op(), services)
0971: .printContinuingBlock(t, this );
0972: }
0973:
0974: /** Print a term in <code>f(t1,...tn)</code> style. If the
0975: * operator has arity 0, no parentheses are printed, i.e.
0976: * <code>f</code> instead of <code>f()</code>. If the term
0977: * doesn't fit on one line, <code>t2...tn</code> are aligned below
0978: * <code>t1</code>.
0979: *
0980: * @param name the name to be printed before the parentheses.
0981: * @param t the term to be printed. */
0982: public void printFunctionTerm(String name, Term t)
0983: throws IOException {
0984: //For OCL simplification
0985: if (oclPrettyPrinting && PresentationFeatures.ENABLED
0986: && t.arity() > 0) {
0987: printOCLUMLPropertyTerm(name, t);
0988: }
0989: //
0990: else {
0991: startTerm(t.arity());
0992: layouter.print(name);
0993: if (t.arity() > 0 || t.op() instanceof ProgramMethod) {
0994: layouter.print("(").beginC(0);
0995: for (int i = 0; i < t.arity(); i++) {
0996: markStartSub();
0997: printTerm(t.sub(i));
0998: markEndSub();
0999:
1000: if (i < t.arity() - 1) {
1001: layouter.print(",").brk(1, 0);
1002: }
1003: }
1004: layouter.print(")").end();
1005: }
1006: }
1007: }
1008:
1009: public void printCast(String pre, String post, Term t, int ass)
1010: throws IOException {
1011: final CastFunctionSymbol cast = (CastFunctionSymbol) t.op();
1012: startTerm(t.arity());
1013: layouter.print(pre);
1014: layouter.print(cast.getSortDependingOn().toString());
1015: layouter.print(post);
1016: maybeParens(t.sub(0), ass);
1017: }
1018:
1019: /** Print a term in <code>f(t1,...tn)</code> style. If it doesn't
1020: * fit on one line, <code>t2...tn</code> are aligned below t1.
1021: * Print a term in <code>o.q(t1,...tn)</code> style.
1022: *
1023: * @param name the name of the query
1024: * @param t the Term to be printed
1025: * @param ass the int defining the associativity of
1026: * the term
1027: */
1028: public void printQueryTerm(String name, Term t, int ass)
1029: throws IOException {
1030: int start = 0;
1031: if ((t.op() instanceof ProgramMethod)
1032: && (((ProgramMethod) t.op()).isStatic() || ((ProgramMethod) t
1033: .op()).isConstructor())) {
1034: startTerm(t.arity());
1035: layouter.print(((ProgramMethod) t.op()).getContainerType()
1036: .getName());
1037: } else {
1038: start = 1;
1039: startTerm(t.arity());
1040: maybeParens(t.sub(0), ass);
1041: }
1042: layouter.print(".").print(name).print("(").beginC(0);
1043: for (int i = start; i < t.arity(); i++) {
1044: markStartSub();
1045: printTerm(t.sub(i));
1046: markEndSub();
1047: if (i < t.arity() - 1) {
1048: layouter.print(",").brk(1, 0);
1049: }
1050: }
1051: layouter.print(")").end();
1052: }
1053:
1054: /** Print a unary term in prefix style. For instance
1055: * <code>!a</code>. No line breaks are possible.
1056: *
1057: * @param name the prefix operator
1058: * @param t the subterm to be printed
1059: * @param ass the associativity for the subterm
1060: */
1061: public void printPrefixTerm(String name, Term t, int ass)
1062: throws IOException {
1063: startTerm(1);
1064: layouter.print(name);
1065: maybeParens(t, ass);
1066: }
1067:
1068: /** Print a unary term in postfix style. For instance
1069: * <code>t.a</code>, where <code>.a</code> is the postfix operator.
1070: * No line breaks are possible.
1071: *
1072: * @param name the postfix operator
1073: * @param t the subterm to be printed
1074: * @param ass the associativity for the subterm
1075: */
1076: public void printPostfixTerm(Term t, int ass, String name)
1077: throws IOException {
1078: startTerm(1);
1079: maybeParens(t, ass);
1080: layouter.print(name);
1081: }
1082:
1083: /**
1084: * Pretty-prints a shadowed attribute
1085: * @param t1 the attribute prefix
1086: * @param ass1 the associativity for the reference prefix
1087: * @param name the attribute name
1088: * @param t2 the shadow number term
1089: */
1090: public void printShadowedAttribute(Term t1, int ass1, String name,
1091: Term t2) throws java.io.IOException {
1092: startTerm(2);
1093: maybeParens(t1, ass1);
1094: layouter.print(name);
1095: printTransactionNumber(t2);
1096: }
1097:
1098: /** Print a binary term in infix style. For instance <code>p
1099: * & q</code>, where <code>&</code> is the infix
1100: * operator. If line breaks are necessary, the format is like
1101: *
1102: * <pre>
1103: * p
1104: * & q
1105: * </pre>
1106: *
1107: * The subterms are printed using
1108: * {@link #printTermContinuingBlock(Term)}.
1109: *
1110: * @param l the left subterm
1111: * @param assLeft associativity for left subterm
1112: * @param name the infix operator
1113: * @param r the right subterm
1114: * @param assRight associativity for right subterm
1115: */
1116: public void printInfixTerm(Term l, int assLeft, String name,
1117: Term r, int assRight) throws IOException {
1118: int indent = name.length() + 1;
1119: layouter.beginC(indent);
1120: printInfixTermContinuingBlock(l, assLeft, name, r, assRight);
1121: layouter.end();
1122: }
1123:
1124: /** Print a binary term in infix style, continuing a containing
1125: * block. See {@link #printTermContinuingBlock(Term)} for the
1126: * idea. Otherwise like
1127: * {@link #printInfixTerm(Term,int,String,Term,int)}.
1128: *
1129: * @param l the left subterm
1130: * @param assLeft associativity for left subterm
1131: * @param name the infix operator
1132: * @param r the right subterm
1133: * @param assRight associativity for right subterm
1134: * */
1135: public void printInfixTermContinuingBlock(Term l, int assLeft,
1136: String name, Term r, int assRight) throws IOException {
1137: int indent = name.length() + 1;
1138: startTerm(2);
1139: layouter.ind();
1140: maybeParens(l, assLeft);
1141: layouter.brk(1, -indent).print(name).ind(1, 0);
1142: maybeParens(r, assRight);
1143: }
1144:
1145: /**
1146: * prints an anonymous update
1147: */
1148: public void printAnonymousUpdate(Term t, int ass)
1149: throws IOException {
1150: mark(MARK_START_UPDATE);
1151: layouter.beginC(2).print("{");
1152: startTerm(1);
1153: layouter.print(t.op().name().toString());
1154: layouter.print("}");
1155: mark(MARK_END_UPDATE);
1156: layouter.brk(1);
1157: maybeParens(t.sub(t.arity() - 1), ass);
1158: layouter.end();
1159: }
1160:
1161: /**
1162: * Print a term with an (quantified) update. This looks like
1163: * <code>{loc1 := val1 || ... || locn := valn} t</code>. If line breaks are necessary, the
1164: * format is
1165: *
1166: * <pre>
1167: * {loc1:=val1 || ... || locn:=valn}
1168: * t
1169: * </pre>
1170: *
1171: * @param l the left brace
1172: * @param asgn the assignment operator (including spaces)
1173: * @param r the right brace
1174: * @param t the update term
1175: * @param ass1 associativity for the locations
1176: * @param ass2 associativity for the new values
1177: * @param ass3 associativity for phi
1178: */
1179:
1180: public void printQuanUpdateTerm(String l, String asgn, String r,
1181: Term t, int ass1, int ass2, int ass3) throws IOException {
1182: final QuanUpdateOperator op = (QuanUpdateOperator) t.op();
1183: mark(MARK_START_UPDATE);
1184: layouter.beginC(2).print(l);
1185: startTerm(t.arity());
1186: for (int i = 0; i < op.locationCount(); i++) {
1187: final Operator loc = op.location(i);
1188:
1189: layouter.beginC(0);
1190: printUpdateQuantification(t, op, i);
1191:
1192: final String[] separator = setupUpdateSeparators(loc, op
1193: .location(t, i));
1194: for (int j = loc.arity(); j >= 1; j--) {
1195: final Term sub = t.sub(op.valuePos(i) - j);
1196:
1197: if (loc instanceof ShadowedOperator && j == 1) {
1198: printTransactionNumber(sub);
1199: } else {
1200: markStartSub();
1201: printTerm(sub);
1202: markEndSub();
1203: layouter.print(separator[loc.arity() - j]);
1204: }
1205: }
1206: layouter.print(asgn).brk(0, 0);
1207: layouter.end();
1208: maybeParens(op.value(t, i), ass2);
1209: if (i < op.locationCount() - 1) {
1210: layouter.print(" ||").brk(1, 0);
1211: }
1212: }
1213:
1214: layouter.print(r);
1215: mark(MARK_END_UPDATE);
1216: layouter.brk(0);
1217: maybeParens(t.sub(t.arity() - 1), ass3);
1218: layouter.end();
1219: }
1220:
1221: /**
1222: * @param sub
1223: * @throws IOException
1224: */
1225: private void printTransactionNumber(final Term sub)
1226: throws IOException {
1227: final int primes = asPrimes(sub);
1228: if (primes == -1) {
1229: layouter.print("^(");
1230: markStartSub();
1231: printTerm(sub);
1232: markEndSub();
1233: layouter.print(")");
1234: } else {
1235: final StringBuffer s_primes = new StringBuffer();
1236: for (int p = 0; p < primes; p++) {
1237: s_primes.append("\'");
1238: }
1239: markStartSub();
1240: markEndSub();
1241: layouter.print(s_primes.toString());
1242:
1243: }
1244: }
1245:
1246: private void printUpdateQuantification(Term t,
1247: QuanUpdateOperator op, int locationNum) throws IOException {
1248: final ArrayOfQuantifiableVariable boundVars = t
1249: .varsBoundHere(op.valuePos(locationNum));
1250: if (boundVars.size() > 0) {
1251: layouter.print("\\for ");
1252: printVariables(boundVars);
1253: }
1254:
1255: if (op.guardExists(locationNum)) {
1256: layouter.print("\\if (").beginC(0);
1257: markStartSub();
1258: printTerm(t.sub(op.guardPos(locationNum)));
1259: markEndSub();
1260: layouter.print(") ").end();
1261: }
1262: }
1263:
1264: private void printVariables(ArrayOfQuantifiableVariable vars)
1265: throws IOException {
1266: int size = vars.size();
1267: if (size != 1)
1268: layouter.print("(");
1269: for (int j = 0; j != vars.size();) {
1270: final QuantifiableVariable v = vars
1271: .getQuantifiableVariable(j);
1272: if (v instanceof LogicVariable) {
1273: Term t = TermFactory.DEFAULT
1274: .createVariableTerm((LogicVariable) v);
1275: if (notationInfo.getAbbrevMap().containsTerm(t)) {
1276: layouter.print(v.sort().name().toString() + " "
1277: + notationInfo.getAbbrevMap().getAbbrev(t));
1278: } else {
1279: layouter.print(v.sort().name() + " " + v.name());
1280: }
1281: } else {
1282: layouter.print(v.name().toString());
1283: }
1284: ++j;
1285: if (j != vars.size())
1286: layouter.print("; ");
1287: }
1288: if (size != 1)
1289: layouter.print(") ");
1290: else
1291: layouter.print("; ");
1292: }
1293:
1294: private int asPrimes(Term shadowNum) {
1295: int result = 0;
1296: Term t = shadowNum;
1297: if (services == null
1298: || t.op() != services.getTypeConverter()
1299: .getIntegerLDT().getNumberSymbol()) {
1300: return -1;
1301: }
1302:
1303: final String numberString = Notation.NumLiteral
1304: .printNumberTerm(t);
1305: if (numberString == null) {
1306: result = -1;
1307: } else {
1308: try {
1309: result = Integer.parseInt(numberString);
1310: } catch (NumberFormatException nfe) {
1311: result = -1;
1312: }
1313: }
1314: return result > 0 ? result : -1;
1315:
1316: }
1317:
1318: String[] setupUpdateSeparators(final Operator loc, final Term t)
1319: throws IOException {
1320: String[] separator = new String[loc.arity()];
1321: if (loc instanceof AttributeOp) {
1322: separator[0] = Notation.Attribute.printName(
1323: ((AttributeOp) loc), t.sub(0), this );
1324: } else if (loc instanceof ArrayOp) {
1325: separator[0] = "[";
1326: separator[1] = "]";
1327: } else if (loc.arity() == 0) {
1328: layouter.print(loc.name().toString().replaceAll("::", "."));
1329: } else {
1330: layouter.print(loc.name().toString() + "(");
1331: for (int m = 0; m < loc.arity() - 1; m++) {
1332: separator[m] = ",";
1333: }
1334: separator[loc.arity() - 1] = ")";
1335: }
1336: return separator;
1337: }
1338:
1339: public void printIfThenElseTerm(Term t, String keyword)
1340: throws IOException {
1341: startTerm(t.arity());
1342:
1343: layouter.beginC(0);
1344:
1345: layouter.print(keyword);
1346:
1347: if (t.varsBoundHere(0).size() > 0) {
1348: layouter.print(" ");
1349: printVariables(t.varsBoundHere(0));
1350: }
1351: layouter.print(" (");
1352: markStartSub();
1353: printTerm(t.sub(0));
1354: markEndSub();
1355: layouter.print(")");
1356:
1357: for (int i = 1; i < t.arity(); ++i) {
1358: layouter.brk(1, 3);
1359: if (i == 1) {
1360: layouter.print(" \\then (");
1361: } else {
1362: layouter.print(" \\else (");
1363: }
1364: markStartSub();
1365: printTerm(t.sub(i));
1366: markEndSub();
1367: layouter.print(")");
1368: }
1369:
1370: layouter.end();
1371: }
1372:
1373: /** Print a substitution term. This looks like
1374: * <code>{var/t}s</code>. If line breaks are necessary, the
1375: * format is
1376: *
1377: * <pre>
1378: * {var/t}
1379: * s
1380: * </pre>
1381: *
1382: * @param l the String used as left brace symbol
1383: * @param v the {@link QuantifiableVariable} to be substituted
1384: * @param t the Term to be used as new value
1385: * @param ass2 the int defining the associativity for the new value
1386: * @param r the String used as right brace symbol
1387: * @param phi the substituted term/formula
1388: * @param ass3 the int defining the associativity for phi
1389: */
1390: public void printSubstTerm(String l, QuantifiableVariable v,
1391: Term t, int ass2, String r, Term phi, int ass3)
1392: throws IOException {
1393: layouter.beginC(2).print(l);
1394: printVariables(new ArrayOfQuantifiableVariable(v));
1395: startTerm(2);
1396: maybeParens(t, ass2);
1397: layouter.print(r).brk(0);
1398: maybeParens(phi, ass3);
1399: layouter.end();
1400: }
1401:
1402: /** Print a quantified term. Normally, this looks like
1403: * <code>all x:s.phi</code>. If line breaks are necessary,
1404: * the format is
1405: *
1406: * <pre>
1407: * all x:s.
1408: * phi
1409: * </pre>
1410: *
1411: * Note that the parameter <code>var</code> has to contain the
1412: * variable name with colon and sort.
1413: *
1414: * @param name the name of the quantifier
1415: * @param var the quantified variable (+colon and sort)
1416: * @param sep the separator (usually a dot)
1417: * @param phi the quantified formula
1418: * @param ass associativity for phi
1419: */
1420: public void printQuantifierTerm(String name,
1421: ArrayOfQuantifiableVariable vars, Term phi, int ass)
1422: throws IOException {
1423: layouter.beginC(2);
1424: layouter.print(name).print(" ");
1425: printVariables(vars);
1426: layouter.brk();
1427: startTerm(1);
1428: maybeParens(phi, ass);
1429: layouter.end();
1430: }
1431:
1432: /** Print a constant. This just prints the string <code>s</code> and
1433: * marks it as a nullary term.
1434: *
1435: * @param s the constant
1436: */
1437: public void printConstant(String s) throws IOException {
1438:
1439: startTerm(0);
1440: layouter.print(s);
1441: }
1442:
1443: /**
1444: * Prints a metavariable. If the {@link #formulaConstraint}
1445: * contains an instantiation for the metavariable the instantiation
1446: * is printed rather than the metavariable itself.
1447: *
1448: * @param p_mv the Metavariable to be printed
1449: *
1450: */
1451: public void printMetavariable(Metavariable p_mv) throws IOException {
1452: if (formulaConstraint != null) {
1453: Term t = formulaConstraint.getInstantiation(p_mv);
1454: if (t.op() != p_mv) {
1455: printTerm(t);
1456: return;
1457: }
1458: }
1459:
1460: printConstant(p_mv.name().toString());
1461: }
1462:
1463: /**
1464: * Print a Java block. This is formatted using the ProgramPrinter
1465: * given to the constructor. The result is indented according to
1466: * the surrounding material. The first `executable' statement is
1467: * marked for highlighting.
1468: *
1469: * @param j the Java block to be printed
1470: */
1471: public void printJavaBlock(JavaBlock j) throws IOException {
1472: java.io.StringWriter sw = new java.io.StringWriter();
1473: prgPrinter.reset();
1474: prgPrinter.setWriter(sw);
1475: Range r = null;
1476: try {
1477: j.program().prettyPrint(prgPrinter);
1478: r = prgPrinter.getRangeOfFirstExecutableStatement();
1479: } catch (java.io.IOException e) {
1480: layouter.print("ERROR");
1481: System.err.println("Error while printing Java program \n"
1482: + e);
1483: throw new RuntimeException(
1484: "Error while printing Java program \n" + e);
1485: }
1486: // send first executable statement range
1487: printMarkingFirstStatement(sw.toString(), r);
1488:
1489: }
1490:
1491: /** Print a string marking a range as first statement. The range
1492: * <code>r</code> indicates the `first statement' character range in
1493: * string <code>s</code>. This is sent to the layouter by decomposing
1494: * <code>s</code> into parts and using the appropriate
1495: * {@link de.uka.ilkd.key.util.pp.Layouter#mark(Object)} calls.
1496: * This solves the problem that the material in <code>s</code> might
1497: * be further indented.
1498: *
1499: * @param s the string containing a program
1500: * @param r the range of the first statement
1501: */
1502: private void printMarkingFirstStatement(String s, Range r)
1503: throws IOException {
1504:
1505: int iEnd = r.end() <= s.length() ? r.end() : s.length();
1506: int iStart = r.start() <= iEnd ? r.start() : iEnd;
1507: String start = s.substring(0, iStart);
1508: String firstStmt = s.substring(iStart, iEnd);
1509: String end = s.substring(iEnd);
1510: layouter.beginC(0);
1511: printVerbatim(start);
1512: mark(MARK_START_FIRST_STMT);
1513: printVerbatim(firstStmt);
1514: mark(MARK_END_FIRST_STMT);
1515: printVerbatim(end);
1516: layouter.end();
1517: }
1518:
1519: /** Print a string containing newlines to the layouter. This is like
1520: * {@link de.uka.ilkd.key.util.pp.Layouter#pre(String)}, but
1521: * no block is opened.
1522: */
1523: private void printVerbatim(String s) throws IOException {
1524: StringTokenizer st = new StringTokenizer(s, "\n", true);
1525: while (st.hasMoreTokens()) {
1526: String line = st.nextToken();
1527: if ("\n".equals(line)) {
1528: layouter.nl();
1529: } else {
1530: layouter.print(line);
1531: }
1532: }
1533: }
1534:
1535: /** Print a DL modality formula. <code>phi</code> is the whole
1536: * modality formula, not just the subformula inside the modality.
1537: * Normally, this looks like
1538: * <code><Program>psi</code>, where <code>psi = phi.sub(0)</code>.
1539: * No line breaks are inserted, as the program itself is always broken.
1540: * In case of a program modality with arity greater than 1,
1541: * the subformulae are listed between parens, like
1542: * <code><Program>(psi1,psi2)</code>
1543: */
1544:
1545: public void printModalityTerm(String left, JavaBlock jb,
1546: String right, Term phi, int ass) throws IOException {
1547: if (phi.op() instanceof ModalOperatorSV) {
1548: Object o = getInstantiations().getInstantiation(
1549: (ModalOperatorSV) phi.op());
1550: if (o == null) {
1551: logger.debug("PMT NO " + phi + " @[ " + phi.op()
1552: + " ]@ " + " is : " + phi.getClass().getName()
1553: + " @[" + phi.op().getClass().getName()
1554: + "]@ known");
1555: } else {
1556: //logger.debug("Instantiation of " + phi + " @[" + phi.op() + "]@" + " is : " + o + o.getClass().getName());
1557: //logger.debug(getInstantiations());
1558: logger.debug("PMT YES " + phi.op() + " -> " + o + " @["
1559: + o.getClass().getName() + "]@");
1560:
1561: if (notationInfo.getAbbrevMap().isEnabled(phi)) {
1562: startTerm(0);
1563: layouter.print(notationInfo.getAbbrevMap()
1564: .getAbbrev(phi));
1565: } else {
1566: Term[] ta = new Term[phi.arity()];
1567: for (int i = 0; i < phi.arity(); i++) {
1568: ta[i] = phi.sub(i);
1569: }
1570: ArrayOfQuantifiableVariable[] aa = new ArrayOfQuantifiableVariable[phi
1571: .arity()];
1572: for (int i = 0; i < phi.arity(); i++) {
1573: aa[i] = phi.varsBoundHere(i);
1574: }
1575: Term term = TermFactory.DEFAULT.createTerm(
1576: (Modality) o, ta, aa, phi.javaBlock());
1577: notationInfo.getNotation((Modality) o, services)
1578: .print(term, this );
1579: return;
1580: }
1581:
1582: }
1583: }
1584:
1585: mark(MARK_MODPOSTBL);
1586: startTerm(phi.arity());
1587: layouter.print(left);
1588: printJavaBlock(jb);
1589:
1590: layouter.print(right + " ");
1591: if (phi.arity() == 1) {
1592: maybeParens(phi.sub(0), ass);
1593: } else if (phi.arity() > 1) {
1594: layouter.print("(");
1595: for (int i = 0; i < phi.arity(); i++) {
1596: markStartSub();
1597: printTerm(phi.sub(i));
1598: markEndSub();
1599: if (i < phi.arity() - 1) {
1600: layouter.print(",").brk(1, 0);
1601: }
1602: }
1603: layouter.print(")");
1604: }
1605: }
1606:
1607: /**
1608: * Used for OCL Simplification.
1609: */
1610: public void printOCLWrapperTerm(Term t) throws IOException {
1611: oclPrettyPrinting = true;
1612: startTerm(1);
1613: markStartSub();
1614: printTerm(t.sub(0));
1615: markEndSub();
1616: }
1617:
1618: /**
1619: * Used for OCL Simplification.
1620: * Pretty-prints iterate expressions.
1621: * "collection->iterate(elem:T1 ; acc:T2=init | expr(elem, acc))"
1622: */
1623: public void printOCLIterateTerm(Term collection, String arrow,
1624: String name, String leftParens, String iterVarDecl,
1625: String sep1, String accVarDecl, String equals,
1626: Term accVarInit, String sep2, Term expr, String rightParens)
1627: throws IOException {
1628: startTerm(3);
1629: layouter.beginC(0);
1630: layouter.beginI(0);
1631: markStartSub();
1632: printTerm(collection);
1633: markEndSub();
1634: layouter.print(arrow).brk(0, 2).print(name).end();
1635: layouter.print(leftParens);
1636: layouter.print(iterVarDecl).print(sep1);
1637: layouter.brk(1, 5);
1638: layouter.print(accVarDecl).print(equals);
1639: markStartSub();
1640: printTerm(accVarInit);
1641: markEndSub();
1642: layouter.print(sep2);
1643: layouter.brk(1, 5);
1644: markStartSub();
1645: printTerm(expr);
1646: markEndSub();
1647: layouter.print(rightParens).end();
1648: }
1649:
1650: /**
1651: * Used for OCL Simplification.
1652: * Pretty-prints Collection operation expressions with one iteration variable.
1653: * "collection->forAll(elem:T | expr(elem))"
1654: */
1655: public void printOCLCollOpBoundVarTerm(Term collection,
1656: String arrow, String name, String leftParens,
1657: String iterVarDecl, String sep, Term expr,
1658: String rightParens) throws IOException {
1659: startTerm(2);
1660: layouter.beginC(0);
1661: layouter.beginI(0);
1662: markStartSub();
1663: printTerm(collection);
1664: markEndSub();
1665: layouter.print(arrow).brk(0, 2).print(name).end();
1666: layouter.print(leftParens);
1667: layouter.print(iterVarDecl).print(sep);
1668: layouter.brk(1, 5);
1669: markStartSub();
1670: printTerm(expr);
1671: markEndSub();
1672: layouter.print(rightParens).end();
1673: }
1674:
1675: /**
1676: * Used for OCL Simplification.
1677: * Pretty-prints Collection operation expressions without iteration variable.
1678: * "collection->includes(object)"
1679: */
1680: public void printOCLCollOpTerm(String name, Term t)
1681: throws IOException {
1682: startTerm(t.arity());
1683: markStartSub();
1684: printTerm(t.sub(0));
1685: markEndSub();
1686: layouter.print("->").print(name).print("(").beginC(0);
1687: for (int i = 1; i < t.arity(); i++) {
1688: markStartSub();
1689: printTerm(t.sub(i));
1690: markEndSub();
1691: if (i < t.arity() - 1) {
1692: layouter.print(",").brk(1, 0);
1693: }
1694: }
1695: layouter.print(")").end();
1696: }
1697:
1698: /**
1699: * Used for OCL Simplification.
1700: * Pretty-prints if-then-else-endif expressions.
1701: */
1702: public void printOCLIfTerm(String ifS, Term ifT, String thenS,
1703: Term thenT, String elseS, Term elseT, String endif)
1704: throws IOException {
1705: startTerm(3);
1706: layouter.beginC(0);
1707: layouter.print(ifS);
1708: markStartSub();
1709: printTerm(ifT);
1710: markEndSub();
1711: layouter.brk(1, 1).print(thenS);
1712: markStartSub();
1713: printTerm(thenT);
1714: markEndSub();
1715: layouter.brk(1, 1).print(elseS);
1716: markStartSub();
1717: printTerm(elseT);
1718: markEndSub();
1719: layouter.brk(1, 0).print(endif).end();
1720: }
1721:
1722: /**
1723: * Used for OCL Simplification.
1724: * Pretty-prints Collection expressions.
1725: * "Set{Alpha, Beta, Gamma}"
1726: */
1727: public void printOCLCollectionTerm(Term t) throws IOException {
1728: startTerm(2);
1729: markStartSub();
1730: printTerm(t.sub(0));
1731: markEndSub();
1732: if (t.sub(1).op() == OclOp.EMPTY_SET
1733: || t.sub(1).op() == OclOp.EMPTY_BAG
1734: || t.sub(1).op() == OclOp.EMPTY_SEQUENCE) {
1735: markStartSub();
1736: layouter.print("");
1737: markEndSub();
1738: } else if (t.sub(1).op() == OclOp.INSERT_SET
1739: || t.sub(1).op() == OclOp.INSERT_BAG
1740: || t.sub(1).op() == OclOp.INSERT_SEQUENCE) {
1741: layouter.print(",").brk(1, 2);
1742: markStartSub();
1743: printOCLCollectionTerm(t.sub(1));
1744: markEndSub();
1745: } else {
1746: layouter.print(",").brk(1, 2);
1747: markStartSub();
1748: printTerm(t.sub(1));
1749: markEndSub();
1750: }
1751: }
1752:
1753: /**
1754: * Used for OCL Simplification.
1755: * Pretty-prints references to UML properties.
1756: * "self.queryMethod()"
1757: */
1758: public void printOCLUMLPropertyTerm(String name, Term t)
1759: throws IOException {
1760: int index = name.indexOf("+~");
1761: if (index == -1) {
1762: String attribute = "."
1763: + name.substring(name.lastIndexOf("~") + 1);
1764: printPostfixTerm(t.sub(0), 80, attribute);
1765: } else {
1766: String temp = name.substring(0, index);
1767: String method = temp.substring(temp.lastIndexOf("~") + 1);
1768: printQueryTerm(method, t, 121);
1769: }
1770: }
1771:
1772: /**
1773: * Used for OCL Simplification.
1774: * Pretty-prints list of OCL constraints.
1775: * "context <Context> inv:
1776: * <the invariant>"
1777: */
1778: public void printOCLInvariantTerm(Term context, Term invariant)
1779: throws IOException {
1780: startTerm(2);
1781: layouter.beginC(0);
1782: layouter.print("context ");
1783: markStartSub();
1784: printTerm(context);
1785: markEndSub();
1786: layouter.print(" inv:").brk(1, 3);
1787: markStartSub();
1788: printTerm(invariant);
1789: markEndSub();
1790: layouter.end();
1791: }
1792:
1793: /**
1794: * Used for OCL Simplification.
1795: * Pretty-prints OCL constraints.
1796: * "context <Context1> inv:
1797: * <invariant1>
1798: *
1799: * context <Context2> inv:
1800: * <invariant2>"
1801: */
1802: public void printOCLListOfInvariantsTerm(Term t) throws IOException {
1803: if (t.arity() > 0) {
1804: startTerm(2);
1805: markStartSub();
1806: printTerm(t.sub(0));
1807: markEndSub();
1808: if (t.sub(1).op() == OclOp.NIL_INV) {
1809: markStartSub();
1810: layouter.print("");
1811: markEndSub();
1812: } else {
1813: layouter.print("\n\n").brk(0, 0);
1814: markStartSub();
1815: printOCLListOfInvariantsTerm(t.sub(1));
1816: markEndSub();
1817: }
1818: }
1819: }
1820:
1821: /**
1822: * Returns the pretty-printed sequent. This should only be called
1823: * after a <tt>printSequent</tt> invocation returns.
1824: *
1825: * @return the pretty-printed sequent.
1826: */
1827: public String toString() {
1828: try {
1829: layouter.flush();
1830: } catch (IOException e) {
1831: throw new RuntimeException(
1832: "IO Exception in pretty printer:\n" + e);
1833: }
1834: return ((PosTableStringBackend) backend).getString() + "\n";
1835: }
1836:
1837: /**
1838: * Returns the pretty-printed sequent in a StringBuffer. This
1839: * should only be called after a <tt>printSequent</tt> invocation
1840: * returns.
1841: *
1842: * @return the pretty-printed sequent.
1843: */
1844: public StringBuffer result() {
1845: try {
1846: layouter.flush();
1847: } catch (IOException e) {
1848: throw new RuntimeException(
1849: "IO Exception in pretty printer:\n" + e);
1850: }
1851: return new StringBuffer(((PosTableStringBackend) backend)
1852: .getString()).append("\n");
1853: }
1854:
1855: protected Layouter mark(Object o) {
1856: if (pure) {
1857: return null;
1858: } else {
1859: return layouter.mark(o);
1860: }
1861: }
1862:
1863: /**
1864: * returns the PositionTable representing position information on
1865: * the sequent of this LogicPrinter. Subclasses may overwrite
1866: * this method with a null returning body if position information
1867: * is not computed there.
1868: */
1869: public InitialPositionTable getPositionTable() {
1870: if (pure) {
1871: return null;
1872: }
1873: return ((PosTableStringBackend) backend).getPositionTable();
1874: }
1875:
1876: /** Returns the ProgramPrinter
1877: * @return the ProgramPrinter
1878: */
1879: public ProgramPrinter programPrinter() {
1880: return prgPrinter;
1881: }
1882:
1883: /** Returns the Layouter
1884: * @return the Layouter
1885: */
1886: protected Layouter getLayouter() {
1887: return layouter;
1888: }
1889:
1890: /**
1891: * Prints a subterm, if needed with parentheses. Each subterm has
1892: * a Priority. If the priority is less than the associativity for
1893: * that subterm fixed by the Notation/NotationInfo, parentheses
1894: * are needed.
1895: *
1896: * <p>If prio and associativity are equal, the subterm is printed
1897: * using {@link #printTermContinuingBlock(Term)}. This currently
1898: * only makes a difference for infix operators.
1899: *
1900: * @param t the the subterm to print
1901: * @param ass the associativity for this subterm */
1902: protected void maybeParens(Term t, int ass) throws IOException {
1903: if (t.op() instanceof SchemaVariable
1904: && instantiations != null
1905: && instantiations.getInstantiation((SchemaVariable) t
1906: .op()) instanceof Term) {
1907: t = (Term) instantiations
1908: .getInstantiation((SchemaVariable) t.op());
1909: }
1910:
1911: if (notationInfo.getNotation(t.op(), services).getPriority() < ass) {
1912: markStartSub();
1913: layouter.print("(");
1914: printTerm(t);
1915: layouter.print(")");
1916: markEndSub();
1917: } else {
1918: markStartSub();
1919: if (notationInfo.getNotation(t.op(), services)
1920: .getPriority() == ass) {
1921: printTermContinuingBlock(t);
1922: } else {
1923: printTerm(t);
1924: }
1925: markEndSub();
1926: }
1927: }
1928:
1929: /**
1930: * @return The SVInstantiations given with the last printTaclet call.
1931: */
1932: public SVInstantiations getInstantiations() {
1933: return instantiations;
1934: }
1935:
1936: /** Mark the start of a subterm. Needed for PositionTable construction.*/
1937: private static final Object MARK_START_SUB = new Object();
1938: /** Mark the end of a subterm. Needed for PositionTable construction.*/
1939: private static final Object MARK_END_SUB = new Object();
1940: /** Mark the start of a term with a number of subterms.
1941: * Needed for PositionTable construction.*/
1942: private static final Object MARK_START_TERM = new Object();
1943: /** Mark the start of the first executable statement.
1944: * Needed for PositionTable construction.*/
1945: private static final Object MARK_START_FIRST_STMT = new Object();
1946: /** Mark the end of the first executable statement.
1947: * Needed for PositionTable construction.*/
1948: private static final Object MARK_END_FIRST_STMT = new Object();
1949: /** Mark the need for a ModalityPositionTable. The next
1950: * startTerm mark will construct a ModalityPositionTable
1951: * instead of the usual PositionTable.
1952: * Needed for PositionTable construction.*/
1953: private static final Object MARK_MODPOSTBL = new Object();
1954: /** Mark the start of an update.*/
1955: private static final Object MARK_START_UPDATE = new Object();
1956: /** Mark the end of an update.*/
1957: private static final Object MARK_END_UPDATE = new Object();
1958:
1959: private boolean createPositionTable = true;
1960:
1961: /**
1962: * Called before a substring is printed that has its own entry in
1963: * a position table. The method sends a mark to the layouter,
1964: * which will make the backend set a start entry in posTbl, push a
1965: * new StackEntry with the current posTbl and current pos on the
1966: * stack and set the current pos to the length of the current
1967: * string result. Subclasses may overwrite this method with an
1968: * empty body if position information is not needed there.
1969: */
1970: protected void markStartSub() {
1971: if (createPositionTable) {
1972: mark(MARK_START_SUB);
1973: }
1974: }
1975:
1976: /**
1977: * Called after a substring is printed that has its own entry in a
1978: * position table. The backend will finishes the position table
1979: * on the top of the stack and set the entry on the top of the
1980: * stack to be the current position/position table. Subclasses may
1981: * overwrite this method with an empty body if position
1982: * information is not needed there.
1983: */
1984: protected void markEndSub() {
1985: if (createPositionTable) {
1986: mark(MARK_END_SUB);
1987: }
1988: }
1989:
1990: /**
1991: * Start a term with subterms. The backend will set the current
1992: * posTbl to a newly created position table with the given number
1993: * of rows. Subclasses may overwrite this method with an empty
1994: * body if position information is not needed there.
1995: *
1996: * @param size the number of rows of the new position table
1997: */
1998: protected void startTerm(int size) {
1999: if (createPositionTable) {
2000: mark(new Integer(size));
2001: }
2002: }
2003:
2004: /**
2005: * returns true if an attribute term shall be printed in short form.
2006: * In opposite to the other <tt>printInShortForm</tt> methods
2007: * it takes care of meta variable instantiations
2008: * @param attributeProgramName the String of the attribute's program
2009: * name
2010: * @param t the Term used as reference prefix
2011: * @return true if an attribute term shall be printed in short form.
2012: */
2013: public boolean printInShortForm(String attributeProgramName, Term t) {
2014: final Sort prefixSort;
2015: if (t.op() instanceof Metavariable) {
2016: Metavariable mv = (Metavariable) t.op();
2017: if (formulaConstraint != null) {
2018: prefixSort = formulaConstraint.getInstantiation(mv)
2019: .sort();
2020: } else {
2021: prefixSort = t.sort();
2022: }
2023: } else {
2024: prefixSort = t.sort();
2025: }
2026: return printInShortForm(attributeProgramName, prefixSort);
2027: }
2028:
2029: /**
2030: * tests if the program name together with the prefix sort
2031: * determines the attribute in a unique way
2032: * @param programName the String denoting the program name of
2033: * the attribute
2034: * @param sort the ObjectSort in whose reachable hierarchy
2035: * we test for uniqueness
2036: * @return true if the attribute is uniquely determined
2037: */
2038: public boolean printInShortForm(String programName, Sort sort) {
2039: return printInShortForm(programName, sort, services);
2040: }
2041:
2042: /**
2043: * tests if the program name together with the prefix sort
2044: * determines the attribute in a unique way
2045: * @param programName the String denoting the program name of
2046: * the attribute
2047: * @param sort the ObjectSort specifying the hierarchy
2048: * where to test for uniqueness
2049: * @param services the Services class used to access the type hierarchy
2050: * @return true if the attribute is uniquely determined
2051: */
2052: public static boolean printInShortForm(String programName,
2053: Sort sort, Services services) {
2054: if (!(services != null && sort != Sort.NULL && sort instanceof ObjectSort))
2055: return false;
2056: final KeYJavaType kjt = services.getJavaInfo().getKeYJavaType(
2057: sort);
2058: assert kjt != null : "Did not find KeYJavaType for " + sort;
2059: return services.getJavaInfo()
2060: .getAllAttributes(programName, kjt).size() == 1;
2061: }
2062:
2063: /** Utility class for stack entries containing the position table
2064: * and the position of the start of the subterm in the result. */
2065: private class StackEntry {
2066:
2067: PositionTable posTbl;
2068: int p;
2069:
2070: StackEntry(PositionTable posTbl, int p) {
2071: this .posTbl = posTbl;
2072: this .p = p;
2073: }
2074:
2075: PositionTable posTbl() {
2076: return posTbl;
2077: }
2078:
2079: int pos() {
2080: return p;
2081: }
2082:
2083: }
2084:
2085: /** A {@link de.uka.ilkd.key.util.pp.Backend} which puts its
2086: * result in a StringBuffer and builds a PositionTable. Position
2087: * table construction is done using the {@link
2088: * de.uka.ilkd.key.util.pp.Layouter#mark(Object)} facility of the
2089: * layouter with the various static <code>MARK_</code> objects
2090: * declared {@link LogicPrinter}.
2091: */
2092: private class PosTableStringBackend extends StringBackend {
2093:
2094: /** The top PositionTable */
2095: private InitialPositionTable initPosTbl = new InitialPositionTable();
2096:
2097: /** The resulting position table or an intermediate result */
2098: private PositionTable posTbl = initPosTbl;
2099:
2100: /** The position in result where the current subterm starts */
2101: private int pos = 0;
2102:
2103: /** The stack of StackEntry representing the nodes above
2104: * the current subterm */
2105: private Stack stack = new Stack();
2106:
2107: /** If this is set, a ModalityPositionTable will
2108: * be built next.
2109: */
2110: private boolean need_modPosTable = false;
2111:
2112: /** These two remember the range corresponding to the first
2113: * executable statement in a JavaBlock */
2114: private int firstStmtStart;
2115: private Range firstStmtRange;
2116:
2117: /** Remembers the start of an update to create a range */
2118: private int updateStart;
2119:
2120: PosTableStringBackend(int lineWidth) {
2121: super (lineWidth);
2122: }
2123:
2124: /** Returns the constructed position table.
2125: * @return the constructed position table
2126: */
2127: public InitialPositionTable getPositionTable() {
2128: return initPosTbl;
2129: }
2130:
2131: private void setupModalityPositionTable(StatementBlock block) {
2132: int count = block.getStatementCount();
2133: int position = 0;
2134: for (int i = 0; i < count; i++) {
2135: posTbl.setStart(position);
2136: position += block.getStatementAt(i).toString().length();
2137: posTbl.setEnd(position - 1, null);
2138: }
2139: }
2140:
2141: /** Receive a mark and act appropriately.
2142: */
2143: public void mark(Object o) {
2144:
2145: // IMPLEMENTATION NOTE
2146: //
2147: // This if-cascade is really ugly. In paricular the part
2148: // which says <code>instanceof Integer</code>, which stand
2149: // for a startTerm with given arity.
2150: //
2151: // The alternative would be to 1.: spread these
2152: // mini-functionalties across several inner classes in a
2153: // visitor-like style, effectively preventing anybody from
2154: // finding out what happens, and 2.: allocate separate
2155: // objects for each startTerm call to wrap the arity.
2156: //
2157: // I (MG) prefer it this way.
2158: if (o == MARK_START_SUB) {
2159: posTbl.setStart(count() - pos);
2160: stack.push(new StackEntry(posTbl, pos));
2161: pos = count();
2162: } else if (o == MARK_END_SUB) {
2163: StackEntry se = (StackEntry) stack.peek();
2164: stack.pop();
2165: pos = se.pos();
2166: se.posTbl().setEnd(count() - pos, posTbl);
2167: posTbl = se.posTbl();
2168: } else if (o == MARK_MODPOSTBL) {
2169: need_modPosTable = true;
2170: } else if (o instanceof Integer) {
2171: // This is sent by startTerm
2172: int rows = ((Integer) o).intValue();
2173: if (need_modPosTable) {
2174: posTbl = new ModalityPositionTable(rows);
2175: } else {
2176: posTbl = new PositionTable(rows);
2177: }
2178: need_modPosTable = false;
2179: } else if (o == MARK_START_FIRST_STMT) {
2180: firstStmtStart = count() - pos;
2181: } else if (o == MARK_END_FIRST_STMT) {
2182: firstStmtRange = new Range(firstStmtStart, count()
2183: - pos);
2184: ((ModalityPositionTable) posTbl)
2185: .setFirstStatementRange(firstStmtRange);
2186: } else if (o == MARK_START_UPDATE) {
2187: updateStart = count();
2188: } else if (o == MARK_END_UPDATE) {
2189: initPosTbl.addUpdateRange(new Range(updateStart,
2190: count()));
2191: }
2192: }
2193: }
2194: }
|