1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.bo.service.logic;
17
18 import java.util.HashMap;
19 import java.util.Iterator;
20 import java.util.Map;
21
22 import org.qedeq.base.io.Parameters;
23 import org.qedeq.base.io.Version;
24 import org.qedeq.base.trace.Trace;
25 import org.qedeq.base.utility.EqualsUtility;
26 import org.qedeq.base.utility.StringUtility;
27 import org.qedeq.kernel.bo.log.QedeqLog;
28 import org.qedeq.kernel.bo.logic.FormulaCheckerFactoryImpl;
29 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
30 import org.qedeq.kernel.bo.logic.common.FormulaCheckerFactory;
31 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
32 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
33 import org.qedeq.kernel.bo.logic.common.FunctionKey;
34 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
35 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
36 import org.qedeq.kernel.bo.logic.common.PredicateKey;
37 import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
38 import org.qedeq.kernel.bo.module.InternalModuleServiceCall;
39 import org.qedeq.kernel.bo.module.InternalServiceJob;
40 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
41 import org.qedeq.kernel.bo.module.KernelQedeqBo;
42 import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
43 import org.qedeq.kernel.bo.service.basis.ControlVisitor;
44 import org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor;
45 import org.qedeq.kernel.bo.service.dependency.LoadRequiredModulesPlugin;
46 import org.qedeq.kernel.se.base.list.Element;
47 import org.qedeq.kernel.se.base.list.ElementList;
48 import org.qedeq.kernel.se.base.module.Axiom;
49 import org.qedeq.kernel.se.base.module.ChangedRule;
50 import org.qedeq.kernel.se.base.module.ChangedRuleList;
51 import org.qedeq.kernel.se.base.module.ConditionalProof;
52 import org.qedeq.kernel.se.base.module.FormalProof;
53 import org.qedeq.kernel.se.base.module.FormalProofLine;
54 import org.qedeq.kernel.se.base.module.FormalProofLineList;
55 import org.qedeq.kernel.se.base.module.Formula;
56 import org.qedeq.kernel.se.base.module.FunctionDefinition;
57 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
58 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
59 import org.qedeq.kernel.se.base.module.PredicateDefinition;
60 import org.qedeq.kernel.se.base.module.Proposition;
61 import org.qedeq.kernel.se.base.module.Reason;
62 import org.qedeq.kernel.se.base.module.Rule;
63 import org.qedeq.kernel.se.base.module.Specification;
64 import org.qedeq.kernel.se.base.module.SubstFree;
65 import org.qedeq.kernel.se.base.module.SubstFunc;
66 import org.qedeq.kernel.se.base.module.SubstPred;
67 import org.qedeq.kernel.se.common.CheckLevel;
68 import org.qedeq.kernel.se.common.IllegalModuleDataException;
69 import org.qedeq.kernel.se.common.ModuleDataException;
70 import org.qedeq.kernel.se.common.ModuleService;
71 import org.qedeq.kernel.se.common.RuleKey;
72 import org.qedeq.kernel.se.common.SourceFileException;
73 import org.qedeq.kernel.se.common.SourceFileExceptionList;
74 import org.qedeq.kernel.se.dto.list.ElementSet;
75 import org.qedeq.kernel.se.state.WellFormedState;
76 import org.qedeq.kernel.se.visitor.InterruptException;
77
78
79
80
81
82
83
84
85 public final class WellFormedCheckerExecutor extends ControlVisitor implements ModuleServicePluginExecutor {
86
87
88 private static final Class CLASS = WellFormedCheckerExecutor.class;
89
90
91 private static final RuleKey CLASS_DEFINITION_VIA_FORMULA_RULE
92 = new RuleKey("CLASS_DEFINITION_BY_FORMULA", "1.00.00");
93
94
95 private ModuleConstantsExistenceCheckerImpl existence;
96
97
98 private FormulaCheckerFactory checkerFactory = null;
99
100
101
102
103
104
105
106
107 WellFormedCheckerExecutor(final ModuleService plugin, final KernelQedeqBo qedeq,
108 final Parameters parameters) {
109 super(plugin, qedeq);
110 final String method = "QedeqBoFormalLogicChecker(Plugin, KernelQedeqBo, Map)";
111 final String checkerFactoryClass = parameters.getString("checkerFactory");
112 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
113 try {
114 Class cl = Class.forName(checkerFactoryClass);
115 checkerFactory = (FormulaCheckerFactory) cl.newInstance();
116 } catch (ClassNotFoundException e) {
117 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class not in class path: "
118 + checkerFactoryClass, e);
119 } catch (InstantiationException e) {
120 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class could not be instanciated: "
121 + checkerFactoryClass, e);
122 } catch (IllegalAccessException e) {
123 Trace.fatal(CLASS, this, method,
124 "Programming error, access for instantiation failed for model: "
125 + checkerFactoryClass, e);
126 } catch (RuntimeException e) {
127 Trace.fatal(CLASS, this, method,
128 "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
129 }
130 }
131
132 if (checkerFactory == null) {
133 checkerFactory = new FormulaCheckerFactoryImpl();
134 }
135 }
136
137 public Object executePlugin(final InternalModuleServiceCall call, final Object data) throws InterruptException {
138 if (getKernelQedeqBo().isWellFormed()) {
139 return Boolean.TRUE;
140 }
141 QedeqLog.getInstance().logRequest(
142 "Check logical well formedness", getKernelQedeqBo().getUrl());
143 if (!getKernelQedeqBo().hasLoadedRequiredModules()) {
144 getServices().executePlugin(call.getInternalServiceProcess(),
145 LoadRequiredModulesPlugin.class.getName(), getKernelQedeqBo(), null);
146 }
147 if (!getKernelQedeqBo().hasLoadedRequiredModules()) {
148 final String msg = "Check of logical well formedness failed";
149 QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
150 "Not all required modules could be loaded.");
151 return Boolean.FALSE;
152 }
153 getKernelQedeqBo().setWellFormedProgressState(WellFormedState.STATE_EXTERNAL_CHECKING);
154 getKernelQedeqBo().getLabels().resetNodesToWellFormedUnchecked();
155 final SourceFileExceptionList sfl = new SourceFileExceptionList();
156 final Map rules = new HashMap();
157 final KernelModuleReferenceList list = getKernelQedeqBo().getKernelRequiredModules();
158 for (int i = 0; i < list.size(); i++) {
159 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
160 getServices().checkWellFormedness(call.getInternalServiceProcess(), list.getKernelQedeqBo(i));
161 if (!list.getKernelQedeqBo(i).isWellFormed()) {
162 ModuleDataException md = new CheckRequiredModuleException(
163 LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
164 LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
165 + list.getQedeqBo(i).getModuleAddress(),
166 list.getModuleContext(i));
167 sfl.add(getKernelQedeqBo().createSourceFileException(getService(), md));
168 }
169 final ModuleConstantsExistenceChecker existenceChecker
170 = list.getKernelQedeqBo(i).getExistenceChecker();
171 if (existenceChecker != null) {
172 final Iterator iter = existenceChecker.getRules().keySet().iterator();
173 while (iter.hasNext()) {
174 final RuleKey key = (RuleKey) iter.next();
175 final KernelQedeqBo newQedeq = existenceChecker.getQedeq(key);
176 final KernelQedeqBo previousQedeq = (KernelQedeqBo) rules.get(key);
177 if (previousQedeq != null && !newQedeq.equals(previousQedeq)) {
178 ModuleDataException md = new CheckRequiredModuleException(
179 LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_CODE,
180 LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_TEXT
181 + key + " " + previousQedeq.getUrl() + " " + newQedeq.getUrl(),
182 list.getModuleContext(i));
183 sfl.add(getKernelQedeqBo().createSourceFileException(getService(), md));
184 } else {
185 rules.put(key, newQedeq);
186 }
187 }
188 }
189 }
190
191 if (sfl.size() > 0) {
192 getKernelQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
193 final String msg = "Check of logical well formedness failed";
194 QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
195 StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
196 return Boolean.FALSE;
197 }
198 getKernelQedeqBo().setWellFormedProgressState(WellFormedState.STATE_INTERNAL_CHECKING);
199
200 try {
201 traverse(call.getInternalServiceProcess());
202 } catch (SourceFileExceptionList e) {
203 getKernelQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_INTERNAL_CHECKING_FAILED, e);
204 getKernelQedeqBo().setExistenceChecker(existence);
205 final String msg = "Check of logical well formedness failed";
206 QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
207 StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
208 return Boolean.FALSE;
209 }
210 getKernelQedeqBo().setWellFormed(existence);
211 QedeqLog.getInstance().logSuccessfulReply(
212 "Check of logical well formedness successful", getKernelQedeqBo().getUrl());
213 return Boolean.TRUE;
214 }
215
216 public void traverse(final InternalServiceJob process) throws SourceFileExceptionList {
217 try {
218 this.existence = new ModuleConstantsExistenceCheckerImpl(getKernelQedeqBo());
219 } catch (ModuleDataException me) {
220 addError(me);
221 throw getErrorList();
222 }
223 super.traverse(process);
224
225
226 setLocationWithinModule("");
227 if (getKernelQedeqBo().getQedeq().getHeader() == null) {
228 addError(new IllegalModuleDataException(
229 LogicErrors.MODULE_HAS_NO_HEADER_CODE,
230 LogicErrors.MODULE_HAS_NO_HEADER_TEXT,
231 getCurrentContext()));
232 }
233 if (getKernelQedeqBo().getQedeq().getHeader().getSpecification() == null) {
234 addError(new IllegalModuleDataException(
235 LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_CODE,
236 LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_TEXT,
237 getCurrentContext()));
238 }
239 }
240
241 public void visitEnter(final Specification specification) throws ModuleDataException {
242 if (specification == null) {
243 return;
244 }
245 final String context = getCurrentContext().getLocationWithinModule();
246
247 setLocationWithinModule(context + ".getRuleVersion()");
248 final String version = specification.getRuleVersion();
249 try {
250 new Version(version);
251 } catch (RuntimeException e) {
252 addError(new IllegalModuleDataException(
253 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
254 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
255 getCurrentContext()));
256 }
257 }
258
259 public void visitEnter(final Axiom axiom) throws ModuleDataException {
260 if (axiom == null) {
261 return;
262 }
263 final String context = getCurrentContext().getLocationWithinModule();
264
265 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
266 if (axiom.getFormula() != null) {
267 setLocationWithinModule(context + ".getFormula().getElement()");
268 final Formula formula = axiom.getFormula();
269 LogicalCheckExceptionList list =
270 checkerFactory.createFormulaChecker().checkFormula(
271 formula.getElement(), getCurrentContext(), existence);
272 for (int i = 0; i < list.size(); i++) {
273 addError(list.get(i));
274 }
275 } else {
276 getNodeBo().setWellFormed(CheckLevel.FAILURE);
277 }
278
279 if (!getNodeBo().isNotWellFormed()) {
280 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
281 }
282 setLocationWithinModule(context);
283 setBlocked(true);
284 }
285
286 public void visitLeave(final Axiom axiom) {
287 setBlocked(false);
288 }
289
290 public void visitEnter(final PredicateDefinition definition)
291 throws ModuleDataException {
292 if (definition == null) {
293 return;
294 }
295 final String context = getCurrentContext().getLocationWithinModule();
296
297 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
298 final PredicateKey predicateKey = new PredicateKey(definition.getName(),
299 definition.getArgumentNumber());
300
301 do {
302 if (existence.predicateExists(predicateKey)) {
303 addError(new IllegalModuleDataException(
304 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
305 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicateKey,
306 getCurrentContext()));
307 break;
308 }
309 if (definition.getFormula() == null) {
310 addError(new IllegalModuleDataException(
311 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
312 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
313 getCurrentContext()));
314 break;
315 }
316 final Element completeFormula = definition.getFormula().getElement();
317 if (completeFormula == null) {
318 addError(new IllegalModuleDataException(
319 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
320 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
321 getCurrentContext()));
322 break;
323 }
324 setLocationWithinModule(context + ".getFormula().getElement()");
325 if (completeFormula.isAtom()) {
326 addError(new IllegalModuleDataException(
327 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
328 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
329 getCurrentContext()));
330 break;
331 }
332 final ElementList equi = completeFormula.getList();
333 final String operator = equi.getOperator();
334 if (!operator.equals(FormulaCheckerImpl.EQUIVALENCE_OPERATOR)
335 || equi.size() != 2) {
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 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(0)");
343 if (equi.getElement(0).isAtom()) {
344 addError(new IllegalModuleDataException(
345 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
346 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
347 getCurrentContext()));
348 break;
349 }
350 final ElementList predicate = equi.getElement(0).getList();
351 if (predicate.getOperator() != FormulaCheckerImpl.PREDICATE_CONSTANT) {
352 addError(new IllegalModuleDataException(
353 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
354 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
355 getCurrentContext()));
356 break;
357 }
358 final Element definingFormula = equi.getElement(1);
359
360 final ElementSet free = FormulaUtility.getFreeSubjectVariables(definingFormula);
361 for (int i = 0; i < predicate.size(); i++) {
362 setLocationWithinModule(context
363 + ".getFormula().getElement().getList().getElement(0).getList().getElement(" + i + ")");
364 if (i == 0) {
365 if (!predicate.getElement(0).isAtom()
366 || !EqualsUtility.equals(definition.getName(),
367 predicate.getElement(0).getAtom().getString())) {
368 addError(new IllegalModuleDataException(
369 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_CODE,
370 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_TEXT
371 + StringUtility.quote(definition.getName()) + " - "
372 + StringUtility.quote(predicate.getElement(0).getAtom().getString()),
373 getCurrentContext()));
374 continue;
375 }
376 } else if (!FormulaUtility.isSubjectVariable(predicate.getElement(i))) {
377 addError(new IllegalModuleDataException(
378 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
379 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT + predicate.getElement(i),
380 getCurrentContext()));
381 continue;
382 }
383 setLocationWithinModule(context
384 + ".getFormula().getElement().getList().getElement(1)");
385 if (i != 0 && !free.contains(predicate.getElement(i))) {
386 addError(new IllegalModuleDataException(
387 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
388 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT + predicate.getElement(i),
389 getCurrentContext()));
390 }
391 }
392 setLocationWithinModule(context + ".getFormula().getElement()");
393 if (predicate.size() - 1 != free.size()) {
394 addError(new IllegalModuleDataException(
395 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
396 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
397 getCurrentContext()));
398 }
399 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
400 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
401 definingFormula, getCurrentContext(), existence);
402 for (int i = 0; i < list.size(); i++) {
403 addError(list.get(i));
404 }
405 if (list.size() > 0) {
406 break;
407 }
408 setLocationWithinModule(context + ".getFormula().getElement().getList()");
409 final PredicateConstant constant = new PredicateConstant(predicateKey,
410 equi, getCurrentContext());
411 setLocationWithinModule(context);
412 if (existence.predicateExists(predicateKey)) {
413 addError(new IllegalModuleDataException(
414 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
415 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
416 + predicateKey, getCurrentContext()));
417 break;
418 }
419
420 if (!getNodeBo().isNotWellFormed()) {
421 existence.add(constant);
422 setLocationWithinModule(context + ".getFormula().getElement()");
423 final LogicalCheckExceptionList errorlist = checkerFactory.createFormulaChecker()
424 .checkFormula(completeFormula, getCurrentContext(), existence);
425 for (int i = 0; i < errorlist.size(); i++) {
426 addError(errorlist.get(i));
427 }
428 }
429 } while (false);
430
431
432 setLocationWithinModule(context);
433 if ("2".equals(predicateKey.getArguments())
434 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
435 existence.setIdentityOperatorDefined(predicateKey.getName(),
436 getKernelQedeqBo(), getCurrentContext());
437 }
438
439 if (!getNodeBo().isNotWellFormed()) {
440 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
441 }
442 setBlocked(true);
443 }
444
445 public void visitLeave(final PredicateDefinition definition) {
446 setBlocked(false);
447 }
448
449 public void visitEnter(final InitialPredicateDefinition definition)
450 throws ModuleDataException {
451 if (definition == null) {
452 return;
453 }
454 final String context = getCurrentContext().getLocationWithinModule();
455
456 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
457 final PredicateKey predicateKey = new PredicateKey(
458 definition.getName(), definition.getArgumentNumber());
459 setLocationWithinModule(context);
460 if (existence.predicateExists(predicateKey)) {
461 addError(new IllegalModuleDataException(
462 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
463 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
464 + predicateKey, getCurrentContext()));
465 }
466 existence.add(definition);
467
468 if ("2".equals(predicateKey.getArguments())
469 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
470 existence.setIdentityOperatorDefined(predicateKey.getName(),
471 getKernelQedeqBo(), getCurrentContext());
472 }
473
474 if (!getNodeBo().isNotWellFormed()) {
475 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
476 }
477 setBlocked(true);
478 }
479
480 public void visitLeave(final InitialPredicateDefinition definition) {
481 setBlocked(false);
482 }
483
484 public void visitEnter(final InitialFunctionDefinition definition)
485 throws ModuleDataException {
486 if (definition == null) {
487 return;
488 }
489 final String context = getCurrentContext().getLocationWithinModule();
490
491 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
492 final FunctionKey function = new FunctionKey(definition.getName(),
493 definition.getArgumentNumber());
494 if (existence.functionExists(function)) {
495 addError(new IllegalModuleDataException(
496 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
497 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT + function,
498 getCurrentContext()));
499 }
500 existence.add(definition);
501 setLocationWithinModule(context);
502
503 if (!getNodeBo().isNotWellFormed()) {
504 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
505 }
506 setBlocked(true);
507 }
508
509 public void visitLeave(final InitialFunctionDefinition definition) {
510 setBlocked(false);
511 }
512
513 public void visitEnter(final FunctionDefinition definition)
514 throws ModuleDataException {
515 if (definition == null) {
516 return;
517 }
518 final String context = getCurrentContext().getLocationWithinModule();
519
520 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
521 final FunctionKey function = new FunctionKey(definition.getName(),
522 definition.getArgumentNumber());
523
524 do {
525 if (existence.functionExists(function)) {
526 addError(new IllegalModuleDataException(
527 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
528 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT
529 + function, getCurrentContext()));
530 break;
531 }
532 if (definition.getFormula() == null) {
533 addError(new IllegalModuleDataException(
534 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
535 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
536 getCurrentContext()));
537 break;
538 }
539 final Formula formulaArgument = definition.getFormula();
540 setLocationWithinModule(context + ".getFormula()");
541 if (formulaArgument.getElement() == null || formulaArgument.getElement().isAtom()) {
542 addError(new IllegalModuleDataException(
543 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
544 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
545 getCurrentContext()));
546 break;
547 }
548 final ElementList formula = formulaArgument.getElement().getList();
549 setLocationWithinModule(context + ".getFormula().getElement().getList()");
550 if (!existence.identityOperatorExists()) {
551 addError(new IllegalModuleDataException(
552 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE,
553 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT,
554 getCurrentContext()));
555 break;
556 }
557 if (!FormulaCheckerImpl.PREDICATE_CONSTANT.equals(formula.getOperator())) {
558 addError(new IllegalModuleDataException(
559 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
560 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
561 getCurrentContext()));
562 break;
563 }
564 if (formula.size() != 3) {
565 addError(new IllegalModuleDataException(
566 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
567 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
568 getCurrentContext()));
569 break;
570 }
571 if (!formula.getElement(0).isAtom()) {
572 addError(new IllegalModuleDataException(
573 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
574 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
575 getCurrentContext()));
576 break;
577 }
578 if (!EqualsUtility.equals(existence.getIdentityOperator(),
579 formula.getElement(0).getAtom().getString())) {
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 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
587 if (formula.getElement(1).isAtom()) {
588 addError(new IllegalModuleDataException(
589 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
590 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
591 getCurrentContext()));
592 break;
593 }
594 final ElementList functionConstant = formula.getElement(1).getList();
595 if (!FormulaCheckerImpl.FUNCTION_CONSTANT.equals(functionConstant.getOperator())) {
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 setLocationWithinModule(context
603 + ".getFormula().getElement().getList().getElement(1).getList()");
604 final int size = functionConstant.size();
605 if (!("" + (size - 1)).equals(definition.getArgumentNumber())) {
606 addError(new IllegalModuleDataException(
607 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
608 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
609 getCurrentContext()));
610 break;
611 }
612 setLocationWithinModule(context
613 + ".getFormula().getElement().getList().getElement(1).getList().getElement(0)");
614 if (!functionConstant.getElement(0).isAtom()) {
615 addError(new IllegalModuleDataException(
616 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
617 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
618 getCurrentContext()));
619 break;
620 }
621 if (!EqualsUtility.equals(definition.getName(),
622 functionConstant.getElement(0).getAtom().getString())) {
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 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
630 if (formula.getElement(2).isAtom()) {
631 addError(new IllegalModuleDataException(
632 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_CODE,
633 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_TEXT,
634 getCurrentContext()));
635 break;
636 }
637 final ElementList term = formula.getElement(2).getList();
638 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
639 final ElementSet free = FormulaUtility.getFreeSubjectVariables(term);
640 if (size - 1 != free.size()) {
641 addError(new IllegalModuleDataException(
642 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
643 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
644 getCurrentContext()));
645 break;
646 }
647 if (functionConstant.getElement(0).isList()
648 || !EqualsUtility.equals(function.getName(),
649 functionConstant.getElement(0).getAtom().getString())) {
650 addError(new IllegalModuleDataException(
651 LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_CODE,
652 LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_TEXT
653 + function.getName(), getCurrentContext()));
654 }
655 for (int i = 1; i < size; i++) {
656 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"
657 + ".getList().getElement(" + i + ")");
658 if (!FormulaUtility.isSubjectVariable(functionConstant.getElement(i))) {
659 addError(new IllegalModuleDataException(
660 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
661 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT
662 + functionConstant.getElement(i), getCurrentContext()));
663 }
664 if (!free.contains(functionConstant.getElement(i))) {
665 addError(new IllegalModuleDataException(
666 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
667 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT
668 + functionConstant.getElement(i), getCurrentContext()));
669 }
670 }
671 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
672 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker()
673 .checkTerm(term, getCurrentContext(), existence);
674 for (int i = 0; i < list.size(); i++) {
675 addError(list.get(i));
676 }
677 if (list.size() > 0) {
678 break;
679 }
680 setLocationWithinModule(context + ".getFormula().getElement()");
681
682 if (!getNodeBo().isNotWellFormed()) {
683 existence.add(new FunctionConstant(function, formula, getCurrentContext()));
684
685 final LogicalCheckExceptionList listComplete = checkerFactory.createFormulaChecker()
686 .checkFormula(formulaArgument.getElement(), getCurrentContext(), existence);
687 for (int i = 0; i < listComplete.size(); i++) {
688 addError(listComplete.get(i));
689 }
690 }
691 } while (false);
692 setLocationWithinModule(context);
693
694 if (!getNodeBo().isNotWellFormed()) {
695 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
696 }
697 setBlocked(true);
698 }
699
700 public void visitLeave(final FunctionDefinition definition) {
701 setBlocked(false);
702 }
703
704 public void visitEnter(final Proposition proposition)
705 throws ModuleDataException {
706 if (proposition == null) {
707 return;
708 }
709 final String context = getCurrentContext().getLocationWithinModule();
710
711 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
712 if (proposition.getFormula() != null) {
713 setLocationWithinModule(context + ".getFormula().getElement()");
714 final Formula formula = proposition.getFormula();
715 LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
716 formula.getElement(), getCurrentContext(), existence);
717 for (int i = 0; i < list.size(); i++) {
718 addError(list.get(i));
719 }
720 } else {
721 getNodeBo().setWellFormed(CheckLevel.FAILURE);
722 }
723 if (proposition.getFormalProofList() != null) {
724 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
725 final FormalProof proof = proposition.getFormalProofList().get(i);
726 if (proof != null) {
727 final FormalProofLineList list = proof.getFormalProofLineList();
728 setLocationWithinModule(context + ".getFormalProofList().get("
729 + i + ").getFormalProofLineList()");
730 checkFormalProof(list);
731 }
732 }
733 }
734 setLocationWithinModule(context);
735
736 if (!getNodeBo().isNotWellFormed()) {
737 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
738 }
739 setBlocked(true);
740 }
741
742
743
744
745
746
747 private void checkFormalProof(final FormalProofLineList list) {
748 final String context = getCurrentContext().getLocationWithinModule();
749 if (list != null) {
750 for (int i = 0; i < list.size(); i++) {
751 final FormalProofLine line = list.get(i);
752 setLocationWithinModule(context + ".get(" + i + ")");
753 checkProofLine(line);
754 }
755 }
756 }
757
758
759
760
761
762
763 private void checkProofLine(final FormalProofLine line) {
764 if (line instanceof ConditionalProof) {
765 checkProofLine((ConditionalProof) line);
766 return;
767 }
768 final String context = getCurrentContext().getLocationWithinModule();
769 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
770 if (line != null) {
771 final Formula formula = line.getFormula();
772 if (formula != null) {
773 setLocationWithinModule(context + ".getFormula().getElement()");
774 elist = checkerFactory.createFormulaChecker().checkFormula(
775 formula.getElement(), getCurrentContext(), existence);
776 for (int k = 0; k < elist.size(); k++) {
777 addError(elist.get(k));
778 }
779 }
780 final Reason reason = line.getReason();
781 if (reason != null) {
782 if (reason instanceof SubstFree) {
783 final SubstFree subst = (SubstFree) reason;
784 if (subst.getSubstFree().getSubstituteTerm() != null) {
785 setLocationWithinModule(context
786 + ".getReason().getSubstFree().getSubstituteTerm()");
787 elist = checkerFactory.createFormulaChecker().checkTerm(
788 subst.getSubstFree().getSubstituteTerm(),
789 getCurrentContext(), existence);
790 }
791 } else if (reason instanceof SubstPred) {
792 final SubstPred subst = (SubstPred) reason;
793 if (subst.getSubstPred().getSubstituteFormula() != null) {
794 setLocationWithinModule(context
795 + ".getReason().getSubstPred().getSubstituteFormula()");
796 elist = checkerFactory.createFormulaChecker().checkFormula(
797 subst.getSubstPred().getSubstituteFormula(),
798 getCurrentContext(), existence);
799 }
800 } else if (reason instanceof SubstFunc) {
801 final SubstFunc subst = (SubstFunc) reason;
802 if (subst.getSubstFunc().getSubstituteTerm() != null) {
803 setLocationWithinModule(context
804 + ".getReason().getSubstFunc().getSubstituteTerm()");
805 elist = checkerFactory.createFormulaChecker().checkTerm(
806 subst.getSubstFunc().getSubstituteTerm(),
807 getCurrentContext(), existence);
808 }
809 }
810 for (int k = 0; k < elist.size(); k++) {
811 addError(elist.get(k));
812 }
813 }
814 }
815 }
816
817
818
819
820
821
822 private void checkProofLine(final ConditionalProof line) {
823 final String context = getCurrentContext().getLocationWithinModule();
824 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
825 if (line != null) {
826 {
827 final Formula formula = line.getFormula();
828 if (formula != null && formula.getElement() != null) {
829 setLocationWithinModule(context + ".getFormula().getElement()");
830 elist = checkerFactory.createFormulaChecker().checkFormula(
831 formula.getElement(), getCurrentContext(), existence);
832 for (int k = 0; k < elist.size(); k++) {
833 addError(elist.get(k));
834 }
835 }
836 }
837 if (line.getHypothesis() != null) {
838 final Formula formula = line.getHypothesis().getFormula();;
839 if (formula != null && formula.getElement() != null) {
840 setLocationWithinModule(context
841 + ".getHypothesis().getFormula().getElement()");
842 elist = checkerFactory.createFormulaChecker().checkFormula(
843 formula.getElement(), getCurrentContext(), existence);
844 for (int k = 0; k < elist.size(); k++) {
845 addError(elist.get(k));
846 }
847 }
848 }
849 if (line.getFormalProofLineList() != null) {
850 setLocationWithinModule(context + ".getFormalProofLineList()");
851 checkFormalProof(line.getFormalProofLineList());
852 }
853 if (line.getConclusion() != null) {
854 final Formula formula = line.getConclusion().getFormula();;
855 if (formula != null && formula.getElement() != null) {
856 setLocationWithinModule(context
857 + ".getConclusion().getFormula().getElement()");
858 elist = checkerFactory.createFormulaChecker().checkFormula(
859 formula.getElement(), getCurrentContext(), existence);
860 for (int k = 0; k < elist.size(); k++) {
861 addError(elist.get(k));
862 }
863 }
864 }
865 }
866 }
867
868 public void visitLeave(final Proposition definition) {
869 setBlocked(false);
870 }
871
872 public void visitEnter(final Rule rule) throws ModuleDataException {
873 final String context = getCurrentContext().getLocationWithinModule();
874
875 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
876 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
877 if (rule.getName() != null && rule.getName().length() > 0 && rule.getVersion() != null
878 && rule.getVersion().length() > 0) {
879 try {
880 setLocationWithinModule(context + ".getVersion()");
881 new Version(rule.getVersion());
882 } catch (RuntimeException e) {
883 addError(new IllegalModuleDataException(
884 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
885 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
886 getCurrentContext()));
887 }
888 if (existence.ruleExists(ruleKey)) {
889 addError(new IllegalModuleDataException(
890 LogicErrors.RULE_ALREADY_DEFINED_CODE,
891 LogicErrors.RULE_ALREADY_DEFINED_TEXT
892 + ruleKey + " " + existence.getQedeq(ruleKey).getUrl(),
893 getCurrentContext()));
894 } else {
895 if (CLASS_DEFINITION_VIA_FORMULA_RULE.equals(ruleKey)) {
896
897
898 existence.setClassOperatorModule(getKernelQedeqBo(),
899 getCurrentContext());
900 }
901 existence.add(ruleKey, rule);
902 }
903 if (rule.getChangedRuleList() != null) {
904 final ChangedRuleList list = rule.getChangedRuleList();
905 for (int i = 0; i < list.size(); i++) {
906 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ")");
907 final ChangedRule r = list.get(i);
908 if (r == null || r.getName() == null || r.getName().length() <= 0
909 || r.getVersion() == null || r.getVersion().length() <= 0) {
910 addError(new IllegalModuleDataException(
911 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
912 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
913 + (r == null ? "null" : r.getName() + " [" + r.getVersion() + "]"),
914 getCurrentContext()));
915 continue;
916 }
917 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
918 final String ruleName = r.getName();
919 final String ruleVersion = r.getVersion();
920 try {
921 new Version(ruleVersion);
922 } catch (RuntimeException e) {
923 addError(new IllegalModuleDataException(
924 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
925 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
926 getCurrentContext()));
927 }
928 RuleKey key1 = getLocalRuleKey(ruleName);
929 if (key1 == null) {
930 key1 = existence.getParentRuleKey(ruleName);
931 }
932 if (key1 == null) {
933 addError(new IllegalModuleDataException(
934 LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_CODE,
935 LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_TEXT
936 + ruleName, getCurrentContext()));
937 } else {
938 final RuleKey key2 = new RuleKey(ruleName, ruleVersion);
939 if (existence.ruleExists(key2)) {
940 addError(new IllegalModuleDataException(
941 LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_CODE,
942 LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_TEXT
943 + ruleName, getCurrentContext(), getKernelQedeqBo().getLabels()
944 .getRuleContext(key2)));
945 } else {
946 try {
947 if (!Version.less(key1.getVersion(), key2.getVersion())) {
948 addError(new IllegalModuleDataException(
949 LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_CODE,
950 LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_TEXT
951 + key1 + " " + key2, getCurrentContext(), getKernelQedeqBo().getLabels()
952 .getRuleContext(key2)));
953 }
954 } catch (RuntimeException e) {
955 addError(new IllegalModuleDataException(
956 LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_CODE,
957 LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_TEXT
958 + key1 + " " + key2, getCurrentContext(), getKernelQedeqBo().getLabels()
959 .getRuleContext(key2)));
960 }
961 }
962 existence.add(key2, rule);
963 }
964 }
965 }
966 } else {
967 addError(new IllegalModuleDataException(
968 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
969 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
970 + ruleKey, getCurrentContext()));
971 }
972
973 if (!getNodeBo().isNotWellFormed()) {
974 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
975 }
976 setBlocked(true);
977 }
978
979 public void visitLeave(final Rule rule) {
980 setBlocked(false);
981 }
982
983 protected void addError(final ModuleDataException me) {
984 if (getNodeBo() != null) {
985 getNodeBo().setWellFormed(CheckLevel.FAILURE);
986 }
987 super.addError(me);
988 }
989
990 protected void addError(final SourceFileException me) {
991 if (getNodeBo() != null) {
992 getNodeBo().setWellFormed(CheckLevel.FAILURE);
993 }
994 super.addError(me);
995 }
996
997 }