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.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 | * This class deals with {@link org.qedeq.kernel.se.base.list.Element}s which represent a |
33 | * formula. It has methods to check those elements for being well-formed. |
34 | * |
35 | * LATER mime 20070307: here are sometimes error messages that get concatenated with |
36 | * an {@link org.qedeq.kernel.se.base.list.ElementList#getOperator()} string. Perhaps these |
37 | * strings must be translated into the original input format and a mapping must be done. |
38 | * |
39 | * @author Michael Meyling |
40 | */ |
41 | public class FormulaCheckerImpl implements Operators, FormulaBasicErrors, FormulaChecker { |
42 | |
43 | /** This class. */ |
44 | private static final Class CLASS = FormulaCheckerImpl.class; |
45 | |
46 | /** Current context during creation. */ |
47 | private ModuleContext currentContext; |
48 | |
49 | /** Existence checker for operators. */ |
50 | private ExistenceChecker existenceChecker; |
51 | |
52 | /** All exceptions that occurred during checking. */ |
53 | private LogicalCheckExceptionList exceptions; |
54 | |
55 | |
56 | /** |
57 | * Constructor. |
58 | * |
59 | */ |
60 | public FormulaCheckerImpl() { |
61 | // nothing to do |
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 | * Check if {@link Element} is a term. If there are any errors the returned list |
84 | * (which is always not <code>null</code>) has a size greater zero. |
85 | * |
86 | * @param element Check this element. |
87 | * @param context For location information. Important for locating errors. |
88 | * @param existenceChecker Existence checker for operators. |
89 | * @return Collected errors if there are any. Not <code>null</code>. |
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 | * Check if {@link Element} is a term. If there are any errors the returned list |
106 | * (which is always not <code>null</code>) has a size greater zero. |
107 | * If the existence context is known you should use |
108 | * {@link #checkTerm(Element, ModuleContext, ExistenceChecker)}. |
109 | * |
110 | * @param element Check this element. |
111 | * @param context For location information. Important for locating errors. |
112 | * @return Collected errors if there are any. Not <code>null</code>. |
113 | */ |
114 | public final LogicalCheckExceptionList checkTerm(final Element element, |
115 | final ModuleContext context) { |
116 | return checkTerm(element, context, EverythingExists.getInstance()); |
117 | } |
118 | |
119 | /** |
120 | * Is {@link Element} a formula? |
121 | * |
122 | * @param element Check this element. |
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 | // check if first argument is an atom |
183 | setLocationWithinModule(listContext + ".getElement(0)"); |
184 | if (!checkAtomFirst(list.getElement(0))) { |
185 | return; |
186 | } |
187 | |
188 | // check if rest arguments are terms |
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 | // check if predicate is known |
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 | // restore context |
220 | setLocationWithinModule(context); |
221 | Trace.end(CLASS, this, method); |
222 | } |
223 | |
224 | /** |
225 | * Check quantifier element. |
226 | * |
227 | * @param element Check this element. Must be a quantifier element. |
228 | * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no |
229 | * quantifier operator. |
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 | // save context |
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 | // check if unique existential operator could be used |
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 | // check if first argument is subject variable |
264 | setLocationWithinModule(listContext + ".getElement(" + 0 + ")"); |
265 | checkSubjectVariable(list.getElement(0)); |
266 | |
267 | // check if second argument is a formula |
268 | setLocationWithinModule(listContext + ".getElement(" + 1 + ")"); |
269 | checkFormula(list.getElement(1)); |
270 | |
271 | setLocationWithinModule(listContext); |
272 | // check if subject variable is not already bound in formula |
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 | // check if third argument is a formula |
287 | setLocationWithinModule(listContext + ".getElement(" + 2 + ")"); |
288 | checkFormula(list.getElement(2)); |
289 | |
290 | // check if subject variable is not bound in formula |
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 | // restore context |
303 | setLocationWithinModule(context); |
304 | Trace.end(CLASS, this, method); |
305 | } |
306 | |
307 | /** |
308 | * Is {@link Element} a term? |
309 | * |
310 | * @param element Check this element. |
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 | // save current context |
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 | // function constants must have at least a function name |
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 | // function variables must have at least a function name and at least one argument |
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 | // check if first argument is an atom |
346 | setLocationWithinModule(listContext + ".getElement(0)"); |
347 | if (!checkAtomFirst(list.getElement(0))) { |
348 | return; |
349 | } |
350 | |
351 | // check if all arguments are terms |
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 | // check if function is known |
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 | // check if first argument is a subject variable |
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 | // check if the second argument is a formula |
386 | setLocationWithinModule(listContext + ".getElement(" + 1 + ")"); |
387 | checkFormula(list.getElement(1)); |
388 | |
389 | // check if class operator is allowed |
390 | setLocationWithinModule(listContext); |
391 | if (!existenceChecker.classOperatorExists()) { |
392 | handleFormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN, |
393 | CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext()); |
394 | } |
395 | |
396 | // check if subject variable is not bound in formula |
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 | // restore context |
411 | setLocationWithinModule(context); |
412 | Trace.end(CLASS, this, method); |
413 | } |
414 | |
415 | /** |
416 | * Check if no bound variables are free and vice versa. |
417 | * The current context must be at the list element. |
418 | * |
419 | * @param start Start check with this list position. Beginning with 0. |
420 | * @param list List element to check. |
421 | */ |
422 | private void checkFreeAndBoundDisjunct(final int start, |
423 | final ElementList list) { |
424 | // save current context |
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 | // restore context |
450 | setLocationWithinModule(context); |
451 | } |
452 | |
453 | /** |
454 | * Check if {@link Element} is a subject variable. |
455 | * |
456 | * @param element Check this element. |
457 | * @return Is it a subject variable? |
458 | */ |
459 | private boolean checkSubjectVariable(final Element element) { |
460 | // throws LogicalCheckException { |
461 | // save current context |
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 | // check if first argument is an atom |
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 | // restore context |
485 | setLocationWithinModule(context); |
486 | return true; |
487 | } |
488 | |
489 | /** |
490 | * Check common requirements for list elements that are checked for being a term or formula. |
491 | * That includes: is the element a true list, has the operator a non zero size. |
492 | * |
493 | * @param element List element. |
494 | * @return Are the requirements fulfilled? |
495 | */ |
496 | private boolean checkList(final Element element) { |
497 | // save current context |
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 | // restore context |
531 | setLocationWithinModule(context); |
532 | return true; |
533 | } |
534 | |
535 | /** |
536 | * Check if element is an atom and has valid content. It is assumed, that this element is the |
537 | * first of a list. |
538 | * |
539 | * @param element Check this for an atom. |
540 | * @return Is the content valid? |
541 | */ |
542 | private boolean checkAtomFirst(final Element element) { |
543 | // save current context |
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()) { // TODO mime 20061126: this is special? |
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 | // restore context |
573 | setLocationWithinModule(context); |
574 | return true; |
575 | } |
576 | |
577 | /** |
578 | * Add new {@link FormulaCheckException} to exception list. |
579 | * |
580 | * @param code Error code. |
581 | * @param msg Error message. |
582 | * @param element Element with error. |
583 | * @param context Error context. |
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 | * Add new {@link TermCheckException} to exception list. |
593 | * |
594 | * @param code Error code. |
595 | * @param msg Error message. |
596 | * @param element Element with error. |
597 | * @param context Error context. |
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 | * Add new {@link ElementCheckException} to exception list. |
607 | * |
608 | * @param code Error code. |
609 | * @param msg Error message. |
610 | * @param element Element with error. |
611 | * @param context Error context. |
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 | * Set location information where are we within the original module. |
621 | * |
622 | * @param locationWithinModule Location within module. |
623 | */ |
624 | protected void setLocationWithinModule(final String locationWithinModule) { |
625 | getCurrentContext().setLocationWithinModule(locationWithinModule); |
626 | } |
627 | |
628 | /** |
629 | * Get current context within original. |
630 | * |
631 | * @return Current context. |
632 | */ |
633 | protected final ModuleContext getCurrentContext() { |
634 | return currentContext; |
635 | } |
636 | |
637 | } |