001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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 }
062
063 public final LogicalCheckExceptionList checkFormula(final Element element,
064 final ModuleContext context, final ExistenceChecker existenceChecker) {
065 if (existenceChecker.identityOperatorExists()
066 && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
067 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
068 }
069 this.existenceChecker = existenceChecker;
070 currentContext = new ModuleContext(context);
071 exceptions = new LogicalCheckExceptionList();
072 checkFormula(element);
073 return exceptions;
074 }
075
076 public final LogicalCheckExceptionList checkFormula(final Element element,
077 final ModuleContext context) {
078 return checkFormula(element, context, EverythingExists.getInstance());
079 }
080
081 /**
082 * Check if {@link Element} is a term. If there are any errors the returned list
083 * (which is always not <code>null</code>) has a size greater zero.
084 *
085 * @param element Check this element.
086 * @param context For location information. Important for locating errors.
087 * @param existenceChecker Existence checker for operators.
088 * @return Collected errors if there are any. Not <code>null</code>.
089 */
090 public final LogicalCheckExceptionList checkTerm(final Element element,
091 final ModuleContext context, final ExistenceChecker existenceChecker) {
092 if (existenceChecker.identityOperatorExists()
093 && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
094 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
095 }
096 this.existenceChecker = existenceChecker;
097 currentContext = new ModuleContext(context);
098 exceptions = new LogicalCheckExceptionList();
099 checkTerm(element);
100 return exceptions;
101 }
102
103 /**
104 * Check if {@link Element} is a term. If there are any errors the returned list
105 * (which is always not <code>null</code>) has a size greater zero.
106 * If the existence context is known you should use
107 * {@link #checkTerm(Element, ModuleContext, ExistenceChecker)}.
108 *
109 * @param element Check this element.
110 * @param context For location information. Important for locating errors.
111 * @return Collected errors if there are any. Not <code>null</code>.
112 */
113 public final LogicalCheckExceptionList checkTerm(final Element element,
114 final ModuleContext context) {
115 return checkTerm(element, context, EverythingExists.getInstance());
116 }
117
118 /**
119 * Is {@link Element} a formula?
120 *
121 * @param element Check this element.
122 */
123 private final void checkFormula(final Element element) {
124 final String method = "checkFormula";
125 Trace.begin(CLASS, this, method);
126 Trace.param(CLASS, this, method, "element", element);
127 final String context = getCurrentContext().getLocationWithinModule();
128 Trace.param(CLASS, this, method, "context", context);
129 if (!checkList(element)) {
130 return;
131 }
132 final ElementList list = element.getList();
133 final String listContext = context + ".getList()";
134 setLocationWithinModule(listContext);
135 final String operator = list.getOperator();
136 if (operator.equals(CONJUNCTION_OPERATOR)
137 || operator.equals(DISJUNCTION_OPERATOR)
138 || operator.equals(IMPLICATION_OPERATOR)
139 || operator.equals(EQUIVALENCE_OPERATOR)) {
140 Trace.trace(CLASS, this, method,
141 "one of (and, or, implication, equivalence) operator found");
142 if (list.size() <= 1) {
143 handleFormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
144 MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
145 + operator + "\"", element, getCurrentContext());
146 return;
147 }
148 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
149 handleFormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
150 EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
151 + operator + "\"", element, getCurrentContext());
152 return;
153 }
154 for (int i = 0; i < list.size(); i++) {
155 setLocationWithinModule(listContext + ".getElement(" + i + ")");
156 checkFormula(list.getElement(i));
157 }
158 setLocationWithinModule(listContext);
159 checkFreeAndBoundDisjunct(0, list);
160 } else if (operator.equals(NEGATION_OPERATOR)) {
161 Trace.trace(CLASS, this, method, "negation operator found");
162 setLocationWithinModule(listContext);
163 if (list.size() != 1) {
164 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
165 EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
166 element, getCurrentContext());
167 return;
168 }
169 setLocationWithinModule(listContext + ".getElement(0)");
170 checkFormula(list.getElement(0));
171 } else if (operator.equals(PREDICATE_VARIABLE)
172 || operator.equals(PREDICATE_CONSTANT)) {
173 Trace.trace(CLASS, this, method, "predicate operator found");
174 setLocationWithinModule(listContext);
175 if (list.size() < 1) {
176 handleFormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
177 AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
178 element, getCurrentContext());
179 return;
180 }
181 // check if first argument is an atom
182 setLocationWithinModule(listContext + ".getElement(0)");
183 if (!checkAtomFirst(list.getElement(0))) {
184 return;
185 }
186
187 // check if rest arguments are terms
188 for (int i = 1; i < list.size(); i++) {
189 setLocationWithinModule(listContext + ".getElement(" + i + ")");
190 checkTerm(list.getElement(i));
191 }
192
193 setLocationWithinModule(listContext);
194 checkFreeAndBoundDisjunct(1, list);
195
196 // check if predicate is known
197 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
198 list.getElement(0).getAtom().getString(), list.size() - 1)) {
199 setLocationWithinModule(listContext + ".getElement(0)");
200 handleFormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
201 UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
202 + list.getElement(0).getAtom().getString() + "\" [" + (list.size() - 1) + "]",
203 element, getCurrentContext());
204 }
205
206 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
207 || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
208 || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
209 Trace.trace(CLASS, this, method, "quantifier found");
210 setLocationWithinModule(context);
211 checkQuantifier(element);
212 } else {
213 setLocationWithinModule(listContext + ".getOperator()");
214 handleFormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
215 UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
216 element, getCurrentContext());
217 }
218 // restore context
219 setLocationWithinModule(context);
220 Trace.end(CLASS, this, method);
221 }
222
223 /**
224 * Check quantifier element.
225 *
226 * @param element Check this element. Must be a quantifier element.
227 * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
228 * quantifier operator.
229 */
230 private void checkQuantifier(final Element element) {
231 final String method = "checkQuantifier";
232 Trace.begin(CLASS, this, method);
233 Trace.param(CLASS, this, method, "element", element);
234 // save context
235 final String context = getCurrentContext().getLocationWithinModule();
236 Trace.param(CLASS, this, method, "context", context);
237 checkList(element);
238 final ElementList list = element.getList();
239 final String listContext = context + ".getList()";
240 setLocationWithinModule(listContext);
241 final String operator = list.getOperator();
242 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
243 && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
244 && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
245 throw new IllegalArgumentException("quantifier element expected but found: "
246 + element.toString());
247 }
248 if (list.size() < 2 || list.size() > 3) {
249 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
250 EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
251 return;
252 }
253
254 // check if unique existential operator could be used
255 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
256 && !existenceChecker.identityOperatorExists()) {
257 setLocationWithinModule(listContext + ".getOperator()");
258 handleFormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
259 EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
260 }
261
262 // check if first argument is subject variable
263 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
264 checkSubjectVariable(list.getElement(0));
265
266 // check if second argument is a formula
267 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
268 checkFormula(list.getElement(1));
269
270 setLocationWithinModule(listContext);
271 // check if subject variable is not already bound in formula
272 if (FormulaUtility.getBoundSubjectVariables(list.getElement(1)).contains(
273 list.getElement(0))) {
274 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
275 SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
276 getCurrentContext());
277 }
278 if (list.size() > 3) {
279 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
280 EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
281 getCurrentContext());
282 return;
283 }
284 if (list.size() > 2) {
285 // check if third argument is a formula
286 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
287 checkFormula(list.getElement(2));
288
289 // check if subject variable is not bound in formula
290 setLocationWithinModule(listContext);
291 if (FormulaUtility.getBoundSubjectVariables(list.getElement(2)).contains(
292 list.getElement(0))) {
293 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
294 SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
295 getCurrentContext());
296 return;
297 }
298 setLocationWithinModule(listContext);
299 checkFreeAndBoundDisjunct(1, list);
300 }
301 // restore context
302 setLocationWithinModule(context);
303 Trace.end(CLASS, this, method);
304 }
305
306 /**
307 * Is {@link Element} a term?
308 *
309 * @param element Check this element.
310 */
311 private void checkTerm(final Element element) {
312 final String method = "checkTerm";
313 Trace.begin(CLASS, this, method);
314 Trace.param(CLASS, this, method, "element", element);
315 // save current context
316 final String context = getCurrentContext().getLocationWithinModule();
317 Trace.param(CLASS, this, method, "context", context);
318 if (!checkList(element)) {
319 return;
320 }
321 final ElementList list = element.getList();
322 final String listContext = context + ".getList()";
323 setLocationWithinModule(listContext);
324 final String operator = list.getOperator();
325 if (operator.equals(SUBJECT_VARIABLE)) {
326 checkSubjectVariable(element);
327 } else if (operator.equals(FUNCTION_CONSTANT)
328 || operator.equals(FUNCTION_VARIABLE)) {
329
330 // function constants must have at least a function name
331 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
332 handleTermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
333 AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
334 return;
335 }
336
337 // function variables must have at least a function name and at least one argument
338 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
339 handleTermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
340 MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
341 return;
342 }
343
344 // check if first argument is an atom
345 setLocationWithinModule(listContext + ".getElement(0)");
346 if (!checkAtomFirst(list.getElement(0))) {
347 return;
348 }
349
350 // check if all arguments are terms
351 setLocationWithinModule(listContext);
352 for (int i = 1; i < list.size(); i++) {
353 setLocationWithinModule(listContext + ".getElement(" + i + ")");
354 checkTerm(list.getElement(i));
355 }
356
357 setLocationWithinModule(listContext);
358 checkFreeAndBoundDisjunct(1, list);
359
360 // check if function is known
361 setLocationWithinModule(listContext);
362 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
363 list.getElement(0).getAtom().getString(), list.size() - 1)) {
364 handleFormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
365 UNKNOWN_FUNCTION_CONSTANT_TEXT + "\""
366 + list.getElement(0).getAtom().getString() + "\"", element,
367 getCurrentContext());
368 }
369
370 } else if (operator.equals(CLASS_OP)) {
371
372 if (list.size() != 2) {
373 handleTermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
374 EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
375 return;
376 }
377 // check if first argument is a subject variable
378 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
379 if (!FormulaUtility.isSubjectVariable(list.getElement(0))) {
380 handleTermCheckException(SUBJECT_VARIABLE_EXPECTED,
381 SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
382 }
383
384 // check if the second argument is a formula
385 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
386 checkFormula(list.getElement(1));
387
388 // check if class operator is allowed
389 setLocationWithinModule(listContext);
390 if (!existenceChecker.classOperatorExists()) {
391 handleFormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
392 CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
393 }
394
395 // check if subject variable is not bound in formula
396 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
397 if (FormulaUtility.getBoundSubjectVariables(list.getElement(1)).contains(
398 list.getElement(0))) {
399 handleTermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
400 SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
401 getCurrentContext());
402 }
403
404 } else {
405 setLocationWithinModule(listContext + ".getOperator()");
406 handleTermCheckException(UNKNOWN_TERM_OPERATOR,
407 UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
408 }
409 // restore context
410 setLocationWithinModule(context);
411 Trace.end(CLASS, this, method);
412 }
413
414 /**
415 * Check if no bound variables are free and vice versa.
416 * The current context must be at the list element.
417 *
418 * @param start Start check with this list position. Beginning with 0.
419 * @param list List element to check.
420 */
421 private void checkFreeAndBoundDisjunct(final int start,
422 final ElementList list) {
423 // save current context
424 final String context = getCurrentContext().getLocationWithinModule();
425 final ElementSet free = new ElementSet();
426 final ElementSet bound = new ElementSet();
427 for (int i = start; i < list.size(); i++) {
428 setLocationWithinModule(context + ".getElement(" + i + ")");
429 final ElementSet newFree
430 = FormulaUtility.getFreeSubjectVariables(list.getElement(i));
431 final ElementSet newBound
432 = FormulaUtility.getBoundSubjectVariables(list.getElement(i));
433 final ElementSet interBound = newFree.newIntersection(bound);
434 if (!interBound.isEmpty()) {
435 handleFormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
436 FREE_VARIABLE_ALREADY_BOUND_TEXT
437 + interBound, list.getElement(i), getCurrentContext());
438 }
439 final ElementSet interFree = newBound.newIntersection(free);
440 if (!interFree.isEmpty()) {
441 handleFormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
442 BOUND_VARIABLE_ALREADY_FREE_TEXT
443 + interFree, list.getElement(i), getCurrentContext());
444 }
445 bound.union(newBound);
446 free.union(newFree);
447 }
448 // restore context
449 setLocationWithinModule(context);
450 }
451
452 /**
453 * Check if {@link Element} is a subject variable.
454 *
455 * @param element Check this element.
456 * @return Is it a subject variable?
457 */
458 private boolean checkSubjectVariable(final Element element) {
459 // throws LogicalCheckException {
460 // save current context
461 final String context = getCurrentContext().getLocationWithinModule();
462 if (!checkList(element)) {
463 return false;
464 }
465 setLocationWithinModule(context + ".getList()");
466 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
467 if (element.getList().size() != 1) {
468 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
469 EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
470 return false;
471 }
472 // check if first argument is an atom
473 setLocationWithinModule(context + ".getList().getElement(0)");
474 if (checkAtomFirst(element.getList().getElement(0))) {
475 return false;
476 }
477 } else {
478 setLocationWithinModule(context + ".getList().getOperator()");
479 handleFormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
480 SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
481 return false;
482 }
483 // restore context
484 setLocationWithinModule(context);
485 return true;
486 }
487
488 /**
489 * Check common requirements for list elements that are checked for being a term or formula.
490 * That includes: is the element a true list, has the operator a non zero size.
491 *
492 * @param element List element.
493 * @return Are the requirements fulfilled?
494 */
495 private boolean checkList(final Element element) {
496 // save current context
497 final String context = getCurrentContext().getLocationWithinModule();
498 if (element == null) {
499 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
500 ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
501 return false;
502 }
503 if (!element.isList()) {
504 handleElementCheckException(LIST_EXPECTED,
505 LIST_EXPECTED_TEXT, element, getCurrentContext());
506 return false;
507 }
508 final ElementList list = element.getList();
509 setLocationWithinModule(context + ".getList()");
510 if (list == null) {
511 handleElementCheckException(LIST_MUST_NOT_BE_NULL,
512 LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
513 return false;
514 }
515 final String operator = list.getOperator();
516 setLocationWithinModule(context + ".getList().getOperator()");
517 if (operator == null) {
518 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
519 OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT , element,
520 getCurrentContext());
521 return false;
522 }
523 if (operator.length() == 0) {
524 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
525 OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
526 + operator + "\"", element, getCurrentContext());
527 return false;
528 }
529 // restore context
530 setLocationWithinModule(context);
531 return true;
532 }
533
534 /**
535 * Check if element is an atom and has valid content. It is assumed, that this element is the
536 * first of a list.
537 *
538 * @param element Check this for an atom.
539 * @return Is the content valid?
540 */
541 private boolean checkAtomFirst(final Element element) {
542 // save current context
543 final String context = getCurrentContext().getLocationWithinModule();
544 if (element == null) {
545 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
546 ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
547 return false;
548 }
549 if (!element.isAtom()) { // TODO mime 20061126: this is special?
550 handleElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
551 FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
552 return false;
553 }
554 final Atom atom = element.getAtom();
555 setLocationWithinModule(context + ".getAtom()");
556 if (atom == null) {
557 handleElementCheckException(ATOM_MUST_NOT_BE_NULL,
558 ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
559 return false;
560 }
561 if (atom.getString() == null) {
562 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
563 ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
564 return false;
565 }
566 if (atom.getString().length() == 0) {
567 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
568 ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
569 return false;
570 }
571 // restore context
572 setLocationWithinModule(context);
573 return true;
574 }
575
576 /**
577 * Add new {@link FormulaCheckException} to exception list.
578 *
579 * @param code Error code.
580 * @param msg Error message.
581 * @param element Element with error.
582 * @param context Error context.
583 */
584 private void handleFormulaCheckException(final int code, final String msg,
585 final Element element, final ModuleContext context) {
586 final FormulaCheckException ex = new FormulaCheckException(code, msg, element, context);
587 exceptions.add(ex);
588 }
589
590 /**
591 * Add new {@link TermCheckException} to exception list.
592 *
593 * @param code Error code.
594 * @param msg Error message.
595 * @param element Element with error.
596 * @param context Error context.
597 */
598 private void handleTermCheckException(final int code, final String msg,
599 final Element element, final ModuleContext context) {
600 final TermCheckException ex = new TermCheckException(code, msg, element, context);
601 exceptions.add(ex);
602 }
603
604 /**
605 * Add new {@link ElementCheckException} to exception list.
606 *
607 * @param code Error code.
608 * @param msg Error message.
609 * @param element Element with error.
610 * @param context Error context.
611 */
612 private void handleElementCheckException(final int code, final String msg,
613 final Element element, final ModuleContext context) {
614 final ElementCheckException ex = new ElementCheckException(code, msg, element, context);
615 exceptions.add(ex);
616 }
617
618 /**
619 * Set location information where are we within the original module.
620 *
621 * @param locationWithinModule Location within module.
622 */
623 protected void setLocationWithinModule(final String locationWithinModule) {
624 getCurrentContext().setLocationWithinModule(locationWithinModule);
625 }
626
627 /**
628 * Get current context within original.
629 *
630 * @return Current context.
631 */
632 protected final ModuleContext getCurrentContext() {
633 return currentContext;
634 }
635
636 }
|