0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, 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.xml.mapper;
0017
0018 import java.util.ArrayList;
0019 import java.util.HashMap;
0020 import java.util.List;
0021 import java.util.Map;
0022
0023 import org.qedeq.base.trace.Trace;
0024 import org.qedeq.base.utility.Enumerator;
0025 import org.qedeq.kernel.se.base.list.ElementList;
0026 import org.qedeq.kernel.se.base.module.Add;
0027 import org.qedeq.kernel.se.base.module.Author;
0028 import org.qedeq.kernel.se.base.module.AuthorList;
0029 import org.qedeq.kernel.se.base.module.Axiom;
0030 import org.qedeq.kernel.se.base.module.ChangedRule;
0031 import org.qedeq.kernel.se.base.module.ChangedRuleList;
0032 import org.qedeq.kernel.se.base.module.Chapter;
0033 import org.qedeq.kernel.se.base.module.ChapterList;
0034 import org.qedeq.kernel.se.base.module.Conclusion;
0035 import org.qedeq.kernel.se.base.module.ConditionalProof;
0036 import org.qedeq.kernel.se.base.module.Existential;
0037 import org.qedeq.kernel.se.base.module.FormalProof;
0038 import org.qedeq.kernel.se.base.module.FormalProofLine;
0039 import org.qedeq.kernel.se.base.module.FormalProofLineList;
0040 import org.qedeq.kernel.se.base.module.FormalProofList;
0041 import org.qedeq.kernel.se.base.module.Formula;
0042 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0043 import org.qedeq.kernel.se.base.module.Header;
0044 import org.qedeq.kernel.se.base.module.Hypothesis;
0045 import org.qedeq.kernel.se.base.module.Import;
0046 import org.qedeq.kernel.se.base.module.ImportList;
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.common.ModuleContext;
0077 import org.qedeq.kernel.se.common.ModuleDataException;
0078 import org.qedeq.kernel.se.visitor.AbstractModuleVisitor;
0079 import org.qedeq.kernel.se.visitor.QedeqNotNullTraverser;
0080 import org.qedeq.kernel.xml.tracker.SimpleXPath;
0081
0082
0083 /**
0084 * Map content string to SimpleXPath string. This class makes it possible to transfer an location
0085 * of an {@link org.qedeq.kernel.se.base.module.Qedeq} object into an XPath like position description
0086 * for an XML file representation of that object.
0087 *
0088 * <p>
0089 * See {@link #getXPath(ModuleContext, Qedeq)} for further details.
0090 *
0091 * <p>
0092 * TODO mime 20070217: It seems to work this way but: this class assumes that we can find
0093 * QEDEQ/CHAPTER[2]/SECTION[4]/SUBSECTIONS/SUBSECTION[2]
0094 * even if we have some ../NODE s inbetween.
0095 * (Example: NODE, NODE, SUBSECTION, NODE, SUBSECTION, NODE..)
0096 *
0097 * Is this still a correct XPath? (Old solution was usage of "*")
0098 * Seems ok for official XPath specification, but does it work for our SimpleXPathFinder?
0099 *
0100 * @author Michael Meyling
0101 */
0102 public final class Context2SimpleXPath extends AbstractModuleVisitor {
0103
0104 /** This class. */
0105 private static final Class CLASS = Context2SimpleXPath.class;
0106
0107 /** Traverse QEDEQ module with this traverser. */
0108 private QedeqNotNullTraverser traverser;
0109
0110 /** QEDEQ object to work on. */
0111 private Qedeq qedeq;
0112
0113 /** Search for this context. */
0114 private final ModuleContext find;
0115
0116 /** We are currently at this position. */
0117 private SimpleXPath current;
0118
0119 /** Element stack. */
0120 private final List elements;
0121
0122 /** Current stack level. */
0123 private int level;
0124
0125 /** Is the current context already matching the beginning of the search context? */
0126 private boolean matching;
0127
0128 /** Last matching begin of search context. See {@link #matching}. */
0129 private String matchingBegin;
0130
0131 /** Corresponding XPath for the {@link #matchingBegin}. */
0132 private SimpleXPath matchingPath;
0133
0134 /**
0135 * Constructor.
0136 *
0137 * @param find Find this location.
0138 * @param qedeq Within this QEDEQ object.
0139 */
0140 private Context2SimpleXPath(final ModuleContext find, final Qedeq qedeq) {
0141 this.qedeq = qedeq;
0142 traverser = new QedeqNotNullTraverser(find.getModuleLocation(), this);
0143 this.find = find;
0144 elements = new ArrayList(20);
0145 }
0146
0147 /**
0148 * This method finds a {@link ModuleContext} something like<br>
0149 * <code>
0150 * getChapterList().get(4).getSectionList().get(0).getSubsectionList().get(4).getLatex().get(0)
0151 * </code><br>
0152 * within a {@link Qedeq} module and returns a kind of XPath location for an associated
0153 * XML document:<br>
0154 * <code>QEDEQ/CHAPTER[5]/SECTION/SUBSECTIONS/SUBSECTION[2]/TEXT/LATEX</code>
0155 *
0156 * <p>
0157 * At this example one can already see that <code>getSubsectionList().get(4)</code> is
0158 * transformed into <code>SUBSECTIONS/SUBSECTION[2]</code>. This is due to the fact that
0159 * <code>SUBSECTION</code> contains a sequence of <code>SUBSECTION</code> or <code>NODE</code>
0160 * elements. The transformation depends not only from the context but also from
0161 * the concrete QEDEQ module.
0162 *
0163 * <p>
0164 * Especially the transformation of formula location information in their XML counterpart
0165 * demands parsing the whole formula.
0166 *
0167 * @param find Find this location.
0168 * @param qedeq Within this QEDEQ object.
0169 * @return XPath for this location in the XML document.
0170 * @throws ModuleDataException Problem with module data.
0171 */
0172 public static SimpleXPath getXPath(final ModuleContext find, final Qedeq qedeq)
0173 throws ModuleDataException {
0174 final Context2SimpleXPath converter = new Context2SimpleXPath(find, qedeq);
0175 return converter.find();
0176 }
0177
0178 private final SimpleXPath find() throws ModuleDataException {
0179 final String method = "find()";
0180 Trace.paramInfo(CLASS, this, method, "find", find);
0181 elements.clear();
0182 level = 0;
0183 current = new SimpleXPath();
0184 try {
0185 traverser.accept(qedeq);
0186 } catch (LocationFoundException e) {
0187 Trace.paramInfo(CLASS, this, method, "location found", current);
0188 return current;
0189 }
0190 Trace.param(CLASS, this, method, "level", level); // level should be equal to zero now
0191 Trace.info(CLASS, this, method, "location was not found");
0192 throw new LocationNotFoundException(traverser.getCurrentContext(), "",
0193 find.getLocationWithinModule());
0194 }
0195
0196 public final void visitEnter(final Qedeq qedeq) throws ModuleDataException {
0197 enter("QEDEQ");
0198 final String method = "visitEnter(Qedeq)";
0199 Trace.param(CLASS, this, method, "current", current);
0200 checkMatching(method);
0201 }
0202
0203 public final void visitLeave(final Qedeq qedeq) {
0204 leave();
0205 }
0206
0207 public final void visitEnter(final Header header) throws ModuleDataException {
0208 enter("HEADER");
0209 final String method = "visitEnter(Header)";
0210 Trace.param(CLASS, this, method, "current", current);
0211 final String context = traverser.getCurrentContext().getLocationWithinModule();
0212 checkMatching(method);
0213
0214 traverser.setLocationWithinModule(context + ".getEmail()");
0215 current.setAttribute("email");
0216 checkIfFound();
0217 }
0218
0219 public final void visitLeave(final Header header) {
0220 leave();
0221 }
0222
0223 public final void visitEnter(final Specification specification) throws ModuleDataException {
0224 enter("SPECIFICATION");
0225 final String method = "visitEnter(Specification)";
0226 Trace.param(CLASS, this, method, "current", current);
0227 final String context = traverser.getCurrentContext().getLocationWithinModule();
0228 checkMatching(method);
0229
0230 traverser.setLocationWithinModule(context + ".getName()");
0231 current.setAttribute("name");
0232 checkIfFound();
0233
0234 traverser.setLocationWithinModule(context + ".getRuleVersion()");
0235 current.setAttribute("ruleVersion");
0236 checkIfFound();
0237 }
0238
0239 public final void visitLeave(final Specification specification) {
0240 leave();
0241 }
0242
0243 public final void visitEnter(final LatexList latexList) throws ModuleDataException {
0244 final String method = "visitEnter(LatexList)";
0245 final String context = traverser.getCurrentContext().getLocationWithinModule();
0246 final String name;
0247 if (context.endsWith(".getTitle()")) {
0248 name = "TITLE";
0249 } else if (context.endsWith(".getSummary()")) {
0250 name = "ABSTRACT";
0251 } else if (context.endsWith(".getIntroduction()")) {
0252 name = "INTRODUCTION";
0253 } else if (context.endsWith(".getName()")) {
0254 name = "NAME";
0255 } else if (context.endsWith(".getPrecedingText()")) {
0256 name = "PRECEDING";
0257 } else if (context.endsWith(".getSucceedingText()")) {
0258 name = "SUCCEEDING";
0259 } else if (context.endsWith(".getLatex()")) {
0260 name = "TEXT";
0261 } else if (context.endsWith(".getDescription()")) {
0262 if (context.indexOf(".getChangedRuleList().get(") >= 0) {
0263 name = null;
0264 } else {
0265 name = "DESCRIPTION";
0266 }
0267 } else if (context.endsWith(".getNonFormalProof()")) { // no extra XSD element
0268 name = null;
0269 } else if (context.endsWith(".getItem()")) { // no extra XSD element
0270 name = null;
0271 } else { // programming error
0272 throw new IllegalArgumentException("unknown LatexList " + context);
0273 }
0274 Trace.param(CLASS, this, method, "name", name);
0275 if (name != null) {
0276 enter(name);
0277 }
0278 Trace.param(CLASS, this, method, "current", current);
0279
0280 checkMatching(method);
0281 }
0282
0283 public final void visitLeave(final LatexList latexList) {
0284 final String context = traverser.getCurrentContext().getLocationWithinModule();
0285 if (!context.endsWith(".getNonFormalProof()") // no extra XSD element
0286 && !context.endsWith(".getItem()") && !(context.endsWith(".getDescription()")
0287 && context.indexOf(".getChangedRuleList().get(") >= 0)) {
0288 leave();
0289 }
0290 }
0291
0292 public final void visitEnter(final Latex latex) throws ModuleDataException {
0293 final String context = traverser.getCurrentContext().getLocationWithinModule();
0294 if (context.indexOf(".getAuthorList().get(") >= 0) { // TODO mime 20070216: why is the
0295 enter("NAME"); // XSD so cruel???
0296 }
0297 enter("LATEX");
0298 final String method = "visitEnter(Latex)";
0299 Trace.param(CLASS, this, method, "current", current);
0300 checkMatching(method);
0301
0302 traverser.setLocationWithinModule(context + ".getLanguage()");
0303 current.setAttribute("language");
0304 checkIfFound();
0305
0306 traverser.setLocationWithinModule(context + ".getLatex()");
0307 current.setAttribute(null); // element character data of LATEX is LaTeX content
0308 checkIfFound();
0309 }
0310
0311 public final void visitLeave(final Latex latex) {
0312 // because NAME of AUTHOR/NAME/LATEX has no equivalent in interfaces:
0313 final String context = traverser.getCurrentContext().getLocationWithinModule();
0314 if (context.indexOf(".getAuthorList().get(") >= 0) {
0315 leave();
0316 }
0317 leave();
0318 }
0319
0320 public final void visitEnter(final LocationList locationList) throws ModuleDataException {
0321 enter("LOCATIONS");
0322 final String method = "visitEnter(LocationList)";
0323 Trace.param(CLASS, this, method, "current", current);
0324 checkMatching(method);
0325
0326 }
0327
0328 public final void visitLeave(final LocationList locationList) {
0329 leave();
0330 }
0331
0332 public final void visitEnter(final Location location) throws ModuleDataException {
0333 enter("LOCATION");
0334 final String method = "visitEnter(Location)";
0335 Trace.param(CLASS, this, method, "current", current);
0336 final String context = traverser.getCurrentContext().getLocationWithinModule();
0337 checkMatching(method);
0338
0339 traverser.setLocationWithinModule(context + ".getLocation()");
0340 current.setAttribute("value");
0341 checkIfFound();
0342 }
0343
0344 public final void visitLeave(final Location location) {
0345 leave();
0346 }
0347
0348 public final void visitEnter(final AuthorList authorList) throws ModuleDataException {
0349 enter("AUTHORS");
0350 final String method = "visitEnter(AuthorList)";
0351 Trace.param(CLASS, this, method, "current", current);
0352 checkMatching(method);
0353 }
0354
0355 public final void visitLeave(final AuthorList authorList) {
0356 leave();
0357 }
0358
0359 public final void visitEnter(final Author author) throws ModuleDataException {
0360 enter("AUTHOR");
0361 final String method = "visitEnter(Author)";
0362 Trace.param(CLASS, this, method, "current", current);
0363 final String context = traverser.getCurrentContext().getLocationWithinModule();
0364 checkMatching(method);
0365
0366 traverser.setLocationWithinModule(context + ".getEmail()");
0367 current.setAttribute("email");
0368 checkIfFound();
0369 }
0370
0371 public final void visitLeave(final Author author) {
0372 leave();
0373 }
0374
0375 public final void visitEnter(final ImportList importList) throws ModuleDataException {
0376 enter("IMPORTS");
0377 final String method = "visitEnter(ImportList)";
0378 Trace.param(CLASS, this, method, "current", current);
0379 checkMatching(method);
0380 }
0381
0382 public final void visitLeave(final ImportList importList) {
0383 leave();
0384 }
0385
0386 public final void visitEnter(final Import imp) throws ModuleDataException {
0387 enter("IMPORT");
0388 final String method = "visitEnter(Import)";
0389 Trace.param(CLASS, this, method, "current", current);
0390 final String context = traverser.getCurrentContext().getLocationWithinModule();
0391 checkMatching(method);
0392
0393 traverser.setLocationWithinModule(context + ".getLabel()");
0394 current.setAttribute("label");
0395 checkIfFound();
0396 }
0397
0398 public final void visitLeave(final Import imp) {
0399 leave();
0400 }
0401
0402 public final void visitEnter(final UsedByList usedByList) throws ModuleDataException {
0403 enter("USEDBY");
0404 final String method = "visitEnter(UsedByList)";
0405 Trace.param(CLASS, this, method, "current", current);
0406 checkMatching(method);
0407 }
0408
0409 public final void visitLeave(final UsedByList usedByList) {
0410 leave();
0411 }
0412
0413 public final void visitEnter(final ChapterList chapterList) throws ModuleDataException {
0414 final String method = "visitEnter(ChapterList)";
0415 // because no equivalent level of "getChapterList()" exists in the XSD we simply
0416 // point to the current location that must be "QEDEQ"
0417 checkMatching(method);
0418 }
0419
0420 public final void visitLeave(final ChapterList chapterList) {
0421 traverser.setBlocked(false); // free sub node search
0422 }
0423
0424 public final void visitEnter(final Chapter chapter) throws ModuleDataException {
0425 enter("CHAPTER");
0426 final String method = "visitEnter(Chapter)";
0427 Trace.param(CLASS, this, method, "current", current);
0428 final String context = traverser.getCurrentContext().getLocationWithinModule();
0429 checkMatching(method);
0430
0431 traverser.setLocationWithinModule(context + ".getNoNumber()");
0432 current.setAttribute("noNumber");
0433 checkIfFound();
0434 }
0435
0436 public final void visitLeave(final Chapter chapter) {
0437 leave();
0438 }
0439
0440 public final void visitEnter(final SectionList sectionList) throws ModuleDataException {
0441 final String method = "visitEnter(SectionList)";
0442 // because no equivalent level of "getSectionList()" exists in the XSD we simply
0443 // point to the current location that must be "QEDEQ/CHAPTER[x]"
0444 checkMatching(method);
0445 }
0446
0447 public final void visitLeave(final SectionList sectionList) {
0448 traverser.setBlocked(false); // free node search again
0449 }
0450
0451 public final void visitEnter(final Section section) throws ModuleDataException {
0452 enter("SECTION");
0453 final String method = "visitEnter(Section)";
0454 Trace.param(CLASS, this, method, "current", current);
0455 final String context = traverser.getCurrentContext().getLocationWithinModule();
0456 checkMatching(method);
0457
0458 traverser.setLocationWithinModule(context + ".getNoNumber()");
0459 current.setAttribute("noNumber");
0460 checkIfFound();
0461 }
0462
0463 public final void visitLeave(final Section section) {
0464 leave();
0465 }
0466
0467 public final void visitEnter(final SubsectionList subsectionList) throws ModuleDataException {
0468 enter("SUBSECTIONS");
0469 final String method = "visitEnter(SubsectionList)";
0470 Trace.param(CLASS, this, method, "current", current);
0471 checkMatching(method);
0472 }
0473
0474 public final void visitLeave(final SubsectionList subsectionList) {
0475 leave();
0476 }
0477
0478 public final void visitEnter(final Subsection subsection) throws ModuleDataException {
0479 enter("SUBSECTION");
0480 final String method = "visitEnter(Subsection)";
0481 Trace.param(CLASS, this, method, "current", current);
0482 final String context = traverser.getCurrentContext().getLocationWithinModule();
0483 checkMatching(method);
0484
0485 traverser.setLocationWithinModule(context + ".getId()");
0486 current.setAttribute("id");
0487 checkIfFound();
0488
0489 traverser.setLocationWithinModule(context + ".getLevel()");
0490 current.setAttribute("level");
0491 checkIfFound();
0492 }
0493
0494 public final void visitLeave(final Subsection subsection) {
0495 leave();
0496 }
0497
0498 public final void visitEnter(final Node node) throws ModuleDataException {
0499 enter("NODE");
0500 final String method = "visitEnter(Node)";
0501 Trace.param(CLASS, this, method, "current", current);
0502 final String context = traverser.getCurrentContext().getLocationWithinModule();
0503 checkMatching(method);
0504
0505 traverser.setLocationWithinModule(context + ".getId()");
0506 current.setAttribute("id");
0507 checkIfFound();
0508
0509 traverser.setLocationWithinModule(context + ".getLevel()");
0510 current.setAttribute("level");
0511 checkIfFound();
0512
0513 // we dont't differentiate the different node types here and point to the parent element
0514 traverser.setLocationWithinModule(context + ".getNodeType()");
0515 current.setAttribute(null);
0516 checkIfFound();
0517
0518 }
0519
0520 public final void visitLeave(final Node node) {
0521 leave();
0522 }
0523
0524 public final void visitEnter(final Axiom axiom) throws ModuleDataException {
0525 enter("AXIOM");
0526 final String method = "visitEnter(Axiom)";
0527 Trace.param(CLASS, this, method, "current", current);
0528 final String context = traverser.getCurrentContext().getLocationWithinModule();
0529 checkMatching(method);
0530
0531 traverser.setLocationWithinModule(context + ".getDefinedOperator()");
0532 current.setAttribute("definedOperator");
0533 checkIfFound();
0534 }
0535
0536 public final void visitLeave(final Axiom axiom) {
0537 leave();
0538 }
0539
0540 public final void visitEnter(final Proposition proposition) throws ModuleDataException {
0541 enter("THEOREM");
0542 final String method = "visitEnter(Proposition)";
0543 Trace.param(CLASS, this, method, "current", current);
0544 checkMatching(method);
0545 }
0546
0547 public final void visitLeave(final Proposition proposition) {
0548 leave();
0549 }
0550
0551 public final void visitEnter(final ProofList proofList) throws ModuleDataException {
0552 final String method = "visitEnter(ProofList)";
0553 // because no equivalent level of "getProofList()" exists in the XSD we simply
0554 // point to the current location that must be within the element "THEOREM" or "RULE"
0555 checkMatching(method);
0556 }
0557
0558 public final void visitEnter(final Proof proof) throws ModuleDataException {
0559 enter("PROOF");
0560 final String method = "visitEnter(Proof)";
0561 Trace.param(CLASS, this, method, "current", current);
0562 final String context = traverser.getCurrentContext().getLocationWithinModule();
0563 checkMatching(method);
0564
0565 traverser.setLocationWithinModule(context + ".getKind()");
0566 current.setAttribute("kind");
0567 checkIfFound();
0568
0569 traverser.setLocationWithinModule(context + ".getLevel()");
0570 current.setAttribute("level");
0571 checkIfFound();
0572 }
0573
0574 public final void visitLeave(final Proof proof) {
0575 leave();
0576 }
0577
0578 public final void visitEnter(final FormalProofList proofList) throws ModuleDataException {
0579 final String method = "visitEnter(FormalProofList)";
0580 // because no equivalent level of "getProofList()" exists in the XSD we simply
0581 // point to the current location that must be within the element "THEOREM"
0582 checkMatching(method);
0583 }
0584
0585 public final void visitEnter(final FormalProof proof) throws ModuleDataException {
0586 enter("FORMAL_PROOF");
0587 final String method = "visitEnter(FormalProof)";
0588 Trace.param(CLASS, this, method, "current", current);
0589 checkMatching(method);
0590 }
0591
0592 public final void visitLeave(final FormalProof proof) {
0593 leave();
0594 }
0595
0596 public final void visitEnter(final FormalProofLineList list) throws ModuleDataException {
0597 enter("LINES");
0598 final String method = "visitEnter(FormalProofLineList)";
0599 Trace.param(CLASS, this, method, "current", current);
0600 checkMatching(method);
0601 }
0602
0603 public final void visitLeave(final FormalProofLineList list) {
0604 leave();
0605 }
0606
0607 public final void visitEnter(final FormalProofLine line) throws ModuleDataException {
0608 enter("L");
0609 final String method = "visitEnter(FormalProofLine)";
0610 Trace.param(CLASS, this, method, "current", current);
0611 final String context = traverser.getCurrentContext().getLocationWithinModule();
0612 checkMatching(method);
0613
0614 traverser.setLocationWithinModule(context + ".getLabel()");
0615 current.setAttribute("label");
0616 checkIfFound();
0617 }
0618
0619 public final void visitLeave(final FormalProofLine line) {
0620 leave();
0621 }
0622
0623 public final void visitEnter(final ConditionalProof reason) throws ModuleDataException {
0624 enter("CP");
0625 final String method = "visitEnter(ConditionalProof)";
0626 Trace.param(CLASS, this, method, "current", current);
0627 checkMatching(method);
0628 }
0629
0630 public final void visitLeave(final ConditionalProof reason) {
0631 leave();
0632 }
0633
0634 public final void visitEnter(final Reason reason) throws ModuleDataException {
0635 // nothing to enter in XML
0636 final String method = "visitEnter(Reason)";
0637 Trace.param(CLASS, this, method, "current", current);
0638 checkMatching(method);
0639
0640 }
0641
0642 public final void visitLeave(final Reason reason) {
0643 // nothing to leave in XML
0644 }
0645
0646 public final void visitEnter(final Add reason) throws ModuleDataException {
0647 enter("ADD");
0648 final String method = "visitEnter(Add)";
0649 Trace.param(CLASS, this, method, "current", current);
0650 final String context = traverser.getCurrentContext().getLocationWithinModule();
0651 checkMatching(method);
0652
0653 traverser.setLocationWithinModule(context + ".getReference()");
0654 current.setAttribute("ref");
0655 checkIfFound();
0656 }
0657
0658 public final void visitLeave(final Add reason) {
0659 leave();
0660 }
0661
0662 public final void visitEnter(final ModusPonens reason) throws ModuleDataException {
0663 enter("MP");
0664 final String method = "visitEnter(ModusPonens)";
0665 Trace.param(CLASS, this, method, "current", current);
0666 final String context = traverser.getCurrentContext().getLocationWithinModule();
0667 checkMatching(method);
0668
0669 traverser.setLocationWithinModule(context + ".getReference1()");
0670 current.setAttribute("ref1");
0671 checkIfFound();
0672
0673 traverser.setLocationWithinModule(context + ".getReference2()");
0674 current.setAttribute("ref2");
0675 checkIfFound();
0676 }
0677
0678 public final void visitLeave(final ModusPonens reason) {
0679 leave();
0680 }
0681
0682 public final void visitEnter(final Rename reason) throws ModuleDataException {
0683 enter("RENAME");
0684 final String method = "visitEnter(Add)";
0685 Trace.param(CLASS, this, method, "current", current);
0686 final String context = traverser.getCurrentContext().getLocationWithinModule();
0687 checkMatching(method);
0688
0689 traverser.setLocationWithinModule(context + ".getReference()");
0690 current.setAttribute("ref");
0691 checkIfFound();
0692
0693 traverser.setLocationWithinModule(context + ".getOccurrence()");
0694 current.setAttribute("occurrence");
0695 checkIfFound();
0696 }
0697
0698 public final void visitLeave(final Rename reason) {
0699 leave();
0700 }
0701
0702 public final void visitEnter(final SubstFree reason) throws ModuleDataException {
0703 enter("SUBST_FREE");
0704 final String method = "visitEnter(SubstFree)";
0705 Trace.param(CLASS, this, method, "current", current);
0706 final String context = traverser.getCurrentContext().getLocationWithinModule();
0707 checkMatching(method);
0708
0709 traverser.setLocationWithinModule(context + ".getReference()");
0710 current.setAttribute("ref");
0711 checkIfFound();
0712 }
0713
0714 public final void visitLeave(final SubstFree reason) {
0715 leave();
0716 }
0717
0718 public final void visitEnter(final SubstFunc reason) throws ModuleDataException {
0719 enter("SUBST_FUNVAR");
0720 final String method = "visitEnter(SubstFunc)";
0721 Trace.param(CLASS, this, method, "current", current);
0722 final String context = traverser.getCurrentContext().getLocationWithinModule();
0723 checkMatching(method);
0724
0725 traverser.setLocationWithinModule(context + ".getReference()");
0726 current.setAttribute("ref");
0727 checkIfFound();
0728 }
0729
0730 public final void visitLeave(final SubstFunc reason) {
0731 leave();
0732 }
0733
0734 public final void visitEnter(final SubstPred reason) throws ModuleDataException {
0735 enter("SUBST_PREDVAR");
0736 final String method = "visitEnter(SubstPred)";
0737 Trace.param(CLASS, this, method, "current", current);
0738 final String context = traverser.getCurrentContext().getLocationWithinModule();
0739 checkMatching(method);
0740
0741 traverser.setLocationWithinModule(context + ".getReference()");
0742 current.setAttribute("ref");
0743 checkIfFound();
0744 }
0745
0746 public final void visitLeave(final SubstPred reason) {
0747 leave();
0748 }
0749
0750 public final void visitEnter(final Existential reason) throws ModuleDataException {
0751 enter("EXISTENTIAL");
0752 final String method = "visitEnter(Existential)";
0753 Trace.param(CLASS, this, method, "current", current);
0754 final String context = traverser.getCurrentContext().getLocationWithinModule();
0755 checkMatching(method);
0756
0757 traverser.setLocationWithinModule(context + ".getReference()");
0758 current.setAttribute("ref");
0759 checkIfFound();
0760 }
0761
0762 public final void visitLeave(final Existential reason) {
0763 leave();
0764 }
0765
0766 public final void visitEnter(final Universal reason) throws ModuleDataException {
0767 enter("UNIVERSAL");
0768 final String method = "visitEnter(Universal)";
0769 Trace.param(CLASS, this, method, "current", current);
0770 final String context = traverser.getCurrentContext().getLocationWithinModule();
0771 checkMatching(method);
0772
0773 traverser.setLocationWithinModule(context + ".getReference()");
0774 current.setAttribute("ref");
0775 checkIfFound();
0776 }
0777
0778 public final void visitLeave(final Universal reason) {
0779 leave();
0780 }
0781
0782 public final void visitEnter(final Hypothesis hypothesis) throws ModuleDataException {
0783 enter("HYPOTHESIS");
0784 final String method = "visitEnter(Hypothesis)";
0785 Trace.param(CLASS, this, method, "current", current);
0786 final String context = traverser.getCurrentContext().getLocationWithinModule();
0787 checkMatching(method);
0788
0789 traverser.setLocationWithinModule(context + ".getLabel()");
0790 current.setAttribute("label");
0791 checkIfFound();
0792 }
0793
0794 public final void visitLeave(final Hypothesis hypothesis) {
0795 leave();
0796 }
0797
0798 public final void visitEnter(final Conclusion conclusion) throws ModuleDataException {
0799 enter("CONCLUSION");
0800 final String method = "visitEnter(Conclusion)";
0801 Trace.param(CLASS, this, method, "current", current);
0802 final String context = traverser.getCurrentContext().getLocationWithinModule();
0803 checkMatching(method);
0804
0805 traverser.setLocationWithinModule(context + ".getLabel()");
0806 current.setAttribute("label");
0807 checkIfFound();
0808 }
0809
0810 public final void visitLeave(final Conclusion conclusion) {
0811 leave();
0812 }
0813
0814 public final void visitEnter(final InitialPredicateDefinition definition) throws ModuleDataException {
0815 enter("DEFINITION_PREDICATE_INITIAL");
0816 final String method = "visitEnter(InitialPredicateDefinition)";
0817 Trace.param(CLASS, this, method, "current", current);
0818 final String context = traverser.getCurrentContext().getLocationWithinModule();
0819 checkMatching(method);
0820
0821 traverser.setLocationWithinModule(context + ".getArgumentNumber()");
0822 current.setAttribute("arguments");
0823 checkIfFound();
0824
0825 traverser.setLocationWithinModule(context + ".getName()");
0826 current.setAttribute("name");
0827 checkIfFound();
0828
0829 traverser.setLocationWithinModule(context + ".getLatexPattern()");
0830 enter("LATEXPATTERN");
0831 if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
0832 .getLocationWithinModule())) {
0833 if (definition.getLatexPattern() == null) { // NOT FOUND
0834 leave();
0835 }
0836 throw new LocationFoundException(traverser.getCurrentContext());
0837 }
0838 leave();
0839 }
0840
0841 public final void visitLeave(final InitialPredicateDefinition definition) {
0842 leave();
0843 }
0844
0845 public final void visitEnter(final PredicateDefinition definition) throws ModuleDataException {
0846 enter("DEFINITION_PREDICATE");
0847 final String method = "visitEnter(PredicateDefinition)";
0848 Trace.param(CLASS, this, method, "current", current);
0849 final String context = traverser.getCurrentContext().getLocationWithinModule();
0850 checkMatching(method);
0851
0852 traverser.setLocationWithinModule(context + ".getArgumentNumber()");
0853 current.setAttribute("arguments");
0854 checkIfFound();
0855
0856 traverser.setLocationWithinModule(context + ".getName()");
0857 current.setAttribute("name");
0858 checkIfFound();
0859
0860 traverser.setLocationWithinModule(context + ".getLatexPattern()");
0861 enter("LATEXPATTERN");
0862 if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
0863 .getLocationWithinModule())) {
0864 if (definition.getLatexPattern() == null) { // NOT FOUND
0865 leave();
0866 }
0867 throw new LocationFoundException(traverser.getCurrentContext());
0868 }
0869 leave();
0870 }
0871
0872 public final void visitLeave(final PredicateDefinition definition) {
0873 leave();
0874 }
0875
0876 public final void visitEnter(final FunctionDefinition definition) throws ModuleDataException {
0877 enter("DEFINITION_FUNCTION");
0878 final String method = "visitEnter(FunctionDefinition)";
0879 Trace.param(CLASS, this, method, "current", current);
0880 final String context = traverser.getCurrentContext().getLocationWithinModule();
0881 checkMatching(method);
0882
0883 traverser.setLocationWithinModule(context + ".getArgumentNumber()");
0884 current.setAttribute("arguments");
0885 checkIfFound();
0886
0887 traverser.setLocationWithinModule(context + ".getName()");
0888 current.setAttribute("name");
0889 checkIfFound();
0890
0891 traverser.setLocationWithinModule(context + ".getLatexPattern()");
0892 enter("LATEXPATTERN");
0893 if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
0894 .getLocationWithinModule())) {
0895 if (definition.getLatexPattern() == null) { // NOT FOUND
0896 leave();
0897 }
0898 throw new LocationFoundException(traverser.getCurrentContext());
0899 }
0900 leave();
0901 }
0902
0903 public final void visitLeave(final FunctionDefinition definition) {
0904 leave();
0905 }
0906
0907 public final void visitEnter(final Rule rule) throws ModuleDataException {
0908 enter("RULE");
0909 final String method = "visitEnter(Rule)";
0910 Trace.param(CLASS, this, method, "current", current);
0911 final String context = traverser.getCurrentContext().getLocationWithinModule();
0912 checkMatching(method);
0913
0914 traverser.setLocationWithinModule(context + ".getName()");
0915 current.setAttribute("name");
0916 checkIfFound();
0917
0918 traverser.setLocationWithinModule(context + ".getVersion()");
0919 current.setAttribute("version");
0920 checkIfFound();
0921 }
0922
0923 public final void visitLeave(final Rule rule) {
0924 leave();
0925 }
0926
0927 public final void visitEnter(final ChangedRuleList list) throws ModuleDataException {
0928 final String method = "visitEnter(ChangedRuleList)";
0929 // because no equivalent level of "getChangedRuleList()" exists in the XSD we simply
0930 // point to the current location that must be within the element "RULE"
0931 checkMatching(method);
0932 }
0933
0934 public final void visitLeave(final ChangedRuleList list) {
0935 traverser.setBlocked(false); // free node search again
0936 }
0937
0938 public final void visitEnter(final ChangedRule rule) throws ModuleDataException {
0939 enter("CHANGED_RULE");
0940 final String method = "visitEnter(ChangedRule)";
0941 Trace.param(CLASS, this, method, "current", current);
0942 final String context = traverser.getCurrentContext().getLocationWithinModule();
0943 checkMatching(method);
0944
0945 traverser.setLocationWithinModule(context + ".getName()");
0946 current.setAttribute("name");
0947 checkIfFound();
0948
0949 traverser.setLocationWithinModule(context + ".getVersion()");
0950 current.setAttribute("version");
0951 checkIfFound();
0952 }
0953
0954 public final void visitLeave(final ChangedRule rule) {
0955 leave();
0956 }
0957
0958 public final void visitEnter(final LinkList linkList) throws ModuleDataException {
0959 final String method = "visitEnter(LinkList)";
0960 Trace.param(CLASS, this, method, "current", current);
0961 final String context = traverser.getCurrentContext().getLocationWithinModule();
0962 checkMatching(method);
0963
0964 for (int i = 0; i < linkList.size(); i++) {
0965 enter("LINK");
0966 if (linkList.get(i) != null) {
0967 traverser.setLocationWithinModule(context + ".get(" + i + ")");
0968 current.setAttribute("id");
0969 checkIfFound();
0970 }
0971 leave();
0972 };
0973 }
0974
0975 public final void visitLeave(final LinkList linkList) {
0976 // nothing to do
0977 }
0978
0979 public final void visitEnter(final Formula formula) throws ModuleDataException {
0980 enter("FORMULA");
0981 final String method = "visitEnter(Formula)";
0982 Trace.param(CLASS, this, method, "current", current);
0983 checkMatching(method);
0984 }
0985
0986 public final void visitLeave(final Formula formula) {
0987 leave();
0988 }
0989
0990 public final void visitEnter(final Term term) throws ModuleDataException {
0991 enter("TERM");
0992 final String method = "visitEnter(Term)";
0993 Trace.param(CLASS, this, method, "current", current);
0994 checkMatching(method);
0995 }
0996
0997 public final void visitLeave(final Term term) {
0998 leave();
0999 }
1000
1001 public final void visitEnter(final ElementList list) throws ModuleDataException {
1002 final String operator = list.getOperator();
1003 enter(operator);
1004 final String method = "visitEnter(ElementList)";
1005 Trace.param(CLASS, this, method, "current", current);
1006 String context = traverser.getCurrentContext().getLocationWithinModule();
1007
1008 // to find something like getElement(0).getList().getElement(0)
1009 if (context.startsWith(find.getLocationWithinModule())) {
1010 throw new LocationFoundException(find);
1011 }
1012
1013 checkMatching(method);
1014
1015 traverser.setLocationWithinModule(context + ".getOperator()");
1016 checkIfFound();
1017 traverser.setLocationWithinModule(context);
1018 final boolean firstIsAtom = list.size() > 0 && list.getElement(0).isAtom();
1019 if (firstIsAtom) {
1020 traverser.setLocationWithinModule(context + ".getElement(0)");
1021 if ("VAR".equals(operator) || "PREDVAR".equals(operator)
1022 || "FUNVAR".equals(operator)) {
1023 current.setAttribute("id");
1024 checkIfFound();
1025 } else if ("PREDCON".equals(operator) || "FUNCON".equals(operator)) {
1026 current.setAttribute("ref");
1027 checkIfFound();
1028 } else { // should not occur, but just in case
1029 current.setAttribute(null);
1030 Trace.info(CLASS, this, method, "unknown operator " + operator);
1031 throw new LocationFoundException(traverser.getCurrentContext());
1032 }
1033 }
1034 }
1035
1036 public final void visitLeave(final ElementList list) {
1037 leave();
1038 }
1039
1040 /* we dont need it any more
1041 public final void visitEnter(final Atom atom) throws ModuleDataException {
1042 final String method = "visitEnter(Atom)";
1043 Trace.param(this, method, "current", current);
1044 final String context = traverser.getCurrentContext().getLocationWithinModule();
1045 // mime 20070217: should never occur
1046 checkMatching(method);
1047 }
1048 */
1049 public final void visitEnter(final LiteratureItemList list) throws ModuleDataException {
1050 enter("BIBLIOGRAPHY");
1051 final String method = "visitEnter(LiteratureItemList)";
1052 Trace.param(CLASS, this, method, "current", current);
1053 checkMatching(method);
1054 }
1055
1056 public final void visitLeave(final LiteratureItemList list) {
1057 leave();
1058 }
1059
1060 public final void visitEnter(final LiteratureItem item) throws ModuleDataException {
1061 enter("ITEM");
1062 final String method = "visitEnter(LiteratureItem)";
1063 Trace.param(CLASS, this, method, "current", current);
1064 final String context = traverser.getCurrentContext().getLocationWithinModule();
1065 checkMatching(method);
1066
1067 traverser.setLocationWithinModule(context + ".getLabel()");
1068 current.setAttribute("label");
1069 checkIfFound();
1070 }
1071
1072 public final void visitLeave(final LiteratureItem item) {
1073 leave();
1074 }
1075
1076 /**
1077 * Check if searched for context is already reached.
1078 *
1079 * @throws LocationFoundException We have found it.
1080 */
1081 private final void checkIfFound() throws LocationFoundException {
1082 if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
1083 .getLocationWithinModule())) {
1084 throw new LocationFoundException(traverser.getCurrentContext());
1085 }
1086 }
1087
1088 /**
1089 * Checks if the current context matches the beginning of the context we want to find.
1090 * This method must be called at the beginning of the <code>visitEnter</code> method when
1091 * {@link #current} is correctly set. If the context of a previously visited node was already
1092 * matching and the current node doesn't start with the old matching context any longer we
1093 * throw a {@link LocationNotFoundException}.
1094 *
1095 * @param method Method we were called from.
1096 * @throws LocationNotFoundException Not found.
1097 * @throws LocationFoundException Success!
1098 */
1099 private final void checkMatching(final String method)
1100 throws LocationNotFoundException, LocationFoundException {
1101 final String context = traverser.getCurrentContext().getLocationWithinModule();
1102 if (find.getLocationWithinModule().startsWith(context)) {
1103 Trace.info(CLASS, this, method, "beginning matches");
1104 Trace.paramInfo(CLASS, this, method, "context", context);
1105 matching = true;
1106 matchingBegin = context; // remember matching context
1107 matchingPath = new SimpleXPath(current); // remember last matching XPath
1108 } else {
1109 if (matching) {
1110 // for example we are looking for "getHeader().getImportList().getImport(2)"
1111 // getHeader() matches, we remember "getHeader()"
1112 // getHeader().getSpecification() doesn't match, but still starts with "getHeader()"
1113 // getHeader().getImportList() matches, we remember "getHeader.getImportList()"
1114 // getHeader().getImportList().get(0) doesn't match but still starts with
1115 // "getHeader.getImportList()"
1116 if (!context.startsWith(matchingBegin)) {
1117 // Matching lost, that means we will never found the location
1118 // so what can we do? We just return the last matching location and hope
1119 // it is close enough to the searched one. But at least we do some
1120 // logging here:
1121 Trace.info(CLASS, this, method, "matching lost");
1122 Trace.paramInfo(CLASS, this, method, "last match ", matchingBegin);
1123 Trace.paramInfo(CLASS, this, method, "current context", context);
1124 Trace.paramInfo(CLASS, this, method, "find context ", find.getLocationWithinModule());
1125
1126 // do we really want to fail?
1127 if (Boolean.TRUE.toString().equalsIgnoreCase(
1128 System.getProperty("qedeq.test.xmlLocationFailures"))) {
1129 throw new LocationNotFoundException(traverser.getCurrentContext(),
1130 matchingBegin, find.getLocationWithinModule());
1131 }
1132
1133 Trace.traceStack(CLASS, this, method);
1134 Trace.info(CLASS, this, method, "changing XPath to last matching one");
1135 // now we change the current XPath to the last matching one because the
1136 // contents of "current" is used as the resulting XPath later on when
1137 // catching the exception in {@link #find()}
1138 current = matchingPath;
1139 throw new LocationFoundException(new ModuleContext(find.getModuleLocation(),
1140 matchingBegin));
1141 }
1142 }
1143 traverser.setBlocked(true); // block further search in sub nodes
1144 }
1145 checkIfFound();
1146 }
1147
1148 /**
1149 * Enter new XML element.
1150 *
1151 * @param element Element name.
1152 */
1153 private final void enter(final String element) {
1154 level++;
1155 current.addElement(element, addOccurence(element));
1156 }
1157
1158 /**
1159 * Leave last XML element.
1160 */
1161 private final void leave() {
1162 level--;
1163 current.deleteLastElement();
1164 traverser.setBlocked(false); // enable further search in nodes
1165 }
1166
1167 /**
1168 * Add element occurrence. For example we have <code>getHeader().getImportList().get(2)</code>
1169 * and we want to get <code>QEDEQ/HEADER/IMPORTS/IMPORT[3]</code>.
1170 * So we call <code>enter("QEDEQ")</code>, <code>enter("HEADER")</code>,
1171 * <code>enter("IMPORTS")</code> and last but not least
1172 * three times the sequence <code>enter("IMPORT")</code>, <code>leave("IMPORT")</code>,
1173 *
1174 * @param name Element that occurred.
1175 * @return Number of occurrences including this one.
1176 */
1177 private final int addOccurence(final String name) {
1178 while (level < elements.size()) {
1179 elements.remove(elements.size() - 1);
1180 }
1181 while (level > elements.size()) {
1182 elements.add(new HashMap());
1183 }
1184 final Map levelMap = (Map) elements.get(level - 1);
1185 final Enumerator counter;
1186 if (levelMap.containsKey(name)) {
1187 counter = (Enumerator) levelMap.get(name);
1188 counter.increaseNumber();
1189 } else {
1190 counter = new Enumerator(1);
1191 levelMap.put(name, counter);
1192 }
1193 return counter.getNumber();
1194 }
1195
1196 }
|