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