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.io.VersionSet;
23 import org.qedeq.base.utility.Enumerator;
24 import org.qedeq.base.utility.EqualsUtility;
25 import org.qedeq.base.utility.StringUtility;
26 import org.qedeq.kernel.bo.logic.common.FormulaChecker;
27 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
28 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
29 import org.qedeq.kernel.bo.logic.common.Operators;
30 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
31 import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
32 import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
33 import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
34 import org.qedeq.kernel.se.base.list.Element;
35 import org.qedeq.kernel.se.base.list.ElementList;
36 import org.qedeq.kernel.se.base.module.Add;
37 import org.qedeq.kernel.se.base.module.ConditionalProof;
38 import org.qedeq.kernel.se.base.module.Existential;
39 import org.qedeq.kernel.se.base.module.FormalProofLine;
40 import org.qedeq.kernel.se.base.module.FormalProofLineList;
41 import org.qedeq.kernel.se.base.module.ModusPonens;
42 import org.qedeq.kernel.se.base.module.Reason;
43 import org.qedeq.kernel.se.base.module.Rename;
44 import org.qedeq.kernel.se.base.module.Rule;
45 import org.qedeq.kernel.se.base.module.SubstFree;
46 import org.qedeq.kernel.se.base.module.SubstFunc;
47 import org.qedeq.kernel.se.base.module.SubstPred;
48 import org.qedeq.kernel.se.base.module.Universal;
49 import org.qedeq.kernel.se.common.ModuleAddress;
50 import org.qedeq.kernel.se.common.ModuleContext;
51 import org.qedeq.kernel.se.common.RuleKey;
52 import org.qedeq.kernel.se.dto.list.DefaultElementList;
53 import org.qedeq.kernel.se.dto.list.ElementSet;
54
55
56
57
58
59
60
61 public class ProofChecker2Impl implements ProofChecker, ReferenceResolver {
62
63
64 private FormalProofLineList proof;
65
66
67 private ModuleContext moduleContext;
68
69
70 private ModuleContext currentContext;
71
72
73 private ReferenceResolver resolver;
74
75
76 private LogicalCheckExceptionList exceptions;
77
78
79 private boolean[] lineProved;
80
81
82 private Map label2line;
83
84
85 private final VersionSet supported;
86
87
88 private ElementList conditions;
89
90
91 private RuleChecker checker;
92
93
94
95
96 public ProofChecker2Impl() {
97 supported = new VersionSet();
98 supported.add("0.01.00");
99 supported.add("0.02.00");
100 }
101
102 public LogicalCheckExceptionList checkRule(final Rule rule,
103 final ModuleContext context, final RuleChecker checker,
104 final ReferenceResolver resolver) {
105 exceptions = new LogicalCheckExceptionList();
106 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
107 if (rule.getVersion() == null || !supported.contains(rule.getVersion())) {
108 final ProofCheckException ex = new ProofCheckException(
109 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
110 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey
111 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
112 context);
113 exceptions.add(ex);
114 }
115 return exceptions;
116 }
117
118 public LogicalCheckExceptionList checkProof(final Element formula,
119 final FormalProofLineList proof,
120 final RuleChecker checker,
121 final ModuleContext moduleContext,
122 final ReferenceResolver resolver) {
123 final DefaultElementList con = new DefaultElementList(
124 Operators.CONJUNCTION_OPERATOR);
125
126 return checkProof(con, formula, proof, checker, moduleContext, resolver);
127 }
128
129 private LogicalCheckExceptionList checkProof(final ElementList conditions, final Element formula,
130 final FormalProofLineList proof,
131 final RuleChecker checker,
132 final ModuleContext moduleContext,
133 final ReferenceResolver resolver) {
134 this.conditions = conditions;
135 this.proof = proof;
136 this.checker = checker;
137 this.resolver = resolver;
138 this.moduleContext = moduleContext;
139
140 currentContext = new ModuleContext(moduleContext);
141 exceptions = new LogicalCheckExceptionList();
142 final String context = moduleContext.getLocationWithinModule();
143 lineProved = new boolean[proof.size()];
144 label2line = new HashMap();
145 for (int i = 0; i < proof.size(); i++) {
146 boolean ok = true;
147 setLocationWithinModule(context + ".get(" + i + ")");
148 final FormalProofLine line = proof.get(i);
149 if (line == null || line.getFormula() == null
150 || line.getFormula().getElement() == null) {
151 ok = false;
152 handleProofCheckException(
153 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
154 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
155 getCurrentContext());
156 continue;
157 }
158 setLocationWithinModule(context + ".get(" + i + ").getReason()");
159 final Reason reason = line.getReason();
160 if (reason == null) {
161 ok = false;
162 handleProofCheckException(
163 BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
164 BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
165 getCurrentContext());
166 continue;
167 }
168 if (line.getLabel() != null && line.getLabel().length() > 0) {
169 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
170 addLocalLineLabel(i, line.getLabel());
171 }
172
173
174 if (hasConditions()) {
175 setLocationWithinModule(context + ".get(" + i + ").getFormula.getElement()");
176 ElementList full = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
177 if (conditions.size() > 1) {
178 full.add(conditions);
179 } else {
180 full.add(conditions.getElement(0));
181 }
182 full.add(line.getFormula().getElement());
183 FormulaChecker checkWf = new FormulaCheckerImpl();
184 final LogicalCheckExceptionList list = checkWf.checkFormula(full, getCurrentContext());
185 if (list.size() > 0) {
186 ok = false;
187 handleProofCheckException(
188 BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_CODE,
189 BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT
190 + list.get(0).getMessage(),
191 getCurrentContext());
192 continue;
193 }
194 }
195
196
197
198
199 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
200 if (getReason.endsWith("Vo")) {
201 getReason = getReason.substring(0, getReason.length() - 2) + "()";
202 setLocationWithinModule(context + ".get(" + i + ").getReason()"
203 + getReason);
204
205 }
206 if (reason instanceof Add) {
207 ok = check((Add) reason, i, line.getFormula().getElement());
208 } else if (reason instanceof Rename) {
209 ok = check((Rename) reason, i, line.getFormula().getElement());
210 } else if (reason instanceof ModusPonens) {
211 ok = check((ModusPonens) reason, i, line.getFormula().getElement());
212 } else if (reason instanceof SubstFree) {
213 ok = check((SubstFree) reason, i, line.getFormula().getElement());
214 } else if (reason instanceof SubstPred) {
215 ok = check((SubstPred) reason, i, line.getFormula().getElement());
216 } else if (reason instanceof SubstFunc) {
217 ok = check((SubstFunc) reason, i, line.getFormula().getElement());
218 } else if (reason instanceof Universal) {
219 ok = check((Universal) reason, i, line.getFormula().getElement());
220 } else if (reason instanceof Existential) {
221 ok = check((Existential) reason, i, line.getFormula().getElement());
222 } else if (reason instanceof ConditionalProof) {
223 setLocationWithinModule(context + ".get(" + i + ")");
224 ok = check((ConditionalProof) reason, i, line.getFormula().getElement());
225 } else {
226 ok = false;
227 handleProofCheckException(
228 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
229 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
230 + reason.getName(),
231 getCurrentContext());
232 }
233 lineProved[i] = ok;
234
235 if (i == proof.size() - 1) {
236 if (!formula.equals(line.getFormula().getElement())) {
237 handleProofCheckException(
238 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
239 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT,
240 getModuleContextOfProofLineFormula(i));
241 }
242 }
243 }
244 return exceptions;
245 }
246
247 private void addLocalLineLabel(final int i, final String label) {
248 if (label != null && label.length() > 0) {
249 final Integer n = (Integer) label2line.get(label);
250 if (n != null) {
251 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
252 moduleContext.getLocationWithinModule() + ".get("
253 + label2line.get(label)
254 + ").getLabel()");
255 handleProofCheckException(
256 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
257 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
258 + label,
259 getCurrentContext(),
260 lc);
261 } else {
262 if (isLocalProofLineReference(label)) {
263 handleProofCheckException(
264 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
265 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
266 + label,
267 getCurrentContext(),
268 resolver.getReferenceContext(label));
269
270
271 }
272 }
273
274 label2line.put(label, new Integer(i));
275 }
276 }
277
278 private boolean check(final Add add, final int i, final Element element) {
279 final String context = currentContext.getLocationWithinModule();
280 boolean ok = true;
281 if (add.getReference() == null) {
282 ok = false;
283 setLocationWithinModule(context + ".getReference()");
284 handleProofCheckException(
285 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
286 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
287 getCurrentContext());
288 return ok;
289 }
290 if (!resolver.isProvedFormula(add.getReference())) {
291 ok = false;
292 setLocationWithinModule(context + ".getReference()");
293 handleProofCheckException(
294 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
295 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
296 + add.getReference(),
297 getCurrentContext());
298 return ok;
299 }
300 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
301 final Element current = resolver.getNormalizedFormula(element);
302 if (!EqualsUtility.equals(expected, current)) {
303 ok = false;
304 handleProofCheckException(
305 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
306 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
307 + add.getReference(),
308 getDiffModuleContextOfProofLineFormula(i, expected));
309 return ok;
310 }
311 final RuleKey defined = checker.getRule(add.getName());
312 if (defined == null) {
313 ok = false;
314 handleProofCheckException(
315 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
316 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
317 + add.getName(),
318 getCurrentContext());
319 return ok;
320 } else if (!supported.contains(defined.getVersion())) {
321 ok = false;
322 handleProofCheckException(
323 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
324 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
325 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
326 getCurrentContext());
327 return ok;
328 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
329 ok = false;
330 handleProofCheckException(
331 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
332 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
333 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
334 getCurrentContext());
335 return ok;
336 }
337 return ok;
338 }
339
340 private boolean check(final Rename rename, final int i, final Element element) {
341 final String context = currentContext.getLocationWithinModule();
342 boolean ok = true;
343 final Element f = getNormalizedLocalProofLineReference(rename.getReference());
344 if (f == null) {
345 ok = false;
346 setLocationWithinModule(context + ".getReference()");
347 handleProofCheckException(
348 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
349 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
350 + rename.getReference(),
351 getCurrentContext());
352 } else {
353 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
354 rename.getOriginalSubjectVariable(),
355 rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
356 new Enumerator());
357 final Element current = resolver.getNormalizedFormula(element);
358 if (!EqualsUtility.equals(expected, current)) {
359 ok = false;
360 handleProofCheckException(
361 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
362 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
363 + rename.getReference(),
364 getDiffModuleContextOfProofLineFormula(i, expected));
365 } else {
366 ok = true;
367 }
368 }
369 final RuleKey defined = checker.getRule(rename.getName());
370 if (defined == null) {
371 ok = false;
372 handleProofCheckException(
373 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
374 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
375 + rename.getName(),
376 getCurrentContext());
377 return ok;
378 } else if (!supported.contains(defined.getVersion())) {
379 ok = false;
380 handleProofCheckException(
381 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
382 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
383 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
384 getCurrentContext());
385 return ok;
386 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
387 ok = false;
388 handleProofCheckException(
389 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
390 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
391 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
392 getCurrentContext());
393 return ok;
394 }
395 return ok;
396 }
397
398 private boolean check(final SubstFree substFree, final int i, final Element element) {
399 final String context = currentContext.getLocationWithinModule();
400 boolean ok = true;
401 final Element f = getNormalizedLocalProofLineReference(substFree.getReference());
402 if (f == null) {
403 ok = false;
404 setLocationWithinModule(context + ".getReference()");
405 handleProofCheckException(
406 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
407 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
408 + substFree.getReference(),
409 getCurrentContext());
410 } else {
411 final Element current = resolver.getNormalizedFormula(element);
412 final Element expected = f.replace(substFree.getSubjectVariable(),
413 resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
414 if (!EqualsUtility.equals(current, expected)) {
415 ok = false;
416 handleProofCheckException(
417 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
418 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
419 + substFree.getReference(),
420 getDiffModuleContextOfProofLineFormula(i, expected));
421 return ok;
422 }
423 }
424
425 if (FormulaUtility.containsOperatorVariable(conditions, substFree.getSubjectVariable())) {
426 ok = false;
427 setLocationWithinModule(context + ".getSubstituteFormula()");
428 handleProofCheckException(
429 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
430 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
431 getCurrentContext());
432 return ok;
433 }
434 final RuleKey defined = checker.getRule(substFree.getName());
435 if (defined == null) {
436 ok = false;
437 handleProofCheckException(
438 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
439 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
440 + substFree.getName(),
441 getCurrentContext());
442 return ok;
443 } else if (!supported.contains(defined.getVersion())) {
444 ok = false;
445 handleProofCheckException(
446 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
447 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
448 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
449 getCurrentContext());
450 return ok;
451 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
452 ok = false;
453 handleProofCheckException(
454 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
455 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
456 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
457 getCurrentContext());
458 return ok;
459 }
460 return ok;
461 }
462
463 private boolean check(final SubstPred substPred, final int i, final Element element) {
464 final String context = currentContext.getLocationWithinModule();
465 boolean ok = true;
466 final Element alpha = getNormalizedLocalProofLineReference(substPred.getReference());
467 if (alpha == null) {
468 ok = false;
469 setLocationWithinModule(context + ".getReference()");
470 handleProofCheckException(
471 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
472 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
473 + substPred.getReference(),
474 getCurrentContext());
475 return ok;
476 }
477 final Element current = resolver.getNormalizedFormula(element);
478 if (substPred.getSubstituteFormula() == null) {
479 ok = false;
480 handleProofCheckException(
481 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
482 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
483 getCurrentContext());
484 return ok;
485 }
486 final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
487 final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
488 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
489 if (!EqualsUtility.equals(current, expected)) {
490 ok = false;
491 handleProofCheckException(
492 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
493 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
494 + substPred.getReference(),
495 getDiffModuleContextOfProofLineFormula(i, expected));
496 return ok;
497 }
498
499
500 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
501 if (predFree.size() != p.getList().size() - 1) {
502 ok = false;
503 setLocationWithinModule(context + ".getPredicateVariable()");
504 handleProofCheckException(
505 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
506 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
507 getDiffModuleContextOfProofLineFormula(i, expected));
508 return ok;
509 }
510 for (int j = 1; j < p.getList().size(); j++) {
511 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
512 ok = false;
513 setLocationWithinModule(context + ".getPredicateVariable()");
514 handleProofCheckException(
515 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
516 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
517 getCurrentContext());
518 return ok;
519 }
520 }
521
522
523 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
524 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
525 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
526 ok = false;
527 setLocationWithinModule(context + ".getSubstituteFormula()");
528 handleProofCheckException(
529 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
530 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
531 getCurrentContext());
532 return ok;
533 }
534
535
536 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
537 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
538 ok = false;
539 setLocationWithinModule(context + ".getSubstituteFormula()");
540 handleProofCheckException(
541 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
542 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
543 getCurrentContext());
544 return ok;
545 }
546
547 if (FormulaUtility.containsOperatorVariable(conditions, p)) {
548 ok = false;
549 setLocationWithinModule(context + ".getPredicateVariable()");
550 handleProofCheckException(
551 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
552 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
553 getCurrentContext());
554 return ok;
555 }
556
557
558
559 final RuleKey defined = checker.getRule(substPred.getName());
560 if (defined == null) {
561 ok = false;
562 handleProofCheckException(
563 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
564 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
565 + substPred.getName(),
566 getCurrentContext());
567 return ok;
568 } else if (!supported.contains(defined.getVersion())) {
569 ok = false;
570 handleProofCheckException(
571 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
572 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
573 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
574 getCurrentContext());
575 return ok;
576 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
577 ok = false;
578 handleProofCheckException(
579 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
580 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
581 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
582 getCurrentContext());
583 return ok;
584 }
585 return ok;
586 }
587
588 private boolean check(final SubstFunc substFunc, final int i, final Element element) {
589 final String context = currentContext.getLocationWithinModule();
590 boolean ok = true;
591 final Element alpha = getNormalizedLocalProofLineReference(substFunc.getReference());
592 if (alpha == null) {
593 ok = false;
594 setLocationWithinModule(context + ".getReference()");
595 handleProofCheckException(
596 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
597 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
598 + substFunc.getReference(),
599 getCurrentContext());
600 return ok;
601 }
602 final Element current = resolver.getNormalizedFormula(element);
603 if (substFunc.getSubstituteTerm() == null) {
604 ok = false;
605 handleProofCheckException(
606 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
607 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
608 getCurrentContext());
609 return ok;
610 }
611 final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
612 final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
613 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
614 if (!EqualsUtility.equals(current, expected)) {
615 ok = false;
616 handleProofCheckException(
617 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
618 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
619 + substFunc.getReference(),
620 getDiffModuleContextOfProofLineFormula(i, expected));
621 return ok;
622 }
623
624
625 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
626 if (funcFree.size() != sigma.getList().size() - 1) {
627 ok = false;
628 setLocationWithinModule(context + ".getPredicateVariable()");
629 handleProofCheckException(
630 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
631 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
632 getDiffModuleContextOfProofLineFormula(i, expected));
633 return ok;
634 }
635 for (int j = 1; j < sigma.getList().size(); j++) {
636 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
637 ok = false;
638 setLocationWithinModule(context + ".getPredicateVariable()");
639 handleProofCheckException(
640 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
641 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
642 getCurrentContext());
643 return ok;
644 }
645 }
646
647
648 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
649 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
650 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
651 ok = false;
652 setLocationWithinModule(context + ".getSubstituteFormula()");
653 handleProofCheckException(
654 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
655 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
656 getCurrentContext());
657 return ok;
658 }
659
660
661 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
662 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
663 ok = false;
664 setLocationWithinModule(context + ".getSubstituteFormula()");
665 handleProofCheckException(
666 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
667 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
668 getCurrentContext());
669 return ok;
670 }
671
672 if (FormulaUtility.containsOperatorVariable(conditions, sigma)) {
673 ok = false;
674 setLocationWithinModule(context + ".getPredicateVariable()");
675 handleProofCheckException(
676 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
677 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
678 getCurrentContext());
679 return ok;
680 }
681
682
683
684 final RuleKey defined = checker.getRule(substFunc.getName());
685 if (defined == null) {
686 ok = false;
687 handleProofCheckException(
688 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
689 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
690 + substFunc.getName(),
691 getCurrentContext());
692 return ok;
693 } else if (!supported.contains(defined.getVersion())) {
694 ok = false;
695 handleProofCheckException(
696 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
697 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
698 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
699 getCurrentContext());
700 return ok;
701 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
702 ok = false;
703 handleProofCheckException(
704 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
705 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
706 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
707 getCurrentContext());
708 return ok;
709 }
710 return ok;
711 }
712
713 private boolean check(final ModusPonens mp, final int i, final Element element) {
714 final String context = currentContext.getLocationWithinModule();
715 boolean ok = true;
716 final Element f1 = getNormalizedLocalProofLineReference(mp.getReference1());
717 if (f1 == null) {
718 ok = false;
719 setLocationWithinModule(context + ".getReference1()");
720 handleProofCheckException(
721 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
722 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
723 + mp.getReference1(),
724 getCurrentContext());
725 }
726 final Element f2 = getNormalizedLocalProofLineReference(mp.getReference2());
727 if (f2 == null) {
728 ok = false;
729 setLocationWithinModule(context + ".getReference2()");
730 handleProofCheckException(
731 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
732 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
733 + mp.getReference2(),
734 getCurrentContext());
735 }
736 if (ok) {
737 final Element current = getNormalizedFormula(element);
738 if (!FormulaUtility.isImplication(f1)) {
739 ok = false;
740 setLocationWithinModule(context + ".getReference1()");
741 handleProofCheckException(
742 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
743 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
744 + mp.getReference1(),
745 getCurrentContext());
746 } else if (!f2.equals(f1.getList().getElement(0))) {
747 ok = false;
748 setLocationWithinModule(context + ".getReference2()");
749 handleProofCheckException(
750 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
751 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
752 + mp.getReference2(),
753 getCurrentContext(),
754 resolver.getReferenceContext(mp.getReference1()));
755 } else if (!current.equals(f1.getList().getElement(1))) {
756 ok = false;
757 setLocationWithinModule(context + ".getReference1()");
758 handleProofCheckException(
759 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
760 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
761 + mp.getReference1(),
762 getCurrentContext(),
763 resolver.getReferenceContext(mp.getReference1()));
764 } else {
765 ok = true;
766 }
767 }
768 final RuleKey defined = checker.getRule(mp.getName());
769 if (defined == null) {
770 ok = false;
771 handleProofCheckException(
772 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
773 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
774 + mp.getName(),
775 getCurrentContext());
776 return ok;
777 } else if (!supported.contains(defined.getVersion())) {
778 ok = false;
779 handleProofCheckException(
780 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
781 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
782 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
783 getCurrentContext());
784 return ok;
785 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
786 ok = false;
787 handleProofCheckException(
788 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
789 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
790 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
791 getCurrentContext());
792 return ok;
793 }
794 return ok;
795 }
796
797 private boolean check(final Universal universal, final int i, final Element element) {
798 final String context = currentContext.getLocationWithinModule();
799 boolean ok = true;
800 final Element reference = getNormalizedLocalProofLineReference(universal.getReference());
801 if (reference == null) {
802 ok = false;
803 setLocationWithinModule(context + ".getReference()");
804 handleProofCheckException(
805 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
806 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
807 + universal.getReference(),
808 getCurrentContext());
809
810
811
812
813
814
815
816
817 } else {
818 final Element current = getNormalizedFormula(element);
819 if (!FormulaUtility.isImplication(current)) {
820 ok = false;
821 setLocationWithinModule(context + ".getReference()");
822 handleProofCheckException(
823 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
824 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
825 + universal.getReference(),
826 getCurrentContext());
827 return ok;
828 }
829 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
830 ok = false;
831 setLocationWithinModule(context + ".getSubjectVariable()");
832 handleProofCheckException(
833 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
834 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
835 getCurrentContext());
836 return ok;
837 }
838 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
839 expected.add(reference.getList().getElement(0));
840 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
841 uni.add(universal.getSubjectVariable());
842 uni.add(reference.getList().getElement(1));
843 expected.add(uni);
844
845
846
847
848 if (!EqualsUtility.equals(current, expected)) {
849 ok = false;
850 handleProofCheckException(
851 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
852 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
853 + universal.getReference(),
854 getDiffModuleContextOfProofLineFormula(i, expected));
855 return ok;
856 }
857 }
858 final RuleKey defined = checker.getRule(universal.getName());
859 if (defined == null) {
860 ok = false;
861 handleProofCheckException(
862 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
863 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
864 + universal.getName(),
865 getCurrentContext());
866 return ok;
867 } else if (!supported.contains(defined.getVersion())) {
868 ok = false;
869 handleProofCheckException(
870 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
871 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
872 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
873 getCurrentContext());
874 return ok;
875 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
876 ok = false;
877 handleProofCheckException(
878 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
879 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
880 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
881 getCurrentContext());
882 return ok;
883 }
884 return ok;
885 }
886
887 private boolean check(final Existential existential, final int i, final Element element) {
888 final String context = currentContext.getLocationWithinModule();
889 boolean ok = true;
890 final Element reference = getNormalizedLocalProofLineReference(existential.getReference());
891 if (reference == null) {
892 ok = false;
893 setLocationWithinModule(context + ".getReference()");
894 handleProofCheckException(
895 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
896 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
897 + existential.getReference(),
898 getCurrentContext());
899
900
901
902
903
904
905
906
907 } else {
908 final Element current = getNormalizedFormula(element);
909 if (!FormulaUtility.isImplication(current)) {
910 ok = false;
911 setLocationWithinModule(context + ".getReference()");
912 handleProofCheckException(
913 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
914 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
915 + existential.getReference(),
916 getCurrentContext());
917 return ok;
918 }
919 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
920 ok = false;
921 setLocationWithinModule(context + ".getSubjectVariable()");
922 handleProofCheckException(
923 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
924 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
925 getCurrentContext());
926 return ok;
927 }
928 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
929 final ElementList exi = new DefaultElementList(
930 Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
931 exi.add(existential.getSubjectVariable());
932 exi.add(reference.getList().getElement(0));
933 expected.add(exi);
934 expected.add((reference.getList().getElement(1)));
935 if (!EqualsUtility.equals(current, expected)) {
936 ok = false;
937 handleProofCheckException(
938 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
939 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
940 + existential.getReference(),
941 getDiffModuleContextOfProofLineFormula(i, expected));
942 return ok;
943 }
944 }
945 final RuleKey defined = checker.getRule(existential.getName());
946 if (defined == null) {
947 ok = false;
948 handleProofCheckException(
949 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
950 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
951 + existential.getName(),
952 getCurrentContext());
953 return ok;
954 } else if (!supported.contains(defined.getVersion())) {
955 ok = false;
956 handleProofCheckException(
957 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
958 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
959 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
960 getCurrentContext());
961 return ok;
962 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
963 ok = false;
964 handleProofCheckException(
965 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
966 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
967 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
968 getCurrentContext());
969 return ok;
970 }
971 return ok;
972 }
973
974 private boolean check(final ConditionalProof cp, final int i, final Element element) {
975 final ModuleAddress address = currentContext.getModuleLocation();
976 final String context = currentContext.getLocationWithinModule();
977
978 boolean ok = true;
979 if (cp.getHypothesis() == null || cp.getHypothesis().getFormula() == null
980 || cp.getHypothesis().getFormula().getElement() == null) {
981 ok = false;
982 setLocationWithinModule(context + ".getHypothesis()");
983 handleProofCheckException(
984 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
985 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
986 getCurrentContext());
987 return ok;
988 }
989 if (cp.getFormalProofLineList() == null || cp.getFormalProofLineList().size() <= 0) {
990 ok = false;
991 setLocationWithinModule(context + ".getFormalProofLineList()");
992 handleProofCheckException(
993 BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE,
994 BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT,
995 getCurrentContext());
996 return ok;
997 }
998 final ReferenceResolver newResolver = new ReferenceResolver() {
999
1000 public Element getNormalizedFormula(final Element formula) {
1001 return ProofChecker2Impl.this.getNormalizedFormula(formula);
1002 }
1003
1004 public Element getNormalizedReferenceFormula(final String reference) {
1005
1006 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1007 return resolver.getNormalizedFormula(cp.getHypothesis().getFormula()
1008 .getElement());
1009 }
1010 return ProofChecker2Impl.this.getNormalizedReferenceFormula(reference);
1011 }
1012
1013 public boolean isProvedFormula(final String reference) {
1014 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1015 return true;
1016 }
1017 return ProofChecker2Impl.this.isProvedFormula(reference);
1018 }
1019
1020 public boolean isLocalProofLineReference(final String reference) {
1021 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1022 return true;
1023 }
1024 return ProofChecker2Impl.this.isLocalProofLineReference(reference);
1025 }
1026
1027 public ModuleContext getReferenceContext(final String reference) {
1028 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1029 return new ModuleContext(address, context
1030 + ".getHypothesis().getLabel()");
1031 }
1032 return ProofChecker2Impl.this.getReferenceContext(reference);
1033 }
1034
1035 public Element getNormalizedLocalProofLineReference(final String reference) {
1036
1037 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1038
1039 return resolver.getNormalizedFormula(
1040 cp.getHypothesis().getFormula().getElement());
1041 }
1042 return ProofChecker2Impl.this.getNormalizedLocalProofLineReference(reference);
1043 }
1044
1045 };
1046 final int last = cp.getFormalProofLineList().size() - 1;
1047 setLocationWithinModule(context + ".getFormalProofLineList().get(" + last + ")");
1048 final FormalProofLine line = cp.getFormalProofLineList().get(last);
1049 if (line == null || line.getFormula() == null
1050 || line.getFormula().getElement() == null) {
1051 ok = false;
1052 handleProofCheckException(
1053 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1054 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1055 getCurrentContext());
1056 return ok;
1057 }
1058 final Element lastFormula = resolver.getNormalizedFormula(line.getFormula().getElement());
1059 final ElementList newConditions = (ElementList) conditions.copy();
1060
1061 newConditions.add(cp.getHypothesis().getFormula().getElement());
1062 setLocationWithinModule(context + ".getFormalProofLineList()");
1063 final LogicalCheckExceptionList eList = (new ProofChecker2Impl()).checkProof(
1064 newConditions, lastFormula, cp.getFormalProofLineList(), checker, getCurrentContext(),
1065 newResolver);
1066 exceptions.add(eList);
1067 ok = eList.size() == 0;
1068 setLocationWithinModule(context + ".getConclusion()");
1069 if (cp.getConclusion() == null || cp.getConclusion().getFormula() == null
1070 || cp.getConclusion().getFormula().getElement() == null) {
1071 ok = false;
1072 handleProofCheckException(
1073 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1074 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1075 getCurrentContext());
1076 return ok;
1077 }
1078 final Element c = resolver.getNormalizedFormula(cp.getConclusion().getFormula().getElement());
1079 setLocationWithinModule(context + ".getConclusion().getFormula().getElement()");
1080 if (!FormulaUtility.isImplication(c)) {
1081 ok = false;
1082 handleProofCheckException(
1083 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
1084 BasicProofErrors.IMPLICATION_EXPECTED_TEXT,
1085 getCurrentContext());
1086 return ok;
1087 }
1088 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
1089 expected.add(cp.getHypothesis().getFormula().getElement());
1090 expected.add(lastFormula);
1091
1092
1093 if (!EqualsUtility.equals(cp.getConclusion().getFormula().getElement(), expected)) {
1094
1095
1096 ok = false;
1097 handleProofCheckException(
1098 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_CODE,
1099 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_TEXT,
1100 getDiffModuleContextOfProofLineFormula(i, expected));
1101 return ok;
1102 }
1103 final RuleKey defined = checker.getRule(cp.getName());
1104 if (defined == null) {
1105 ok = false;
1106 handleProofCheckException(
1107 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
1108 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
1109 + cp.getName(),
1110 getCurrentContext());
1111 return ok;
1112 } else if (!supported.contains(defined.getVersion())) {
1113 ok = false;
1114 handleProofCheckException(
1115 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
1116 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
1117 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
1118 getCurrentContext());
1119 return ok;
1120 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
1121 ok = false;
1122 handleProofCheckException(
1123 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
1124 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
1125 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
1126 getCurrentContext());
1127 return ok;
1128 }
1129 return ok;
1130 }
1131
1132 private ModuleContext getModuleContextOfProofLineFormula(final int i) {
1133 if (proof.get(i) instanceof ConditionalProof) {
1134 return new ModuleContext(moduleContext.getModuleLocation(),
1135 moduleContext.getLocationWithinModule() + ".get(" + i
1136 + ").getConclusion().getFormula().getElement()");
1137 }
1138 return new ModuleContext(moduleContext.getModuleLocation(),
1139 moduleContext.getLocationWithinModule() + ".get(" + i
1140 + ").getFormula().getElement()");
1141 }
1142
1143 private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
1144 final Element expected) {
1145 final String diff = FormulaUtility.getDifferenceLocation(
1146 proof.get(i).getFormula().getElement(), expected);
1147 if (proof.get(i) instanceof ConditionalProof) {
1148 return new ModuleContext(moduleContext.getModuleLocation(),
1149 moduleContext.getLocationWithinModule() + ".get(" + i
1150 + ").getConclusion().getFormula().getElement()" + diff);
1151 }
1152 return new ModuleContext(moduleContext.getModuleLocation(),
1153 moduleContext.getLocationWithinModule() + ".get(" + i
1154 + ").getFormula().getElement()" + diff);
1155 }
1156
1157
1158
1159
1160
1161
1162 private boolean hasConditions() {
1163 return conditions.size() > 0;
1164 }
1165
1166 private Element getNormalizedProofLine(final Integer n) {
1167 if (n == null) {
1168 return null;
1169 }
1170 int i = n.intValue();
1171 if (i < 0 || i >= proof.size()) {
1172 return null;
1173 }
1174 return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
1175 }
1176
1177
1178
1179
1180
1181
1182
1183
1184 private void handleProofCheckException(final int code, final String msg,
1185 final ModuleContext context) {
1186
1187
1188 final ProofCheckException ex = new ProofCheckException(code, msg, context);
1189 exceptions.add(ex);
1190 }
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200 private void handleProofCheckException(final int code, final String msg,
1201 final ModuleContext context, final ModuleContext referenceContext) {
1202
1203
1204 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
1205 referenceContext);
1206 exceptions.add(ex);
1207 }
1208
1209
1210
1211
1212
1213
1214 protected final ModuleContext getCurrentContext() {
1215 return currentContext;
1216 }
1217
1218
1219
1220
1221
1222
1223 protected void setLocationWithinModule(final String locationWithinModule) {
1224 getCurrentContext().setLocationWithinModule(locationWithinModule);
1225 }
1226
1227 public boolean isProvedFormula(final String reference) {
1228 if (label2line.containsKey(reference)) {
1229 return lineProved[((Integer) label2line.get(reference)).intValue()];
1230 }
1231 return resolver.isProvedFormula(reference);
1232 }
1233
1234 public Element getNormalizedReferenceFormula(final String reference) {
1235
1236 if (label2line.containsKey(reference)) {
1237
1238 return getNormalizedProofLine((Integer) label2line.get(reference));
1239 }
1240
1241 return resolver.getNormalizedReferenceFormula(reference);
1242 }
1243
1244 public Element getNormalizedFormula(final Element element) {
1245 return resolver.getNormalizedFormula(element);
1246 }
1247
1248 public boolean isLocalProofLineReference(final String reference) {
1249 if (label2line.containsKey(reference)) {
1250 return true;
1251 }
1252 return resolver.isLocalProofLineReference(reference);
1253 }
1254
1255 public Element getNormalizedLocalProofLineReference(final String reference) {
1256
1257 if (label2line.containsKey(reference)) {
1258
1259 return getNormalizedProofLine((Integer) label2line.get(reference));
1260 }
1261
1262 final Element result = resolver.getNormalizedLocalProofLineReference(reference);
1263
1264
1265
1266
1267
1268 return result;
1269 }
1270
1271 public ModuleContext getReferenceContext(final String reference) {
1272 if (label2line.containsKey(reference)) {
1273 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
1274 moduleContext.getLocationWithinModule() + ".get("
1275 + label2line.get(reference)
1276 + ").getLabel()");
1277 return lc;
1278 }
1279 return resolver.getReferenceContext(reference);
1280 }
1281
1282 }