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