1
2
3
4
5
6
7
8
9
10
11
12
13
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
51
52
53
54
55 public abstract class ControlVisitor extends AbstractModuleVisitor {
56
57
58 private static final Class CLASS = ControlVisitor.class;
59
60
61 private final Service service;
62
63
64 private final KernelQedeqBo prop;
65
66
67 private InternalModuleServiceCall call;
68
69
70 private final QedeqNotNullTraverser traverser;
71
72
73 private SourceFileExceptionList errorList;
74
75
76 private SourceFileExceptionList warningList;
77
78
79 private boolean interrupted;
80
81
82
83
84
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
96
97
98
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
110
111
112
113 public KernelQedeqBo getKernelQedeqBo() {
114 return this.prop;
115 }
116
117
118
119
120
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
132
133
134
135
136
137
138
139
140
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;
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
172
173
174
175
176 public ModuleContext getCurrentContext() {
177 return this.traverser.getCurrentContext();
178 }
179
180
181
182
183
184
185 protected void addError(final ModuleDataException me) {
186 addError(prop.createSourceFileException(getService(), me));
187 }
188
189
190
191
192
193
194 protected void addError(final SourceFileException sf) {
195 errorList.add(sf);
196 }
197
198
199
200
201
202
203 public SourceFileExceptionList getErrorList() {
204 return errorList;
205 }
206
207
208
209
210
211
212 public boolean hasErrors() {
213 return errorList.size() > 0;
214 }
215
216
217
218
219
220
221 public boolean hasNoErrors() {
222 return !hasErrors();
223 }
224
225
226
227
228
229
230 protected void addWarning(final ModuleDataException me) {
231
232
233
234
235
236 addWarning(prop.createSourceFileException(getService(), me));
237 }
238
239
240
241
242
243
244 private void addWarning(final SourceFileException sf) {
245 warningList.add(sf);
246 }
247
248
249
250
251
252
253 public SourceFileExceptionList getWarningList() {
254 return warningList;
255 }
256
257
258
259
260
261
262 protected void setBlocked(final boolean blocked) {
263 traverser.setBlocked(blocked);
264 }
265
266
267
268
269
270
271 public boolean getBlocked() {
272 return traverser.getBlocked();
273 }
274
275
276
277
278
279
280 public InternalModuleServiceCall getInternalServiceCall() {
281 return call;
282 }
283
284
285
286
287
288
289 public Service getService() {
290 return service;
291 }
292
293
294
295
296
297
298 public String getLocationDescription() {
299 return traverser.getLocationDescription();
300 }
301
302
303
304
305
306
307 public double getVisitPercentage() {
308 return traverser.getVisitPercentage();
309 }
310
311
312
313
314
315
316 public QedeqNumbers getCurrentNumbers() {
317 return traverser.getCurrentNumbers();
318 }
319
320
321
322
323
324
325
326 public RuleKey getLocalRuleKey(final String name) {
327 return traverser.getLocalRuleKey(name);
328 }
329
330
331
332
333
334
335 public InternalKernelServices getServices() {
336 return prop.getKernelServices();
337 }
338
339
340
341
342
343
344 public boolean getInterrupted() {
345 return interrupted;
346 }
347
348
349
350
351
352
353
354
355
356
357 public Reference getReference(final String reference, final ModuleContext context,
358 final boolean addWarning, final boolean addError) {
359
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
381 if (node != null && node.isProofLineLabel(reference)) {
382 return new DefaultReference(node, null, "", node, node.getNodeVo().getId(), "", reference);
383 }
384
385 if (getKernelQedeqBo().getLabels().isNode(reference)) {
386 return new DefaultReference(node, null, "", getKernelQedeqBo().getLabels().getNode(
387 reference), reference, "", "");
388 }
389
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 = "";
398 String nodeLabel = "";
399 String lineLabel = "";
400 String subLabel = "";
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
511
512
513
514
515
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
571
572
573
574 public void setLocationWithinModule(final String locationWithinModule) {
575 getCurrentContext().setLocationWithinModule(locationWithinModule);
576 getServices().getContextChecker().checkContext(getKernelQedeqBo().getQedeq(), getCurrentContext());
577 }
578
579
580
581
582
583
584 public QedeqTraverser getTraverser() {
585 return traverser;
586 }
587
588 }