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