001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.module;
017
018 import org.qedeq.base.io.SourceArea;
019 import org.qedeq.base.trace.Trace;
020 import org.qedeq.base.utility.StringUtility;
021 import org.qedeq.kernel.se.base.module.Axiom;
022 import org.qedeq.kernel.se.base.module.FunctionDefinition;
023 import org.qedeq.kernel.se.base.module.Node;
024 import org.qedeq.kernel.se.base.module.PredicateDefinition;
025 import org.qedeq.kernel.se.base.module.Proposition;
026 import org.qedeq.kernel.se.base.module.Rule;
027 import org.qedeq.kernel.se.common.ModuleContext;
028 import org.qedeq.kernel.se.common.ModuleDataException;
029 import org.qedeq.kernel.se.common.Plugin;
030 import org.qedeq.kernel.se.common.RuleKey;
031 import org.qedeq.kernel.se.common.SourceFileException;
032 import org.qedeq.kernel.se.common.SourceFileExceptionList;
033 import org.qedeq.kernel.se.visitor.AbstractModuleVisitor;
034 import org.qedeq.kernel.se.visitor.QedeqNotNullTraverser;
035 import org.qedeq.kernel.se.visitor.QedeqNumbers;
036 import org.qedeq.kernel.se.visitor.QedeqTraverser;
037
038
039 /**
040 * Basic visitor that gives some error collecting features. Also hides the
041 * traverser that does the work.
042 * <p>
043 * If you change the implementation of this class you also have to change the
044 * implementation of the same class in project QedeqKernelBoTest!!!
045 *
046 * @author Michael Meyling
047 */
048 public abstract class ControlVisitor extends AbstractModuleVisitor {
049
050 /** This class. */
051 private static final Class CLASS = ControlVisitor.class;
052
053 /** This plugin we work for. */
054 private final Plugin plugin;
055
056 /** QEDEQ BO object to work on. */
057 private final KernelQedeqBo prop;
058
059 /** Traverse QEDEQ module with this traverser. */
060 private final QedeqNotNullTraverser traverser;
061
062 /** List of Exceptions of type error during Module visit. */
063 private SourceFileExceptionList errorList;
064
065 /** List of Exceptions of type warnings during Module visit. */
066 private SourceFileExceptionList warningList;
067
068
069 /**
070 * Constructor. Can only be used if instance also implements {@link Plugin}.
071 *
072 * @param prop Internal QedeqBo.
073 */
074 protected ControlVisitor(final KernelQedeqBo prop) {
075 this.prop = prop;
076 this.plugin = (Plugin) this;
077 this.traverser = new QedeqNotNullTraverser(prop.getModuleAddress(), this);
078 }
079
080 /**
081 * Constructor.
082 *
083 * @param plugin This plugin we work for.
084 * @param prop Internal QedeqBo.
085 */
086 protected ControlVisitor(final Plugin plugin, final KernelQedeqBo prop) {
087 this.plugin = plugin;
088 this.prop = prop;
089 this.traverser = new QedeqNotNullTraverser(prop.getModuleAddress(), this);
090 }
091
092 /**
093 * Get QedeqBo.
094 *
095 * @return QEDEQ module were are in.
096 */
097 public KernelQedeqBo getQedeqBo() {
098 return this.prop;
099 }
100
101 /**
102 * Get node that is currently parsed. Might be <code>null</code>.
103 *
104 * @return QEDEQ node were are currently in.
105 */
106 public KernelNodeBo getNodeBo() {
107 final Node node = traverser.getNode();
108 if (node == null || getQedeqBo() == null) {
109 return null;
110 }
111 return getQedeqBo().getLabels().getNode(node.getId());
112 }
113
114 /**
115 * Start traverse of QedeqBo. If during the traverse a {@link ModuleDataException}
116 * occurs it is thrown till high level and transformed into a
117 * {@link SourceFileExceptionList}. Otherwise all collected exceptions
118 * (via {@link #addError(ModuleDataException)} and
119 * {@link #addError(SourceFileException)}) are thrown.
120 *
121 * @throws SourceFileExceptionList All collected exceptions.
122 */
123 public void traverse() throws SourceFileExceptionList {
124 if (getQedeqBo().getQedeq() == null) {
125 addWarning(new SourceFileException(getPlugin(),
126 ModuleErrors.QEDEQ_MODULE_NOT_LOADED_CODE,
127 ModuleErrors.QEDEQ_MODULE_NOT_LOADED_TEXT,
128 new IllegalArgumentException(),
129 new SourceArea(getQedeqBo().getModuleAddress().getUrl()),
130 null));
131 return; // we can do nothing without a loaded module
132 }
133 try {
134 this.traverser.accept(getQedeqBo().getQedeq());
135 } catch (ModuleDataException me) {
136 addError(me);
137 } catch (RuntimeException e) {
138 Trace.fatal(CLASS, this, "traverse", "looks like a programming error", e);
139 addError(new RuntimeVisitorException(getCurrentContext(), e));
140 }
141 if (errorList != null && errorList.size() > 0) {
142 throw errorList;
143 }
144 }
145
146 /**
147 * Get current context within original. Remember to use the copy constructor
148 * when trying to remember this context!
149 *
150 * @return Current context.
151 */
152 public ModuleContext getCurrentContext() {
153 return this.traverser.getCurrentContext();
154 }
155
156 /**
157 * Add exception to error collection.
158 *
159 * @param me Exception to be added.
160 */
161 protected void addError(final ModuleDataException me) {
162 addError(prop.createSourceFileException(getPlugin(), me));
163 }
164
165 /**
166 * Add exception to error collection.
167 *
168 * @param sf Exception to be added.
169 */
170 protected void addError(final SourceFileException sf) {
171 if (errorList == null) {
172 errorList = new SourceFileExceptionList(sf);
173 } else {
174 errorList.add(sf);
175 }
176 }
177
178 /**
179 * Get list of errors that occurred during visit.
180 *
181 * @return Exception list.
182 */
183 public SourceFileExceptionList getErrorList() {
184 return errorList;
185 }
186
187 /**
188 * Add exception to warning collection.
189 *
190 * @param me Exception to be added.
191 */
192 protected void addWarning(final ModuleDataException me) {
193 // FIXME 20101026 m31: here no SourcefileException should be added!
194 // there might exist different representations (e.g. XML, utf8 text, html)
195 // and we might want to resolve the location for them also.
196 // And perhaps resolving all error locations at the same time is
197 // faster because one has to load the source file only once...
198 addWarning(prop.createSourceFileException(getPlugin(), me));
199 }
200
201 /**
202 * Add exception to warning collection.
203 *
204 * @param sf Exception to be added.
205 */
206 private void addWarning(final SourceFileException sf) {
207 if (warningList == null) {
208 warningList = new SourceFileExceptionList(sf);
209 } else {
210 warningList.add(sf);
211 }
212 }
213
214 /**
215 * Get list of warnings that occurred during visit.
216 *
217 * @return Exception list.
218 */
219 public SourceFileExceptionList getWarningList() {
220 return warningList;
221 }
222
223 /**
224 * Set if further traverse is blocked.
225 *
226 * @param blocked Further traverse blocked?
227 */
228 protected void setBlocked(final boolean blocked) {
229 traverser.setBlocked(blocked);
230 }
231
232 /**
233 * Get if further traverse is blocked.
234 *
235 * @return Further traverse blocked?
236 */
237 public boolean getBlocked() {
238 return traverser.getBlocked();
239 }
240
241 /**
242 * Get plugin we work for.
243 *
244 * @return Plugin we work for.
245 */
246 public Plugin getPlugin() {
247 return plugin;
248 }
249
250 /**
251 * Get location info from traverser.
252 *
253 * @return Location description.
254 */
255 public String getLocationDescription() {
256 return traverser.getLocationDescription();
257 }
258
259 /**
260 * Get percentage of visit currently done.
261 *
262 * @return Value between 0 and 100.
263 */
264 public double getExecutionPercentage() {
265 return traverser.getVisitPercentage();
266 }
267
268 /**
269 * Get copy of current counters.
270 *
271 * @return Values of various counters.
272 */
273 public QedeqNumbers getCurrentNumbers() {
274 return traverser.getCurrentNumbers();
275 }
276
277 /**
278 * Get current (QEDEQ module local) rule version for given rule name.
279 *
280 * @param name Rule name
281 * @return Current (local) rule version. Might be <code>null</code>.
282 */
283 public RuleKey getLocalRuleKey(final String name) {
284 return traverser.getLocalRuleKey(name);
285 }
286
287 /**
288 * Get internal kernel services. Convenience method.
289 *
290 * @return Internal kernel services.
291 */
292 public InternalKernelServices getServices() {
293 return prop.getKernelServices();
294 }
295
296 /**
297 * Get link for given reference.
298 *
299 * @param reference String to parse.
300 * @param context Here the link is in the source text.
301 * @param addWarning Should we add a warning if an error occurs?
302 * @param addError Should we add an error if an error occurs?
303 * @return Generated link.
304 */
305 public Reference getReference(final String reference, final ModuleContext context,
306 final boolean addWarning, final boolean addError) {
307 // get node we are currently in
308 KernelNodeBo node = getNodeBo();
309 final Reference fallback = new DefaultReference(node, null, "", null,
310 (reference != null ? reference : "") + "?", "", "");
311 if (reference == null || reference.length() <= 0) {
312 return fallback;
313 }
314 if (reference.indexOf("!") >= 0 && reference.indexOf("/") >= 0) {
315 if (addWarning) {
316 addWarning(new ReferenceLinkException(
317 ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_CODE,
318 ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_TEXT
319 + "\"" + reference + "\"", context));
320 }
321 if (addError) {
322 addError(new ReferenceLinkException(
323 ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_CODE,
324 ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_TEXT
325 + "\"" + reference + "\"", context));
326 }
327 }
328 // is the reference a pure proof line label?
329 if (node != null && node.isProofLineLabel(reference)) {
330 return new DefaultReference(node, null, "", node, node.getNodeVo().getId(), "", reference);
331 }
332 // is the reference a pure node label?
333 if (getQedeqBo().getLabels().isNode(reference)) {
334 return new DefaultReference(node, null, "", getQedeqBo().getLabels().getNode(
335 reference), reference, "", "");
336 }
337 // do we have an external module reference without node?
338 if (getQedeqBo().getLabels().isModule(reference)) {
339 return new DefaultReference(node,
340 (KernelQedeqBo) getQedeqBo().getLabels().getReferences().getQedeqBo(reference),
341 reference, null, "", "", "");
342
343 }
344
345 String moduleLabel = ""; // module import
346 String nodeLabel = ""; // module intern node reference
347 String lineLabel = ""; // proof line label
348 String subLabel = ""; // sub label
349
350 final String[] split = StringUtility.split(reference, ".");
351 if (split.length <= 1 || split.length > 2) {
352 if (split.length == 1) {
353 nodeLabel = split[0];
354 } else if (split.length > 2) {
355 if (addWarning) {
356 addWarning(new ReferenceLinkException(
357 ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_CODE,
358 ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_TEXT
359 + "\"" + reference + "\"", context));
360 }
361 if (addError) {
362 addError(new ReferenceLinkException(
363 ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_CODE,
364 ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_TEXT
365 + "\"" + reference + "\"", context));
366 }
367 return fallback;
368 }
369 } else {
370 moduleLabel = split[0];
371 nodeLabel = split[1];
372 }
373
374 if (nodeLabel.indexOf("!") >= 0) {
375 final String[] split2 = StringUtility.split(nodeLabel, "!");
376 if (split2.length != 2) {
377 if (addWarning) {
378 addWarning(new ReferenceLinkException(
379 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_CODE,
380 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_TEXT
381 + "\"" + reference + "\"", context));
382 }
383 if (addError) {
384 addError(new ReferenceLinkException(
385 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_CODE,
386 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_TEXT
387 + "\"" + reference + "\"", context));
388 }
389 }
390 nodeLabel = split2[0];
391 if (split.length > 1) {
392 lineLabel = split2[1];
393 }
394 }
395 if (nodeLabel.indexOf("/") >= 0) {
396 final String[] split2 = StringUtility.split(nodeLabel, "/");
397 if (split2.length != 2) {
398 if (addWarning) {
399 addWarning(new ReferenceLinkException(
400 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_CODE,
401 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_TEXT
402 + "\"" + reference + "\"", context));
403 }
404 if (addError) {
405 addError(new ReferenceLinkException(
406 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_CODE,
407 ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_TEXT
408 + "\"" + reference + "\"", context));
409 }
410 }
411 nodeLabel = split2[0];
412 if (split.length > 1) {
413 subLabel = split2[1];
414 }
415 }
416 KernelQedeqBo module = null;
417 KernelNodeBo eNode = null;
418 if (moduleLabel != null && moduleLabel.length() > 0) {
419 module = getQedeqBo().getKernelRequiredModules().getKernelQedeqBo(moduleLabel);
420 eNode = (module != null ? module.getLabels().getNode(nodeLabel) : null);
421 } else {
422 eNode = getQedeqBo().getLabels().getNode(nodeLabel);
423 }
424 if ((moduleLabel != null && moduleLabel.length() > 0) && module == null) {
425 if (addWarning) {
426 addWarning(new ReferenceLinkException(
427 ModuleErrors.MODULE_REFERENCE_NOT_FOUND_CODE,
428 ModuleErrors.MODULE_REFERENCE_NOT_FOUND_TEXT
429 + "\"" + reference + "\"", context));
430 }
431 if (addError) {
432 addError(new ReferenceLinkException(
433 ModuleErrors.MODULE_REFERENCE_NOT_FOUND_CODE,
434 ModuleErrors.MODULE_REFERENCE_NOT_FOUND_TEXT
435 + "\"" + reference + "\"", context));
436 }
437 return new DefaultReference(node, module, moduleLabel + "?", eNode, nodeLabel, subLabel, lineLabel);
438 }
439 if (eNode == null) {
440 if (addWarning) {
441 addWarning(new ReferenceLinkException(
442 ModuleErrors.NODE_REFERENCE_NOT_FOUND_CODE,
443 ModuleErrors.NODE_REFERENCE_NOT_FOUND_TEXT
444 + "\"" + reference + "\"", context));
445 }
446 if (addError) {
447 addError(new ReferenceLinkException(
448 ModuleErrors.NODE_REFERENCE_NOT_FOUND_CODE,
449 ModuleErrors.NODE_REFERENCE_NOT_FOUND_TEXT
450 + "\"" + reference + "\"", context));
451 }
452 return new DefaultReference(node, module, moduleLabel, eNode, nodeLabel + "?", subLabel, lineLabel);
453 }
454 return new DefaultReference(node, module, moduleLabel, eNode, nodeLabel, subLabel, lineLabel);
455 }
456
457 /**
458 * Get display text for node. The module of the node is ignored.
459 *
460 * @param label Label for node. Fallback if <code>kNode == null</code>.
461 * @param kNode Node for which we want a textual representation.
462 * @param language Language. Might be <code>null</code>.
463 * @return Textual node representation.
464 */
465 public String getNodeDisplay(final String label, final KernelNodeBo kNode, final String language) {
466 String display = label;
467 if (kNode == null) {
468 return display;
469 }
470 QedeqNumbers data = kNode.getNumbers();
471 Node node = kNode.getNodeVo();
472 if (node.getNodeType() instanceof Axiom) {
473 if ("de".equals(language)) {
474 display = "Axiom";
475 } else {
476 display = "axiom";
477 }
478 display += " " + data.getAxiomNumber();
479 } else if (node.getNodeType() instanceof Proposition) {
480 if ("de".equals(language)) {
481 display = "Proposition";
482 } else {
483 display = "proposition";
484 }
485 display += " " + data.getPropositionNumber();
486 } else if (node.getNodeType() instanceof FunctionDefinition) {
487 if ("de".equals(language)) {
488 display = "Definition";
489 } else {
490 display = "definition";
491 }
492 display += " " + (data.getPredicateDefinitionNumber() + data.getFunctionDefinitionNumber());
493 } else if (node.getNodeType() instanceof PredicateDefinition) {
494 if ("de".equals(language)) {
495 display = "Definition";
496 } else {
497 display = "definition";
498 }
499 display += " " + (data.getPredicateDefinitionNumber() + data.getFunctionDefinitionNumber());
500 } else if (node.getNodeType() instanceof Rule) {
501 if ("de".equals(language)) {
502 display = "Regel";
503 } else {
504 display = "rule";
505 }
506 display += " " + data.getRuleNumber();
507 } else {
508 if ("de".equals(language)) {
509 display = "Unbekannt " + node.getId();
510 } else {
511 display = "unknown " + node.getId();
512 }
513 }
514 return display;
515 }
516
517 /**
518 * Set location information where are we within the original module.
519 *
520 * @param locationWithinModule Location within module.
521 */
522 public void setLocationWithinModule(final String locationWithinModule) {
523 getCurrentContext().setLocationWithinModule(locationWithinModule);
524 // m31: for testing [code is integrated in JUnit test, this class is doubled in QedeqKernelBoTest
525 // try {
526 // DynamicGetter.get(getQedeqBo().getQedeq(), getCurrentContext().getLocationWithinModule());
527 // } catch (RuntimeException e) {
528 // System.err.println(getCurrentContext().getLocationWithinModule());
529 // throw e;
530 // } catch (IllegalAccessException e) {
531 // throw new RuntimeException(e);
532 // } catch (InvocationTargetException e) {
533 // throw new RuntimeException(e);
534 // }
535 }
536
537 /**
538 * Get traverser for QEDEQ module.
539 *
540 * @return Traverser used.
541 */
542 public QedeqTraverser getTraverser() {
543 return traverser;
544 }
545 }
|