0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.bo.service.unicode;
0017
0018 import java.io.IOException;
0019 import java.util.ArrayList;
0020 import java.util.List;
0021
0022 import org.apache.commons.lang.ArrayUtils;
0023 import org.qedeq.base.io.AbstractOutput;
0024 import org.qedeq.base.io.SourcePosition;
0025 import org.qedeq.base.io.TextOutput;
0026 import org.qedeq.base.trace.Trace;
0027 import org.qedeq.base.utility.DateUtility;
0028 import org.qedeq.base.utility.EqualsUtility;
0029 import org.qedeq.base.utility.StringUtility;
0030 import org.qedeq.kernel.bo.common.ServiceProcess;
0031 import org.qedeq.kernel.bo.module.ControlVisitor;
0032 import org.qedeq.kernel.bo.module.KernelNodeBo;
0033 import org.qedeq.kernel.bo.module.KernelQedeqBo;
0034 import org.qedeq.kernel.bo.module.Reference;
0035 import org.qedeq.kernel.se.base.list.Element;
0036 import org.qedeq.kernel.se.base.list.ElementList;
0037 import org.qedeq.kernel.se.base.module.Add;
0038 import org.qedeq.kernel.se.base.module.Author;
0039 import org.qedeq.kernel.se.base.module.AuthorList;
0040 import org.qedeq.kernel.se.base.module.Axiom;
0041 import org.qedeq.kernel.se.base.module.ChangedRule;
0042 import org.qedeq.kernel.se.base.module.ChangedRuleList;
0043 import org.qedeq.kernel.se.base.module.Chapter;
0044 import org.qedeq.kernel.se.base.module.Conclusion;
0045 import org.qedeq.kernel.se.base.module.ConditionalProof;
0046 import org.qedeq.kernel.se.base.module.Existential;
0047 import org.qedeq.kernel.se.base.module.FormalProof;
0048 import org.qedeq.kernel.se.base.module.FormalProofLine;
0049 import org.qedeq.kernel.se.base.module.Formula;
0050 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0051 import org.qedeq.kernel.se.base.module.Header;
0052 import org.qedeq.kernel.se.base.module.Hypothesis;
0053 import org.qedeq.kernel.se.base.module.Import;
0054 import org.qedeq.kernel.se.base.module.ImportList;
0055 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
0056 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
0057 import org.qedeq.kernel.se.base.module.Latex;
0058 import org.qedeq.kernel.se.base.module.LatexList;
0059 import org.qedeq.kernel.se.base.module.LinkList;
0060 import org.qedeq.kernel.se.base.module.LiteratureItem;
0061 import org.qedeq.kernel.se.base.module.LiteratureItemList;
0062 import org.qedeq.kernel.se.base.module.LocationList;
0063 import org.qedeq.kernel.se.base.module.ModusPonens;
0064 import org.qedeq.kernel.se.base.module.Node;
0065 import org.qedeq.kernel.se.base.module.PredicateDefinition;
0066 import org.qedeq.kernel.se.base.module.Proof;
0067 import org.qedeq.kernel.se.base.module.Proposition;
0068 import org.qedeq.kernel.se.base.module.Qedeq;
0069 import org.qedeq.kernel.se.base.module.Rename;
0070 import org.qedeq.kernel.se.base.module.Rule;
0071 import org.qedeq.kernel.se.base.module.Section;
0072 import org.qedeq.kernel.se.base.module.SectionList;
0073 import org.qedeq.kernel.se.base.module.Specification;
0074 import org.qedeq.kernel.se.base.module.Subsection;
0075 import org.qedeq.kernel.se.base.module.SubsectionList;
0076 import org.qedeq.kernel.se.base.module.SubsectionType;
0077 import org.qedeq.kernel.se.base.module.SubstFree;
0078 import org.qedeq.kernel.se.base.module.SubstFunc;
0079 import org.qedeq.kernel.se.base.module.SubstPred;
0080 import org.qedeq.kernel.se.base.module.Universal;
0081 import org.qedeq.kernel.se.base.module.UsedByList;
0082 import org.qedeq.kernel.se.common.ModuleAddress;
0083 import org.qedeq.kernel.se.common.ModuleContext;
0084 import org.qedeq.kernel.se.common.ModuleDataException;
0085 import org.qedeq.kernel.se.common.Plugin;
0086 import org.qedeq.kernel.se.common.SourceFileExceptionList;
0087 import org.qedeq.kernel.se.visitor.QedeqNumbers;
0088
0089
0090 /**
0091 * Transfer a QEDEQ module into unicode text.
0092 * <p>
0093 * <b>This is just a quick written generator. This class just generates some text output to be able
0094 * to get a visual impression of a QEDEQ module.</b>
0095 *
0096 * @author Michael Meyling
0097 */
0098 public class Qedeq2UnicodeVisitor extends ControlVisitor implements ReferenceFinder {
0099
0100 /** This class. */
0101 private static final Class CLASS = Qedeq2UnicodeVisitor.class;
0102
0103 /** Output goes here. */
0104 private AbstractOutput printer;
0105
0106 /** Filter text to get and produce text in this language. */
0107 private String language;
0108
0109 /** Filter for this detail level. */
0110 // private String level;
0111
0112 /** Should additional information be put into LaTeX output? E.g. QEDEQ reference names. */
0113 private final boolean info;
0114
0115 /** Current node id. */
0116 private String id;
0117
0118 /** Current node title. */
0119 private String title;
0120
0121 /** Sub context like "getIntroduction()". */
0122 private String subContext = "";
0123
0124 /** Maximum column number. If zero no line breaking is done automatically. */
0125 private int maxColumns;
0126
0127 /** Should warning messages be generated if LaTeX problems occur? */
0128 private boolean addWarnings;
0129
0130 /** Should only names and formulas be be printed? */
0131 private final boolean brief;
0132
0133 /** Alphabet for tagging. */
0134 private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
0135
0136 /** Printing data for a single formal proof line. */
0137 private ProofLineData lineData = new ProofLineData();
0138
0139 /** This is the maximal formula width. All proof line formulas that are bigger are wrapped. */
0140 private int formulaWidth = 60;
0141
0142 /** This is the maximal reason width. All proof line reasons that are bigger are wrapped. */
0143 private int reasonWidth = 35;
0144
0145 /** Tabulation string. */
0146 private String tab = "";
0147
0148 /**
0149 * Constructor.
0150 *
0151 * @param plugin This plugin we work for.
0152 * @param prop QEDEQ BO object.
0153 * @param info Write reference info?
0154 * @param maximumColumn Maximum column before automatic break.
0155 * 0 means no automatic break.
0156 * @param addWarnings Should warning messages be generated
0157 * if LaTeX problems occur?
0158 * @param brief Should only names and formulas be be printed?
0159 */
0160 public Qedeq2UnicodeVisitor(final Plugin plugin, final KernelQedeqBo prop,
0161 final boolean info, final int maximumColumn, final boolean addWarnings,
0162 final boolean brief) {
0163 super(plugin, prop);
0164 this.info = info;
0165 this.maxColumns = maximumColumn;
0166 this.addWarnings = addWarnings;
0167 this.brief = brief;
0168 }
0169
0170 /**
0171 * Gives a UTF-8 representation of given QEDEQ module as InputStream.
0172 *
0173 * @param process We run in this process.
0174 * @param printer Print herein.
0175 * @param language Filter text to get and produce text in this language only.
0176 * @param level Filter for this detail level. LATER 20100205 m31: not yet supported
0177 * yet.
0178 * @throws SourceFileExceptionList Major problem occurred.
0179 * @throws IOException File IO failed.
0180 */
0181 public void generateUtf8(final ServiceProcess process, final AbstractOutput printer, final String language,
0182 final String level) throws SourceFileExceptionList, IOException {
0183 setParameters(printer, language);
0184 try {
0185 traverse(process);
0186 } finally {
0187 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
0188 }
0189 }
0190
0191 /**
0192 * Set parameters.
0193 *
0194 * @param printer Print herein.
0195 * @param language Choose this language.
0196 */
0197 public void setParameters(final AbstractOutput printer,
0198 final String language) {
0199 this.printer = printer;
0200 this.printer.setColumns(maxColumns);
0201 // TODO 20110208 m31: perhaps we should have some config parameters for those percentage splittings
0202 if (maxColumns <= 0) {
0203 formulaWidth = 80;
0204 reasonWidth = 50;
0205 } else if (maxColumns <= 50) {
0206 this.printer.setColumns(50);
0207 formulaWidth = 21;
0208 reasonWidth = 21;
0209 } else if (maxColumns <= 100) {
0210 formulaWidth = (maxColumns - 8) * 50 / 100;
0211 reasonWidth = (maxColumns - 8) * 50 / 100;
0212 } else if (maxColumns <= 120) {
0213 reasonWidth = 46 + (maxColumns - 100) / 5;
0214 formulaWidth = maxColumns - 8 - reasonWidth;
0215 } else {
0216 reasonWidth = 50 + (maxColumns - 120) / 10;
0217 formulaWidth = maxColumns - 8 - reasonWidth;
0218 }
0219 // System.out.println("maxColums =" + this.printer.getColumns());
0220 // System.out.println("formulaWidth =" + this.formulaWidth);
0221 // System.out.println("reasonWidth =" + this.reasonWidth);
0222 if (language == null) {
0223 this.language = "en";
0224 } else {
0225 this.language = language;
0226 }
0227 // if (level == null) {
0228 // this.level = "1";
0229 // } else {
0230 // this.level = level;
0231 // }
0232
0233 init();
0234 }
0235
0236 /**
0237 * Reset counters and other variables. Should be executed before {@link #traverse()}.
0238 */
0239 protected void init() {
0240 id = null;
0241 title = null;
0242 subContext = "";
0243 }
0244
0245 public final void visitEnter(final Qedeq qedeq) {
0246 if (printer instanceof TextOutput) {
0247 printer.println("================================================================================");
0248 printer.println("UTF-8-file " + ((TextOutput) printer).getName());
0249 printer.println("Generated from " + getQedeqBo().getModuleAddress());
0250 printer.println("Generated at " + DateUtility.getTimestamp());
0251 printer.println("================================================================================");
0252 printer.println();
0253 printer.println("If the characters of this document don't display correctly try opening this");
0254 printer.println("document within a webbrowser and if necessary change the encoding to");
0255 printer.println("Unicode (UTF-8)");
0256 printer.println();
0257 printer.println("Permission is granted to copy, distribute and/or modify this document");
0258 printer.println("under the terms of the GNU Free Documentation License, Version 1.2");
0259 printer.println("or any later version published by the Free Software Foundation;");
0260 printer.println("with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
0261 printer.println();
0262 printer.println();
0263 printer.println();
0264 }
0265 }
0266
0267 public final void visitLeave(final Qedeq qedeq) {
0268 printer.println();
0269 }
0270
0271 public void visitEnter(final Header header) {
0272 final LatexList tit = header.getTitle();
0273 underlineBig(getLatexListEntry("getTitle()", tit));
0274 printer.println();
0275 final AuthorList authors = getQedeqBo().getQedeq().getHeader().getAuthorList();
0276 final StringBuffer authorList = new StringBuffer();
0277 for (int i = 0; i < authors.size(); i++) {
0278 if (i > 0) {
0279 authorList.append(" \n");
0280 printer.println(", ");
0281 }
0282 final Author author = authors.get(i);
0283 final String name = author.getName().getLatex().trim();
0284 printer.print(name);
0285 authorList.append(" " + name);
0286 String email = author.getEmail();
0287 if (email != null && email.trim().length() > 0) {
0288 authorList.append(" <" + email + ">");
0289 }
0290 }
0291 printer.println();
0292 printer.println();
0293 final String url = getQedeqBo().getUrl();
0294 if (url != null && url.length() > 0) {
0295 printer.println();
0296 if ("de".equals(language)) {
0297 printer.println("Die Quelle f\u00FCr dieses Dokument ist hier zu finden:");
0298 } else {
0299 if (!"en".equals(language)) {
0300 printer.println("%%% TODO unknown language: " + language);
0301 }
0302 printer.println("The source for this document can be found here:");
0303 }
0304 printer.println();
0305 printer.println(url);
0306 printer.println();
0307 }
0308 {
0309 printer.println();
0310 if ("de".equals(language)) {
0311 printer.println("Die vorliegende Publikation ist urheberrechtlich gesch\u00FCtzt.");
0312 } else {
0313 if (!"en".equals(language)) {
0314 printer.println("%%% TODO unknown language: " + language);
0315 }
0316 printer.println("Copyright by the authors. All rights reserved.");
0317 }
0318 }
0319 final String email = header.getEmail();
0320 if (email != null && email.length() > 0) {
0321 printer.println();
0322 printer.println();
0323 if ("de".equals(language)) {
0324 printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der"
0325 + " abh\u00E4ngigen Module schicken Sie bitte eine EMail an die Adresse "
0326 + email);
0327 printer.println();
0328 printer.println();
0329 printer.println("Die Autoren dieses Dokuments sind:");
0330 printer.println();
0331 printer.println(authorList);
0332 } else {
0333 if (!"en".equals(language)) {
0334 printer.println("%%% TODO unknown language: " + language);
0335 }
0336 printer.println("If you have any questions, suggestions or want to add something"
0337 + " to the list of modules that use this one, please send an email to the"
0338 + " address " + email);
0339 printer.println();
0340 printer.println();
0341 printer.println("The authors of this document are:");
0342 printer.println(authorList);
0343 }
0344 printer.println();
0345 }
0346 printer.println();
0347 printer.println();
0348 }
0349
0350 public void visitEnter(final ImportList imports) throws ModuleDataException {
0351 // this method call is a little bit odd but we have to print the imports
0352 // also in the literature list and we don't want to have doubled code
0353 printImports();
0354 }
0355
0356 /**
0357 * Get URL for QEDEQ XML module.
0358 *
0359 * @param address Current module address.
0360 * @param specification Find URL for this location list.
0361 * @return URL or <code>""</code> if none (valid?) was found.
0362 */
0363 private String getUrl(final ModuleAddress address, final Specification specification) {
0364 final LocationList list = specification.getLocationList();
0365 if (list == null || list.size() <= 0) {
0366 return "";
0367 }
0368 try {
0369 return address.getModulePaths(specification)[0].getUrl();
0370 } catch (IOException e) {
0371 return "";
0372 }
0373 }
0374
0375 public void visitEnter(final Chapter chapter) {
0376 // check if we print only brief and test for non text subnodes
0377 if (brief) {
0378 boolean hasFormalContent = false;
0379 do {
0380 final SectionList sections = chapter.getSectionList();
0381 if (sections == null) {
0382 break;
0383 }
0384 for (int i = 0; i < sections.size() && !hasFormalContent; i++) {
0385 final Section section = sections.get(i);
0386 if (section == null) {
0387 continue;
0388 }
0389 final SubsectionList subSections = section.getSubsectionList();
0390 if (subSections == null) {
0391 continue;
0392 }
0393 for (int j = 0; j < subSections.size(); j++) {
0394 final SubsectionType subSection = subSections.get(j);
0395 if (!(subSection instanceof Subsection)) {
0396 hasFormalContent = true;
0397 break;
0398 }
0399 }
0400 }
0401 } while (false);
0402 if (!hasFormalContent) {
0403 setBlocked(true);
0404 return;
0405 }
0406 }
0407 final QedeqNumbers numbers = getCurrentNumbers();
0408 if (numbers.isChapterNumbering()) {
0409 if ("de".equals(language)) {
0410 printer.println("Kapitel " + numbers.getChapterNumber() + " ");
0411 } else {
0412 printer.println("Chapter " + numbers.getChapterNumber() + " ");
0413 }
0414 printer.println();
0415 printer.println();
0416 }
0417 underlineBig(getLatexListEntry("getTitle()", chapter.getTitle()));
0418 printer.println();
0419 if (chapter.getIntroduction() != null && !brief) {
0420 printer.append(getLatexListEntry("getIntroduction()", chapter.getIntroduction()));
0421 printer.println();
0422 printer.println();
0423 printer.println();
0424 }
0425 }
0426
0427 public void visitLeave(final Header header) {
0428 printer.println();
0429 printer.println("___________________________________________________");
0430 printer.println();
0431 printer.println();
0432 }
0433
0434 public void visitLeave(final Chapter chapter) {
0435 if (!getBlocked()) {
0436 printer.println();
0437 printer.println("___________________________________________________");
0438 printer.println();
0439 printer.println();
0440 }
0441 setBlocked(false);
0442 }
0443
0444 public void visitEnter(final Section section) {
0445 // check if we print only brief and test for non text subnodes
0446 if (brief) {
0447 boolean hasFormalContent = false;
0448 do {
0449 final SubsectionList subSections = section.getSubsectionList();
0450 if (subSections == null) {
0451 break;
0452 }
0453 for (int j = 0; j < subSections.size(); j++) {
0454 final SubsectionType subSection = subSections.get(j);
0455 if (!(subSection instanceof Subsection)) {
0456 hasFormalContent = true;
0457 break;
0458 }
0459 }
0460 } while (false);
0461 if (!hasFormalContent) {
0462 setBlocked(true);
0463 return;
0464 }
0465 }
0466 final QedeqNumbers numbers = getCurrentNumbers();
0467 final StringBuffer buffer = new StringBuffer();
0468 if (numbers.isChapterNumbering()) {
0469 buffer.append(numbers.getChapterNumber());
0470 }
0471 if (numbers.isSectionNumbering()) {
0472 if (buffer.length() > 0) {
0473 buffer.append(".");
0474 }
0475 buffer.append(numbers.getSectionNumber());
0476 }
0477 if (buffer.length() > 0 && section.getTitle() != null) {
0478 buffer.append(" ");
0479 }
0480 buffer.append(getLatexListEntry("getTitle()", section.getTitle()));
0481 underline(buffer.toString());
0482 printer.println();
0483 if (section.getIntroduction() != null && !brief) {
0484 printer.append(getLatexListEntry("getIntroduction()", section.getIntroduction()));
0485 printer.println();
0486 printer.println();
0487 printer.println();
0488 }
0489 }
0490
0491 public void visitLeave(final Section section) {
0492 if (!getBlocked()) {
0493 printer.println();
0494 }
0495 setBlocked(false);
0496 }
0497
0498 public void visitEnter(final Subsection subsection) {
0499 if (brief) {
0500 return;
0501 }
0502 final QedeqNumbers numbers = getCurrentNumbers();
0503 final StringBuffer buffer = new StringBuffer();
0504 if (numbers.isChapterNumbering()) {
0505 buffer.append(numbers.getChapterNumber());
0506 }
0507 if (numbers.isSectionNumbering()) {
0508 if (buffer.length() > 0) {
0509 buffer.append(".");
0510 }
0511 buffer.append(numbers.getSectionNumber());
0512 }
0513 if (buffer.length() > 0) {
0514 buffer.append(".");
0515 }
0516 buffer.append(numbers.getSubsectionNumber());
0517 if (buffer.length() > 0 && subsection.getTitle() != null) {
0518 buffer.append(" ");
0519 }
0520 if (subsection.getTitle() != null) {
0521 printer.print(buffer.toString());
0522 printer.print(getLatexListEntry("getTitle()", subsection.getTitle()));
0523 }
0524 if (subsection.getId() != null && info) {
0525 printer.print(" [" + subsection.getId() + "]");
0526 }
0527 if (subsection.getTitle() != null) {
0528 printer.println();
0529 printer.println();
0530 }
0531 printer.append(getLatexListEntry("getLatex()", subsection.getLatex()));
0532 printer.println();
0533 printer.println();
0534 }
0535
0536 public void visitEnter(final Node node) {
0537 if (node.getPrecedingText() != null && !brief) {
0538 printer.append(getLatexListEntry("getPrecedingText()", node.getPrecedingText()));
0539 printer.println();
0540 printer.println();
0541 }
0542 id = node.getId();
0543 title = null;
0544 if (node.getTitle() != null) {
0545 title = getLatexListEntry("getTitle()", node.getTitle());
0546 }
0547 }
0548
0549 public void visitLeave(final Node node) {
0550 if (node.getSucceedingText() != null && !brief) {
0551 printer.append(getLatexListEntry("getSucceedingText()", node.getSucceedingText()));
0552 printer.println();
0553 printer.println();
0554 }
0555 printer.println();
0556 }
0557
0558 public void visitEnter(final Axiom axiom) {
0559 final QedeqNumbers numbers = getCurrentNumbers();
0560 printer.print("\u2609 ");
0561 printer.print("Axiom " + numbers.getAxiomNumber());
0562 printer.print(" ");
0563 if (title != null && title.length() > 0) {
0564 printer.print(" (" + title + ")");
0565 }
0566 if (info) {
0567 printer.print(" [" + id + "]");
0568 }
0569 printer.println();
0570 printer.println();
0571 printer.print(" ");
0572 printFormula(axiom.getFormula().getElement());
0573 printer.println();
0574 if (axiom.getDescription() != null) {
0575 printer.append(getLatexListEntry("getDescription()", axiom.getDescription()));
0576 printer.println();
0577 printer.println();
0578 }
0579 }
0580
0581 public void visitEnter(final Proposition proposition) {
0582 final QedeqNumbers numbers = getCurrentNumbers();
0583 printer.print("\u2609 ");
0584 printer.print("Proposition " + numbers.getPropositionNumber());
0585 printer.print(" ");
0586 if (title != null && title.length() > 0) {
0587 printer.print(" (" + title + ")");
0588 }
0589 if (info) {
0590 printer.print(" [" + id + "]");
0591 }
0592 printer.println();
0593 printer.println();
0594 printTopFormula(proposition.getFormula().getElement(), id);
0595 printer.println();
0596 if (proposition.getDescription() != null) {
0597 printer.append(getLatexListEntry("getDescription()", proposition.getDescription()));
0598 printer.println();
0599 printer.println();
0600 }
0601 }
0602
0603 public void visitEnter(final Proof proof) {
0604 if (brief) {
0605 setBlocked(true);
0606 return;
0607 }
0608 if ("de".equals(language)) {
0609 printer.println("Beweis:");
0610 } else {
0611 printer.println("Proof:");
0612 }
0613 printer.append(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof()));
0614 }
0615
0616 public void visitLeave(final Proof proof) {
0617 printer.println();
0618 printer.println("q.e.d.");
0619 printer.println();
0620 setBlocked(false);
0621 }
0622
0623 public void visitEnter(final FormalProof proof) {
0624 if (brief) {
0625 setBlocked(true);
0626 return;
0627 }
0628 if ("de".equals(language)) {
0629 printer.println("Beweis (formal):");
0630 } else {
0631 printer.println("Proof (formal):");
0632 }
0633 }
0634
0635 public void visitLeave(final FormalProof proof) {
0636 if (!brief) {
0637 printer.println("q.e.d.");
0638 printer.println();
0639 }
0640 setBlocked(false);
0641 }
0642
0643
0644 public void visitEnter(final FormalProofLine line) {
0645 lineData.init();
0646 if (line.getLabel() != null) {
0647 lineData.setLineLabel(line.getLabel());
0648 }
0649 if (line.getReason() != null) {
0650 setReason(line.getReason().toString());
0651 }
0652 setFormula(line.getFormula());
0653 }
0654
0655 public void visitLeave(final FormalProofLine line) {
0656 linePrintln();
0657 }
0658
0659 /**
0660 * Print formula and reason.
0661 */
0662 private void linePrintln() {
0663 if (!lineData.containsData()) {
0664 return;
0665 }
0666 if (lineData.getLineLabel().length() > 0) {
0667 printer.print(StringUtility.alignRight("(" + lineData.getLineLabel() + ")", 5) + " ");
0668 }
0669 for (int i = 0; i < lineData.lines(); i++) {
0670 printer.skipToColumn(6);
0671 printer.print(tab);
0672 if (i < lineData.getFormula().length) {
0673 printer.print(lineData.getFormula()[i]);
0674 }
0675 if (i < lineData.getReason().length) {
0676 printer.skipToColumn(6 + 2 + formulaWidth);
0677 printer.print(lineData.getReason()[i]);
0678 }
0679 printer.println();
0680 }
0681 lineData.init();
0682 }
0683
0684 public void visitEnter(final ConditionalProof r) throws ModuleDataException {
0685 lineData.init();
0686 printer.skipToColumn(6);
0687 printer.print(tab);
0688 printer.println("Conditional Proof");
0689 tab = tab + " ";
0690 }
0691
0692 public void visitLeave(final ConditionalProof proof) {
0693 tab = StringUtility.substring(tab, 0, tab.length() - 2);
0694 }
0695
0696 public void visitEnter(final Hypothesis hypothesis) {
0697 lineData.init();
0698 if (hypothesis.getLabel() != null) {
0699 lineData.setLineLabel(hypothesis.getLabel());
0700 }
0701 setReason("Hypothesis");
0702 setFormula(hypothesis.getFormula());
0703 }
0704
0705 public void visitLeave(final Hypothesis hypothesis) {
0706 linePrintln();
0707 }
0708
0709 public void visitEnter(final Conclusion conclusion) {
0710 tab = StringUtility.substring(tab, 0, tab.length() - 2);
0711 lineData.init();
0712 if (conclusion.getLabel() != null) {
0713 lineData.setLineLabel(conclusion.getLabel());
0714 }
0715 setReason("Conclusion");
0716 setFormula(conclusion.getFormula());
0717 linePrintln();
0718 }
0719
0720 public void visitLeave(final Conclusion conclusion) {
0721 linePrintln();
0722 tab = tab + " ";
0723 }
0724
0725 private void setReason(final String reasonString) {
0726 final List list = new ArrayList();
0727 int index = 0;
0728 while (index < reasonString.length()) {
0729 list.add(StringUtility.substring(reasonString, index, reasonWidth));
0730 index += reasonWidth;
0731 }
0732 lineData.setReason((String[]) list.toArray(ArrayUtils.EMPTY_STRING_ARRAY));
0733 }
0734
0735 private void setFormula(final Formula f) {
0736 if (f != null && f.getElement() != null) {
0737 lineData.setFormula(getUtf8(f.getElement(),
0738 formulaWidth - tab.length()));
0739 }
0740 }
0741
0742 private String getReference(final String reference) {
0743 return getReference(reference, "getReference()");
0744 }
0745
0746 private String getReference(final String reference, final String subContext) {
0747 final String context = getCurrentContext().getLocationWithinModule();
0748 try {
0749 getCurrentContext().setLocationWithinModule(context + "." + subContext);
0750 return (getReferenceLink(reference, null, null));
0751 } finally {
0752 getCurrentContext().setLocationWithinModule(context);
0753 }
0754 }
0755
0756 public void visitEnter(final ModusPonens r) throws ModuleDataException {
0757 String buffer = r.getName();
0758 boolean one = false;
0759 if (r.getReference1() != null) {
0760 buffer += " " + getReference(r.getReference1(), "getReference1()");
0761 one = true;
0762 }
0763 if (r.getReference1() != null) {
0764 if (one) {
0765 buffer += ",";
0766 }
0767 buffer += " " + getReference(r.getReference2(), "getReference2()");
0768 }
0769 setReason(buffer);
0770 }
0771
0772 public void visitEnter(final Add r) throws ModuleDataException {
0773 String buffer = r.getName();
0774 if (r.getReference() != null) {
0775 buffer += " " + getReference(r.getReference());
0776 }
0777 setReason(buffer);
0778 }
0779
0780 public void visitEnter(final Rename r) throws ModuleDataException {
0781 String buffer = r.getName();
0782 if (r.getOriginalSubjectVariable() != null) {
0783 buffer += " " + getUtf8(r.getOriginalSubjectVariable());
0784 }
0785 if (r.getReplacementSubjectVariable() != null) {
0786 buffer += " by " + getUtf8(r.getReplacementSubjectVariable());
0787 }
0788 if (r.getReference() != null) {
0789 buffer += " in " + getReference(r.getReference());
0790 }
0791 setReason(buffer);
0792 }
0793
0794 public void visitEnter(final SubstFree r) throws ModuleDataException {
0795 String buffer = r.getName();
0796 if (r.getSubjectVariable() != null) {
0797 buffer += " " + getUtf8(r.getSubjectVariable());
0798 }
0799 if (r.getSubstituteTerm() != null) {
0800 buffer += " by " + getUtf8(r.getSubstituteTerm());
0801 }
0802 if (r.getReference() != null) {
0803 buffer += " in " + getReference(r.getReference());
0804 }
0805 setReason(buffer);
0806 }
0807
0808 public void visitEnter(final SubstFunc r) throws ModuleDataException {
0809 String buffer = r.getName();
0810 if (r.getFunctionVariable() != null) {
0811 buffer += " " + getUtf8(r.getFunctionVariable());
0812 }
0813 if (r.getSubstituteTerm() != null) {
0814 buffer += " by " + getUtf8(r.getSubstituteTerm());
0815 }
0816 if (r.getReference() != null) {
0817 buffer += " in " + getReference(r.getReference());
0818 }
0819 setReason(buffer);
0820 }
0821
0822 public void visitEnter(final SubstPred r) throws ModuleDataException {
0823 String buffer = r.getName();
0824 if (r.getPredicateVariable() != null) {
0825 buffer += " " + getUtf8(r.getPredicateVariable());
0826 }
0827 if (r.getSubstituteFormula() != null) {
0828 buffer += " by " + getUtf8(r.getSubstituteFormula());
0829 }
0830 if (r.getReference() != null) {
0831 buffer += " in " + getReference(r.getReference());
0832 }
0833 setReason(buffer);
0834 }
0835
0836 public void visitEnter(final Existential r) throws ModuleDataException {
0837 String buffer = r.getName();
0838 if (r.getSubjectVariable() != null) {
0839 buffer += " with " + getUtf8(r.getSubjectVariable());
0840 }
0841 if (r.getReference() != null) {
0842 buffer += " in " + getReference(r.getReference());
0843 }
0844 setReason(buffer);
0845 }
0846
0847 public void visitEnter(final Universal r) throws ModuleDataException {
0848 String buffer = r.getName();
0849 if (r.getSubjectVariable() != null) {
0850 buffer += " with " + getQedeqBo().getElement2Utf8().getUtf8(
0851 r.getSubjectVariable());
0852 }
0853 if (r.getReference() != null) {
0854 buffer += " in " + getReference(r.getReference());
0855 }
0856 setReason(buffer);
0857 }
0858
0859 public void visitEnter(final InitialPredicateDefinition definition) {
0860 final QedeqNumbers numbers = getCurrentNumbers();
0861 printer.print("\u2609 ");
0862 final StringBuffer buffer = new StringBuffer();
0863 if ("de".equals(language)) {
0864 buffer.append("initiale ");
0865 } else {
0866 buffer.append("initial ");
0867 }
0868 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0869 + numbers.getFunctionDefinitionNumber()));
0870 printer.print(buffer.toString());
0871 printer.print(" ");
0872 if (title != null && title.length() > 0) {
0873 printer.print(" (" + title + ")");
0874 }
0875 if (info) {
0876 printer.print(" [" + id + "]");
0877 }
0878 printer.println();
0879 printer.println();
0880 printer.print(" ");
0881 printer.println(getUtf8(definition.getPredCon()));
0882 printer.println();
0883 if (definition.getDescription() != null) {
0884 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
0885 printer.println();
0886 printer.println();
0887 }
0888 }
0889
0890 public void visitEnter(final PredicateDefinition definition) {
0891 final QedeqNumbers numbers = getCurrentNumbers();
0892 printer.print("\u2609 ");
0893 final StringBuffer buffer = new StringBuffer();
0894 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0895 + numbers.getFunctionDefinitionNumber()));
0896 printer.print(buffer.toString());
0897 printer.print(" ");
0898 if (title != null && title.length() > 0) {
0899 printer.print(" (" + title + ")");
0900 }
0901 if (info) {
0902 printer.print(" [" + id + "]");
0903 }
0904 printer.println();
0905 printer.println();
0906 printer.print(" ");
0907 printer.println(getUtf8(definition.getFormula().getElement()));
0908 printer.println();
0909 if (definition.getDescription() != null) {
0910 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
0911 printer.println();
0912 printer.println();
0913 }
0914 }
0915
0916 public void visitEnter(final InitialFunctionDefinition definition) {
0917 final QedeqNumbers numbers = getCurrentNumbers();
0918 printer.print("\u2609 ");
0919 final StringBuffer buffer = new StringBuffer();
0920 if ("de".equals(language)) {
0921 buffer.append("initiale ");
0922 } else {
0923 buffer.append("initial ");
0924 }
0925 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0926 + numbers.getFunctionDefinitionNumber()));
0927 printer.print(buffer.toString());
0928 printer.print(" ");
0929 if (title != null && title.length() > 0) {
0930 printer.print(" (" + title + ")");
0931 }
0932 if (info) {
0933 printer.print(" [" + id + "]");
0934 }
0935 printer.println();
0936 printer.println();
0937 printer.print(" ");
0938 printer.println(getUtf8(definition.getFunCon()));
0939 printer.println();
0940 if (definition.getDescription() != null) {
0941 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
0942 printer.println();
0943 }
0944 }
0945
0946 public void visitEnter(final FunctionDefinition definition) {
0947 final QedeqNumbers numbers = getCurrentNumbers();
0948 printer.print("\u2609 ");
0949 final StringBuffer buffer = new StringBuffer();
0950 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0951 + numbers.getFunctionDefinitionNumber()));
0952 printer.print(buffer.toString());
0953 printer.print(" ");
0954 if (title != null && title.length() > 0) {
0955 printer.print(" (" + title + ")");
0956 }
0957 if (info) {
0958 printer.print(" [" + id + "]");
0959 }
0960 printer.println();
0961 printer.println();
0962 printer.print(" ");
0963 printer.println(getUtf8(definition.getFormula().getElement()));
0964 printer.println();
0965 if (definition.getDescription() != null) {
0966 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
0967 printer.println();
0968 }
0969 }
0970
0971 public void visitEnter(final Rule rule) {
0972 final QedeqNumbers numbers = getCurrentNumbers();
0973 printer.print("\u2609 ");
0974 if ("de".equals(language)) {
0975 printer.print("Regel");
0976 } else {
0977 printer.print("Rule");
0978 }
0979 printer.print(" " + numbers.getRuleNumber());
0980 printer.print(" ");
0981 if (title != null && title.length() > 0) {
0982 printer.print(" (" + title + ")");
0983 }
0984 if (info) {
0985 printer.print(" [" + id + "]");
0986 }
0987 printer.println();
0988 printer.println((rule.getName() != null ? " Name: " + rule.getName() : "")
0989 + (rule.getVersion() != null ? " - Version: " + rule.getVersion() : ""));
0990 printer.println();
0991 if (rule.getDescription() != null) {
0992 printer.append(getLatexListEntry("getDescription()", rule.getDescription()));
0993 printer.println();
0994 printer.println();
0995 }
0996 }
0997
0998 public void visitEnter(final LinkList linkList) {
0999 if (linkList.size() <= 0) {
1000 return;
1001 }
1002 if ("de".equals(language)) {
1003 printer.println("Basierend auf: ");
1004 } else {
1005 if (!"en".equals(language)) {
1006 printer.println("%%% TODO unknown language: " + language);
1007 }
1008 printer.println("Based on: ");
1009 }
1010 for (int i = 0; i < linkList.size(); i++) {
1011 if (linkList.get(i) != null) {
1012 printer.print(" (" + linkList.get(i) + ")");
1013 }
1014 };
1015 printer.println();
1016 }
1017
1018 public void visitEnter(final ChangedRuleList list) {
1019 if (list.size() <= 0) {
1020 return;
1021 }
1022 printer.println();
1023 if ("de".equals(language)) {
1024 printer.println("Die folgenden Regeln m\u00FCssen erweitert werden.");
1025 } else {
1026 if (!"en".equals(language)) {
1027 printer.println("%%% TODO unknown language: " + language);
1028 }
1029 printer.println("The following rules have to be extended.");
1030 }
1031 printer.println();
1032 }
1033
1034 public void visitEnter(final ChangedRule rule) {
1035 printer.println((rule.getName() != null ? " Name: " + rule.getName() : "")
1036 + (rule.getVersion() != null ? " - Version: " + rule.getVersion() : ""));
1037 printer.println();
1038 if (rule.getDescription() != null) {
1039 printer.append(getLatexListEntry("getDescription()", rule.getDescription()));
1040 printer.println();
1041 printer.println();
1042 }
1043
1044 }
1045
1046 public void visitEnter(final LiteratureItemList list) {
1047 printer.println();
1048 printer.println();
1049 if ("de".equals(language)) {
1050 underlineBig("Literaturverzeichnis");
1051 } else {
1052 underlineBig("Bibliography");
1053 }
1054 printImports();
1055 }
1056
1057 /**
1058 * Print all imports if any.
1059 */
1060 private void printImports() {
1061 final ImportList imports = getQedeqBo().getQedeq().getHeader().getImportList();
1062 if (imports != null && imports.size() > 0) {
1063 printer.println();
1064 printer.println();
1065 if ("de".equals(language)) {
1066 printer.println("Benutzte andere QEDEQ-Module:");
1067 } else {
1068 printer.println("Used other QEDEQ modules:");
1069 }
1070 printer.println();
1071 for (int i = 0; i < imports.size(); i++) {
1072 final Import imp = imports.get(i);
1073 printer.print("[" + imp.getLabel() + "] ");
1074 final Specification spec = imp.getSpecification();
1075 printer.print(spec.getName());
1076 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
1077 && spec.getLocationList().get(0).getLocation().length() > 0) {
1078 printer.print(" ");
1079 printer.print(getUrl(getQedeqBo().getModuleAddress(), spec));
1080 }
1081 printer.println();
1082 }
1083 printer.println();
1084 printer.println();
1085 }
1086 }
1087
1088 public void visitLeave(final LiteratureItemList list) {
1089 final UsedByList usedby = getQedeqBo().getQedeq().getHeader().getUsedByList();
1090 if (usedby != null && usedby.size() > 0) {
1091 printer.println();
1092 printer.println();
1093 if ("de".equals(language)) {
1094 printer.println("QEDEQ-Module, welche dieses hier verwenden:");
1095 } else {
1096 printer.println("QEDEQ modules that use this one:");
1097 }
1098 for (int i = 0; i < usedby.size(); i++) {
1099 final Specification spec = usedby.get(i);
1100 printer.print(spec.getName());
1101 final String url = getUrl(getQedeqBo().getModuleAddress(), spec);
1102 if (url != null && url.length() > 0) {
1103 printer.print(" ");
1104 printer.print(url);
1105 }
1106 printer.println();
1107 }
1108 printer.println();
1109 printer.println();
1110 }
1111 printer.println();
1112 }
1113
1114 public void visitEnter(final LiteratureItem item) {
1115 printer.print("[" + item.getLabel() + "] ");
1116 printer.println(getLatexListEntry("getItem()", item.getItem()));
1117 printer.println();
1118 }
1119
1120 /**
1121 * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
1122 * formula is broken down in several labeled lines.
1123 *
1124 * @param element Formula to print.
1125 * @param mainLabel Main formula label.
1126 */
1127 private void printTopFormula(final Element element, final String mainLabel) {
1128 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
1129 printer.print(" ");
1130 printFormula(element);
1131 return;
1132 }
1133 final ElementList list = element.getList();
1134 for (int i = 0; i < list.size(); i++) {
1135 String label = "";
1136 if (list.size() >= ALPHABET.length() * ALPHABET.length()) {
1137 label = "" + (i + 1);
1138 } else {
1139 if (list.size() > ALPHABET.length()) {
1140 final int div = (i / ALPHABET.length());
1141 label = "" + ALPHABET.charAt(div);
1142 }
1143 label += ALPHABET.charAt(i % ALPHABET.length());
1144 }
1145 printer.println(" (" + label + ") " + getUtf8(list.getElement(i)));
1146 }
1147 }
1148
1149 /**
1150 * Print formula.
1151 *
1152 * @param element Formula to print.
1153 */
1154 private void printFormula(final Element element) {
1155 printer.println(getUtf8(element));
1156 }
1157
1158 /**
1159 * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
1160 * language.
1161 *
1162 * @param method This method was called. Used to get the correct sub context.
1163 * Should not be null. If it is empty the <code>subContext</code>
1164 * is not changed.
1165 * @param list List of LaTeX texts.
1166 * @return Filtered text.
1167 */
1168 private String getLatexListEntry(final String method, final LatexList list) {
1169 if (list == null) {
1170 return "";
1171 }
1172 if (method.length() > 0) {
1173 subContext = method;
1174 }
1175 try {
1176 for (int i = 0; i < list.size(); i++) {
1177 if (language.equals(list.get(i).getLanguage())) {
1178 if (method.length() > 0) {
1179 subContext = method + ".get(" + i + ")";
1180 }
1181 return getUtf8(list.get(i));
1182 }
1183 }
1184 // OK, we didn't found the language, so we take the default language
1185 final String def = getQedeqBo().getOriginalLanguage();
1186 for (int i = 0; i < list.size(); i++) {
1187 if (EqualsUtility.equals(def, list.get(i).getLanguage())) {
1188 if (method.length() > 0) {
1189 subContext = method + ".get(" + i + ")";
1190 }
1191 return "MISSING! OTHER: " + getUtf8(list.get(i));
1192 }
1193 }
1194 // OK, we didn't find wanted and default language, so we take the first non empty one
1195 for (int i = 0; i < list.size(); i++) {
1196 if (method.length() > 0) {
1197 subContext = method + ".get(" + i + ")";
1198 }
1199 if (null != list.get(i) && null != list.get(i).getLatex()
1200 && list.get(i).getLatex().trim().length() > 0) {
1201 return "MISSING! OTHER: " + getUtf8(list.get(i));
1202 }
1203 }
1204 return "MISSING!";
1205 } finally {
1206 if (method.length() > 0) {
1207 subContext = "";
1208 }
1209 }
1210 }
1211
1212 /**
1213 * Get current module context. Uses sub context information.
1214 *
1215 * @param startDelta Skip position (relative to location start). Could be
1216 * <code>null</code>.
1217 * @param endDelta Mark until this column (relative to location start).
1218 * be <code>null</code>
1219 * @return Current module context.
1220 */
1221 private ModuleContext getCurrentContext(final SourcePosition startDelta,
1222 final SourcePosition endDelta) {
1223 if (subContext.length() == 0) {
1224 return super.getCurrentContext();
1225 }
1226 final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(),
1227 super.getCurrentContext().getLocationWithinModule() + "." + subContext,
1228 startDelta, endDelta);
1229 return c;
1230 }
1231
1232 /**
1233 * Add warning.
1234 *
1235 * @param code Warning code.
1236 * @param msg Warning message.
1237 * @param startDelta Skip position (relative to location start). Could be
1238 * <code>null</code>.
1239 * @param endDelta Mark until this column (relative to location start). Could be
1240 * be <code>null</code>
1241 */
1242 public void addWarning(final int code, final String msg, final SourcePosition startDelta,
1243 final SourcePosition endDelta) {
1244 Trace.param(CLASS, this, "addWarning", "msg", msg);
1245 if (addWarnings) {
1246 addWarning(new UnicodeException(code, msg, getCurrentContext(startDelta,
1247 endDelta)));
1248 }
1249 }
1250
1251 /**
1252 * Add warning.
1253 *
1254 * @param code Warning code.
1255 * @param msg Warning message.
1256 */
1257 public void addWarning(final int code, final String msg) {
1258 Trace.param(CLASS, this, "addWarning", "msg", msg);
1259 if (addWarnings) {
1260 addWarning(new UnicodeException(code, msg, getCurrentContext()));
1261 }
1262 }
1263
1264 /**
1265 * Get Utf8 element presentation.
1266 *
1267 * @param element Get presentation of this element.
1268 * @param max Maximum column.
1269 * @return UTF-8 form of element.
1270 */
1271 protected String[] getUtf8(final Element element, final int max) {
1272 return getQedeqBo().getElement2Utf8().getUtf8(element, max);
1273 }
1274
1275
1276 /**
1277 * Get Utf8 element presentation.
1278 *
1279 * @param element Get presentation of this element.
1280 * @return UTF-8 form of element.
1281 */
1282 protected String getUtf8(final Element element) {
1283 return getUtf8(getQedeqBo().getElement2Latex().getLatex(element));
1284 }
1285
1286 /**
1287 * Get UTF-8 String for LaTeX.
1288 *
1289 * @param latex LaTeX we got.
1290 * @return UTF-8 result string.
1291 */
1292 private String getUtf8(final Latex latex) {
1293 if (latex == null || latex.getLatex() == null) {
1294 return "";
1295 }
1296 return getUtf8(latex.getLatex());
1297 }
1298
1299 /**
1300 * Transform LaTeX into UTF-8 String..
1301 *
1302 * @param latex LaTeX text.
1303 * @return String.
1304 */
1305 private String getUtf8(final String latex) {
1306 if (latex == null) {
1307 return "";
1308 }
1309 return Latex2UnicodeParser.transform(this, latex, maxColumns);
1310 }
1311
1312 /**
1313 * Print text in one line and print another line with = to underline it.
1314 *
1315 * @param text Line to print.
1316 */
1317 private void underlineBig(final String text) {
1318 printer.println(text);
1319 for (int i = 0; i < text.length(); i++) {
1320 printer.print("\u2550");
1321 }
1322 printer.println();
1323 }
1324
1325 /**
1326 * Print text in one line and print another line with = to underline it.
1327 *
1328 * @param text Line to print.
1329 */
1330 private void underline(final String text) {
1331 printer.println(text);
1332 for (int i = 0; i < text.length(); i++) {
1333 printer.print("\u2015");
1334 }
1335 printer.println();
1336 }
1337
1338 public String getReferenceLink(final String reference, final SourcePosition start,
1339 final SourcePosition end) {
1340 final Reference ref = getReference(reference, getCurrentContext(start, end), addWarnings,
1341 false);
1342
1343 if (ref.isNodeLocalReference() && ref.isSubReference()) {
1344 return "(" + ref.getSubLabel() + ")";
1345 }
1346
1347 if (ref.isNodeLocalReference() && ref.isProofLineReference()) {
1348 return "(" + ref.getProofLineLabel() + ")";
1349 }
1350
1351 if (!ref.isExternal()) {
1352 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1353 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1354 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "");
1355 }
1356
1357 // do we have an external module reference without node?
1358 if (ref.isExternalModuleReference()) {
1359 return "[" + ref.getExternalQedeqLabel() + "]";
1360 }
1361
1362 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1363 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1364 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1365 + (ref.isExternal() ? " [" + ref.getExternalQedeqLabel() + "]" : "");
1366 }
1367
1368 private String getNodeDisplay(final String label, final KernelNodeBo kNode) {
1369 return getNodeDisplay(label, kNode, language);
1370 }
1371
1372 }
|