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