/* $Id: FormulaChecker.java,v 1.4 2006/10/20 20:23:03 m31 Exp $
 *
 * This file is part of the project "Hilbert II" - http://www.qedeq.org
 *
 * Copyright 2000-2006,  Michael Meyling <mime@qedeq.org>.
 *
 * "Hilbert II" is free software; you can redistribute
 * it and/or modify it under the terms of the GNU General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 * GNU General Public License for more details.
 */

package org.qedeq.kernel.bo.logic;
/* $Id: CheckException.java,v 1.5 2006/10/20 20:23:03 m31 Exp $
 *
 * This file is part of the project "Hilbert II" - http://www.qedeq.org
 *
 * Copyright 2000-2006,  Michael Meyling <mime@qedeq.org>.
 *
 * "Hilbert II" is free software; you can redistribute
 * it and/or modify it under the terms of the GNU General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 * GNU General Public License for more details.
 */

import org.qedeq.kernel.base.list.Atom;
import org.qedeq.kernel.base.list.Element;
import org.qedeq.kernel.base.list.ElementList;
import org.qedeq.kernel.context.ModuleContext;
import org.qedeq.kernel.dto.list.ElementSet;
import org.qedeq.kernel.log.Trace;


/**
 * This class deals with {@link org.qedeq.kernel.base.list.Element}s which represent a
 * formula. It has methods to check those elements for certain criteria.
 *
 * @version $Revision: 1.4 $
 * @author  Michael Meyling
 */
public final class FormulaChecker implements Operators, FormulaBasicErrors {

    /** Current context during creation. */
    private final ModuleContext currentContext;

    /** Existence checker for operators. */
    private final ExistenceChecker existenceChecker;


    /**
     * Constructor.
     *
     * @param   context             For location information. Important for locating errors.
     * @param   existenceChecker    Existence checker for operators.
     * @throws  IllegalArgumentException    The <code>existenceChecker</code> says the equality
     *          operator exists but the predicate is not found.
     */
    private FormulaChecker(final ModuleContext context,
            final ExistenceChecker existenceChecker) {
        this.existenceChecker = existenceChecker;
        if (existenceChecker.equalityOperatorExists()
                && !existenceChecker.predicateExists(existenceChecker.getEqualityOperator(), 2)) {
            throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
        }
        currentContext = new ModuleContext(context);
    }

    /**
     * Is {@link Element} a formula?
     *
     * @param   element             Check this element.
     * @param   context             For location information. Important for locating errors.
     * @throws  CheckException  It is no formula.
     */
    public static final void checkFormula(final Element element, final ModuleContext context)
            throws CheckException {
        checkFormula(element, context, EverythingExists.getInstance());
    }

    /**
     * Is {@link Element} a formula?
     *
     * @param   element             Check this element.
     * @param   context             For location information. Important for locating errors.
     * @param   existenceChecker    Existence checker for operators.
     * @throws  CheckException  It is no formula.
     */
    public static final void checkFormula(final Element element, final ModuleContext context,
            final ExistenceChecker existenceChecker) throws CheckException {
        final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
        checker.checkFormula(element);
    }

    /**
     * Is {@link Element} a term?
     *
     * @param   element Check this element.
     * @param   context For location information. Important for locating errors.
     * @throws  CheckException  It is no term.
     */
    public static final void checkTerm(final Element element, final ModuleContext context)
            throws CheckException {
        checkTerm(element, context, EverythingExists.getInstance());
    }

    /**
     * Is {@link Element} a term?
     *
     * @param   element             Check this element.
     * @param   context             For location information. Important for locating errors.
     * @param   existenceChecker    Existence checker for operators.
     * @throws  CheckException      It is no term.
     */
    public static final void checkTerm(final Element element, final ModuleContext context,
            final ExistenceChecker existenceChecker) throws CheckException {
        final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
        checker.checkTerm(element);
    }

