1 |
| |
2 |
| |
3 |
| |
4 |
| |
5 |
| |
6 |
| |
7 |
| |
8 |
| |
9 |
| |
10 |
| |
11 |
| |
12 |
| |
13 |
| |
14 |
| |
15 |
| |
16 |
| |
17 |
| |
18 |
| package org.qedeq.kernel.latex; |
19 |
| |
20 |
| import java.io.File; |
21 |
| import java.io.FileOutputStream; |
22 |
| import java.io.IOException; |
23 |
| import java.io.OutputStream; |
24 |
| import java.io.PrintStream; |
25 |
| import java.util.HashMap; |
26 |
| import java.util.Map; |
27 |
| |
28 |
| import org.qedeq.kernel.base.list.Element; |
29 |
| import org.qedeq.kernel.base.list.ElementList; |
30 |
| import org.qedeq.kernel.base.module.Axiom; |
31 |
| import org.qedeq.kernel.base.module.Chapter; |
32 |
| import org.qedeq.kernel.base.module.ChapterList; |
33 |
| import org.qedeq.kernel.base.module.FunctionDefinition; |
34 |
| import org.qedeq.kernel.base.module.Latex; |
35 |
| import org.qedeq.kernel.base.module.LatexList; |
36 |
| import org.qedeq.kernel.base.module.LiteratureItem; |
37 |
| import org.qedeq.kernel.base.module.LiteratureItemList; |
38 |
| import org.qedeq.kernel.base.module.Node; |
39 |
| import org.qedeq.kernel.base.module.NodeType; |
40 |
| import org.qedeq.kernel.base.module.PredicateDefinition; |
41 |
| import org.qedeq.kernel.base.module.Proposition; |
42 |
| import org.qedeq.kernel.base.module.Qedeq; |
43 |
| import org.qedeq.kernel.base.module.Rule; |
44 |
| import org.qedeq.kernel.base.module.Section; |
45 |
| import org.qedeq.kernel.base.module.SectionList; |
46 |
| import org.qedeq.kernel.base.module.Subsection; |
47 |
| import org.qedeq.kernel.base.module.SubsectionList; |
48 |
| import org.qedeq.kernel.base.module.SubsectionType; |
49 |
| import org.qedeq.kernel.base.module.VariableList; |
50 |
| import org.qedeq.kernel.bo.control.QedeqBoFactory; |
51 |
| import org.qedeq.kernel.bo.module.ModuleDataException; |
52 |
| import org.qedeq.kernel.dto.module.PredicateDefinitionVo; |
53 |
| import org.qedeq.kernel.log.Trace; |
54 |
| import org.qedeq.kernel.utility.ReplaceUtility; |
55 |
| |
56 |
| |
57 |
| |
58 |
| |
59 |
| |
60 |
| |
61 |
| |
62 |
| |
63 |
| |
64 |
| |
65 |
| |
66 |
| |
67 |
| |
68 |
| |
69 |
| |
70 |
| public final class Qedeq2Wiki { |
71 |
| |
72 |
| |
73 |
| private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz"; |
74 |
| |
75 |
| |
76 |
| private PrintStream printer; |
77 |
| |
78 |
| |
79 |
| private Qedeq qedeq; |
80 |
| |
81 |
| |
82 |
| private String language; |
83 |
| |
84 |
| |
85 |
| private Object level; |
86 |
| |
87 |
| |
88 |
| private Map definitions = new HashMap(); |
89 |
| |
90 |
| |
91 |
| private File outputDirectory; |
92 |
| |
93 |
| |
94 |
| |
95 |
| |
96 |
| |
97 |
| |
98 |
| |
99 |
| |
100 |
0
| public Qedeq2Wiki(final String context, final Qedeq qedeq) throws ModuleDataException {
|
101 |
0
| this.qedeq = QedeqBoFactory.createQedeq(context, qedeq);
|
102 |
0
| final PredicateDefinitionVo equal = new PredicateDefinitionVo();
|
103 |
| |
104 |
0
| equal.setArgumentNumber("2");
|
105 |
0
| equal.setLatexPattern("#1 \\ = \\ #2");
|
106 |
0
| definitions.put("equal", equal);
|
107 |
| |
108 |
0
| final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
|
109 |
0
| notEqual.setArgumentNumber("2");
|
110 |
0
| notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
|
111 |
0
| definitions.put("notEqual", notEqual);
|
112 |
| } |
113 |
| |
114 |
| |
115 |
| |
116 |
| |
117 |
| |
118 |
| |
119 |
| |
120 |
| |
121 |
| |
122 |
0
| public final synchronized void printWiki(final String language, final String level,
|
123 |
| final File outputDirectory) throws IOException { |
124 |
0
| if (language == null) {
|
125 |
0
| this.language = "en";
|
126 |
| } else { |
127 |
0
| this.language = language;
|
128 |
| } |
129 |
0
| if (level == null) {
|
130 |
0
| this.level = "1";
|
131 |
| } else { |
132 |
0
| this.level = level;
|
133 |
| } |
134 |
0
| this.outputDirectory = outputDirectory;
|
135 |
0
| printQedeqChapters();
|
136 |
0
| printQedeqBibliography();
|
137 |
0
| if (printer.checkError()) {
|
138 |
0
| throw new IOException("TODO mime: better use another OutputStream");
|
139 |
| } |
140 |
| } |
141 |
| |
142 |
| |
143 |
| |
144 |
| |
145 |
| |
146 |
| |
147 |
0
| private void printQedeqChapters() throws IOException {
|
148 |
0
| final ChapterList chapters = qedeq.getChapterList();
|
149 |
0
| for (int i = 0; i < chapters.size(); i++) {
|
150 |
0
| final String label = qedeq.getHeader().getSpecification().getName() + "_ch_" + i;
|
151 |
0
| final OutputStream outputStream = new FileOutputStream(new File(outputDirectory,
|
152 |
| label + "_" + language + ".wiki")); |
153 |
0
| this.printer = new PrintStream(outputStream);
|
154 |
0
| final Chapter chapter = chapters.get(i);
|
155 |
0
| printer.print("\\chapter");
|
156 |
0
| if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
|
157 |
0
| printer.print("*");
|
158 |
| } |
159 |
0
| printer.println("== " + getLatexListEntry(chapter.getTitle()) + " ==");
|
160 |
0
| printer.println();
|
161 |
0
| printer.println("<div id=\"" + label + "\"></div>");
|
162 |
| |
163 |
0
| printer.println();
|
164 |
0
| if (chapter.getIntroduction() != null) {
|
165 |
0
| printer.println(getLatexListEntry(chapter.getIntroduction()));
|
166 |
0
| printer.println();
|
167 |
| } |
168 |
0
| final SectionList sections = chapter.getSectionList();
|
169 |
0
| if (sections != null) {
|
170 |
0
| printSections(i, sections);
|
171 |
0
| printer.println();
|
172 |
| } |
173 |
0
| printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
|
174 |
0
| printer.println();
|
175 |
| } |
176 |
| } |
177 |
| |
178 |
| |
179 |
| |
180 |
| |
181 |
0
| private void printQedeqBibliography() {
|
182 |
0
| final LiteratureItemList items = qedeq.getLiteratureItemList();
|
183 |
0
| if (items == null) {
|
184 |
0
| return;
|
185 |
| } |
186 |
0
| printer.println("\\begin{thebibliography}{99}");
|
187 |
0
| for (int i = 0; i < items.size(); i++) {
|
188 |
0
| final LiteratureItem item = items.get(i);
|
189 |
0
| printer.print("\\bibitem{" + item.getLabel() + "} ");
|
190 |
0
| printer.println(getLatexListEntry(item.getItem()));
|
191 |
0
| printer.println();
|
192 |
| } |
193 |
0
| printer.println("\\end{thebibliography}");
|
194 |
0
| printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
|
195 |
| } |
196 |
| |
197 |
| |
198 |
| |
199 |
| |
200 |
| |
201 |
| |
202 |
| |
203 |
0
| private void printSections(final int chapter, final SectionList sections) {
|
204 |
0
| if (sections == null) {
|
205 |
0
| return;
|
206 |
| } |
207 |
0
| for (int i = 0; i < sections.size(); i++) {
|
208 |
0
| final Section section = sections.get(i);
|
209 |
0
| printer.print("\\section{");
|
210 |
0
| printer.print(getLatexListEntry(section.getTitle()));
|
211 |
0
| final String label = "chapter" + chapter + "_section" + i;
|
212 |
0
| printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
|
213 |
0
| printer.println(getLatexListEntry(section.getIntroduction()));
|
214 |
0
| printer.println();
|
215 |
0
| printSubsections(section.getSubsectionList());
|
216 |
| } |
217 |
| } |
218 |
| |
219 |
| |
220 |
| |
221 |
| |
222 |
| |
223 |
| |
224 |
0
| private void printSubsections(final SubsectionList nodes) {
|
225 |
0
| if (nodes == null) {
|
226 |
0
| return;
|
227 |
| } |
228 |
0
| for (int i = 0; i < nodes.size(); i++) {
|
229 |
0
| final SubsectionType subsectionType = nodes.get(i);
|
230 |
0
| if (subsectionType instanceof Node) {
|
231 |
0
| final Node node = (Node) subsectionType;
|
232 |
0
| printer.println(getLatexListEntry(node.getPrecedingText()));
|
233 |
0
| printer.println();
|
234 |
0
| printer.println("\\par");
|
235 |
0
| final String id = node.getId();
|
236 |
0
| final NodeType type = node.getNodeType();
|
237 |
0
| String title = null;
|
238 |
0
| if (node.getTitle() != null) {
|
239 |
0
| title = getLatexListEntry(node.getTitle());
|
240 |
| } |
241 |
0
| if (type instanceof Axiom) {
|
242 |
0
| printAxiom((Axiom) type, title, id);
|
243 |
0
| } else if (type instanceof PredicateDefinition) {
|
244 |
0
| printPredicateDefinition((PredicateDefinition) type, title, id);
|
245 |
0
| } else if (type instanceof FunctionDefinition) {
|
246 |
0
| printFunctionDefinition((FunctionDefinition) type, title, id);
|
247 |
0
| } else if (type instanceof Proposition) {
|
248 |
0
| printProposition((Proposition) type, title, id);
|
249 |
0
| } else if (type instanceof Rule) {
|
250 |
0
| printRule((Rule) type, title, id);
|
251 |
| } else { |
252 |
0
| throw new RuntimeException((type != null ? "unknown type: "
|
253 |
| + type.getClass().getName() : "node type empty")); |
254 |
| } |
255 |
0
| printer.println();
|
256 |
0
| printer.println(getLatexListEntry(node.getSucceedingText()));
|
257 |
| } else { |
258 |
0
| final Subsection subsection = (Subsection) subsectionType;
|
259 |
0
| if (subsection.getTitle() != null) {
|
260 |
0
| printer.print("\\subsection{");
|
261 |
0
| printer.println(getLatexListEntry(subsection.getTitle()));
|
262 |
0
| printer.println("}");
|
263 |
| } |
264 |
0
| printer.println(getLatexListEntry(subsection.getLatex()));
|
265 |
| } |
266 |
0
| printer.println();
|
267 |
0
| printer.println();
|
268 |
| } |
269 |
| } |
270 |
| |
271 |
| |
272 |
| |
273 |
| |
274 |
| |
275 |
| |
276 |
| |
277 |
| |
278 |
0
| private void printAxiom(final Axiom axiom, final String title, final String id) {
|
279 |
0
| printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
|
280 |
0
| printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
|
281 |
0
| printFormula(axiom.getFormula().getElement());
|
282 |
0
| printer.println(getLatexListEntry(axiom.getDescription()));
|
283 |
0
| printer.println("\\end{ax}");
|
284 |
| } |
285 |
| |
286 |
| |
287 |
| |
288 |
| |
289 |
| |
290 |
| |
291 |
| |
292 |
| |
293 |
0
| private void printTopFormula(final Element element, final String mainLabel) {
|
294 |
0
| if (!element.isList() || !element.getList().getOperator().equals("AND")) {
|
295 |
0
| printFormula(element);
|
296 |
0
| return;
|
297 |
| } |
298 |
0
| final ElementList list = element.getList();
|
299 |
0
| printer.println("\\mbox{}");
|
300 |
0
| printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
|
301 |
0
| for (int i = 0; i < list.size(); i++) {
|
302 |
0
| final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
|
303 |
0
| printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
|
304 |
| + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":" |
305 |
| + label + "}{} \\mbox{\\emph{(" + label + ")}} " |
306 |
0
| + (i + 1 < list.size() ? "\\\\" : ""));
|
307 |
| } |
308 |
0
| printer.println("\\end{longtable}");
|
309 |
| } |
310 |
| |
311 |
| |
312 |
| |
313 |
| |
314 |
| |
315 |
| |
316 |
0
| private void printFormula(final Element element) {
|
317 |
0
| printer.println("\\mbox{}");
|
318 |
0
| printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
|
319 |
0
| printer.println("\\centering $" + getLatex(element) + "$");
|
320 |
0
| printer.println("\\end{longtable}");
|
321 |
| } |
322 |
| |
323 |
| |
324 |
| |
325 |
| |
326 |
| |
327 |
| |
328 |
| |
329 |
| |
330 |
0
| private void printPredicateDefinition(final PredicateDefinition definition, final String title,
|
331 |
| final String id) { |
332 |
0
| final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
|
333 |
0
| final VariableList list = definition.getVariableList();
|
334 |
0
| if (list != null) {
|
335 |
0
| for (int i = list.size() - 1; i >= 0; i--) {
|
336 |
0
| Trace.trace(this, "printDefinition", "replacing!");
|
337 |
0
| ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
|
338 |
| } |
339 |
| } |
340 |
0
| if (definition.getFormula() != null) {
|
341 |
0
| printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
|
342 |
0
| printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
|
343 |
0
| define.append("\\ :\\leftrightarrow \\ ");
|
344 |
0
| define.append(getLatex(definition.getFormula().getElement()));
|
345 |
| } else { |
346 |
0
| printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
|
347 |
0
| printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
|
348 |
| } |
349 |
0
| define.append("$$");
|
350 |
0
| definitions.put(id, definition);
|
351 |
0
| Trace.param(this, "printDefinition", "define", define);
|
352 |
0
| printer.println(define);
|
353 |
0
| printer.println(getLatexListEntry(definition.getDescription()));
|
354 |
0
| if (definition.getFormula() != null) {
|
355 |
0
| printer.println("\\end{defn}");
|
356 |
| } else { |
357 |
0
| printer.println("\\end{idefn}");
|
358 |
| } |
359 |
| } |
360 |
| |
361 |
| |
362 |
| |
363 |
| |
364 |
| |
365 |
| |
366 |
| |
367 |
| |
368 |
0
| private void printFunctionDefinition(final FunctionDefinition definition, final String title,
|
369 |
| final String id) { |
370 |
0
| final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
|
371 |
0
| final VariableList list = definition.getVariableList();
|
372 |
0
| if (list != null) {
|
373 |
0
| for (int i = list.size() - 1; i >= 0; i--) {
|
374 |
0
| Trace.trace(this, "printDefinition", "replacing!");
|
375 |
0
| ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
|
376 |
| } |
377 |
| } |
378 |
0
| if (definition.getTerm() != null) {
|
379 |
0
| printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
|
380 |
0
| printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
|
381 |
0
| define.append("\\ := \\ ");
|
382 |
0
| define.append(getLatex(definition.getTerm().getElement()));
|
383 |
| } else { |
384 |
0
| printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
|
385 |
0
| printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
|
386 |
| } |
387 |
0
| define.append("$$");
|
388 |
0
| definitions.put(id, definition);
|
389 |
0
| Trace.param(this, "printDefinition", "define", define);
|
390 |
0
| printer.println(define);
|
391 |
0
| printer.println(getLatexListEntry(definition.getDescription()));
|
392 |
0
| if (definition.getTerm() != null) {
|
393 |
0
| printer.println("\\end{defn}");
|
394 |
| } else { |
395 |
0
| printer.println("\\end{idefn}");
|
396 |
| } |
397 |
| } |
398 |
| |
399 |
| |
400 |
| |
401 |
| |
402 |
| |
403 |
| |
404 |
| |
405 |
| |
406 |
0
| private void printProposition(final Proposition proposition, final String title,
|
407 |
| final String id) { |
408 |
0
| printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
|
409 |
0
| printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
|
410 |
0
| printTopFormula(proposition.getFormula().getElement(), id);
|
411 |
0
| printer.println(getLatexListEntry(proposition.getDescription()));
|
412 |
0
| printer.println("\\end{prop}");
|
413 |
0
| if (proposition.getProofList() != null) {
|
414 |
0
| for (int i = 0; i < proposition.getProofList().size(); i++) {
|
415 |
0
| printer.println("\\begin{proof}");
|
416 |
0
| printer.println(getLatexListEntry(proposition.getProofList().get(i)
|
417 |
| .getNonFormalProof())); |
418 |
0
| printer.println("\\end{proof}");
|
419 |
| } |
420 |
| } |
421 |
| } |
422 |
| |
423 |
| |
424 |
| |
425 |
| |
426 |
| |
427 |
| |
428 |
| |
429 |
| |
430 |
0
| private void printRule(final Rule rule, final String title,
|
431 |
| final String id) { |
432 |
0
| printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
|
433 |
0
| printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
|
434 |
0
| printer.println(getLatexListEntry(rule.getDescription()));
|
435 |
0
| printer.println("\\end{rul}");
|
436 |
| |
437 |
| |
438 |
| |
439 |
| |
440 |
| |
441 |
| |
442 |
| |
443 |
| |
444 |
| |
445 |
| |
446 |
| |
447 |
| |
448 |
| |
449 |
| |
450 |
0
| if (rule.getProofList() != null) {
|
451 |
0
| for (int i = 0; i < rule.getProofList().size(); i++) {
|
452 |
0
| printer.println("\\begin{proof}");
|
453 |
0
| printer.println(getLatexListEntry(rule.getProofList().get(i)
|
454 |
| .getNonFormalProof())); |
455 |
0
| printer.println("\\end{proof}");
|
456 |
| } |
457 |
| } |
458 |
| } |
459 |
| |
460 |
| |
461 |
| |
462 |
| |
463 |
| |
464 |
| |
465 |
| |
466 |
0
| private String getLatex(final Element element) {
|
467 |
0
| return getLatex(element, true);
|
468 |
| } |
469 |
| |
470 |
| |
471 |
| |
472 |
| |
473 |
| |
474 |
| |
475 |
| |
476 |
| |
477 |
0
| private String getLatex(final Element element, final boolean first) {
|
478 |
0
| final StringBuffer buffer = new StringBuffer();
|
479 |
0
| if (element.isAtom()) {
|
480 |
0
| return element.getAtom().getString();
|
481 |
| } |
482 |
0
| final ElementList list = element.getList();
|
483 |
0
| if (list.getOperator().equals("PREDCON")) {
|
484 |
0
| final String identifier = list.getElement(0).getAtom().getString();
|
485 |
0
| if (definitions.containsKey(identifier)) {
|
486 |
0
| final PredicateDefinition definition
|
487 |
| = (PredicateDefinition) definitions.get(identifier); |
488 |
0
| final StringBuffer define = new StringBuffer(definition.getLatexPattern());
|
489 |
0
| for (int i = list.size() - 1; i >= 1; i--) {
|
490 |
0
| ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
|
491 |
| } |
492 |
0
| buffer.append(define);
|
493 |
| } else { |
494 |
0
| buffer.append(identifier);
|
495 |
0
| buffer.append("(");
|
496 |
0
| for (int i = 1; i < list.size(); i++) {
|
497 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
498 |
0
| if (i + 1 < list.size()) {
|
499 |
0
| buffer.append(", ");
|
500 |
| } |
501 |
| } |
502 |
0
| buffer.append(")");
|
503 |
| } |
504 |
0
| } else if (list.getOperator().equals("PREDVAR")) {
|
505 |
0
| final String identifier = list.getElement(0).getAtom().getString();
|
506 |
0
| buffer.append(identifier);
|
507 |
0
| if (list.size() > 1) {
|
508 |
0
| buffer.append("(");
|
509 |
0
| for (int i = 1; i < list.size(); i++) {
|
510 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
511 |
0
| if (i + 1 < list.size()) {
|
512 |
0
| buffer.append(", ");
|
513 |
| } |
514 |
| } |
515 |
0
| buffer.append(")");
|
516 |
| } |
517 |
0
| } else if (list.getOperator().equals("FUNCON")) {
|
518 |
0
| final String identifier = list.getElement(0).getAtom().getString();
|
519 |
0
| if (definitions.containsKey(identifier)) {
|
520 |
0
| final FunctionDefinition definition
|
521 |
| = (FunctionDefinition) definitions.get(identifier); |
522 |
0
| final StringBuffer define = new StringBuffer(definition.getLatexPattern());
|
523 |
0
| for (int i = list.size() - 1; i >= 1; i--) {
|
524 |
0
| ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
|
525 |
| } |
526 |
0
| buffer.append(define);
|
527 |
| } else { |
528 |
0
| buffer.append(identifier);
|
529 |
0
| buffer.append("(");
|
530 |
0
| for (int i = 1; i < list.size(); i++) {
|
531 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
532 |
0
| if (i + 1 < list.size()) {
|
533 |
0
| buffer.append(", ");
|
534 |
| } |
535 |
| } |
536 |
0
| buffer.append(")");
|
537 |
| } |
538 |
0
| } else if (list.getOperator().equals("FUNVAR")) {
|
539 |
0
| final String identifier = list.getElement(0).getAtom().getString();
|
540 |
0
| buffer.append(identifier);
|
541 |
0
| if (list.size() > 1) {
|
542 |
0
| buffer.append("(");
|
543 |
0
| for (int i = 1; i < list.size(); i++) {
|
544 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
545 |
0
| if (i + 1 < list.size()) {
|
546 |
0
| buffer.append(", ");
|
547 |
| } |
548 |
| } |
549 |
0
| buffer.append(")");
|
550 |
| } |
551 |
0
| } else if (list.getOperator().equals("VAR")) {
|
552 |
0
| final String text = list.getElement(0).getAtom().getString();
|
553 |
0
| try {
|
554 |
0
| final int index = Integer.parseInt(text);
|
555 |
0
| switch (index) {
|
556 |
0
| case 1:
|
557 |
0
| return "x";
|
558 |
0
| case 2:
|
559 |
0
| return "y";
|
560 |
0
| case 3:
|
561 |
0
| return "z";
|
562 |
0
| case 4:
|
563 |
0
| return "u";
|
564 |
0
| case 5:
|
565 |
0
| return "v";
|
566 |
0
| case 6:
|
567 |
0
| return "w";
|
568 |
0
| default:
|
569 |
0
| return "x_" + (index - 6);
|
570 |
| } |
571 |
| } catch (NumberFormatException e) { |
572 |
0
| return text;
|
573 |
| } |
574 |
0
| } else if (list.getOperator().equals("AND") || list.getOperator().equals("OR")
|
575 |
| || list.getOperator().equals("EQUI") || list.getOperator().equals("IMPL")) { |
576 |
0
| final String infix;
|
577 |
0
| if (list.getOperator().equals("AND")) {
|
578 |
0
| infix = "\\ \\land \\ ";
|
579 |
0
| } else if (list.getOperator().equals("OR")) {
|
580 |
0
| infix = "\\ \\lor \\ ";
|
581 |
0
| } else if (list.getOperator().equals("EQUI")) {
|
582 |
0
| infix = "\\ \\leftrightarrow \\ ";
|
583 |
| } else { |
584 |
0
| infix = "\\ \\rightarrow \\ ";
|
585 |
| } |
586 |
0
| if (!first) {
|
587 |
0
| buffer.append("(");
|
588 |
| } |
589 |
0
| for (int i = 0; i < list.size(); i++) {
|
590 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
591 |
0
| if (i + 1 < list.size()) {
|
592 |
0
| buffer.append(infix);
|
593 |
| } |
594 |
| } |
595 |
0
| if (!first) {
|
596 |
0
| buffer.append(")");
|
597 |
| } |
598 |
0
| } else if (list.getOperator().equals("FORALL") || list.getOperator().equals("EXISTS")
|
599 |
| || list.getOperator().equals("EXISTSU")) { |
600 |
0
| final String prefix;
|
601 |
0
| if (list.getOperator().equals("FORALL")) {
|
602 |
0
| prefix = "\\forall ";
|
603 |
0
| } else if (list.getOperator().equals("EXISTS")) {
|
604 |
0
| prefix = "\\exists ";
|
605 |
| } else { |
606 |
0
| prefix = "\\exists! ";
|
607 |
| } |
608 |
0
| buffer.append(prefix);
|
609 |
0
| for (int i = 0; i < list.size(); i++) {
|
610 |
0
| if (i != 0 || (i == 0 && list.size() <= 2)) {
|
611 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
612 |
| } |
613 |
0
| if (i + 1 < list.size()) {
|
614 |
0
| buffer.append("\\ ");
|
615 |
| } |
616 |
0
| if (list.size() > 2 && i == 1) {
|
617 |
0
| buffer.append("\\ ");
|
618 |
| } |
619 |
| } |
620 |
0
| } else if (list.getOperator().equals("NOT")) {
|
621 |
0
| final String prefix = "\\neg ";
|
622 |
0
| buffer.append(prefix);
|
623 |
0
| for (int i = 0; i < list.size(); i++) {
|
624 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
625 |
| } |
626 |
0
| } else if (list.getOperator().equals("CLASS")) {
|
627 |
0
| final String prefix = "\\{ ";
|
628 |
0
| buffer.append(prefix);
|
629 |
0
| for (int i = 0; i < list.size(); i++) {
|
630 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
631 |
0
| if (i + 1 < list.size()) {
|
632 |
0
| buffer.append(" \\ | \\ ");
|
633 |
| } |
634 |
| } |
635 |
0
| buffer.append(" \\} ");
|
636 |
0
| } else if (list.getOperator().equals("CLASSLIST")) {
|
637 |
0
| final String prefix = "\\{ ";
|
638 |
0
| buffer.append(prefix);
|
639 |
0
| for (int i = 0; i < list.size(); i++) {
|
640 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
641 |
0
| if (i + 1 < list.size()) {
|
642 |
0
| buffer.append(", \\ ");
|
643 |
| } |
644 |
| } |
645 |
0
| buffer.append(" \\} ");
|
646 |
0
| } else if (list.getOperator().equals("QUANTOR_INTERSECTION")) {
|
647 |
0
| final String prefix = "\\bigcap";
|
648 |
0
| buffer.append(prefix);
|
649 |
0
| if (0 < list.size()) {
|
650 |
0
| buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
|
651 |
| } |
652 |
0
| for (int i = 1; i < list.size(); i++) {
|
653 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
654 |
0
| if (i + 1 < list.size()) {
|
655 |
0
| buffer.append(" \\ \\ ");
|
656 |
| } |
657 |
| } |
658 |
0
| buffer.append(" \\} ");
|
659 |
0
| } else if (list.getOperator().equals("QUANTOR_UNION")) {
|
660 |
0
| final String prefix = "\\bigcup";
|
661 |
0
| buffer.append(prefix);
|
662 |
0
| if (0 < list.size()) {
|
663 |
0
| buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
|
664 |
| } |
665 |
0
| for (int i = 1; i < list.size(); i++) {
|
666 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
667 |
0
| if (i + 1 < list.size()) {
|
668 |
0
| buffer.append(" \\ \\ ");
|
669 |
| } |
670 |
| } |
671 |
0
| buffer.append(" \\} ");
|
672 |
| } else { |
673 |
0
| buffer.append(list.getOperator());
|
674 |
0
| buffer.append("(");
|
675 |
0
| for (int i = 0; i < list.size(); i++) {
|
676 |
0
| buffer.append(getLatex(list.getElement(i), false));
|
677 |
0
| if (i + 1 < list.size()) {
|
678 |
0
| buffer.append(", ");
|
679 |
| } |
680 |
| } |
681 |
0
| buffer.append(")");
|
682 |
| } |
683 |
0
| return buffer.toString();
|
684 |
| } |
685 |
| |
686 |
| |
687 |
| |
688 |
| |
689 |
| |
690 |
| |
691 |
| |
692 |
| |
693 |
| |
694 |
0
| private String getLatexListEntry(final LatexList list) {
|
695 |
0
| if (list == null) {
|
696 |
0
| return "";
|
697 |
| } |
698 |
0
| for (int i = 0; i < list.size(); i++) {
|
699 |
0
| if (language.equals(list.get(i).getLanguage())) {
|
700 |
0
| return getLatex(list.get(i));
|
701 |
| } |
702 |
| } |
703 |
| |
704 |
0
| for (int i = 0; i < list.size(); i++) {
|
705 |
0
| if (list.get(i).getLanguage() == null) {
|
706 |
0
| return getLatex(list.get(i));
|
707 |
| } |
708 |
| } |
709 |
0
| for (int i = 0; i < list.size(); i++) {
|
710 |
0
| return "MISSING! OTHER: " + getLatex(list.get(i));
|
711 |
| } |
712 |
0
| return "MISSING!";
|
713 |
| } |
714 |
| |
715 |
| |
716 |
| |
717 |
| |
718 |
| |
719 |
| |
720 |
| |
721 |
| |
722 |
0
| private String getLatex(final Latex latex) {
|
723 |
0
| return LatexTextParser.transform(latex.getLatex());
|
724 |
| } |
725 |
| |
726 |
| } |