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