Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Sa Jan 26 2008 14:11:34 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.1 2008/01/26 12:39:09 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2007, 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.logic.DefaultExistenceChecker;
 28    import org.qedeq.kernel.bo.logic.ExistenceChecker;
 29    import org.qedeq.kernel.bo.module.ModuleProperties;
 30    import org.qedeq.kernel.bo.module.ModuleReferenceList;
 31    import org.qedeq.kernel.bo.visitor.AbstractModuleVisitor;
 32    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 33    import org.qedeq.kernel.utility.ReplaceUtility;
 34   
 35   
 36    /**
 37    * Transfer a QEDEQ formulas into LaTeX text.
 38    *
 39    * @version $Revision: 1.1 $
 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  29 public Element2Latex(final ModuleReferenceList references) {
 65  29 this.references = references;
 66   
 67  29 this.elementList2ListType.put("PREDVAR", new Predvar());
 68  29 this.elementList2ListType.put("FUNVAR", new Funvar());
 69  29 this.elementList2ListType.put("PREDCON", new Predcon());
 70  29 this.elementList2ListType.put("FUNCON", new Funcon());
 71  29 this.elementList2ListType.put("VAR", new Var());
 72   
 73  29 this.elementList2ListType.put("AND", new BinaryLogical("\\land"));
 74  29 this.elementList2ListType.put("OR", new BinaryLogical("\\lor"));
 75  29 this.elementList2ListType.put("IMPL", new BinaryLogical("\\rightarrow"));
 76  29 this.elementList2ListType.put("EQUI", new BinaryLogical("\\leftrightarrow"));
 77   
 78  29 this.elementList2ListType.put("FORALL", new Quantifier("\\forall"));
 79  29 this.elementList2ListType.put("EXISTS", new Quantifier("\\exists"));
 80  29 this.elementList2ListType.put("EXISTSU", new Quantifier("\\exists!"));
 81   
 82  29 this.elementList2ListType.put("NOT", new Not());
 83  29 this.elementList2ListType.put("CLASS", new Class());
 84  29 this.elementList2ListType.put("CLASSLIST", new Classlist());
 85   
 86    // TODO mime 20080126: wrong spelled and not used any longer (?)
 87  29 this.elementList2ListType.put("QUANTOR_INTERSECTION", new QuantorIntersection());
 88  29 this.elementList2ListType.put("QUANTOR_UNION", new QuantorUnion());
 89   
 90    // quick hack to have the logical identity operator
 91  29 final String nameEqual = ExistenceChecker.NAME_EQUAL;
 92  29 final String argNumberEqual = "2";
 93  29 final String keyEqual = nameEqual + "_" + argNumberEqual;
 94  29 if (!getPredicateDefinitions().containsKey(keyEqual)) {
 95  29 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 96  29 equal.setArgumentNumber(argNumberEqual);
 97  29 equal.setName(nameEqual);
 98  29 equal.setLatexPattern("#1 \\ = \\ #2");
 99  29 getPredicateDefinitions().put(keyEqual, equal);
 100    }
 101   
 102    // LATER mime 20080107: quick hack to get the negation of the logical identity operator
 103  29 final String nameNotEqual = "notEqual";
 104  29 final String argNumberNotEqual = "2";
 105  29 final String keyNotEqual = nameNotEqual + "_" + argNumberNotEqual;
 106  29 if (!getPredicateDefinitions().containsKey(keyNotEqual)) {
 107  29 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 108  29 notEqual.setArgumentNumber("2");
 109  29 notEqual.setName("notEqual");
 110  29 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 111  29 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  94 public void addPredicate(final PredicateDefinition definition) {
 121  94 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  1145 public String getLatex(final Element element) {
 142  1145 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  8710 String getLatex(final Element element, final boolean first) {
 153  8710 if (element.isAtom()) {
 154  0 return element.getAtom().getString();
 155    }
 156  8710 final ElementList list = element.getList();
 157   
 158  8710 ListType converter = (ListType) elementList2ListType.get(list.getOperator());
 159   
 160  8710 if (converter == null) {
 161  0 converter = this.unknown;
 162    }
 163  8710 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  1086 ModuleReferenceList getReferences() {
 173  1086 return this.references;
 174    }
 175   
 176    /**
 177    * Get mapping of predicate definitions.
 178    *
 179    * @return Mapping of predicate definitions.
 180    */
 181  1612 Map getPredicateDefinitions() {
 182  1612 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  934 public String getLatex(final ElementList list, final boolean first) {
 215  934 final StringBuffer buffer = new StringBuffer();
 216  934 final String identifier = list.getElement(0).getAtom().getString();
 217  934 buffer.append(identifier);
 218  934 if (list.size() > 1) {
 219  298 buffer.append("(");
 220  298 for (int i = 1; i < list.size(); i++) {
 221  314 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 222  314 if (i + 1 < list.size()) {
 223  16 buffer.append(", ");
 224    }
 225    }
 226  298 buffer.append(")");
 227    }
 228  934 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  365 try {
 270  365 final int external = name.indexOf(".");
 271  365 if (external >= 0 && Element2Latex.this.getReferences() != null
 272    && Element2Latex.this.getReferences().size() > 0) {
 273  362 final String label = name.substring(0, external);
 274  362 final ModuleProperties newProp = Element2Latex.this.getReferences()
 275    .getModuleProperties(label);
 276  362 if (newProp != null) {
 277  362 final String shortName = name.substring(external + 1);
 278  354 if (newProp.getExistenceChecker().predicateExists(shortName,
 279    arguments)) {
 280    // FIXME mime 20080120: Quick and very dirty!
 281  354 DefaultExistenceChecker checker = (DefaultExistenceChecker)
 282    newProp.getExistenceChecker();
 283  354 definition = checker.getPredicate(shortName, arguments);
 284    }
 285    }
 286    }
 287    } catch (Exception e) {
 288    // try failed...
 289    }
 290    }
 291  1402 if (definition != null) {
 292  1391 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 293  1391 for (int i = list.size() - 1; i >= 1; i--) {
 294  2281 ReplaceUtility.replace(define, "#" + i, Element2Latex.this.getLatex(
 295    list.getElement(i), false));
 296    }
 297  1391 buffer.append(define);
 298    } else {
 299  11 buffer.append(identifier);
 300  11 buffer.append("(");
 301  11 for (int i = 1; i < list.size(); i++) {
 302  22 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 303  22 if (i + 1 < list.size()) {
 304  11 buffer.append(", ");
 305    }
 306    }
 307  11 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 ModuleProperties newProp = Element2Latex.this.getReferences().
 335    getModuleProperties(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 ReplaceUtility.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  3442 public String getLatex(final ElementList list, final boolean first) {
 378  3442 final String text = list.getElement(0).getAtom().getString();
 379    // interpret variable identifier as number
 380  3442 try {
 381  3442 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  3442 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  116 BinaryLogical(final String latex) {
 423  116 this.latex = latex;
 424    }
 425   
 426  1309 public String getLatex(final ElementList list, final boolean first) {
 427  1309 final StringBuffer buffer = new StringBuffer();
 428  1309 final String infix = "\\ " + latex + " \\ ";
 429  1309 if (!first) {
 430  757 buffer.append("(");
 431    }
 432    // we also handle it if it has not exactly two operands
 433  1309 for (int i = 0; i < list.size(); i++) {
 434  2642 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
 435  2642 if (i + 1 < list.size()) {
 436  1333 buffer.append(infix);
 437    }
 438    }
 439  1309 if (!first) {
 440  757 buffer.append(")");
 441    }
 442  1309 return buffer.toString();
 443    }