001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, 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
019 import org.qedeq.base.io.Parameters;
020 import org.qedeq.base.io.Version;
021 import org.qedeq.base.trace.Trace;
022 import org.qedeq.base.utility.StringUtility;
023 import org.qedeq.kernel.bo.common.PluginExecutor;
024 import org.qedeq.kernel.bo.log.QedeqLog;
025 import org.qedeq.kernel.bo.logic.ProofCheckerFactoryImpl;
026 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
027 import org.qedeq.kernel.bo.logic.common.FunctionKey;
028 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
029 import org.qedeq.kernel.bo.logic.common.PredicateKey;
030 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
031 import org.qedeq.kernel.bo.logic.proof.checker.ProofCheckException;
032 import org.qedeq.kernel.bo.logic.proof.common.ProofCheckerFactory;
033 import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
034 import org.qedeq.kernel.bo.module.ControlVisitor;
035 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
036 import org.qedeq.kernel.bo.module.KernelQedeqBo;
037 import org.qedeq.kernel.bo.module.Reference;
038 import org.qedeq.kernel.se.base.list.Element;
039 import org.qedeq.kernel.se.base.list.ElementList;
040 import org.qedeq.kernel.se.base.module.Axiom;
041 import org.qedeq.kernel.se.base.module.ChangedRule;
042 import org.qedeq.kernel.se.base.module.ChangedRuleList;
043 import org.qedeq.kernel.se.base.module.FormalProof;
044 import org.qedeq.kernel.se.base.module.FormalProofLineList;
045 import org.qedeq.kernel.se.base.module.FunctionDefinition;
046 import org.qedeq.kernel.se.base.module.Header;
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.Rule;
052 import org.qedeq.kernel.se.common.CheckLevel;
053 import org.qedeq.kernel.se.common.ModuleContext;
054 import org.qedeq.kernel.se.common.ModuleDataException;
055 import org.qedeq.kernel.se.common.Plugin;
056 import org.qedeq.kernel.se.common.RuleKey;
057 import org.qedeq.kernel.se.common.SourceFileException;
058 import org.qedeq.kernel.se.common.SourceFileExceptionList;
059 import org.qedeq.kernel.se.dto.list.DefaultAtom;
060 import org.qedeq.kernel.se.dto.list.DefaultElementList;
061
062
063 /**
064 * Checks if all propositions have a correct formal proof.
065 *
066 * @author Michael Meyling
067 */
068 public final class FormalProofCheckerExecutor extends ControlVisitor implements PluginExecutor,
069 ReferenceResolver, RuleChecker {
070
071 /** This class. */
072 private static final Class CLASS = FormalProofCheckerExecutor.class;
073
074 /** Factory for generating new checkers. */
075 private ProofCheckerFactory checkerFactory = null;
076
077 /** Parameters for checker. */
078 private Parameters parameters;
079
080 /** Rule version the module claims to use at maximum. */
081 private Version ruleVersion;
082
083 /**
084 * Constructor.
085 *
086 * @param plugin This plugin we work for.
087 * @param qedeq QEDEQ BO object.
088 * @param parameters Parameters.
089 */
090 FormalProofCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
091 final Parameters parameters) {
092 super(plugin, qedeq);
093 final String method = "FormalProofCheckerExecutor(Plugin, KernelQedeqBo, Map)";
094 this.parameters = parameters;
095 final String checkerFactoryClass = parameters.getString("checkerFactory");
096 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
097 try {
098 Class cl = Class.forName(checkerFactoryClass);
099 checkerFactory = (ProofCheckerFactory) cl.newInstance();
100 } catch (ClassNotFoundException e) {
101 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class not in class path: "
102 + checkerFactoryClass, e);
103 } catch (InstantiationException e) {
104 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class could not be instanciated: "
105 + checkerFactoryClass, e);
106 } catch (IllegalAccessException e) {
107 Trace.fatal(CLASS, this, method,
108 "Programming error, access for instantiation failed for model: "
109 + checkerFactoryClass, e);
110 } catch (RuntimeException e) {
111 Trace.fatal(CLASS, this, method,
112 "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
113 }
114 }
115 // fallback is the default checker factory
116 if (checkerFactory == null) {
117 checkerFactory = new ProofCheckerFactoryImpl();
118 }
119 }
120
121 private Parameters getParameters() {
122 return parameters;
123 }
124
125 public Object executePlugin() {
126 ruleVersion = new Version("0.00.00"); // we set this as module rule version, and hope it will be changed
127 QedeqLog.getInstance().logRequest(
128 "Check logical correctness", getQedeqBo().getUrl());
129 getServices().checkModule(getQedeqBo().getModuleAddress());
130 if (!getQedeqBo().isChecked()) {
131 final String msg = "Check of logical correctness failed";
132 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
133 "Module is not even well formed.");
134 return Boolean.FALSE;
135 }
136 // getQedeqBo().setLogicalProgressState(LogicalModuleState.STATE_EXTERNAL_CHECKING);
137 KernelModuleReferenceList list = (KernelModuleReferenceList) getQedeqBo().getRequiredModules();
138 for (int i = 0; i < list.size(); i++) {
139 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
140 final FormalProofCheckerExecutor checker = new FormalProofCheckerExecutor(getPlugin(),
141 list.getKernelQedeqBo(i), getParameters());
142 checker.executePlugin();
143 if (list.getKernelQedeqBo(i).hasErrors()) {
144 addError(new CheckRequiredModuleException(
145 LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
146 LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
147 + list.getQedeqBo(i).getModuleAddress(),
148 list.getModuleContext(i)));
149 }
150 }
151 // has at least one import errors?
152 if (getQedeqBo().hasErrors()) {
153 final String msg = "Check of logical correctness failed";
154 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
155 StringUtility.replace(getQedeqBo().getErrors().getMessage(), "\n", "\n\t"));
156 return Boolean.FALSE;
157 }
158 try {
159 traverse();
160 } catch (SourceFileExceptionList e) {
161 final String msg = "Check of logical correctness failed";
162 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
163 StringUtility.replace(e.getMessage(), "\n", "\n\t"));
164 return Boolean.FALSE;
165 } finally {
166 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
167 }
168 QedeqLog.getInstance().logSuccessfulReply(
169 "Check of logical correctness successful", getQedeqBo().getUrl());
170 return Boolean.TRUE;
171 }
172
173 public void visitEnter(final Header header) throws ModuleDataException {
174 if (header.getSpecification() == null
175 || header.getSpecification().getRuleVersion() == null) {
176 return;
177 }
178 final String context = getCurrentContext().getLocationWithinModule();
179 setLocationWithinModule(context + ".getSpecification().getRuleVersion()");
180 final String version = header.getSpecification().getRuleVersion().trim();
181 if (!checkerFactory.isRuleVersionSupported(version)) {
182 addError(new ProofCheckException(
183 LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_CODE,
184 LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_TEXT + version,
185 getCurrentContext()));
186 } else {
187 try {
188 ruleVersion = new Version(version);
189 } catch (RuntimeException e) {
190 addError(new ProofCheckException(
191 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
192 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + version,
193 getCurrentContext()));
194 }
195 }
196 setLocationWithinModule(context);
197 }
198
199 public void visitEnter(final Axiom axiom) throws ModuleDataException {
200 if (getNodeBo().isWellFormed()) {
201 getNodeBo().setProved(CheckLevel.SUCCESS);
202 } else {
203 getNodeBo().setProved(CheckLevel.FAILURE);
204 addError(new ProofCheckException(
205 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
206 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
207 getCurrentContext()));
208 return;
209 }
210 setBlocked(true);
211 }
212
213 public void visitLeave(final Axiom axiom) {
214 setBlocked(false);
215 }
216
217 public void visitEnter(final PredicateDefinition definition)
218 throws ModuleDataException {
219 if (getNodeBo().isWellFormed()) {
220 getNodeBo().setProved(CheckLevel.SUCCESS);
221 } else {
222 getNodeBo().setProved(CheckLevel.FAILURE);
223 addError(new ProofCheckException(
224 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
225 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
226 getCurrentContext()));
227 return;
228 }
229 setBlocked(true);
230 }
231
232 public void visitLeave(final PredicateDefinition definition) {
233 setBlocked(false);
234 }
235
236 public void visitEnter(final InitialPredicateDefinition definition)
237 throws ModuleDataException {
238 if (getNodeBo().isWellFormed()) {
239 getNodeBo().setProved(CheckLevel.SUCCESS);
240 } else {
241 getNodeBo().setProved(CheckLevel.FAILURE);
242 addError(new ProofCheckException(
243 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
244 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
245 getCurrentContext()));
246 return;
247 }
248 setBlocked(true);
249 }
250
251 public void visitLeave(final InitialPredicateDefinition definition) {
252 setBlocked(false);
253 }
254
255 public void visitEnter(final InitialFunctionDefinition definition)
256 throws ModuleDataException {
257 if (getNodeBo().isWellFormed()) {
258 getNodeBo().setProved(CheckLevel.SUCCESS);
259 } else {
260 getNodeBo().setProved(CheckLevel.FAILURE);
261 addError(new ProofCheckException(
262 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
263 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
264 getCurrentContext()));
265 return;
266 }
267 setBlocked(true);
268 }
269
270 public void visitLeave(final InitialFunctionDefinition definition) {
271 setBlocked(false);
272 }
273
274 public void visitEnter(final FunctionDefinition definition)
275 throws ModuleDataException {
276 if (getNodeBo().isWellFormed()) {
277 getNodeBo().setProved(CheckLevel.SUCCESS);
278 } else {
279 getNodeBo().setProved(CheckLevel.FAILURE);
280 addError(new ProofCheckException(
281 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
282 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
283 getCurrentContext()));
284 return;
285 }
286 setBlocked(true);
287 }
288
289 public void visitLeave(final FunctionDefinition definition) {
290 setBlocked(false);
291 }
292
293 public void visitEnter(final Proposition proposition)
294 throws ModuleDataException {
295 // we only check this node, if the well formed check was successful
296 if (!getNodeBo().isWellFormed()) {
297 getNodeBo().setProved(CheckLevel.FAILURE);
298 addError(new ProofCheckException(
299 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
300 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
301 getCurrentContext()));
302 return;
303 }
304 getNodeBo().setProved(CheckLevel.UNCHECKED);
305 if (proposition.getFormula() == null) {
306 getNodeBo().setProved(CheckLevel.FAILURE);
307 addError(new ProofCheckException(
308 LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_CODE,
309 LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_TEXT,
310 getCurrentContext()));
311 return;
312 }
313 final String context = getCurrentContext().getLocationWithinModule();
314 boolean correctProofFound = false;
315 // we start checking
316 if (proposition.getFormalProofList() != null) {
317 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
318 final FormalProof proof = proposition.getFormalProofList().get(i);
319 if (proof != null) {
320 final FormalProofLineList list = proof.getFormalProofLineList();
321 if (list != null) {
322 setLocationWithinModule(context + ".getFormalProofList().get("
323 + i + ").getFormalProofLineList()");
324 LogicalCheckExceptionList eList
325 = checkerFactory.createProofChecker(ruleVersion).checkProof(
326 proposition.getFormula().getElement(), list, this,
327 getCurrentContext(),
328 this);
329 if (!correctProofFound && eList.size() == 0) {
330 correctProofFound = true;
331 }
332 for (int j = 0; j < eList.size(); j++) {
333 addError(eList.get(j));
334 }
335 }
336 }
337 }
338 }
339 setLocationWithinModule(context + ".getFormula()");
340 // only if we found at least one error free formal proof
341 if (correctProofFound) {
342 getNodeBo().setProved(CheckLevel.SUCCESS);
343 } else {
344 getNodeBo().setProved(CheckLevel.FAILURE);
345 addError(new ProofCheckException(
346 LogicErrors.NO_FORMAL_PROOF_FOUND_CODE,
347 LogicErrors.NO_FORMAL_PROOF_FOUND_TEXT,
348 getCurrentContext()));
349 }
350 setBlocked(true);
351 }
352
353 public void visitLeave(final Proposition definition) {
354 setBlocked(false);
355 }
356
357 public void visitEnter(final Rule rule) throws ModuleDataException {
358 final String context = getCurrentContext().getLocationWithinModule();
359 // FIXME 20110618 m31: check if this is really a higher version than before?
360 getNodeBo().setProved(CheckLevel.UNCHECKED);
361 final ChangedRuleList list = rule.getChangedRuleList();
362 for (int i = 0; list != null && i < list.size(); i++) {
363 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
364 final ChangedRule r = list.get(i);
365 if (!Version.equals(rule.getVersion(), r.getVersion())) {
366 addError(new ProofCheckException(
367 LogicErrors.OTHER_RULE_VERSION_EXPECTED_CODE,
368 LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT1 + rule.getVersion()
369 + LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT2 + r.getVersion(),
370 getCurrentContext()));
371 }
372 }
373
374 if (getNodeBo().isNotProved()) {
375 getNodeBo().setProved(CheckLevel.SUCCESS);
376 } else {
377 getNodeBo().setProved(CheckLevel.FAILURE);
378 }
379 }
380
381 protected void addError(final ModuleDataException me) {
382 if (getNodeBo() != null) {
383 getNodeBo().setProved(CheckLevel.FAILURE);
384 }
385 super.addError(me);
386 }
387
388 protected void addError(final SourceFileException me) {
389 if (getNodeBo() != null) {
390 getNodeBo().setProved(CheckLevel.FAILURE);
391 }
392 super.addError(me);
393 }
394
395 public boolean isProvedFormula(final String reference) {
396 final String method = "hasProvedFormula";
397 final Reference ref = getReference(reference, getCurrentContext(), false, false);
398 if (ref == null) {
399 Trace.info(CLASS, method, "ref == null");
400 return false;
401 }
402 if (ref.isExternalModuleReference()) {
403 Trace.info(CLASS, method, "ref is external module");
404 return false;
405 }
406 if (!ref.isNodeReference()) {
407 Trace.info(CLASS, method, "ref is no node reference");
408 return false;
409 }
410 if (null == ref.getNode()) {
411 Trace.info(CLASS, method, "ref node == null");
412 return false;
413 }
414 if (ref.isSubReference()) {
415 return false;
416 }
417 if (!ref.isProofLineReference()) {
418 if (!ref.getNode().isProved()) {
419 Trace.info(CLASS, method, "ref node is not marked as proved: " + reference);
420 }
421 if (!ref.getNode().isProved()) {
422 return false;
423 }
424 if (!ref.getNode().hasFormula()) {
425 Trace.info(CLASS, method, "node has no formula: " + reference);
426 return false;
427 }
428 return ref.getNode().isProved();
429 } else {
430 Trace.info(CLASS, method, "proof line references are not ok!");
431 return false;
432 }
433 }
434
435 public Element getNormalizedReferenceFormula(final String reference) {
436 if (!isProvedFormula(reference)) {
437 return null;
438 }
439 final Reference ref = getReference(reference, getCurrentContext(), false, false);
440 final Element formula = ref.getNode().getFormula();
441 return getNormalizedFormula(ref.getNode().getQedeqBo(), formula);
442 }
443
444 public Element getNormalizedFormula(final Element formula) {
445 return getNormalizedFormula(getQedeqBo(), formula);
446 }
447
448 private Element getNormalizedFormula(final KernelQedeqBo qedeq, final Element formula) {
449 if (formula == null) {
450 return null;
451 }
452 if (formula.isAtom()) {
453 return new DefaultAtom(formula.getAtom().getString());
454 }
455 return getNormalizedFormula(qedeq, formula.getList());
456 }
457
458 private ElementList getNormalizedFormula(final KernelQedeqBo qedeq, final ElementList formula) {
459 final ElementList result = new DefaultElementList(formula.getOperator());
460 if (FormulaUtility.isPredicateConstant(formula)) {
461 final PredicateKey key = new PredicateKey(formula.getElement(0).getAtom().getString(),
462 "" + (formula.getList().size() - 1));
463 final DefaultAtom atom = new DefaultAtom(
464 qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
465 + "$" + key.getName());
466 result.add(atom);
467 for (int i = 1; i < formula.size(); i++) {
468 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
469 }
470 } else if (FormulaUtility.isFunctionConstant(formula)) {
471 final FunctionKey key = new FunctionKey(formula.getElement(0).getAtom().getString(),
472 "" + (formula.getList().size() - 1));
473 final DefaultAtom atom = new DefaultAtom(
474 qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
475 + "$" + key.getName());
476 result.add(atom);
477 for (int i = 1; i < formula.size(); i++) {
478 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
479 }
480 } else {
481 for (int i = 0; i < formula.size(); i++) {
482 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
483 }
484 }
485 return result;
486 }
487
488 public boolean isLocalProofLineReference(final String reference) {
489 // here we have no proof lines
490 return false;
491 }
492
493 public ModuleContext getReferenceContext(final String reference) {
494 // here we have no proof lines
495 return null;
496 }
497
498 public Element getNormalizedLocalProofLineReference(final String reference) {
499 // here we have no proof lines
500 return null;
501 }
502
503 public RuleKey getRule(final String ruleName) {
504 final RuleKey local = getLocalRuleKey(ruleName);
505 if (local == null) {
506 return getQedeqBo().getExistenceChecker().getParentRuleKey(
507 ruleName);
508 }
509 return local;
510 }
511
512
513 }
|