org.qedeq.kernel.bo.logic.wf
Class FormulaCheckerImpl

java.lang.Object
  org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl

All Implemented Interfaces:

FormulaChecker, Operators, FormulaBasicErrors, ErrorCodes

public class FormulaCheckerImpl
extends java.lang.Object
implements Operators, FormulaBasicErrors, FormulaChecker

This class deals with Elements which represent a formula. It has methods to check those elements for being well-formed. LATER mime 20070307: here are sometimes error messages that get concatenated with an ElementList.getOperator() string. Perhaps these strings must be translated into the original input format and a mapping must be done.

Author:

Michael Meyling

Field Summary

Fields inherited from interface org.qedeq.kernel.bo.logic.common.Operators

CLASS_OP, CONJUNCTION_OPERATOR, DISJUNCTION_OPERATOR, EQUIVALENCE_OPERATOR, EXISTENTIAL_QUANTIFIER_OPERATOR, FUNCTION_CONSTANT, FUNCTION_VARIABLE, IMPLICATION_OPERATOR, META_VARIABLE, NEGATION_OPERATOR, PREDICATE_CONSTANT, PREDICATE_VARIABLE, SUBJECT_VARIABLE, UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR, UNIVERSAL_QUANTIFIER_OPERATOR

Fields inherited from interface org.qedeq.kernel.bo.logic.wf.FormulaBasicErrors

AT_LEAST_ONE_ARGUMENT_EXPECTED, AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, ATOM_CONTENT_MUST_NOT_BE_EMPTY, ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, ATOM_CONTENT_MUST_NOT_BE_NULL, ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, ATOM_MUST_NOT_BE_NULL, ATOM_MUST_NOT_BE_NULL_TEXT, BOUND_VARIABLE_ALREADY_FREE, BOUND_VARIABLE_ALREADY_FREE_TEXT, CLASS_OPERATOR_STILL_UNKNOWN, CLASS_OPERATOR_STILL_UNKNOWN_TEXT, ELEMENT_MUST_NOT_BE_NULL, ELEMENT_MUST_NOT_BE_NULL_TEXT, EQUALITY_PREDICATE_NOT_YET_DEFINED, EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, EXACTLY_ONE_ARGUMENT_EXPECTED, EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, EXACTLY_TWO_ARGUMENTS_EXPECTED, EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED, EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, FIRST_ARGUMENT_MUST_BE_AN_ATOM, FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, FREE_VARIABLE_ALREADY_BOUND, FREE_VARIABLE_ALREADY_BOUND_TEXT, LIST_EXPECTED, LIST_EXPECTED_TEXT, LIST_MUST_NOT_BE_NULL, LIST_MUST_NOT_BE_NULL_TEXT, MORE_THAN_ONE_ARGUMENT_EXPECTED, MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, OPERATOR_CONTENT_MUST_NOT_BE_EMPTY, OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT, OPERATOR_CONTENT_MUST_NOT_BE_NULL, OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT, SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA, SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, SUBJECT_VARIABLE_EXPECTED, SUBJECT_VARIABLE_EXPECTED_TEXT, SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA, SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA_TEXT, UNKNOWN_FUNCTION_CONSTANT, UNKNOWN_FUNCTION_CONSTANT_TEXT, UNKNOWN_LOGICAL_OPERATOR, UNKNOWN_LOGICAL_OPERATOR_TEXT, UNKNOWN_PREDICATE_CONSTANT, UNKNOWN_PREDICATE_CONSTANT_TEXT, UNKNOWN_TERM_OPERATOR, UNKNOWN_TERM_OPERATOR_TEXT

Constructor Summary

FormulaCheckerImpl()
Constructor.

Method Summary

LogicalCheckExceptionList	checkFormula(Element element, ModuleContext context) Checks if an Element is a formula.
LogicalCheckExceptionList	checkFormula(Element element, ModuleContext context, ExistenceChecker existenceChecker) Checks if an Element is a formula.
LogicalCheckExceptionList	checkTerm(Element element, ModuleContext context) Check if Element is a term.
LogicalCheckExceptionList	checkTerm(Element element, ModuleContext context, ExistenceChecker existenceChecker) Check if Element is a term.
protected ModuleContext	getCurrentContext() Get current context within original.
protected void	setLocationWithinModule(java.lang.String locationWithinModule) Set location information where are we within the original module.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

FormulaCheckerImpl

public FormulaCheckerImpl()

Constructor.

Method Detail

checkFormula

public final LogicalCheckExceptionList checkFormula(Element element,
                                                    ModuleContext context,
                                                    ExistenceChecker existenceChecker)

Description copied from interface: FormulaChecker

Checks if an Element is a formula. If there are any errors the returned list (which is always not null) has a size greater zero.

Specified by:

checkFormula in interface FormulaChecker

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

existenceChecker - Existence checker for operators.

Returns:

Collected errors if there are any. Not null.

checkFormula

public final LogicalCheckExceptionList checkFormula(Element element,
                                                    ModuleContext context)

Description copied from interface: FormulaChecker

Checks if an Element is a formula. All predicates and functions are assumed to exist. If there are any errors the returned list (which is always not null) has a size greater zero. If the existence context is known you should use FormulaChecker.checkFormula(Element, ModuleContext, ExistenceChecker).

Specified by:

checkFormula in interface FormulaChecker

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

Returns:

Collected errors if there are any. Not null.

checkTerm

public final LogicalCheckExceptionList checkTerm(Element element,
                                                 ModuleContext context,
                                                 ExistenceChecker existenceChecker)

Check if Element is a term. If there are any errors the returned list (which is always not null) has a size greater zero.

Specified by:

checkTerm in interface FormulaChecker

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

existenceChecker - Existence checker for operators.

Returns:

Collected errors if there are any. Not null.

checkTerm

public final LogicalCheckExceptionList checkTerm(Element element,
                                                 ModuleContext context)

Check if Element is a term. If there are any errors the returned list (which is always not null) has a size greater zero. If the existence context is known you should use checkTerm(Element, ModuleContext, ExistenceChecker).

Specified by:

checkTerm in interface FormulaChecker

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

Returns:

Collected errors if there are any. Not null.

setLocationWithinModule

protected void setLocationWithinModule(java.lang.String locationWithinModule)

Set location information where are we within the original module.

Parameters:

locationWithinModule - Location within module.

getCurrentContext

protected final ModuleContext getCurrentContext()

Get current context within original.

Returns:

Current context.