View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">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 }