0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.se.visitor;
0017
0018 import java.util.HashMap;
0019 import java.util.Map;
0020 import java.util.Stack;
0021
0022 import org.qedeq.kernel.se.base.list.Atom;
0023 import org.qedeq.kernel.se.base.list.Element;
0024 import org.qedeq.kernel.se.base.list.ElementList;
0025 import org.qedeq.kernel.se.base.module.Add;
0026 import org.qedeq.kernel.se.base.module.Author;
0027 import org.qedeq.kernel.se.base.module.AuthorList;
0028 import org.qedeq.kernel.se.base.module.Axiom;
0029 import org.qedeq.kernel.se.base.module.ChangedRule;
0030 import org.qedeq.kernel.se.base.module.ChangedRuleList;
0031 import org.qedeq.kernel.se.base.module.Chapter;
0032 import org.qedeq.kernel.se.base.module.ChapterList;
0033 import org.qedeq.kernel.se.base.module.Conclusion;
0034 import org.qedeq.kernel.se.base.module.ConditionalProof;
0035 import org.qedeq.kernel.se.base.module.Existential;
0036 import org.qedeq.kernel.se.base.module.FormalProof;
0037 import org.qedeq.kernel.se.base.module.FormalProofLine;
0038 import org.qedeq.kernel.se.base.module.FormalProofLineList;
0039 import org.qedeq.kernel.se.base.module.FormalProofList;
0040 import org.qedeq.kernel.se.base.module.Formula;
0041 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0042 import org.qedeq.kernel.se.base.module.Header;
0043 import org.qedeq.kernel.se.base.module.Hypothesis;
0044 import org.qedeq.kernel.se.base.module.Import;
0045 import org.qedeq.kernel.se.base.module.ImportList;
0046 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
0047 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
0048 import org.qedeq.kernel.se.base.module.Latex;
0049 import org.qedeq.kernel.se.base.module.LatexList;
0050 import org.qedeq.kernel.se.base.module.LinkList;
0051 import org.qedeq.kernel.se.base.module.LiteratureItem;
0052 import org.qedeq.kernel.se.base.module.LiteratureItemList;
0053 import org.qedeq.kernel.se.base.module.Location;
0054 import org.qedeq.kernel.se.base.module.LocationList;
0055 import org.qedeq.kernel.se.base.module.ModusPonens;
0056 import org.qedeq.kernel.se.base.module.Node;
0057 import org.qedeq.kernel.se.base.module.PredicateDefinition;
0058 import org.qedeq.kernel.se.base.module.Proof;
0059 import org.qedeq.kernel.se.base.module.ProofList;
0060 import org.qedeq.kernel.se.base.module.Proposition;
0061 import org.qedeq.kernel.se.base.module.Qedeq;
0062 import org.qedeq.kernel.se.base.module.Reason;
0063 import org.qedeq.kernel.se.base.module.Rename;
0064 import org.qedeq.kernel.se.base.module.Rule;
0065 import org.qedeq.kernel.se.base.module.Section;
0066 import org.qedeq.kernel.se.base.module.SectionList;
0067 import org.qedeq.kernel.se.base.module.Specification;
0068 import org.qedeq.kernel.se.base.module.Subsection;
0069 import org.qedeq.kernel.se.base.module.SubsectionList;
0070 import org.qedeq.kernel.se.base.module.SubstFree;
0071 import org.qedeq.kernel.se.base.module.SubstFunc;
0072 import org.qedeq.kernel.se.base.module.SubstPred;
0073 import org.qedeq.kernel.se.base.module.Term;
0074 import org.qedeq.kernel.se.base.module.Universal;
0075 import org.qedeq.kernel.se.base.module.UsedByList;
0076 import org.qedeq.kernel.se.base.module.VariableList;
0077 import org.qedeq.kernel.se.common.ModuleAddress;
0078 import org.qedeq.kernel.se.common.ModuleContext;
0079 import org.qedeq.kernel.se.common.ModuleDataException;
0080 import org.qedeq.kernel.se.common.RuleKey;
0081 import org.qedeq.kernel.se.dto.module.FormulaVo;
0082 import org.qedeq.kernel.se.dto.module.TermVo;
0083
0084
0085 /**
0086 * Traverse QEDEQ module. Calls visitors of {@link org.qedeq.kernel.se.visitor.QedeqVisitor}
0087 * for non <code>null</code> arguments.
0088 *
0089 * @author Michael Meyling
0090 */
0091 public class QedeqNotNullTraverser implements QedeqTraverser {
0092
0093 /** Current context during creation. */
0094 private final ModuleContext currentContext;
0095
0096 /** Readable traverse location info. */
0097 private final Stack location = new Stack();
0098
0099 /** Herein are various counters for the current node. */
0100 private QedeqNumbers data = new QedeqNumbers(0, 0);
0101
0102 /** Converts chapter and other titles into text. */
0103 private final LatexList2Text transform = new LatexList2Text();
0104
0105 /**
0106 * These methods are called if a node is visited. To start the whole process just call
0107 * {@link #accept(Qedeq)}.
0108 */
0109 private QedeqVisitor visitor;
0110
0111 /** Is sub node traverse currently blocked? */
0112 private boolean blocked;
0113
0114 /** Currently visited node element of QEDEQ module. Might be <code>null</code>. */
0115 private Node node;
0116
0117 /** Maps local {@link ruleName}s to local {@link RuleKey}s. */
0118 private Map ruleExistence;
0119
0120 /**
0121 * Constructor.
0122 *
0123 * @param globalContext Module location information.
0124 * @param visitor These methods are called if a node is visited.
0125 */
0126 public QedeqNotNullTraverser(final ModuleAddress globalContext, final QedeqVisitor visitor) {
0127 currentContext = globalContext.createModuleContext();
0128 this.visitor = visitor;
0129 }
0130
0131 public void accept(final Qedeq qedeq) throws ModuleDataException {
0132 ruleExistence = new HashMap();
0133 setLocation("started");
0134 if (qedeq == null) {
0135 throw new NullPointerException("null QEDEQ module");
0136 }
0137 data = new QedeqNumbers(
0138 (qedeq.getHeader() != null && qedeq.getHeader().getImportList() != null
0139 ? qedeq.getHeader().getImportList().size() : 0),
0140 (qedeq.getChapterList() != null ? qedeq.getChapterList().size() : 0)
0141 );
0142 getCurrentContext().setLocationWithinModule("");
0143 checkForInterrupt();
0144 blocked = false;
0145 final String context = getCurrentContext().getLocationWithinModule();
0146 visitor.visitEnter(qedeq);
0147 if (qedeq.getHeader() != null) {
0148 getCurrentContext().setLocationWithinModule(context + "getHeader()");
0149 accept(qedeq.getHeader());
0150 }
0151 if (qedeq.getChapterList() != null) {
0152 getCurrentContext().setLocationWithinModule(context + "getChapterList()");
0153 accept(qedeq.getChapterList());
0154 }
0155 if (qedeq.getLiteratureItemList() != null) {
0156 getCurrentContext().setLocationWithinModule(context + "getLiteratureItemList()");
0157 accept(qedeq.getLiteratureItemList());
0158 }
0159 setLocationWithinModule(context);
0160 visitor.visitLeave(qedeq);
0161 setLocationWithinModule(context);
0162 setLocation("finished");
0163 data.setFinished(true);
0164 }
0165
0166 /**
0167 * Check if current thread is interrupted.
0168 *
0169 * @throws InterruptException We were interrupted.
0170 */
0171 private void checkForInterrupt() throws InterruptException {
0172 if (Thread.interrupted()) {
0173 throw new InterruptException(getCurrentContext());
0174 }
0175 }
0176
0177 public void accept(final Header header) throws ModuleDataException {
0178 checkForInterrupt();
0179 if (blocked || header == null) {
0180 return;
0181 }
0182 setLocation("analyzing header");
0183 final String context = getCurrentContext().getLocationWithinModule();
0184 visitor.visitEnter(header);
0185 if (header.getSpecification() != null) {
0186 setLocationWithinModule(context + ".getSpecification()");
0187 accept(header.getSpecification());
0188 }
0189 if (header.getTitle() != null) {
0190 setLocationWithinModule(context + ".getTitle()");
0191 accept(header.getTitle());
0192 }
0193 if (header.getSummary() != null) {
0194 setLocationWithinModule(context + ".getSummary()");
0195 accept(header.getSummary());
0196 }
0197 if (header.getAuthorList() != null) {
0198 setLocationWithinModule(context + ".getAuthorList()");
0199 accept(header.getAuthorList());
0200 }
0201 if (header.getImportList() != null) {
0202 setLocationWithinModule(context + ".getImportList()");
0203 accept(header.getImportList());
0204 }
0205 if (header.getUsedByList() != null) {
0206 setLocationWithinModule(context + ".getUsedByList()");
0207 accept(header.getUsedByList());
0208 }
0209 setLocationWithinModule(context);
0210 visitor.visitLeave(header);
0211 setLocationWithinModule(context);
0212 }
0213
0214 public void accept(final UsedByList usedByList) throws ModuleDataException {
0215 checkForInterrupt();
0216 if (blocked || usedByList == null) {
0217 return;
0218 }
0219 location.push("working on used by list");
0220 final String context = getCurrentContext().getLocationWithinModule();
0221 visitor.visitEnter(usedByList);
0222 for (int i = 0; i < usedByList.size(); i++) {
0223 setLocationWithinModule(context + ".get(" + i + ")");
0224 accept(usedByList.get(i));
0225 }
0226 setLocationWithinModule(context);
0227 visitor.visitLeave(usedByList);
0228 setLocationWithinModule(context);
0229 location.pop();
0230 }
0231
0232 public void accept(final ImportList importList) throws ModuleDataException {
0233 checkForInterrupt();
0234 if (blocked || importList == null) {
0235 return;
0236 }
0237 location.push("working on import list");
0238 final String context = getCurrentContext().getLocationWithinModule();
0239 visitor.visitEnter(importList);
0240 for (int i = 0; i < importList.size(); i++) {
0241 setLocationWithinModule(context + ".get(" + i + ")");
0242 accept(importList.get(i));
0243 }
0244 setLocationWithinModule(context);
0245 visitor.visitLeave(importList);
0246 setLocationWithinModule(context);
0247 location.pop();
0248 }
0249
0250 public void accept(final Import imp) throws ModuleDataException {
0251 data.increaseImportNumber();
0252 checkForInterrupt();
0253 if (blocked || imp == null) {
0254 return;
0255 }
0256 location.push("import " + data.getImportNumber() + ": " + imp.getLabel());
0257 final String context = getCurrentContext().getLocationWithinModule();
0258 visitor.visitEnter(imp);
0259 if (imp.getSpecification() != null) {
0260 setLocationWithinModule(context + ".getSpecification()");
0261 accept(imp.getSpecification());
0262 }
0263 setLocationWithinModule(context);
0264 visitor.visitLeave(imp);
0265 setLocationWithinModule(context);
0266 location.pop();
0267 }
0268
0269 public void accept(final Specification specification) throws ModuleDataException {
0270 checkForInterrupt();
0271 if (blocked || specification == null) {
0272 return;
0273 }
0274 final String context = getCurrentContext().getLocationWithinModule();
0275 visitor.visitEnter(specification);
0276 if (specification.getLocationList() != null) {
0277 setLocationWithinModule(context + ".getLocationList()");
0278 accept(specification.getLocationList());
0279 }
0280 setLocationWithinModule(context);
0281 visitor.visitLeave(specification);
0282 setLocationWithinModule(context);
0283 }
0284
0285 public void accept(final LocationList locationList) throws ModuleDataException {
0286 checkForInterrupt();
0287 if (blocked || locationList == null) {
0288 return;
0289 }
0290 final String context = getCurrentContext().getLocationWithinModule();
0291 visitor.visitEnter(locationList);
0292 for (int i = 0; i < locationList.size(); i++) {
0293 setLocationWithinModule(context + ".get(" + i + ")");
0294 accept(locationList.get(i));
0295 }
0296 setLocationWithinModule(context);
0297 visitor.visitLeave(locationList);
0298 setLocationWithinModule(context);
0299 }
0300
0301 public void accept(final Location location) throws ModuleDataException {
0302 checkForInterrupt();
0303 if (blocked || location == null) {
0304 return;
0305 }
0306 final String context = getCurrentContext().getLocationWithinModule();
0307 visitor.visitEnter(location);
0308 setLocationWithinModule(context);
0309 visitor.visitLeave(location);
0310 setLocationWithinModule(context);
0311 }
0312
0313 public void accept(final AuthorList authorList) throws ModuleDataException {
0314 checkForInterrupt();
0315 if (blocked || authorList == null) {
0316 return;
0317 }
0318 final String context = getCurrentContext().getLocationWithinModule();
0319 visitor.visitEnter(authorList);
0320 for (int i = 0; i < authorList.size(); i++) {
0321 setLocationWithinModule(context + ".get(" + i + ")");
0322 accept(authorList.get(i));
0323 }
0324 setLocationWithinModule(context);
0325 visitor.visitLeave(authorList);
0326 setLocationWithinModule(context);
0327 }
0328
0329 public void accept(final Author author) throws ModuleDataException {
0330 checkForInterrupt();
0331 if (blocked || author == null) {
0332 return;
0333 }
0334 final String context = getCurrentContext().getLocationWithinModule();
0335 visitor.visitEnter(author);
0336 if (author.getName() != null) {
0337 setLocationWithinModule(context + ".getName()");
0338 accept(author.getName());
0339 }
0340 setLocationWithinModule(context);
0341 visitor.visitLeave(author);
0342 setLocationWithinModule(context);
0343 }
0344
0345 public void accept(final ChapterList chapterList) throws ModuleDataException {
0346 checkForInterrupt();
0347 if (blocked || chapterList == null) {
0348 return;
0349 }
0350 final String context = getCurrentContext().getLocationWithinModule();
0351 visitor.visitEnter(chapterList);
0352 for (int i = 0; i < chapterList.size(); i++) {
0353 setLocationWithinModule(context + ".get(" + i + ")");
0354 accept(chapterList.get(i));
0355 }
0356 setLocationWithinModule(context);
0357 visitor.visitLeave(chapterList);
0358 setLocationWithinModule(context);
0359 }
0360
0361 public void accept(final Chapter chapter) throws ModuleDataException {
0362 checkForInterrupt();
0363 if (blocked || chapter == null) {
0364 return;
0365 }
0366 data.increaseChapterNumber(
0367 (chapter.getSectionList() != null ? chapter.getSectionList().size() : 0),
0368 chapter.getNoNumber() == null || !chapter.getNoNumber().booleanValue()
0369 );
0370 if (data.isChapterNumbering()) {
0371 setLocation("Chapter " + data.getChapterNumber() + " "
0372 + transform.transform(chapter.getTitle()));
0373 } else {
0374 setLocation(transform.transform(chapter.getTitle()));
0375 }
0376 final String context = getCurrentContext().getLocationWithinModule();
0377 visitor.visitEnter(chapter);
0378 if (chapter.getTitle() != null) {
0379 setLocationWithinModule(context + ".getTitle()");
0380 accept(chapter.getTitle());
0381 }
0382 if (chapter.getIntroduction() != null) {
0383 setLocationWithinModule(context + ".getIntroduction()");
0384 accept(chapter.getIntroduction());
0385 }
0386 if (chapter.getSectionList() != null) {
0387 setLocationWithinModule(context + ".getSectionList()");
0388 accept(chapter.getSectionList());
0389 }
0390 setLocationWithinModule(context);
0391 visitor.visitLeave(chapter);
0392 setLocationWithinModule(context);
0393 }
0394
0395 public void accept(final LiteratureItemList literatureItemList)
0396 throws ModuleDataException {
0397 checkForInterrupt();
0398 if (blocked || literatureItemList == null) {
0399 return;
0400 }
0401 setLocation("working on literature list");
0402 final String context = getCurrentContext().getLocationWithinModule();
0403 visitor.visitEnter(literatureItemList);
0404 for (int i = 0; i < literatureItemList.size(); i++) {
0405 setLocationWithinModule(context + ".get(" + i + ")");
0406 accept(literatureItemList.get(i));
0407 }
0408 setLocationWithinModule(context);
0409 visitor.visitLeave(literatureItemList);
0410 setLocationWithinModule(context);
0411 }
0412
0413 public void accept(final LiteratureItem item) throws ModuleDataException {
0414 checkForInterrupt();
0415 if (blocked || item == null) {
0416 return;
0417 }
0418 final String context = getCurrentContext().getLocationWithinModule();
0419 visitor.visitEnter(item);
0420 if (item.getItem() != null) {
0421 setLocationWithinModule(context + ".getItem()");
0422 accept(item.getItem());
0423 }
0424 setLocationWithinModule(context);
0425 visitor.visitLeave(item);
0426 setLocationWithinModule(context);
0427 }
0428
0429 public void accept(final SectionList sectionList) throws ModuleDataException {
0430 checkForInterrupt();
0431 if (blocked || sectionList == null) {
0432 return;
0433 }
0434 final String context = getCurrentContext().getLocationWithinModule();
0435 visitor.visitEnter(sectionList);
0436 for (int i = 0; i < sectionList.size(); i++) {
0437 setLocationWithinModule(context + ".get(" + i + ")");
0438 accept(sectionList.get(i));
0439 }
0440 setLocationWithinModule(context);
0441 visitor.visitLeave(sectionList);
0442 setLocationWithinModule(context);
0443 }
0444
0445 public void accept(final Section section) throws ModuleDataException {
0446 checkForInterrupt();
0447 if (blocked || section == null) {
0448 return;
0449 }
0450 data.increaseSectionNumber(
0451 (section.getSubsectionList() != null ? section.getSubsectionList().size() : 0),
0452 section.getNoNumber() == null || !section.getNoNumber().booleanValue()
0453 );
0454 String title = "";
0455 if (data.isChapterNumbering()) {
0456 title += data.getChapterNumber();
0457 }
0458 if (data.isSectionNumbering()) {
0459 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
0460 }
0461 if (section.getTitle() != null) {
0462 title += " " + transform.transform(section.getTitle());
0463 }
0464 location.push(title);
0465 final String context = getCurrentContext().getLocationWithinModule();
0466 visitor.visitEnter(section);
0467 if (section.getTitle() != null) {
0468 setLocationWithinModule(context + ".getTitle()");
0469 accept(section.getTitle());
0470 }
0471 if (section.getIntroduction() != null) {
0472 setLocationWithinModule(context + ".getIntroduction()");
0473 accept(section.getIntroduction());
0474 }
0475 if (section.getSubsectionList() != null) {
0476 setLocationWithinModule(context + ".getSubsectionList()");
0477 accept(section.getSubsectionList());
0478 }
0479 setLocationWithinModule(context);
0480 visitor.visitLeave(section);
0481 setLocationWithinModule(context);
0482 location.pop();
0483 }
0484
0485 public void accept(final SubsectionList subsectionList) throws ModuleDataException {
0486 checkForInterrupt();
0487 if (blocked || subsectionList == null) {
0488 return;
0489 }
0490 final String context = getCurrentContext().getLocationWithinModule();
0491 visitor.visitEnter(subsectionList);
0492 for (int i = 0; i < subsectionList.size(); i++) {
0493 setLocationWithinModule(context + ".get(" + i + ")");
0494 // TODO mime 20050608: here the Subsection context is type dependently specified
0495 if (subsectionList.get(i) instanceof Subsection) {
0496 accept((Subsection) subsectionList.get(i));
0497 } else if (subsectionList.get(i) instanceof Node) {
0498 accept((Node) subsectionList.get(i));
0499 } else if (subsectionList.get(i) == null) {
0500 // ignore
0501 } else {
0502 throw new IllegalArgumentException("unexpected subsection type: "
0503 + subsectionList.get(i).getClass());
0504 }
0505 }
0506 setLocationWithinModule(context);
0507 visitor.visitLeave(subsectionList);
0508 setLocationWithinModule(context);
0509 }
0510
0511 public void accept(final Subsection subsection) throws ModuleDataException {
0512 checkForInterrupt();
0513 if (blocked || subsection == null) {
0514 return;
0515 }
0516 data.increaseSubsectionNumber();
0517 String title = "";
0518 if (data.isChapterNumbering()) {
0519 title += data.getChapterNumber();
0520 }
0521 if (data.isSectionNumbering()) {
0522 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
0523 }
0524 title += (title.length() > 0 ? "." : "") + data.getSubsectionNumber();
0525 if (subsection.getTitle() != null) {
0526 title += " " + transform.transform(subsection.getTitle());
0527 }
0528 title = title + " [" + subsection.getId() + "]";
0529 location.push(title);
0530 final String context = getCurrentContext().getLocationWithinModule();
0531 visitor.visitEnter(subsection);
0532 if (subsection.getTitle() != null) {
0533 setLocationWithinModule(context + ".getTitle()");
0534 accept(subsection.getTitle());
0535 }
0536 if (subsection.getLatex() != null) {
0537 setLocationWithinModule(context + ".getLatex()");
0538 accept(subsection.getLatex());
0539 }
0540 setLocationWithinModule(context);
0541 visitor.visitLeave(subsection);
0542 setLocationWithinModule(context);
0543 location.pop();
0544 }
0545
0546 public void accept(final Node node) throws ModuleDataException {
0547 checkForInterrupt();
0548 data.increaseNodeNumber();
0549 if (blocked || node == null) {
0550 return;
0551 }
0552 this.node = node;
0553 String title = "";
0554 if (node.getTitle() != null) {
0555 title = transform.transform(node.getTitle());
0556 }
0557 title = title + " [" + node.getId() + "]";
0558 location.push(title);
0559 final String context = getCurrentContext().getLocationWithinModule();
0560 visitor.visitEnter(node);
0561 if (node.getName() != null) {
0562 setLocationWithinModule(context + ".getName()");
0563 accept(node.getName());
0564 }
0565 if (node.getTitle() != null) {
0566 setLocationWithinModule(context + ".getTitle()");
0567 accept(node.getTitle());
0568 }
0569 if (node.getPrecedingText() != null) {
0570 setLocationWithinModule(context + ".getPrecedingText()");
0571 accept(node.getPrecedingText());
0572 }
0573 if (node.getNodeType() != null) {
0574 setLocationWithinModule(context + ".getNodeType()");
0575 if (node.getNodeType() instanceof Axiom) {
0576 setLocationWithinModule(context + ".getNodeType().getAxiom()");
0577 accept((Axiom) node.getNodeType());
0578 } else if (node.getNodeType() instanceof InitialPredicateDefinition) {
0579 setLocationWithinModule(context + ".getNodeType().getInitialPredicateDefinition()");
0580 accept((InitialPredicateDefinition) node.getNodeType());
0581 } else if (node.getNodeType() instanceof PredicateDefinition) {
0582 setLocationWithinModule(context + ".getNodeType().getPredicateDefinition()");
0583 accept((PredicateDefinition) node.getNodeType());
0584 } else if (node.getNodeType() instanceof InitialFunctionDefinition) {
0585 setLocationWithinModule(context + ".getNodeType().getInitialFunctionDefinition()");
0586 accept((FunctionDefinition) node.getNodeType());
0587 } else if (node.getNodeType() instanceof FunctionDefinition) {
0588 setLocationWithinModule(context + ".getNodeType().getFunctionDefinition()");
0589 accept((FunctionDefinition) node.getNodeType());
0590 } else if (node.getNodeType() instanceof Proposition) {
0591 setLocationWithinModule(context + ".getNodeType().getProposition()");
0592 accept((Proposition) node.getNodeType());
0593 } else if (node.getNodeType() instanceof Rule) {
0594 setLocationWithinModule(context + ".getNodeType().getRule()");
0595 accept((Rule) node.getNodeType());
0596 } else {
0597 throw new IllegalArgumentException("unexpected node type: "
0598 + node.getNodeType().getClass());
0599 }
0600 }
0601 if (node.getSucceedingText() != null) {
0602 setLocationWithinModule(context + ".getSucceedingText()");
0603 accept(node.getSucceedingText());
0604 }
0605 setLocationWithinModule(context);
0606 visitor.visitLeave(node);
0607 setLocationWithinModule(context);
0608 location.pop();
0609 this.node = null;
0610 }
0611
0612 public void accept(final Axiom axiom) throws ModuleDataException {
0613 checkForInterrupt();
0614 if (blocked || axiom == null) {
0615 return;
0616 }
0617 data.increaseAxiomNumber();
0618 location.set(location.size() - 1, "Axiom " + data.getAxiomNumber() + " "
0619 + (String) location.lastElement());
0620 final String context = getCurrentContext().getLocationWithinModule();
0621 visitor.visitEnter(axiom);
0622 if (axiom.getFormula() != null) {
0623 setLocationWithinModule(context + ".getFormula()");
0624 accept(axiom.getFormula());
0625 }
0626 if (axiom.getDescription() != null) {
0627 setLocationWithinModule(context + ".getDescription()");
0628 accept(axiom.getDescription());
0629 }
0630 setLocationWithinModule(context);
0631 visitor.visitLeave(axiom);
0632 setLocationWithinModule(context);
0633 }
0634
0635 public void accept(final PredicateDefinition definition)
0636 throws ModuleDataException {
0637 checkForInterrupt();
0638 if (blocked || definition == null) {
0639 return;
0640 }
0641 data.increasePredicateDefinitionNumber();
0642 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
0643 + data.getFunctionDefinitionNumber()) + " "
0644 + (String) location.lastElement());
0645 final String context = getCurrentContext().getLocationWithinModule();
0646 visitor.visitEnter(definition);
0647 if (definition.getFormula() != null) {
0648 setLocationWithinModule(context + ".getFormula()");
0649 accept(definition.getFormula());
0650 }
0651 if (definition.getDescription() != null) {
0652 setLocationWithinModule(context + ".getDescription()");
0653 accept(definition.getDescription());
0654 }
0655 setLocationWithinModule(context);
0656 visitor.visitLeave(definition);
0657 setLocationWithinModule(context);
0658 }
0659
0660 public void accept(final InitialPredicateDefinition definition)
0661 throws ModuleDataException {
0662 checkForInterrupt();
0663 if (blocked || definition == null) {
0664 return;
0665 }
0666 data.increasePredicateDefinitionNumber();
0667 location.set(location.size() - 1, "Definition "
0668 + (data.getPredicateDefinitionNumber() + data
0669 .getFunctionDefinitionNumber()) + " "
0670 + (String) location.lastElement());
0671 final String context = getCurrentContext().getLocationWithinModule();
0672 visitor.visitEnter(definition);
0673 if (definition.getPredCon() != null) {
0674 setLocationWithinModule(context + ".getPredCon()");
0675 accept(definition.getPredCon());
0676 }
0677 if (definition.getDescription() != null) {
0678 setLocationWithinModule(context + ".getDescription()");
0679 accept(definition.getDescription());
0680 }
0681 setLocationWithinModule(context);
0682 visitor.visitLeave(definition);
0683 setLocationWithinModule(context);
0684 }
0685
0686 public void accept(final InitialFunctionDefinition definition) throws ModuleDataException {
0687 checkForInterrupt();
0688 if (blocked || definition == null) {
0689 return;
0690 }
0691 data.increaseFunctionDefinitionNumber();
0692 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
0693 + data.getFunctionDefinitionNumber()) + " "
0694 + (String) location.lastElement());
0695 final String context = getCurrentContext().getLocationWithinModule();
0696 visitor.visitEnter(definition);
0697 if (definition.getFunCon() != null) {
0698 setLocationWithinModule(context + ".getFunCon()");
0699 accept(definition.getFunCon());
0700 }
0701 if (definition.getDescription() != null) {
0702 setLocationWithinModule(context + ".getDescription()");
0703 accept(definition.getDescription());
0704 }
0705 setLocationWithinModule(context);
0706 visitor.visitLeave(definition);
0707 setLocationWithinModule(context);
0708 }
0709
0710 public void accept(final FunctionDefinition definition) throws ModuleDataException {
0711 checkForInterrupt();
0712 if (blocked || definition == null) {
0713 return;
0714 }
0715 data.increaseFunctionDefinitionNumber();
0716 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
0717 + data.getFunctionDefinitionNumber()) + " "
0718 + (String) location.lastElement());
0719 final String context = getCurrentContext().getLocationWithinModule();
0720 visitor.visitEnter(definition);
0721 if (definition.getFormula() != null) {
0722 setLocationWithinModule(context + ".getFormula()");
0723 accept(definition.getFormula());
0724 }
0725 if (definition.getDescription() != null) {
0726 setLocationWithinModule(context + ".getDescription()");
0727 accept(definition.getDescription());
0728 }
0729 setLocationWithinModule(context);
0730 visitor.visitLeave(definition);
0731 setLocationWithinModule(context);
0732 }
0733
0734 public void accept(final Proposition proposition) throws ModuleDataException {
0735 checkForInterrupt();
0736 if (blocked || proposition == null) {
0737 return;
0738 }
0739 data.increasePropositionNumber();
0740 location.set(location.size() - 1, "Proposition " + data.getPropositionNumber() + " "
0741 + (String) location.lastElement());
0742 final String context = getCurrentContext().getLocationWithinModule();
0743 visitor.visitEnter(proposition);
0744 if (proposition.getFormula() != null) {
0745 setLocationWithinModule(context + ".getFormula()");
0746 accept(proposition.getFormula());
0747 }
0748 if (proposition.getDescription() != null) {
0749 setLocationWithinModule(context + ".getDescription()");
0750 accept(proposition.getDescription());
0751 }
0752 if (proposition.getProofList() != null) {
0753 setLocationWithinModule(context + ".getProofList()");
0754 accept(proposition.getProofList());
0755 }
0756 if (proposition.getFormalProofList() != null) {
0757 setLocationWithinModule(context + ".getFormalProofList()");
0758 accept(proposition.getFormalProofList());
0759 }
0760 setLocationWithinModule(context);
0761 visitor.visitLeave(proposition);
0762 setLocationWithinModule(context);
0763 }
0764
0765 public void accept(final Rule rule) throws ModuleDataException {
0766 checkForInterrupt();
0767 if (blocked || rule == null) {
0768 return;
0769 }
0770 data.increaseRuleNumber();
0771 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
0772 + (String) location.lastElement());
0773 final String context = getCurrentContext().getLocationWithinModule();
0774 visitor.visitEnter(rule);
0775 if (rule.getLinkList() != null) {
0776 setLocationWithinModule(context + ".getLinkList()");
0777 accept(rule.getLinkList());
0778 }
0779 if (rule.getDescription() != null) {
0780 setLocationWithinModule(context + ".getDescription()");
0781 accept(rule.getDescription());
0782 }
0783 if (rule.getChangedRuleList() != null) {
0784 setLocationWithinModule(context + ".getChangedRuleList()");
0785 accept(rule.getChangedRuleList());
0786 }
0787 if (rule.getProofList() != null) {
0788 setLocationWithinModule(context + ".getProofList()");
0789 accept(rule.getProofList());
0790 }
0791 setLocationWithinModule(context);
0792 visitor.visitLeave(rule);
0793 setLocationWithinModule(context);
0794 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
0795 ruleExistence.put(rule.getName(), newRuleKey);
0796 }
0797
0798 public void accept(final ChangedRuleList list) throws ModuleDataException {
0799 checkForInterrupt();
0800 if (blocked || list == null) {
0801 return;
0802 }
0803 final String context = getCurrentContext().getLocationWithinModule();
0804 visitor.visitEnter(list);
0805 setLocationWithinModule(context);
0806 for (int i = 0; i < list.size(); i++) {
0807 setLocationWithinModule(context + ".get(" + i + ")");
0808 accept(list.get(i));
0809 }
0810 setLocationWithinModule(context);
0811 visitor.visitLeave(list);
0812 setLocationWithinModule(context);
0813 }
0814
0815 public void accept(final ChangedRule rule) throws ModuleDataException {
0816 checkForInterrupt();
0817 if (blocked || rule == null) {
0818 return;
0819 }
0820 data.increaseRuleNumber();
0821 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
0822 + (String) location.lastElement());
0823 final String context = getCurrentContext().getLocationWithinModule();
0824 visitor.visitEnter(rule);
0825 if (rule.getDescription() != null) {
0826 setLocationWithinModule(context + ".getDescription()");
0827 accept(rule.getDescription());
0828 }
0829 setLocationWithinModule(context);
0830 visitor.visitLeave(rule);
0831 setLocationWithinModule(context);
0832 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
0833 ruleExistence.put(rule.getName(), newRuleKey);
0834 }
0835
0836 public void accept(final LinkList linkList) throws ModuleDataException {
0837 checkForInterrupt();
0838 if (blocked || linkList == null) {
0839 return;
0840 }
0841 final String context = getCurrentContext().getLocationWithinModule();
0842 visitor.visitEnter(linkList);
0843 setLocationWithinModule(context);
0844 visitor.visitLeave(linkList);
0845 setLocationWithinModule(context);
0846 }
0847
0848 public void accept(final VariableList variableList) throws ModuleDataException {
0849 checkForInterrupt();
0850 if (blocked || variableList == null) {
0851 return;
0852 }
0853 final String context = getCurrentContext().getLocationWithinModule();
0854 visitor.visitEnter(variableList);
0855 for (int i = 0; i < variableList.size(); i++) {
0856 final String piece = context + ".get(" + i + ")";
0857 setLocationWithinModule(piece);
0858 if (variableList.get(i) != null) {
0859 if (variableList.get(i).isList()) {
0860 setLocationWithinModule(piece + ".getList()");
0861 accept(variableList.get(i).getList());
0862 } else if (variableList.get(i).isAtom()) {
0863 setLocationWithinModule(piece + ".getAtom()");
0864 accept(variableList.get(i).getAtom());
0865 } else {
0866 throw new IllegalArgumentException("unexpected element type: "
0867 + variableList.get(i).toString());
0868 }
0869 }
0870 }
0871 setLocationWithinModule(context);
0872 visitor.visitLeave(variableList);
0873 setLocationWithinModule(context);
0874 }
0875
0876 public void accept(final ProofList proofList) throws ModuleDataException {
0877 checkForInterrupt();
0878 if (blocked || proofList == null) {
0879 return;
0880 }
0881 final String context = getCurrentContext().getLocationWithinModule();
0882 visitor.visitEnter(proofList);
0883 for (int i = 0; i < proofList.size(); i++) {
0884 setLocationWithinModule(context + ".get(" + i + ")");
0885 accept(proofList.get(i));
0886 }
0887 setLocationWithinModule(context);
0888 visitor.visitLeave(proofList);
0889 setLocationWithinModule(context);
0890 }
0891
0892 public void accept(final Proof proof) throws ModuleDataException {
0893 checkForInterrupt();
0894 if (blocked || proof == null) {
0895 return;
0896 }
0897 final String context = getCurrentContext().getLocationWithinModule();
0898 visitor.visitEnter(proof);
0899 if (proof.getNonFormalProof() != null) {
0900 setLocationWithinModule(context + ".getNonFormalProof()");
0901 accept(proof.getNonFormalProof());
0902 }
0903 setLocationWithinModule(context);
0904 visitor.visitLeave(proof);
0905 setLocationWithinModule(context);
0906 }
0907
0908 public void accept(final FormalProofList proofList) throws ModuleDataException {
0909 checkForInterrupt();
0910 if (blocked || proofList == null) {
0911 return;
0912 }
0913 final String context = getCurrentContext().getLocationWithinModule();
0914 visitor.visitEnter(proofList);
0915 for (int i = 0; i < proofList.size(); i++) {
0916 setLocationWithinModule(context + ".get(" + i + ")");
0917 accept(proofList.get(i));
0918 }
0919 setLocationWithinModule(context);
0920 visitor.visitLeave(proofList);
0921 setLocationWithinModule(context);
0922 }
0923
0924 public void accept(final FormalProof proof) throws ModuleDataException {
0925 checkForInterrupt();
0926 if (blocked || proof == null) {
0927 return;
0928 }
0929 final String context = getCurrentContext().getLocationWithinModule();
0930 visitor.visitEnter(proof);
0931 if (proof.getPrecedingText() != null) {
0932 setLocationWithinModule(context + ".getPrecedingText()");
0933 accept(proof.getFormalProofLineList());
0934 }
0935 if (proof.getFormalProofLineList() != null) {
0936 setLocationWithinModule(context + ".getFormalProofLineList()");
0937 accept(proof.getFormalProofLineList());
0938 }
0939 if (proof.getSucceedingText() != null) {
0940 setLocationWithinModule(context + ".getSucceedingText()");
0941 accept(proof.getFormalProofLineList());
0942 }
0943 setLocationWithinModule(context);
0944 visitor.visitLeave(proof);
0945 setLocationWithinModule(context);
0946 }
0947
0948 public void accept(final FormalProofLineList proofLineList) throws ModuleDataException {
0949 checkForInterrupt();
0950 if (blocked || proofLineList == null) {
0951 return;
0952 }
0953 final String context = getCurrentContext().getLocationWithinModule();
0954 visitor.visitEnter(proofLineList);
0955 for (int i = 0; i < proofLineList.size(); i++) {
0956 setLocationWithinModule(context + ".get(" + i + ")");
0957 if (proofLineList.get(i) instanceof ConditionalProof) {
0958 accept((ConditionalProof) proofLineList.get(i));
0959 } else {
0960 accept(proofLineList.get(i));
0961 }
0962 }
0963 setLocationWithinModule(context);
0964 visitor.visitLeave(proofLineList);
0965 setLocationWithinModule(context);
0966 }
0967
0968 public void accept(final FormalProofLine proofLine) throws ModuleDataException {
0969 checkForInterrupt();
0970 if (blocked || proofLine == null) {
0971 return;
0972 }
0973 final String context = getCurrentContext().getLocationWithinModule();
0974 visitor.visitEnter(proofLine);
0975 if (proofLine.getFormula() != null) {
0976 setLocationWithinModule(context + ".getFormula()");
0977 accept(proofLine.getFormula());
0978 }
0979 if (proofLine.getReason() != null) {
0980 setLocationWithinModule(context + ".getReason()");
0981 accept(proofLine.getReason());
0982 }
0983 setLocationWithinModule(context);
0984 visitor.visitLeave(proofLine);
0985 setLocationWithinModule(context);
0986 }
0987
0988 public void accept(final Reason reason) throws ModuleDataException {
0989 checkForInterrupt();
0990 if (blocked || reason == null) {
0991 return;
0992 }
0993 final String context = getCurrentContext().getLocationWithinModule();
0994 visitor.visitEnter(reason);
0995 if (reason instanceof ModusPonens) {
0996 setLocationWithinModule(context + ".getModusPonens()");
0997 accept(((ModusPonens) reason).getModusPonens());
0998 } else if (reason instanceof Add) {
0999 setLocationWithinModule(context + ".getAdd()");
1000 accept(((Add) reason).getAdd());
1001 } else if (reason instanceof Rename) {
1002 setLocationWithinModule(context + ".getRename()");
1003 accept(((Rename) reason).getRename());
1004 } else if (reason instanceof SubstFree) {
1005 setLocationWithinModule(context + ".getSubstFree()");
1006 accept(((SubstFree) reason).getSubstFree());
1007 } else if (reason instanceof SubstFunc) {
1008 setLocationWithinModule(context + ".getSubstFunc()");
1009 accept(((SubstFunc) reason).getSubstFunc());
1010 } else if (reason instanceof SubstPred) {
1011 setLocationWithinModule(context + ".getSubstPred()");
1012 accept(((SubstPred) reason).getSubstPred());
1013 } else if (reason instanceof Existential) {
1014 setLocationWithinModule(context + ".getExistential()");
1015 accept(((Existential) reason).getExistential());
1016 } else if (reason instanceof Universal) {
1017 setLocationWithinModule(context + ".getUniversal()");
1018 accept(((Universal) reason).getUniversal());
1019 } else {
1020 throw new IllegalArgumentException("unexpected reason type: "
1021 + reason.getClass());
1022 }
1023 setLocationWithinModule(context);
1024 visitor.visitLeave(reason);
1025 setLocationWithinModule(context);
1026 }
1027
1028 public void accept(final ModusPonens reason) throws ModuleDataException {
1029 checkForInterrupt();
1030 if (blocked || reason == null) {
1031 return;
1032 }
1033 final String context = getCurrentContext().getLocationWithinModule();
1034 visitor.visitEnter(reason);
1035 setLocationWithinModule(context);
1036 visitor.visitLeave(reason);
1037 setLocationWithinModule(context);
1038 }
1039
1040 public void accept(final Add reason) throws ModuleDataException {
1041 checkForInterrupt();
1042 if (blocked || reason == null) {
1043 return;
1044 }
1045 final String context = getCurrentContext().getLocationWithinModule();
1046 visitor.visitEnter(reason);
1047 setLocationWithinModule(context);
1048 visitor.visitLeave(reason);
1049 setLocationWithinModule(context);
1050 }
1051
1052 public void accept(final Rename reason) throws ModuleDataException {
1053 checkForInterrupt();
1054 if (blocked || reason == null) {
1055 return;
1056 }
1057 final String context = getCurrentContext().getLocationWithinModule();
1058 visitor.visitEnter(reason);
1059 if (reason.getOriginalSubjectVariable() != null) {
1060 setLocationWithinModule(context + ".getOriginalSubjectVariable()");
1061 accept(reason.getOriginalSubjectVariable());
1062 }
1063 if (reason.getReplacementSubjectVariable() != null) {
1064 setLocationWithinModule(context + ".getReplacementSubjectVariable()");
1065 accept(reason.getReplacementSubjectVariable());
1066 }
1067 setLocationWithinModule(context);
1068 visitor.visitLeave(reason);
1069 setLocationWithinModule(context);
1070 }
1071
1072 public void accept(final SubstFree reason) throws ModuleDataException {
1073 checkForInterrupt();
1074 if (blocked || reason == null) {
1075 return;
1076 }
1077 final String context = getCurrentContext().getLocationWithinModule();
1078 visitor.visitEnter(reason);
1079 if (reason.getSubjectVariable() != null) {
1080 setLocationWithinModule(context + ".getSubjectVariable()");
1081 accept(reason.getSubjectVariable());
1082 }
1083 if (reason.getSubstituteTerm() != null) {
1084 setLocationWithinModule(context + ".getSubstituteTerm()");
1085 accept(new TermVo(reason.getSubstituteTerm()));
1086 }
1087 setLocationWithinModule(context);
1088 visitor.visitLeave(reason);
1089 setLocationWithinModule(context);
1090 }
1091
1092 public void accept(final SubstFunc reason) throws ModuleDataException {
1093 checkForInterrupt();
1094 if (blocked || reason == null) {
1095 return;
1096 }
1097 final String context = getCurrentContext().getLocationWithinModule();
1098 visitor.visitEnter(reason);
1099 if (reason.getFunctionVariable() != null) {
1100 setLocationWithinModule(context + ".getFunctionVariable()");
1101 accept(reason.getFunctionVariable());
1102 }
1103 if (reason.getSubstituteTerm() != null) {
1104 setLocationWithinModule(context + ".getSubstituteTerm()");
1105 accept(new TermVo(reason.getSubstituteTerm()));
1106 }
1107 setLocationWithinModule(context);
1108 visitor.visitLeave(reason);
1109 setLocationWithinModule(context);
1110 }
1111
1112 public void accept(final SubstPred reason) throws ModuleDataException {
1113 checkForInterrupt();
1114 if (blocked || reason == null) {
1115 return;
1116 }
1117 final String context = getCurrentContext().getLocationWithinModule();
1118 visitor.visitEnter(reason);
1119 if (reason.getPredicateVariable() != null) {
1120 setLocationWithinModule(context + ".getPredicateVariable()");
1121 accept(reason.getPredicateVariable());
1122 }
1123 if (reason.getSubstituteFormula() != null) {
1124 setLocationWithinModule(context + ".getSubstituteFormula()");
1125 accept(new FormulaVo(reason.getSubstituteFormula()));
1126 }
1127 setLocationWithinModule(context);
1128 visitor.visitLeave(reason);
1129 setLocationWithinModule(context);
1130 }
1131
1132 public void accept(final Existential reason) throws ModuleDataException {
1133 checkForInterrupt();
1134 if (blocked || reason == null) {
1135 return;
1136 }
1137 final String context = getCurrentContext().getLocationWithinModule();
1138 visitor.visitEnter(reason);
1139 if (reason.getSubjectVariable() != null) {
1140 setLocationWithinModule(context + ".getSubjectVariable()");
1141 accept(reason.getSubjectVariable());
1142 }
1143 setLocationWithinModule(context);
1144 visitor.visitLeave(reason);
1145 setLocationWithinModule(context);
1146 }
1147
1148 public void accept(final Universal reason) throws ModuleDataException {
1149 checkForInterrupt();
1150 if (blocked || reason == null) {
1151 return;
1152 }
1153 final String context = getCurrentContext().getLocationWithinModule();
1154 visitor.visitEnter(reason);
1155 if (reason.getSubjectVariable() != null) {
1156 setLocationWithinModule(context + ".getSubjectVariable()");
1157 accept(reason.getSubjectVariable());
1158 }
1159 setLocationWithinModule(context);
1160 visitor.visitLeave(reason);
1161 setLocationWithinModule(context);
1162 }
1163
1164 public void accept(final ConditionalProof reason) throws ModuleDataException {
1165 checkForInterrupt();
1166 if (blocked || reason == null) {
1167 return;
1168 }
1169 final String context = getCurrentContext().getLocationWithinModule();
1170 visitor.visitEnter(reason);
1171 if (reason.getHypothesis() != null) {
1172 setLocationWithinModule(context + ".getHypothesis()");
1173 accept(reason.getHypothesis());
1174 }
1175 if (reason.getFormalProofLineList() != null) {
1176 setLocationWithinModule(context + ".getFormalProofLineList()");
1177 accept(reason.getFormalProofLineList());
1178 }
1179 if (reason.getConclusion() != null) {
1180 setLocationWithinModule(context + ".getConclusion()");
1181 accept(reason.getConclusion());
1182 }
1183 setLocationWithinModule(context);
1184 visitor.visitLeave(reason);
1185 setLocationWithinModule(context);
1186 }
1187
1188 public void accept(final Hypothesis hypothesis) throws ModuleDataException {
1189 checkForInterrupt();
1190 if (blocked || hypothesis == null) {
1191 return;
1192 }
1193 final String context = getCurrentContext().getLocationWithinModule();
1194 visitor.visitEnter(hypothesis);
1195 if (hypothesis.getFormula() != null) {
1196 setLocationWithinModule(context + ".getFormula()");
1197 accept(hypothesis.getFormula());
1198 }
1199 setLocationWithinModule(context);
1200 visitor.visitLeave(hypothesis);
1201 setLocationWithinModule(context);
1202 }
1203
1204 public void accept(final Conclusion conclusion) throws ModuleDataException {
1205 checkForInterrupt();
1206 if (blocked || conclusion == null) {
1207 return;
1208 }
1209 final String context = getCurrentContext().getLocationWithinModule();
1210 visitor.visitEnter(conclusion);
1211 if (conclusion.getFormula() != null) {
1212 setLocationWithinModule(context + ".getFormula()");
1213 accept(conclusion.getFormula());
1214 }
1215 setLocationWithinModule(context);
1216 visitor.visitLeave(conclusion);
1217 setLocationWithinModule(context);
1218 }
1219
1220 public void accept(final Formula formula) throws ModuleDataException {
1221 checkForInterrupt();
1222 if (blocked || formula == null) {
1223 return;
1224 }
1225 final String context = getCurrentContext().getLocationWithinModule();
1226 visitor.visitEnter(formula);
1227 if (formula.getElement() != null) {
1228 setLocationWithinModule(context + ".getElement()");
1229 accept(formula.getElement());
1230 }
1231 setLocationWithinModule(context);
1232 visitor.visitLeave(formula);
1233 setLocationWithinModule(context);
1234 }
1235
1236 public void accept(final Term term) throws ModuleDataException {
1237 checkForInterrupt();
1238 if (blocked || term == null) {
1239 return;
1240 }
1241 final String context = getCurrentContext().getLocationWithinModule();
1242 visitor.visitEnter(term);
1243 if (term.getElement() != null) {
1244 setLocationWithinModule(context + ".getElement()");
1245 accept(term.getElement());
1246 }
1247 setLocationWithinModule(context);
1248 visitor.visitLeave(term);
1249 setLocationWithinModule(context);
1250 }
1251
1252 public void accept(final Element element) throws ModuleDataException {
1253 checkForInterrupt();
1254 if (blocked || element == null) {
1255 return;
1256 }
1257 final String context = getCurrentContext().getLocationWithinModule();
1258 if (element.isList()) {
1259 setLocationWithinModule(context + ".getList()");
1260 accept(element.getList());
1261 } else if (element.isAtom()) {
1262 setLocationWithinModule(context + ".getAtom()");
1263 accept(element.getAtom());
1264 } else {
1265 throw new IllegalArgumentException("unexpected element type: "
1266 + element.toString());
1267 }
1268 setLocationWithinModule(context);
1269 }
1270
1271 public void accept(final Atom atom) throws ModuleDataException {
1272 checkForInterrupt();
1273 if (blocked || atom == null) {
1274 return;
1275 }
1276 final String context = getCurrentContext().getLocationWithinModule();
1277 visitor.visitEnter(atom);
1278 setLocationWithinModule(context);
1279 visitor.visitLeave(atom);
1280 setLocationWithinModule(context);
1281 }
1282
1283 public void accept(final ElementList list) throws ModuleDataException {
1284 checkForInterrupt();
1285 if (blocked || list == null) {
1286 return;
1287 }
1288 final String context = getCurrentContext().getLocationWithinModule();
1289 visitor.visitEnter(list);
1290 for (int i = 0; i < list.size(); i++) {
1291 setLocationWithinModule(context + ".getElement(" + i + ")");
1292 accept(list.getElement(i));
1293 }
1294 setLocationWithinModule(context);
1295 visitor.visitLeave(list);
1296 setLocationWithinModule(context);
1297 }
1298
1299 public void accept(final LatexList latexList) throws ModuleDataException {
1300 checkForInterrupt();
1301 if (blocked || latexList == null) {
1302 return;
1303 }
1304 final String context = getCurrentContext().getLocationWithinModule();
1305 visitor.visitEnter(latexList);
1306 for (int i = 0; i < latexList.size(); i++) {
1307 setLocationWithinModule(context + ".get(" + i + ")");
1308 accept(latexList.get(i));
1309 }
1310 setLocationWithinModule(context);
1311 visitor.visitLeave(latexList);
1312 setLocationWithinModule(context);
1313 }
1314
1315 public void accept(final Latex latex) throws ModuleDataException {
1316 checkForInterrupt();
1317 if (blocked || latex == null) {
1318 return;
1319 }
1320 final String context = getCurrentContext().getLocationWithinModule();
1321 visitor.visitEnter(latex);
1322 setLocationWithinModule(context);
1323 visitor.visitLeave(latex);
1324 setLocationWithinModule(context);
1325 }
1326
1327 /**
1328 * Get node that is currently parsed. Might be <code>null</code>.
1329 *
1330 * @return QEDEQ node were are currently in.
1331 */
1332 public Node getNode() {
1333 return node;
1334 }
1335
1336 /**
1337 * Set location information where are we within the original module.
1338 *
1339 * @param locationWithinModule Location within module.
1340 */
1341 public void setLocationWithinModule(final String locationWithinModule) {
1342 getCurrentContext().setLocationWithinModule(locationWithinModule);
1343 }
1344
1345 /**
1346 * Get current context within original. Remember to use the copy constructor
1347 * when trying to remember this context!
1348 *
1349 * @return Current context.
1350 */
1351 public final ModuleContext getCurrentContext() {
1352 return currentContext;
1353 }
1354
1355 /**
1356 * Is further traversing blocked?
1357 *
1358 * @return Is further traversing blocked?
1359 */
1360 public final boolean getBlocked() {
1361 return blocked;
1362 }
1363
1364 /**
1365 * Set if further traverse is blocked.
1366 *
1367 * @param blocked Further transversion?
1368 */
1369 public final void setBlocked(final boolean blocked) {
1370 this.blocked = blocked;
1371 }
1372
1373 /**
1374 * Get calculated visit percentage.
1375 *
1376 * @return Value between 0 and 100.
1377 */
1378 public double getVisitPercentage() {
1379 if (data == null) {
1380 return 0;
1381 }
1382 return data.getVisitPercentage();
1383 }
1384
1385 /**
1386 * Set absolute location description.
1387 *
1388 * @param text Description.
1389 */
1390 private void setLocation(final String text) {
1391 location.setSize(0);
1392 location.push(text);
1393 }
1394 /**
1395 * Get readable description of current location.
1396 *
1397 * @return Description.
1398 */
1399 public String getLocationDescription() {
1400 final StringBuffer buffer = new StringBuffer();
1401 for (int i = 0; i < location.size(); i++) {
1402 if (i > 0) {
1403 buffer.append(" / ");
1404 }
1405 buffer.append(location.get(i));
1406 }
1407 return buffer.toString();
1408 }
1409
1410 /**
1411 * Get copy of current counters.
1412 *
1413 * @return Values of various counters.
1414 */
1415 public QedeqNumbers getCurrentNumbers() {
1416 return new QedeqNumbers(data);
1417 }
1418
1419 /**
1420 * Get current (QEDEQ module local) rule version for given rule name.
1421 *
1422 * @param name Rule name
1423 * @return Current (local) rule version. Might be <code>null</code>.
1424 */
1425 public RuleKey getLocalRuleKey(final String name) {
1426 return (RuleKey) ruleExistence.get(name);
1427 }
1428
1429 }
|