1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.bo.logic.wf;
17
18 import org.qedeq.base.trace.Trace;
19 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
20 import org.qedeq.kernel.bo.logic.common.FormulaChecker;
21 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
22 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
23 import org.qedeq.kernel.bo.logic.common.Operators;
24 import org.qedeq.kernel.se.base.list.Atom;
25 import org.qedeq.kernel.se.base.list.Element;
26 import org.qedeq.kernel.se.base.list.ElementList;
27 import org.qedeq.kernel.se.common.ModuleContext;
28 import org.qedeq.kernel.se.dto.list.ElementSet;
29
30
31
32
33
34
35
36
37
38
39
40
41 public class FormulaCheckerImpl implements Operators, FormulaBasicErrors, FormulaChecker {
42
43
44 private static final Class CLASS = FormulaCheckerImpl.class;
45
46
47 private ModuleContext currentContext;
48
49
50 private ExistenceChecker existenceChecker;
51
52
53 private LogicalCheckExceptionList exceptions;
54
55
56
57
58
59
60 public FormulaCheckerImpl() {
61
62 }
63
64 public final LogicalCheckExceptionList checkFormula(final Element element,
65 final ModuleContext context, final ExistenceChecker existenceChecker) {
66 if (existenceChecker.identityOperatorExists()
67 && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
68 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
69 }
70 this.existenceChecker = existenceChecker;
71 currentContext = new ModuleContext(context);
72 exceptions = new LogicalCheckExceptionList();
73 checkFormula(element);
74 return exceptions;
75 }
76
77 public final LogicalCheckExceptionList checkFormula(final Element element,
78 final ModuleContext context) {
79 return checkFormula(element, context, EverythingExists.getInstance());
80 }
81
82
83
84
85
86
87
88
89
90
91 public final LogicalCheckExceptionList checkTerm(final Element element,
92 final ModuleContext context, final ExistenceChecker existenceChecker) {
93 if (existenceChecker.identityOperatorExists()
94 && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
95 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
96 }
97 this.existenceChecker = existenceChecker;
98 currentContext = new ModuleContext(context);
99 exceptions = new LogicalCheckExceptionList();
100 checkTerm(element);
101 return exceptions;
102 }
103
104
105
106
107
108
109
110
111
112
113
114 public final LogicalCheckExceptionList checkTerm(final Element element,
115 final ModuleContext context) {
116 return checkTerm(element, context, EverythingExists.getInstance());
117 }
118
119
120
121
122
123
124 private final void checkFormula(final Element element) {
125 final String method = "checkFormula";
126 Trace.begin(CLASS, this, method);
127 Trace.param(CLASS, this, method, "element", element);
128 final String context = getCurrentContext().getLocationWithinModule();
129 Trace.param(CLASS, this, method, "context", context);
130 if (!checkList(element)) {
131 return;
132 }
133 final ElementList list = element.getList();
134 final String listContext = context + ".getList()";
135 setLocationWithinModule(listContext);
136 final String operator = list.getOperator();
137 if (operator.equals(CONJUNCTION_OPERATOR)
138 || operator.equals(DISJUNCTION_OPERATOR)
139 || operator.equals(IMPLICATION_OPERATOR)
140 || operator.equals(EQUIVALENCE_OPERATOR)) {
141 Trace.trace(CLASS, this, method,
142 "one of (and, or, implication, equivalence) operator found");
143 if (list.size() <= 1) {
144 handleFormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
145 MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
146 + operator + "\"", element, getCurrentContext());
147 return;
148 }
149 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
150 handleFormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
151 EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
152 + operator + "\"", element, getCurrentContext());
153 return;
154 }
155 for (int i = 0; i < list.size(); i++) {
156 setLocationWithinModule(listContext + ".getElement(" + i + ")");
157 checkFormula(list.getElement(i));
158 }
159 setLocationWithinModule(listContext);
160 checkFreeAndBoundDisjunct(0, list);
161 } else if (operator.equals(NEGATION_OPERATOR)) {
162 Trace.trace(CLASS, this, method, "negation operator found");
163 setLocationWithinModule(listContext);
164 if (list.size() != 1) {
165 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
166 EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
167 element, getCurrentContext());
168 return;
169 }
170 setLocationWithinModule(listContext + ".getElement(0)");
171 checkFormula(list.getElement(0));
172 } else if (operator.equals(PREDICATE_VARIABLE)
173 || operator.equals(PREDICATE_CONSTANT)) {
174 Trace.trace(CLASS, this, method, "predicate operator found");
175 setLocationWithinModule(listContext);
176 if (list.size() < 1) {
177 handleFormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
178 AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
179 element, getCurrentContext());
180 return;
181 }
182
183 setLocationWithinModule(listContext + ".getElement(0)");
184 if (!checkAtomFirst(list.getElement(0))) {
185 return;
186 }
187
188
189 for (int i = 1; i < list.size(); i++) {
190 setLocationWithinModule(listContext + ".getElement(" + i + ")");
191 checkTerm(list.getElement(i));
192 }
193
194 setLocationWithinModule(listContext);
195 checkFreeAndBoundDisjunct(1, list);
196
197
198 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
199 list.getElement(0).getAtom().getString(), list.size() - 1)) {
200 setLocationWithinModule(listContext + ".getElement(0)");
201 handleFormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
202 UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
203 + list.getElement(0).getAtom().getString() + "\" [" + (list.size() - 1) + "]",
204 element, getCurrentContext());
205 }
206
207 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
208 || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
209 || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
210 Trace.trace(CLASS, this, method, "quantifier found");
211 setLocationWithinModule(context);
212 checkQuantifier(element);
213 } else {
214 setLocationWithinModule(listContext + ".getOperator()");
215 handleFormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
216 UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
217 element, getCurrentContext());
218 }
219
220 setLocationWithinModule(context);
221 Trace.end(CLASS, this, method);
222 }
223
224
225
226
227
228
229
230
231 private void checkQuantifier(final Element element) {
232 final String method = "checkQuantifier";
233 Trace.begin(CLASS, this, method);
234 Trace.param(CLASS, this, method, "element", element);
235
236 final String context = getCurrentContext().getLocationWithinModule();
237 Trace.param(CLASS, this, method, "context", context);
238 checkList(element);
239 final ElementList list = element.getList();
240 final String listContext = context + ".getList()";
241 setLocationWithinModule(listContext);
242 final String operator = list.getOperator();
243 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
244 && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
245 && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
246 throw new IllegalArgumentException("quantifier element expected but found: "
247 + element.toString());
248 }
249 if (list.size() < 2 || list.size() > 3) {
250 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
251 EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
252 return;
253 }
254
255
256 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
257 && !existenceChecker.identityOperatorExists()) {
258 setLocationWithinModule(listContext + ".getOperator()");
259 handleFormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
260 EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
261 }
262
263
264 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
265 checkSubjectVariable(list.getElement(0));
266
267
268 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
269 checkFormula(list.getElement(1));
270
271 setLocationWithinModule(listContext);
272
273 if (FormulaUtility.getBoundSubjectVariables(list.getElement(1)).contains(
274 list.getElement(0))) {
275 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
276 SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
277 getCurrentContext());
278 }
279 if (list.size() > 3) {
280 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
281 EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
282 getCurrentContext());
283 return;
284 }
285 if (list.size() > 2) {
286
287 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
288 checkFormula(list.getElement(2));
289
290
291 setLocationWithinModule(listContext);
292 if (FormulaUtility.getBoundSubjectVariables(list.getElement(2)).contains(
293 list.getElement(0))) {
294 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
295 SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
296 getCurrentContext());
297 return;
298 }
299 setLocationWithinModule(listContext);
300 checkFreeAndBoundDisjunct(1, list);
301 }
302
303 setLocationWithinModule(context);
304 Trace.end(CLASS, this, method);
305 }
306
307
308
309
310
311
312 private void checkTerm(final Element element) {
313 final String method = "checkTerm";
314 Trace.begin(CLASS, this, method);
315 Trace.param(CLASS, this, method, "element", element);
316
317 final String context = getCurrentContext().getLocationWithinModule();
318 Trace.param(CLASS, this, method, "context", context);
319 if (!checkList(element)) {
320 return;
321 }
322 final ElementList list = element.getList();
323 final String listContext = context + ".getList()";
324 setLocationWithinModule(listContext);
325 final String operator = list.getOperator();
326 if (operator.equals(SUBJECT_VARIABLE)) {
327 checkSubjectVariable(element);
328 } else if (operator.equals(FUNCTION_CONSTANT)
329 || operator.equals(FUNCTION_VARIABLE)) {
330
331
332 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
333 handleTermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
334 AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
335 return;
336 }
337
338
339 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
340 handleTermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
341 MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
342 return;
343 }
344
345
346 setLocationWithinModule(listContext + ".getElement(0)");
347 if (!checkAtomFirst(list.getElement(0))) {
348 return;
349 }
350
351
352 setLocationWithinModule(listContext);
353 for (int i = 1; i < list.size(); i++) {
354 setLocationWithinModule(listContext + ".getElement(" + i + ")");
355 checkTerm(list.getElement(i));
356 }
357
358 setLocationWithinModule(listContext);
359 checkFreeAndBoundDisjunct(1, list);
360
361
362 setLocationWithinModule(listContext);
363 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
364 list.getElement(0).getAtom().getString(), list.size() - 1)) {
365 handleFormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
366 UNKNOWN_FUNCTION_CONSTANT_TEXT + "\""
367 + list.getElement(0).getAtom().getString() + "\"", element,
368 getCurrentContext());
369 }
370
371 } else if (operator.equals(CLASS_OP)) {
372
373 if (list.size() != 2) {
374 handleTermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
375 EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
376 return;
377 }
378
379 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
380 if (!FormulaUtility.isSubjectVariable(list.getElement(0))) {
381 handleTermCheckException(SUBJECT_VARIABLE_EXPECTED,
382 SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
383 }
384
385
386 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
387 checkFormula(list.getElement(1));
388
389
390 setLocationWithinModule(listContext);
391 if (!existenceChecker.classOperatorExists()) {
392 handleFormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
393 CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
394 }
395
396
397 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
398 if (FormulaUtility.getBoundSubjectVariables(list.getElement(1)).contains(
399 list.getElement(0))) {
400 handleTermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
401 SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
402 getCurrentContext());
403 }
404
405 } else {
406 setLocationWithinModule(listContext + ".getOperator()");
407 handleTermCheckException(UNKNOWN_TERM_OPERATOR,
408 UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
409 }
410
411 setLocationWithinModule(context);
412 Trace.end(CLASS, this, method);
413 }
414
415
416
417
418
419
420
421
422 private void checkFreeAndBoundDisjunct(final int start,
423 final ElementList list) {
424
425 final String context = getCurrentContext().getLocationWithinModule();
426 final ElementSet free = new ElementSet();
427 final ElementSet bound = new ElementSet();
428 for (int i = start; i < list.size(); i++) {
429 setLocationWithinModule(context + ".getElement(" + i + ")");
430 final ElementSet newFree
431 = FormulaUtility.getFreeSubjectVariables(list.getElement(i));
432 final ElementSet newBound
433 = FormulaUtility.getBoundSubjectVariables(list.getElement(i));
434 final ElementSet interBound = newFree.newIntersection(bound);
435 if (!interBound.isEmpty()) {
436 handleFormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
437 FREE_VARIABLE_ALREADY_BOUND_TEXT
438 + interBound, list.getElement(i), getCurrentContext());
439 }
440 final ElementSet interFree = newBound.newIntersection(free);
441 if (!interFree.isEmpty()) {
442 handleFormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
443 BOUND_VARIABLE_ALREADY_FREE_TEXT
444 + interFree, list.getElement(i), getCurrentContext());
445 }
446 bound.union(newBound);
447 free.union(newFree);
448 }
449
450 setLocationWithinModule(context);
451 }
452
453
454
455
456
457
458
459 private boolean checkSubjectVariable(final Element element) {
460
461
462 final String context = getCurrentContext().getLocationWithinModule();
463 if (!checkList(element)) {
464 return false;
465 }
466 setLocationWithinModule(context + ".getList()");
467 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
468 if (element.getList().size() != 1) {
469 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
470 EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
471 return false;
472 }
473
474 setLocationWithinModule(context + ".getList().getElement(0)");
475 if (checkAtomFirst(element.getList().getElement(0))) {
476 return false;
477 }
478 } else {
479 setLocationWithinModule(context + ".getList().getOperator()");
480 handleFormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
481 SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
482 return false;
483 }
484
485 setLocationWithinModule(context);
486 return true;
487 }
488
489
490
491
492
493
494
495
496 private boolean checkList(final Element element) {
497
498 final String context = getCurrentContext().getLocationWithinModule();
499 if (element == null) {
500 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
501 ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
502 return false;
503 }
504 if (!element.isList()) {
505 handleElementCheckException(LIST_EXPECTED,
506 LIST_EXPECTED_TEXT, element, getCurrentContext());
507 return false;
508 }
509 final ElementList list = element.getList();
510 setLocationWithinModule(context + ".getList()");
511 if (list == null) {
512 handleElementCheckException(LIST_MUST_NOT_BE_NULL,
513 LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
514 return false;
515 }
516 final String operator = list.getOperator();
517 setLocationWithinModule(context + ".getList().getOperator()");
518 if (operator == null) {
519 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
520 OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT , element,
521 getCurrentContext());
522 return false;
523 }
524 if (operator.length() == 0) {
525 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
526 OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
527 + operator + "\"", element, getCurrentContext());
528 return false;
529 }
530
531 setLocationWithinModule(context);
532 return true;
533 }
534
535
536
537
538
539
540
541
542 private boolean checkAtomFirst(final Element element) {
543
544 final String context = getCurrentContext().getLocationWithinModule();
545 if (element == null) {
546 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
547 ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
548 return false;
549 }
550 if (!element.isAtom()) {
551 handleElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
552 FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
553 return false;
554 }
555 final Atom atom = element.getAtom();
556 setLocationWithinModule(context + ".getAtom()");
557 if (atom == null) {
558 handleElementCheckException(ATOM_MUST_NOT_BE_NULL,
559 ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
560 return false;
561 }
562 if (atom.getString() == null) {
563 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
564 ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
565 return false;
566 }
567 if (atom.getString().length() == 0) {
568 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
569 ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
570 return false;
571 }
572
573 setLocationWithinModule(context);
574 return true;
575 }
576
577
578
579
580
581
582
583
584
585 private void handleFormulaCheckException(final int code, final String msg,
586 final Element element, final ModuleContext context) {
587 final FormulaCheckException ex = new FormulaCheckException(code, msg, element, context);
588 exceptions.add(ex);
589 }
590
591
592
593
594
595
596
597
598
599 private void handleTermCheckException(final int code, final String msg,
600 final Element element, final ModuleContext context) {
601 final TermCheckException ex = new TermCheckException(code, msg, element, context);
602 exceptions.add(ex);
603 }
604
605
606
607
608
609
610
611
612
613 private void handleElementCheckException(final int code, final String msg,
614 final Element element, final ModuleContext context) {
615 final ElementCheckException ex = new ElementCheckException(code, msg, element, context);
616 exceptions.add(ex);
617 }
618
619
620
621
622
623
624 protected void setLocationWithinModule(final String locationWithinModule) {
625 getCurrentContext().setLocationWithinModule(locationWithinModule);
626 }
627
628
629
630
631
632
633 protected final ModuleContext getCurrentContext() {
634 return currentContext;
635 }
636
637 }