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