org.qedeq.kernel.bo.logic
Class FormulaChecker

java.lang.Object
  org.qedeq.kernel.bo.logic.FormulaChecker

All Implemented Interfaces:

FormulaBasicErrors, Operators

public final class FormulaChecker

extends Object

implements Operators, FormulaBasicErrors

This class deals with Elements which represent a formula. It has methods to check those elements for certain criteria. 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.

Version:

$Revision: 1.9 $

Field Summary

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

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

Fields inherited from interface org.qedeq.kernel.bo.logic.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

Method Summary

static void	checkFormula(Element element, ModuleContext context) Is Element a formula?
static void	checkFormula(Element element, ModuleContext context, ExistenceChecker existenceChecker) Is Element a formula?
static void	checkTerm(Element element, ModuleContext context) Is Element a term?
static void	checkTerm(Element element, ModuleContext context, ExistenceChecker existenceChecker) Is Element a term?
static ElementSet	getBoundSubjectVariables(Element element) Return all bound subject variables of an element.
protected ModuleContext	getCurrentContext() Get current context within original.
protected void	setLocationWithinModule(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

Method Detail

checkFormula

public static final void checkFormula(Element element,
                                      ModuleContext context,
                                      ExistenceChecker existenceChecker)
                               throws LogicalCheckException

Is Element a formula?

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

existenceChecker - Existence checker for operators.

Throws:

LogicalCheckException - It is no formula.

checkFormula

public static final void checkFormula(Element element,
                                      ModuleContext context)
                               throws LogicalCheckException

Is Element a formula? All predicates and functions are assumed to exit. If the existence context is known you should use checkFormula(Element, ModuleContext, ExistenceChecker).

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

Throws:

LogicalCheckException - It is no formula.

checkTerm

public static final void checkTerm(Element element,
                                   ModuleContext context,
                                   ExistenceChecker existenceChecker)
                            throws LogicalCheckException

Is Element a term?

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

existenceChecker - Existence checker for operators.

Throws:

LogicalCheckException - It is no term.

checkTerm

public static final void checkTerm(Element element,
                                   ModuleContext context)
                            throws LogicalCheckException

Is Element a term? If the existence context is known you should use checkTerm(Element, ModuleContext, ExistenceChecker).

Parameters:

element - Check this element.

context - For location information. Important for locating errors.

Throws:

LogicalCheckException - It is no term.

getBoundSubjectVariables

public static final ElementSet getBoundSubjectVariables(Element element)

Return all bound subject variables of an element.

Parameters:

element - Work on this element.

Returns:

All bound subject variables.

setLocationWithinModule

protected void setLocationWithinModule(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.