Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Jan 11 2007 09:03:50 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 919   Methods: 22
NCLOC: 695   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2Latex.java 67,3% 77,4% 100% 74,9%
coverage coverage
 1    /* $Id: Qedeq2Latex.java,v 1.41 2006/10/20 20:23:08 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2006, Michael Meyling <mime@qedeq.org>.
 6    *
 7    * "Hilbert II" is free software; you can redistribute
 8    * it and/or modify it under the terms of the GNU General Public
 9    * License as published by the Free Software Foundation; either
 10    * version 2 of the License, or (at your option) any later version.
 11    *
 12    * This program is distributed in the hope that it will be useful,
 13    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 14    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 15    * GNU General Public License for more details.
 16    */
 17   
 18    package org.qedeq.kernel.latex;
 19   
 20    import java.io.IOException;
 21    import java.io.OutputStream;
 22    import java.io.PrintStream;
 23    import java.text.SimpleDateFormat;
 24    import java.util.Date;
 25    import java.util.HashMap;
 26    import java.util.Map;
 27   
 28    import org.qedeq.kernel.base.list.Element;
 29    import org.qedeq.kernel.base.list.ElementList;
 30    import org.qedeq.kernel.base.module.Author;
 31    import org.qedeq.kernel.base.module.AuthorList;
 32    import org.qedeq.kernel.base.module.Axiom;
 33    import org.qedeq.kernel.base.module.Chapter;
 34    import org.qedeq.kernel.base.module.ChapterList;
 35    import org.qedeq.kernel.base.module.FunctionDefinition;
 36    import org.qedeq.kernel.base.module.Latex;
 37    import org.qedeq.kernel.base.module.LatexList;
 38    import org.qedeq.kernel.base.module.LiteratureItem;
 39    import org.qedeq.kernel.base.module.LiteratureItemList;
 40    import org.qedeq.kernel.base.module.Node;
 41    import org.qedeq.kernel.base.module.NodeType;
 42    import org.qedeq.kernel.base.module.PredicateDefinition;
 43    import org.qedeq.kernel.base.module.Proposition;
 44    import org.qedeq.kernel.base.module.Qedeq;
 45    import org.qedeq.kernel.base.module.Rule;
 46    import org.qedeq.kernel.base.module.Section;
 47    import org.qedeq.kernel.base.module.SectionList;
 48    import org.qedeq.kernel.base.module.Subsection;
 49    import org.qedeq.kernel.base.module.SubsectionList;
 50    import org.qedeq.kernel.base.module.SubsectionType;
 51    import org.qedeq.kernel.base.module.VariableList;
 52    import org.qedeq.kernel.bo.control.QedeqBoFactory;
 53    import org.qedeq.kernel.bo.module.ModuleDataException;
 54    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 55    import org.qedeq.kernel.log.Trace;
 56    import org.qedeq.kernel.utility.IoUtility;
 57    import org.qedeq.kernel.utility.ReplaceUtility;
 58   
 59   
 60    /**
 61    * Transfer a qedeq module into a LaTeX file.
 62    * <p>
 63    * <b>TODO mime 20050205: This is just a quick hacked generator. No parsing or validation
 64    * of inline LaTeX text is done. No reference is resolved. This class just
 65    * generates some LaTeX to get some visual impression of a QEDEQ module
 66    * in an early development stage.</b>
 67    * <p>
 68    * This generator operates operates against the interface declaration of a QEDEQ module.
 69    * No business object is required.
 70    *
 71    * @version $Revision: 1.41 $
 72    * @author Michael Meyling
 73    */
 74    public final class Qedeq2Latex {
 75   
 76    /** Alphabet for tagging. */
 77    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
 78   
 79    /** Output goes here. */
 80    private PrintStream printer;
 81   
 82    /** Qedeq module to transfer into LaTeX form. */
 83    private Qedeq qedeq;
 84   
 85    /** Filter text to get and produce text in this language. */
 86    private String language;
 87   
 88    /** Filter for this detail level. TODO mime 20050205: not used yet. */
 89    private Object level;
 90   
 91    /** Maps identifiers to {@link PredicateDefinition}s. */ // FIXME mime 20070102: also for Function Definitions!!!
 92    private Map definitions = new HashMap();
 93   
 94    /**
 95    * Constructor.
 96    *
 97    * @param context Context within this module is created.
 98    * @param qedeq Work with this qedeq module.
 99    * @throws ModuleDataException
 100    */
 101  11 public Qedeq2Latex(final String context, final Qedeq qedeq) throws ModuleDataException {
 102    // although we work against the interfaces we create an BO just for testing purposes
 103  11 this.qedeq = QedeqBoFactory.createQedeq(context, qedeq);
 104  10 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 105    // TODO mime 20050224: quick hack to have the logical identity operator
 106  10 equal.setArgumentNumber("2");
 107  10 equal.setName("equal");
 108  10 equal.setLatexPattern("#1 \\ = \\ #2");
 109  10 definitions.put("equal_2", equal);
 110    // TODO mime 20060822: quick hack to get the negation of the logical identity operator
 111  10 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 112  10 notEqual.setArgumentNumber("2");
 113  10 notEqual.setName("notEqual");
 114  10 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 115  10 definitions.put("notEqual_2", notEqual);
 116    }
 117   
 118    /**
 119    * Prints a LaTeX file into a given output stream.
 120    *
 121    * @param language Filter text to get and produce text in this language only.
 122    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 123    * @param outputStream Write output herein.
 124    * @throws IOException
 125    */
 126  10 public final synchronized void printLatex(final String language, final String level,
 127    final OutputStream outputStream) throws IOException {
 128  10 if (language == null) {
 129  0 this.language = "en";
 130    } else {
 131  10 this.language = language;
 132    }
 133  10 if (level == null) {
 134  0 this.level = "1";
 135    } else {
 136  10 this.level = level;
 137    }
 138  10 this.printer = new PrintStream(outputStream);
 139  10 printLatexHeader();
 140  10 printQedeqHeader();
 141  10 printQedeqChapters();
 142  10 printQedeqBibliography();
 143  10 printLatexTrailer();
 144  10 if (printer.checkError()) {
 145  0 throw new IOException("TODO mime: better use another OutputStream");
 146    }
 147    }
 148   
 149    /**
 150    * Prints the header.
 151    */
 152  10 private void printQedeqHeader() {
 153  10 final LatexList title = qedeq.getHeader().getTitle();
 154  10 printer.print("\\title{");
 155  10 printer.print(getLatexListEntry(title));
 156  10 printer.println("}");
 157  10 printer.println("\\author{");
 158  10 final AuthorList authors = qedeq.getHeader().getAuthorList();
 159  10 for (int i = 0; i < authors.size(); i++) {
 160  10 final Author author = authors.get(i);
 161  10 printer.println(author.getName().getLatex());
 162    }
 163  10 printer.println("}");
 164  10 printer.println();
 165  10 printer.println("\\begin{document}");
 166  10 printer.println();
 167  10 printer.println("\\maketitle");
 168  10 printer.println();
 169  10 printer.println("\\setlength{\\parskip}{0pt}");
 170  10 printer.println("\\tableofcontents");
 171  10 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
 172  10 printer.println();
 173    }
 174   
 175    /**
 176    * Print all chapters.
 177    */
 178  10 private void printQedeqChapters() {
 179  10 final ChapterList chapters = qedeq.getChapterList();
 180  10 for (int i = 0; i < chapters.size(); i++) {
 181  50 final Chapter chapter = chapters.get(i);
 182  50 printer.print("\\chapter");
 183  50 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 184  16 printer.print("*");
 185    }
 186  50 printer.print("{");
 187  50 printer.print(getLatexListEntry(chapter.getTitle()));
 188  50 final String label = "chapter" + i;
 189  50 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 190  50 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 191  16 printer.println("\\addcontentsline{toc}{chapter}{"
 192    + getLatexListEntry(chapter.getTitle()) + "}");
 193    }
 194  50 printer.println();
 195  50 if (chapter.getIntroduction() != null) {
 196  50 printer.println(getLatexListEntry(chapter.getIntroduction()));
 197  50 printer.println();
 198    }
 199  50 final SectionList sections = chapter.getSectionList();
 200  50 if (sections != null) {
 201  28 printSections(i, sections);
 202  28 printer.println();
 203    }
 204  50 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 205  50 printer.println();
 206    }
 207    }
 208   
 209    /**
 210    * Print bibliography (if any).
 211    */
 212  10 private void printQedeqBibliography() {
 213  10 final LiteratureItemList items = qedeq.getLiteratureItemList();
 214  10 if (items == null) {
 215  6 return;
 216    }
 217  4 printer.println("\\begin{thebibliography}{99}");
 218  4 for (int i = 0; i < items.size(); i++) {
 219  18 final LiteratureItem item = items.get(i);
 220  18 printer.print("\\bibitem{" + item.getLabel() + "} ");
 221  18 printer.println(getLatexListEntry(item.getItem()));
 222  18 printer.println();
 223    }
 224  4 printer.println("\\end{thebibliography}");
 225    // TODO mime 20060926: remove language dependency
 226  4 if ("de".equals(language)) {
 227  2 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
 228    } else {
 229  2 printer.println("\\addcontentsline{toc}{chapter}{Bibliography}");
 230    }
 231   
 232    }
 233   
 234    /**
 235    * Print all given sections.
 236    *
 237    * @param chapter Chapter number.
 238    * @param sections List of sections.
 239    */
 240  28 private void printSections(final int chapter, final SectionList sections) {
 241  28 if (sections == null) {
 242  0 return;
 243    }
 244  28 for (int i = 0; i < sections.size(); i++) {
 245  84 final Section section = sections.get(i);
 246  84 printer.print("\\section{");
 247  84 printer.print(getLatexListEntry(section.getTitle()));
 248  84 final String label = "chapter" + chapter + "_section" + i;
 249  84 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 250  84 printer.println(getLatexListEntry(section.getIntroduction()));
 251  84 printer.println();
 252  84 printSubsections(section.getSubsectionList());
 253    }
 254    }
 255   
 256    /**
 257    * Print all given subsections.
 258    *
 259    * @param nodes List of subsections.
 260    */
 261  84 private void printSubsections(final SubsectionList nodes) {
 262  84 if (nodes == null) {
 263  44 return;
 264    }
 265  40 for (int i = 0; i < nodes.size(); i++) {
 266  248 final SubsectionType subsectionType = nodes.get(i);
 267  248 if (subsectionType instanceof Node) {
 268  200 final Node node = (Node) subsectionType;
 269  200 printer.println("\\par");
 270  200 printer.println(getLatexListEntry(node.getPrecedingText()));
 271  200 printer.println();
 272  200 final String id = node.getId();
 273  200 final NodeType type = node.getNodeType();
 274  200 String title = null;
 275  200 if (node.getTitle() != null) {
 276  92 title = getLatexListEntry(node.getTitle());
 277    }
 278  200 if (type instanceof Axiom) {
 279  32 printAxiom((Axiom) type, title, id);
 280  168 } else if (type instanceof PredicateDefinition) {
 281  24 printPredicateDefinition((PredicateDefinition) type, title, id);
 282  144 } else if (type instanceof FunctionDefinition) {
 283  32 printFunctionDefinition((FunctionDefinition) type, title, id);
 284  112 } else if (type instanceof Proposition) {
 285  108 printProposition((Proposition) type, title, id);
 286  4 } else if (type instanceof Rule) {
 287  4 printRule((Rule) type, title, id);
 288    } else {
 289  0 throw new RuntimeException((type != null ? "unknown type: "
 290    + type.getClass().getName() : "node type empty"));
 291    }
 292  200 printer.println();
 293  200 printer.println(getLatexListEntry(node.getSucceedingText()));
 294    } else {
 295  48 final Subsection subsection = (Subsection) subsectionType;
 296  48 if (subsection.getTitle() != null) {
 297  42 printer.print("\\subsection{");
 298  42 printer.println(getLatexListEntry(subsection.getTitle()));
 299  42 printer.println("}");
 300    }
 301  48 printer.println(getLatexListEntry(subsection.getLatex()));
 302    }
 303  248 printer.println();
 304  248 printer.println();
 305    }
 306    }
 307   
 308    /**
 309    * Print axiom.
 310    *
 311    * @param axiom Print this.
 312    * @param title Extra name.
 313    * @param id Label for marking this axiom.
 314    */
 315  32 private void printAxiom(final Axiom axiom, final String title, final String id) {
 316  32 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
 317  32 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 318  32 printFormula(axiom.getFormula().getElement());
 319  32 printer.println(getLatexListEntry(axiom.getDescription()));
 320  32 printer.println("\\end{ax}");
 321    }
 322   
 323    /**
 324    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
 325    * formula is broken down in several labeled lines.
 326    *
 327    * @param element Formula to print.
 328    * @param mainLabel Main formula label.
 329    */
 330  108 private void printTopFormula(final Element element, final String mainLabel) {
 331  108 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
 332  76 printFormula(element);
 333  76 return;
 334    }
 335  32 final ElementList list = element.getList();
 336  32 printer.println("\\mbox{}");
 337  32 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
 338  32 for (int i = 0; i < list.size(); i++) {
 339  158 final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
 340  158 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
 341    + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
 342    + label + "}{} \\mbox{\\emph{(" + label + ")}} "
 343  158 + (i + 1 < list.size() ? "\\\\" : ""));
 344    }
 345  32 printer.println("\\end{longtable}");
 346    }
 347   
 348    /**
 349    * Print formula.
 350    *
 351    * @param element Formula to print.
 352    */
 353  108 private void printFormula(final Element element) {
 354  108 printer.println("\\mbox{}");
 355  108 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
 356  108 printer.println("\\centering $" + getLatex(element) + "$");
 357  108 printer.println("\\end{longtable}");
 358    }
 359   
 360    /**
 361    * Print predicate definition.
 362    *
 363    * @param definition Print this.
 364    * @param title Extra name.
 365    * @param id Label for marking this definition.
 366    */
 367  24 private void printPredicateDefinition(final PredicateDefinition definition, final String title,
 368    final String id) {
 369  24 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 370  24 final VariableList list = definition.getVariableList();
 371  24 if (list != null) {
 372  24 for (int i = list.size() - 1; i >= 0; i--) {
 373  38 Trace.trace(this, "printPredicateDefinition", "replacing!");
 374  38 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 375    }
 376    }
 377  24 if (definition.getFormula() != null) {
 378  20 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 379  20 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 380  20 define.append("\\ :\\leftrightarrow \\ ");
 381  20 define.append(getLatex(definition.getFormula().getElement()));
 382    } else {
 383  4 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 384  4 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 385    }
 386  24 define.append("$$");
 387  24 definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
 388  24 Trace.param(this, "printPredicateDefinition", "define", define);
 389  24 printer.println(define);
 390  24 printer.println(getLatexListEntry(definition.getDescription()));
 391  24 if (definition.getFormula() != null) {
 392  20 printer.println("\\end{defn}");
 393    } else {
 394  4 printer.println("\\end{idefn}");
 395    }
 396    }
 397   
 398    /**
 399    * Print function definition.
 400    *
 401    * @param definition Print this.
 402    * @param title Extra name.
 403    * @param id Label for marking this definition.
 404    */
 405  32 private void printFunctionDefinition(final FunctionDefinition definition, final String title,
 406    final String id) {
 407  32 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 408  32 final VariableList list = definition.getVariableList();
 409  32 if (list != null) {
 410  26 for (int i = list.size() - 1; i >= 0; i--) {
 411  36 Trace.trace(this, "printFunctionDefinition", "replacing!");
 412  36 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 413    }
 414    }
 415  32 if (definition.getTerm() != null) {
 416  32 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 417  32 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 418  32 define.append("\\ := \\ ");
 419  32 define.append(getLatex(definition.getTerm().getElement()));
 420    } else {
 421  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 422  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 423    }
 424  32 define.append("$$");
 425  32 definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
 426  32 Trace.param(this, "printFunctionDefinition", "define", define);
 427  32 printer.println(define);
 428  32 printer.println(getLatexListEntry(definition.getDescription()));