1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.bo.logic.proof.checker;
17
18 import java.util.HashMap;
19 import java.util.Map;
20
21 import org.qedeq.base.io.Version;
22 import org.qedeq.base.utility.Enumerator;
23 import org.qedeq.base.utility.EqualsUtility;
24 import org.qedeq.base.utility.StringUtility;
25 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
26 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
27 import org.qedeq.kernel.bo.logic.common.Operators;
28 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
29 import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
30 import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
31 import org.qedeq.kernel.se.base.list.Element;
32 import org.qedeq.kernel.se.base.list.ElementList;
33 import org.qedeq.kernel.se.base.module.Add;
34 import org.qedeq.kernel.se.base.module.Existential;
35 import org.qedeq.kernel.se.base.module.FormalProofLine;
36 import org.qedeq.kernel.se.base.module.FormalProofLineList;
37 import org.qedeq.kernel.se.base.module.ModusPonens;
38 import org.qedeq.kernel.se.base.module.Reason;
39 import org.qedeq.kernel.se.base.module.Rename;
40 import org.qedeq.kernel.se.base.module.Rule;
41 import org.qedeq.kernel.se.base.module.SubstFree;
42 import org.qedeq.kernel.se.base.module.SubstFunc;
43 import org.qedeq.kernel.se.base.module.SubstPred;
44 import org.qedeq.kernel.se.base.module.Universal;
45 import org.qedeq.kernel.se.common.ModuleContext;
46 import org.qedeq.kernel.se.common.RuleKey;
47 import org.qedeq.kernel.se.dto.list.DefaultElementList;
48 import org.qedeq.kernel.se.dto.list.ElementSet;
49
50
51
52
53
54
55
56 public class ProofChecker1Impl implements ProofChecker {
57
58
59 private FormalProofLineList proof;
60
61
62 private ModuleContext moduleContext;
63
64
65 private ModuleContext currentContext;
66
67
68 private ReferenceResolver resolver;
69
70
71 private LogicalCheckExceptionList exceptions;
72
73
74 private boolean[] lineProved;
75
76
77 private Map label2line;
78
79
80 private final Version ruleVersion;
81
82
83 private RuleChecker checker;
84
85
86
87
88
89 public ProofChecker1Impl() {
90 this.ruleVersion = new Version("0.01.00");
91 }
92
93 public LogicalCheckExceptionList checkRule(final Rule rule,
94 final ModuleContext context, final RuleChecker checker,
95 final ReferenceResolver resolver) {
96 exceptions = new LogicalCheckExceptionList();
97 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
98 if (rule.getVersion() == null || !ruleVersion.equals(rule.getVersion())) {
99 final ProofCheckException ex = new ProofCheckException(
100 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
101 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey
102 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + "{" + ruleVersion + "}",
103 context);
104 exceptions.add(ex);
105 }
106 return exceptions;
107 }
108
109 public LogicalCheckExceptionList checkProof(final Element formula,
110 final FormalProofLineList proof,
111 final RuleChecker checker,
112 final ModuleContext moduleContext,
113 final ReferenceResolver resolver) {
114 this.proof = proof;
115 this.resolver = resolver;
116 this.moduleContext = moduleContext;
117 this.checker = checker;
118
119 currentContext = new ModuleContext(moduleContext);
120 exceptions = new LogicalCheckExceptionList();
121 final String context = moduleContext.getLocationWithinModule();
122 lineProved = new boolean[proof.size()];
123 label2line = new HashMap();
124 for (int i = 0; i < proof.size(); i++) {
125 boolean ok = true;
126 setLocationWithinModule(context + ".get(" + i + ")");
127 final FormalProofLine line = proof.get(i);
128 if (line == null || line.getFormula() == null
129 || line.getFormula().getElement() == null) {
130 ok = false;
131 handleProofCheckException(
132 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
133 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
134 getCurrentContext());
135 continue;
136 }
137 setLocationWithinModule(context + ".get(" + i + ").getReason()");
138 final Reason reason = line.getReason();
139 if (reason == null) {
140 ok = false;
141 handleProofCheckException(
142 BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
143 BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
144 getCurrentContext());
145 continue;
146 }
147 if (line.getLabel() != null && line.getLabel().length() > 0) {
148 final Integer n = (Integer) label2line.get(line.getLabel());
149 if (n != null) {
150 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
151 moduleContext.getLocationWithinModule() + ".get("
152 + label2line.get(line.getLabel())
153 + ").getLabel()");
154 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
155 handleProofCheckException(
156 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
157 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
158 + line.getLabel(),
159 getCurrentContext(),
160 lc);
161 }
162 label2line.put(line.getLabel(), new Integer(i));
163 }
164
165
166
167 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
168 if (getReason.endsWith("Vo")) {
169 getReason = getReason.substring(0, getReason.length() - 2) + "()";
170 setLocationWithinModule(context + ".get(" + i + ").getReason()"
171 + getReason);
172 }
173 if (reason instanceof Add) {
174 ok = check((Add) reason, i, line.getFormula().getElement());
175 } else if (reason instanceof Rename) {
176 ok = check((Rename) reason, i, line.getFormula().getElement());
177 } else if (reason instanceof ModusPonens) {
178 ok = check((ModusPonens) reason, i, line.getFormula().getElement());
179 } else if (reason instanceof SubstFree) {
180 ok = check((SubstFree) reason, i, line.getFormula().getElement());
181 } else if (reason instanceof SubstPred) {
182 ok = check((SubstPred) reason, i, line.getFormula().getElement());
183 } else if (reason instanceof SubstFunc) {
184 ok = check((SubstFunc) reason, i, line.getFormula().getElement());
185 } else if (reason instanceof Universal) {
186 ok = check((Universal) reason, i, line.getFormula().getElement());
187 } else if (reason instanceof Existential) {
188 ok = check((Existential) reason, i, line.getFormula().getElement());
189 } else {
190 ok = false;
191 handleProofCheckException(
192 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
193 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
194 + reason.getName(),
195 getCurrentContext());
196 }
197 lineProved[i] = ok;
198
199 if (i == proof.size() - 1) {
200 if (!formula.equals(line.getFormula().getElement())) {
201 handleProofCheckException(
202 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
203 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT
204 + reason.getName(),
205 getModuleContextOfProofLineFormula(i));
206 }
207 }
208 }
209 return exceptions;
210 }
211
212 private boolean check(final Add add, final int i, final Element element) {
213 final String context = currentContext.getLocationWithinModule();
214 boolean ok = true;
215 if (add.getReference() == null) {
216 ok = false;
217 setLocationWithinModule(context + ".getReference()");
218 handleProofCheckException(
219 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
220 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
221 getCurrentContext());
222 return ok;
223 }
224 if (!resolver.isProvedFormula(add.getReference())) {
225 ok = false;
226 setLocationWithinModule(context + ".getReference()");
227 handleProofCheckException(
228 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
229 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
230 + add.getReference(),
231 getCurrentContext());
232 return ok;
233 }
234 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
235 final Element current = resolver.getNormalizedFormula(element);
236 if (!EqualsUtility.equals(expected, current)) {
237 ok = false;
238 handleProofCheckException(
239 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
240 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
241 + add.getReference(),
242 getDiffModuleContextOfProofLineFormula(i, expected));
243 return ok;
244 }
245 final RuleKey defined = checker.getRule(add.getName());
246 if (defined == null) {
247 ok = false;
248 handleProofCheckException(
249 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
250 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
251 + add.getName(),
252 getCurrentContext());
253 return ok;
254 } else if (!ruleVersion.equals(defined.getVersion())) {
255 ok = false;
256 handleProofCheckException(
257 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
258 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
259 getCurrentContext());
260 return ok;
261 }
262 return ok;
263 }
264
265 private boolean check(final Rename rename, final int i, final Element element) {
266 final String context = currentContext.getLocationWithinModule();
267 boolean ok = true;
268 final Integer n = (Integer) label2line.get(rename.getReference());
269 if (n == null) {
270 ok = false;
271 setLocationWithinModule(context + ".getReference()");
272 handleProofCheckException(
273 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
274 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
275 + rename.getReference(),
276 getCurrentContext());
277
278
279
280
281
282
283
284
285 } else {
286 final Element f = getNormalizedProofLine(n);
287 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
288 rename.getOriginalSubjectVariable(),
289 rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
290 new Enumerator());
291 final Element current = resolver.getNormalizedFormula(element);
292 if (!EqualsUtility.equals(expected, current)) {
293 ok = false;
294 handleProofCheckException(
295 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
296 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
297 + rename.getReference(),
298 getDiffModuleContextOfProofLineFormula(i, expected));
299 } else {
300 ok = true;
301 }
302 }
303 final RuleKey defined = checker.getRule(rename.getName());
304 if (defined == null) {
305 ok = false;
306 handleProofCheckException(
307 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
308 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
309 + rename.getName(),
310 getCurrentContext());
311 return ok;
312 } else if (!ruleVersion.equals(defined.getVersion())) {
313 ok = false;
314 handleProofCheckException(
315 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
316 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
317 getCurrentContext());
318 return ok;
319 }
320 return ok;
321 }
322
323 private boolean check(final SubstFree substFree, final int i, final Element element) {
324 final String context = currentContext.getLocationWithinModule();
325 boolean ok = true;
326 final Integer n = (Integer) label2line.get(substFree.getReference());
327 if (n == null) {
328 ok = false;
329 setLocationWithinModule(context + ".getReference()");
330 handleProofCheckException(
331 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
332 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
333 + substFree.getReference(),
334 getCurrentContext());
335
336
337
338
339
340
341
342
343 } else {
344 final Element f = getNormalizedProofLine(n);
345 final Element current = resolver.getNormalizedFormula(element);
346 final Element expected = f.replace(substFree.getSubjectVariable(),
347 resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
348 if (!EqualsUtility.equals(current, expected)) {
349 ok = false;
350 handleProofCheckException(
351 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
352 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
353 + substFree.getReference(),
354 getDiffModuleContextOfProofLineFormula(i, expected));
355 return ok;
356 }
357 }
358 final RuleKey defined = checker.getRule(substFree.getName());
359 if (defined == null) {
360 ok = false;
361 handleProofCheckException(
362 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
363 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
364 + substFree.getName(),
365 getCurrentContext());
366 return ok;
367 } else if (!ruleVersion.equals(defined.getVersion())) {
368 ok = false;
369 handleProofCheckException(
370 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
371 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
372 getCurrentContext());
373 return ok;
374 }
375 return ok;
376 }
377
378 private boolean check(final SubstPred substPred, final int i, final Element element) {
379 final String context = currentContext.getLocationWithinModule();
380 boolean ok = true;
381 final Integer n = (Integer) label2line.get(substPred.getReference());
382 if (n == null) {
383 ok = false;
384 setLocationWithinModule(context + ".getReference()");
385 handleProofCheckException(
386 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
387 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
388 + substPred.getReference(),
389 getCurrentContext());
390
391
392
393
394
395
396
397
398 } else {
399 final Element alpha = getNormalizedProofLine(n);
400 final Element current = resolver.getNormalizedFormula(element);
401 if (substPred.getSubstituteFormula() == null) {
402 ok = false;
403 handleProofCheckException(
404 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
405 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
406 getCurrentContext());
407 return ok;
408 }
409 final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
410 final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
411 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
412 if (!EqualsUtility.equals(current, expected)) {
413 ok = false;
414 handleProofCheckException(
415 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
416 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
417 + substPred.getReference(),
418 getDiffModuleContextOfProofLineFormula(i, expected));
419 return ok;
420 }
421
422
423 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
424 if (predFree.size() != p.getList().size() - 1) {
425 ok = false;
426 setLocationWithinModule(context + ".getPredicateVariable()");
427 handleProofCheckException(
428 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
429 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
430 getDiffModuleContextOfProofLineFormula(i, expected));
431 return ok;
432 }
433 for (int j = 1; j < p.getList().size(); j++) {
434 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
435 ok = false;
436 setLocationWithinModule(context + ".getPredicateVariable()");
437 handleProofCheckException(
438 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
439 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
440 getCurrentContext());
441 return ok;
442 }
443 }
444
445
446 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
447 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
448 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
449 ok = false;
450 setLocationWithinModule(context + ".getSubstituteFormula()");
451 handleProofCheckException(
452 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
453 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
454 getCurrentContext());
455 return ok;
456 }
457
458
459 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
460 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
461 ok = false;
462 setLocationWithinModule(context + ".getSubstituteFormula()");
463 handleProofCheckException(
464 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
465 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
466 getCurrentContext());
467 return ok;
468 }
469
470
471 }
472 final RuleKey defined = checker.getRule(substPred.getName());
473 if (defined == null) {
474 ok = false;
475 handleProofCheckException(
476 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
477 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
478 + substPred.getName(),
479 getCurrentContext());
480 return ok;
481 } else if (!ruleVersion.equals(defined.getVersion())) {
482 ok = false;
483 handleProofCheckException(
484 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
485 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
486 getCurrentContext());
487 return ok;
488 }
489 return ok;
490 }
491
492 private boolean check(final SubstFunc substFunc, final int i, final Element element) {
493 final String context = currentContext.getLocationWithinModule();
494 boolean ok = true;
495 final Integer n = (Integer) label2line.get(substFunc.getReference());
496 if (n == null) {
497 ok = false;
498 setLocationWithinModule(context + ".getReference()");
499 handleProofCheckException(
500 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
501 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
502 + substFunc.getReference(),
503 getCurrentContext());
504
505
506
507
508
509
510
511
512 } else {
513 final Element alpha = getNormalizedProofLine(n);
514 final Element current = resolver.getNormalizedFormula(element);
515 if (substFunc.getSubstituteTerm() == null) {
516 ok = false;
517 handleProofCheckException(
518 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
519 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
520 getCurrentContext());
521 return ok;
522 }
523 final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
524 final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
525 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
526 if (!EqualsUtility.equals(current, expected)) {
527 ok = false;
528 handleProofCheckException(
529 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
530 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
531 + substFunc.getReference(),
532 getDiffModuleContextOfProofLineFormula(i, expected));
533 return ok;
534 }
535
536
537 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
538 if (funcFree.size() != sigma.getList().size() - 1) {
539 ok = false;
540 setLocationWithinModule(context + ".getPredicateVariable()");
541 handleProofCheckException(
542 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
543 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
544 getDiffModuleContextOfProofLineFormula(i, expected));
545 return ok;
546 }
547 for (int j = 1; j < sigma.getList().size(); j++) {
548 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
549 ok = false;
550 setLocationWithinModule(context + ".getPredicateVariable()");
551 handleProofCheckException(
552 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
553 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
554 getCurrentContext());
555 return ok;
556 }
557 }
558
559
560 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
561 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
562 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
563 ok = false;
564 setLocationWithinModule(context + ".getSubstituteFormula()");
565 handleProofCheckException(
566 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
567 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
568 getCurrentContext());
569 return ok;
570 }
571
572
573 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
574 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
575 ok = false;
576 setLocationWithinModule(context + ".getSubstituteFormula()");
577 handleProofCheckException(
578 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
579 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
580 getCurrentContext());
581 return ok;
582 }
583
584
585 }
586 final RuleKey defined = checker.getRule(substFunc.getName());
587 if (defined == null) {
588 ok = false;
589 handleProofCheckException(
590 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
591 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
592 + substFunc.getName(),
593 getCurrentContext());
594 return ok;
595 } else if (!ruleVersion.equals(defined.getVersion())) {
596 ok = false;
597 handleProofCheckException(
598 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
599 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
600 getCurrentContext());
601 return ok;
602 }
603 return ok;
604 }
605
606 private boolean check(final ModusPonens mp, final int i, final Element element) {
607 final String context = currentContext.getLocationWithinModule();
608 boolean ok = true;
609 final Integer n1 = (Integer) label2line.get(mp.getReference1());
610 if (n1 == null) {
611 ok = false;
612 setLocationWithinModule(context + ".getReference1()");
613 handleProofCheckException(
614 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
615 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
616 + mp.getReference1(),
617 getCurrentContext());
618
619
620
621
622
623
624
625
626 }
627 final Integer n2 = (Integer) label2line.get(mp.getReference2());
628 if (n2 == null) {
629 ok = false;
630 setLocationWithinModule(context + ".getReference2()");
631 handleProofCheckException(
632 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
633 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
634 + mp.getReference2(),
635 getCurrentContext());
636
637
638
639
640
641
642
643
644 }
645 if (ok) {
646 final Element f1 = getNormalizedProofLine(n1);
647 final Element f2 = getNormalizedProofLine(n2);
648 final Element current = getNormalizedProofLine(i);
649 if (!FormulaUtility.isImplication(f1)) {
650 ok = false;
651 setLocationWithinModule(context + ".getReference1()");
652 handleProofCheckException(
653 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
654 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
655 + mp.getReference1(),
656 getCurrentContext());
657 } else if (!f2.equals(f1.getList().getElement(0))) {
658 ok = false;
659 setLocationWithinModule(context + ".getReference2()");
660 handleProofCheckException(
661 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
662 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
663 + mp.getReference2(),
664 getCurrentContext(),
665 getModuleContextOfProofLineFormula(n1.intValue()));
666 } else if (!current.equals(f1.getList().getElement(1))) {
667 ok = false;
668 setLocationWithinModule(context + ".getReference1()");
669 handleProofCheckException(
670 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
671 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
672 + mp.getReference1(),
673 getCurrentContext(),
674 getModuleContextOfProofLineFormula(n1.intValue()));
675 } else {
676 ok = true;
677 }
678 }
679 final RuleKey defined = checker.getRule(mp.getName());
680 if (defined == null) {
681 ok = false;
682 handleProofCheckException(
683 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
684 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
685 + mp.getName(),
686 getCurrentContext());
687 return ok;
688 } else if (!ruleVersion.equals(defined.getVersion())) {
689 ok = false;
690 handleProofCheckException(
691 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
692 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
693 getCurrentContext());
694 return ok;
695 }
696 return ok;
697 }
698
699 private boolean check(final Universal universal, final int i, final Element element) {
700 final String context = currentContext.getLocationWithinModule();
701 boolean ok = true;
702 final Integer n = (Integer) label2line.get(universal.getReference());
703 if (n == null) {
704 ok = false;
705 setLocationWithinModule(context + ".getReference()");
706 handleProofCheckException(
707 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
708 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
709 + universal.getReference(),
710 getCurrentContext());
711
712
713
714
715
716
717
718
719 } else {
720 final Element f = getNormalizedProofLine(n);
721 final Element current = resolver.getNormalizedFormula(element);
722 if (!FormulaUtility.isImplication(f)) {
723 ok = false;
724 setLocationWithinModule(context + ".getReference()");
725 handleProofCheckException(
726 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
727 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
728 + universal.getReference(),
729 getCurrentContext());
730 return ok;
731 }
732 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
733 ok = false;
734 setLocationWithinModule(context + ".getSubjectVariable()");
735 handleProofCheckException(
736 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
737 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
738 getCurrentContext());
739 return ok;
740 }
741 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
742 expected.add((f.getList().getElement(0)));
743 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
744 uni.add(universal.getSubjectVariable());
745 uni.add(f.getList().getElement(1));
746 expected.add(uni);
747 if (!EqualsUtility.equals(current, expected)) {
748 ok = false;
749 handleProofCheckException(
750 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
751 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
752 + universal.getReference(),
753 getDiffModuleContextOfProofLineFormula(i, expected));
754 return ok;
755 }
756 }
757 final RuleKey defined = checker.getRule(universal.getName());
758 if (defined == null) {
759 ok = false;
760 handleProofCheckException(
761 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
762 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
763 + universal.getName(),
764 getCurrentContext());
765 return ok;
766 } else if (!ruleVersion.equals(defined.getVersion())) {
767 ok = false;
768 handleProofCheckException(
769 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
770 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
771 getCurrentContext());
772 return ok;
773 }
774 return ok;
775 }
776
777 private boolean check(final Existential existential, final int i, final Element element) {
778 final String context = currentContext.getLocationWithinModule();
779 boolean ok = true;
780 final Integer n = (Integer) label2line.get(existential.getReference());
781 if (n == null) {
782 ok = false;
783 setLocationWithinModule(context + ".getReference()");
784 handleProofCheckException(
785 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
786 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
787 + existential.getReference(),
788 getCurrentContext());
789
790
791
792
793
794
795
796
797 } else {
798 final Element f = getNormalizedProofLine(n);
799 final Element current = resolver.getNormalizedFormula(element);
800 if (!FormulaUtility.isImplication(f)) {
801 ok = false;
802 setLocationWithinModule(context + ".getReference()");
803 handleProofCheckException(
804 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
805 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
806 + existential.getReference(),
807 getCurrentContext());
808 return ok;
809 }
810 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
811 ok = false;
812 setLocationWithinModule(context + ".getSubjectVariable()");
813 handleProofCheckException(
814 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
815 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
816 getCurrentContext());
817 return ok;
818 }
819 final DefaultElementList expected = new DefaultElementList(f.getList().getOperator());
820 final ElementList exi = new DefaultElementList(
821 Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
822 exi.add(existential.getSubjectVariable());
823 exi.add(f.getList().getElement(0));
824 expected.add(exi);
825 expected.add((f.getList().getElement(1)));
826 if (!EqualsUtility.equals(current, expected)) {
827 ok = false;
828 handleProofCheckException(
829 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
830 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
831 + existential.getReference(),
832 getDiffModuleContextOfProofLineFormula(i, expected));
833 return ok;
834 }
835 }
836 final RuleKey defined = checker.getRule(existential.getName());
837 if (defined == null) {
838 ok = false;
839 handleProofCheckException(
840 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
841 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
842 + existential.getName(),
843 getCurrentContext());
844 return ok;
845 } else if (!ruleVersion.equals(defined.getVersion())) {
846 ok = false;
847 handleProofCheckException(
848 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
849 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
850 getCurrentContext());
851 return ok;
852 }
853 return ok;
854 }
855
856 private ModuleContext getModuleContextOfProofLineFormula(final int i) {
857 return new ModuleContext(moduleContext.getModuleLocation(),
858 moduleContext.getLocationWithinModule() + ".get(" + i
859 + ").getFormula().getElement()");
860 }
861
862 private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
863 final Element expected) {
864 final String diff = FormulaUtility.getDifferenceLocation(
865 proof.get(i).getFormula().getElement(), expected);
866 return new ModuleContext(moduleContext.getModuleLocation(),
867 moduleContext.getLocationWithinModule() + ".get(" + i
868 + ").getFormula().getElement()" + diff);
869 }
870
871 private Element getNormalizedProofLine(final Integer n) {
872 if (n == null) {
873 return null;
874 }
875 return getNormalizedProofLine(n.intValue());
876 }
877
878 private Element getNormalizedProofLine(final int i) {
879 if (i < 0 || i >= proof.size()) {
880 return null;
881 }
882 return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
883 }
884
885
886
887
888
889
890
891
892 private void handleProofCheckException(final int code, final String msg,
893 final ModuleContext context) {
894
895
896 final ProofCheckException ex = new ProofCheckException(code, msg, context);
897 exceptions.add(ex);
898 }
899
900
901
902
903
904
905
906
907
908 private void handleProofCheckException(final int code, final String msg,
909 final ModuleContext context, final ModuleContext referenceContext) {
910
911
912 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
913 referenceContext);
914 exceptions.add(ex);
915 }
916
917
918
919
920
921
922 protected void setLocationWithinModule(final String locationWithinModule) {
923 getCurrentContext().setLocationWithinModule(locationWithinModule);
924 }
925
926
927
928
929
930
931 protected final ModuleContext getCurrentContext() {
932 return currentContext;
933 }
934
935
936 }