001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service;
017
018 import java.util.HashMap;
019 import java.util.Map;
020
021 import org.qedeq.base.utility.StringUtility;
022 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
023 import org.qedeq.kernel.bo.module.Element2Latex;
024 import org.qedeq.kernel.bo.module.ModuleLabels;
025 import org.qedeq.kernel.se.base.list.Element;
026 import org.qedeq.kernel.se.base.list.ElementList;
027 import org.qedeq.kernel.se.base.module.FunctionDefinition;
028 import org.qedeq.kernel.se.base.module.PredicateDefinition;
029 import org.qedeq.kernel.se.dto.module.FunctionDefinitionVo;
030 import org.qedeq.kernel.se.dto.module.PredicateDefinitionVo;
031
032
033 /**
034 * Transfer a QEDEQ formulas into LaTeX text.
035 *
036 * @author Michael Meyling
037 */
038 public final class Element2LatexImpl implements Element2Latex {
039
040 /** Knows about labels, definitions and external QEDEQ module references. */
041 private ModuleLabels labels;
042
043 /** Maps operator strings to {@link ElementList} to LaTeX mappers. */
044 private final Map elementList2ListType = new HashMap();
045
046 /** For mapping an unknown operator. */
047 private final ListType unknown = new Unknown();
048
049 /** Maps predicate identifiers to {@link PredicateDefinition}s. Contains default definitions
050 * as a fallback.*/
051 private final Map backupPredicateDefinitions = new HashMap();
052
053 /** Maps function identifiers to {@link FunctionDefinition}s. Contains default definitions. */
054 private final Map backupFunctionDefinitions = new HashMap();
055
056 /**
057 * Constructor.
058 *
059 * @param labels Knows about labels, definitions and external QEDEQ module references.
060 */
061 public Element2LatexImpl(final ModuleLabels labels) {
062 this.labels = labels;
063
064 this.elementList2ListType.put("PREDVAR", new Predvar());
065 this.elementList2ListType.put("FUNVAR", new Funvar());
066 this.elementList2ListType.put("PREDCON", new Predcon());
067 this.elementList2ListType.put("FUNCON", new Funcon());
068 this.elementList2ListType.put("VAR", new Var());
069
070 this.elementList2ListType.put("AND", new BinaryLogical("\\land"));
071 this.elementList2ListType.put("OR", new BinaryLogical("\\lor"));
072 this.elementList2ListType.put("IMPL", new BinaryLogical("\\rightarrow"));
073 this.elementList2ListType.put("EQUI", new BinaryLogical("\\leftrightarrow"));
074
075 this.elementList2ListType.put("FORALL", new Quantifier("\\forall"));
076 this.elementList2ListType.put("EXISTS", new Quantifier("\\exists"));
077 this.elementList2ListType.put("EXISTSU", new Quantifier("\\exists!"));
078
079 this.elementList2ListType.put("NOT", new Not());
080 this.elementList2ListType.put("CLASS", new Class());
081 this.elementList2ListType.put("CLASSLIST", new Classlist());
082
083 // TODO mime 20080126: wrong spelled and not used any longer (?)
084 this.elementList2ListType.put("QUANTOR_INTERSECTION", new QuantorIntersection());
085 this.elementList2ListType.put("QUANTOR_UNION", new QuantorUnion());
086
087 fillBackup();
088
089 }
090
091 /**
092 * Fill backup predicate list (if required modules could not be loaded, or the predicate is
093 * not yet defined.
094 */
095 private void fillBackup() {
096 // logical identity operator
097 addBackupPredicate(ExistenceChecker.NAME_EQUAL, "2", "#1 \\ = \\ #2");
098
099 // negation of the logical identity operator
100 addBackupPredicate("notEqual", "2", "#1 \\ \\neq \\ #2");
101
102 addBackupPredicate("in", "2", "#1 \\in #2");
103 addBackupPredicate("notIn", "2", "#1 \\notin #2");
104 addBackupPredicate("isSet", "1", "\\mathfrak{M}(#1)");
105 addBackupPredicate("subclass", "2", "#1 \\ \\subseteq \\ #2");
106 addBackupPredicate("isOrderedPair", "1", "\\mbox{isOrderedPair}(#1)");
107 addBackupPredicate("isRelation", "1", "\\mathfrak{Rel}(#1)");
108 addBackupPredicate("isFunction", "1", "\\mathfrak{Funct}(#1)");
109
110 addBackupFunction("RussellClass", "0", "\\mathfrak{Ru}");
111 addBackupFunction("universalClass", "0", "\\mathfrak{V}");
112 addBackupFunction("emptySet", "0", "\\emptyset");
113 addBackupFunction("union", "2", "(#1 \\cup #2)");
114 addBackupFunction("intersection", "2", "(#1 \\cap #2)");
115 addBackupFunction("complement", "1", "\\overline{#1}");
116 addBackupFunction("classList", "1", "\\{ #1 \\}");
117 addBackupFunction("classList", "2", "\\{ #1, #2 \\}");
118 addBackupFunction("setProduct", "1", "\\bigcap \\ #1");
119 addBackupFunction("setSum", "1", "\\bigcup \\ #1");
120 addBackupFunction("power", "1", "\\mathfrak{P}(#1)");
121 addBackupFunction("orderedPair", "2", "\\langle #1, #2 \\rangle");
122 addBackupFunction("cartesianProduct", "2", "( #1 \\times #2)");
123 addBackupFunction("domain", "1", "\\mathfrak{Dom}(#1)");
124 addBackupFunction("range", "1", "\\mathfrak{Rng}(#1)");
125 addBackupFunction("successor", "1", "#1'");
126
127 }
128
129 /**
130 * Add predicate to backup list.
131 *
132 * @param name Predicate name.
133 * @param argNumber Number of arguments.
134 * @param latexPattern This is the latex presentation. Variables are marked by "#1", "#2"
135 * and so on.
136 */
137 private void addBackupPredicate(final String name, final String argNumber,
138 final String latexPattern) {
139 final String key = name + "_" + argNumber;
140 final PredicateDefinitionVo predicate = new PredicateDefinitionVo();
141 predicate.setArgumentNumber(argNumber);
142 predicate.setName(name);
143 predicate.setLatexPattern(latexPattern);
144 backupPredicateDefinitions.put(key, predicate);
145 }
146
147 /**
148 * Add function to backup list.
149 *
150 * @param name Function name.
151 * @param argNumber Number of arguments.
152 * @param latexPattern This is the LaTex presentation. Variables are marked by "#1", "#2"
153 * and so on.
154 */
155 private void addBackupFunction(final String name, final String argNumber,
156 final String latexPattern) {
157 final String key = name + "_" + argNumber;
158 final FunctionDefinitionVo function = new FunctionDefinitionVo();
159 function.setArgumentNumber(argNumber);
160 function.setName(name);
161 function.setLatexPattern(latexPattern);
162 backupFunctionDefinitions.put(key, function);
163 }
164
165 public String getLatex(final Element element) {
166 return getLatex(element, true);
167 }
168
169 /**
170 * Get LaTeX element presentation.
171 *
172 * @param element Print this element.
173 * @param first First level?
174 * @return LaTeX form of element.
175 */
176 String getLatex(final Element element, final boolean first) {
177 if (element == null) {
178 return "";
179 }
180 if (element.isAtom()) {
181 return element.getAtom().getString();
182 }
183 final ElementList list = element.getList();
184
185 ListType converter = (ListType) elementList2ListType.get(list.getOperator());
186
187 if (converter == null) {
188 converter = this.unknown;
189 }
190 return converter.getLatex(list, first);
191
192 }
193
194 /**
195 * Get default definition mapping of predicate definitions. Our last hope.
196 *
197 * @return Mapping of predicate definitions.
198 */
199 Map getBackupPredicateDefinitions() {
200 return this.backupPredicateDefinitions;
201 }
202
203 /**
204 * Get default definition mapping of function definitions. Our last hope.
205 *
206 * @return Mapping of predicate definitions.
207 */
208 Map getBackupFunctionDefinitions() {
209 return this.backupFunctionDefinitions;
210 }
211
212 /**
213 * Describes the interface for an {@link ElementList} to LaTeX converter.
214 */
215 interface ListType {
216
217 /**
218 * Transform list into LaTeX.
219 *
220 * @param list This list shall be transformed.
221 * @param first Is the resulting LaTeX formula or term at top level? If so we possibly
222 * can omit some brackets.
223 * @return LaTeX formula or term.
224 */
225 public String getLatex(ElementList list, boolean first);
226 }
227
228 /**
229 * Transformer for a predicate variable.
230 */
231 class Predvar implements ListType {
232 public String getLatex(final ElementList list, final boolean first) {
233 final StringBuffer buffer = new StringBuffer();
234 final String identifier = list.getElement(0).getAtom().getString();
235 buffer.append(identifier);
236 if (list.size() > 1) {
237 buffer.append("(");
238 for (int i = 1; i < list.size(); i++) {
239 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
240 if (i + 1 < list.size()) {
241 buffer.append(", ");
242 }
243 }
244 buffer.append(")");
245 }
246 return buffer.toString();
247 }
248 }
249
250 /**
251 * Transformer for a function variable.
252 */
253 class Funvar implements ListType {
254 public String getLatex(final ElementList list, final boolean first) {
255 final StringBuffer buffer = new StringBuffer();
256 final String identifier = list.getElement(0).getAtom().getString();
257 buffer.append(identifier);
258 if (list.size() > 1) {
259 buffer.append("(");
260 for (int i = 1; i < list.size(); i++) {
261 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
262 if (i + 1 < list.size()) {
263 buffer.append(", ");
264 }
265 }
266 buffer.append(")");
267 }
268 return buffer.toString();
269 }
270 }
271
272 /**
273 * Transformer for a predicate constant.
274 */
275 class Predcon implements ListType {
276 public String getLatex(final ElementList list, final boolean first) {
277 final StringBuffer buffer = new StringBuffer();
278 final String name = list.getElement(0).getAtom().getString();
279 final int arguments = list.size() - 1;
280 String identifier = name + "_" + (arguments);
281 // LATER 20060922 m31: is only working for definition name + argument number
282 // if argument length is dynamic this dosen't work
283 PredicateDefinition definition = (PredicateDefinition)
284 Element2LatexImpl.this.labels.getPredicateDefinitions().get(identifier);
285 if (definition == null) {
286 // try external modules
287 try {
288 final int external = name.indexOf(".");
289 if (external >= 0) {
290 final String shortName = name.substring(external + 1);
291 identifier = shortName + "_" + (arguments);
292 if (Element2LatexImpl.this.labels.getReferences() != null
293 && Element2LatexImpl.this.labels.getReferences().size() > 0) {
294 final String label = name.substring(0, external);
295 final DefaultKernelQedeqBo newProp = (DefaultKernelQedeqBo)
296 Element2LatexImpl.this.labels.getReferences().getQedeqBo(label);
297 if (newProp != null) {
298 if (newProp.getExistenceChecker().predicateExists(shortName,
299 arguments)) {
300 definition = newProp.getLabels()
301 .getPredicate(shortName, arguments);
302 }
303 }
304 }
305 }
306 } catch (Exception e) {
307 // try failed...
308 }
309 }
310 // we try our backup
311 if (definition == null) {
312 definition = (PredicateDefinition) Element2LatexImpl.this.getBackupPredicateDefinitions()
313 .get(identifier);
314 }
315 if (definition != null) {
316 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
317 for (int i = list.size() - 1; i >= 1; i--) {
318 StringUtility.replace(define, "#" + i, Element2LatexImpl.this.getLatex(
319 list.getElement(i), false));
320 }
321 buffer.append(define);
322 } else {
323 buffer.append(identifier);
324 buffer.append("(");
325 for (int i = 1; i < list.size(); i++) {
326 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
327 if (i + 1 < list.size()) {
328 buffer.append(", ");
329 }
330 }
331 buffer.append(")");
332 }
333 return buffer.toString();
334 }
335 }
336
337 /**
338 * Transformer for a function constant.
339 */
340 class Funcon implements ListType {
341
342 public String getLatex(final ElementList list, final boolean first) {
343 final StringBuffer buffer = new StringBuffer();
344 final String name = list.getElement(0).getAtom().getString();
345 final int arguments = list.size() - 1;
346 String identifier = name + "_" + (arguments);
347 // LATER 20060922 m31: is only working for definition name + argument number
348 // if argument length is dynamic this dosen't work
349 FunctionDefinition definition = (FunctionDefinition)
350 Element2LatexImpl.this.labels.getFunctionDefinitions().get(identifier);
351 if (definition == null) {
352 // try external modules
353 try {
354 final int external = name.indexOf(".");
355 if (external >= 0) {
356 final String shortName = name.substring(external + 1);
357 identifier = shortName + "_" + (arguments);
358 if (Element2LatexImpl.this.labels.getReferences() != null
359 && Element2LatexImpl.this.labels.getReferences().size() > 0) {
360 final String label = name.substring(0, external);
361 final DefaultKernelQedeqBo newProp = (DefaultKernelQedeqBo)
362 Element2LatexImpl.this.labels.getReferences().getQedeqBo(label);
363 if (newProp != null) {
364 if (newProp.getExistenceChecker().functionExists(shortName,
365 arguments)) {
366 definition = newProp.getLabels()
367 .getFunction(shortName, arguments);
368 }
369 }
370 }
371 }
372 } catch (Exception e) {
373 // try failed...
374 }
375 }
376 // we try our backup
377 if (definition == null) {
378 definition = (FunctionDefinition) Element2LatexImpl.this.getBackupFunctionDefinitions()
379 .get(identifier);
380 }
381 if (definition != null) {
382 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
383 for (int i = list.size() - 1; i >= 1; i--) {
384 StringUtility.replace(define, "#" + i, Element2LatexImpl.this.
385 getLatex(list.getElement(i), false));
386 }
387 buffer.append(define);
388 } else {
389 buffer.append(identifier);
390 buffer.append("(");
391 for (int i = 1; i < list.size(); i++) {
392 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
393 if (i + 1 < list.size()) {
394 buffer.append(", ");
395 }
396 }
397 buffer.append(")");
398 }
399 return buffer.toString();
400 }
401 }
402
403 /**
404 * Transformer for a subject variable.
405 */
406 static class Var implements ListType {
407 public String getLatex(final ElementList list, final boolean first) {
408 final String text = list.getElement(0).getAtom().getString();
409 // interpret variable identifier as number
410 try {
411 final int index = Integer.parseInt(text);
412 final String newText = "" + index;
413 if (!text.equals(newText) || newText.startsWith("-")) {
414 throw new NumberFormatException("This is no allowed number: " + text);
415 }
416 switch (index) {
417 case 1:
418 return "x";
419 case 2:
420 return "y";
421 case 3:
422 return "z";
423 case 4:
424 return "u";
425 case 5:
426 return "v";
427 case 6:
428 return "w";
429 default:
430 return "x_" + (index - 6);
431 }
432 } catch (NumberFormatException e) {
433 // variable identifier is no number, just take it as it is
434 return text;
435 }
436 }
437 }
438
439 /**
440 * Transformer for a binary logical operator written in infix notation.
441 */
442 class BinaryLogical implements ListType {
443
444 /** LaTeX for operator. */
445 private final String latex;
446
447 /**
448 * Constructor.
449 *
450 * @param latex LaTeX for operator.
451 */
452 BinaryLogical(final String latex) {
453 this.latex = latex;
454 }
455
456 public String getLatex(final ElementList list, final boolean first) {
457 final StringBuffer buffer = new StringBuffer();
458 final String infix = "\\ " + latex + "\\ ";
459 if (!first) {
460 buffer.append("(");
461 }
462 // we also handle it if it has not exactly two operands
463 for (int i = 0; i < list.size(); i++) {
464 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
465 if (i + 1 < list.size()) {
466 buffer.append(infix);
467 }
468 }
469 if (!first) {
470 buffer.append(")");
471 }
472 return buffer.toString();
473 }
474 }
475
476 /**
477 * Transformer for a quantifier operator.
478 */
479 class Quantifier implements ListType {
480
481 /** LaTeX for quantifier. */
482 private final String latex;
483
484 /**
485 * Constructor.
486 *
487 * @param latex LaTeX for quantifier.
488 */
489 Quantifier(final String latex) {
490 this.latex = latex;
491 }
492
493 public String getLatex(final ElementList list, final boolean first) {
494 final StringBuffer buffer = new StringBuffer();
495 buffer.append(latex + " ");
496 for (int i = 0; i < list.size(); i++) {
497 if (i != 0 || (i == 0 && list.size() <= 2)) {
498 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
499 }
500 if (i + 1 < list.size()) {
501 buffer.append("\\ ");
502 }
503 if (list.size() > 2 && i == 1) {
504 buffer.append("\\ ");
505 }
506 }
507 return buffer.toString();
508 }
509 }
510
511 /**
512 * Transformer for negation.
513 */
514 class Not implements ListType {
515 public String getLatex(final ElementList list, final boolean first) {
516 final StringBuffer buffer = new StringBuffer();
517 final String prefix = "\\neg ";
518 buffer.append(prefix);
519 for (int i = 0; i < list.size(); i++) {
520 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
521 }
522 return buffer.toString();
523 }
524 }
525
526 /**
527 * Transformer for a class operator.
528 */
529 class Class implements ListType {
530 public String getLatex(final ElementList list, final boolean first) {
531 final StringBuffer buffer = new StringBuffer();
532 final String prefix = "\\{ ";
533 buffer.append(prefix);
534 for (int i = 0; i < list.size(); i++) {
535 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
536 if (i + 1 < list.size()) {
537 buffer.append(" \\ | \\ ");
538 }
539 }
540 buffer.append(" \\} ");
541 return buffer.toString();
542 }
543 }
544
545 /**
546 * Transformer for class list operator.
547 */
548 class Classlist implements ListType {
549 public String getLatex(final ElementList list, final boolean first) {
550 final StringBuffer buffer = new StringBuffer();
551 final String prefix = "\\{ ";
552 buffer.append(prefix);
553 for (int i = 0; i < list.size(); i++) {
554 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
555 if (i + 1 < list.size()) {
556 buffer.append(", \\ ");
557 }
558 }
559 buffer.append(" \\} ");
560 return buffer.toString();
561 }
562 }
563
564 /**
565 * Transformer for a quantifier intersection.
566 */
567 class QuantorIntersection implements ListType {
568 public String getLatex(final ElementList list, final boolean first) {
569 final StringBuffer buffer = new StringBuffer();
570 final String prefix = "\\bigcap";
571 buffer.append(prefix);
572 if (0 < list.size()) {
573 buffer.append("{").append(Element2LatexImpl.this.getLatex(list.getElement(0), false))
574 .append("}");
575 }
576 for (int i = 1; i < list.size(); i++) {
577 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
578 if (i + 1 < list.size()) {
579 buffer.append(" \\ \\ ");
580 }
581 }
582 buffer.append(" \\} ");
583 return buffer.toString();
584 }
585 }
586
587 /**
588 * LATER mime 20080126: needed?
589 */
590 class QuantorUnion implements ListType {
591 public String getLatex(final ElementList list, final boolean first) {
592 final StringBuffer buffer = new StringBuffer();
593 final String prefix = "\\bigcup";
594 buffer.append(prefix);
595 if (0 < list.size()) {
596 buffer.append("{").append(Element2LatexImpl.this.getLatex(list.getElement(0), false))
597 .append("}");
598 }
599 for (int i = 1; i < list.size(); i++) {
600 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
601 if (i + 1 < list.size()) {
602 buffer.append(" \\ \\ ");
603 }
604 }
605 buffer.append(" \\} ");
606 return buffer.toString();
607 }
608 }
609
610 /**
611 * LATER mime 20080126: needed?
612 */
613 class Unknown implements ListType {
614 public String getLatex(final ElementList list, final boolean first) {
615 final StringBuffer buffer = new StringBuffer();
616 buffer.append(list.getOperator());
617 buffer.append("(");
618 for (int i = 0; i < list.size(); i++) {
619 buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
620 if (i + 1 < list.size()) {
621 buffer.append(", ");
622 }
623 }
624 buffer.append(")");
625 return buffer.toString();
626 }
627 }
628
629
630 }
|