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