1 /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2 *
3 * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>.
4 *
5 * "Hilbert II" is free software; you can redistribute
6 * it and/or modify it under the terms of the GNU General Public
7 * License as published by the Free Software Foundation; either
8 * version 2 of the License, or (at your option) any later version.
9 *
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 */
15
16 package org.qedeq.kernel.bo.logic.common;
17
18 import org.qedeq.kernel.se.base.list.Element;
19 import org.qedeq.kernel.se.common.ModuleContext;
20
21 /**
22 * A formula checker can check logical correctness of a formula or term.
23 *
24 * @author Michael Meyling
25 */
26 public interface FormulaChecker {
27
28 /**
29 * Checks if an {@link Element} is a formula. If there are any errors the returned list
30 * (which is always not <code>null</code>) has a size greater zero.
31 *
32 * @param element Check this element.
33 * @param context For location information. Important for locating errors.
34 * @param existenceChecker Existence checker for operators.
35 * @return Collected errors if there are any. Not <code>null</code>.
36 */
37 public LogicalCheckExceptionList checkFormula(final Element element,
38 final ModuleContext context, final ExistenceChecker existenceChecker);
39
40 /**
41 * Checks if an {@link Element} is a formula. All predicates and functions are assumed to exist.
42 * If there are any errors the returned list (which is always not <code>null</code>) has a size
43 * greater zero.
44 * If the existence context is known you should use
45 * {@link #checkFormula(Element, ModuleContext, ExistenceChecker)}.
46 *
47 * @param element Check this element.
48 * @param context For location information. Important for locating errors.
49 * @return Collected errors if there are any. Not <code>null</code>.
50 */
51 public LogicalCheckExceptionList checkFormula(final Element element,
52 final ModuleContext context);
53
54 /**
55 * Check if {@link Element} is a term. If there are any errors the returned list
56 * (which is always not <code>null</code>) has a size greater zero.
57 *
58 * @param element Check this element.
59 * @param context For location information. Important for locating errors.
60 * @param existenceChecker Existence checker for operators.
61 * @return Collected errors if there are any. Not <code>null</code>.
62 */
63 public LogicalCheckExceptionList checkTerm(final Element element,
64 final ModuleContext context, final ExistenceChecker existenceChecker);
65
66 /**
67 * Check if {@link Element} is a term. If there are any errors the returned list
68 * (which is always not <code>null</code>) has a size greater zero.
69 * If the existence context is known you should use
70 * {@link #checkTerm(Element, ModuleContext, ExistenceChecker)}.
71 *
72 * @param element Check this element.
73 * @param context For location information. Important for locating errors.
74 * @return Collected errors if there are any. Not <code>null</code>.
75 */
76 public LogicalCheckExceptionList checkTerm(final Element element,
77 final ModuleContext context);
78
79 }