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
19 import org.qedeq.base.io.Parameters;
20 import org.qedeq.base.io.Version;
21 import org.qedeq.base.trace.Trace;
22 import org.qedeq.base.utility.StringUtility;
23 import org.qedeq.kernel.bo.log.QedeqLog;
24 import org.qedeq.kernel.bo.logic.ProofCheckerFactoryImpl;
25 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
26 import org.qedeq.kernel.bo.logic.common.FunctionKey;
27 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
28 import org.qedeq.kernel.bo.logic.common.PredicateKey;
29 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
30 import org.qedeq.kernel.bo.logic.proof.checker.ProofCheckException;
31 import org.qedeq.kernel.bo.logic.proof.common.ProofCheckerFactory;
32 import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
33 import org.qedeq.kernel.bo.module.InternalModuleServiceCall;
34 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
35 import org.qedeq.kernel.bo.module.KernelQedeqBo;
36 import org.qedeq.kernel.bo.module.Reference;
37 import org.qedeq.kernel.bo.service.basis.ControlVisitor;
38 import org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor;
39 import org.qedeq.kernel.se.base.list.Element;
40 import org.qedeq.kernel.se.base.list.ElementList;
41 import org.qedeq.kernel.se.base.module.Axiom;
42 import org.qedeq.kernel.se.base.module.ChangedRule;
43 import org.qedeq.kernel.se.base.module.ChangedRuleList;
44 import org.qedeq.kernel.se.base.module.FormalProof;
45 import org.qedeq.kernel.se.base.module.FormalProofLineList;
46 import org.qedeq.kernel.se.base.module.FunctionDefinition;
47 import org.qedeq.kernel.se.base.module.Header;
48 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
49 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
50 import org.qedeq.kernel.se.base.module.PredicateDefinition;
51 import org.qedeq.kernel.se.base.module.Proposition;
52 import org.qedeq.kernel.se.base.module.Rule;
53 import org.qedeq.kernel.se.common.CheckLevel;
54 import org.qedeq.kernel.se.common.ModuleContext;
55 import org.qedeq.kernel.se.common.ModuleDataException;
56 import org.qedeq.kernel.se.common.ModuleService;
57 import org.qedeq.kernel.se.common.RuleKey;
58 import org.qedeq.kernel.se.common.SourceFileException;
59 import org.qedeq.kernel.se.common.SourceFileExceptionList;
60 import org.qedeq.kernel.se.dto.list.DefaultAtom;
61 import org.qedeq.kernel.se.dto.list.DefaultElementList;
62 import org.qedeq.kernel.se.state.FormallyProvedState;
63 import org.qedeq.kernel.se.visitor.InterruptException;
64
65
66
67
68
69
70
71 public final class FormalProofCheckerExecutor extends ControlVisitor implements ModuleServicePluginExecutor,
72 ReferenceResolver, RuleChecker {
73
74
75 private static final Class CLASS = FormalProofCheckerExecutor.class;
76
77
78 private ProofCheckerFactory checkerFactory = null;
79
80
81 private Version ruleVersion;
82
83
84
85
86
87
88
89
90 FormalProofCheckerExecutor(final ModuleService plugin, final KernelQedeqBo qedeq,
91 final Parameters parameters) {
92 super(plugin, qedeq);
93 final String method = "FormalProofCheckerExecutor(Plugin, KernelQedeqBo, Map)";
94 final String checkerFactoryClass = parameters.getString("checkerFactory");
95 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
96 try {
97 Class cl = Class.forName(checkerFactoryClass);
98 checkerFactory = (ProofCheckerFactory) cl.newInstance();
99 } catch (ClassNotFoundException e) {
100 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class not in class path: "
101 + checkerFactoryClass, e);
102 } catch (InstantiationException e) {
103 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class could not be instanciated: "
104 + checkerFactoryClass, e);
105 } catch (IllegalAccessException e) {
106 Trace.fatal(CLASS, this, method,
107 "Programming error, access for instantiation failed for model: "
108 + checkerFactoryClass, e);
109 } catch (RuntimeException e) {
110 Trace.fatal(CLASS, this, method,
111 "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
112 }
113 }
114
115 if (checkerFactory == null) {
116 checkerFactory = new ProofCheckerFactoryImpl();
117 }
118 }
119
120 public Object executePlugin(final InternalModuleServiceCall call, final Object data) throws InterruptException {
121
122 ruleVersion = new Version("0.00.00");
123 QedeqLog.getInstance().logRequest(
124 "Check logical correctness", getKernelQedeqBo().getUrl());
125 getServices().checkWellFormedness(call.getInternalServiceProcess(), getKernelQedeqBo());
126 if (!getKernelQedeqBo().isWellFormed()) {
127 final String msg = "Check of logical correctness failed";
128 QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
129 "Module is not even well formed.");
130 return Boolean.FALSE;
131 }
132 getKernelQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_EXTERNAL_CHECKING);
133 getKernelQedeqBo().getLabels().resetNodesToProvedUnchecked();
134 final KernelModuleReferenceList list = getKernelQedeqBo().getKernelRequiredModules();
135 for (int i = 0; i < list.size(); i++) {
136 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
137 getServices().checkFormallyProved(call.getInternalServiceProcess(), list.getKernelQedeqBo(i));
138 if (list.getKernelQedeqBo(i).hasErrors()) {
139 addError(new CheckRequiredModuleException(
140 LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
141 LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
142 + list.getQedeqBo(i).getModuleAddress(),
143 list.getModuleContext(i)));
144 }
145 }
146
147 if (getKernelQedeqBo().hasErrors()) {
148 getKernelQedeqBo().setFormallyProvedFailureState(FormallyProvedState.STATE_EXTERNAL_CHECKING_FAILED,
149 getErrorList());
150 final String msg = "Check of logical correctness failed";
151 QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
152 StringUtility.replace(getKernelQedeqBo().getErrors().getMessage(), "\n", "\n\t"));
153 return Boolean.FALSE;
154 }
155 getKernelQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_INTERNAL_CHECKING);
156 try {
157 traverse(call.getInternalServiceProcess());
158 } catch (SourceFileExceptionList e) {
159 getKernelQedeqBo().setFormallyProvedFailureState(FormallyProvedState.STATE_INTERNAL_CHECKING_FAILED,
160 getErrorList());
161 final String msg = "Check of logical correctness failed";
162 QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
163 StringUtility.replace(e.getMessage(), "\n", "\n\t"));
164 return Boolean.FALSE;
165 }
166 getKernelQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_CHECKED);
167 QedeqLog.getInstance().logSuccessfulReply(
168 "Check of logical correctness successful", getKernelQedeqBo().getUrl());
169 return Boolean.TRUE;
170 }
171
172 public void visitEnter(final Header header) throws ModuleDataException {
173 if (header.getSpecification() == null
174 || header.getSpecification().getRuleVersion() == null) {
175 return;
176 }
177 final String context = getCurrentContext().getLocationWithinModule();
178 setLocationWithinModule(context + ".getSpecification().getRuleVersion()");
179 final String version = header.getSpecification().getRuleVersion().trim();
180 if (!checkerFactory.isRuleVersionSupported(version)) {
181 addError(new ProofCheckException(
182 LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_CODE,
183 LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_TEXT + version,
184 getCurrentContext()));
185 } else {
186 try {
187 ruleVersion = new Version(version);
188 } catch (RuntimeException e) {
189 addError(new ProofCheckException(
190 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
191 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + version,
192 getCurrentContext()));
193 }
194 }
195 setLocationWithinModule(context);
196 }
197
198 public void visitEnter(final Axiom axiom) throws ModuleDataException {
199 if (getNodeBo().isWellFormed()) {
200 getNodeBo().setProved(CheckLevel.SUCCESS);
201 } else {
202 getNodeBo().setProved(CheckLevel.FAILURE);
203 addError(new ProofCheckException(
204 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
205 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
206 getCurrentContext()));
207 return;
208 }
209 setBlocked(true);
210 }
211
212 public void visitLeave(final Axiom axiom) {
213 setBlocked(false);
214 }
215
216 public void visitEnter(final PredicateDefinition definition)
217 throws ModuleDataException {
218 if (getNodeBo().isWellFormed()) {
219 getNodeBo().setProved(CheckLevel.SUCCESS);
220 } else {
221 getNodeBo().setProved(CheckLevel.FAILURE);
222 addError(new ProofCheckException(
223 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
224 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
225 getCurrentContext()));
226 return;
227 }
228 setBlocked(true);
229 }
230
231 public void visitLeave(final PredicateDefinition definition) {
232 setBlocked(false);
233 }
234
235 public void visitEnter(final InitialPredicateDefinition definition)
236 throws ModuleDataException {
237 if (getNodeBo().isWellFormed()) {
238 getNodeBo().setProved(CheckLevel.SUCCESS);
239 } else {
240 getNodeBo().setProved(CheckLevel.FAILURE);
241 addError(new ProofCheckException(
242 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
243 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
244 getCurrentContext()));
245 return;
246 }
247 setBlocked(true);
248 }
249
250 public void visitLeave(final InitialPredicateDefinition definition) {
251 setBlocked(false);
252 }
253
254 public void visitEnter(final InitialFunctionDefinition definition)
255 throws ModuleDataException {
256 if (getNodeBo().isWellFormed()) {
257 getNodeBo().setProved(CheckLevel.SUCCESS);
258 } else {
259 getNodeBo().setProved(CheckLevel.FAILURE);
260 addError(new ProofCheckException(
261 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
262 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
263 getCurrentContext()));
264 return;
265 }
266 setBlocked(true);
267 }
268
269 public void visitLeave(final InitialFunctionDefinition definition) {
270 setBlocked(false);
271 }
272
273 public void visitEnter(final FunctionDefinition definition)
274 throws ModuleDataException {
275 if (getNodeBo().isWellFormed()) {
276 getNodeBo().setProved(CheckLevel.SUCCESS);
277 } else {
278 getNodeBo().setProved(CheckLevel.FAILURE);
279 addError(new ProofCheckException(
280 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
281 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
282 getCurrentContext()));
283 return;
284 }
285 setBlocked(true);
286 }
287
288 public void visitLeave(final FunctionDefinition definition) {
289 setBlocked(false);
290 }
291
292 public void visitEnter(final Proposition proposition)
293 throws ModuleDataException {
294
295 if (!getNodeBo().isWellFormed()) {
296 getNodeBo().setProved(CheckLevel.FAILURE);
297 addError(new ProofCheckException(
298 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
299 LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
300 getCurrentContext()));
301 return;
302 }
303 getNodeBo().setProved(CheckLevel.UNCHECKED);
304 if (proposition.getFormula() == null) {
305 getNodeBo().setProved(CheckLevel.FAILURE);
306 addError(new ProofCheckException(
307 LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_CODE,
308 LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_TEXT,
309 getCurrentContext()));
310 return;
311 }
312 final String context = getCurrentContext().getLocationWithinModule();
313 boolean correctProofFound = false;
314
315 if (proposition.getFormalProofList() != null) {
316 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
317 final FormalProof proof = proposition.getFormalProofList().get(i);
318 if (proof != null) {
319 final FormalProofLineList list = proof.getFormalProofLineList();
320 if (list != null) {
321 setLocationWithinModule(context + ".getFormalProofList().get("
322 + i + ").getFormalProofLineList()");
323 LogicalCheckExceptionList eList
324 = checkerFactory.createProofChecker(ruleVersion).checkProof(
325 proposition.getFormula().getElement(), list, this,
326 getCurrentContext(),
327 this);
328 if (!correctProofFound && eList.size() == 0) {
329 correctProofFound = true;
330 }
331 for (int j = 0; j < eList.size(); j++) {
332 addError(eList.get(j));
333 }
334 }
335 }
336 }
337 }
338 setLocationWithinModule(context + ".getFormula()");
339
340 if (correctProofFound) {
341 getNodeBo().setProved(CheckLevel.SUCCESS);
342 } else {
343 getNodeBo().setProved(CheckLevel.FAILURE);
344 addError(new ProofCheckException(
345 LogicErrors.NO_FORMAL_PROOF_FOUND_CODE,
346 LogicErrors.NO_FORMAL_PROOF_FOUND_TEXT,
347 getCurrentContext()));
348 }
349 setBlocked(true);
350 }
351
352 public void visitLeave(final Proposition definition) {
353 setBlocked(false);
354 }
355
356 public void visitEnter(final Rule rule) throws ModuleDataException {
357 final String context = getCurrentContext().getLocationWithinModule();
358
359
360
361 getNodeBo().setProved(CheckLevel.UNCHECKED);
362 final ChangedRuleList list = rule.getChangedRuleList();
363 for (int i = 0; list != null && i < list.size(); i++) {
364 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
365 final ChangedRule r = list.get(i);
366 if (!Version.equals(rule.getVersion(), r.getVersion())) {
367 addError(new ProofCheckException(
368 LogicErrors.OTHER_RULE_VERSION_EXPECTED_CODE,
369 LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT1 + rule.getVersion()
370 + LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT2 + r.getVersion(),
371 getCurrentContext()));
372 }
373 }
374
375 if (getNodeBo().isNotProved()) {
376 getNodeBo().setProved(CheckLevel.SUCCESS);
377 } else {
378 getNodeBo().setProved(CheckLevel.FAILURE);
379 }
380 }
381
382 protected void addError(final ModuleDataException me) {
383 if (getNodeBo() != null) {
384 getNodeBo().setProved(CheckLevel.FAILURE);
385 }
386 super.addError(me);
387 }
388
389 protected void addError(final SourceFileException me) {
390 if (getNodeBo() != null) {
391 getNodeBo().setProved(CheckLevel.FAILURE);
392 }
393 super.addError(me);
394 }
395
396 public boolean isProvedFormula(final String reference) {
397 final String method = "hasProvedFormula";
398 final Reference ref = getReference(reference, getCurrentContext(), false, false);
399 if (ref == null) {
400 Trace.info(CLASS, method, "ref == null");
401 return false;
402 }
403 if (ref.isExternalModuleReference()) {
404 Trace.info(CLASS, method, "ref is external module");
405 return false;
406 }
407 if (!ref.isNodeReference()) {
408 Trace.info(CLASS, method, "ref is no node reference");
409 return false;
410 }
411 if (null == ref.getNode()) {
412 Trace.info(CLASS, method, "ref node == null");
413 return false;
414 }
415 if (ref.isSubReference()) {
416 return false;
417 }
418 if (!ref.isProofLineReference()) {
419 if (!ref.getNode().isProved()) {
420 Trace.info(CLASS, method, "ref node is not marked as proved: " + reference);
421 }
422 if (!ref.getNode().isProved()) {
423 return false;
424 }
425 if (!ref.getNode().hasFormula()) {
426 Trace.info(CLASS, method, "node has no formula: " + reference);
427 return false;
428 }
429 return ref.getNode().isProved();
430 }
431 Trace.info(CLASS, method, "proof line references are not ok!");
432 return false;
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(getKernelQedeqBo(), 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
490 return false;
491 }
492
493 public ModuleContext getReferenceContext(final String reference) {
494
495 return null;
496 }
497
498 public Element getNormalizedLocalProofLineReference(final String reference) {
499
500 return null;
501 }
502
503 public RuleKey getRule(final String ruleName) {
504 final RuleKey local = getLocalRuleKey(ruleName);
505 if (local == null) {
506 return getKernelQedeqBo().getExistenceChecker().getParentRuleKey(
507 ruleName);
508 }
509 return local;
510 }
511
512
513 }