    /**
     * Is {@link Element} a formula?
     *
     * @param   element    Check this element.
     * @throws  CheckException  It is no formula.
     */
    private final void checkFormula(final Element element)
            throws CheckException {
        final String method = "checkFormula";
        Trace.begin(this, method);
        Trace.param(this, method, "element", element);
        final String context = getCurrentContext().getLocationWithinModule();
        Trace.param(this, method, "context", context);
        checkList(element);
        final ElementList list = element.getList();
        final String operator = list.getOperator();
        if (operator.equals(CONJUNCTION_OPERATOR)
                || operator.equals(DISJUNCTION_OPERATOR)
                || operator.equals(IMPLICATION_OPERATOR)
                || operator.equals(EQUIVALENCE_OPERATOR)) {
            Trace.trace(this, method, "one of (and, or, implication, equivalence) operator found");
            setLocationWithinModule(context + ".getList()");
            if (list.size() <= 1) {
                throw new FormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
                    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
                    + operator + "\"", element, getCurrentContext());
            }
            if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
                throw new FormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
                    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
                    + operator + "\"", element, getCurrentContext());
            }
            for (int i = 0; i < list.size(); i++) {
                setLocationWithinModule(context + ".getList().getElement(" + i + ")");
                checkFormula(list.getElement(i));
            }
            setLocationWithinModule(context + ".getList()");
            checkFreeAndBoundDisjunct(0, list);
        } else if (operator.equals(NEGATION_OPERATOR)) {
            Trace.trace(this, method, "negation operator found");
            setLocationWithinModule(context + ".getList()");
            if (list.size() != 1) {
                throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
                    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
                    element, getCurrentContext());
            }
            setLocationWithinModule(context + ".getList().getElement(0)");
            checkFormula(list.getElement(0));
        } else if (operator.equals(PREDICATE_VARIABLE)
                || operator.equals(PREDICATE_CONSTANT)) {
            Trace.trace(this, method, "predicate operator found");
            setLocationWithinModule(context + ".getList()");
            if (list.size() < 1) {
                throw new FormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
                    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
                    element, getCurrentContext());
            }
            // check if first argument is an atom
            setLocationWithinModule(context + ".getList().getElement(0)");
            checkAtomFirst(list.getElement(0));

            // check if rest arguments are terms
            for (int i = 1; i < list.size(); i++) {
                setLocationWithinModule(context + ".getElement(" + i + ")");
                checkTerm(list.getElement(i));
            }

            setLocationWithinModule(context + ".getList()");
            checkFreeAndBoundDisjunct(1, list);

            // check if predicate is known
            if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
                    list.getElement(0).getAtom().getString(), list.size() - 1)) {
                throw new FormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
                    UNKNOWN_PREDICATE_CONSTANT_TEXT, element, getCurrentContext());
            }

        } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
                || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
                || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
            Trace.trace(this, method, "quantifier found");
            setLocationWithinModule(context);
            checkQuantifier(element);
        } else {
            setLocationWithinModule(context + ".getOperator()");
            throw new FormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
                UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
                element, getCurrentContext());
        }
        // restore context
        setLocationWithinModule(context);
        Trace.end(this, method);
    }

    /**
     * Check quantifier element.
     *
     * @param   element     Check this element. Must be a quantifier element.
     * @throws  CheckException  Check failed.
     * @throws  IllegalArgumentException    <code>element.getList().getOperator()</code> is no
     *          quantifier operator.
     */
    private void checkQuantifier(final Element element) throws CheckException {
        final String method = "checkQuantifier";
        Trace.begin(this, method);
        Trace.param(this, method, "element", element);
        // save context
        final String context = getCurrentContext().getLocationWithinModule();
        Trace.param(this, method, "context", context);
        setLocationWithinModule(context + ".getList()");
        checkList(element);
        final ElementList list = element.getList();
        final String operator = list.getOperator();
        if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
                && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
                && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
            throw new IllegalArgumentException("quantifier element expected but found: "
                    + element.toString());
        }
        if (list.size() < 2 || list.size() > 3) {
            throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
                EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
        }

        // check if unique existential operator could be used
        setLocationWithinModule(context + ".getOperator()");
        if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
                && !existenceChecker.equalityOperatorExists()) {
            throw new FormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
                EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
        }

        // check if first argument is subject variable
        setLocationWithinModule(context + ".getList().getElement(" + 0 + ")");
        checkSubjectVariable(list.getElement(0));

        // check if second argument is a formula
        setLocationWithinModule(context + ".getList().getElement(" + 1 + ")");
        checkFormula(list.getElement(1));

        setLocationWithinModule(context + ".getList()");
        // check if subject variable is not already bound in formula
        if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
                list.getElement(0))) {
            throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
                SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
                getCurrentContext());
        }
        if (list.size() > 3) {
            throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
                EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
                getCurrentContext());
        }
        if (list.size() > 2) {
            // check if third argument is a formula
            setLocationWithinModule(context + ".getList().getElement(" + 2 + ")");
            checkFormula(list.getElement(2));

            setLocationWithinModule(context + ".getList()");
            // check if subject variable is not bound in formula
            if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains(
                    list.getElement(0))) {
                throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
                    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
                    getCurrentContext());
            }
            // the following check restricts the restriction formula for quantifiers
            // to formulas that contain the subject variable as free variable
            setLocationWithinModule(context + ".getList()");
            if (!getFreeSubjectVariables(list.getElement(1)).contains(
                    list.getElement(0))) {
                throw new FormulaCheckException(
                    SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA,
                    SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA_TEXT,
                    list.getElement(0), getCurrentContext());
            }
            checkFreeAndBoundDisjunct(1, list);
        }
        // restore context
        setLocationWithinModule(context);
        Trace.end(this, method);
    }

    /**
     * Is {@link Element} a term?
     *
     * @param   element    Check this element.
     * @throws  CheckException  It is no term.
     */
    private void checkTerm(final Element element) throws CheckException {
        final String method = "checkTerm";
        Trace.begin(this, method);
        Trace.param(this, method, "element", element);
        // save current context
        final String context = getCurrentContext().getLocationWithinModule();
        Trace.param(this, method, "context", context);
        checkList(element);
        final ElementList list = element.getList();
        final String operator = list.getOperator();
        if (operator.equals(SUBJECT_VARIABLE)) {
            checkSubjectVariable(element);
        } else if (operator.equals(FUNCTION_CONSTANT)
                || operator.equals(FUNCTION_VARIABLE)) {

            setLocationWithinModule(context + ".getList()");

            // function constants must have at least a function name
            if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
                throw new TermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
                    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
            }

            // function variables must have at least a function name and at least one argument
            if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
                throw new TermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
                    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
            }

            // check if first argument is an atom
            setLocationWithinModule(context + ".getList().getElement(0)");
            checkAtomFirst(list.getElement(0));

            // check if all arguments are terms
            setLocationWithinModule(context + ".getList()");
            for (int i = 1; i < list.size(); i++) {
                setLocationWithinModule(context + ".getElement(" + i + ")");
                checkTerm(list.getElement(i));
            }

            setLocationWithinModule(context + ".getList()");
            checkFreeAndBoundDisjunct(1, list);

            // check if function is known
            setLocationWithinModule(context);
            if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
                    list.getElement(0).getAtom().getString(), list.size() - 1)) {
                throw new FormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
                    UNKNOWN_FUNCTION_CONSTANT_TEXT, element, getCurrentContext());
            }

        } else if (operator.equals(CLASS)) {

            setLocationWithinModule(context + ".getList()");
            if (list.size() != 2) {
                throw new TermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
                    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
            }
            // check if first argument is a subject variable
            setLocationWithinModule(context + ".getList().getElement(" + 0 + ")");
            if (!isSubjectVariable(list.getElement(0))) {
                throw new TermCheckException(SUBJECT_VARIABLE_EXPECTED,
                    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
            }

            // check if the second argument is a formula
            setLocationWithinModule(context + ".getList().getElement(" + 1 + ")");
            checkFormula(list.getElement(1));

            // check if class operator is allowed
            if (!existenceChecker.classOperatorExists()) {
                throw new FormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
                    CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
            }

            // check if subject variable is not bound in formula
            setLocationWithinModule(context + ".getList().getElement(" + 0 + ")");
            if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
                    list.getElement(0))) {
                throw new TermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
                    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
                    getCurrentContext());
            }

        } else {
            setLocationWithinModule(context + ".getOperator()");
            throw new TermCheckException(UNKNOWN_TERM_OPERATOR,
                UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
        }
        // restore context
        setLocationWithinModule(context);
        Trace.end(this, method);
    }

    /**
     * Check if no bound variables are free and vice versa.
     * The current context must be at the list element.
     *
     * @param   start   Start check with this list position. Beginning with 0.
     * @param   list    List element to check.
     * @throws  CheckException  At least one variable occurs free and bound in different
     *          sub-elements.
     */
    private void checkFreeAndBoundDisjunct(final int start,
            final ElementList list) throws CheckException {
        // save current context
        final String context = getCurrentContext().getLocationWithinModule();
        final ElementSet free = new ElementSet();
        final ElementSet bound = new ElementSet();
        for (int i = start; i < list.size(); i++) {
            setLocationWithinModule(context + ".getElement(" + i + ")");
            final ElementSet newFree
                = getFreeSubjectVariables(list.getElement(i));
            final ElementSet newBound
                = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
            final ElementSet interBound = newFree.newIntersection(bound);
            if (!interBound.isEmpty()) {
                throw new FormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
                    FREE_VARIABLE_ALREADY_BOUND_TEXT
                    + interBound, list.getElement(i), getCurrentContext());
            }
            final ElementSet interFree = newBound.newIntersection(free);
            if (!interFree.isEmpty()) {
                throw new FormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
                    BOUND_VARIABLE_ALREADY_FREE_TEXT
                    + interFree, list.getElement(i), getCurrentContext());
            }
            bound.union(newBound);
            free.union(newFree);
        }
        // restore context
        setLocationWithinModule(context);
    }


    /**
     * Is {@link Element} a subject variable?
     *
     * @param   element    Element to look onto.
     * @return  Is it a subject variable?
     */
    private final boolean isSubjectVariable(final Element element) {
        try {
            checkSubjectVariable(element);
        } catch (CheckException e) {
            return false;
        }
        return true;
    }


    /**
     * Check if {@link Element} is a subject variable.
     *
     * @param   element    Check this element.
     * @throws  CheckException  It is no subject variable.
     */
    private final void checkSubjectVariable(final Element element)
            throws CheckException {
        // save current context
        final String context = getCurrentContext().getLocationWithinModule();
        checkList(element);
        setLocationWithinModule(context + ".getOperator()");
        if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
            setLocationWithinModule(context + ".getList()");
            if (element.getList().size() != 1) {
                throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
                    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
            }
            // check if first argument is an atom
            setLocationWithinModule(context + ".getList().getElement(0)");
            checkAtomFirst(element.getList().getElement(0));
        } else {
            throw new FormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
                SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
        }
        // restore context
        setLocationWithinModule(context);
    }


    /**
     * Return all free subject variables of an element.
     *
     * @param   element    Work on this element.
     * @return  All free subject variables.
     */
    private final ElementSet getFreeSubjectVariables(final Element element) {
        final ElementSet free = new ElementSet();
        if (isSubjectVariable(element)) {
            free.add(element);
        } else if (element.isList()) {
            final ElementList list = element.getList();
            final String operator = list.getOperator();
            if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
                || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
                || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
                || operator.equals(CLASS)) {
                for (int i = 1; i < list.size(); i++) {
                    free.union(getFreeSubjectVariables(list.getElement(i)));
                }
                free.remove(list.getElement(0));
            } else {
                for (int i = 0; i < list.size(); i++) {
                    free.union(getFreeSubjectVariables(list.getElement(i)));
                }
            }
        }
        return free;
    }

    /**
     * Return all bound subject variables of an element.
     *
     * @param   element    Work on this element.
     * @return  All bound subject variables.
     */
    public static final ElementSet getBoundSubjectVariables(final Element element) {
        final ElementSet bound = new ElementSet();
        if (element.isList()) {
            ElementList list = element.getList();
            final String operator = list.getOperator();
            // if operator is quantifier or class term
            if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
                    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
                    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
                    || operator.equals(CLASS)) {
                // add subject variable to bound list
                bound.add(list.getElement(0));
                // add all bound variables of sub-elements
                for (int i = 1; i < list.size(); i++) {
                    bound.union(FormulaChecker.getBoundSubjectVariables(
                        list.getElement(i)));
                }
            } else {
                // add all bound variables of sub-elements
                for (int i = 0; i < list.size(); i++) {
                    bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
                }
            }
        }
        return bound;
    }

    /**
     * Check common requirements for list elements that are checked for being a term or formula.
     *
     * @param   element     List element.
     * @throws  ElementCheckException   Requirements not fulfilled.
     */
    private void checkList(final Element element) throws ElementCheckException {
        // save current context
        final String context = getCurrentContext().getLocationWithinModule();
        if (element == null) {
            throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
                ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
        }
        if (!element.isList()) {
            throw new ElementCheckException(LIST_EXPECTED,
                LIST_EXPECTED_TEXT, element, getCurrentContext());
        }
        final ElementList list = element.getList();
        setLocationWithinModule(context + ".getList()");
        if (list == null) {
            throw new ElementCheckException(LIST_MUST_NOT_BE_NULL,
                LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
        }
        final String operator = list.getOperator();
        setLocationWithinModule(context + ".getOperator()");
        if (operator == null) {
            throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
                OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT + "\""
                + operator + "\"", element, getCurrentContext());
        }
        if (operator.length() == 0) {
            throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
                OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
                + operator + "\"", element, getCurrentContext());
        }
        // restore context
        setLocationWithinModule(context);
    }

    /**
     * Check if element is an atom and has valid content. It is assumed, that this element is the
     * first of a list.
     *
     * @param   element Check this for an atom.
     * @throws  ElementCheckException   No valid content.
     */
    private void checkAtomFirst(final Element element) throws ElementCheckException {
        // save current context
        final String context = getCurrentContext().getLocationWithinModule();
        if (element == null) {
            throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
                ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
        }
        if (!element.isAtom()) {    // TODO mime 20061126: this is special?
            throw new ElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
                FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
        }
        final Atom atom = element.getAtom();
        setLocationWithinModule(context + ".getAtom()");
        if (atom == null) {
            throw new ElementCheckException(ATOM_MUST_NOT_BE_NULL,
                ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
        }
        if (atom.getString() == null) {
            throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
                ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
        }
        if (atom.getString().length() == 0) {
            throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
                ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
        }
        // restore context
        setLocationWithinModule(context);
    }

    /**
     * Set location information where are we within the original module.
     *
     * @param   locationWithinModule    Location within module.
     */
    protected void setLocationWithinModule(final String locationWithinModule) {
        getCurrentContext().setLocationWithinModule(locationWithinModule);
    }

    /**
     * Get current context within original.
     *
     * @return  Current context.
     */
    protected final ModuleContext getCurrentContext() {
        return currentContext;
    }

}