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.HashMap;
019 import java.util.Iterator;
020 import java.util.Map;
021
022 import org.qedeq.base.io.Parameters;
023 import org.qedeq.base.io.Version;
024 import org.qedeq.base.trace.Trace;
025 import org.qedeq.base.utility.EqualsUtility;
026 import org.qedeq.base.utility.StringUtility;
027 import org.qedeq.kernel.bo.common.PluginExecutor;
028 import org.qedeq.kernel.bo.log.QedeqLog;
029 import org.qedeq.kernel.bo.logic.FormulaCheckerFactoryImpl;
030 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
031 import org.qedeq.kernel.bo.logic.common.FormulaCheckerFactory;
032 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
033 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
034 import org.qedeq.kernel.bo.logic.common.FunctionKey;
035 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
036 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
037 import org.qedeq.kernel.bo.logic.common.PredicateKey;
038 import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
039 import org.qedeq.kernel.bo.module.ControlVisitor;
040 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
041 import org.qedeq.kernel.bo.module.KernelQedeqBo;
042 import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
043 import org.qedeq.kernel.se.base.list.Element;
044 import org.qedeq.kernel.se.base.list.ElementList;
045 import org.qedeq.kernel.se.base.module.Axiom;
046 import org.qedeq.kernel.se.base.module.ChangedRule;
047 import org.qedeq.kernel.se.base.module.ChangedRuleList;
048 import org.qedeq.kernel.se.base.module.ConditionalProof;
049 import org.qedeq.kernel.se.base.module.FormalProof;
050 import org.qedeq.kernel.se.base.module.FormalProofLine;
051 import org.qedeq.kernel.se.base.module.FormalProofLineList;
052 import org.qedeq.kernel.se.base.module.Formula;
053 import org.qedeq.kernel.se.base.module.FunctionDefinition;
054 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
055 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
056 import org.qedeq.kernel.se.base.module.PredicateDefinition;
057 import org.qedeq.kernel.se.base.module.Proposition;
058 import org.qedeq.kernel.se.base.module.Reason;
059 import org.qedeq.kernel.se.base.module.Rule;
060 import org.qedeq.kernel.se.base.module.Specification;
061 import org.qedeq.kernel.se.base.module.SubstFree;
062 import org.qedeq.kernel.se.base.module.SubstFunc;
063 import org.qedeq.kernel.se.base.module.SubstPred;
064 import org.qedeq.kernel.se.common.CheckLevel;
065 import org.qedeq.kernel.se.common.DefaultSourceFileExceptionList;
066 import org.qedeq.kernel.se.common.IllegalModuleDataException;
067 import org.qedeq.kernel.se.common.LogicalModuleState;
068 import org.qedeq.kernel.se.common.ModuleDataException;
069 import org.qedeq.kernel.se.common.Plugin;
070 import org.qedeq.kernel.se.common.RuleKey;
071 import org.qedeq.kernel.se.common.SourceFileException;
072 import org.qedeq.kernel.se.common.SourceFileExceptionList;
073 import org.qedeq.kernel.se.dto.list.ElementSet;
074
075
076 /**
077 * Checks if all formulas of a QEDEQ module are well formed.
078 * This plugin assumes all required modules are loaded!
079 *
080 * @author Michael Meyling
081 */
082 public final class WellFormedCheckerExecutor extends ControlVisitor implements PluginExecutor {
083
084 /** This class. */
085 private static final Class CLASS = WellFormedCheckerExecutor.class;
086
087 /** Class definition via formula rule key. */
088 private static final RuleKey CLASS_DEFINITION_VIA_FORMULA_RULE
089 = new RuleKey("CLASS_DEFINITION_BY_FORMULA", "1.00.00");
090
091 /** Existence checker for predicate and function constants and rules. */
092 private ModuleConstantsExistenceCheckerImpl existence;
093
094 /** Factory for generating new checkers. */
095 private FormulaCheckerFactory checkerFactory = null;
096
097 /** Parameters for checker. */
098 private Parameters parameters;
099
100 /**
101 * Constructor.
102 *
103 * @param plugin This plugin we work for.
104 * @param qedeq QEDEQ BO object.
105 * @param parameters Parameters.
106 */
107 WellFormedCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
108 final Parameters parameters) {
109 super(plugin, qedeq);
110 final String method = "QedeqBoFormalLogicChecker(Plugin, KernelQedeqBo, Map)";
111 this.parameters = parameters;
112 final String checkerFactoryClass = parameters.getString("checkerFactory");
113 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
114 try {
115 Class cl = Class.forName(checkerFactoryClass);
116 checkerFactory = (FormulaCheckerFactory) cl.newInstance();
117 } catch (ClassNotFoundException e) {
118 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class not in class path: "
119 + checkerFactoryClass, e);
120 } catch (InstantiationException e) {
121 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class could not be instanciated: "
122 + checkerFactoryClass, e);
123 } catch (IllegalAccessException e) {
124 Trace.fatal(CLASS, this, method,
125 "Programming error, access for instantiation failed for model: "
126 + checkerFactoryClass, e);
127 } catch (RuntimeException e) {
128 Trace.fatal(CLASS, this, method,
129 "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
130 }
131 }
132 // fallback is the default checker factory
133 if (checkerFactory == null) {
134 checkerFactory = new FormulaCheckerFactoryImpl();
135 }
136 }
137
138 private Parameters getParameters() {
139 return parameters;
140 }
141
142 public Object executePlugin() {
143 if (getQedeqBo().isChecked()) {
144 return Boolean.TRUE;
145 }
146 QedeqLog.getInstance().logRequest(
147 "Check logical well formedness", getQedeqBo().getUrl());
148 getServices().loadModule(getQedeqBo().getModuleAddress());
149 if (!getQedeqBo().isLoaded()) {
150 final String msg = "Check of logical correctness failed";
151 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
152 "Module could not even be loaded.");
153 return Boolean.FALSE;
154 }
155 getServices().loadRequiredModules(getQedeqBo().getModuleAddress());
156 if (!getQedeqBo().hasLoadedRequiredModules()) {
157 final String msg = "Check of logical well formedness failed";
158 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
159 "Not all required modules could be loaded.");
160 return Boolean.FALSE;
161 }
162 getQedeqBo().setLogicalProgressState(LogicalModuleState.STATE_EXTERNAL_CHECKING);
163 final SourceFileExceptionList sfl = new DefaultSourceFileExceptionList();
164 final Map rules = new HashMap(); // map RuleKey to KernelQedeqBo
165 KernelModuleReferenceList list = (KernelModuleReferenceList) getQedeqBo().getRequiredModules();
166 for (int i = 0; i < list.size(); i++) {
167 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
168 final WellFormedCheckerExecutor checker = new WellFormedCheckerExecutor(getPlugin(),
169 list.getKernelQedeqBo(i), getParameters());
170 checker.executePlugin();
171 if (!list.getKernelQedeqBo(i).isChecked()) {
172 ModuleDataException md = new CheckRequiredModuleException(
173 LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
174 LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
175 + list.getQedeqBo(i).getModuleAddress(),
176 list.getModuleContext(i));
177 sfl.add(getQedeqBo().createSourceFileException(getPlugin(), md));
178 }
179 final ModuleConstantsExistenceChecker existenceChecker
180 = list.getKernelQedeqBo(i).getExistenceChecker();
181 if (existenceChecker != null) {
182 final Iterator iter = existenceChecker.getRules().keySet().iterator();
183 while (iter.hasNext()) {
184 final RuleKey key = (RuleKey) iter.next();
185 final KernelQedeqBo newQedeq = existenceChecker.getQedeq(key);
186 final KernelQedeqBo previousQedeq = (KernelQedeqBo) rules.get(key);
187 if (previousQedeq != null && !newQedeq.equals(previousQedeq)) {
188 ModuleDataException md = new CheckRequiredModuleException(
189 LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_CODE,
190 LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_TEXT
191 + key + " " + previousQedeq.getUrl() + " " + newQedeq.getUrl(),
192 list.getModuleContext(i));
193 sfl.add(getQedeqBo().createSourceFileException(getPlugin(), md));
194 } else {
195 rules.put(key, newQedeq);
196 }
197 }
198 }
199 }
200 // has at least one import errors?
201 if (sfl.size() > 0) {
202 getQedeqBo().setLogicalFailureState(LogicalModuleState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
203 final String msg = "Check of logical well formedness failed";
204 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
205 StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
206 return Boolean.FALSE;
207 }
208 getQedeqBo().setLogicalProgressState(LogicalModuleState.STATE_INTERNAL_CHECKING);
209
210 try {
211 traverse();
212 } catch (SourceFileExceptionList e) {
213 getQedeqBo().setLogicalFailureState(LogicalModuleState.STATE_INTERNAL_CHECKING_FAILED, e);
214 getQedeqBo().setExistenceChecker(existence);
215 final String msg = "Check of logical well formedness failed";
216 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
217 StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
218 return Boolean.FALSE;
219 }
220 getQedeqBo().setChecked(existence);
221 QedeqLog.getInstance().logSuccessfulReply(
222 "Check of logical well formedness successful", getQedeqBo().getUrl());
223 return Boolean.TRUE;
224 }
225
226 public void traverse() throws SourceFileExceptionList {
227 try {
228 this.existence = new ModuleConstantsExistenceCheckerImpl(getQedeqBo());
229 } catch (ModuleDataException me) {
230 addError(me);
231 throw getErrorList();
232 }
233 super.traverse();
234
235 // check if we have the important module parts
236 setLocationWithinModule("");
237 if (getQedeqBo().getQedeq().getHeader() == null) {
238 addError(new IllegalModuleDataException(
239 LogicErrors.MODULE_HAS_NO_HEADER_CODE,
240 LogicErrors.MODULE_HAS_NO_HEADER_TEXT,
241 getCurrentContext()));
242 }
243 if (getQedeqBo().getQedeq().getHeader().getSpecification() == null) {
244 addError(new IllegalModuleDataException(
245 LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_CODE,
246 LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_TEXT,
247 getCurrentContext()));
248 }
249 }
250
251 public void visitEnter(final Specification specification) throws ModuleDataException {
252 if (specification == null) {
253 return;
254 }
255 final String context = getCurrentContext().getLocationWithinModule();
256 // we start checking if we have a correct version format
257 setLocationWithinModule(context + ".getRuleVersion()");
258 final String version = specification.getRuleVersion();
259 try {
260 new Version(version);
261 } catch (RuntimeException e) {
262 addError(new IllegalModuleDataException(
263 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
264 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
265 getCurrentContext()));
266 }
267 }
268
269 public void visitEnter(final Axiom axiom) throws ModuleDataException {
270 if (axiom == null) {
271 return;
272 }
273 final String context = getCurrentContext().getLocationWithinModule();
274 // we start checking
275 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
276 if (axiom.getFormula() != null) {
277 setLocationWithinModule(context + ".getFormula().getElement()");
278 final Formula formula = axiom.getFormula();
279 LogicalCheckExceptionList list =
280 checkerFactory.createFormulaChecker().checkFormula(
281 formula.getElement(), getCurrentContext(), existence);
282 for (int i = 0; i < list.size(); i++) {
283 addError(list.get(i));
284 }
285 } else {
286 getNodeBo().setWellFormed(CheckLevel.FAILURE);
287 }
288 // if we found no errors this node is ok
289 if (!getNodeBo().isNotWellFormed()) {
290 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
291 }
292 setLocationWithinModule(context);
293 setBlocked(true);
294 }
295
296 public void visitLeave(final Axiom axiom) {
297 setBlocked(false);
298 }
299
300 public void visitEnter(final PredicateDefinition definition)
301 throws ModuleDataException {
302 if (definition == null) {
303 return;
304 }
305 final String context = getCurrentContext().getLocationWithinModule();
306 // we start checking
307 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
308 final PredicateKey predicateKey = new PredicateKey(definition.getName(),
309 definition.getArgumentNumber());
310 // we misuse a do loop to be able to break
311 do {
312 if (existence.predicateExists(predicateKey)) {
313 addError(new IllegalModuleDataException(
314 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
315 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicateKey,
316 getCurrentContext()));
317 break;
318 }
319 if (definition.getFormula() == null) {
320 addError(new IllegalModuleDataException(
321 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
322 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
323 getCurrentContext()));
324 break;
325 }
326 final Element completeFormula = definition.getFormula().getElement();
327 if (completeFormula == null) {
328 addError(new IllegalModuleDataException(
329 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
330 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
331 getCurrentContext()));
332 break;
333 }
334 setLocationWithinModule(context + ".getFormula().getElement()");
335 if (completeFormula.isAtom()) {
336 addError(new IllegalModuleDataException(
337 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
338 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
339 getCurrentContext()));
340 break;
341 }
342 final ElementList equi = completeFormula.getList();
343 final String operator = equi.getOperator();
344 if (!operator.equals(FormulaCheckerImpl.EQUIVALENCE_OPERATOR)
345 || equi.size() != 2) {
346 addError(new IllegalModuleDataException(
347 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
348 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
349 getCurrentContext()));
350 break;
351 }
352 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(0)");
353 if (equi.getElement(0).isAtom()) {
354 addError(new IllegalModuleDataException(
355 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
356 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
357 getCurrentContext()));
358 break;
359 }
360 final ElementList predicate = equi.getElement(0).getList();
361 if (predicate.getOperator() != FormulaCheckerImpl.PREDICATE_CONSTANT) {
362 addError(new IllegalModuleDataException(
363 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
364 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
365 getCurrentContext()));
366 break;
367 }
368 final Element definingFormula = equi.getElement(1);
369
370 final ElementSet free = FormulaUtility.getFreeSubjectVariables(definingFormula);
371 for (int i = 0; i < predicate.size(); i++) {
372 setLocationWithinModule(context
373 + ".getFormula().getElement().getList().getElement(0).getList().getElement(" + i + ")");
374 if (i == 0) {
375 if (!predicate.getElement(0).isAtom()
376 || !EqualsUtility.equals(definition.getName(),
377 predicate.getElement(0).getAtom().getString())) {
378 addError(new IllegalModuleDataException(
379 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_CODE,
380 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_TEXT
381 + StringUtility.quote(definition.getName()) + " - "
382 + StringUtility.quote(predicate.getElement(0).getAtom().getString()),
383 getCurrentContext()));
384 continue;
385 }
386 } else if (!FormulaUtility.isSubjectVariable(predicate.getElement(i))) {
387 addError(new IllegalModuleDataException(
388 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
389 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT + predicate.getElement(i),
390 getCurrentContext()));
391 continue;
392 }
393 setLocationWithinModule(context
394 + ".getFormula().getElement().getList().getElement(1)");
395 if (i != 0 && !free.contains(predicate.getElement(i))) {
396 addError(new IllegalModuleDataException(
397 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
398 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT + predicate.getElement(i),
399 getCurrentContext()));
400 }
401 }
402 setLocationWithinModule(context + ".getFormula().getElement()");
403 if (predicate.size() - 1 != free.size()) {
404 addError(new IllegalModuleDataException(
405 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
406 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
407 getCurrentContext()));
408 }
409 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
410 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
411 definingFormula, getCurrentContext(), existence);
412 for (int i = 0; i < list.size(); i++) {
413 addError(list.get(i));
414 }
415 if (list.size() > 0) {
416 break;
417 }
418 setLocationWithinModule(context + ".getFormula().getElement().getList()");
419 final PredicateConstant constant = new PredicateConstant(predicateKey,
420 equi, getCurrentContext());
421 setLocationWithinModule(context);
422 if (existence.predicateExists(predicateKey)) {
423 addError(new IllegalModuleDataException(
424 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
425 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
426 + predicateKey, getCurrentContext()));
427 break;
428 }
429 existence.add(constant);
430 // a final check, we don't expect any errors here, but hey - we want to be very sure!
431 setLocationWithinModule(context + ".getFormula().getElement().getList()");
432 final LogicalCheckExceptionList errorlist = checkerFactory.createFormulaChecker()
433 .checkFormula(completeFormula, getCurrentContext(), existence);
434 for (int i = 0; i < errorlist.size(); i++) {
435 addError(errorlist.get(i));
436 }
437 } while (false);
438
439 // check if we just found the identity operator
440 setLocationWithinModule(context);
441 if ("2".equals(predicateKey.getArguments())
442 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
443 existence.setIdentityOperatorDefined(predicateKey.getName(),
444 (KernelQedeqBo) getQedeqBo(), getCurrentContext());
445 }
446 // if we found no errors this node is ok
447 if (!getNodeBo().isNotWellFormed()) {
448 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
449 }
450 setBlocked(true);
451 }
452
453 public void visitLeave(final PredicateDefinition definition) {
454 setBlocked(false);
455 }
456
457 public void visitEnter(final InitialPredicateDefinition definition)
458 throws ModuleDataException {
459 if (definition == null) {
460 return;
461 }
462 final String context = getCurrentContext().getLocationWithinModule();
463 // we start checking
464 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
465 final PredicateKey predicateKey = new PredicateKey(
466 definition.getName(), definition.getArgumentNumber());
467 setLocationWithinModule(context);
468 if (existence.predicateExists(predicateKey)) {
469 addError(new IllegalModuleDataException(
470 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
471 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
472 + predicateKey, getCurrentContext()));
473 }
474 existence.add(definition);
475 // check if we just found the identity operator
476 if ("2".equals(predicateKey.getArguments())
477 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
478 existence.setIdentityOperatorDefined(predicateKey.getName(),
479 (KernelQedeqBo) getQedeqBo(), getCurrentContext());
480 }
481 // if we found no errors this node is ok
482 if (!getNodeBo().isNotWellFormed()) {
483 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
484 }
485 setBlocked(true);
486 }
487
488 public void visitLeave(final InitialPredicateDefinition definition) {
489 setBlocked(false);
490 }
491
492 public void visitEnter(final InitialFunctionDefinition definition)
493 throws ModuleDataException {
494 if (definition == null) {
495 return;
496 }
497 final String context = getCurrentContext().getLocationWithinModule();
498 // we start checking
499 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
500 final FunctionKey function = new FunctionKey(definition.getName(),
501 definition.getArgumentNumber());
502 if (existence.functionExists(function)) {
503 addError(new IllegalModuleDataException(
504 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
505 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT + function,
506 getCurrentContext()));
507 }
508 existence.add(definition);
509 setLocationWithinModule(context);
510 // if we found no errors this node is ok
511 if (!getNodeBo().isNotWellFormed()) {
512 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
513 }
514 setBlocked(true);
515 }
516
517 public void visitLeave(final InitialFunctionDefinition definition) {
518 setBlocked(false);
519 }
520
521 public void visitEnter(final FunctionDefinition definition)
522 throws ModuleDataException {
523 if (definition == null) {
524 return;
525 }
526 final String context = getCurrentContext().getLocationWithinModule();
527 // we start checking
528 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
529 final FunctionKey function = new FunctionKey(definition.getName(),
530 definition.getArgumentNumber());
531 // we misuse a do loop to be able to break
532 do {
533 if (existence.functionExists(function)) {
534 addError(new IllegalModuleDataException(
535 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
536 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT
537 + function, getCurrentContext()));
538 break;
539 }
540 if (definition.getFormula() == null) {
541 addError(new IllegalModuleDataException(
542 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
543 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
544 getCurrentContext()));
545 break;
546 }
547 final Formula formulaArgument = definition.getFormula();
548 setLocationWithinModule(context + ".getFormula()");
549 if (formulaArgument.getElement() == null || formulaArgument.getElement().isAtom()) {
550 addError(new IllegalModuleDataException(
551 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
552 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
553 getCurrentContext()));
554 break;
555 }
556 final ElementList formula = formulaArgument.getElement().getList();
557 setLocationWithinModule(context + ".getFormula().getElement().getList()");
558 if (!existence.identityOperatorExists()) {
559 addError(new IllegalModuleDataException(
560 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE,
561 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT,
562 getCurrentContext()));
563 break;
564 }
565 if (!FormulaCheckerImpl.PREDICATE_CONSTANT.equals(formula.getOperator())) {
566 addError(new IllegalModuleDataException(
567 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
568 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
569 getCurrentContext()));
570 break;
571 }
572 if (formula.size() != 3) {
573 addError(new IllegalModuleDataException(
574 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
575 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
576 getCurrentContext()));
577 break;
578 }
579 if (!formula.getElement(0).isAtom()) {
580 addError(new IllegalModuleDataException(
581 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
582 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
583 getCurrentContext()));
584 break;
585 }
586 if (!EqualsUtility.equals(existence.getIdentityOperator(),
587 formula.getElement(0).getAtom().getString())) {
588 addError(new IllegalModuleDataException(
589 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
590 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
591 getCurrentContext()));
592 break;
593 }
594 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
595 if (formula.getElement(1).isAtom()) {
596 addError(new IllegalModuleDataException(
597 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
598 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
599 getCurrentContext()));
600 break;
601 }
602 final ElementList functionConstant = formula.getElement(1).getList();
603 if (!FormulaCheckerImpl.FUNCTION_CONSTANT.equals(functionConstant.getOperator())) {
604 addError(new IllegalModuleDataException(
605 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
606 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
607 getCurrentContext()));
608 break;
609 }
610 setLocationWithinModule(context
611 + ".getFormula().getElement().getList().getElement(1).getList()");
612 final int size = functionConstant.size();
613 if (!("" + (size - 1)).equals(definition.getArgumentNumber())) {
614 addError(new IllegalModuleDataException(
615 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
616 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
617 getCurrentContext()));
618 break;
619 }
620 setLocationWithinModule(context
621 + ".getFormula().getElement().getList().getElement(1).getList().getElement(0)");
622 if (!functionConstant.getElement(0).isAtom()) {
623 addError(new IllegalModuleDataException(
624 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
625 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
626 getCurrentContext()));
627 break;
628 }
629 if (!EqualsUtility.equals(definition.getName(),
630 functionConstant.getElement(0).getAtom().getString())) {
631 addError(new IllegalModuleDataException(
632 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
633 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
634 getCurrentContext()));
635 break;
636 }
637 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
638 if (formula.getElement(2).isAtom()) {
639 addError(new IllegalModuleDataException(
640 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_CODE,
641 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_TEXT,
642 getCurrentContext()));
643 break;
644 }
645 final ElementList term = formula.getElement(2).getList();
646 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
647 final ElementSet free = FormulaUtility.getFreeSubjectVariables(term);
648 if (size - 1 != free.size()) {
649 addError(new IllegalModuleDataException(
650 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
651 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
652 getCurrentContext()));
653 break;
654 }
655 if (functionConstant.getElement(0).isList()
656 || !EqualsUtility.equals(function.getName(),
657 functionConstant.getElement(0).getAtom().getString())) {
658 }
659 for (int i = 1; i < size; i++) {
660 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"
661 + ".getList().getElement(" + i + ")");
662 if (!FormulaUtility.isSubjectVariable(functionConstant.getElement(i))) {
663 addError(new IllegalModuleDataException(
664 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
665 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT
666 + functionConstant.getElement(i), getCurrentContext()));
667 }
668 if (!free.contains(functionConstant.getElement(i))) {
669 addError(new IllegalModuleDataException(
670 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
671 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT
672 + functionConstant.getElement(i), getCurrentContext()));
673 }
674 }
675 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
676 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker()
677 .checkTerm(term, getCurrentContext(), existence);
678 for (int i = 0; i < list.size(); i++) {
679 addError(list.get(i));
680 }
681 if (list.size() > 0) {
682 break;
683 }
684 setLocationWithinModule(context + ".getFormula().getElement().getList()");
685 existence.add(new FunctionConstant(function, formula, getCurrentContext()));
686 // a final check, we don't expect any errors here, but hey - we want to be very sure!
687 final LogicalCheckExceptionList listComplete = checkerFactory.createFormulaChecker()
688 .checkFormula(formulaArgument.getElement(), getCurrentContext(), existence);
689 for (int i = 0; i < listComplete.size(); i++) {
690 addError(listComplete.get(i));
691 }
692 } while (false);
693 setLocationWithinModule(context);
694 // if we found no errors this node is ok
695 if (!getNodeBo().isNotWellFormed()) {
696 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
697 }
698 setBlocked(true);
699 }
700
701 public void visitLeave(final FunctionDefinition definition) {
702 setBlocked(false);
703 }
704
705 public void visitEnter(final Proposition proposition)
706 throws ModuleDataException {
707 if (proposition == null) {
708 return;
709 }
710 final String context = getCurrentContext().getLocationWithinModule();
711 // we start checking
712 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
713 if (proposition.getFormula() != null) {
714 setLocationWithinModule(context + ".getFormula().getElement()");
715 final Formula formula = proposition.getFormula();
716 LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
717 formula.getElement(), getCurrentContext(), existence);
718 for (int i = 0; i < list.size(); i++) {
719 addError(list.get(i));
720 }
721 } else { // no formula
722 getNodeBo().setWellFormed(CheckLevel.FAILURE);
723 }
724 if (proposition.getFormalProofList() != null) {
725 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
726 final FormalProof proof = proposition.getFormalProofList().get(i);
727 if (proof != null) {
728 final FormalProofLineList list = proof.getFormalProofLineList();
729 setLocationWithinModule(context + ".getFormalProofList().get("
730 + i + ").getFormalProofLineList()");
731 checkFormalProof(list);
732 }
733 }
734 }
735 setLocationWithinModule(context);
736 // if we found no errors this node is ok
737 if (!getNodeBo().isNotWellFormed()) {
738 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
739 }
740 setBlocked(true);
741 }
742
743 /**
744 * Check formal proof formulas.
745 *
746 * @param list List of lines.
747 */
748 private void checkFormalProof(final FormalProofLineList list) {
749 final String context = getCurrentContext().getLocationWithinModule();
750 if (list != null) {
751 for (int i = 0; i < list.size(); i++) {
752 final FormalProofLine line = list.get(i);
753 setLocationWithinModule(context + ".get(" + i + ")");
754 checkProofLine(line);
755 }
756 }
757 }
758
759 /**
760 * Check well-formedness of proof lines.
761 *
762 * @param line Check formulas and terms of this proof line.
763 */
764 private void checkProofLine(final FormalProofLine line) {
765 if (line instanceof ConditionalProof) {
766 checkProofLine((ConditionalProof) line);
767 return;
768 }
769 final String context = getCurrentContext().getLocationWithinModule();
770 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
771 if (line != null) {
772 final Formula formula = line.getFormula();
773 if (formula != null) {
774 setLocationWithinModule(context + ".getFormula().getElement()");
775 elist = checkerFactory.createFormulaChecker().checkFormula(
776 formula.getElement(), getCurrentContext(), existence);
777 for (int k = 0; k < elist.size(); k++) {
778 addError(elist.get(k));
779 }
780 }
781 final Reason reason = line.getReason();
782 if (reason != null) {
783 if (reason instanceof SubstFree) {
784 final SubstFree subst = (SubstFree) reason;
785 if (subst.getSubstFree().getSubstituteTerm() != null) {
786 setLocationWithinModule(context
787 + ".getReason().getSubstFree().getSubstituteTerm()");
788 elist = checkerFactory.createFormulaChecker().checkTerm(
789 subst.getSubstFree().getSubstituteTerm(),
790 getCurrentContext(), existence);
791 }
792 } else if (reason instanceof SubstPred) {
793 final SubstPred subst = (SubstPred) reason;
794 if (subst.getSubstPred().getSubstituteFormula() != null) {
795 setLocationWithinModule(context
796 + ".getReason().getSubstPred().getSubstituteFormula()");
797 elist = checkerFactory.createFormulaChecker().checkFormula(
798 subst.getSubstPred().getSubstituteFormula(),
799 getCurrentContext(), existence);
800 }
801 } else if (reason instanceof SubstFunc) {
802 final SubstFunc subst = (SubstFunc) reason;
803 if (subst.getSubstFunc().getSubstituteTerm() != null) {
804 setLocationWithinModule(context
805 + ".getReason().getSubstFunc().getSubstituteTerm()");
806 elist = checkerFactory.createFormulaChecker().checkTerm(
807 subst.getSubstFunc().getSubstituteTerm(),
808 getCurrentContext(), existence);
809 }
810 }
811 for (int k = 0; k < elist.size(); k++) {
812 addError(elist.get(k));
813 }
814 }
815 }
816 }
817
818 /**
819 * Check well-formedness of proof lines.
820 *
821 * @param line Check formulas and terms of this proof line.
822 */
823 private void checkProofLine(final ConditionalProof line) {
824 final String context = getCurrentContext().getLocationWithinModule();
825 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
826 if (line != null) {
827 {
828 final Formula formula = line.getFormula();
829 if (formula != null && formula.getElement() != null) {
830 setLocationWithinModule(context + ".getFormula().getElement()");
831 elist = checkerFactory.createFormulaChecker().checkFormula(
832 formula.getElement(), getCurrentContext(), existence);
833 for (int k = 0; k < elist.size(); k++) {
834 addError(elist.get(k));
835 }
836 }
837 }
838 if (line.getHypothesis() != null) {
839 final Formula formula = line.getHypothesis().getFormula();;
840 if (formula != null && formula.getElement() != null) {
841 setLocationWithinModule(context
842 + ".getHypothesis().getFormula().getElement()");
843 elist = checkerFactory.createFormulaChecker().checkFormula(
844 formula.getElement(), getCurrentContext(), existence);
845 for (int k = 0; k < elist.size(); k++) {
846 addError(elist.get(k));
847 }
848 }
849 }
850 if (line.getFormalProofLineList() != null) {
851 setLocationWithinModule(context + ".getFormalProofLineList()");
852 checkFormalProof(line.getFormalProofLineList());
853 }
854 if (line.getConclusion() != null) {
855 final Formula formula = line.getConclusion().getFormula();;
856 if (formula != null && formula.getElement() != null) {
857 setLocationWithinModule(context
858 + ".getConclusion().getFormula().getElement()");
859 elist = checkerFactory.createFormulaChecker().checkFormula(
860 formula.getElement(), getCurrentContext(), existence);
861 for (int k = 0; k < elist.size(); k++) {
862 addError(elist.get(k));
863 }
864 }
865 }
866 }
867 }
868
869 public void visitLeave(final Proposition definition) {
870 setBlocked(false);
871 }
872
873 public void visitEnter(final Rule rule) throws ModuleDataException {
874 final String context = getCurrentContext().getLocationWithinModule();
875 // we start checking
876 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
877 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
878 if (rule.getName() != null && rule.getName().length() > 0 && rule.getVersion() != null
879 && rule.getVersion().length() > 0) {
880 try {
881 setLocationWithinModule(context + ".getVersion()");
882 new Version(rule.getVersion());
883 } catch (RuntimeException e) {
884 addError(new IllegalModuleDataException(
885 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
886 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
887 getCurrentContext()));
888 }
889 if (existence.ruleExists(ruleKey)) {
890 addError(new IllegalModuleDataException(
891 LogicErrors.RULE_ALREADY_DEFINED_CODE,
892 LogicErrors.RULE_ALREADY_DEFINED_TEXT
893 + ruleKey + " " + existence.getQedeq(ruleKey).getUrl(),
894 getCurrentContext()));
895 } else {
896 if (CLASS_DEFINITION_VIA_FORMULA_RULE.equals(ruleKey)) {
897 // TODO 20080114 m31: check if this rule can be proposed
898 // are the preconditions for using this rule fulfilled?
899 existence.setClassOperatorModule(getQedeqBo(),
900 getCurrentContext());
901 }
902 existence.add(ruleKey, rule);
903 }
904 if (rule.getChangedRuleList() != null) {
905 final ChangedRuleList list = rule.getChangedRuleList();
906 for (int i = 0; i < list.size(); i++) {
907 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ")");
908 final ChangedRule r = list.get(i);
909 if (r == null || r.getName() == null || r.getName().length() <= 0
910 || r.getVersion() == null || r.getVersion().length() <= 0) {
911 addError(new IllegalModuleDataException(
912 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
913 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
914 + (r == null ? "null" : r.getName() + " [" + r.getVersion() + "]"),
915 getCurrentContext()));
916 continue;
917 }
918 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
919 final String ruleName = r.getName();
920 final String ruleVersion = r.getVersion();
921 try {
922 new Version(ruleVersion);
923 } catch (RuntimeException e) {
924 addError(new IllegalModuleDataException(
925 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
926 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
927 getCurrentContext()));
928 }
929 RuleKey key1 = getLocalRuleKey(ruleName);
930 if (key1 == null) {
931 key1 = existence.getParentRuleKey(ruleName);
932 }
933 if (key1 == null) {
934 addError(new IllegalModuleDataException(
935 LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_CODE,
936 LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_TEXT
937 + ruleName, getCurrentContext()));
938 } else {
939 final RuleKey key2 = new RuleKey(ruleName, ruleVersion);
940 if (existence.ruleExists(key2)) {
941 addError(new IllegalModuleDataException(
942 LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_CODE,
943 LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_TEXT
944 + ruleName, getCurrentContext(), getQedeqBo().getLabels()
945 .getRuleContext(key2)));
946 } else {
947 try {
948 if (!Version.less(key1.getVersion(), key2.getVersion())) {
949 addError(new IllegalModuleDataException(
950 LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_CODE,
951 LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_TEXT
952 + key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels()
953 .getRuleContext(key2)));
954 }
955 } catch (RuntimeException e) {
956 addError(new IllegalModuleDataException(
957 LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_CODE,
958 LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_TEXT
959 + key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels()
960 .getRuleContext(key2)));
961 }
962 }
963 existence.add(key2, rule);
964 }
965 }
966 }
967 } else {
968 addError(new IllegalModuleDataException(
969 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
970 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
971 + ruleKey, getCurrentContext()));
972 }
973 // if we found no errors this node is ok
974 if (!getNodeBo().isNotWellFormed()) {
975 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
976 }
977 setBlocked(true);
978 }
979
980 public void visitLeave(final Rule rule) {
981 setBlocked(false);
982 }
983
984 protected void addError(final ModuleDataException me) {
985 if (getNodeBo() != null) {
986 getNodeBo().setWellFormed(CheckLevel.FAILURE);
987 }
988 super.addError(me);
989 }
990
991 protected void addError(final SourceFileException me) {
992 if (getNodeBo() != null) {
993 getNodeBo().setWellFormed(CheckLevel.FAILURE);
994 }
995 super.addError(me);
996 }
997
998 }
|