1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
2 | * |
3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
4 | * |
5 | * "Hilbert II" is free software; you can redistribute |
6 | * it and/or modify it under the terms of the GNU General Public |
7 | * License as published by the Free Software Foundation; either |
8 | * version 2 of the License, or (at your option) any later version. |
9 | * |
10 | * This program is distributed in the hope that it will be useful, |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
13 | * GNU General Public License for more details. |
14 | */ |
15 | |
16 | package org.qedeq.kernel.bo.service.basis; |
17 | |
18 | import org.qedeq.base.io.SourceArea; |
19 | import org.qedeq.base.trace.Trace; |
20 | import org.qedeq.base.utility.StringUtility; |
21 | import org.qedeq.kernel.bo.module.DefaultReference; |
22 | import org.qedeq.kernel.bo.module.InternalKernelServices; |
23 | import org.qedeq.kernel.bo.module.InternalModuleServiceCall; |
24 | import org.qedeq.kernel.bo.module.InternalServiceJob; |
25 | import org.qedeq.kernel.bo.module.KernelNodeBo; |
26 | import org.qedeq.kernel.bo.module.KernelQedeqBo; |
27 | import org.qedeq.kernel.bo.module.ModuleErrors; |
28 | import org.qedeq.kernel.bo.module.Reference; |
29 | import org.qedeq.kernel.bo.module.ReferenceLinkException; |
30 | import org.qedeq.kernel.se.base.module.Axiom; |
31 | import org.qedeq.kernel.se.base.module.FunctionDefinition; |
32 | import org.qedeq.kernel.se.base.module.Node; |
33 | import org.qedeq.kernel.se.base.module.PredicateDefinition; |
34 | import org.qedeq.kernel.se.base.module.Proposition; |
35 | import org.qedeq.kernel.se.base.module.Rule; |
36 | import org.qedeq.kernel.se.common.ModuleContext; |
37 | import org.qedeq.kernel.se.common.ModuleDataException; |
38 | import org.qedeq.kernel.se.common.RuleKey; |
39 | import org.qedeq.kernel.se.common.Service; |
40 | import org.qedeq.kernel.se.common.SourceFileException; |
41 | import org.qedeq.kernel.se.common.SourceFileExceptionList; |
42 | import org.qedeq.kernel.se.visitor.AbstractModuleVisitor; |
43 | import org.qedeq.kernel.se.visitor.InterruptException; |
44 | import org.qedeq.kernel.se.visitor.QedeqNotNullTraverser; |
45 | import org.qedeq.kernel.se.visitor.QedeqNumbers; |
46 | import org.qedeq.kernel.se.visitor.QedeqTraverser; |
47 | |
48 | |
49 | /** |
50 | * Basic visitor that gives some error collecting features. Also hides the |
51 | * traverser that does the work. |
52 | * |
53 | * @author Michael Meyling |
54 | */ |
55 | public abstract class ControlVisitor extends AbstractModuleVisitor { |
56 | |
57 | /** This class. */ |
58 | private static final Class CLASS = ControlVisitor.class; |
59 | |
60 | /** This service we work for. */ |
61 | private final Service service; |
62 | |
63 | /** QEDEQ BO object to work on. */ |
64 | private final KernelQedeqBo prop; |
65 | |
66 | /** We work in this service call. */ |
67 | private InternalModuleServiceCall call; |
68 | |
69 | /** Traverse QEDEQ module with this traverser. */ |
70 | private final QedeqNotNullTraverser traverser; |
71 | |
72 | /** List of Exceptions of type error during Module visit. */ |
73 | private SourceFileExceptionList errorList; |
74 | |
75 | /** List of Exceptions of type warnings during Module visit. */ |
76 | private SourceFileExceptionList warningList; |
77 | |
78 | /** Was traverse interrupted by user? */ |
79 | private boolean interrupted; |
80 | |
81 | /** |
82 | * Constructor. Can only be used if instance also implements {@link Service}. |
83 | * |
84 | * @param prop Internal QedeqBo. |
85 | */ |
86 | protected ControlVisitor(final KernelQedeqBo prop) { |
87 | this.prop = prop; |
88 | this.service = (Service) this; |
89 | this.traverser = new QedeqNotNullTraverser(prop.getModuleAddress(), this); |
90 | this.errorList = new SourceFileExceptionList(); |
91 | this.warningList = new SourceFileExceptionList(); |
92 | } |
93 | |
94 | /** |
95 | * Constructor. |
96 | * |
97 | * @param service This service we work for. |
98 | * @param prop Internal QedeqBo. |
99 | */ |
100 | protected ControlVisitor(final Service service, final KernelQedeqBo prop) { |
101 | this.service = service; |
102 | this.prop = prop; |
103 | this.traverser = new QedeqNotNullTraverser(prop.getModuleAddress(), this); |
104 | this.errorList = new SourceFileExceptionList(); |
105 | this.warningList = new SourceFileExceptionList(); |
106 | } |
107 | |
108 | /** |
109 | * Get QedeqBo. |
110 | * |
111 | * @return QEDEQ module were are in. |
112 | */ |
113 | public KernelQedeqBo getKernelQedeqBo() { |
114 | return this.prop; |
115 | } |
116 | |
117 | /** |
118 | * Get node that is currently parsed. Might be <code>null</code>. |
119 | * |
120 | * @return QEDEQ node were are currently in. |
121 | */ |
122 | public KernelNodeBo getNodeBo() { |
123 | final Node node = traverser.getNode(); |
124 | if (node == null || getKernelQedeqBo() == null) { |
125 | return null; |
126 | } |
127 | return getKernelQedeqBo().getLabels().getNode(node.getId()); |
128 | } |
129 | |
130 | /** |
131 | * Start traverse of QedeqBo. If during the traverse a {@link ModuleDataException} |
132 | * occurs it is thrown till high level, transformed into a |
133 | * {@link SourceFileException} and added to the error list. All collected exceptions |
134 | * (via {@link #addError(ModuleDataException)} and |
135 | * {@link #addError(SourceFileException)}) are thrown (if there were any). |
136 | * <br/> |
137 | * If you are interested in warnings you have to call {@link #getWarningList()} afterwards. |
138 | * |
139 | * @param process We work in this service process. |
140 | * @throws SourceFileExceptionList All collected error exceptions. |
141 | */ |
142 | public void traverse(final InternalServiceJob process) throws SourceFileExceptionList { |
143 | this.call = process.getInternalServiceCall(); |
144 | interrupted = false; |
145 | if (getKernelQedeqBo().getQedeq() == null) { |
146 | addWarning(new SourceFileException(getService(), |
147 | ModuleErrors.QEDEQ_MODULE_NOT_LOADED_CODE, |
148 | ModuleErrors.QEDEQ_MODULE_NOT_LOADED_TEXT, |
149 | new IllegalArgumentException(), |
150 | new SourceArea(getKernelQedeqBo().getModuleAddress().getUrl()), |
151 | null)); |
152 | return; // we can do nothing without a loaded module |
153 | } |
154 | try { |
155 | this.traverser.accept(getKernelQedeqBo().getQedeq()); |
156 | } catch (InterruptException ie) { |
157 | addError(ie); |
158 | interrupted = true; |
159 | } catch (ModuleDataException me) { |
160 | addError(me); |
161 | } catch (RuntimeException e) { |
162 | Trace.fatal(CLASS, this, "traverse", "looks like a programming error", e); |
163 | addError(new RuntimeVisitorException(getCurrentContext(), e)); |
164 | } |
165 | if (errorList.size() > 0) { |
166 | throw errorList; |
167 | } |
168 | } |
169 | |
170 | /** |
171 | * Get current context within original. Remember to use the copy constructor |
172 | * when trying to remember this context! |
173 | * |
174 | * @return Current context. |
175 | */ |
176 | public ModuleContext getCurrentContext() { |
177 | return this.traverser.getCurrentContext(); |
178 | } |
179 | |
180 | /** |
181 | * Add exception to error collection. |
182 | * |
183 | * @param me Exception to be added. |
184 | */ |
185 | protected void addError(final ModuleDataException me) { |
186 | addError(prop.createSourceFileException(getService(), me)); |
187 | } |
188 | |
189 | /** |
190 | * Add exception to error collection. |
191 | * |
192 | * @param sf Exception to be added. |
193 | */ |
194 | protected void addError(final SourceFileException sf) { |
195 | errorList.add(sf); |
196 | } |
197 | |
198 | /** |
199 | * Get list of errors that occurred during visit. |
200 | * |
201 | * @return Exception list. |
202 | */ |
203 | public SourceFileExceptionList getErrorList() { |
204 | return errorList; |
205 | } |
206 | |
207 | /** |
208 | * Did any errors occur yet? |
209 | * |
210 | * @return Non error free visits? |
211 | */ |
212 | public boolean hasErrors() { |
213 | return errorList.size() > 0; |
214 | } |
215 | |
216 | /** |
217 | * Did no errors occur yet? |
218 | * |
219 | * @return Error free visits? |
220 | */ |
221 | public boolean hasNoErrors() { |
222 | return !hasErrors(); |
223 | } |
224 | |
225 | /** |
226 | * Add exception to warning collection. |
227 | * |
228 | * @param me Exception to be added. |
229 | */ |
230 | protected void addWarning(final ModuleDataException me) { |
231 | // TODO 20101026 m31: here no SourcefileException should be added! |
232 | // there might exist different representations (e.g. XML, utf8 text, html) |
233 | // and we might want to resolve the location for them also. |
234 | // And perhaps resolving all error locations at the same time is |
235 | // faster because one has to load the source file only once... |
236 | addWarning(prop.createSourceFileException(getService(), me)); |
237 | } |
238 | |
239 | /** |
240 | * Add exception to warning collection. |
241 | * |
242 | * @param sf Exception to be added. |
243 | */ |
244 | private void addWarning(final SourceFileException sf) { |
245 | warningList.add(sf); |
246 | } |
247 | |
248 | /** |
249 | * Get list of warnings that occurred during visit. |
250 | * |
251 | * @return Exception list. |
252 | */ |
253 | public SourceFileExceptionList getWarningList() { |
254 | return warningList; |
255 | } |
256 | |
257 | /** |
258 | * Set if further traverse is blocked. |
259 | * |
260 | * @param blocked Further traverse blocked? |
261 | */ |
262 | protected void setBlocked(final boolean blocked) { |
263 | traverser.setBlocked(blocked); |
264 | } |
265 | |
266 | /** |
267 | * Get if further traverse is blocked. |
268 | * |
269 | * @return Further traverse blocked? |
270 | */ |
271 | public boolean getBlocked() { |
272 | return traverser.getBlocked(); |
273 | } |
274 | |
275 | /** |
276 | * Get service call we work in. |
277 | * |
278 | * @return Service process we work for. |
279 | */ |
280 | public InternalModuleServiceCall getInternalServiceCall() { |
281 | return call; |
282 | } |
283 | |
284 | /** |
285 | * Get service we work for. |
286 | * |
287 | * @return Service we work for. |
288 | */ |
289 | public Service getService() { |
290 | return service; |
291 | } |
292 | |
293 | /** |
294 | * Get location info from traverser. |
295 | * |
296 | * @return Location description. |
297 | */ |
298 | public String getLocationDescription() { |
299 | return traverser.getLocationDescription(); |
300 | } |
301 | |
302 | /** |
303 | * Get percentage of visit currently done. |
304 | * |
305 | * @return Value between 0 and 100. |
306 | */ |
307 | public double getVisitPercentage() { |
308 | return traverser.getVisitPercentage(); |
309 | } |
310 | |
311 | /** |
312 | * Get copy of current counters. |
313 | * |
314 | * @return Values of various counters. |
315 | */ |
316 | public QedeqNumbers getCurrentNumbers() { |
317 | return traverser.getCurrentNumbers(); |
318 | } |
319 | |
320 | /** |
321 | * Get current (QEDEQ module local) rule version for given rule name. |
322 | * |
323 | * @param name Rule name |
324 | * @return Current (local) rule version. Might be <code>null</code>. |
325 | */ |
326 | public RuleKey getLocalRuleKey(final String name) { |
327 | return traverser.getLocalRuleKey(name); |
328 | } |
329 | |
330 | /** |
331 | * Get internal kernel services. Convenience method. |
332 | * |
333 | * @return Internal kernel services. |
334 | */ |
335 | public InternalKernelServices getServices() { |
336 | return prop.getKernelServices(); |
337 | } |
338 | |
339 | /** |
340 | * Was traverse interrupted by user? |
341 | * |
342 | * @return Did we get an interrupt? |
343 | */ |
344 | public boolean getInterrupted() { |
345 | return interrupted; |
346 | } |
347 | |
348 | /** |
349 | * Get link for given reference. |
350 | * |
351 | * @param reference String to parse. |
352 | * @param context Here the link is in the source text. |
353 | * @param addWarning Should we add a warning if an error occurs? |
354 | * @param addError Should we add an error if an error occurs? |
355 | * @return Generated link. Never <code>null</code>. |
356 | */ |
357 | public Reference getReference(final String reference, final ModuleContext context, |
358 | final boolean addWarning, final boolean addError) { |
359 | // get node we are currently in |
360 | KernelNodeBo node = getNodeBo(); |
361 | final Reference fallback = new DefaultReference(node, null, "", null, |
362 | (reference != null ? reference : "") + "?", "", ""); |
363 | if (reference == null || reference.length() <= 0) { |
364 | return fallback; |
365 | } |
366 | if (reference.indexOf("!") >= 0 && reference.indexOf("/") >= 0) { |
367 | if (addWarning) { |
368 | addWarning(new ReferenceLinkException( |
369 | ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_CODE, |
370 | ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_TEXT |
371 | + "\"" + reference + "\"", context)); |
372 | } |
373 | if (addError) { |
374 | addError(new ReferenceLinkException( |
375 | ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_CODE, |
376 | ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_TEXT |
377 | + "\"" + reference + "\"", context)); |
378 | } |
379 | } |
380 | // is the reference a pure proof line label? |
381 | if (node != null && node.isProofLineLabel(reference)) { |
382 | return new DefaultReference(node, null, "", node, node.getNodeVo().getId(), "", reference); |
383 | } |
384 | // is the reference a pure node label? |
385 | if (getKernelQedeqBo().getLabels().isNode(reference)) { |
386 | return new DefaultReference(node, null, "", getKernelQedeqBo().getLabels().getNode( |
387 | reference), reference, "", ""); |
388 | } |
389 | // do we have an external module reference without node? |
390 | if (getKernelQedeqBo().getLabels().isModule(reference)) { |
391 | return new DefaultReference(node, |
392 | (KernelQedeqBo) getKernelQedeqBo().getLabels().getReferences().getQedeqBo(reference), |
393 | reference, null, "", "", ""); |
394 | |
395 | } |
396 | |
397 | String moduleLabel = ""; // module import |
398 | String nodeLabel = ""; // module intern node reference |
399 | String lineLabel = ""; // proof line label |
400 | String subLabel = ""; // sub label |
401 | |
402 | final String[] split = StringUtility.split(reference, "."); |
403 | if (split.length <= 1 || split.length > 2) { |
404 | if (split.length == 1) { |
405 | nodeLabel = split[0]; |
406 | } else if (split.length > 2) { |
407 | if (addWarning) { |
408 | addWarning(new ReferenceLinkException( |
409 | ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_CODE, |
410 | ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_TEXT |
411 | + "\"" + reference + "\"", context)); |
412 | } |
413 | if (addError) { |
414 | addError(new ReferenceLinkException( |
415 | ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_CODE, |
416 | ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_TEXT |
417 | + "\"" + reference + "\"", context)); |
418 | } |
419 | return fallback; |
420 | } |
421 | } else { |
422 | moduleLabel = split[0]; |
423 | nodeLabel = split[1]; |
424 | } |
425 | |
426 | if (nodeLabel.indexOf("!") >= 0) { |
427 | final String[] split2 = StringUtility.split(nodeLabel, "!"); |
428 | if (split2.length != 2) { |
429 | if (addWarning) { |
430 | addWarning(new ReferenceLinkException( |
431 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_CODE, |
432 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_TEXT |
433 | + "\"" + reference + "\"", context)); |
434 | } |
435 | if (addError) { |
436 | addError(new ReferenceLinkException( |
437 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_CODE, |
438 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_TEXT |
439 | + "\"" + reference + "\"", context)); |
440 | } |
441 | } |
442 | nodeLabel = split2[0]; |
443 | if (split.length > 1) { |
444 | lineLabel = split2[1]; |
445 | } |
446 | } |
447 | if (nodeLabel.indexOf("/") >= 0) { |
448 | final String[] split2 = StringUtility.split(nodeLabel, "/"); |
449 | if (split2.length != 2) { |
450 | if (addWarning) { |
451 | addWarning(new ReferenceLinkException( |
452 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_CODE, |
453 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_TEXT |
454 | + "\"" + reference + "\"", context)); |
455 | } |
456 | if (addError) { |
457 | addError(new ReferenceLinkException( |
458 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_CODE, |
459 | ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_TEXT |
460 | + "\"" + reference + "\"", context)); |
461 | } |
462 | } |
463 | nodeLabel = split2[0]; |
464 | if (split.length > 1) { |
465 | subLabel = split2[1]; |
466 | } |
467 | } |
468 | KernelQedeqBo module = null; |
469 | KernelNodeBo eNode = null; |
470 | if (moduleLabel != null && moduleLabel.length() > 0) { |
471 | module = getKernelQedeqBo().getKernelRequiredModules().getKernelQedeqBo(moduleLabel); |
472 | eNode = (module != null ? module.getLabels().getNode(nodeLabel) : null); |
473 | } else { |
474 | eNode = getKernelQedeqBo().getLabels().getNode(nodeLabel); |
475 | } |
476 | if ((moduleLabel != null && moduleLabel.length() > 0) && module == null) { |
477 | if (addWarning) { |
478 | addWarning(new ReferenceLinkException( |
479 | ModuleErrors.MODULE_REFERENCE_NOT_FOUND_CODE, |
480 | ModuleErrors.MODULE_REFERENCE_NOT_FOUND_TEXT |
481 | + "\"" + reference + "\"", context)); |
482 | } |
483 | if (addError) { |
484 | addError(new ReferenceLinkException( |
485 | ModuleErrors.MODULE_REFERENCE_NOT_FOUND_CODE, |
486 | ModuleErrors.MODULE_REFERENCE_NOT_FOUND_TEXT |
487 | + "\"" + reference + "\"", context)); |
488 | } |
489 | return new DefaultReference(node, module, moduleLabel + "?", eNode, nodeLabel, subLabel, lineLabel); |
490 | } |
491 | if (eNode == null) { |
492 | if (addWarning) { |
493 | addWarning(new ReferenceLinkException( |
494 | ModuleErrors.NODE_REFERENCE_NOT_FOUND_CODE, |
495 | ModuleErrors.NODE_REFERENCE_NOT_FOUND_TEXT |
496 | + "\"" + reference + "\"", context)); |
497 | } |
498 | if (addError) { |
499 | addError(new ReferenceLinkException( |
500 | ModuleErrors.NODE_REFERENCE_NOT_FOUND_CODE, |
501 | ModuleErrors.NODE_REFERENCE_NOT_FOUND_TEXT |
502 | + "\"" + reference + "\"", context)); |
503 | } |
504 | return new DefaultReference(node, module, moduleLabel, eNode, nodeLabel + "?", subLabel, lineLabel); |
505 | } |
506 | return new DefaultReference(node, module, moduleLabel, eNode, nodeLabel, subLabel, lineLabel); |
507 | } |
508 | |
509 | /** |
510 | * Get display text for node. The module of the node is ignored. |
511 | * |
512 | * @param label Label for node. Fallback if <code>kNode == null</code>. |
513 | * @param kNode Node for which we want a textual representation. |
514 | * @param language Language. Might be <code>null</code>. |
515 | * @return Textual node representation. |
516 | */ |
517 | public String getNodeDisplay(final String label, final KernelNodeBo kNode, final String language) { |
518 | String display = label; |
519 | if (kNode == null) { |
520 | return display; |
521 | } |
522 | QedeqNumbers data = kNode.getNumbers(); |
523 | Node node = kNode.getNodeVo(); |
524 | if (node.getNodeType() instanceof Axiom) { |
525 | if ("de".equals(language)) { |
526 | display = "Axiom"; |
527 | } else { |
528 | display = "axiom"; |
529 | } |
530 | display += " " + data.getAxiomNumber(); |
531 | } else if (node.getNodeType() instanceof Proposition) { |
532 | if ("de".equals(language)) { |
533 | display = "Proposition"; |
534 | } else { |
535 | display = "proposition"; |
536 | } |
537 | display += " " + data.getPropositionNumber(); |
538 | } else if (node.getNodeType() instanceof FunctionDefinition) { |
539 | if ("de".equals(language)) { |
540 | display = "Definition"; |
541 | } else { |
542 | display = "definition"; |
543 | } |
544 | display += " " + (data.getPredicateDefinitionNumber() + data.getFunctionDefinitionNumber()); |
545 | } else if (node.getNodeType() instanceof PredicateDefinition) { |
546 | if ("de".equals(language)) { |
547 | display = "Definition"; |
548 | } else { |
549 | display = "definition"; |
550 | } |
551 | display += " " + (data.getPredicateDefinitionNumber() + data.getFunctionDefinitionNumber()); |
552 | } else if (node.getNodeType() instanceof Rule) { |
553 | if ("de".equals(language)) { |
554 | display = "Regel"; |
555 | } else { |
556 | display = "rule"; |
557 | } |
558 | display += " " + data.getRuleNumber(); |
559 | } else { |
560 | if ("de".equals(language)) { |
561 | display = "Unbekannt " + node.getId(); |
562 | } else { |
563 | display = "unknown " + node.getId(); |
564 | } |
565 | } |
566 | return display; |
567 | } |
568 | |
569 | /** |
570 | * Set location information where are we within the original module. |
571 | * |
572 | * @param locationWithinModule Location within module. |
573 | */ |
574 | public void setLocationWithinModule(final String locationWithinModule) { |
575 | getCurrentContext().setLocationWithinModule(locationWithinModule); |
576 | getServices().getContextChecker().checkContext(getKernelQedeqBo().getQedeq(), getCurrentContext()); |
577 | } |
578 | |
579 | /** |
580 | * Get traverser for QEDEQ module. |
581 | * |
582 | * @return Traverser used. |
583 | */ |
584 | public QedeqTraverser getTraverser() { |
585 | return traverser; |
586 | } |
587 | |
588 | } |