Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart6.png 69% of files have more coverage
229   600   88   9,96
96   400   0,38   1,53
23     3,83  
15    
 
  Element2Latex       Line # 42 49 12 90,8% 0.9076923
  Element2Latex.ListType       Line # 197 0 0 - -1.0
  Element2Latex.Predvar       Line # 213 11 4 100% 1.0
  Element2Latex.Funvar       Line # 235 11 4 83,3% 0.8333333
  Element2Latex.Predcon       Line # 257 29 12 67,4% 0.67391306
  Element2Latex.Funcon       Line # 316 29 12 37% 0.36956522
  Element2Latex.Var       Line # 376 22 10 20% 0.2
  Element2Latex.BinaryLogical       Line # 412 12 6 100% 1.0
  Element2Latex.Quantifier       Line # 449 11 9 100% 1.0
  Element2Latex.Not       Line # 484 6 2 100% 1.0
  Element2Latex.Class       Line # 499 9 3 100% 1.0
  Element2Latex.Classlist       Line # 518 9 3 0% 0.0
  Element2Latex.QuantorIntersection       Line # 537 11 4 0% 0.0
  Element2Latex.QuantorUnion       Line # 560 11 4 0% 0.0
  Element2Latex.Unknown       Line # 583 9 3 0% 0.0
 
  (3)
 
1    /* $Id: Element2Latex.java,v 1.1 2008/07/26 07:58:28 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.bo.service.latex;
19   
20    import java.util.HashMap;
21    import java.util.Map;
22   
23    import org.qedeq.base.utility.StringUtility;
24    import org.qedeq.kernel.base.list.Element;
25    import org.qedeq.kernel.base.list.ElementList;
26    import org.qedeq.kernel.base.module.FunctionDefinition;
27    import org.qedeq.kernel.base.module.PredicateDefinition;
28    import org.qedeq.kernel.bo.ModuleReferenceList;
29    import org.qedeq.kernel.bo.logic.wf.ExistenceChecker;
30    import org.qedeq.kernel.bo.module.DefaultExistenceChecker;
31    import org.qedeq.kernel.bo.module.KernelQedeqBo;
32    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
33    import org.qedeq.kernel.visitor.AbstractModuleVisitor;
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  18 toggle public Element2Latex(final ModuleReferenceList references) {
65  18 this.references = references;
66   
67  18 this.elementList2ListType.put("PREDVAR", new Predvar());
68  18 this.elementList2ListType.put("FUNVAR", new Funvar());
69  18 this.elementList2ListType.put("PREDCON", new Predcon());
70  18 this.elementList2ListType.put("FUNCON", new Funcon());
71  18 this.elementList2ListType.put("VAR", new Var());
72   
73  18 this.elementList2ListType.put("AND", new BinaryLogical("\\land"));
74  18 this.elementList2ListType.put("OR", new BinaryLogical("\\lor"));
75  18 this.elementList2ListType.put("IMPL", new BinaryLogical("\\rightarrow"));
76  18 this.elementList2ListType.put("EQUI", new BinaryLogical("\\leftrightarrow"));
77   
78  18 this.elementList2ListType.put("FORALL", new Quantifier("\\forall"));
79  18 this.elementList2ListType.put("EXISTS", new Quantifier("\\exists"));
80  18 this.elementList2ListType.put("EXISTSU", new Quantifier("\\exists!"));
81   
82  18 this.elementList2ListType.put("NOT", new Not());
83  18 this.elementList2ListType.put("CLASS", new Class());
84  18 this.elementList2ListType.put("CLASSLIST", new Classlist());
85   
86    // TODO mime 20080126: wrong spelled and not used any longer (?)
87  18 this.elementList2ListType.put("QUANTOR_INTERSECTION", new QuantorIntersection());
88  18 this.elementList2ListType.put("QUANTOR_UNION", new QuantorUnion());
89   
90    // quick hack to have the logical identity operator
91  18 final String nameEqual = ExistenceChecker.NAME_EQUAL;
92  18 final String argNumberEqual = "2";
93  18 final String keyEqual = nameEqual + "_" + argNumberEqual;
94  18 if (!getPredicateDefinitions().containsKey(keyEqual)) {
95  18 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
96  18 equal.setArgumentNumber(argNumberEqual);
97  18 equal.setName(nameEqual);
98  18 equal.setLatexPattern("#1 \\ = \\ #2");
99  18 getPredicateDefinitions().put(keyEqual, equal);
100    }
101   
102    // LATER mime 20080107: quick hack to get the negation of the logical identity operator
103  18 final String nameNotEqual = "notEqual";
104  18 final String argNumberNotEqual = "2";
105  18 final String keyNotEqual = nameNotEqual + "_" + argNumberNotEqual;
106  18 if (!getPredicateDefinitions().containsKey(keyNotEqual)) {
107  18 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
108  18 notEqual.setArgumentNumber("2");
109  18 notEqual.setName("notEqual");
110  18 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
111  18 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  76 toggle public void addPredicate(final PredicateDefinition definition) {
121  76 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 toggle 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  1092 toggle public String getLatex(final Element element) {
142  1092 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  8396 toggle String getLatex(final Element element, final boolean first) {
153  8396 if (element.isAtom()) {
154  0 return element.getAtom().getString();
155    }
156  8396 final ElementList list = element.getList();
157   
158  8396 ListType converter = (ListType) elementList2ListType.get(list.getOperator());
159   
160  8396 if (converter == null) {
161  0 converter = this.unknown;
162    }
163  8396 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  1032 toggle ModuleReferenceList getReferences() {
173  1032 return this.references;
174    }
175   
176    /**
177    * Get mapping of predicate definitions.
178    *
179    * @return Mapping of predicate definitions.
180    */
 
