1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.bo.service.basis;
17
18 import org.qedeq.kernel.se.base.list.Atom;
19 import org.qedeq.kernel.se.base.list.Element;
20 import org.qedeq.kernel.se.base.list.ElementList;
21 import org.qedeq.kernel.se.base.module.Add;
22 import org.qedeq.kernel.se.base.module.Author;
23 import org.qedeq.kernel.se.base.module.AuthorList;
24 import org.qedeq.kernel.se.base.module.Axiom;
25 import org.qedeq.kernel.se.base.module.ChangedRule;
26 import org.qedeq.kernel.se.base.module.ChangedRuleList;
27 import org.qedeq.kernel.se.base.module.Chapter;
28 import org.qedeq.kernel.se.base.module.ChapterList;
29 import org.qedeq.kernel.se.base.module.Conclusion;
30 import org.qedeq.kernel.se.base.module.ConditionalProof;
31 import org.qedeq.kernel.se.base.module.Existential;
32 import org.qedeq.kernel.se.base.module.FormalProof;
33 import org.qedeq.kernel.se.base.module.FormalProofLine;
34 import org.qedeq.kernel.se.base.module.FormalProofLineList;
35 import org.qedeq.kernel.se.base.module.FormalProofList;
36 import org.qedeq.kernel.se.base.module.Formula;
37 import org.qedeq.kernel.se.base.module.FunctionDefinition;
38 import org.qedeq.kernel.se.base.module.Header;
39 import org.qedeq.kernel.se.base.module.Hypothesis;
40 import org.qedeq.kernel.se.base.module.Import;
41 import org.qedeq.kernel.se.base.module.ImportList;
42 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
43 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
44 import org.qedeq.kernel.se.base.module.Latex;
45 import org.qedeq.kernel.se.base.module.LatexList;
46 import org.qedeq.kernel.se.base.module.LinkList;
47 import org.qedeq.kernel.se.base.module.LiteratureItem;
48 import org.qedeq.kernel.se.base.module.LiteratureItemList;
49 import org.qedeq.kernel.se.base.module.Location;
50 import org.qedeq.kernel.se.base.module.LocationList;
51 import org.qedeq.kernel.se.base.module.ModusPonens;
52 import org.qedeq.kernel.se.base.module.Node;
53 import org.qedeq.kernel.se.base.module.PredicateDefinition;
54 import org.qedeq.kernel.se.base.module.Proof;
55 import org.qedeq.kernel.se.base.module.ProofList;
56 import org.qedeq.kernel.se.base.module.Proposition;
57 import org.qedeq.kernel.se.base.module.Qedeq;
58 import org.qedeq.kernel.se.base.module.Reason;
59 import org.qedeq.kernel.se.base.module.Rename;
60 import org.qedeq.kernel.se.base.module.Rule;
61 import org.qedeq.kernel.se.base.module.Section;
62 import org.qedeq.kernel.se.base.module.SectionList;
63 import org.qedeq.kernel.se.base.module.Specification;
64 import org.qedeq.kernel.se.base.module.Subsection;
65 import org.qedeq.kernel.se.base.module.SubsectionList;
66 import org.qedeq.kernel.se.base.module.SubstFree;
67 import org.qedeq.kernel.se.base.module.SubstFunc;
68 import org.qedeq.kernel.se.base.module.SubstPred;
69 import org.qedeq.kernel.se.base.module.Universal;
70 import org.qedeq.kernel.se.base.module.UsedByList;
71 import org.qedeq.kernel.se.common.IllegalModuleDataException;
72 import org.qedeq.kernel.se.common.ModuleAddress;
73 import org.qedeq.kernel.se.common.ModuleContext;
74 import org.qedeq.kernel.se.common.ModuleDataException;
75 import org.qedeq.kernel.se.dto.list.DefaultAtom;
76 import org.qedeq.kernel.se.dto.list.DefaultElementList;
77 import org.qedeq.kernel.se.dto.module.AddVo;
78 import org.qedeq.kernel.se.dto.module.AuthorListVo;
79 import org.qedeq.kernel.se.dto.module.AuthorVo;
80 import org.qedeq.kernel.se.dto.module.AxiomVo;
81 import org.qedeq.kernel.se.dto.module.ChangedRuleListVo;
82 import org.qedeq.kernel.se.dto.module.ChangedRuleVo;
83 import org.qedeq.kernel.se.dto.module.ChapterListVo;
84 import org.qedeq.kernel.se.dto.module.ChapterVo;
85 import org.qedeq.kernel.se.dto.module.ConclusionVo;
86 import org.qedeq.kernel.se.dto.module.ConditionalProofVo;
87 import org.qedeq.kernel.se.dto.module.ExistentialVo;
88 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
89 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
90 import org.qedeq.kernel.se.dto.module.FormalProofListVo;
91 import org.qedeq.kernel.se.dto.module.FormalProofVo;
92 import org.qedeq.kernel.se.dto.module.FormulaVo;
93 import org.qedeq.kernel.se.dto.module.FunctionDefinitionVo;
94 import org.qedeq.kernel.se.dto.module.HeaderVo;
95 import org.qedeq.kernel.se.dto.module.HypothesisVo;
96 import org.qedeq.kernel.se.dto.module.ImportListVo;
97 import org.qedeq.kernel.se.dto.module.ImportVo;
98 import org.qedeq.kernel.se.dto.module.InitialFunctionDefinitionVo;
99 import org.qedeq.kernel.se.dto.module.InitialPredicateDefinitionVo;
100 import org.qedeq.kernel.se.dto.module.LatexListVo;
101 import org.qedeq.kernel.se.dto.module.LatexVo;
102 import org.qedeq.kernel.se.dto.module.LinkListVo;
103 import org.qedeq.kernel.se.dto.module.LiteratureItemListVo;
104 import org.qedeq.kernel.se.dto.module.LiteratureItemVo;
105 import org.qedeq.kernel.se.dto.module.LocationListVo;
106 import org.qedeq.kernel.se.dto.module.LocationVo;
107 import org.qedeq.kernel.se.dto.module.ModusPonensVo;
108 import org.qedeq.kernel.se.dto.module.NodeVo;
109 import org.qedeq.kernel.se.dto.module.PredicateDefinitionVo;
110 import org.qedeq.kernel.se.dto.module.ProofListVo;
111 import org.qedeq.kernel.se.dto.module.ProofVo;
112 import org.qedeq.kernel.se.dto.module.PropositionVo;
113 import org.qedeq.kernel.se.dto.module.QedeqVo;
114 import org.qedeq.kernel.se.dto.module.RenameVo;
115 import org.qedeq.kernel.se.dto.module.RuleVo;
116 import org.qedeq.kernel.se.dto.module.SectionListVo;
117 import org.qedeq.kernel.se.dto.module.SectionVo;
118 import org.qedeq.kernel.se.dto.module.SpecificationVo;
119 import org.qedeq.kernel.se.dto.module.SubsectionListVo;
120 import org.qedeq.kernel.se.dto.module.SubsectionVo;
121 import org.qedeq.kernel.se.dto.module.SubstFreeVo;
122 import org.qedeq.kernel.se.dto.module.SubstFuncVo;
123 import org.qedeq.kernel.se.dto.module.SubstPredVo;
124 import org.qedeq.kernel.se.dto.module.UniversalVo;
125 import org.qedeq.kernel.se.dto.module.UsedByListVo;
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141 public class QedeqVoBuilder {
142
143
144 private Qedeq original;
145
146
147 private ModuleContext currentContext;
148
149
150
151
152
153
154 protected QedeqVoBuilder(final ModuleAddress address) {
155 this.currentContext = address.createModuleContext();
156 }
157
158
159
160
161
162
163
164
165
166
167
168
169
170 public static QedeqVo createQedeq(final ModuleAddress address,
171 final Qedeq original) throws ModuleDataException {
172 final QedeqVoBuilder creator = new QedeqVoBuilder(address);
173 QedeqVo vo = creator.create(original);
174 return vo;
175 }
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191 protected final QedeqVo create(final Qedeq original) throws IllegalModuleDataException {
192 this.original = original;
193 getCurrentContext().setLocationWithinModule("");
194 QedeqVo qedeq;
195 if (original == null) {
196 qedeq = null;
197 return qedeq;
198 }
199 qedeq = new QedeqVo();
200 final String context = getCurrentContext().getLocationWithinModule();
201 if (original.getHeader() != null) {
202 getCurrentContext().setLocationWithinModule(context + "getHeader()");
203 qedeq.setHeader(create(original.getHeader()));
204 }
205 if (original.getChapterList() != null) {
206 getCurrentContext().setLocationWithinModule(context + "getChapterList()");
207 qedeq.setChapterList(create(original.getChapterList()));
208 }
209 if (original.getLiteratureItemList() != null) {
210 getCurrentContext().setLocationWithinModule(context + "getLiteratureItemList()");
211 qedeq.setLiteratureItemList(create(original.getLiteratureItemList()));
212 }
213 return qedeq;
214 }
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229 private final HeaderVo create(final Header header)
230 throws IllegalModuleDataException {
231 if (header == null) {
232 return null;
233 }
234 final HeaderVo h = new HeaderVo();
235 final String context = getCurrentContext().getLocationWithinModule();
236 if (header.getTitle() != null) {
237 setLocationWithinModule(context + ".getTitle()");
238 h.setTitle(create(header.getTitle()));
239 }
240 if (header.getAuthorList() != null) {
241 setLocationWithinModule(context + ".getAuthorList()");
242 h.setAuthorList(create(header.getAuthorList()));
243 }
244 if (header.getSummary() != null) {
245 setLocationWithinModule(context + ".getSummary()");
246 h.setSummary(create(header.getSummary()));
247 }
248 if (header.getEmail() != null) {
249 setLocationWithinModule(context + ".getEmail()");
250 h.setEmail(header.getEmail());
251 }
252 if (header.getSpecification() != null) {
253 setLocationWithinModule(context + ".getSpecification()");
254 h.setSpecification(create(header.getSpecification()));
255 }
256 if (header.getImportList() != null) {
257 setLocationWithinModule(context + ".getImportList()");
258 h.setImportList(create(header.getImportList()));
259 }
260 if (header.getUsedByList() != null) {
261 setLocationWithinModule(context + ".getUsedByList()");
262 h.setUsedByList(create(header.getUsedByList()));
263 }
264 setLocationWithinModule(context);
265 return h;
266 }
267
268
269
270
271
272
273
274
275
276
277
278
279
280 private final UsedByListVo create(final UsedByList usedByList) {
281 if (usedByList == null) {
282 return null;
283 }
284 final String context = getCurrentContext().getLocationWithinModule();
285 final UsedByListVo list = new UsedByListVo();
286 for (int i = 0; i < usedByList.size(); i++) {
287 setLocationWithinModule(context + ".get(" + i + ")");
288 list.add(create(usedByList.get(i)));
289 }
290 setLocationWithinModule(context);
291 return list;
292 }
293
294 private final ImportListVo create(final ImportList importList) {
295 if (importList == null) {
296 return null;
297 }
298 final String context = getCurrentContext().getLocationWithinModule();
299 final ImportListVo list = new ImportListVo();
300 for (int i = 0; i < importList.size(); i++) {
301 setLocationWithinModule(context + ".get(" + i + ")");
302 list.add(create(importList.get(i)));
303 }
304 setLocationWithinModule(context);
305 return list;
306 }
307
308 private final ImportVo create(final Import imp) {
309 if (imp == null) {
310 return null;
311 }
312 final ImportVo i = new ImportVo();
313 final String context = getCurrentContext().getLocationWithinModule();
314 if (imp.getLabel() != null) {
315 setLocationWithinModule(context + ".getLabel()");
316 i.setLabel(imp.getLabel());
317 }
318 if (imp.getSpecification() != null) {
319 setLocationWithinModule(context + ".getSpecification()");
320 i.setSpecification(create(imp.getSpecification()));
321 }
322 setLocationWithinModule(context);
323 return i;
324 }
325
326 private final SpecificationVo create(final Specification specification) {
327 if (specification == null) {
328 return null;
329 }
330 final SpecificationVo s = new SpecificationVo();
331 final String context = getCurrentContext().getLocationWithinModule();
332 if (specification.getName() != null) {
333 setLocationWithinModule(context + ".getName()");
334 s.setName(specification.getName());
335 }
336 if (specification.getRuleVersion() != null) {
337 setLocationWithinModule(context + ".getRuleVersion()");
338 s.setRuleVersion(specification.getRuleVersion());
339 }
340 if (specification.getLocationList() != null) {
341 setLocationWithinModule(context + ".getLocationList()");
342 s.setLocationList(create(specification.getLocationList()));
343 }
344 setLocationWithinModule(context);
345 return s;
346 }
347
348 private final LocationListVo create(final LocationList locationList) {
349 if (locationList == null) {
350 return null;
351 }
352 final LocationListVo list = new LocationListVo();
353 final String context = getCurrentContext().getLocationWithinModule();
354 for (int i = 0; i < locationList.size(); i++) {
355 setLocationWithinModule(context + ".get(" + i + ")");
356 list.add(create(locationList.get(i)));
357 }
358 setLocationWithinModule(context);
359 return list;
360 }
361
362 private final LocationVo create(final Location location) {
363 if (location == null) {
364 return null;
365 }
366 final LocationVo loc = new LocationVo();
367 final String context = getCurrentContext().getLocationWithinModule();
368 if (location.getLocation() != null) {
369 setLocationWithinModule(context + ".getLocation()");
370 loc.setLocation(location.getLocation());
371 }
372 setLocationWithinModule(context);
373 return loc;
374 }
375
376 private final AuthorListVo create(final AuthorList authorList) {
377 if (authorList == null) {
378 return null;
379 }
380 final AuthorListVo list = new AuthorListVo();
381 final String context = getCurrentContext().getLocationWithinModule();
382 for (int i = 0; i < authorList.size(); i++) {
383 setLocationWithinModule(context + ".get(" + i + ")");
384 list.add(create(authorList.get(i)));
385 }
386 setLocationWithinModule(context);
387 return list;
388 }
389
390 private final AuthorVo create(final Author author) {
391 if (author == null) {
392 return null;
393 }
394 final AuthorVo a = new AuthorVo();
395 final String context = getCurrentContext().getLocationWithinModule();
396 if (author.getName() != null) {
397 setLocationWithinModule(context + ".getName()");
398 a.setName(create(author.getName()));
399 }
400 if (author.getEmail() != null) {
401 setLocationWithinModule(context + ".getEmail()");
402 a.setEmail(author.getEmail());
403 }
404 setLocationWithinModule(context);
405 return a;
406 }
407
408 private final ChapterListVo create(final ChapterList chapterList)
409 throws IllegalModuleDataException {
410 if (chapterList == null) {
411 return null;
412 }
413 final ChapterListVo list = new ChapterListVo();
414 final String context = getCurrentContext().getLocationWithinModule();
415 for (int i = 0; i < chapterList.size(); i++) {
416 setLocationWithinModule(context + ".get(" + i + ")");
417 list.add(create(chapterList.get(i)));
418 }
419 setLocationWithinModule(context);
420 return list;
421 }
422
423 private final ChapterVo create(final Chapter chapter)
424 throws IllegalModuleDataException {
425 if (chapter == null) {
426 return null;
427 }
428 final ChapterVo c = new ChapterVo();
429 final String context = getCurrentContext().getLocationWithinModule();
430 if (chapter.getTitle() != null) {
431 setLocationWithinModule(context + ".getTitle()");
432 c.setTitle(create(chapter.getTitle()));
433 }
434 if (chapter.getNoNumber() != null) {
435 setLocationWithinModule(context + ".getNoNumber()");
436 c.setNoNumber(chapter.getNoNumber());
437 }
438 if (chapter.getIntroduction() != null) {
439 setLocationWithinModule(context + ".getIntroduction()");
440 c.setIntroduction(create(chapter.getIntroduction()));
441 }
442 if (chapter.getSectionList() != null) {
443 setLocationWithinModule(context + ".getSectionList()");
444 c.setSectionList(create(chapter.getSectionList()));
445 }
446 setLocationWithinModule(context);
447 return c;
448 }
449
450 private LiteratureItemListVo create(final LiteratureItemList literatureItemList) {
451 if (literatureItemList == null) {
452 return null;
453 }
454 final LiteratureItemListVo list = new LiteratureItemListVo();
455 final String context = getCurrentContext().getLocationWithinModule();
456 for (int i = 0; i < literatureItemList.size(); i++) {
457 setLocationWithinModule(context + ".get(" + i + ")");
458 list.add(create(literatureItemList.get(i)));
459 }
460 setLocationWithinModule(context);
461 return list;
462 }
463
464 private LiteratureItemVo create(final LiteratureItem item) {
465 if (item == null) {
466 return null;
467 }
468 final LiteratureItemVo it = new LiteratureItemVo();
469 final String context = getCurrentContext().getLocationWithinModule();
470 if (item.getLabel() != null) {
471 setLocationWithinModule(context + ".getLabel()");
472 it.setLabel(item.getLabel());
473 }
474 if (item.getItem() != null) {
475 setLocationWithinModule(context + ".getItem()");
476 it.setItem(create(item.getItem()));
477 }
478 setLocationWithinModule(context);
479 return it;
480
481 }
482
483 private final SectionListVo create(final SectionList sectionList)
484 throws IllegalModuleDataException {
485 if (sectionList == null) {
486 return null;
487 }
488 final SectionListVo list = new SectionListVo();
489 final String context = getCurrentContext().getLocationWithinModule();
490 for (int i = 0; i < sectionList.size(); i++) {
491 setLocationWithinModule(context + ".get(" + i + ")");
492 list.add(create(sectionList.get(i)));
493 }
494 setLocationWithinModule(context);
495 return list;
496 }
497
498 private final SectionVo create(final Section section)
499 throws IllegalModuleDataException {
500 if (section == null) {
501 return null;
502 }
503 final SectionVo s = new SectionVo();
504 final String context = getCurrentContext().getLocationWithinModule();
505 if (section.getTitle() != null) {
506 setLocationWithinModule(context + ".getTitle()");
507 s.setTitle(create(section.getTitle()));
508 }
509 if (section.getNoNumber() != null) {
510 setLocationWithinModule(context + ".getNoNumber()");
511 s.setNoNumber(section.getNoNumber());
512 }
513 if (section.getIntroduction() != null) {
514 setLocationWithinModule(context + ".getIntroduction()");
515 s.setIntroduction(create(section.getIntroduction()));
516 }
517 if (section.getSubsectionList() != null) {
518 setLocationWithinModule(context + ".getSubsectionList()");
519 s.setSubsectionList(create(section.getSubsectionList()));
520 }
521 setLocationWithinModule(context);
522 return s;
523 }
524
525 private final SubsectionListVo create(final SubsectionList subsectionList)
526 throws IllegalModuleDataException {
527 if (subsectionList == null) {
528 return null;
529 }
530 final SubsectionListVo list = new SubsectionListVo();
531 final String context = getCurrentContext().getLocationWithinModule();
532 for (int i = 0; i < subsectionList.size(); i++) {
533
534
535
536
537 if (subsectionList.get(i).getSubsection() != null) {
538 setLocationWithinModule(context + ".get(" + i + ").getSubsection()");
539 list.add(create(subsectionList.get(i).getSubsection()));
540 } else if (subsectionList.get(i).getNode() != null) {
541 setLocationWithinModule(context + ".get(" + i + ").getNode()");
542 list.add(create(subsectionList.get(i).getNode()));
543 } else {
544 throw new IllegalArgumentException("unexpected subsection type: "
545 + subsectionList.get(i).getClass());
546 }
547 }
548 setLocationWithinModule(context);
549 return list;
550 }
551
552 private final SubsectionVo create(final Subsection subsection) {
553 if (subsection == null) {
554 return null;
555 }
556 final SubsectionVo s = new SubsectionVo();
557 final String context = getCurrentContext().getLocationWithinModule();
558 if (subsection.getId() != null) {
559 setLocationWithinModule(context + ".getId()");
560 s.setId(subsection.getId());
561 }
562 if (subsection.getLevel() != null) {
563 setLocationWithinModule(context + ".getLevel()");
564 s.setLevel(subsection.getLevel());
565 }
566 if (subsection.getTitle() != null) {
567 setLocationWithinModule(context + ".getTitle()");
568 s.setTitle(create(subsection.getTitle()));
569 }
570 if (subsection.getLatex() != null) {
571 setLocationWithinModule(context + ".getLatex()");
572 s.setLatex(create(subsection.getLatex()));
573 }
574 setLocationWithinModule(context);
575 return s;
576 }
577
578 private final NodeVo create(final Node node)
579 throws IllegalModuleDataException {
580 if (node == null) {
581 return null;
582 }
583 final NodeVo n = new NodeVo();
584 final String context = getCurrentContext().getLocationWithinModule();
585 if (node.getName() != null) {
586 setLocationWithinModule(context + ".getName()");
587 n.setName(create(node.getName()));
588 }
589 if (node.getId() != null) {
590 setLocationWithinModule(context + ".getId()");
591 n.setId(node.getId());
592 }
593 if (node.getLevel() != null) {
594 setLocationWithinModule(context + ".getLevel()");
595 n.setLevel(node.getLevel());
596 }
597 if (node.getTitle() != null) {
598 setLocationWithinModule(context + ".getTitle()");
599 n.setTitle(create(node.getTitle()));
600 }
601 if (node.getPrecedingText() != null) {
602 setLocationWithinModule(context + ".getPrecedingText()");
603 n.setPrecedingText(create(node.getPrecedingText()));
604 }
605 if (node.getNodeType() != null) {
606 setLocationWithinModule(context + ".getNodeType()");
607 if (node.getNodeType() instanceof Axiom) {
608 setLocationWithinModule(context + ".getNodeType().getAxiom()");
609 n.setNodeType(create((Axiom) node.getNodeType()));
610 } else if (node.getNodeType() instanceof InitialPredicateDefinition) {
611 setLocationWithinModule(context + ".getNodeType().getInitialPredicateDefinition()");
612 n.setNodeType(create((InitialPredicateDefinition) node.getNodeType()));
613 } else if (node.getNodeType() instanceof PredicateDefinition) {
614 setLocationWithinModule(context + ".getNodeType().getPredicateDefinition()");
615 n.setNodeType(create((PredicateDefinition) node.getNodeType()));
616 } else if (node.getNodeType() instanceof InitialFunctionDefinition) {
617 setLocationWithinModule(context + ".getNodeType().getInitialFunctionDefinition()");
618 n.setNodeType(create((InitialFunctionDefinition) node.getNodeType()));
619 } else if (node.getNodeType() instanceof FunctionDefinition) {
620 setLocationWithinModule(context + ".getNodeType().getFunctionDefinition()");
621 n.setNodeType(create((FunctionDefinition) node.getNodeType()));
622 } else if (node.getNodeType() instanceof Proposition) {
623 setLocationWithinModule(context + ".getNodeType().getProposition()");
624 n.setNodeType(create((Proposition) node.getNodeType()));
625 } else if (node.getNodeType() instanceof Rule) {
626 setLocationWithinModule(context + ".getNodeType().getRule()");
627 n.setNodeType(create((Rule) node.getNodeType()));
628 } else {
629 throw new IllegalModuleDataException(ServiceErrors.RUNTIME_ERROR_CODE,
630 ServiceErrors.RUNTIME_ERROR_TEXT + " "
631 + "unexpected node type: " + node.getNodeType().getClass(),
632 getCurrentContext());
633 }
634 }
635 if (node.getSucceedingText() != null) {
636 setLocationWithinModule(context + ".getSucceedingText()");
637 n.setSucceedingText(create(node.getSucceedingText()));
638 }
639 setLocationWithinModule(context);
640 return n;
641 }
642
643 private final AxiomVo create(final Axiom axiom) {
644 if (axiom == null) {
645 return null;
646 }
647 final AxiomVo a = new AxiomVo();
648 final String context = getCurrentContext().getLocationWithinModule();
649 if (axiom.getDefinedOperator() != null) {
650 setLocationWithinModule(context + ".getDefinedOperator()");
651 a.setDefinedOperator(axiom.getDefinedOperator());
652 }
653 if (axiom.getFormula() != null) {
654 setLocationWithinModule(context + ".getFormula()");
655 a.setFormula(create(axiom.getFormula()));
656 }
657 if (axiom.getDescription() != null) {
658 setLocationWithinModule(context + ".getDescription()");
659 a.setDescription(create(axiom.getDescription()));
660 }
661 setLocationWithinModule(context);
662 return a;
663 }
664
665 private final InitialPredicateDefinitionVo create(final InitialPredicateDefinition definition) {
666 if (definition == null) {
667 return null;
668 }
669 final InitialPredicateDefinitionVo d = new InitialPredicateDefinitionVo();
670 final String context = getCurrentContext().getLocationWithinModule();
671 if (definition.getLatexPattern() != null) {
672 setLocationWithinModule(context + ".getLatexPattern()");
673 d.setLatexPattern(definition.getLatexPattern());
674 }
675 if (definition.getName() != null) {
676 setLocationWithinModule(context + ".getName()");
677 d.setName(definition.getName());
678 }
679 if (definition.getArgumentNumber() != null) {
680 setLocationWithinModule(context + ".getArgumentNumber()");
681 d.setArgumentNumber(definition.getArgumentNumber());
682 }
683 if (definition.getPredCon() != null) {
684 setLocationWithinModule(context + ".getPredCon()");
685 d.setPredCon(create(definition.getPredCon()));
686 }
687 if (definition.getDescription() != null) {
688 setLocationWithinModule(context + ".getDescription()");
689 d.setDescription(create(definition.getDescription()));
690 }
691 setLocationWithinModule(context);
692 return d;
693 }
694
695 private final PredicateDefinitionVo create(final PredicateDefinition definition) {
696 if (definition == null) {
697 return null;
698 }
699 final PredicateDefinitionVo d = new PredicateDefinitionVo();
700 final String context = getCurrentContext().getLocationWithinModule();
701 if (definition.getLatexPattern() != null) {
702 setLocationWithinModule(context + ".getLatexPattern()");
703 d.setLatexPattern(definition.getLatexPattern());
704 }
705 if (definition.getName() != null) {
706 setLocationWithinModule(context + ".getName()");
707 d.setName(definition.getName());
708 }
709 if (definition.getArgumentNumber() != null) {
710 setLocationWithinModule(context + ".getArgumentNumber()");
711 d.setArgumentNumber(definition.getArgumentNumber());
712 }
713 if (definition.getFormula() != null) {
714 setLocationWithinModule(context + ".getFormula()");
715 d.setFormula(create(definition.getFormula()));
716 }
717 if (definition.getDescription() != null) {
718 setLocationWithinModule(context + ".getDescription()");
719 d.setDescription(create(definition.getDescription()));
720 }
721 setLocationWithinModule(context);
722 return d;
723 }
724
725 private final InitialFunctionDefinitionVo create(final InitialFunctionDefinition definition) {
726 if (definition == null) {
727 return null;
728 }
729 final InitialFunctionDefinitionVo d = new InitialFunctionDefinitionVo();
730 final String context = getCurrentContext().getLocationWithinModule();
731 if (definition.getLatexPattern() != null) {
732 setLocationWithinModule(context + ".getLatexPattern()");
733 d.setLatexPattern(definition.getLatexPattern());
734 }
735 if (definition.getArgumentNumber() != null) {
736 setLocationWithinModule(context + ".getArgumentNumber()");
737 d.setArgumentNumber(definition.getArgumentNumber());
738 }
739 if (definition.getName() != null) {
740 setLocationWithinModule(context + ".getName()");
741 d.setName(definition.getName());
742 }
743 if (definition.getFunCon() != null) {
744 setLocationWithinModule(context + ".getFunCon()");
745 d.setFunCon(create(definition.getFunCon()));
746 }
747 if (definition.getDescription() != null) {
748 setLocationWithinModule(context + ".getDescription()");
749 d.setDescription(create(definition.getDescription()));
750 }
751 setLocationWithinModule(context);
752 return d;
753 }
754
755 private final FunctionDefinitionVo create(final FunctionDefinition definition) {
756 if (definition == null) {
757 return null;
758 }
759 final FunctionDefinitionVo d = new FunctionDefinitionVo();
760 final String context = getCurrentContext().getLocationWithinModule();
761 if (definition.getLatexPattern() != null) {
762 setLocationWithinModule(context + ".getLatexPattern()");
763 d.setLatexPattern(definition.getLatexPattern());
764 }
765 if (definition.getArgumentNumber() != null) {
766 setLocationWithinModule(context + ".getArgumentNumber()");
767 d.setArgumentNumber(definition.getArgumentNumber());
768 }
769 if (definition.getName() != null) {
770 setLocationWithinModule(context + ".getName()");
771 d.setName(definition.getName());
772 }
773 if (definition.getFormula() != null) {
774 setLocationWithinModule(context + ".getFormula()");
775 d.setFormula(create(definition.getFormula()));
776 }
777 if (definition.getDescription() != null) {
778 setLocationWithinModule(context + ".getDescription()");
779 d.setDescription(create(definition.getDescription()));
780 }
781 setLocationWithinModule(context);
782 return d;
783 }
784
785 private final PropositionVo create(final Proposition proposition) {
786 if (proposition == null) {
787 return null;
788 }
789 final PropositionVo p = new PropositionVo();
790 final String context = getCurrentContext().getLocationWithinModule();
791 if (proposition.getFormula() != null) {
792 setLocationWithinModule(context + ".getFormula()");
793 p.setFormula(create(proposition.getFormula()));
794 }
795 if (proposition.getDescription() != null) {
796 setLocationWithinModule(context + ".getDescription()");
797 p.setDescription(create(proposition.getDescription()));
798 }
799 if (proposition.getProofList() != null) {
800 setLocationWithinModule(context + ".getProofList()");
801 p.setProofList(create(proposition.getProofList()));
802 }
803 if (proposition.getFormalProofList() != null) {
804 setLocationWithinModule(context + ".getFormalProofList()");
805 p.setFormalProofList(create(proposition.getFormalProofList()));
806 }
807 setLocationWithinModule(context);
808 return p;
809 }
810
811 private final RuleVo create(final Rule rule) {
812 if (rule == null) {
813 return null;
814 }
815 final RuleVo r = new RuleVo();
816 final String context = getCurrentContext().getLocationWithinModule();
817 if (rule.getName() != null) {
818 setLocationWithinModule(context + ".getName()");
819 r.setName(rule.getName());
820 }
821 if (rule.getVersion() != null) {
822 setLocationWithinModule(context + ".getVersion()");
823 r.setVersion(rule.getVersion());
824 }
825 if (rule.getLinkList() != null) {
826 setLocationWithinModule(context + ".getLinkList()");
827 r.setLinkList(create(rule.getLinkList()));
828 }
829 if (rule.getDescription() != null) {
830 setLocationWithinModule(context + ".getDescription()");
831 r.setDescription(create(rule.getDescription()));
832 }
833 if (rule.getChangedRuleList() != null) {
834 setLocationWithinModule(context + ".getChangedRuleList()");
835 r.setChangedRuleList(create(rule.getChangedRuleList()));
836 }
837 if (rule.getProofList() != null) {
838 setLocationWithinModule(context + ".getProofList()");
839 r.setProofList(create(rule.getProofList()));
840 }
841 setLocationWithinModule(context);
842 return r;
843 }
844
845 private final ChangedRuleListVo create(final ChangedRuleList changedRuleList) {
846 if (changedRuleList == null) {
847 return null;
848 }
849 final ChangedRuleListVo list = new ChangedRuleListVo();
850 final String context = getCurrentContext().getLocationWithinModule();
851 for (int i = 0; i < changedRuleList.size(); i++) {
852 setLocationWithinModule(context + ".get(" + i + ")");
853 list.add(create(changedRuleList.get(i)));
854 }
855 setLocationWithinModule(context);
856 return list;
857 }
858
859 private final ChangedRuleVo create(final ChangedRule rule) {
860 if (rule == null) {
861 return null;
862 }
863 final ChangedRuleVo r = new ChangedRuleVo();
864 final String context = getCurrentContext().getLocationWithinModule();
865 if (rule.getName() != null) {
866 setLocationWithinModule(context + ".getName()");
867 r.setName(rule.getName());
868 }
869 if (rule.getVersion() != null) {
870 setLocationWithinModule(context + ".getVersion()");
871 r.setVersion(rule.getVersion());
872 }
873 if (rule.getDescription() != null) {
874 setLocationWithinModule(context + ".getDescription()");
875 r.setDescription(create(rule.getDescription()));
876 }
877 setLocationWithinModule(context);
878 return r;
879 }
880
881 private final LinkListVo create(final LinkList linkList) {
882 if (linkList == null) {
883 return null;
884 }
885 final LinkListVo list = new LinkListVo();
886 final String context = getCurrentContext().getLocationWithinModule();
887 for (int i = 0; i < linkList.size(); i++) {
888 setLocationWithinModule(context + ".get(" + i + ")");
889 list.add(linkList.get(i));
890 }
891 setLocationWithinModule(context);
892 return list;
893 }
894
895 private final ProofListVo create(final ProofList proofList) {
896 if (proofList == null) {
897 return null;
898 }
899 final ProofListVo list = new ProofListVo();
900 final String context = getCurrentContext().getLocationWithinModule();
901 for (int i = 0; i < proofList.size(); i++) {
902 setLocationWithinModule(context + ".get(" + i + ")");
903 list.add(create(proofList.get(i)));
904 }
905 setLocationWithinModule(context);
906 return list;
907 }
908
909 private final ProofVo create(final Proof proof) {
910 if (proof == null) {
911 return null;
912 }
913 final ProofVo p = new ProofVo();
914 final String context = getCurrentContext().getLocationWithinModule();
915 setLocationWithinModule(context + ".getKind()");
916 p.setKind(proof.getKind());
917 setLocationWithinModule(context + ".getLevel()");
918 p.setLevel(proof.getLevel());
919 setLocationWithinModule(context);
920 if (proof.getNonFormalProof() != null) {
921 setLocationWithinModule(context + ".getNonFormalProof()");
922 p.setNonFormalProof(create(proof.getNonFormalProof()));
923 }
924 setLocationWithinModule(context);
925 return p;
926 }
927
928 private final FormalProofListVo create(final FormalProofList proofList) {
929 if (proofList == null) {
930 return null;
931 }
932 final FormalProofListVo list = new FormalProofListVo();
933 final String context = getCurrentContext().getLocationWithinModule();
934 for (int i = 0; i < proofList.size(); i++) {
935 setLocationWithinModule(context + ".get(" + i + ")");
936 list.add(create(proofList.get(i)));
937 }
938 setLocationWithinModule(context);
939 return list;
940 }
941
942 private final FormalProofVo create(final FormalProof proof) {
943 if (proof == null) {
944 return null;
945 }
946 final FormalProofVo p = new FormalProofVo();
947 final String context = getCurrentContext().getLocationWithinModule();
948 setLocationWithinModule(context);
949 if (proof.getPrecedingText() != null) {
950 setLocationWithinModule(context + ".getPrecedingText()");
951 p.setPrecedingText(create(proof.getPrecedingText()));
952 }
953 if (proof.getFormalProofLineList() != null) {
954 setLocationWithinModule(context + ".getFormalProofLineList()");
955 p.setFormalProofLineList(create(proof.getFormalProofLineList()));
956 }
957 if (proof.getSucceedingText() != null) {
958 setLocationWithinModule(context + ".getSucceedingText()");
959 p.setSucceedingText(create(proof.getSucceedingText()));
960 }
961 setLocationWithinModule(context);
962 return p;
963 }
964
965 private final FormalProofLineListVo create(final FormalProofLineList proofList) {
966 if (proofList == null) {
967 return null;
968 }
969 final FormalProofLineListVo list = new FormalProofLineListVo();
970 final String context = getCurrentContext().getLocationWithinModule();
971 for (int i = 0; i < proofList.size(); i++) {
972 setLocationWithinModule(context + ".get(" + i + ")");
973 if (proofList.get(i) instanceof ConditionalProof) {
974 list.add(create((ConditionalProof) proofList.get(i)));
975 } else {
976 list.add(create(proofList.get(i)));
977 }
978 }
979 setLocationWithinModule(context);
980 return list;
981 }
982
983 private final FormalProofLineVo create(final FormalProofLine proofLine) {
984 if (proofLine == null) {
985 return null;
986 }
987 final FormalProofLineVo line = new FormalProofLineVo();
988 final String context = getCurrentContext().getLocationWithinModule();
989 if (proofLine.getLabel() != null) {
990 setLocationWithinModule(context + ".getLabel()");
991 line.setLabel(proofLine.getLabel());
992 }
993 if (proofLine.getFormula() != null) {
994 setLocationWithinModule(context + ".getFormula()");
995 line.setFormula(create(proofLine.getFormula()));
996 }
997 if (proofLine.getReason() != null) {
998 setLocationWithinModule(context + ".getReason()");
999 line.setReason(create(proofLine.getReason()));
1000 }
1001 setLocationWithinModule(context);
1002 return line;
1003 }
1004
1005 private final ConditionalProofVo create(final ConditionalProof proofLine) {
1006 if (proofLine == null) {
1007 return null;
1008 }
1009 final ConditionalProofVo line = new ConditionalProofVo();
1010 final String context = getCurrentContext().getLocationWithinModule();
1011 if (proofLine.getHypothesis() != null) {
1012 setLocationWithinModule(context + ".getHypothesis()");
1013 line.setHypothesis(proofLine.getHypothesis());
1014 }
1015 if (proofLine.getFormalProofLineList() != null) {
1016 setLocationWithinModule(context + ".getFormalProofLineList()");
1017 line.setFormalProofLineList(create(proofLine.getFormalProofLineList()));
1018 }
1019 if (proofLine.getConclusion() != null) {
1020 setLocationWithinModule(context + ".getConclusion()");
1021 line.setConclusion(create(proofLine.getConclusion()));
1022 }
1023 setLocationWithinModule(context);
1024 return line;
1025 }
1026
1027 private final Reason create(final Reason reason) {
1028 if (reason == null) {
1029 return null;
1030 }
1031 final String context = getCurrentContext().getLocationWithinModule();
1032 Reason result = null;
1033 if (reason instanceof ModusPonens) {
1034 setLocationWithinModule(context + ".getModusPonens()");
1035 final ModusPonens r = (ModusPonens) reason;
1036 result = new ModusPonensVo(r.getReference1(), r.getReference2());
1037 } else if (reason instanceof Add) {
1038 setLocationWithinModule(context + ".getAdd()");
1039 final Add r = (Add) reason;
1040 result = new AddVo(r.getReference());
1041 } else if (reason instanceof Rename) {
1042 setLocationWithinModule(context + ".getRename()");
1043 final Rename r = (Rename) reason;
1044 result = new RenameVo(r.getReference(), r.getOriginalSubjectVariable(),
1045 r.getReplacementSubjectVariable(), r.getOccurrence());
1046 } else if (reason instanceof SubstFree) {
1047 setLocationWithinModule(context + ".getSubstFree()");
1048 final SubstFree r = (SubstFree) reason;
1049 result = new SubstFreeVo(r.getReference(), r.getSubjectVariable(),
1050 r.getSubstituteTerm());
1051 } else if (reason instanceof SubstFunc) {
1052 setLocationWithinModule(context + ".getSubstFunc()");
1053 final SubstFunc r = (SubstFunc) reason;
1054 result = new SubstFuncVo(r.getReference(), r.getFunctionVariable(),
1055 r.getSubstituteTerm());
1056 } else if (reason instanceof SubstPred) {
1057 setLocationWithinModule(context + ".getSubstPred()");
1058 final SubstPred r = (SubstPred) reason;
1059 result = new SubstPredVo(r.getReference(), r.getPredicateVariable(),
1060 r.getSubstituteFormula());
1061 } else if (reason instanceof Existential) {
1062 setLocationWithinModule(context + ".getExistential()");
1063 final Existential r = (Existential) reason;
1064 result = new ExistentialVo(r.getReference(), r.getSubjectVariable());
1065 } else if (reason instanceof Universal) {
1066 setLocationWithinModule(context + ".getUniversal()");
1067 final Universal r = (Universal) reason;
1068 result = new UniversalVo(r.getReference(), r.getSubjectVariable());
1069 } else if (reason instanceof ConditionalProof) {
1070 setLocationWithinModule(context + ".getConditionalProof()");
1071 final ConditionalProof r = (ConditionalProof) reason;
1072 setLocationWithinModule(context + ".getConditionalProof().getHypothesis()");
1073 final Hypothesis h = create(r.getHypothesis());
1074 setLocationWithinModule(context + ".getConditionalProof().getFormalProofLineList()");
1075 final FormalProofLineList l = create(r.getFormalProofLineList());
1076 setLocationWithinModule(context + ".getConditionalProof().getConclusion()");
1077 final Conclusion c = create(r.getConclusion());
1078 result = new ConditionalProofVo(h, l, c);
1079 } else {
1080 throw new RuntimeException("unknown reason class: " + reason.getClass());
1081 }
1082 setLocationWithinModule(context);
1083 return result;
1084 }
1085
1086 private final HypothesisVo create(final Hypothesis hypothesis) {
1087 if (hypothesis == null) {
1088 return null;
1089 }
1090 final HypothesisVo h = new HypothesisVo();
1091 final String context = getCurrentContext().getLocationWithinModule();
1092 if (hypothesis.getLabel() != null) {
1093 h.setLabel(hypothesis.getLabel());
1094 }
1095 if (hypothesis.getFormula() != null) {
1096 setLocationWithinModule(context + ".getFormula()");
1097 h.setFormula(create(hypothesis.getFormula()));
1098 }
1099 setLocationWithinModule(context);
1100 return h;
1101 }
1102
1103 private final ConclusionVo create(final Conclusion conclusion) {
1104 if (conclusion == null) {
1105 return null;
1106 }
1107 final ConclusionVo c = new ConclusionVo();
1108 final String context = getCurrentContext().getLocationWithinModule();
1109 if (conclusion.getLabel() != null) {
1110 c.setLabel(conclusion.getLabel());
1111 }
1112 if (conclusion.getFormula() != null) {
1113 setLocationWithinModule(context + ".getFormula()");
1114 c.setFormula(create(conclusion.getFormula()));
1115 }
1116 setLocationWithinModule(context);
1117 return c;
1118 }
1119
1120 private final FormulaVo create(final Formula formula) {
1121 if (formula == null) {
1122 return null;
1123 }
1124 final FormulaVo f = new FormulaVo();
1125 final String context = getCurrentContext().getLocationWithinModule();
1126 if (formula.getElement() != null) {
1127 setLocationWithinModule(context + ".getElement()");
1128 f.setElement(create(formula.getElement()));
1129 }
1130 setLocationWithinModule(context);
1131 return f;
1132 }
1133
1134 private final Element create(final Element element) {
1135 if (element == null) {
1136 return null;
1137 }
1138 final Element e;
1139 final String context = getCurrentContext().getLocationWithinModule();
1140 if (element.isList()) {
1141 setLocationWithinModule(context + ".getList()");
1142 e = create(element.getList());
1143 } else if (element.isAtom()) {
1144
1145 return create(element.getAtom());
1146 } else {
1147 throw new RuntimeException("unknown element type: " + element);
1148 }
1149 setLocationWithinModule(context);
1150 return e;
1151 }
1152
1153
1154 private final DefaultElementList create(final ElementList list) {
1155 if (list == null) {
1156 return null;
1157 }
1158 final DefaultElementList n = new DefaultElementList(list.getOperator(), new Element[] {});
1159 final String context = getCurrentContext().getLocationWithinModule();
1160 for (int i = 0; i < list.size(); i++) {
1161 if (list.getElement(i).isList()) {
1162 setLocationWithinModule(context + ".getElement(" + i + ")");
1163 }
1164 n.add(create(list.getElement(i)));
1165 }
1166 setLocationWithinModule(context);
1167 return n;
1168 }
1169
1170 private final DefaultAtom create(final Atom atom) {
1171 if (atom == null) {
1172 return null;
1173 }
1174 return new DefaultAtom(atom.getString());
1175 }
1176
1177 private final LatexListVo create(final LatexList latexList) {
1178 if (latexList == null) {
1179 return null;
1180 }
1181 final LatexListVo list = new LatexListVo();
1182 final String context = getCurrentContext().getLocationWithinModule();
1183 for (int i = 0; i < latexList.size(); i++) {
1184 setLocationWithinModule(context + ".get(" + i + ")");
1185 list.add(create(latexList.get(i)));
1186 }
1187 setLocationWithinModule(context);
1188 return list;
1189 }
1190
1191
1192
1193
1194
1195
1196
1197 private final LatexVo create(final Latex latex) {
1198 if (latex == null) {
1199 return null;
1200 }
1201 final LatexVo lat = new LatexVo();
1202 lat.setLanguage(latex.getLanguage());
1203 lat.setLatex(latex.getLatex());
1204 return lat;
1205 }
1206
1207
1208
1209
1210
1211
1212 protected void setLocationWithinModule(final String locationWithinModule) {
1213 getCurrentContext().setLocationWithinModule(locationWithinModule);
1214 }
1215
1216
1217
1218
1219
1220
1221 protected final ModuleContext getCurrentContext() {
1222 return currentContext;
1223 }
1224
1225
1226
1227
1228
1229
1230 protected final Qedeq getQedeqOriginal() {
1231 return original;
1232 }
1233
1234 }