Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Dez 29 2005 18:38:29 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 756   Methods: 20
NCLOC: 546   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2Latex.java 74,7% 83,6% 100% 81,6%
coverage coverage
 1    /* $Id: Qedeq2Latex.java,v 1.40 2005/12/29 17:31:10 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2005, 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.elli.Element;
 29    import org.qedeq.kernel.base.elli.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.Definition;
 36    import org.qedeq.kernel.base.module.Latex;
 37    import org.qedeq.kernel.base.module.LatexList;
 38    import org.qedeq.kernel.base.module.Node;
 39    import org.qedeq.kernel.base.module.NodeType;
 40    import org.qedeq.kernel.base.module.Proposition;
 41    import org.qedeq.kernel.base.module.Qedeq;
 42    import org.qedeq.kernel.base.module.Rule;
 43    import org.qedeq.kernel.base.module.Section;
 44    import org.qedeq.kernel.base.module.SectionList;
 45    import org.qedeq.kernel.base.module.Subsection;
 46    import org.qedeq.kernel.base.module.SubsectionList;
 47    import org.qedeq.kernel.base.module.SubsectionType;
 48    import org.qedeq.kernel.base.module.VariableList;
 49    import org.qedeq.kernel.bo.control.IllegalModuleDataException;
 50    import org.qedeq.kernel.bo.control.QedeqBoFactory;
 51    import org.qedeq.kernel.dto.module.DefinitionVo;
 52    import org.qedeq.kernel.log.Trace;
 53    import org.qedeq.kernel.utility.ReplaceUtility;
 54   
 55   
 56    /**
 57    * Transfer a qedeq module into a LaTeX file.
 58    * <p>
 59    * <b>TODO mime 20050205: This is just a quick hacked generator. No parsing or validation
 60    * of inline LaTeX text is done. No reference is resolved. This class just
 61    * generates some LaTeX to get some visual impression of a qedeq module
 62    * in an early development stage.</b>
 63    *
 64    * @version $Revision: 1.40 $
 65    * @author Michael Meyling
 66    */
 67    public final class Qedeq2Latex {
 68   
 69    /** Output goes here. */
 70    private PrintStream printer;
 71   
 72    /** Qedeq module to transfer into LaTeX form. */
 73    private Qedeq qedeq;
 74   
 75    /** Filter text to get and produce text in this language. */
 76    private String language;
 77   
 78    /** Filter for this detail level. TODO mime 20050205: not used yet. */
 79    private Object level;
 80   
 81    /** Maps identifiers to {@link Definition}s. */
 82    private Map definitions = new HashMap();
 83   
 84    /**
 85    * Constructor.
 86    *
 87    * @param context Context within this module is created.
 88    * @param qedeq Work with this qedeq module.
 89    * @throws IllegalModuleDataException
 90    */
 91  7 public Qedeq2Latex(final String context, final Qedeq qedeq) throws IllegalModuleDataException {
 92  7 this.qedeq = QedeqBoFactory.createQedeq(context, qedeq);
 93  6 final DefinitionVo definition = new DefinitionVo();
 94    // TODO mime 20050224: quick hack to have the logical identity operator
 95  6 definition.setArgumentNumber("2");
 96  6 definition.setType("PREDCON");
 97  6 definition.setLatexPattern("#1 \\ = \\ #2");
 98  6 definitions.put("equal", definition);
 99    }
 100   
 101    /**
 102    * Prints a LaTeX file into a given output stream.
 103    *
 104    * @param language Filter text to get and produce text in this language only.
 105    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 106    * @param outputStream Write output herein.
 107    * @throws IOException
 108    */
 109  6 public final synchronized void printLatex(final String language, final String level,
 110    final OutputStream outputStream) throws IOException {
 111  6 if (language == null) {
 112  0 this.language = "en";
 113    } else {
 114  6 this.language = language;
 115    }
 116  6 if (level == null) {
 117  0 this.level = "1";
 118    } else {
 119  6 this.level = level;
 120    }
 121  6 this.printer = new PrintStream(outputStream);
 122  6 printLatexHeader();
 123  6 printQedeqHeader();
 124  6 printQedeqChapters();
 125  6 printLatexTrailer();
 126  6 if (printer.checkError()) {
 127  0 throw new IOException("TODO mime: better use another OutputStream");
 128    }
 129    }
 130   
 131    /**
 132    * Prints the header.
 133    */
 134  6 private void printQedeqHeader() {
 135  6 final LatexList title = qedeq.getHeader().getTitle();
 136  6 printer.print("\\title{");
 137  6 printer.print(getLatexListEntry(title));
 138  6 printer.println("}");
 139  6 printer.println("\\author{");
 140  6 final AuthorList authors = qedeq.getHeader().getAuthorList();
 141  6 for (int i = 0; i < authors.size(); i++) {
 142  6 final Author author = authors.get(i);
 143  6 printer.println(author.getName().getLatex());
 144    }
 145  6 printer.println("}");
 146  6 printer.println();
 147  6 printer.println("\\begin{document}");
 148  6 printer.println();
 149  6 printer.println("\\maketitle");
 150  6 printer.println();
 151  6 printer.println("\\setlength{\\parskip}{0pt}");
 152  6 printer.println("\\tableofcontents");
 153  6 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
 154  6 printer.println();
 155    }
 156   
 157    /**
 158    * Print all chapters.
 159    */
 160  6 private void printQedeqChapters() {
 161  6 final ChapterList chapters = qedeq.getChapterList();
 162  6 for (int i = 0; i < chapters.size(); i++) {
 163  22 final Chapter chapter = chapters.get(i);
 164  22 printer.print("\\chapter");
 165  22 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 166  8 printer.print("*");
 167    }
 168  22 printer.print("{");
 169  22 printer.print(getLatexListEntry(chapter.getTitle()));
 170  22 printer.println("} \\label{" + "chapter" + i + "}");
 171  22 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 172  8 printer.println("\\addcontentsline{toc}{chapter}{"
 173    + getLatexListEntry(chapter.getTitle()) + "}");
 174    }
 175  22 printer.println();
 176  22 if (chapter.getIntroduction() != null) {
 177  22 printer.println(getLatexListEntry(chapter.getIntroduction()));
 178  22 printer.println();
 179    }
 180  22 final SectionList sections = chapter.getSectionList();
 181  22 if (sections != null) {
 182  10 printSections(sections);
 183  10 printer.println();
 184    }
 185  22 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 186  22 printer.println();
 187    }
 188    }
 189   
 190    /**
 191    * Print all given sections.
 192    *
 193    * @param sections List of sections.
 194    */
 195  10 private void printSections(final SectionList sections) {
 196  10 if (sections == null) {
 197  0 return;
 198    }
 199  10 for (int i = 0; i < sections.size(); i++) {
 200  20 final Section section = sections.get(i);
 201  20 printer.print("\\section{");
 202  20 printer.print(getLatexListEntry(section.getTitle()));
 203  20 printer.println("} \\label{" + "section" + i + "}");
 204  20 printer.println(getLatexListEntry(section.getIntroduction()));
 205  20 printer.println();
 206  20 printSubsections(section.getSubsectionList());
 207    }
 208    }
 209   
 210    /**
 211    * Print all given subsections.
 212    *
 213    * @param nodes List of subsections.
 214    */
 215  20 private void printSubsections(final SubsectionList nodes) {
 216  20 if (nodes == null) {
 217  12 return;
 218    }
 219  8 for (int i = 0; i < nodes.size(); i++) {
 220  48 final SubsectionType subsectionType = nodes.get(i);
 221  48 if (subsectionType instanceof Node) {
 222  28 final Node node = (Node) subsectionType;
 223  28 printer.println(getLatexListEntry(node.getPrecedingText()));
 224  28 printer.println();
 225  28 printer.println("\\par");
 226  28 final String id = node.getId();
 227  28 final NodeType type = node.getNodeType();
 228  28 String title = null;
 229  28 if (node.getTitle() != null) {
 230  18 title = getLatexListEntry(node.getTitle());
 231    }
 232  28 if (type instanceof Axiom) {
 233  6 printAxiom((Axiom) type, title, id);
 234  22 } else if (type instanceof Definition) {
 235  10 printDefinition((Definition) type, title, id);
 236  12 } else if (type instanceof Proposition) {
 237  10 printProposition((Proposition) type, title, id);
 238  2 } else if (type instanceof Rule) {
 239  2 printRule((Rule) type, title, id);
 240    } else {
 241  0 throw new RuntimeException((type != null ? "unknown type: "
 242    + type.getClass().getName() : "node type empty"));
 243    }
 244  28 printer.println();
 245  28 printer.println(getLatexListEntry(node.getSucceedingText()));
 246    } else {
 247  20 printer.print("\\subsection{");
 248  20 final Subsection subsection = (Subsection) subsectionType;
 249  20 printer.println(getLatexListEntry(subsection.getTitle()));
 250  20 printer.println("}");
 251  20 printer.println(getLatexListEntry(subsection.getLatex()));
 252    }
 253  48 printer.println();
 254  48 printer.println();
 255    }
 256    }
 257   
 258    /**
 259    * Print axiom.
 260    *
 261    * @param axiom Print this.
 262    * @param title Extra name.
 263    * @param id Label for marking this axiom.
 264    */
 265  6 private void printAxiom(final Axiom axiom, final String title, final String id) {
 266  6 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
 267  6 printer.println("\\label{" + id + "}");
 268  6 printFormula(axiom.getFormula().getElement());
 269  6 printer.println(getLatexListEntry(axiom.getDescription()));
 270  6 printer.println("\\end{ax}");
 271    }
 272   
 273    /**
 274    * Print formula.
 275    *
 276    * @param element Formula to print.
 277    */
 278  16 private void printFormula(final Element element) {
 279  16 printer.println("\\mbox{}");
 280  16 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
 281  16 printer.println("$" + getLatex(element) + "$");
 282  16 printer.println("\\end{longtable}");
 283    }
 284   
 285    /**
 286    * Print definition.
 287    *
 288    * @param definition Print this.
 289    * @param title Extra name.
 290    * @param id Label for marking this definition.
 291    */
 292  10 private void printDefinition(final Definition definition, final String title,
 293    final String id) {
 294  10 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 295  10 final VariableList list = definition.getVariableList();
 296  10 if (list != null) {
 297  10 for (int i = list.size() - 1; i >= 0; i--) {
 298  16 Trace.trace(this, "printDefinition", "replacing!");
 299  16 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 300    }
 301    }
 302  10 if (definition.getFormulaOrTerm() != null) {
 303  6 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 304  6 printer.println("\\label{" + id + "}");
 305  6 define.append("\\ := \\ ");
 306  6 define.append(getLatex(definition.getFormulaOrTerm().getElement()));
 307    } else {
 308  4 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 309  4 printer.println("\\label{" + id + "}");
 310    }
 311  10 define.append("$$");
 312  10 definitions.put(id, definition);
 313  10 Trace.traceParam(this, "printDefinition", "define", define);
 314  10 printer.println(define);
 315  10 printer.println(getLatexListEntry(definition.getDescription()));
 316  10 if (definition.getFormulaOrTerm() != null) {
 317  6 printer.println("\\end{defn}");
 318    } else {
 319  4 printer.println("\\end{idefn}");
 320    }
 321    }
 322   
 323    /**
 324    * Print proposition.
 325    *
 326    * @param proposition Print this.
 327    * @param title Extra name.
 328    * @param id Label for marking this proposition.
 329    */
 330  10 private void printProposition(final Proposition proposition, final String title,
 331    final String id) {
 332  10 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
 333  10 printer.println("\\label{" + id + "}");
 334  10 printFormula(proposition.getFormula().getElement());
 335  10 printer.println(getLatexListEntry(proposition.getDescription()));
 336  10 printer.println("\\end{prop}");
 337  10 if (proposition.getProofList() != null) {
 338  10 for (int i = 0; i < proposition.getProofList().size(); i++) {
 339  10 printer.println("\\begin{proof}");
 340  10 printer.println(getLatexListEntry(proposition.getProofList().get(i)
 341    .getNonFormalProof()));
 342  10 printer.println("\\end{proof}");
 343    }
 344    }
 345    }
 346   
 347    /**
 348    * Print rule declaration.
 349    *
 350    * @param rule Print this.
 351    * @param title Extra name.
 352    * @param id Label for marking this proposition.
 353    */
 354  2 private void printRule(final Rule rule, final String title,
 355    final String id) {
 356  2 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
 357  2 printer.println("\\label{" + id + "}");
 358  2 printer.println(getLatexListEntry(rule.getDescription()));
 359  2 printer.println("\\end{rul}");
 360   
 361    // TODO mime 20051210: are these informations equivalent to a formal proof?
 362    /*
 363    if (null != rule.getLinkList()) {
 364    printer.println("\\begin{proof}");
 365    printer.println("Rule name: " + rule.getName());
 366    printer.println();
 367    printer.println();
 368    for (int i = 0; i < rule.getLinkList().size(); i++) {
 369    printer.println(rule.getLinkList().get(i));
 370    }
 371    printer.println("\\end{proof}");
 372    }
 373    */
 374  2 if (rule.getProofList() != null) {
 375  0 for (int i = 0; i < rule.getProofList().size(); i++) {
 376  0 printer.println("\\begin{proof}");
 377  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
 378    .getNonFormalProof()));
 379  0 printer.println("\\end{proof}");
 380    }
 381    }
 382    }
 383   
 384    /**
 385    * Get LaTeX element presentation.
 386    *
 387    * @param element Print this element.
 388    * @return LaTeX form of element.
 389    */
 390  38 private String getLatex(final Element element) {
 391  38 return getLatex(element, true);
 392    }
 393   
 394    /**
 395    * Get LaTeX element presentation.
 396    *
 397    * @param element Print this element.
 398    * @param first First level?
 399    * @return LaTeX form of element.
 400    */
 401  444 private String getLatex(final Element element, final boolean first) {
 402  444 final StringBuffer buffer = new StringBuffer();
 403  444 if (element.isAtom()) {
 404  0 return element.getAtom().getString();
 405    }
 406  444 final ElementList list = element.getList();
 407  444 if (list.getOperator().equals("PREDCON")) {
 408  78 final String identifier = list.getElement(0).getAtom().getString();
 409  78 if (definitions.containsKey(identifier)) {
 410  78 final Definition definition = (Definition) definitions.get(identifier);
 411  78 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 412  78 for (int i = list.size() - 1; i >= 1; i--) {
 413  146 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 414    }
 415  78 buffer.append(define);
 416    } else {
 417  0 buffer.append(identifier);
 418  0 buffer.append("(");
 419  0 for (int i = 1; i < list.size(); i++) {
 420  0 buffer.append(getLatex(list.getElement(i), false));
 421  0 if (i + 1 < list.size()) {
 422  0 buffer.append(", ");
 423    }
 424    }
 425  0 buffer.append(")");
 426    }
 427  366 } else if (list.getOperator().equals("PREDVAR")) {
 428  32 final String identifier = list.getElement(0).getAtom().getString();
 429  32 buffer.append(identifier);
 430  32 buffer.append("(");
 431  32 for (int i = 1; i < list.size(); i++) {
 432  32 buffer.append(getLatex(list.getElement(i), false));
 433  32 if (i + 1 < list.size()) {
 434  0 buffer.append(", ");
 435    }
 436    }
 437  32 buffer.append(")");
 438  334