001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.proof.basic;
017
018 import java.util.HashMap;
019 import java.util.Map;
020
021 import org.qedeq.base.utility.Enumerator;
022 import org.qedeq.base.utility.EqualsUtility;
023 import org.qedeq.base.utility.StringUtility;
024 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
025 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
026 import org.qedeq.kernel.bo.logic.common.Operators;
027 import org.qedeq.kernel.bo.logic.common.ProofChecker;
028 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
029 import org.qedeq.kernel.se.base.list.Element;
030 import org.qedeq.kernel.se.base.list.ElementList;
031 import org.qedeq.kernel.se.base.module.Add;
032 import org.qedeq.kernel.se.base.module.Existential;
033 import org.qedeq.kernel.se.base.module.FormalProofLine;
034 import org.qedeq.kernel.se.base.module.FormalProofLineList;
035 import org.qedeq.kernel.se.base.module.ModusPonens;
036 import org.qedeq.kernel.se.base.module.Reason;
037 import org.qedeq.kernel.se.base.module.ReasonType;
038 import org.qedeq.kernel.se.base.module.Rename;
039 import org.qedeq.kernel.se.base.module.SubstFree;
040 import org.qedeq.kernel.se.base.module.SubstFunc;
041 import org.qedeq.kernel.se.base.module.SubstPred;
042 import org.qedeq.kernel.se.base.module.Universal;
043 import org.qedeq.kernel.se.common.ModuleContext;
044 import org.qedeq.kernel.se.dto.list.DefaultElementList;
045 import org.qedeq.kernel.se.dto.list.ElementSet;
046
047
048 /**
049 * Formal proof checker for basic rules.
050 *
051 * @author Michael Meyling
052 */
053 public class ProofCheckerImpl implements ProofChecker {
054
055 /** Proof we want to check. */
056 private FormalProofLineList proof;
057
058 /** Module context of proof line list. */
059 private ModuleContext moduleContext;
060
061 /** Current context. */
062 private ModuleContext currentContext;
063
064 /** Resolver for external references. */
065 private ReferenceResolver resolver;
066
067 /** All exceptions that occurred during checking. */
068 private LogicalCheckExceptionList exceptions;
069
070 /** Array with proof status for each proof line. */
071 private boolean[] lineProved;
072
073 /** Maps local proof line labels to local line number Integers. */
074 private Map label2line;
075
076 /**
077 * Constructor.
078 *
079 */
080 public ProofCheckerImpl() {
081 }
082
083 public LogicalCheckExceptionList checkProof(final Element formula,
084 final FormalProofLineList proof, final ModuleContext moduleContext,
085 final ReferenceResolver resolver) {
086 this.proof = proof;
087 this.resolver = resolver;
088 this.moduleContext = moduleContext;
089 // use copy constructor for changing context
090 currentContext = new ModuleContext(moduleContext);
091 exceptions = new LogicalCheckExceptionList();
092 final String context = moduleContext.getLocationWithinModule();
093 lineProved = new boolean[proof.size()];
094 label2line = new HashMap();
095 for (int i = 0; i < proof.size(); i++) {
096 boolean ok = true;
097 setLocationWithinModule(context + ".get(" + i + ")");
098 final FormalProofLine line = proof.get(i);
099 if (line == null) {
100 ok = false;
101 handleProofCheckException(
102 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
103 BasicProofErrors.ELEMENT_MUST_NOT_BE_NULL_TEXT,
104 getCurrentContext());
105 continue;
106 }
107 setLocationWithinModule(context + ".get(" + i + ").getReasonType()");
108 final ReasonType reasonType = line.getReasonType();
109 if (reasonType == null) {
110 ok = false;
111 handleProofCheckException(
112 BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
113 BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
114 getCurrentContext());
115 continue;
116 }
117 final Reason reason = reasonType.getReason();
118 if (reason == null) {
119 ok = false;
120 handleProofCheckException(
121 BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
122 BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
123 getCurrentContext());
124 continue;
125 }
126 if (line.getLabel() != null && line.getLabel().length() > 0) {
127 final Integer n = (Integer) label2line.get(line.getLabel());
128 if (n != null) {
129 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
130 moduleContext.getLocationWithinModule() + ".get("
131 + ((Integer) label2line.get(line.getLabel()))
132 + ").getLabel()");
133 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
134 handleProofCheckException(
135 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
136 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
137 + line.getLabel(),
138 getCurrentContext(),
139 lc);
140 }
141 label2line.put(line.getLabel(), new Integer(i));
142 }
143 // check if only basis rules are used
144 // TODO 20110316 m31: this is a dirty trick to get the context of the reason
145 // perhaps we can solve this more elegantly?
146 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
147 if (getReason.endsWith("Vo")) {
148 getReason = getReason.substring(0, getReason.length() - 2) + "()";
149 setLocationWithinModule(context + ".get(" + i + ").getReasonType()"
150 + getReason);
151 }
152 if (reason instanceof Add) {
153 ok = check(reasonType.getAdd(), i, line.getFormula().getElement());
154 } else if (reason instanceof Rename) {
155 ok = check(reasonType.getRename(), i, line.getFormula().getElement());
156 } else if (reason instanceof ModusPonens) {
157 ok = check(reasonType.getModusPonens(), i, line.getFormula().getElement());
158 } else if (reason instanceof SubstFree) {
159 ok = check(reasonType.getSubstFree(), i, line.getFormula().getElement());
160 } else if (reason instanceof SubstPred) {
161 ok = check(reasonType.getSubstPred(), i, line.getFormula().getElement());
162 } else if (reason instanceof SubstFunc) {
163 ok = check(reasonType.getSubstFunc(), i, line.getFormula().getElement());
164 } else if (reason instanceof Universal) {
165 ok = check(reasonType.getUniversal(), i, line.getFormula().getElement());
166 } else if (reason instanceof Existential) {
167 ok = check(reasonType.getExistential(), i, line.getFormula().getElement());
168 } else {
169 ok = false;
170 handleProofCheckException(
171 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
172 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
173 + reason.getName(),
174 getCurrentContext());
175 }
176 lineProved[i] = ok;
177 // check if last proof line is identical with proposition formula
178 if (i == proof.size() - 1) {
179 if (!formula.equals(line.getFormula().getElement())) {
180 handleProofCheckException(
181 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
182 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT
183 + reason.getName(),
184 getModuleContextOfProofLineFormula(i));
185 }
186 }
187 }
188 return exceptions;
189 }
190
191 private boolean check(final Add add, final int i, final Element element) {
192 final String context = currentContext.getLocationWithinModule();
193 boolean ok = true;
194 if (add.getReference() == null) {
195 ok = false;
196 setLocationWithinModule(context + ".getReference()");
197 handleProofCheckException(
198 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
199 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
200 getCurrentContext());
201 return ok;
202 }
203 if (!resolver.hasProvedFormula(add.getReference())) {
204 ok = false;
205 setLocationWithinModule(context + ".getReference()");
206 handleProofCheckException(
207 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
208 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
209 + add.getReference(),
210 getCurrentContext());
211 return ok;
212 }
213 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
214 final Element current = resolver.getNormalizedFormula(element);
215 if (!EqualsUtility.equals(expected, current)) {
216 ok = false;
217 handleProofCheckException(
218 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
219 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
220 + add.getReference(),
221 getDiffModuleContextOfProofLineFormula(i, expected));
222 return ok;
223 }
224 return ok;
225 }
226
227 private boolean check(final Rename rename, final int i, final Element element) {
228 final String context = currentContext.getLocationWithinModule();
229 boolean ok = true;
230 final Integer n = (Integer) label2line.get(rename.getReference());
231 if (n == null) {
232 ok = false;
233 setLocationWithinModule(context + ".getReference()");
234 handleProofCheckException(
235 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
236 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
237 + rename.getReference(),
238 getCurrentContext());
239 // } else if (!lineProved[n.intValue()]) {
240 // ok = false;
241 // setLocationWithinModule(context + ".getReference()");
242 // handleProofCheckException(
243 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
244 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
245 // + rename.getReference(),
246 // getCurrentContext());
247 } else {
248 final Element f = getNormalizedProofLine(n);
249 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
250 rename.getOriginalSubjectVariable(),
251 rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
252 new Enumerator());
253 final Element current = resolver.getNormalizedFormula(element);
254 if (!EqualsUtility.equals(expected, current)) {
255 ok = false;
256 handleProofCheckException(
257 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
258 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
259 + rename.getReference(),
260 getDiffModuleContextOfProofLineFormula(i, expected));
261 } else {
262 ok = true;
263 }
264 }
265 return ok;
266 }
267
268 private boolean check(final SubstFree substfree, final int i, final Element element) {
269 final String context = currentContext.getLocationWithinModule();
270 boolean ok = true;
271 final Integer n = (Integer) label2line.get(substfree.getReference());
272 if (n == null) {
273 ok = false;
274 setLocationWithinModule(context + ".getReference()");
275 handleProofCheckException(
276 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
277 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
278 + substfree.getReference(),
279 getCurrentContext());
280 // } else if (!lineProved[n.intValue()]) {
281 // ok = false;
282 // setLocationWithinModule(context + ".getReference()");
283 // handleProofCheckException(
284 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
285 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
286 // + substfree.getReference(),
287 // getCurrentContext());
288 } else {
289 final Element f = getNormalizedProofLine(n);
290 final Element current = resolver.getNormalizedFormula(element);
291 final Element expected = f.replace(substfree.getSubjectVariable(),
292 resolver.getNormalizedFormula(substfree.getSubstituteTerm()));
293 if (!EqualsUtility.equals(current, expected)) {
294 ok = false;
295 handleProofCheckException(
296 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
297 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
298 + substfree.getReference(),
299 getDiffModuleContextOfProofLineFormula(i, expected));
300 return ok;
301 }
302 }
303 return ok;
304 }
305
306 private boolean check(final SubstPred substpred, final int i, final Element element) {
307 final String context = currentContext.getLocationWithinModule();
308 boolean ok = true;
309 final Integer n = (Integer) label2line.get(substpred.getReference());
310 if (n == null) {
311 ok = false;
312 setLocationWithinModule(context + ".getReference()");
313 handleProofCheckException(
314 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
315 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
316 + substpred.getReference(),
317 getCurrentContext());
318 // } else if (!lineProved[n.intValue()]) {
319 // ok = false;
320 // setLocationWithinModule(context + ".getReference()");
321 // handleProofCheckException(
322 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
323 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
324 // + substpred.getReference(),
325 // getCurrentContext());
326 } else {
327 final Element alpha = getNormalizedProofLine(n);
328 final Element current = resolver.getNormalizedFormula(element);
329 if (substpred.getSubstituteFormula() == null) {
330 ok = false;
331 handleProofCheckException(
332 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
333 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
334 getCurrentContext());
335 return ok;
336 }
337 final Element p = resolver.getNormalizedFormula(substpred.getPredicateVariable());
338 final Element beta = resolver.getNormalizedFormula(substpred.getSubstituteFormula());
339 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
340 if (!EqualsUtility.equals(current, expected)) {
341 ok = false;
342 handleProofCheckException(
343 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
344 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
345 + substpred.getReference(),
346 getDiffModuleContextOfProofLineFormula(i, expected));
347 return ok;
348 }
349 // check precondition: predicate variable p must have n pairwise different free subject
350 // variables as arguments
351 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
352 if (predFree.size() != p.getList().size() - 1) {
353 ok = false;
354 setLocationWithinModule(context + ".getPredicateVariable()");
355 handleProofCheckException(
356 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
357 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
358 getDiffModuleContextOfProofLineFormula(i, expected));
359 return ok;
360 }
361 for (int j = 1; j < p.getList().size(); j++) {
362 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
363 ok = false;
364 setLocationWithinModule(context + ".getPredicateVariable()");
365 handleProofCheckException(
366 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
367 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
368 getCurrentContext());
369 return ok;
370 }
371 }
372 // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
373 // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
374 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
375 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
376 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
377 ok = false;
378 setLocationWithinModule(context + ".getSubstituteFormula()");
379 handleProofCheckException(
380 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
381 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
382 getCurrentContext());
383 return ok;
384 }
385 // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
386 // no bound variable of $\beta(x_1, \ldots, x_n)$
387 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
388 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
389 ok = false;
390 setLocationWithinModule(context + ".getSubstituteFormula()");
391 handleProofCheckException(
392 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
393 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
394 getCurrentContext());
395 return ok;
396 }
397 // check precondition: resulting formula is well formed was already done by well formed
398 // checker
399 }
400 return ok;
401 }
402
403 private boolean check(final SubstFunc substfunc, final int i, final Element element) {
404 final String context = currentContext.getLocationWithinModule();
405 boolean ok = true;
406 final Integer n = (Integer) label2line.get(substfunc.getReference());
407 if (n == null) {
408 ok = false;
409 setLocationWithinModule(context + ".getReference()");
410 handleProofCheckException(
411 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
412 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
413 + substfunc.getReference(),
414 getCurrentContext());
415 // } else if (!lineProved[n.intValue()]) {
416 // ok = false;
417 // setLocationWithinModule(context + ".getReference()");
418 // handleProofCheckException(
419 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
420 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
421 // + substfunc.getReference(),
422 // getCurrentContext());
423 } else {
424 final Element alpha = getNormalizedProofLine(n);
425 final Element current = resolver.getNormalizedFormula(element);
426 if (substfunc.getSubstituteTerm() == null) {
427 ok = false;
428 handleProofCheckException(
429 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
430 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
431 getCurrentContext());
432 return ok;
433 }
434 final Element sigma = resolver.getNormalizedFormula(substfunc.getFunctionVariable());
435 final Element tau = resolver.getNormalizedFormula(substfunc.getSubstituteTerm());
436 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
437 if (!EqualsUtility.equals(current, expected)) {
438 ok = false;
439 handleProofCheckException(
440 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
441 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
442 + substfunc.getReference(),
443 getDiffModuleContextOfProofLineFormula(i, expected));
444 return ok;
445 }
446 // check precondition: function variable $\sigma$ must have n pairwise different free
447 // subject variables as arguments
448 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
449 if (funcFree.size() != sigma.getList().size() - 1) {
450 ok = false;
451 setLocationWithinModule(context + ".getPredicateVariable()");
452 handleProofCheckException(
453 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
454 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
455 getDiffModuleContextOfProofLineFormula(i, expected));
456 return ok;
457 }
458 for (int j = 1; j < sigma.getList().size(); j++) {
459 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
460 ok = false;
461 setLocationWithinModule(context + ".getPredicateVariable()");
462 handleProofCheckException(
463 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
464 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
465 getCurrentContext());
466 return ok;
467 }
468 }
469 // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
470 // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
471 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
472 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
473 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
474 ok = false;
475 setLocationWithinModule(context + ".getSubstituteFormula()");
476 handleProofCheckException(
477 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
478 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
479 getCurrentContext());
480 return ok;
481 }
482 // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
483 // contains no bound variable of $\tau(x_1, \ldots, x_n)$
484 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
485 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
486 ok = false;
487 setLocationWithinModule(context + ".getSubstituteFormula()");
488 handleProofCheckException(
489 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
490 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
491 getCurrentContext());
492 return ok;
493 }
494 // check precondition: resulting formula is well formed was already done by well formed
495 // checker
496 }
497 return ok;
498 }
499
500 private boolean check(final ModusPonens mp, final int i, final Element element) {
501 final String context = currentContext.getLocationWithinModule();
502 boolean ok = true;
503 final Integer n1 = (Integer) label2line.get(mp.getReference1());
504 if (n1 == null) {
505 ok = false;
506 setLocationWithinModule(context + ".getReference1()");
507 handleProofCheckException(
508 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
509 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
510 + mp.getReference1(),
511 getCurrentContext());
512 // } else if (!lineProved[n1.intValue()]) {
513 // ok = false;
514 // setLocationWithinModule(context + ".getReference1()");
515 // handleProofCheckException(
516 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
517 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
518 // + mp.getReference1(),
519 // getCurrentContext());
520 }
521 final Integer n2 = (Integer) label2line.get(mp.getReference2());
522 if (n2 == null) {
523 ok = false;
524 setLocationWithinModule(context + ".getReference2()");
525 handleProofCheckException(
526 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
527 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
528 + mp.getReference2(),
529 getCurrentContext());
530 // } else if (!lineProved[n2.intValue()]) {
531 // ok = false;
532 // setLocationWithinModule(context + ".getReference2()");
533 // handleProofCheckException(
534 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
535 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
536 // + mp.getReference1(),
537 // getCurrentContext());
538 }
539 if (ok) {
540 final Element f1 = getNormalizedProofLine(n1);
541 final Element f2 = getNormalizedProofLine(n2);
542 final Element current = getNormalizedProofLine(i);
543 if (!FormulaUtility.isImplication(f1)) {
544 ok = false;
545 setLocationWithinModule(context + ".getReference1()");
546 handleProofCheckException(
547 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
548 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
549 + mp.getReference1(),
550 getCurrentContext());
551 } else if (!f2.equals(f1.getList().getElement(0))) {
552 ok = false;
553 setLocationWithinModule(context + ".getReference2()");
554 handleProofCheckException(
555 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
556 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
557 + mp.getReference2(),
558 getCurrentContext(),
559 getModuleContextOfProofLineFormula(n1.intValue()));
560 } else if (!current.equals(f1.getList().getElement(1))) {
561 ok = false;
562 setLocationWithinModule(context + ".getReference1()");
563 handleProofCheckException(
564 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
565 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
566 + mp.getReference1(),
567 getCurrentContext(),
568 getModuleContextOfProofLineFormula(n1.intValue()));
569 } else {
570 ok = true;
571 }
572 }
573 return ok;
574 }
575
576 private boolean check(final Universal universal, final int i, final Element element) {
577 final String context = currentContext.getLocationWithinModule();
578 boolean ok = true;
579 final Integer n = (Integer) label2line.get(universal.getReference());
580 if (n == null) {
581 ok = false;
582 setLocationWithinModule(context + ".getReference()");
583 handleProofCheckException(
584 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
585 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
586 + universal.getReference(),
587 getCurrentContext());
588 // } else if (!lineProved[n.intValue()]) {
589 // ok = false;
590 // setLocationWithinModule(context + ".getReference()");
591 // handleProofCheckException(
592 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
593 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
594 // + universal.getReference(),
595 // getCurrentContext());
596 } else {
597 final Element f = getNormalizedProofLine(n);
598 final Element current = resolver.getNormalizedFormula(element);
599 if (!FormulaUtility.isImplication(f)) {
600 ok = false;
601 setLocationWithinModule(context + ".getReference()");
602 handleProofCheckException(
603 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
604 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
605 + universal.getReference(),
606 getCurrentContext());
607 return ok;
608 }
609 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
610 ok = false;
611 setLocationWithinModule(context + ".getSubjectVariable()");
612 handleProofCheckException(
613 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
614 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
615 getCurrentContext());
616 return ok;
617 }
618 final DefaultElementList expected = new DefaultElementList(f.getList().getOperator());
619 expected.add((f.getList().getElement(0)));
620 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
621 uni.add(universal.getSubjectVariable());
622 uni.add(f.getList().getElement(1));
623 expected.add(uni);
624 if (!EqualsUtility.equals(current, expected)) {
625 ok = false;
626 handleProofCheckException(
627 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
628 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
629 + universal.getReference(),
630 getDiffModuleContextOfProofLineFormula(i, expected));
631 return ok;
632 }
633 }
634 return ok;
635 }
636
637 private boolean check(final Existential existential, final int i, final Element element) {
638 final String context = currentContext.getLocationWithinModule();
639 boolean ok = true;
640 final Integer n = (Integer) label2line.get(existential.getReference());
641 if (n == null) {
642 ok = false;
643 setLocationWithinModule(context + ".getReference()");
644 handleProofCheckException(
645 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
646 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
647 + existential.getReference(),
648 getCurrentContext());
649 // } else if (!lineProved[n.intValue()]) {
650 // ok = false;
651 // setLocationWithinModule(context + ".getReference()");
652 // handleProofCheckException(
653 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
654 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
655 // + existential.getReference(),
656 // getCurrentContext());
657 } else {
658 final Element f = getNormalizedProofLine(n);
659 final Element current = resolver.getNormalizedFormula(element);
660 if (!FormulaUtility.isImplication(f)) {
661 ok = false;
662 setLocationWithinModule(context + ".getReference()");
663 handleProofCheckException(
664 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
665 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
666 + existential.getReference(),
667 getCurrentContext());
668 return ok;
669 }
670 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
671 ok = false;
672 setLocationWithinModule(context + ".getSubjectVariable()");
673 handleProofCheckException(
674 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
675 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
676 getCurrentContext());
677 return ok;
678 }
679 final DefaultElementList expected = new DefaultElementList(f.getList().getOperator());
680 final ElementList exi = new DefaultElementList(
681 Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
682 exi.add(existential.getSubjectVariable());
683 exi.add(f.getList().getElement(0));
684 expected.add(exi);
685 expected.add((f.getList().getElement(1)));
686 if (!EqualsUtility.equals(current, expected)) {
687 ok = false;
688 handleProofCheckException(
689 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
690 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
691 + existential.getReference(),
692 getDiffModuleContextOfProofLineFormula(i, expected));
693 return ok;
694 }
695 }
696 return ok;
697 }
698
699 private ModuleContext getModuleContextOfProofLineFormula(final int i) {
700 return new ModuleContext(moduleContext.getModuleLocation(),
701 moduleContext.getLocationWithinModule() + ".get(" + i
702 + ").getFormula().getElement()");
703 }
704
705 private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
706 final Element expected) {
707 final String diff = FormulaUtility.getDifferenceLocation(
708 proof.get(i).getFormula().getElement(), expected);
709 return new ModuleContext(moduleContext.getModuleLocation(),
710 moduleContext.getLocationWithinModule() + ".get(" + i
711 + ").getFormula().getElement()" + diff);
712 }
713
714 private Element getNormalizedProofLine(final Integer n) {
715 if (n == null) {
716 return null;
717 }
718 return getNormalizedProofLine(n.intValue());
719 }
720
721 private Element getNormalizedProofLine(final int i) {
722 if (i < 0 || i >= proof.size()) {
723 return null;
724 }
725 return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
726 }
727
728 /**
729 * Add new {@link ProofCheckException} to exception list.
730 *
731 * @param code Error code.
732 * @param msg Error message.
733 * @param context Error context.
734 */
735 private void handleProofCheckException(final int code, final String msg,
736 final ModuleContext context) {
737 // System.out.println(context);
738 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
739 final ProofCheckException ex = new ProofCheckException(code, msg, context);
740 exceptions.add(ex);
741 }
742
743 /**
744 * Add new {@link ProofCheckException} to exception list.
745 *
746 * @param code Error code.
747 * @param msg Error message.
748 * @param context Error context.
749 * @param referenceContext Reference context.
750 */
751 private void handleProofCheckException(final int code, final String msg,
752 final ModuleContext context, final ModuleContext referenceContext) {
753 // System.out.println(context);
754 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
755 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
756 referenceContext);
757 exceptions.add(ex);
758 }
759
760 /**
761 * Set location information where are we within the original module.
762 *
763 * @param locationWithinModule Location within module.
764 */
765 protected void setLocationWithinModule(final String locationWithinModule) {
766 getCurrentContext().setLocationWithinModule(locationWithinModule);
767 }
768
769 /**
770 * Get current context within original.
771 *
772 * @return Current context.
773 */
774 protected final ModuleContext getCurrentContext() {
775 return currentContext;
776 }
777
778
779 }
|