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