181  1492 toggle Map getPredicateDefinitions() {
182  1492 return this.predicateDefinitions;
183    }
184   
185    /**
186    * Get mapping of function definitions.
187    *
188    * @return Mapping of function definitions.
189    */
 
190  1024 toggle 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  932 toggle public String getLatex(final ElementList list, final boolean first) {
215  932 final StringBuffer buffer = new StringBuffer();
216  932 final String identifier = list.getElement(0).getAtom().getString();
217  932 buffer.append(identifier);
218  932 if (list.size() > 1) {
219  300 buffer.append("(");
220  616 for (int i = 1; i < list.size(); i++) {
221  316 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
222  316 if (i + 1 < list.size()) {
223  16 buffer.append(", ");
224    }
225    }
226  300 buffer.append(")");
227    }
228  932 return buffer.toString();
229    }
230    }
231   
232    /**
233    * Transformer for a function variable.
234    */
 
235    class Funvar implements ListType {
 
236  8 toggle 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  16 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  1344 toggle public String getLatex(final ElementList list, final boolean first) {
259  1344 final StringBuffer buffer = new StringBuffer();
260  1344 final String name = list.getElement(0).getAtom().getString();
261  1344 final int arguments = list.size() - 1;
262  1344 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  1344 PredicateDefinition definition = (PredicateDefinition)
266    Element2Latex.this.getPredicateDefinitions().get(identifier);
267  1344 if (definition == null) {
268    // try external modules
269  344 try {
270  344 final int external = name.indexOf(".");
271  344 if (external >= 0 && Element2Latex.this.getReferences() != null
272    && Element2Latex.this.getReferences().size() > 0) {
273  344 final String label = name.substring(0, external);
274  344 final KernelQedeqBo newProp = (KernelQedeqBo)
275    Element2Latex.this.getReferences().getQedeqBo(label);
276  344 if (newProp != null) {
277  344 final String shortName = name.substring(external + 1);
278  344 if (newProp.getExistenceChecker().predicateExists(shortName,
279    arguments)) {
280    // FIXME mime 20080120: Quick and very dirty!
281  344 final DefaultExistenceChecker checker = (DefaultExistenceChecker)
282    newProp.getExistenceChecker();
283  344 definition = checker.getPredicate(shortName, arguments);
284    }
285    }
286    }
287    } catch (Exception e) {
288    // try failed...
289    }
290    }
291  1344 if (definition != null) {
292  1344 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
293  3536 for (int i = list.size() - 1; i >= 1; i--) {
294  2192 StringUtility.replace(define, "#" + i, Element2Latex.this.getLatex(
295    list.getElement(i), false));
296    }
297  1344 buffer.append(define);
298    } else {
299  0 buffer.append(identifier);
300  0 buffer.append("(");
301  0 for (int i = 1; i < list.size(); i++) {
302  0 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
303  0 if (i + 1 < list.size()) {
304  0 buffer.append(", ");
305    }
306    }
307  0 buffer.append(")");
308    }
309  1344 return buffer.toString();
310    }
311    }
312   
313    /**
314    * Transformer for a function constant.
315    */
 
316    class Funcon implements ListType {
317   
 
318  960 toggle 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 final 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  2092 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  3264 toggle public String getLatex(final ElementList list, final boolean first) {
378  3264 final String text = list.getElement(0).getAtom().getString();
379    // interpret variable identifier as number
380  3264 try {
381  3264 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  3264 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  72 toggle BinaryLogical(final String latex) {
423  72 this.latex = latex;
424    }
425   
 
426  1280 toggle public String getLatex(final ElementList list, final boolean first) {
427  1280 final StringBuffer buffer = new StringBuffer();
428  1280 final String infix = "\\ " + latex + " \\ ";
429  1280 if (!first) {
430  736 buffer.append("(");
431    }
432    // we also handle it if it has not exactly two operands
433  3864 for (int i = 0; i < list.size(); i++) {
434  2584 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
435  2584 if (i + 1 < list.size()) {
436  1304 buffer.append(infix);
437    }
438    }
439  1280 if (!first) {
440  736 buffer.append(")");
441    }
442  1280 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  54 toggle Quantifier(final String latex) {
460  54 this.latex = latex;
461    }
462   
 
463  336 toggle public String getLatex(final ElementList list, final boolean first) {
464  336 final StringBuffer buffer = new StringBuffer();
465  336 buffer.append(latex + " ");
466  1024 for (int i = 0; i < list.size(); i++) {
467  688 if (i != 0 || (i == 0 && list.size() <= 2)) {
468  672 buffer.append(Element2Latex.this.getLatex(list.getElement(i), false));
469    }
470  688 if (i + 1 < list.size()) {
471  352 buffer.append("\\ ");
472    }
473  688 if (list.size() > 2 && i == 1) {
474  16 buffer.append("\\ ");
475    }
476    }
477  336 return buffer.toString();
478    }
479    }
480   
481    /**
482    * Transformer for negation.
483    */
 
484    class Not implements ListType {
 
485  144 toggle 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  288 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 toggle 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  384 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 toggle 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 toggle 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 toggle 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 toggle 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 v2.3.1
Sa Aug 2 2008 13:56:32 CEST.		   Clover: Open Source License registered to qedeq.org .