001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.wf;
017
018 import org.qedeq.base.trace.Trace;
019 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
020 import org.qedeq.kernel.bo.logic.common.FormulaChecker;
021 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
022 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
023 import org.qedeq.kernel.bo.logic.common.Operators;
024 import org.qedeq.kernel.se.base.list.Atom;
025 import org.qedeq.kernel.se.base.list.Element;
026 import org.qedeq.kernel.se.base.list.ElementList;
027 import org.qedeq.kernel.se.common.ModuleContext;
028 import org.qedeq.kernel.se.dto.list.ElementSet;
029
030
031 /**
032 * This class deals with {@link org.qedeq.kernel.se.base.list.Element}s which represent a
033 * formula. It has methods to check those elements for being well-formed.
034 *
035 * LATER mime 20070307: here are sometimes error messages that get concatenated with
036 * an {@link org.qedeq.kernel.se.base.list.ElementList#getOperator()} string. Perhaps these
037 * strings must be translated into the original input format and a mapping must be done.
038 *
039 * @author Michael Meyling
040 */
041 public class FormulaCheckerImpl implements Operators, FormulaBasicErrors, FormulaChecker {
042
043 /** This class. */
044 private static final Class CLASS = FormulaCheckerImpl.class;
045
046 /** Current context during creation. */
047 private ModuleContext currentContext;
048
049 /** Existence checker for operators. */
050 private ExistenceChecker existenceChecker;
051
052 /** All exceptions that occurred during checking. */
053 private LogicalCheckExceptionList exceptions;
054
055
056 /**
057 * Constructor.
058 *
059 */
060 public FormulaCheckerImpl() {
061 // nothing to do
062 }
063
064 public final LogicalCheckExceptionList checkFormula(final Element element,
065 final ModuleContext context, final ExistenceChecker existenceChecker) {
066 if (existenceChecker.identityOperatorExists()
067 && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
068 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
069 }
070 this.existenceChecker = existenceChecker;
071 currentContext = new ModuleContext(context);
072 exceptions = new LogicalCheckExceptionList();
073 checkFormula(element);
074 return exceptions;
075 }
076
077 public final LogicalCheckExceptionList checkFormula(final Element element,
078 final ModuleContext context) {
079 return checkFormula(element, context, EverythingExists.getInstance());
080 }
081
082 /**
083 * Check if {@link Element} is a term. If there are any errors the returned list
084 * (which is always not <code>null</code>) has a size greater zero.
085 *
086 * @param element Check this element.
087 * @param context For location information. Important for locating errors.
088 * @param existenceChecker Existence checker for operators.
089 * @return Collected errors if there are any. Not <code>null</code>.
090 */
091 public final LogicalCheckExceptionList checkTerm(final Element element,
092 final ModuleContext context, final ExistenceChecker existenceChecker) {
093 if (existenceChecker.identityOperatorExists()
094 && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
095 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
096 }
097 this.existenceChecker = existenceChecker;
098 currentContext = new ModuleContext(context);
099 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 }
|