Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Mrz 27 2008 21:46:26 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 600   Methods: 23
NCLOC: 400   Classes: 15
 
 Source file Conditionals Statements Methods TOTAL
Element2Latex.java 56,2% 65,9% 82,6% 64,4%
coverage coverage
 1    /* $Id: Element2Latex.java,v 1.2 2008/03/27 05:16:25 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2008, 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.util.HashMap;
 21    import java.util.Map;
 22   
 23    import org.qedeq.kernel.base.list.Element;
 24    import org.qedeq.kernel.base.list.ElementList;
 25    import org.qedeq.kernel.base.module.FunctionDefinition;
 26    import org.qedeq.kernel.base.module.PredicateDefinition;
 27    import org.qedeq.kernel.bo.control.KernelQedeqBo;
 28    import org.qedeq.kernel.bo.logic.DefaultExistenceChecker;
 29    import org.qedeq.kernel.bo.logic.ExistenceChecker;
 30    import org.qedeq.kernel.bo.visitor.AbstractModuleVisitor;
 31    import org.qedeq.kernel.common.ModuleReferenceList;
 32    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 33    import org.qedeq.kernel.utility.StringUtility;
 34   
 35   
 36    /**
 37    * Transfer a QEDEQ formulas into LaTeX text.
 38    *
 39    * @version $Revision: 1.2 $
 40    * @author Michael Meyling
 41    */
 42    public final class Element2Latex extends AbstractModuleVisitor {
 43   
 44    /** External QEDEQ module references. */
 45    private final ModuleReferenceList references;
 46   
 47    /** Maps identifiers to {@link PredicateDefinition}s. */
 48    private final Map predicateDefinitions = new HashMap();
 49   
 50    /** Maps identifiers to {@link FunctionDefinition}s. */
 51    private final Map functionDefinitions = new HashMap();
 52   
 53    /** Maps operator strings to {@link ElementList} to LaTeX mappers. */
 54    private final Map elementList2ListType = new HashMap();
 55   
 56    /** For mapping an unknown operator. */
 57    private final ListType unknown = new Unknown();
 58   
 59    /**
 60    * Constructor.
 61    *
 62    * @param references External QEDEQ module references.
 63    */
 64  28 public Element2Latex(final ModuleReferenceList references) {
 65  28 this.references = references;
 66   
 67  28 this.elementList2ListType.put("PREDVAR", new Predvar());
 68  28 this.elementList2ListType.put("FUNVAR", new Funvar());
 69  28 this.elementList2ListType.put("PREDCON", new Predcon());
 70  28 this.elementList2ListType.put("FUNCON", new Funcon());
 71  28 this.elementList2ListType.put("VAR", new Var());
 72   
 73  28 this.elementList2ListType.put("AND", new BinaryLogical("\\land"));
 74  28 this.elementList2ListType.put("OR", new BinaryLogical("\\lor"));
 75  28 this.elementList2ListType.put("IMPL", new BinaryLogical("\\rightarrow"));
 76  28 this.elementList2ListType.put("EQUI", new BinaryLogical("\\leftrightarrow"));
 77   
 78  28 this.elementList2ListType.put("FORALL", new Quantifier("\\forall"));
 79  28 this.elementList2ListType.put("EXISTS", new Quantifier("\\exists"));
 80  28 this.elementList2ListType.put("EXISTSU", new Quantifier("\\exists!"));
 81   
 82  28 this.elementList2ListType.put("NOT", new Not());
 83  28 this.elementList2ListType.put("CLASS", new Class());
 84  28 this.elementList2ListType.put("CLASSLIST", new Classlist());
 85   
 86    // TODO mime 20080126: wrong spelled and not used any longer (?)
 87  28 this.elementList2ListType.put("QUANTOR_INTERSECTION", new QuantorIntersection());
 88  28 this.elementList2ListType.put("QUANTOR_UNION", new QuantorUnion());
 89   
 90    // quick hack to have the logical identity operator
 91  28 final String nameEqual = ExistenceChecker.NAME_EQUAL;
 92  28 final String argNumberEqual = "2";
 93  28 final String keyEqual = nameEqual + "_" + argNumberEqual;
 94  28 if (!getPredicateDefinitions().containsKey(keyEqual)) {
 95  28 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 96  28 equal.setArgumentNumber(argNumberEqual);
 97  28 equal.setName(nameEqual);
 98  28 equal.setLatexPattern("#1 \\ = \\ #2");
 99  28 getPredicateDefinitions().put(keyEqual, equal);
 100    }
 101   
 102    // LATER mime 20080107: quick hack to get the negation of the logical identity operator
 103  28 final String nameNotEqual = "notEqual";
 104  28 final String argNumberNotEqual = "2";
 105  28 final String keyNotEqual = nameNotEqual + "_" + argNumberNotEqual;
 106  28 if (!getPredicateDefinitions().containsKey(keyNotEqual)) {
 107  28 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 108  28 notEqual.setArgumentNumber("2");
 109  28 notEqual.setName("notEqual");
 110  28 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 111  28 getPredicateDefinitions().put(keyNotEqual, notEqual);
 112    }
 113    }
 114   
 115    /**
 116    * Add predicate definition. If such a definition already exists it is overwritten.
 117    *
 118    * @param definition Definition to add.
 119    */
 120  92 public void addPredicate(final PredicateDefinition definition) {
 121  92 getPredicateDefinitions().put(definition.getName() + "_" + definition.getArgumentNumber(),
 122    definition);
 123    }
 124   
 125    /**
 126    * Add function definition. If such a definition already exists it is overwritten.
 127    *
 128    * @param definition Definition to add.
 129    */
 130  64 public void addFunction(final FunctionDefinition definition) {
 131  64 getFunctionDefinitions().put(definition.getName() + "_" + definition.getArgumentNumber(),
 132    definition);
 133    }
 134   
 135    /**
 136    * Get LaTeX element presentation.
 137    *
 138    * @param element Print this element.
 139    * @return LaTeX form of element.
 140    */
 141  1141 public String getLatex(final Element element) {
 142  1141 return getLatex(element, true);
 143    }
 144   
 145    /**
 146    * Get LaTeX element presentation.
 147    *
 148    * @param element Print this element.
 149    * @param first First level?
 150    * @return LaTeX form of element.
 151    */
 152  8699 String getLatex(final Element element, final boolean first) {
 153  8699 if (element.isAtom()) {
 154  0 return element.getAtom().getString();
 155    }
 156  8699 final ElementList list = element.getList();
 157   
 158  8699 ListType converter = (ListType) elementList2ListType.get(list.getOperator());
 159   
 160  8699 if (converter == null) {
 161  0 converter = this.unknown;
 162    }
 163  8699 return converter.getLatex(list, first);
 164   
 165    }
 166   
 167    /**
 168    * Get list of external QEDEQ module references.
 169    *
 170    * @return External QEDEQ module references.
 171    */
 172  1080 ModuleReferenceList getReferences() {
 173  1080 return this.references;
 174    }
 175   
 176    /**
 177    * Get mapping of predicate definitions.
 178    *
 179    * @return Mapping of predicate definitions.
 180    */
 181  1606 Map getPredicateDefinitions() {
 182  1606 return this.predicateDefinitions;
 183    }
 184   
 185    /**
 186    * Get mapping of function definitions.
 187    *
 188    * @return Mapping of function definitions.
 189    */
 190  1024 Map getFunctionDefinitions() {
 191  1024 return this.functionDefinitions;
 192    }
 193   
 194    /**
 195    * Describes the interface for an {@link ElementList} to LaTeX converter.
 196    */
 197    interface ListType {
 198   
 199    /**
 200    * Transform list into LaTeX.
 201    *
 202    * @param list This list shall be transformed.
 203    * @param first Is the resulting LaTeX formula or term at top level? If so we possibly
 204    * can omit some brackets.
 205    * @return LaTeX formula or term.
 206    */
 207    public String getLatex(ElementList list, boolean first);
 208    }
 209   
 210    /**
 211    * Transformer for a predicate variable.
 212    */
 213    class Predvar implements ListType {
 214  938 public String getLatex(final ElementList list, final boolean first) {
 215  938 final StringBuffer buffer = new StringBuffer();
 216  938 final String identifier = list.getElement(0).getAtom().getString();
 217  938 buffer.append(identifier);
 218  938 if (list.size() > 1) {
 219  302 buffer.append("(");
 220  302 for (int i = 1; i < list.size(); i++) {
 221  318 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 222  318 if (i + 1 < list.size()) {
 223  16 buffer.append(", ");
 224    }
 225    }
 226  302 buffer.append(")");
 227    }
 228  938 return buffer.toString();
 229    }
 230    }
 231   
 232    /**
 233    * Transformer for a function variable.
 234    */
 235    class Funvar implements ListType {
 236  8 public String getLatex(final ElementList list, final boolean first) {
 237  8 final StringBuffer buffer = new StringBuffer();
 238  8 final String identifier = list.getElement(0).getAtom().getString();
 239  8 buffer.append(identifier);
 240  8 if (list.size() > 1) {
 241  8 buffer.append("(");
 242  8 for (int i = 1; i < list.size(); i++) {
 243  8 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 244  8 if (i + 1 < list.size()) {
 245  0 buffer.append(", ");
 246    }
 247    }
 248  8 buffer.append(")");
 249    }
 250  8 return buffer.toString();
 251    }
 252    }
 253   
 254    /**
 255    * Transformer for a predicate constant.
 256    */
 257    class Predcon implements ListType {
 258  1402 public String getLatex(final ElementList list, final boolean first) {
 259  1402 final StringBuffer buffer = new StringBuffer();
 260  1402 final String name = list.getElement(0).getAtom().getString();
 261  1402 final int arguments = list.size() - 1;
 262  1402 final String identifier = name + "_" + (arguments);
 263    // TODO mime 20060922: is only working for definition name + argument number
 264    // if argument length is dynamic this dosen't work
 265  1402 PredicateDefinition definition = (PredicateDefinition)
 266    Element2Latex.this.getPredicateDefinitions().get(identifier);
 267  1402 if (definition == null) {
 268    // try external modules
 269  362 try {
 270  362 final int external = name.indexOf(".");
 271  362 if (external >= 0 && Element2Latex.this.getReferences() != null
 272    && Element2Latex.this.getReferences().size() > 0) {
 273  360 final String label = name.substring(0, external);
 274  360 final KernelQedeqBo newProp = (KernelQedeqBo)
 275    Element2Latex.this.getReferences().getQedeqBo(label);
 276  360 if (newProp != null) {
 277  360 final String shortName = name.substring(external + 1);
 278  360 if (newProp.getExistenceChecker().predicateExists(shortName,
 279    arguments)) {
 280    // FIXME mime 20080120: Quick and very dirty!
 281  360 DefaultExistenceChecker checker = (DefaultExistenceChecker)
 282    newProp.getExistenceChecker();
 283  360 definition = checker.getPredicate(shortName, arguments);
 284    }
 285    }
 286    }
 287    } catch (Exception e) {
 288    // try failed...
 289    }
 290    }
 291  1402 if (definition != null) {
 292  1400 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 293  1400 for (int i = list.size() - 1; i >= 1; i--) {
 294  2298 StringUtility.replace(define, "#" + i, Element2Latex.this.getLatex(
 295    list.getElement(i), false));
 296    }
 297  1400 buffer.append(define);
 298    } else {
 299  2 buffer.append(identifier);
 300  2 buffer.append("(");
 301  2 for (int i = 1; i < list.size(); i++) {
 302  4 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 303  4 if (i + 1 < list.size()) {
 304  2 buffer.append(", ");
 305    }
 306    }
 307  2 buffer.append(")");
 308    }
 309  1402 return buffer.toString();
 310    }
 311    }
 312   
 313    /**
 314    * Transformer for a function constant.
 315    */
 316    class Funcon implements ListType {
 317   
 318  960 public String getLatex(final ElementList list, final boolean first) {
 319  960 final StringBuffer buffer = new StringBuffer();
 320  960 final String name = list.getElement(0).getAtom().getString();
 321  960 final int arguments = list.size() - 1;
 322  960 final String identifier = name + "_" + (arguments);
 323    // TODO mime 20060922: is only working for definition name + argument number
 324    // if argument length is dynamic this dosen't work
 325  960 FunctionDefinition definition = (FunctionDefinition)
 326    Element2Latex.this.getFunctionDefinitions().get(identifier);
 327  960 if (definition == null) {
 328    // try external modules
 329  0 try {
 330  0 final int external = name.indexOf(".");
 331  0 if (external >= 0 && Element2Latex.this.getReferences() != null
 332    && Element2Latex.this.getReferences().size() > 0) {
 333  0 final String label = name.substring(0, external);
 334  0 final KernelQedeqBo newProp = (KernelQedeqBo)
 335    Element2Latex.this.getReferences().getQedeqBo(label);
 336  0 if (newProp != null) {
 337  0 final String shortName = name.substring(external + 1);
 338  0 if (newProp.getExistenceChecker().functionExists(shortName,
 339    arguments)) {
 340    // FIXME mime 20080120: Quick and very dirty!
 341  0 DefaultExistenceChecker checker = (DefaultExistenceChecker)
 342    newProp.getExistenceChecker();
 343  0 definition = checker.getFunction(shortName, arguments);
 344    }
 345    }
 346    }
 347    } catch (Exception e) {
 348    // try failed...
 349    }
 350    }
 351  960 if (definition != null) {
 352  960 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 353  960 for (int i = list.size() - 1; i >= 1; i--) {
 354  1132 StringUtility.replace(define, "#" + i, Element2Latex.this.
 355    getLatex(list.getElement(i), false));
 356    }
 357  960 buffer.append(define);
 358    } else {
 359  0 buffer.append(identifier);
 360  0 buffer.append("(");
 361  0 for (int i = 1; i < list.size(); i++) {
 362  0 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 363  0 if (i + 1 < list.size()) {
 364  0 buffer.append(", ");
 365    }
 366    }
 367  0 buffer.append(")");
 368    }
 369  960 return buffer.toString();
 370    }
 371    }
 372   
 373    /**
 374    * Transformer for a subject variable.
 375    */
 376    class Var implements ListType {
 377  3432 public String getLatex(final ElementList list, final boolean first) {
 378  3432 final String text = list.getElement(0).getAtom().getString();
 379    // interpret variable identifier as number
 380  3432 try {
 381  3432 final int index = Integer.parseInt(text);
 382  0 final String newText = "" + index;
 383  0 if (!text.equals(newText) || newText.startsWith("-")) {
 384  0 throw new NumberFormatException("This is no allowed number: " + text);
 385    }
 386  0 switch (index) {
 387  0 case 1:
 388  0 return "x";
 389  0 case 2:
 390  0 return "y";
 391  0 case 3:
 392  0 return "z";
 393  0 case 4:
 394  0 return "u";
 395  0 case 5:
 396  0 return "v";
 397  0 case 6:
 398  0 return "w";
 399  0 default:
 400  0 return "x_" + (index - 6);
 401    }
 402    } catch (NumberFormatException e) {
 403    // variable identifier is no number, just take it as it is
 404  3432 return text;
 405    }
 406    }
 407    }
 408   
 409    /**
 410    * Transformer for a binary logical operator written in infix notation.
 411    */
 412    class BinaryLogical implements ListType {
 413   
 414    /** LaTeX for operator. */
 415    private final String latex;
 416   
 417    /**
 418    * Constructor.
 419    *
 420    * @param latex LaTeX for operator.
 421    */
 422  112 BinaryLogical(final String latex) {
 423  112 this.latex = latex;
 424    }
 425   
 426  1311 public String getLatex(final ElementList list, final boolean first) {
 427  1311 final StringBuffer buffer = new StringBuffer();
 428  1311 final String infix = "\\ " + latex + " \\ ";
 429  1311 if (!first) {
 430  756 buffer.append("(");
 431    }
 432    // we also handle it if it has not exactly two operands
 433  1311 for (int i = 0; i < list.size(); i++) {
 434  2646 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 435  2646 if (i + 1 < list.size()) {
 436  1335 buffer.append(infix);
 437    }
 438    }
 439  1311 if (!first) {
 440  756 buffer.append(")");
 441    }
 442  1311 return buffer.toString();
 443    }
 444    }
 445   
 446    /**
 447    * Transformer for a quantifier operator.
 448    */
 449    class Quantifier implements ListType {
 450   
 451    /** LaTeX for quantifier. */
 452    private final String latex;
 453   
 454    /**
 455    * Constructor.
 456    *
 457    * @param latex LaTeX for quantifier.
 458    */
 459  84 Quantifier(final String latex) {
 460  84 this.latex = latex;
 461    }
 462   
 463  376 public String getLatex(final ElementList list, final boolean first) {
 464  376 final StringBuffer buffer = new StringBuffer();
 465  376 buffer.append(latex + " ");
 466  376 for (int i = 0; i < list.size(); i++) {
 467  776 if (i != 0 || (i == 0 && list.size() <= 2)) {
 468  752 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 469    }
 470  776 if (i + 1 < list.size()) {
 471  400 buffer.append("\\ ");
 472    }
 473  776 if (list.size() > 2 && i == 1) {
 474  24 buffer.append("\\ ");
 475    }
 476    }
 477  376 return buffer.toString();
 478    }
 479    }
 480   
 481    /**
 482    * Transformer for negation.
 483    */
 484    class Not implements ListType {
 485  144 public String getLatex(final ElementList list, final boolean first) {
 486  144 final StringBuffer buffer = new StringBuffer();
 487  144 final String prefix = "\\neg ";
 488  144 buffer.append(prefix);
 489  144 for (int i = 0; i < list.size(); i++) {
 490  144 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 491    }
 492  144 return buffer.toString();
 493    }
 494    }
 495   
 496    /**
 497    * Transformer for a class operator.
 498    */
 499    class Class implements ListType {
 500  128 public String getLatex(final ElementList list, final boolean first) {
 501  128 final StringBuffer buffer = new StringBuffer();
 502  128 final String prefix = "\\{ ";
 503  128 buffer.append(prefix);
 504  128 for (int i = 0; i < list.size(); i++) {
 505  256 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 506  256 if (i + 1 < list.size()) {
 507  128 buffer.append(" \\ | \\ ");
 508    }
 509    }
 510  128 buffer.append(" \\} ");
 511  128 return buffer.toString();
 512    }
 513    }
 514   
 515    /**
 516    * Transformer for class list operator.
 517    */
 518    class Classlist implements ListType {
 519  0 public String getLatex(final ElementList list, final boolean first) {
 520  0 final StringBuffer buffer = new StringBuffer();
 521  0 final String prefix = "\\{ ";
 522  0 buffer.append(prefix);
 523  0 for (int i = 0; i < list.size(); i++) {
 524  0 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 525  0 if (i + 1 < list.size()) {
 526  0 buffer.append(", \\ ");
 527    }
 528    }
 529  0 buffer.append(" \\} ");
 530  0 return buffer.toString();
 531    }
 532    }
 533   
 534    /**
 535    * Transformer for a quantifier intersection.
 536    */
 537    class QuantorIntersection implements ListType {
 538  0 public String getLatex(final ElementList list, final boolean first) {
 539  0 final StringBuffer buffer = new StringBuffer();
 540  0 final String prefix = "\\bigcap";
 541  0 buffer.append(prefix);
 542  0 if (0 < list.size()) {
 543  0 buffer.append("{").append(Element2Latex.this.getLatex(list.getElement(0), false))
 544    .append("}");
 545    }
 546  0 for (int i = 1; i < list.size(); i++) {
 547  0 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 548  0 if (i + 1 < list.size()) {
 549  0 buffer.append(" \\ \\ ");
 550    }
 551    }
 552  0 buffer.append(" \\} ");
 553  0 return buffer.toString();
 554    }
 555    }
 556   
 557    /**
 558    * LATER mime 20080126: needed?
 559    */
 560    class QuantorUnion implements ListType {
 561  0 public String getLatex(final ElementList list, final boolean first) {
 562  0 final StringBuffer buffer = new StringBuffer();
 563  0 final String prefix = "\\bigcup";
 564  0 buffer.append(prefix);
 565  0 if (0 < list.size()) {
 566  0 buffer.append("{").append(Element2Latex.this.getLatex(list.getElement(0), false))
 567    .append("}");
 568    }
 569  0 for (int i = 1; i < list.size(); i++) {
 570  0 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 571  0 if (i + 1 < list.size()) {
 572  0 buffer.append(" \\ \\ ");
 573    }
 574    }
 575  0 buffer.append(" \\} ");
 576  0 return buffer.toString();
 577    }
 578    }
 579   
 580    /**
 581    * LATER mime 20080126: needed?
 582    */
 583    class Unknown implements ListType {
 584  0 public String getLatex(final ElementList list, final boolean first) {
 585  0 final StringBuffer buffer = new StringBuffer();
 586  0 buffer.append(list.getOperator());
 587  0 buffer.append("(");
 588  0 for (int i = 0; i < list.size(); i++) {
 589  0 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 590  0 if (i + 1 < list.size()) {
 591  0 buffer.append(", ");
 592    }
 593    }
 594  0 buffer.append(")");
 595  0 return buffer.toString();
 596    }
 597    }
 598   
 599   
 600    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Do Mrz 27 2008 21:55:30 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.