1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.se.visitor;
17
18 import java.util.HashMap;
19 import java.util.Map;
20 import java.util.Stack;
21
22 import org.qedeq.kernel.se.base.list.Atom;
23 import org.qedeq.kernel.se.base.list.Element;
24 import org.qedeq.kernel.se.base.list.ElementList;
25 import org.qedeq.kernel.se.base.module.Add;
26 import org.qedeq.kernel.se.base.module.Author;
27 import org.qedeq.kernel.se.base.module.AuthorList;
28 import org.qedeq.kernel.se.base.module.Axiom;
29 import org.qedeq.kernel.se.base.module.ChangedRule;
30 import org.qedeq.kernel.se.base.module.ChangedRuleList;
31 import org.qedeq.kernel.se.base.module.Chapter;
32 import org.qedeq.kernel.se.base.module.ChapterList;
33 import org.qedeq.kernel.se.base.module.Conclusion;
34 import org.qedeq.kernel.se.base.module.ConditionalProof;
35 import org.qedeq.kernel.se.base.module.Existential;
36 import org.qedeq.kernel.se.base.module.FormalProof;
37 import org.qedeq.kernel.se.base.module.FormalProofLine;
38 import org.qedeq.kernel.se.base.module.FormalProofLineList;
39 import org.qedeq.kernel.se.base.module.FormalProofList;
40 import org.qedeq.kernel.se.base.module.Formula;
41 import org.qedeq.kernel.se.base.module.FunctionDefinition;
42 import org.qedeq.kernel.se.base.module.Header;
43 import org.qedeq.kernel.se.base.module.Hypothesis;
44 import org.qedeq.kernel.se.base.module.Import;
45 import org.qedeq.kernel.se.base.module.ImportList;
46 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
47 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
48 import org.qedeq.kernel.se.base.module.Latex;
49 import org.qedeq.kernel.se.base.module.LatexList;
50 import org.qedeq.kernel.se.base.module.LinkList;
51 import org.qedeq.kernel.se.base.module.LiteratureItem;
52 import org.qedeq.kernel.se.base.module.LiteratureItemList;
53 import org.qedeq.kernel.se.base.module.Location;
54 import org.qedeq.kernel.se.base.module.LocationList;
55 import org.qedeq.kernel.se.base.module.ModusPonens;
56 import org.qedeq.kernel.se.base.module.Node;
57 import org.qedeq.kernel.se.base.module.PredicateDefinition;
58 import org.qedeq.kernel.se.base.module.Proof;
59 import org.qedeq.kernel.se.base.module.ProofList;
60 import org.qedeq.kernel.se.base.module.Proposition;
61 import org.qedeq.kernel.se.base.module.Qedeq;
62 import org.qedeq.kernel.se.base.module.Reason;
63 import org.qedeq.kernel.se.base.module.Rename;
64 import org.qedeq.kernel.se.base.module.Rule;
65 import org.qedeq.kernel.se.base.module.Section;
66 import org.qedeq.kernel.se.base.module.SectionList;
67 import org.qedeq.kernel.se.base.module.Specification;
68 import org.qedeq.kernel.se.base.module.Subsection;
69 import org.qedeq.kernel.se.base.module.SubsectionList;
70 import org.qedeq.kernel.se.base.module.SubstFree;
71 import org.qedeq.kernel.se.base.module.SubstFunc;
72 import org.qedeq.kernel.se.base.module.SubstPred;
73 import org.qedeq.kernel.se.base.module.Term;
74 import org.qedeq.kernel.se.base.module.Universal;
75 import org.qedeq.kernel.se.base.module.UsedByList;
76 import org.qedeq.kernel.se.common.ModuleAddress;
77 import org.qedeq.kernel.se.common.ModuleContext;
78 import org.qedeq.kernel.se.common.ModuleDataException;
79 import org.qedeq.kernel.se.common.RuleKey;
80 import org.qedeq.kernel.se.common.ServiceCompleteness;
81 import org.qedeq.kernel.se.dto.module.FormulaVo;
82 import org.qedeq.kernel.se.dto.module.TermVo;
83
84
85
86
87
88
89
90
91 public class QedeqNotNullTraverser implements QedeqTraverser, ServiceCompleteness {
92
93
94 private final ModuleContext currentContext;
95
96
97 private final Stack location = new Stack();
98
99
100 private QedeqNumbers data = new QedeqNumbers(0, 0);
101
102
103 private final LatexList2Text transform = new LatexList2Text();
104
105
106
107
108
109 private QedeqVisitor visitor;
110
111
112 private boolean blocked;
113
114
115 private Node node;
116
117
118 private Map ruleExistence;
119
120
121
122
123
124
125
126 public QedeqNotNullTraverser(final ModuleAddress globalContext, final QedeqVisitor visitor) {
127 currentContext = globalContext.createModuleContext();
128 this.visitor = visitor;
129 }
130
131
132
133
134
135
136 public QedeqNotNullTraverser(final ModuleAddress globalContext) {
137 currentContext = globalContext.createModuleContext();
138 }
139
140
141
142
143
144
145 public void setVisitor(final QedeqVisitor visitor) {
146 this.visitor = visitor;
147 }
148
149 public void accept(final Qedeq qedeq) throws ModuleDataException {
150 ruleExistence = new HashMap();
151 setLocation("started");
152 if (qedeq == null) {
153 throw new NullPointerException("null QEDEQ module");
154 }
155 data = new QedeqNumbers(
156 (qedeq.getHeader() != null && qedeq.getHeader().getImportList() != null
157 ? qedeq.getHeader().getImportList().size() : 0),
158 (qedeq.getChapterList() != null ? qedeq.getChapterList().size() : 0)
159 );
160 getCurrentContext().setLocationWithinModule("");
161 checkForInterrupt();
162 blocked = false;
163 final String context = getCurrentContext().getLocationWithinModule();
164 visitor.visitEnter(qedeq);
165 if (qedeq.getHeader() != null) {
166 getCurrentContext().setLocationWithinModule(context + "getHeader()");
167 accept(qedeq.getHeader());
168 }
169 if (qedeq.getChapterList() != null) {
170 getCurrentContext().setLocationWithinModule(context + "getChapterList()");
171 accept(qedeq.getChapterList());
172 }
173 if (qedeq.getLiteratureItemList() != null) {
174 getCurrentContext().setLocationWithinModule(context + "getLiteratureItemList()");
175 accept(qedeq.getLiteratureItemList());
176 }
177 setLocationWithinModule(context);
178 visitor.visitLeave(qedeq);
179 setLocationWithinModule(context);
180 setLocation("finished");
181 data.setFinished(true);
182 }
183
184
185
186
187
188
189 private void checkForInterrupt() throws InterruptException {
190 if (Thread.interrupted()) {
191 throw new InterruptException(getCurrentContext());
192 }
193 }
194
195 public void accept(final Header header) throws ModuleDataException {
196 checkForInterrupt();
197 if (blocked || header == null) {
198 return;
199 }
200 setLocation("analyzing header");
201 final String context = getCurrentContext().getLocationWithinModule();
202 visitor.visitEnter(header);
203 if (header.getSpecification() != null) {
204 setLocationWithinModule(context + ".getSpecification()");
205 accept(header.getSpecification());
206 }
207 if (header.getTitle() != null) {
208 setLocationWithinModule(context + ".getTitle()");
209 accept(header.getTitle());
210 }
211 if (header.getSummary() != null) {
212 setLocationWithinModule(context + ".getSummary()");
213 accept(header.getSummary());
214 }
215 if (header.getAuthorList() != null) {
216 setLocationWithinModule(context + ".getAuthorList()");
217 accept(header.getAuthorList());
218 }
219 if (header.getImportList() != null) {
220 setLocationWithinModule(context + ".getImportList()");
221 accept(header.getImportList());
222 }
223 if (header.getUsedByList() != null) {
224 setLocationWithinModule(context + ".getUsedByList()");
225 accept(header.getUsedByList());
226 }
227 setLocationWithinModule(context);
228 visitor.visitLeave(header);
229 setLocationWithinModule(context);
230 }
231
232 public void accept(final UsedByList usedByList) throws ModuleDataException {
233 checkForInterrupt();
234 if (blocked || usedByList == null) {
235 return;
236 }
237 location.push("working on used by list");
238 final String context = getCurrentContext().getLocationWithinModule();
239 visitor.visitEnter(usedByList);
240 for (int i = 0; i < usedByList.size(); i++) {
241 setLocationWithinModule(context + ".get(" + i + ")");
242 accept(usedByList.get(i));
243 }
244 setLocationWithinModule(context);
245 visitor.visitLeave(usedByList);
246 setLocationWithinModule(context);
247 location.pop();
248 }
249
250 public void accept(final ImportList importList) throws ModuleDataException {
251 checkForInterrupt();
252 if (blocked || importList == null) {
253 return;
254 }
255 location.push("working on import list");
256 final String context = getCurrentContext().getLocationWithinModule();
257 visitor.visitEnter(importList);
258 for (int i = 0; i < importList.size(); i++) {
259 setLocationWithinModule(context + ".get(" + i + ")");
260 accept(importList.get(i));
261 }
262 setLocationWithinModule(context);
263 visitor.visitLeave(importList);
264 setLocationWithinModule(context);
265 location.pop();
266 }
267
268 public void accept(final Import imp) throws ModuleDataException {
269 data.increaseImportNumber();
270 checkForInterrupt();
271 if (blocked || imp == null) {
272 return;
273 }
274 location.push("import " + data.getImportNumber() + ": " + imp.getLabel());
275 final String context = getCurrentContext().getLocationWithinModule();
276 visitor.visitEnter(imp);
277 if (imp.getSpecification() != null) {
278 setLocationWithinModule(context + ".getSpecification()");
279 accept(imp.getSpecification());
280 }
281 setLocationWithinModule(context);
282 visitor.visitLeave(imp);
283 setLocationWithinModule(context);
284 location.pop();
285 }
286
287 public void accept(final Specification specification) throws ModuleDataException {
288 checkForInterrupt();
289 if (blocked || specification == null) {
290 return;
291 }
292 final String context = getCurrentContext().getLocationWithinModule();
293 visitor.visitEnter(specification);
294 if (specification.getLocationList() != null) {
295 setLocationWithinModule(context + ".getLocationList()");
296 accept(specification.getLocationList());
297 }
298 setLocationWithinModule(context);
299 visitor.visitLeave(specification);
300 setLocationWithinModule(context);
301 }
302
303 public void accept(final LocationList locationList) throws ModuleDataException {
304 checkForInterrupt();
305 if (blocked || locationList == null) {
306 return;
307 }
308 final String context = getCurrentContext().getLocationWithinModule();
309 visitor.visitEnter(locationList);
310 for (int i = 0; i < locationList.size(); i++) {
311 setLocationWithinModule(context + ".get(" + i + ")");
312 accept(locationList.get(i));
313 }
314 setLocationWithinModule(context);
315 visitor.visitLeave(locationList);
316 setLocationWithinModule(context);
317 }
318
319 public void accept(final Location location) throws ModuleDataException {
320 checkForInterrupt();
321 if (blocked || location == null) {
322 return;
323 }
324 final String context = getCurrentContext().getLocationWithinModule();
325 visitor.visitEnter(location);
326 setLocationWithinModule(context);
327 visitor.visitLeave(location);
328 setLocationWithinModule(context);
329 }
330
331 public void accept(final AuthorList authorList) throws ModuleDataException {
332 checkForInterrupt();
333 if (blocked || authorList == null) {
334 return;
335 }
336 final String context = getCurrentContext().getLocationWithinModule();
337 visitor.visitEnter(authorList);
338 for (int i = 0; i < authorList.size(); i++) {
339 setLocationWithinModule(context + ".get(" + i + ")");
340 accept(authorList.get(i));
341 }
342 setLocationWithinModule(context);
343 visitor.visitLeave(authorList);
344 setLocationWithinModule(context);
345 }
346
347 public void accept(final Author author) throws ModuleDataException {
348 checkForInterrupt();
349 if (blocked || author == null) {
350 return;
351 }
352 final String context = getCurrentContext().getLocationWithinModule();
353 visitor.visitEnter(author);
354 if (author.getName() != null) {
355 setLocationWithinModule(context + ".getName()");
356 accept(author.getName());
357 }
358 setLocationWithinModule(context);
359 visitor.visitLeave(author);
360 setLocationWithinModule(context);
361 }
362
363 public void accept(final ChapterList chapterList) throws ModuleDataException {
364 checkForInterrupt();
365 if (blocked || chapterList == null) {
366 return;
367 }
368 final String context = getCurrentContext().getLocationWithinModule();
369 visitor.visitEnter(chapterList);
370 for (int i = 0; i < chapterList.size(); i++) {
371 setLocationWithinModule(context + ".get(" + i + ")");
372 accept(chapterList.get(i));
373 }
374 setLocationWithinModule(context);
375 visitor.visitLeave(chapterList);
376 setLocationWithinModule(context);
377 }
378
379 public void accept(final Chapter chapter) throws ModuleDataException {
380 checkForInterrupt();
381 if (blocked || chapter == null) {
382 return;
383 }
384 data.increaseChapterNumber(
385 (chapter.getSectionList() != null ? chapter.getSectionList().size() : 0),
386 chapter.getNoNumber() == null || !chapter.getNoNumber().booleanValue()
387 );
388 if (data.isChapterNumbering()) {
389 setLocation("Chapter " + data.getChapterNumber() + " "
390 + transform.transform(chapter.getTitle()));
391 } else {
392 setLocation(transform.transform(chapter.getTitle()));
393 }
394 final String context = getCurrentContext().getLocationWithinModule();
395 visitor.visitEnter(chapter);
396 if (chapter.getTitle() != null) {
397 setLocationWithinModule(context + ".getTitle()");
398 accept(chapter.getTitle());
399 }
400 if (chapter.getIntroduction() != null) {
401 setLocationWithinModule(context + ".getIntroduction()");
402 accept(chapter.getIntroduction());
403 }
404 if (chapter.getSectionList() != null) {
405 setLocationWithinModule(context + ".getSectionList()");
406 accept(chapter.getSectionList());
407 }
408 setLocationWithinModule(context);
409 visitor.visitLeave(chapter);
410 setLocationWithinModule(context);
411 }
412
413 public void accept(final LiteratureItemList literatureItemList)
414 throws ModuleDataException {
415 checkForInterrupt();
416 if (blocked || literatureItemList == null) {
417 return;
418 }
419 setLocation("working on literature list");
420 final String context = getCurrentContext().getLocationWithinModule();
421 visitor.visitEnter(literatureItemList);
422 for (int i = 0; i < literatureItemList.size(); i++) {
423 setLocationWithinModule(context + ".get(" + i + ")");
424 accept(literatureItemList.get(i));
425 }
426 setLocationWithinModule(context);
427 visitor.visitLeave(literatureItemList);
428 setLocationWithinModule(context);
429 }
430
431 public void accept(final LiteratureItem item) throws ModuleDataException {
432 checkForInterrupt();
433 if (blocked || item == null) {
434 return;
435 }
436 final String context = getCurrentContext().getLocationWithinModule();
437 visitor.visitEnter(item);
438 if (item.getItem() != null) {
439 setLocationWithinModule(context + ".getItem()");
440 accept(item.getItem());
441 }
442 setLocationWithinModule(context);
443 visitor.visitLeave(item);
444 setLocationWithinModule(context);
445 }
446
447 public void accept(final SectionList sectionList) throws ModuleDataException {
448 checkForInterrupt();
449 if (blocked || sectionList == null) {
450 return;
451 }
452 final String context = getCurrentContext().getLocationWithinModule();
453 visitor.visitEnter(sectionList);
454 for (int i = 0; i < sectionList.size(); i++) {
455 setLocationWithinModule(context + ".get(" + i + ")");
456 accept(sectionList.get(i));
457 }
458 setLocationWithinModule(context);
459 visitor.visitLeave(sectionList);
460 setLocationWithinModule(context);
461 }
462
463 public void accept(final Section section) throws ModuleDataException {
464 checkForInterrupt();
465 if (blocked || section == null) {
466 return;
467 }
468 data.increaseSectionNumber(
469 (section.getSubsectionList() != null ? section.getSubsectionList().size() : 0),
470 section.getNoNumber() == null || !section.getNoNumber().booleanValue()
471 );
472 String title = "";
473 if (data.isChapterNumbering()) {
474 title += data.getChapterNumber();
475 }
476 if (data.isSectionNumbering()) {
477 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
478 }
479 if (section.getTitle() != null) {
480 title += " " + transform.transform(section.getTitle());
481 }
482 location.push(title);
483 final String context = getCurrentContext().getLocationWithinModule();
484 visitor.visitEnter(section);
485 if (section.getTitle() != null) {
486 setLocationWithinModule(context + ".getTitle()");
487 accept(section.getTitle());
488 }
489 if (section.getIntroduction() != null) {
490 setLocationWithinModule(context + ".getIntroduction()");
491 accept(section.getIntroduction());
492 }
493 if (section.getSubsectionList() != null) {
494 setLocationWithinModule(context + ".getSubsectionList()");
495 accept(section.getSubsectionList());
496 }
497 setLocationWithinModule(context);
498 visitor.visitLeave(section);
499 setLocationWithinModule(context);
500 location.pop();
501 }
502
503 public void accept(final SubsectionList subsectionList) throws ModuleDataException {
504 checkForInterrupt();
505 if (blocked || subsectionList == null) {
506 return;
507 }
508 final String context = getCurrentContext().getLocationWithinModule();
509 visitor.visitEnter(subsectionList);
510 for (int i = 0; i < subsectionList.size(); i++) {
511 setLocationWithinModule(context + ".get(" + i + ")");
512
513
514 if (subsectionList.get(i) instanceof Subsection) {
515 setLocationWithinModule(context + ".get(" + i + ").getSubsection()");
516 accept((Subsection) subsectionList.get(i));
517 } else if (subsectionList.get(i) instanceof Node) {
518 setLocationWithinModule(context + ".get(" + i + ").getNode()");
519 accept((Node) subsectionList.get(i));
520 } else if (subsectionList.get(i) == null) {
521
522 } else {
523 throw new IllegalArgumentException("unexpected subsection type: "
524 + subsectionList.get(i).getClass());
525 }
526 }
527 setLocationWithinModule(context);
528 visitor.visitLeave(subsectionList);
529 setLocationWithinModule(context);
530 }
531
532 public void accept(final Subsection subsection) throws ModuleDataException {
533 checkForInterrupt();
534 if (blocked || subsection == null) {
535 return;
536 }
537 data.increaseSubsectionNumber();
538 String title = "";
539 if (data.isChapterNumbering()) {
540 title += data.getChapterNumber();
541 }
542 if (data.isSectionNumbering()) {
543 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
544 }
545 title += (title.length() > 0 ? "." : "") + data.getSubsectionNumber();
546 if (subsection.getTitle() != null) {
547 title += " " + transform.transform(subsection.getTitle());
548 }
549 title = title + " [" + subsection.getId() + "]";
550 location.push(title);
551 final String context = getCurrentContext().getLocationWithinModule();
552 visitor.visitEnter(subsection);
553 if (subsection.getTitle() != null) {
554 setLocationWithinModule(context + ".getTitle()");
555 accept(subsection.getTitle());
556 }
557 if (subsection.getLatex() != null) {
558 setLocationWithinModule(context + ".getLatex()");
559 accept(subsection.getLatex());
560 }
561 setLocationWithinModule(context);
562 visitor.visitLeave(subsection);
563 setLocationWithinModule(context);
564 location.pop();
565 }
566
567 public void accept(final Node node) throws ModuleDataException {
568 checkForInterrupt();
569 data.increaseNodeNumber();
570 if (blocked || node == null) {
571 return;
572 }
573 this.node = node;
574 String title = "";
575 if (node.getTitle() != null) {
576 title = transform.transform(node.getTitle());
577 }
578 title = title + " [" + node.getId() + "]";
579 location.push(title);
580 final String context = getCurrentContext().getLocationWithinModule();
581 visitor.visitEnter(node);
582 if (node.getName() != null) {
583 setLocationWithinModule(context + ".getName()");
584 accept(node.getName());
585 }
586 if (node.getTitle() != null) {
587 setLocationWithinModule(context + ".getTitle()");
588 accept(node.getTitle());
589 }
590 if (node.getPrecedingText() != null) {
591 setLocationWithinModule(context + ".getPrecedingText()");
592 accept(node.getPrecedingText());
593 }
594 if (node.getNodeType() != null) {
595 setLocationWithinModule(context + ".getNodeType()");
596 if (node.getNodeType() instanceof Axiom) {
597 setLocationWithinModule(context + ".getNodeType().getAxiom()");
598 accept((Axiom) node.getNodeType());
599 } else if (node.getNodeType() instanceof InitialPredicateDefinition) {
600 setLocationWithinModule(context + ".getNodeType().getInitialPredicateDefinition()");
601 accept((InitialPredicateDefinition) node.getNodeType());
602 } else if (node.getNodeType() instanceof PredicateDefinition) {
603 setLocationWithinModule(context + ".getNodeType().getPredicateDefinition()");
604 accept((PredicateDefinition) node.getNodeType());
605 } else if (node.getNodeType() instanceof InitialFunctionDefinition) {
606 setLocationWithinModule(context + ".getNodeType().getInitialFunctionDefinition()");
607 accept((InitialFunctionDefinition) node.getNodeType());
608 } else if (node.getNodeType() instanceof FunctionDefinition) {
609 setLocationWithinModule(context + ".getNodeType().getFunctionDefinition()");
610 accept((FunctionDefinition) node.getNodeType());
611 } else if (node.getNodeType() instanceof Proposition) {
612 setLocationWithinModule(context + ".getNodeType().getProposition()");
613 accept((Proposition) node.getNodeType());
614 } else if (node.getNodeType() instanceof Rule) {
615 setLocationWithinModule(context + ".getNodeType().getRule()");
616 accept((Rule) node.getNodeType());
617 } else {
618 throw new IllegalArgumentException("unexpected node type: "
619 + node.getNodeType().getClass());
620 }
621 }
622 if (node.getSucceedingText() != null) {
623 setLocationWithinModule(context + ".getSucceedingText()");
624 accept(node.getSucceedingText());
625 }
626 setLocationWithinModule(context);
627 visitor.visitLeave(node);
628 setLocationWithinModule(context);
629 location.pop();
630 this.node = null;
631 }
632
633 public void accept(final Axiom axiom) throws ModuleDataException {
634 checkForInterrupt();
635 if (blocked || axiom == null) {
636 return;
637 }
638 data.increaseAxiomNumber();
639 location.set(location.size() - 1, "Axiom " + data.getAxiomNumber() + " "
640 + (String) location.lastElement());
641 final String context = getCurrentContext().getLocationWithinModule();
642 visitor.visitEnter(axiom);
643 if (axiom.getFormula() != null) {
644 setLocationWithinModule(context + ".getFormula()");
645 accept(axiom.getFormula());
646 }
647 if (axiom.getDescription() != null) {
648 setLocationWithinModule(context + ".getDescription()");
649 accept(axiom.getDescription());
650 }
651 setLocationWithinModule(context);
652 visitor.visitLeave(axiom);
653 setLocationWithinModule(context);
654 }
655
656 public void accept(final PredicateDefinition definition)
657 throws ModuleDataException {
658 checkForInterrupt();
659 if (blocked || definition == null) {
660 return;
661 }
662 data.increasePredicateDefinitionNumber();
663 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
664 + data.getFunctionDefinitionNumber()) + " "
665 + (String) location.lastElement());
666 final String context = getCurrentContext().getLocationWithinModule();
667 visitor.visitEnter(definition);
668 if (definition.getFormula() != null) {
669 setLocationWithinModule(context + ".getFormula()");
670 accept(definition.getFormula());
671 }
672 if (definition.getDescription() != null) {
673 setLocationWithinModule(context + ".getDescription()");
674 accept(definition.getDescription());
675 }
676 setLocationWithinModule(context);
677 visitor.visitLeave(definition);
678 setLocationWithinModule(context);
679 }
680
681 public void accept(final InitialPredicateDefinition definition)
682 throws ModuleDataException {
683 checkForInterrupt();
684 if (blocked || definition == null) {
685 return;
686 }
687 data.increasePredicateDefinitionNumber();
688 location.set(location.size() - 1, "Definition "
689 + (data.getPredicateDefinitionNumber() + data
690 .getFunctionDefinitionNumber()) + " "
691 + (String) location.lastElement());
692 final String context = getCurrentContext().getLocationWithinModule();
693 visitor.visitEnter(definition);
694 if (definition.getPredCon() != null) {
695 setLocationWithinModule(context + ".getPredCon()");
696 accept(definition.getPredCon());
697 }
698 if (definition.getDescription() != null) {
699 setLocationWithinModule(context + ".getDescription()");
700 accept(definition.getDescription());
701 }
702 setLocationWithinModule(context);
703 visitor.visitLeave(definition);
704 setLocationWithinModule(context);
705 }
706
707 public void accept(final InitialFunctionDefinition definition) throws ModuleDataException {
708 checkForInterrupt();
709 if (blocked || definition == null) {
710 return;
711 }
712 data.increaseFunctionDefinitionNumber();
713 location.set(location.size() - 1, "Definition " + (data.getFunctionDefinitionNumber()
714 + data.getFunctionDefinitionNumber()) + " "
715 + (String) location.lastElement());
716 final String context = getCurrentContext().getLocationWithinModule();
717 visitor.visitEnter(definition);
718 if (definition.getFunCon() != null) {
719 setLocationWithinModule(context + ".getFunCon()");
720 accept(definition.getFunCon());
721 }
722 if (definition.getDescription() != null) {
723 setLocationWithinModule(context + ".getDescription()");
724 accept(definition.getDescription());
725 }
726 setLocationWithinModule(context);
727 visitor.visitLeave(definition);
728 setLocationWithinModule(context);
729 }
730
731 public void accept(final FunctionDefinition definition) throws ModuleDataException {
732 checkForInterrupt();
733 if (blocked || definition == null) {
734 return;
735 }
736 data.increaseFunctionDefinitionNumber();
737 location.set(location.size() - 1, "Definition " + (data.getFunctionDefinitionNumber()
738 + data.getFunctionDefinitionNumber()) + " "
739 + (String) location.lastElement());
740 final String context = getCurrentContext().getLocationWithinModule();
741 visitor.visitEnter(definition);
742 if (definition.getFormula() != null) {
743 setLocationWithinModule(context + ".getFormula()");
744 accept(definition.getFormula());
745 }
746 if (definition.getDescription() != null) {
747 setLocationWithinModule(context + ".getDescription()");
748 accept(definition.getDescription());
749 }
750 setLocationWithinModule(context);
751 visitor.visitLeave(definition);
752 setLocationWithinModule(context);
753 }
754
755 public void accept(final Proposition proposition) throws ModuleDataException {
756 checkForInterrupt();
757 if (blocked || proposition == null) {
758 return;
759 }
760 data.increasePropositionNumber();
761 location.set(location.size() - 1, "Proposition " + data.getPropositionNumber() + " "
762 + (String) location.lastElement());
763 final String context = getCurrentContext().getLocationWithinModule();
764 visitor.visitEnter(proposition);
765 if (proposition.getFormula() != null) {
766 setLocationWithinModule(context + ".getFormula()");
767 accept(proposition.getFormula());
768 }
769 if (proposition.getDescription() != null) {
770 setLocationWithinModule(context + ".getDescription()");
771 accept(proposition.getDescription());
772 }
773 if (proposition.getProofList() != null) {
774 setLocationWithinModule(context + ".getProofList()");
775 accept(proposition.getProofList());
776 }
777 if (proposition.getFormalProofList() != null) {
778 setLocationWithinModule(context + ".getFormalProofList()");
779 accept(proposition.getFormalProofList());
780 }
781 setLocationWithinModule(context);
782 visitor.visitLeave(proposition);
783 setLocationWithinModule(context);
784 }
785
786 public void accept(final Rule rule) throws ModuleDataException {
787 checkForInterrupt();
788 if (blocked || rule == null) {
789 return;
790 }
791 data.increaseRuleNumber();
792 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
793 + (String) location.lastElement());
794 final String context = getCurrentContext().getLocationWithinModule();
795 visitor.visitEnter(rule);
796 if (rule.getLinkList() != null) {
797 setLocationWithinModule(context + ".getLinkList()");
798 accept(rule.getLinkList());
799 }
800 if (rule.getDescription() != null) {
801 setLocationWithinModule(context + ".getDescription()");
802 accept(rule.getDescription());
803 }
804 if (rule.getChangedRuleList() != null) {
805 setLocationWithinModule(context + ".getChangedRuleList()");
806 accept(rule.getChangedRuleList());
807 }
808 if (rule.getProofList() != null) {
809 setLocationWithinModule(context + ".getProofList()");
810 accept(rule.getProofList());
811 }
812 setLocationWithinModule(context);
813 visitor.visitLeave(rule);
814 setLocationWithinModule(context);
815 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
816 ruleExistence.put(rule.getName(), newRuleKey);
817 }
818
819 public void accept(final ChangedRuleList list) throws ModuleDataException {
820 checkForInterrupt();
821 if (blocked || list == null) {
822 return;
823 }
824 final String context = getCurrentContext().getLocationWithinModule();
825 visitor.visitEnter(list);
826 setLocationWithinModule(context);
827 for (int i = 0; i < list.size(); i++) {
828 setLocationWithinModule(context + ".get(" + i + ")");
829 accept(list.get(i));
830 }
831 setLocationWithinModule(context);
832 visitor.visitLeave(list);
833 setLocationWithinModule(context);
834 }
835
836 public void accept(final ChangedRule rule) throws ModuleDataException {
837 checkForInterrupt();
838 if (blocked || rule == null) {
839 return;
840 }
841 data.increaseRuleNumber();
842 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
843 + (String) location.lastElement());
844 final String context = getCurrentContext().getLocationWithinModule();
845 visitor.visitEnter(rule);
846 if (rule.getDescription() != null) {
847 setLocationWithinModule(context + ".getDescription()");
848 accept(rule.getDescription());
849 }
850 setLocationWithinModule(context);
851 visitor.visitLeave(rule);
852 setLocationWithinModule(context);
853 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
854 ruleExistence.put(rule.getName(), newRuleKey);
855 }
856
857 public void accept(final LinkList linkList) throws ModuleDataException {
858 checkForInterrupt();
859 if (blocked || linkList == null) {
860 return;
861 }
862 final String context = getCurrentContext().getLocationWithinModule();
863 visitor.visitEnter(linkList);
864 setLocationWithinModule(context);
865 visitor.visitLeave(linkList);
866 setLocationWithinModule(context);
867 }
868
869 public void accept(final ProofList proofList) throws ModuleDataException {
870 checkForInterrupt();
871 if (blocked || proofList == null) {
872 return;
873 }
874 final String context = getCurrentContext().getLocationWithinModule();
875 visitor.visitEnter(proofList);
876 for (int i = 0; i < proofList.size(); i++) {
877 setLocationWithinModule(context + ".get(" + i + ")");
878 accept(proofList.get(i));
879 }
880 setLocationWithinModule(context);
881 visitor.visitLeave(proofList);
882 setLocationWithinModule(context);
883 }
884
885 public void accept(final Proof proof) throws ModuleDataException {
886 checkForInterrupt();
887 if (blocked || proof == null) {
888 return;
889 }
890 final String context = getCurrentContext().getLocationWithinModule();
891 visitor.visitEnter(proof);
892 if (proof.getNonFormalProof() != null) {
893 setLocationWithinModule(context + ".getNonFormalProof()");
894 accept(proof.getNonFormalProof());
895 }
896 setLocationWithinModule(context);
897 visitor.visitLeave(proof);
898 setLocationWithinModule(context);
899 }
900
901 public void accept(final FormalProofList proofList) throws ModuleDataException {
902 checkForInterrupt();
903 if (blocked || proofList == null) {
904 return;
905 }
906 final String context = getCurrentContext().getLocationWithinModule();
907 visitor.visitEnter(proofList);
908 for (int i = 0; i < proofList.size(); i++) {
909 setLocationWithinModule(context + ".get(" + i + ")");
910 accept(proofList.get(i));
911 }
912 setLocationWithinModule(context);
913 visitor.visitLeave(proofList);
914 setLocationWithinModule(context);
915 }
916
917 public void accept(final FormalProof proof) throws ModuleDataException {
918 checkForInterrupt();
919 if (blocked || proof == null) {
920 return;
921 }
922 final String context = getCurrentContext().getLocationWithinModule();
923 visitor.visitEnter(proof);
924 if (proof.getPrecedingText() != null) {
925 setLocationWithinModule(context + ".getPrecedingText()");
926 accept(proof.getFormalProofLineList());
927 }
928 if (proof.getFormalProofLineList() != null) {
929 setLocationWithinModule(context + ".getFormalProofLineList()");
930 accept(proof.getFormalProofLineList());
931 }
932 if (proof.getSucceedingText() != null) {
933 setLocationWithinModule(context + ".getSucceedingText()");
934 accept(proof.getFormalProofLineList());
935 }
936 setLocationWithinModule(context);
937 visitor.visitLeave(proof);
938 setLocationWithinModule(context);
939 }
940
941 public void accept(final FormalProofLineList proofLineList) throws ModuleDataException {
942 checkForInterrupt();
943 if (blocked || proofLineList == null) {
944 return;
945 }
946 final String context = getCurrentContext().getLocationWithinModule();
947 visitor.visitEnter(proofLineList);
948 for (int i = 0; i < proofLineList.size(); i++) {
949 setLocationWithinModule(context + ".get(" + i + ")");
950 if (proofLineList.get(i) instanceof ConditionalProof) {
951 accept((ConditionalProof) proofLineList.get(i));
952 } else {
953 accept(proofLineList.get(i));
954 }
955 }
956 setLocationWithinModule(context);
957 visitor.visitLeave(proofLineList);
958 setLocationWithinModule(context);
959 }
960
961 public void accept(final FormalProofLine proofLine) throws ModuleDataException {
962 checkForInterrupt();
963 if (blocked || proofLine == null) {
964 return;
965 }
966 final String context = getCurrentContext().getLocationWithinModule();
967 visitor.visitEnter(proofLine);
968 if (proofLine.getFormula() != null) {
969 setLocationWithinModule(context + ".getFormula()");
970 accept(proofLine.getFormula());
971 }
972 if (proofLine.getReason() != null) {
973 setLocationWithinModule(context + ".getReason()");
974 accept(proofLine.getReason());
975 }
976 setLocationWithinModule(context);
977 visitor.visitLeave(proofLine);
978 setLocationWithinModule(context);
979 }
980
981 public void accept(final Reason reason) throws ModuleDataException {
982 checkForInterrupt();
983 if (blocked || reason == null) {
984 return;
985 }
986 final String context = getCurrentContext().getLocationWithinModule();
987 visitor.visitEnter(reason);
988 if (reason instanceof ModusPonens) {
989 setLocationWithinModule(context + ".getModusPonens()");
990 accept(((ModusPonens) reason).getModusPonens());
991 } else if (reason instanceof Add) {
992 setLocationWithinModule(context + ".getAdd()");
993 accept(((Add) reason).getAdd());
994 } else if (reason instanceof Rename) {
995 setLocationWithinModule(context + ".getRename()");
996 accept(((Rename) reason).getRename());
997 } else if (reason instanceof SubstFree) {
998 setLocationWithinModule(context + ".getSubstFree()");
999 accept(((SubstFree) reason).getSubstFree());
1000 } else if (reason instanceof SubstFunc) {
1001 setLocationWithinModule(context + ".getSubstFunc()");
1002 accept(((SubstFunc) reason).getSubstFunc());
1003 } else if (reason instanceof SubstPred) {
1004 setLocationWithinModule(context + ".getSubstPred()");
1005 accept(((SubstPred) reason).getSubstPred());
1006 } else if (reason instanceof Existential) {
1007 setLocationWithinModule(context + ".getExistential()");
1008 accept(((Existential) reason).getExistential());
1009 } else if (reason instanceof Universal) {
1010 setLocationWithinModule(context + ".getUniversal()");
1011 accept(((Universal) reason).getUniversal());
1012 } else if (reason instanceof ConditionalProof) {
1013 throw new IllegalArgumentException(
1014 "proof line shall not have a conditional proof as a reason, instead the proof line "
1015 + "itself should be the conditional proof!");
1016 } else {
1017 throw new IllegalArgumentException("unexpected reason type: "
1018 + reason.getClass());
1019 }
1020 setLocationWithinModule(context);
1021 visitor.visitLeave(reason);
1022 setLocationWithinModule(context);
1023 }
1024
1025 public void accept(final ModusPonens reason) throws ModuleDataException {
1026 checkForInterrupt();
1027 if (blocked || reason == null) {
1028 return;
1029 }
1030 final String context = getCurrentContext().getLocationWithinModule();
1031 visitor.visitEnter(reason);
1032 setLocationWithinModule(context);
1033 visitor.visitLeave(reason);
1034 setLocationWithinModule(context);
1035 }
1036
1037 public void accept(final Add reason) throws ModuleDataException {
1038 checkForInterrupt();
1039 if (blocked || reason == null) {
1040 return;
1041 }
1042 final String context = getCurrentContext().getLocationWithinModule();
1043 visitor.visitEnter(reason);
1044 setLocationWithinModule(context);
1045 visitor.visitLeave(reason);
1046 setLocationWithinModule(context);
1047 }
1048
1049 public void accept(final Rename reason) throws ModuleDataException {
1050 checkForInterrupt();
1051 if (blocked || reason == null) {
1052 return;
1053 }
1054 final String context = getCurrentContext().getLocationWithinModule();
1055 visitor.visitEnter(reason);
1056 if (reason.getOriginalSubjectVariable() != null) {
1057 setLocationWithinModule(context + ".getOriginalSubjectVariable()");
1058 accept(reason.getOriginalSubjectVariable());
1059 }
1060 if (reason.getReplacementSubjectVariable() != null) {
1061 setLocationWithinModule(context + ".getReplacementSubjectVariable()");
1062 accept(reason.getReplacementSubjectVariable());
1063 }
1064 setLocationWithinModule(context);
1065 visitor.visitLeave(reason);
1066 setLocationWithinModule(context);
1067 }
1068
1069 public void accept(final SubstFree reason) throws ModuleDataException {
1070 checkForInterrupt();
1071 if (blocked || reason == null) {
1072 return;
1073 }
1074 final String context = getCurrentContext().getLocationWithinModule();
1075 visitor.visitEnter(reason);
1076 if (reason.getSubjectVariable() != null) {
1077 setLocationWithinModule(context + ".getSubjectVariable()");
1078 accept(reason.getSubjectVariable());
1079 }
1080 if (reason.getSubstituteTerm() != null) {
1081 setLocationWithinModule(context + ".getSubstituteTerm()");
1082 accept(new TermVo(reason.getSubstituteTerm()));
1083 }
1084 setLocationWithinModule(context);
1085 visitor.visitLeave(reason);
1086 setLocationWithinModule(context);
1087 }
1088
1089 public void accept(final SubstFunc reason) throws ModuleDataException {
1090 checkForInterrupt();
1091 if (blocked || reason == null) {
1092 return;
1093 }
1094 final String context = getCurrentContext().getLocationWithinModule();
1095 visitor.visitEnter(reason);
1096 if (reason.getFunctionVariable() != null) {
1097 setLocationWithinModule(context + ".getFunctionVariable()");
1098 accept(reason.getFunctionVariable());
1099 }
1100 if (reason.getSubstituteTerm() != null) {
1101 setLocationWithinModule(context + ".getSubstituteTerm()");
1102 accept(new TermVo(reason.getSubstituteTerm()));
1103 }
1104 setLocationWithinModule(context);
1105 visitor.visitLeave(reason);
1106 setLocationWithinModule(context);
1107 }
1108
1109 public void accept(final SubstPred reason) throws ModuleDataException {
1110 checkForInterrupt();
1111 if (blocked || reason == null) {
1112 return;
1113 }
1114 final String context = getCurrentContext().getLocationWithinModule();
1115 visitor.visitEnter(reason);
1116 if (reason.getPredicateVariable() != null) {
1117 setLocationWithinModule(context + ".getPredicateVariable()");
1118 accept(reason.getPredicateVariable());
1119 }
1120 if (reason.getSubstituteFormula() != null) {
1121 setLocationWithinModule(context + ".getSubstituteFormula()");
1122 accept(new FormulaVo(reason.getSubstituteFormula()));
1123 }
1124 setLocationWithinModule(context);
1125 visitor.visitLeave(reason);
1126 setLocationWithinModule(context);
1127 }
1128
1129 public void accept(final Existential reason) throws ModuleDataException {
1130 checkForInterrupt();
1131 if (blocked || reason == null) {
1132 return;
1133 }
1134 final String context = getCurrentContext().getLocationWithinModule();
1135 visitor.visitEnter(reason);
1136 if (reason.getSubjectVariable() != null) {
1137 setLocationWithinModule(context + ".getSubjectVariable()");
1138 accept(reason.getSubjectVariable());
1139 }
1140 setLocationWithinModule(context);
1141 visitor.visitLeave(reason);
1142 setLocationWithinModule(context);
1143 }
1144
1145 public void accept(final Universal reason) throws ModuleDataException {
1146 checkForInterrupt();
1147 if (blocked || reason == null) {
1148 return;
1149 }
1150 final String context = getCurrentContext().getLocationWithinModule();
1151 visitor.visitEnter(reason);
1152 if (reason.getSubjectVariable() != null) {
1153 setLocationWithinModule(context + ".getSubjectVariable()");
1154 accept(reason.getSubjectVariable());
1155 }
1156 setLocationWithinModule(context);
1157 visitor.visitLeave(reason);
1158 setLocationWithinModule(context);
1159 }
1160
1161 public void accept(final ConditionalProof reason) throws ModuleDataException {
1162 checkForInterrupt();
1163 if (blocked || reason == null) {
1164 return;
1165 }
1166 final String context = getCurrentContext().getLocationWithinModule();
1167 visitor.visitEnter(reason);
1168 if (reason.getHypothesis() != null) {
1169 setLocationWithinModule(context + ".getHypothesis()");
1170 accept(reason.getHypothesis());
1171 }
1172 if (reason.getFormalProofLineList() != null) {
1173 setLocationWithinModule(context + ".getFormalProofLineList()");
1174 accept(reason.getFormalProofLineList());
1175 }
1176 if (reason.getConclusion() != null) {
1177 setLocationWithinModule(context + ".getConclusion()");
1178 accept(reason.getConclusion());
1179 }
1180 setLocationWithinModule(context);
1181 visitor.visitLeave(reason);
1182 setLocationWithinModule(context);
1183 }
1184
1185 public void accept(final Hypothesis hypothesis) throws ModuleDataException {
1186 checkForInterrupt();
1187 if (blocked || hypothesis == null) {
1188 return;
1189 }
1190 final String context = getCurrentContext().getLocationWithinModule();
1191 visitor.visitEnter(hypothesis);
1192 if (hypothesis.getFormula() != null) {
1193 setLocationWithinModule(context + ".getFormula()");
1194 accept(hypothesis.getFormula());
1195 }
1196 setLocationWithinModule(context);
1197 visitor.visitLeave(hypothesis);
1198 setLocationWithinModule(context);
1199 }
1200
1201 public void accept(final Conclusion conclusion) throws ModuleDataException {
1202 checkForInterrupt();
1203 if (blocked || conclusion == null) {
1204 return;
1205 }
1206 final String context = getCurrentContext().getLocationWithinModule();
1207 visitor.visitEnter(conclusion);
1208 if (conclusion.getFormula() != null) {
1209 setLocationWithinModule(context + ".getFormula()");
1210 accept(conclusion.getFormula());
1211 }
1212 setLocationWithinModule(context);
1213 visitor.visitLeave(conclusion);
1214 setLocationWithinModule(context);
1215 }
1216
1217 public void accept(final Formula formula) throws ModuleDataException {
1218 checkForInterrupt();
1219 if (blocked || formula == null) {
1220 return;
1221 }
1222 final String context = getCurrentContext().getLocationWithinModule();
1223 visitor.visitEnter(formula);
1224 if (formula.getElement() != null) {
1225 setLocationWithinModule(context + ".getElement()");
1226 accept(formula.getElement());
1227 }
1228 setLocationWithinModule(context);
1229 visitor.visitLeave(formula);
1230 setLocationWithinModule(context);
1231 }
1232
1233 public void accept(final Term term) throws ModuleDataException {
1234 checkForInterrupt();
1235 if (blocked || term == null) {
1236 return;
1237 }
1238 final String context = getCurrentContext().getLocationWithinModule();
1239 visitor.visitEnter(term);
1240 if (term.getElement() != null) {
1241 setLocationWithinModule(context + ".getElement()");
1242 accept(term.getElement());
1243 }
1244 setLocationWithinModule(context);
1245 visitor.visitLeave(term);
1246 setLocationWithinModule(context);
1247 }
1248
1249 public void accept(final Element element) throws ModuleDataException {
1250 checkForInterrupt();
1251 if (blocked || element == null) {
1252 return;
1253 }
1254 final String context = getCurrentContext().getLocationWithinModule();
1255 if (element.isList()) {
1256 setLocationWithinModule(context + ".getList()");
1257 accept(element.getList());
1258 } else if (element.isAtom()) {
1259 setLocationWithinModule(context + ".getAtom()");
1260 accept(element.getAtom());
1261 } else {
1262 throw new IllegalArgumentException("unexpected element type: "
1263 + element.toString());
1264 }
1265 setLocationWithinModule(context);
1266 }
1267
1268 public void accept(final Atom atom) throws ModuleDataException {
1269 checkForInterrupt();
1270 if (blocked || atom == null) {
1271 return;
1272 }
1273 final String context = getCurrentContext().getLocationWithinModule();
1274 visitor.visitEnter(atom);
1275 setLocationWithinModule(context);
1276 visitor.visitLeave(atom);
1277 setLocationWithinModule(context);
1278 }
1279
1280 public void accept(final ElementList list) throws ModuleDataException {
1281 checkForInterrupt();
1282 if (blocked || list == null) {
1283 return;
1284 }
1285 final String context = getCurrentContext().getLocationWithinModule();
1286 visitor.visitEnter(list);
1287 for (int i = 0; i < list.size(); i++) {
1288 setLocationWithinModule(context + ".getElement(" + i + ")");
1289 accept(list.getElement(i));
1290 }
1291 setLocationWithinModule(context);
1292 visitor.visitLeave(list);
1293 setLocationWithinModule(context);
1294 }
1295
1296 public void accept(final LatexList latexList) throws ModuleDataException {
1297 checkForInterrupt();
1298 if (blocked || latexList == null) {
1299 return;
1300 }
1301 final String context = getCurrentContext().getLocationWithinModule();
1302 visitor.visitEnter(latexList);
1303 for (int i = 0; i < latexList.size(); i++) {
1304 setLocationWithinModule(context + ".get(" + i + ")");
1305 accept(latexList.get(i));
1306 }
1307 setLocationWithinModule(context);
1308 visitor.visitLeave(latexList);
1309 setLocationWithinModule(context);
1310 }
1311
1312 public void accept(final Latex latex) throws ModuleDataException {
1313 checkForInterrupt();
1314 if (blocked || latex == null) {
1315 return;
1316 }
1317 final String context = getCurrentContext().getLocationWithinModule();
1318 visitor.visitEnter(latex);
1319 setLocationWithinModule(context);
1320 visitor.visitLeave(latex);
1321 setLocationWithinModule(context);
1322 }
1323
1324
1325
1326
1327
1328
1329 public Node getNode() {
1330 return node;
1331 }
1332
1333
1334
1335
1336
1337
1338 public void setLocationWithinModule(final String locationWithinModule) {
1339 getCurrentContext().setLocationWithinModule(locationWithinModule);
1340 }
1341
1342 public final ModuleContext getCurrentContext() {
1343 return currentContext;
1344 }
1345
1346
1347
1348
1349
1350
1351 public final boolean getBlocked() {
1352 return blocked;
1353 }
1354
1355
1356
1357
1358
1359
1360 public final void setBlocked(final boolean blocked) {
1361 this.blocked = blocked;
1362 }
1363
1364
1365
1366
1367
1368
1369 public double getVisitPercentage() {
1370 if (data == null) {
1371 return 0;
1372 }
1373 return data.getVisitPercentage();
1374 }
1375
1376
1377
1378
1379
1380
1381 private void setLocation(final String text) {
1382 location.setSize(0);
1383 location.push(text);
1384 }
1385
1386 public String getLocationDescription() {
1387 final StringBuffer buffer = new StringBuffer();
1388 for (int i = 0; i < location.size(); i++) {
1389 if (i > 0) {
1390 buffer.append(" / ");
1391 }
1392 buffer.append(location.get(i));
1393 }
1394 return buffer.toString();
1395 }
1396
1397
1398
1399
1400
1401
1402 public QedeqNumbers getCurrentNumbers() {
1403 return new QedeqNumbers(data);
1404 }
1405
1406
1407
1408
1409
1410
1411
1412 public RuleKey getLocalRuleKey(final String name) {
1413 return (RuleKey) ruleExistence.get(name);
1414 }
1415
1416 }
1417