001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.logic;
017
018 import java.util.Map;
019
020 import org.qedeq.base.io.IoUtility;
021 import org.qedeq.base.trace.Trace;
022 import org.qedeq.kernel.bo.common.PluginExecutor;
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.ProofCheckerFactory;
030 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
031 import org.qedeq.kernel.bo.logic.proof.basic.ProofCheckException;
032 import org.qedeq.kernel.bo.module.ControlVisitor;
033 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
034 import org.qedeq.kernel.bo.module.KernelQedeqBo;
035 import org.qedeq.kernel.bo.module.Reference;
036 import org.qedeq.kernel.se.base.list.Element;
037 import org.qedeq.kernel.se.base.list.ElementList;
038 import org.qedeq.kernel.se.base.module.Axiom;
039 import org.qedeq.kernel.se.base.module.FormalProof;
040 import org.qedeq.kernel.se.base.module.FormalProofLineList;
041 import org.qedeq.kernel.se.base.module.FunctionDefinition;
042 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
043 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
044 import org.qedeq.kernel.se.base.module.PredicateDefinition;
045 import org.qedeq.kernel.se.base.module.Proposition;
046 import org.qedeq.kernel.se.base.module.Rule;
047 import org.qedeq.kernel.se.common.CheckLevel;
048 import org.qedeq.kernel.se.common.DefaultSourceFileExceptionList;
049 import org.qedeq.kernel.se.common.ModuleDataException;
050 import org.qedeq.kernel.se.common.Plugin;
051 import org.qedeq.kernel.se.common.SourceFileException;
052 import org.qedeq.kernel.se.common.SourceFileExceptionList;
053 import org.qedeq.kernel.se.dto.list.DefaultAtom;
054 import org.qedeq.kernel.se.dto.list.DefaultElementList;
055
056
057 /**
058 * Checks if all propositions have a correct formal proof.
059 *
060 * @author Michael Meyling
061 */
062 public final class FormalProofCheckerExecutor extends ControlVisitor implements PluginExecutor,
063 ReferenceResolver {
064
065 /** This class. */
066 private static final Class CLASS = FormalProofCheckerExecutor.class;
067
068 /** Factory for generating new checkers. */
069 private ProofCheckerFactory checkerFactory = null;
070
071 /** Parameters for checker. */
072 private Map parameters;
073
074 /**
075 * Constructor.
076 *
077 * @param plugin This plugin we work for.
078 * @param qedeq QEDEQ BO object.
079 * @param parameters Parameters.
080 */
081 FormalProofCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
082 final Map parameters) {
083 super(plugin, qedeq);
084 final String method = "FormalProofCheckerExecutor(Plugin, KernelQedeqBo, Map)";
085 this.parameters = parameters;
086 final String checkerFactoryClass
087 = (parameters != null ? (String) parameters.get("checkerFactory") : null);
088 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
089 try {
090 Class cl = Class.forName(checkerFactoryClass);
091 checkerFactory = (ProofCheckerFactory) cl.newInstance();
092 } catch (ClassNotFoundException e) {
093 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class not in class path: "
094 + checkerFactoryClass, e);
095 } catch (InstantiationException e) {
096 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class could not be instanciated: "
097 + checkerFactoryClass, e);
098 } catch (IllegalAccessException e) {
099 Trace.fatal(CLASS, this, method,
100 "Programming error, access for instantiation failed for model: "
101 + checkerFactoryClass, e);
102 } catch (RuntimeException e) {
103 Trace.fatal(CLASS, this, method,
104 "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
105 }
106 }
107 // fallback is the default checker factory
108 if (checkerFactory == null) {
109 checkerFactory = new ProofCheckerFactoryImpl();
110 }
111 }
112
113 private Map getParameters() {
114 return parameters;
115 }
116
117 public Object executePlugin() {
118 QedeqLog.getInstance().logRequest(
119 "Check logical correctness for \"" + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"");
120 getServices().checkModule(getQedeqBo().getModuleAddress());
121 if (!getQedeqBo().isChecked()) {
122 final String msg = "Check of logical correctness failed for \"" + getQedeqBo().getUrl()
123 + "\"";
124 QedeqLog.getInstance().logFailureReply(msg, "Module is not even well formed.");
125 return Boolean.FALSE;
126 }
127 // getQedeqBo().setLogicalProgressState(LogicalModuleState.STATE_EXTERNAL_CHECKING);
128 final SourceFileExceptionList sfl = new DefaultSourceFileExceptionList();
129 KernelModuleReferenceList list = (KernelModuleReferenceList) getQedeqBo().getRequiredModules();
130 for (int i = 0; i < list.size(); i++) {
131 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
132 final FormalProofCheckerExecutor checker = new FormalProofCheckerExecutor(getPlugin(),
133 list.getKernelQedeqBo(i), getParameters());
134 checker.executePlugin();
135 if (list.getKernelQedeqBo(i).hasErrors()) {
136 addError(new CheckRequiredModuleException(
137 LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
138 LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
139 + list.getQedeqBo(i).getModuleAddress(),
140 list.getModuleContext(i)));
141 }
142 }
143 // has at least one import errors?
144 if (getQedeqBo().hasErrors()) {
145 // getQedeqBo().setLogicalFailureState(LogicalModuleState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
146 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), sfl, null);
147 final String msg = "Check of logical correctness failed for \"" + IoUtility.easyUrl(getQedeqBo().getUrl())
148 + "\"";
149 QedeqLog.getInstance().logFailureReply(msg, sfl.getMessage());
150 return Boolean.FALSE;
151 }
152 // getQedeqBo().setLogicalProgressState(LogicalModuleState.STATE_INTERNAL_CHECKING);
153 // getQedeqBo().setExistenceChecker(existence);
154 try {
155 traverse();
156 } catch (SourceFileExceptionList e) {
157 // getQedeqBo().setLogicalFailureState(LogicalModuleState.STATE_INTERNAL_CHECKING_FAILED, e);
158 final String msg = "Check of logical correctness failed for \"" + IoUtility.easyUrl(getQedeqBo().getUrl())
159 + "\"";
160 QedeqLog.getInstance().logFailureReply(msg, sfl.getMessage());
161 return Boolean.FALSE;
162 } finally {
163 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
164 }
165 // getQedeqBo().setChecked(existence);
166 QedeqLog.getInstance().logSuccessfulReply(
167 "Check of logical correctness successful for \"" + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"");
168 return Boolean.TRUE;
169 }
170
171 public void visitEnter(final Axiom axiom) throws ModuleDataException {
172 if (axiom == null) {
173 return;
174 }
175 if (getNodeBo().isWellFormed()) {
176 getNodeBo().setProved(CheckLevel.SUCCESS);
177 } else {
178 getNodeBo().setProved(CheckLevel.FAILURE);
179 addError(new ProofCheckException(
180 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
181 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
182 getCurrentContext()));
183 return;
184 }
185 setBlocked(true);
186 }
187
188 public void visitLeave(final Axiom axiom) {
189 setBlocked(false);
190 }
191
192 public void visitEnter(final PredicateDefinition definition)
193 throws ModuleDataException {
194 if (definition == null) {
195 return;
196 }
197 if (getNodeBo().isWellFormed()) {
198 getNodeBo().setProved(CheckLevel.SUCCESS);
199 } else {
200 getNodeBo().setProved(CheckLevel.FAILURE);
201 addError(new ProofCheckException(
202 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
203 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
204 getCurrentContext()));
205 return;
206 }
207 setBlocked(true);
208 }
209
210 public void visitLeave(final PredicateDefinition definition) {
211 setBlocked(false);
212 }
213
214 public void visitEnter(final InitialPredicateDefinition definition)
215 throws ModuleDataException {
216 if (definition == null) {
217 return;
218 }
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 InitialPredicateDefinition definition) {
233 setBlocked(false);
234 }
235
236 public void visitEnter(final InitialFunctionDefinition definition)
237 throws ModuleDataException {
238 if (definition == null) {
239 return;
240 }
241 if (getNodeBo().isWellFormed()) {
242 getNodeBo().setProved(CheckLevel.SUCCESS);
243 } else {
244 getNodeBo().setProved(CheckLevel.FAILURE);
245 addError(new ProofCheckException(
246 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
247 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
248 getCurrentContext()));
249 return;
250 }
251 setBlocked(true);
252 }
253
254 public void visitLeave(final InitialFunctionDefinition definition) {
255 setBlocked(false);
256 }
257
258 public void visitEnter(final FunctionDefinition definition)
259 throws ModuleDataException {
260 if (definition == null) {
261 return;
262 }
263 if (getNodeBo().isWellFormed()) {
264 getNodeBo().setProved(CheckLevel.SUCCESS);
265 } else {
266 getNodeBo().setProved(CheckLevel.FAILURE);
267 addError(new ProofCheckException(
268 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
269 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
270 getCurrentContext()));
271 return;
272 }
273 setBlocked(true);
274 }
275
276 public void visitLeave(final FunctionDefinition definition) {
277 setBlocked(false);
278 }
279
280 public void visitEnter(final Proposition proposition)
281 throws ModuleDataException {
282 if (proposition == null) {
283 return;
284 }
285 // we only check this node, if the well formed check was successful
286 if (!getNodeBo().isWellFormed()) {
287 getNodeBo().setProved(CheckLevel.FAILURE);
288 addError(new ProofCheckException(
289 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
290 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
291 getCurrentContext()));
292 return;
293 }
294 getNodeBo().setProved(CheckLevel.UNCHECKED);
295 if (proposition.getFormula() == null) {
296 getNodeBo().setProved(CheckLevel.FAILURE);
297 addError(new ProofCheckException(
298 LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_CODE,
299 LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_TEXT,
300 getCurrentContext()));
301 return;
302 }
303 final String context = getCurrentContext().getLocationWithinModule();
304 boolean correctProofFound = false;
305 // we start checking
306 if (proposition.getFormalProofList() != null) {
307 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
308 final FormalProof proof = proposition.getFormalProofList().get(i);
309 if (proof != null) {
310 final FormalProofLineList list = proof.getFormalProofLineList();
311 if (list != null) {
312 setLocationWithinModule(context + ".getFormalProofList().get("
313 + i + ").getFormalProofLineList()");
314 LogicalCheckExceptionList eList
315 = checkerFactory.createProofChecker().checkProof(
316 proposition.getFormula().getElement(), list, getCurrentContext(),
317 this);
318 if (!correctProofFound && eList.size() == 0) {
319 correctProofFound = true;
320 }
321 for (int j = 0; j < eList.size(); j++) {
322 addError(eList.get(j));
323 }
324 }
325 }
326 }
327 }
328 setLocationWithinModule(context + ".getFormula()");
329 // only if we found at least one error free formal proof
330 if (correctProofFound) {
331 getNodeBo().setProved(CheckLevel.SUCCESS);
332 } else {
333 getNodeBo().setProved(CheckLevel.FAILURE);
334 addError(new ProofCheckException(
335 LogicErrors.NO_FORMAL_PROOF_FOUND_CODE,
336 LogicErrors.NO_FORMAL_PROOF_FOUND_TEXT,
337 getCurrentContext()));
338 }
339 setBlocked(true);
340 }
341
342 public void visitLeave(final Proposition definition) {
343 setBlocked(false);
344 }
345
346 public void visitEnter(final Rule rule) throws ModuleDataException {
347 if (rule == null) {
348 return;
349 }
350 if (getNodeBo().isWellFormed()) {
351 getNodeBo().setProved(CheckLevel.SUCCESS);
352 } else {
353 getNodeBo().setProved(CheckLevel.FAILURE);
354 }
355 setBlocked(true);
356 }
357
358 public void visitLeave(final Rule rule) {
359 setBlocked(false);
360 }
361
362 protected void addError(final ModuleDataException me) {
363 if (getNodeBo() != null) {
364 getNodeBo().setWellFormed(CheckLevel.FAILURE);
365 }
366 super.addError(me);
367 }
368
369 protected void addError(final SourceFileException me) {
370 if (getNodeBo() != null) {
371 getNodeBo().setWellFormed(CheckLevel.FAILURE);
372 }
373 super.addError(me);
374 }
375
376 /**
377 * Set location information where are we within the original module.
378 *
379 * @param locationWithinModule Location within module.
380 */
381 public void setLocationWithinModule(final String locationWithinModule) {
382 getCurrentContext().setLocationWithinModule(locationWithinModule);
383 }
384
385 public boolean hasProvedFormula(final String reference) {
386 final String method = "hasProvedFormula";
387 final Reference ref = getReference(reference, getCurrentContext(), false, false);
388 if (ref == null) {
389 Trace.info(CLASS, method, "ref == null");
390 return false;
391 }
392 if (ref.isExternalModuleReference()) {
393 Trace.info(CLASS, method, "ref is external module");
394 return false;
395 }
396 if (!ref.isNodeReference()) {
397 Trace.info(CLASS, method, "ref is no node reference");
398 return false;
399 }
400 if (null == ref.getNode()) {
401 Trace.info(CLASS, method, "ref node == null");
402 return false;
403 }
404 if (ref.isSubReference()) {
405 return false;
406 }
407 if (!ref.isProofLineReference()) {
408 if (!ref.getNode().isProved()) {
409 Trace.info(CLASS, method, "ref node is not marked as proved: " + reference);
410 }
411 if (!ref.getNode().isProved()) {
412 return false;
413 }
414 if (!ref.getNode().hasFormula()) {
415 Trace.info(CLASS, method, "node has no formula: " + reference);
416 return false;
417 }
418 return ref.getNode().isProved();
419 } else {
420 Trace.info(CLASS, method, "proof line references are not ok!");
421 return false;
422 }
423 }
424
425 public Element getNormalizedReferenceFormula(final String reference) {
426 if (!hasProvedFormula(reference)) {
427 return null;
428 }
429 final Reference ref = getReference(reference, getCurrentContext(), false, false);
430 final Element formula = ref.getNode().getFormula();
431 return getNormalizedFormula(ref.getNode().getQedeqBo(), formula);
432 }
433
434 public Element getNormalizedFormula(final Element formula) {
435 return getNormalizedFormula(getQedeqBo(), formula);
436 }
437
438 private Element getNormalizedFormula(final KernelQedeqBo qedeq, final Element formula) {
439 if (formula == null) {
440 return null;
441 }
442 if (formula.isAtom()) {
443 return new DefaultAtom(formula.getAtom().getString());
444 }
445 return getNormalizedFormula(qedeq, formula.getList());
446 }
447
448 private ElementList getNormalizedFormula(final KernelQedeqBo qedeq, final ElementList formula) {
449 final ElementList result = new DefaultElementList(formula.getOperator());
450 if (FormulaUtility.isPredicateConstant(formula)) {
451 final PredicateKey key = new PredicateKey(formula.getElement(0).getAtom().getString(),
452 "" + (formula.getList().size() - 1));
453 final DefaultAtom atom = new DefaultAtom(
454 qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
455 + "$" + key.getName());
456 result.add(atom);
457 for (int i = 1; i < formula.size(); i++) {
458 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
459 }
460 } else if (FormulaUtility.isFunctionConstant(formula)) {
461 final FunctionKey key = new FunctionKey(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 {
471 for (int i = 0; i < formula.size(); i++) {
472 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
473 }
474 }
475 return result;
476 }
477
478 }
|