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.service.logic;
017
018 import java.util.Map;
019
020 import org.qedeq.base.io.IoUtility;
021 import org.qedeq.base.trace.Trace;
022 import org.qedeq.base.utility.EqualsUtility;
023 import org.qedeq.base.utility.StringUtility;
024 import org.qedeq.kernel.bo.common.PluginExecutor;
025 import org.qedeq.kernel.bo.log.QedeqLog;
026 import org.qedeq.kernel.bo.logic.FormulaCheckerFactoryImpl;
027 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
028 import org.qedeq.kernel.bo.logic.common.FormulaCheckerFactory;
029 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
030 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
031 import org.qedeq.kernel.bo.logic.common.FunctionKey;
032 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
033 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
034 import org.qedeq.kernel.bo.logic.common.PredicateKey;
035 import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
036 import org.qedeq.kernel.bo.module.ControlVisitor;
037 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
038 import org.qedeq.kernel.bo.module.KernelQedeqBo;
039 import org.qedeq.kernel.se.base.list.Element;
040 import org.qedeq.kernel.se.base.list.ElementList;
041 import org.qedeq.kernel.se.base.module.Axiom;
042 import org.qedeq.kernel.se.base.module.FormalProof;
043 import org.qedeq.kernel.se.base.module.FormalProofLine;
044 import org.qedeq.kernel.se.base.module.FormalProofLineList;
045 import org.qedeq.kernel.se.base.module.Formula;
046 import org.qedeq.kernel.se.base.module.FunctionDefinition;
047 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
048 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
049 import org.qedeq.kernel.se.base.module.PredicateDefinition;
050 import org.qedeq.kernel.se.base.module.Proposition;
051 import org.qedeq.kernel.se.base.module.ReasonType;
052 import org.qedeq.kernel.se.base.module.Rule;
053 import org.qedeq.kernel.se.common.CheckLevel;
054 import org.qedeq.kernel.se.common.DefaultSourceFileExceptionList;
055 import org.qedeq.kernel.se.common.IllegalModuleDataException;
056 import org.qedeq.kernel.se.common.LogicalModuleState;
057 import org.qedeq.kernel.se.common.ModuleDataException;
058 import org.qedeq.kernel.se.common.Plugin;
059 import org.qedeq.kernel.se.common.SourceFileException;
060 import org.qedeq.kernel.se.common.SourceFileExceptionList;
061 import org.qedeq.kernel.se.dto.list.ElementSet;
062
063
064 /**
065 * Checks if all formulas of a QEDEQ module are well formed.
066 * This plugin assumes all required modules are loaded!
067 *
068 * FIXME 20110329 m31: we must also check, that OR, AND, IMPL and EQUI have only 2 arguments
069 *
070 * @author Michael Meyling
071 */
072 public final class WellFormedCheckerExecutor extends ControlVisitor implements PluginExecutor {
073
074 /** This class. */
075 private static final Class CLASS = WellFormedCheckerExecutor.class;
076
077 /** Existence checker for predicate and function constants. */
078 private ModuleConstantsExistenceCheckerImpl existence;
079
080 /** Factory for generating new checkers. */
081 private FormulaCheckerFactory checkerFactory = null;
082
083 /** Parameters for checker. */
084 private Map parameters;
085
086 /**
087 * Constructor.
088 *
089 * @param plugin This plugin we work for.
090 * @param qedeq QEDEQ BO object.
091 * @param parameters Parameters.
092 */
093 WellFormedCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
094 final Map parameters) {
095 super(plugin, qedeq);
096 final String method = "QedeqBoFormalLogicChecker(Plugin, KernelQedeqBo, Map)";
097 this.parameters = parameters;
098 final String checkerFactoryClass
099 = (parameters != null ? (String) parameters.get("checkerFactory") : null);
100 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
101 try {
102 Class cl = Class.forName(checkerFactoryClass);
103 checkerFactory = (FormulaCheckerFactory) cl.newInstance();
104 } catch (ClassNotFoundException e) {
105 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class not in class path: "
106 + checkerFactoryClass, e);
107 } catch (InstantiationException e) {
108 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class could not be instanciated: "
109 + checkerFactoryClass, e);
110 } catch (IllegalAccessException e) {
111 Trace.fatal(CLASS, this, method,
112 "Programming error, access for instantiation failed for model: "
113 + checkerFactoryClass, e);
114 } catch (RuntimeException e) {
115 Trace.fatal(CLASS, this, method,
116 "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
117 }
118 }
119 // fallback is the default checker factory
120 if (checkerFactory == null) {
121 checkerFactory = new FormulaCheckerFactoryImpl();
122 }
123 }
124
125 private Map getParameters() {
126 return parameters;
127 }
128
129 public Object executePlugin() {
130 if (getQedeqBo().isChecked()) {
131 return Boolean.TRUE;
132 }
133 QedeqLog.getInstance().logRequest(
134 "Check logical well formedness for \"" + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"");
135 getServices().loadModule(getQedeqBo().getModuleAddress());
136 if (!getQedeqBo().isLoaded()) {
137 final String msg = "Check of logical correctness failed for \"" + getQedeqBo().getUrl()
138 + "\"";
139 QedeqLog.getInstance().logFailureReply(msg, "Module could not even be loaded.");
140 return Boolean.FALSE;
141 }
142 getServices().loadRequiredModules(getQedeqBo().getModuleAddress());
143 if (!getQedeqBo().hasLoadedRequiredModules()) {
144 final String msg = "Check of logical well formedness failed for \""
145 + IoUtility.easyUrl(getQedeqBo().getUrl())
146 + "\"";
147 QedeqLog.getInstance().logFailureReply(msg, "Not all required modules could be loaded.");
148 return Boolean.FALSE;
149 }
150 getQedeqBo().setLogicalProgressState(LogicalModuleState.STATE_EXTERNAL_CHECKING);
151 final SourceFileExceptionList sfl = new DefaultSourceFileExceptionList();
152 KernelModuleReferenceList list = (KernelModuleReferenceList) getQedeqBo().getRequiredModules();
153 for (int i = 0; i < list.size(); i++) {
154 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
155 final WellFormedCheckerExecutor checker = new WellFormedCheckerExecutor(getPlugin(),
156 list.getKernelQedeqBo(i), getParameters());
157 checker.executePlugin();
158 if (!list.getKernelQedeqBo(i).isChecked()) {
159 ModuleDataException md = new CheckRequiredModuleException(
160 LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
161 LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
162 + list.getQedeqBo(i).getModuleAddress(),
163 list.getModuleContext(i));
164 sfl.add(getQedeqBo().createSourceFileException(getPlugin(), md));
165 }
166 }
167 // has at least one import errors?
168 if (sfl.size() > 0) {
169 getQedeqBo().setLogicalFailureState(LogicalModuleState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
170 final String msg = "Check of logical well formedness failed for \""
171 + IoUtility.easyUrl(getQedeqBo().getUrl())
172 + "\"";
173 QedeqLog.getInstance().logFailureReply(msg, sfl.getMessage());
174 return Boolean.FALSE;
175 }
176 getQedeqBo().setLogicalProgressState(LogicalModuleState.STATE_INTERNAL_CHECKING);
177 getQedeqBo().setExistenceChecker(existence);
178 try {
179 traverse();
180 } catch (SourceFileExceptionList e) {
181 getQedeqBo().setLogicalFailureState(LogicalModuleState.STATE_INTERNAL_CHECKING_FAILED, e);
182 final String msg = "Check of logical well formedness failed for \""
183 + IoUtility.easyUrl(getQedeqBo().getUrl())
184 + "\"";
185 QedeqLog.getInstance().logFailureReply(msg, sfl.getMessage());
186 return Boolean.FALSE;
187 }
188 getQedeqBo().setChecked(existence);
189 QedeqLog.getInstance().logSuccessfulReply(
190 "Check of logical well formedness successful for \"" + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"");
191 return Boolean.TRUE;
192 }
193
194 public void traverse() throws SourceFileExceptionList {
195 try {
196 this.existence = new ModuleConstantsExistenceCheckerImpl(getQedeqBo());
197 } catch (ModuleDataException me) {
198 addError(me);
199 throw getErrorList();
200 }
201 super.traverse();
202 }
203
204 public void visitEnter(final Axiom axiom) throws ModuleDataException {
205 if (axiom == null) {
206 return;
207 }
208 final String context = getCurrentContext().getLocationWithinModule();
209 // we start checking
210 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
211 if (axiom.getFormula() != null) {
212 setLocationWithinModule(context + ".getFormula().getElement()");
213 final Formula formula = axiom.getFormula();
214 LogicalCheckExceptionList list =
215 checkerFactory.createFormulaChecker().checkFormula(
216 formula.getElement(), getCurrentContext(), existence);
217 for (int i = 0; i < list.size(); i++) {
218 addError(list.get(i));
219 }
220 } else {
221 getNodeBo().setWellFormed(CheckLevel.FAILURE);
222 }
223 // if we found no errors this node is ok
224 if (!getNodeBo().isNotWellFormed()) {
225 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
226 }
227 setLocationWithinModule(context);
228 setBlocked(true);
229 }
230
231 public void visitLeave(final Axiom axiom) {
232 setBlocked(false);
233 }
234
235 public void visitEnter(final PredicateDefinition definition)
236 throws ModuleDataException {
237 if (definition == null) {
238 return;
239 }
240 final String context = getCurrentContext().getLocationWithinModule();
241 // we start checking
242 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
243 final PredicateKey predicateKey = new PredicateKey(definition.getName(),
244 definition.getArgumentNumber());
245 // we misuse a do loop to be able to break
246 do {
247 if (existence.predicateExists(predicateKey)) {
248 addError(new IllegalModuleDataException(
249 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
250 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicateKey,
251 getCurrentContext()));
252 break;
253 }
254 if (definition.getFormula() == null) {
255 addError(new IllegalModuleDataException(
256 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
257 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
258 getCurrentContext()));
259 break;
260 }
261 final Element completeFormula = definition.getFormula().getElement();
262 if (completeFormula == null) {
263 addError(new IllegalModuleDataException(
264 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
265 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
266 getCurrentContext()));
267 break;
268 }
269 setLocationWithinModule(context + ".getFormula().getElement()");
270 if (completeFormula.isAtom()) {
271 addError(new IllegalModuleDataException(
272 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
273 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
274 getCurrentContext()));
275 break;
276 }
277 final ElementList equi = completeFormula.getList();
278 final String operator = equi.getOperator();
279 if (!operator.equals(FormulaCheckerImpl.EQUIVALENCE_OPERATOR)
280 || equi.size() != 2) {
281 addError(new IllegalModuleDataException(
282 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
283 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
284 getCurrentContext()));
285 break;
286 }
287 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(0)");
288 if (equi.getElement(0).isAtom()) {
289 addError(new IllegalModuleDataException(
290 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
291 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
292 getCurrentContext()));
293 break;
294 }
295 final ElementList predicate = equi.getElement(0).getList();
296 if (predicate.getOperator() != FormulaCheckerImpl.PREDICATE_CONSTANT) {
297 addError(new IllegalModuleDataException(
298 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
299 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
300 getCurrentContext()));
301 break;
302 }
303 final Element definingFormula = equi.getElement(1);
304
305 final ElementSet free = FormulaUtility.getFreeSubjectVariables(definingFormula);
306 for (int i = 0; i < predicate.size(); i++) {
307 setLocationWithinModule(context
308 + ".getFormula().getElement().getList().getElement(0).getList().getElement(" + i + ")");
309 if (i == 0) {
310 if (!predicate.getElement(0).isAtom()
311 || !EqualsUtility.equals(definition.getName(),
312 predicate.getElement(0).getAtom().getString())) {
313 addError(new IllegalModuleDataException(
314 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_CODE,
315 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_TEXT
316 + StringUtility.quote(definition.getName()) + " - "
317 + StringUtility.quote(predicate.getElement(0).getAtom().getString()),
318 getCurrentContext()));
319 continue;
320 }
321 } else if (!FormulaUtility.isSubjectVariable(predicate.getElement(i))) {
322 addError(new IllegalModuleDataException(
323 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
324 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT + predicate.getElement(i),
325 getCurrentContext()));
326 continue;
327 }
328 setLocationWithinModule(context
329 + ".getFormula().getElement().getList().getElement(1)");
330 if (i != 0 && !free.contains(predicate.getElement(i))) {
331 addError(new IllegalModuleDataException(
332 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
333 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT + predicate.getElement(i),
334 getCurrentContext()));
335 }
336 }
337 setLocationWithinModule(context + ".getFormula().getElement()");
338 if (predicate.size() - 1 != free.size()) {
339 addError(new IllegalModuleDataException(
340 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
341 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
342 getCurrentContext()));
343 }
344 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
345 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
346 definingFormula, getCurrentContext(), existence);
347 for (int i = 0; i < list.size(); i++) {
348 addError(list.get(i));
349 }
350 if (list.size() > 0) {
351 break;
352 }
353 setLocationWithinModule(context + ".getFormula().getElement().getList()");
354 final PredicateConstant constant = new PredicateConstant(predicateKey,
355 equi, getCurrentContext());
356 setLocationWithinModule(context);
357 if (existence.predicateExists(predicateKey)) {
358 addError(new IllegalModuleDataException(
359 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
360 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
361 + predicateKey, getCurrentContext()));
362 break;
363 }
364 existence.add(constant);
365 // a final check, we don't expect any errors here, but hey - we want to be very sure!
366 setLocationWithinModule(context + ".getFormula().getElement().getList()");
367 final LogicalCheckExceptionList errorlist = checkerFactory.createFormulaChecker()
368 .checkFormula(completeFormula, getCurrentContext(), existence);
369 for (int i = 0; i < errorlist.size(); i++) {
370 addError(errorlist.get(i));
371 }
372 } while (false);
373
374 // check if we just found the identity operator
375 setLocationWithinModule(context);
376 if ("2".equals(predicateKey.getArguments())
377 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
378 existence.setIdentityOperatorDefined(predicateKey.getName(),
379 (KernelQedeqBo) getQedeqBo(), getCurrentContext());
380 }
381 // if we found no errors this node is ok
382 if (!getNodeBo().isNotWellFormed()) {
383 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
384 }
385 setBlocked(true);
386 }
387
388 public void visitLeave(final PredicateDefinition definition) {
389 setBlocked(false);
390 }
391
392 public void visitEnter(final InitialPredicateDefinition definition)
393 throws ModuleDataException {
394 if (definition == null) {
395 return;
396 }
397 final String context = getCurrentContext().getLocationWithinModule();
398 // we start checking
399 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
400 final PredicateKey predicateKey = new PredicateKey(
401 definition.getName(), definition.getArgumentNumber());
402 setLocationWithinModule(context);
403 if (existence.predicateExists(predicateKey)) {
404 addError(new IllegalModuleDataException(
405 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
406 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
407 + predicateKey, getCurrentContext()));
408 }
409 existence.add(definition);
410 // check if we just found the identity operator
411 if ("2".equals(predicateKey.getArguments())
412 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
413 existence.setIdentityOperatorDefined(predicateKey.getName(),
414 (KernelQedeqBo) getQedeqBo(), getCurrentContext());
415 }
416 // if we found no errors this node is ok
417 if (!getNodeBo().isNotWellFormed()) {
418 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
419 }
420 setBlocked(true);
421 }
422
423 public void visitLeave(final InitialPredicateDefinition definition) {
424 setBlocked(false);
425 }
426
427 public void visitEnter(final InitialFunctionDefinition definition)
428 throws ModuleDataException {
429 if (definition == null) {
430 return;
431 }
432 final String context = getCurrentContext().getLocationWithinModule();
433 // we start checking
434 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
435 final FunctionKey function = new FunctionKey(definition.getName(),
436 definition.getArgumentNumber());
437 if (existence.functionExists(function)) {
438 addError(new IllegalModuleDataException(
439 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
440 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT + function,
441 getCurrentContext()));
442 }
443 existence.add(definition);
444 setLocationWithinModule(context);
445 // if we found no errors this node is ok
446 if (!getNodeBo().isNotWellFormed()) {
447 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
448 }
449 setBlocked(true);
450 }
451
452 public void visitLeave(final InitialFunctionDefinition definition) {
453 setBlocked(false);
454 }
455
456 public void visitEnter(final FunctionDefinition definition)
457 throws ModuleDataException {
458 if (definition == null) {
459 return;
460 }
461 final String context = getCurrentContext().getLocationWithinModule();
462 // we start checking
463 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
464 final FunctionKey function = new FunctionKey(definition.getName(),
465 definition.getArgumentNumber());
466 // we misuse a do loop to be able to break
467 do {
468 if (existence.functionExists(function)) {
469 addError(new IllegalModuleDataException(
470 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
471 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT
472 + function, getCurrentContext()));
473 break;
474 }
475 if (definition.getFormula() == null) {
476 addError(new IllegalModuleDataException(
477 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
478 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
479 getCurrentContext()));
480 break;
481 }
482 final Formula formulaArgument = definition.getFormula();
483 setLocationWithinModule(context + ".getFormula()");
484 if (formulaArgument.getElement() == null || formulaArgument.getElement().isAtom()) {
485 addError(new IllegalModuleDataException(
486 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
487 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
488 getCurrentContext()));
489 break;
490 }
491 final ElementList formula = formulaArgument.getElement().getList();
492 setLocationWithinModule(context + ".getFormula().getElement().getList()");
493 if (!existence.identityOperatorExists()) {
494 addError(new IllegalModuleDataException(
495 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE,
496 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT,
497 getCurrentContext()));
498 break;
499 }
500 if (!FormulaCheckerImpl.PREDICATE_CONSTANT.equals(formula.getOperator())) {
501 addError(new IllegalModuleDataException(
502 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
503 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
504 getCurrentContext()));
505 break;
506 }
507 if (formula.size() != 3) {
508 addError(new IllegalModuleDataException(
509 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
510 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
511 getCurrentContext()));
512 break;
513 }
514 if (!formula.getElement(0).isAtom()) {
515 addError(new IllegalModuleDataException(
516 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
517 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
518 getCurrentContext()));
519 break;
520 }
521 if (!EqualsUtility.equals(existence.getIdentityOperator(),
522 formula.getElement(0).getAtom().getString())) {
523 addError(new IllegalModuleDataException(
524 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
525 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
526 getCurrentContext()));
527 break;
528 }
529 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
530 if (formula.getElement(1).isAtom()) {
531 addError(new IllegalModuleDataException(
532 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
533 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
534 getCurrentContext()));
535 break;
536 }
537 final ElementList functionConstant = formula.getElement(1).getList();
538 if (!FormulaCheckerImpl.FUNCTION_CONSTANT.equals(functionConstant.getOperator())) {
539 addError(new IllegalModuleDataException(
540 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
541 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
542 getCurrentContext()));
543 break;
544 }
545 setLocationWithinModule(context
546 + ".getFormula().getElement().getList().getElement(1).getList()");
547 final int size = functionConstant.size();
548 if (!("" + (size - 1)).equals(definition.getArgumentNumber())) {
549 addError(new IllegalModuleDataException(
550 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
551 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
552 getCurrentContext()));
553 break;
554 }
555 setLocationWithinModule(context
556 + ".getFormula().getElement().getList().getElement(1).getList().getElement(0)");
557 if (!functionConstant.getElement(0).isAtom()) {
558 addError(new IllegalModuleDataException(
559 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
560 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
561 getCurrentContext()));
562 break;
563 }
564 if (!EqualsUtility.equals(definition.getName(),
565 functionConstant.getElement(0).getAtom().getString())) {
566 addError(new IllegalModuleDataException(
567 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
568 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
569 getCurrentContext()));
570 break;
571 }
572 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
573 if (formula.getElement(2).isAtom()) {
574 addError(new IllegalModuleDataException(
575 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_CODE,
576 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_TEXT,
577 getCurrentContext()));
578 break;
579 }
580 final ElementList term = formula.getElement(2).getList();
581 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
582 final ElementSet free = FormulaUtility.getFreeSubjectVariables(term);
583 if (size - 1 != free.size()) {
584 addError(new IllegalModuleDataException(
585 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
586 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
587 getCurrentContext()));
588 break;
589 }
590 if (functionConstant.getElement(0).isList()
591 || !EqualsUtility.equals(function.getName(),
592 functionConstant.getElement(0).getAtom().getString())) {
593 }
594 for (int i = 1; i < size; i++) {
595 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"
596 + ".getList().get(" + i + ")");
597 if (!FormulaUtility.isSubjectVariable(functionConstant.getElement(i))) {
598 addError(new IllegalModuleDataException(
599 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
600 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT
601 + functionConstant.getElement(i), getCurrentContext()));
602 }
603 if (!free.contains(functionConstant.getElement(i))) {
604 addError(new IllegalModuleDataException(
605 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
606 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT
607 + functionConstant.getElement(i), getCurrentContext()));
608 }
609 }
610 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
611 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker()
612 .checkTerm(term, getCurrentContext(), existence);
613 for (int i = 0; i < list.size(); i++) {
614 addError(list.get(i));
615 }
616 if (list.size() > 0) {
617 break;
618 }
619 setLocationWithinModule(context + ".getFormula().getElement().getList()");
620 existence.add(new FunctionConstant(function, formula, getCurrentContext()));
621 // a final check, we don't expect any errors here, but hey - we want to be very sure!
622 final LogicalCheckExceptionList listComplete = checkerFactory.createFormulaChecker()
623 .checkFormula(formulaArgument.getElement(), getCurrentContext(), existence);
624 for (int i = 0; i < listComplete.size(); i++) {
625 addError(listComplete.get(i));
626 }
627 } while (false);
628 setLocationWithinModule(context);
629 // if we found no errors this node is ok
630 if (!getNodeBo().isNotWellFormed()) {
631 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
632 }
633 setBlocked(true);
634 }
635
636 public void visitLeave(final FunctionDefinition definition) {
637 setBlocked(false);
638 }
639
640 public void visitEnter(final Proposition proposition)
641 throws ModuleDataException {
642 if (proposition == null) {
643 return;
644 }
645 final String context = getCurrentContext().getLocationWithinModule();
646 // we start checking
647 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
648 if (proposition.getFormula() != null) {
649 setLocationWithinModule(context + ".getFormula().getElement()");
650 final Formula formula = proposition.getFormula();
651 LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
652 formula.getElement(), getCurrentContext(), existence);
653 for (int i = 0; i < list.size(); i++) {
654 addError(list.get(i));
655 }
656 } else { // no formula
657 getNodeBo().setWellFormed(CheckLevel.FAILURE);
658 }
659 if (proposition.getFormalProofList() != null) {
660 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
661 final FormalProof proof = proposition.getFormalProofList().get(i);
662 if (proof != null) {
663 final FormalProofLineList list = proof.getFormalProofLineList();
664 if (list != null) {
665 for (int j = 0; j < list.size(); j++) {
666 final FormalProofLine line = list.get(j);
667 setLocationWithinModule(context + ".getFormalProofList().get("
668 + i + ").getFormalProofLineList().get(" + j + ")");
669 checkProofLine(line);
670 }
671 }
672 }
673 }
674 }
675 setLocationWithinModule(context);
676 // if we found no errors this node is ok
677 if (!getNodeBo().isNotWellFormed()) {
678 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
679 }
680 setBlocked(true);
681 }
682
683 /**
684 * Check well-formedness of proof lines.
685 *
686 * @param line Check formulas and terms of this proof line.
687 */
688 private void checkProofLine(final FormalProofLine line) {
689 final String context = getCurrentContext().getLocationWithinModule();
690 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
691 if (line != null) {
692 final Formula formula = line.getFormula();
693 if (formula != null) {
694 setLocationWithinModule(context + ".getFormula().getElement()");
695 elist = checkerFactory.createFormulaChecker().checkFormula(
696 formula.getElement(), getCurrentContext(), existence);
697 for (int k = 0; k < elist.size(); k++) {
698 addError(elist.get(k));
699 }
700 }
701 final ReasonType reasonType = line.getReasonType();
702 if (reasonType != null) {
703 if (reasonType.getSubstFree() != null
704 && reasonType.getSubstFree().getSubstituteTerm() != null) {
705 setLocationWithinModule(context
706 + ".getReasonType().getSubstFree().getSubstituteTerm()");
707 elist = checkerFactory.createFormulaChecker().checkTerm(
708 reasonType.getSubstFree().getSubstituteTerm(),
709 getCurrentContext(), existence);
710 } else if (reasonType.getSubstPred() != null
711 && reasonType.getSubstPred().getSubstituteFormula() != null) {
712 setLocationWithinModule(context
713 + ".getReasonType().getSubstPred().getSubstituteFormula()");
714 elist = checkerFactory.createFormulaChecker().checkFormula(
715 reasonType.getSubstPred().getSubstituteFormula(),
716 getCurrentContext(), existence);
717 } else if (reasonType.getSubstFunc() != null
718 && reasonType.getSubstFunc().getSubstituteTerm() != null) {
719 setLocationWithinModule(context
720 + ".getReasonType().getSubstFunc().getSubstituteTerm()");
721 elist = checkerFactory.createFormulaChecker().checkTerm(
722 reasonType.getSubstFunc().getSubstituteTerm(),
723 getCurrentContext(), existence);
724 }
725 for (int k = 0; k < elist.size(); k++) {
726 addError(elist.get(k));
727 }
728 }
729 }
730 }
731
732 public void visitLeave(final Proposition definition) {
733 setBlocked(false);
734 }
735
736 public void visitEnter(final Rule rule) throws ModuleDataException {
737 if (rule == null) {
738 return;
739 }
740 // we start checking
741 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
742 if (rule.getName() != null) {
743 if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) {
744 // TODO mime 20080114: check if this rule can be proposed
745 existence.setClassOperatorModule((KernelQedeqBo) getQedeqBo(),
746 getCurrentContext());
747 }
748 } else {
749 getNodeBo().setWellFormed(CheckLevel.FAILURE);
750 }
751 // if we found no errors this node is ok
752 if (!getNodeBo().isNotWellFormed()) {
753 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
754 }
755 setBlocked(true);
756 }
757
758 public void visitLeave(final Rule rule) {
759 setBlocked(false);
760 }
761
762 protected void addError(final ModuleDataException me) {
763 if (getNodeBo() != null) {
764 getNodeBo().setWellFormed(CheckLevel.FAILURE);
765 }
766 super.addError(me);
767 }
768
769 protected void addError(final SourceFileException me) {
770 if (getNodeBo() != null) {
771 getNodeBo().setWellFormed(CheckLevel.FAILURE);
772 }
773 super.addError(me);
774 }
775
776 /**
777 * Set location information where are we within the original module.
778 *
779 * @param locationWithinModule Location within module.
780 */
781 public void setLocationWithinModule(final String locationWithinModule) {
782 getCurrentContext().setLocationWithinModule(locationWithinModule);
783 }
784
785 }
|