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