0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.bo.logic.proof.checker;
0017
0018 import java.util.HashMap;
0019 import java.util.Map;
0020
0021 import org.qedeq.base.io.Version;
0022 import org.qedeq.base.io.VersionSet;
0023 import org.qedeq.base.utility.Enumerator;
0024 import org.qedeq.base.utility.EqualsUtility;
0025 import org.qedeq.base.utility.StringUtility;
0026 import org.qedeq.kernel.bo.logic.common.FormulaChecker;
0027 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
0028 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
0029 import org.qedeq.kernel.bo.logic.common.Operators;
0030 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
0031 import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
0032 import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
0033 import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
0034 import org.qedeq.kernel.se.base.list.Element;
0035 import org.qedeq.kernel.se.base.list.ElementList;
0036 import org.qedeq.kernel.se.base.module.Add;
0037 import org.qedeq.kernel.se.base.module.ConditionalProof;
0038 import org.qedeq.kernel.se.base.module.Existential;
0039 import org.qedeq.kernel.se.base.module.FormalProofLine;
0040 import org.qedeq.kernel.se.base.module.FormalProofLineList;
0041 import org.qedeq.kernel.se.base.module.ModusPonens;
0042 import org.qedeq.kernel.se.base.module.Reason;
0043 import org.qedeq.kernel.se.base.module.Rename;
0044 import org.qedeq.kernel.se.base.module.Rule;
0045 import org.qedeq.kernel.se.base.module.SubstFree;
0046 import org.qedeq.kernel.se.base.module.SubstFunc;
0047 import org.qedeq.kernel.se.base.module.SubstPred;
0048 import org.qedeq.kernel.se.base.module.Universal;
0049 import org.qedeq.kernel.se.common.ModuleAddress;
0050 import org.qedeq.kernel.se.common.ModuleContext;
0051 import org.qedeq.kernel.se.common.RuleKey;
0052 import org.qedeq.kernel.se.dto.list.DefaultElementList;
0053 import org.qedeq.kernel.se.dto.list.ElementSet;
0054
0055
0056 /**
0057 * Formal proof checker for basic rules and conditional proof.
0058 *
0059 * @author Michael Meyling
0060 */
0061 public class ProofChecker2Impl implements ProofChecker, ReferenceResolver {
0062
0063 /** Proof we want to check. */
0064 private FormalProofLineList proof;
0065
0066 /** Module context of proof line list. */
0067 private ModuleContext moduleContext;
0068
0069 /** Current context. */
0070 private ModuleContext currentContext;
0071
0072 /** Resolver for external references. */
0073 private ReferenceResolver resolver;
0074
0075 /** All exceptions that occurred during checking. */
0076 private LogicalCheckExceptionList exceptions;
0077
0078 /** Array with proof status for each proof line. */
0079 private boolean[] lineProved;
0080
0081 /** Maps local proof line labels to local line number Integers. */
0082 private Map label2line;
0083
0084 /** Rule version we support. */
0085 private final VersionSet supported;
0086
0087 /** These preconditions apply. This is a conjunction with 0 to n elements. */
0088 private ElementList conditions;
0089
0090 /** Rule existence checker. */
0091 private RuleChecker checker;
0092
0093 /**
0094 * Constructor.
0095 */
0096 public ProofChecker2Impl() {
0097 supported = new VersionSet();
0098 supported.add("0.01.00");
0099 supported.add("0.02.00");
0100 }
0101
0102 public LogicalCheckExceptionList checkRule(final Rule rule,
0103 final ModuleContext context, final RuleChecker checker,
0104 final ReferenceResolver resolver) {
0105 exceptions = new LogicalCheckExceptionList();
0106 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
0107 if (rule.getVersion() == null || !supported.contains(rule.getVersion())) {
0108 final ProofCheckException ex = new ProofCheckException(
0109 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0110 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey
0111 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0112 context);
0113 exceptions.add(ex);
0114 }
0115 return exceptions;
0116 }
0117
0118 public LogicalCheckExceptionList checkProof(final Element formula,
0119 final FormalProofLineList proof,
0120 final RuleChecker checker,
0121 final ModuleContext moduleContext,
0122 final ReferenceResolver resolver) {
0123 final DefaultElementList con = new DefaultElementList(
0124 Operators.CONJUNCTION_OPERATOR);
0125 // we have no conditions, so we add an empty condition
0126 return checkProof(con, formula, proof, checker, moduleContext, resolver);
0127 }
0128
0129 private LogicalCheckExceptionList checkProof(final ElementList conditions, final Element formula,
0130 final FormalProofLineList proof,
0131 final RuleChecker checker,
0132 final ModuleContext moduleContext,
0133 final ReferenceResolver resolver) {
0134 this.conditions = conditions;
0135 this.proof = proof;
0136 this.checker = checker;
0137 this.resolver = resolver;
0138 this.moduleContext = moduleContext;
0139 // use copy constructor for changing context
0140 currentContext = new ModuleContext(moduleContext);
0141 exceptions = new LogicalCheckExceptionList();
0142 final String context = moduleContext.getLocationWithinModule();
0143 lineProved = new boolean[proof.size()];
0144 label2line = new HashMap();
0145 for (int i = 0; i < proof.size(); i++) {
0146 boolean ok = true;
0147 setLocationWithinModule(context + ".get(" + i + ")");
0148 final FormalProofLine line = proof.get(i);
0149 if (line == null || line.getFormula() == null
0150 || line.getFormula().getElement() == null) {
0151 ok = false;
0152 handleProofCheckException(
0153 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
0154 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
0155 getCurrentContext());
0156 continue;
0157 }
0158 setLocationWithinModule(context + ".get(" + i + ").getReason()");
0159 final Reason reason = line.getReason();
0160 if (reason == null) {
0161 ok = false;
0162 handleProofCheckException(
0163 BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
0164 BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
0165 getCurrentContext());
0166 continue;
0167 }
0168 if (line.getLabel() != null && line.getLabel().length() > 0) {
0169 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
0170 addLocalLineLabel(i, line.getLabel());
0171 }
0172
0173 // check if the formula together with the conditions is well formed
0174 if (hasConditions()) {
0175 setLocationWithinModule(context + ".get(" + i + ").getFormula.getElement()");
0176 ElementList full = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
0177 if (conditions.size() > 1) {
0178 full.add(conditions);
0179 } else {
0180 full.add(conditions.getElement(0));
0181 }
0182 full.add(line.getFormula().getElement());
0183 FormulaChecker checkWf = new FormulaCheckerImpl(); // TODO 20110612 m31: use factory?
0184 final LogicalCheckExceptionList list = checkWf.checkFormula(full, getCurrentContext());
0185 if (list.size() > 0) {
0186 ok = false;
0187 handleProofCheckException(
0188 BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_CODE,
0189 BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT
0190 + list.get(0).getMessage(),
0191 getCurrentContext());
0192 continue;
0193 }
0194 }
0195
0196 // check if only defined rules are used
0197 // FIXME 20110316 m31: this is a dirty trick to get the context of the reason
0198 // perhaps we can solve this more elegantly?
0199 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
0200 if (getReason.endsWith("Vo")) {
0201 getReason = getReason.substring(0, getReason.length() - 2) + "()";
0202 setLocationWithinModule(context + ".get(" + i + ").getReason()"
0203 + getReason);
0204 // System.out.println(getCurrentContext());
0205 }
0206 if (reason instanceof Add) {
0207 ok = check((Add) reason, i, line.getFormula().getElement());
0208 } else if (reason instanceof Rename) {
0209 ok = check((Rename) reason, i, line.getFormula().getElement());
0210 } else if (reason instanceof ModusPonens) {
0211 ok = check((ModusPonens) reason, i, line.getFormula().getElement());
0212 } else if (reason instanceof SubstFree) {
0213 ok = check((SubstFree) reason, i, line.getFormula().getElement());
0214 } else if (reason instanceof SubstPred) {
0215 ok = check((SubstPred) reason, i, line.getFormula().getElement());
0216 } else if (reason instanceof SubstFunc) {
0217 ok = check((SubstFunc) reason, i, line.getFormula().getElement());
0218 } else if (reason instanceof Universal) {
0219 ok = check((Universal) reason, i, line.getFormula().getElement());
0220 } else if (reason instanceof Existential) {
0221 ok = check((Existential) reason, i, line.getFormula().getElement());
0222 } else if (reason instanceof ConditionalProof) {
0223 setLocationWithinModule(context + ".get(" + i + ")");
0224 ok = check((ConditionalProof) reason, i, line.getFormula().getElement());
0225 } else {
0226 ok = false;
0227 handleProofCheckException(
0228 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
0229 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
0230 + reason.getName(),
0231 getCurrentContext());
0232 }
0233 lineProved[i] = ok;
0234 // check if last proof line is identical with proposition formula
0235 if (i == proof.size() - 1) {
0236 if (!formula.equals(line.getFormula().getElement())) {
0237 handleProofCheckException(
0238 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
0239 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT,
0240 getModuleContextOfProofLineFormula(i));
0241 }
0242 }
0243 }
0244 return exceptions;
0245 }
0246
0247 private void addLocalLineLabel(final int i, final String label) {
0248 if (label != null && label.length() > 0) {
0249 final Integer n = (Integer) label2line.get(label);
0250 if (n != null) {
0251 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
0252 moduleContext.getLocationWithinModule() + ".get("
0253 + ((Integer) label2line.get(label)
0254 + ").getLabel()"));
0255 handleProofCheckException(
0256 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
0257 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
0258 + label,
0259 getCurrentContext(),
0260 lc);
0261 } else {
0262 if (isLocalProofLineReference(label)) {
0263 handleProofCheckException(
0264 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
0265 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
0266 + label,
0267 getCurrentContext(),
0268 resolver.getReferenceContext(label));
0269 // System.out.println("we hava label already: " + label);
0270 // ProofFinderUtility.println(getNormalizedLocalProofLineReference(label));
0271 }
0272 }
0273 // System.out.println("adding label: " + label);
0274 label2line.put(label, new Integer(i));
0275 }
0276 }
0277
0278 private boolean check(final Add add, final int i, final Element element) {
0279 final String context = currentContext.getLocationWithinModule();
0280 boolean ok = true;
0281 if (add.getReference() == null) {
0282 ok = false;
0283 setLocationWithinModule(context + ".getReference()");
0284 handleProofCheckException(
0285 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
0286 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
0287 getCurrentContext());
0288 return ok;
0289 }
0290 if (!resolver.isProvedFormula(add.getReference())) {
0291 ok = false;
0292 setLocationWithinModule(context + ".getReference()");
0293 handleProofCheckException(
0294 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
0295 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
0296 + add.getReference(),
0297 getCurrentContext());
0298 return ok;
0299 }
0300 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
0301 final Element current = resolver.getNormalizedFormula(element);
0302 if (!EqualsUtility.equals(expected, current)) {
0303 ok = false;
0304 handleProofCheckException(
0305 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0306 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0307 + add.getReference(),
0308 getDiffModuleContextOfProofLineFormula(i, expected));
0309 return ok;
0310 }
0311 final RuleKey defined = checker.getRule(add.getName());
0312 if (defined == null) {
0313 ok = false;
0314 handleProofCheckException(
0315 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0316 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0317 + add.getName(),
0318 getCurrentContext());
0319 return ok;
0320 } else if (!supported.contains(defined.getVersion())) {
0321 ok = false;
0322 handleProofCheckException(
0323 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0324 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0325 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0326 getCurrentContext());
0327 return ok;
0328 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0329 ok = false;
0330 handleProofCheckException(
0331 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0332 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0333 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0334 getCurrentContext());
0335 return ok;
0336 }
0337 return ok;
0338 }
0339
0340 private boolean check(final Rename rename, final int i, final Element element) {
0341 final String context = currentContext.getLocationWithinModule();
0342 boolean ok = true;
0343 final Element f = getNormalizedLocalProofLineReference(rename.getReference());
0344 if (f == null) {
0345 ok = false;
0346 setLocationWithinModule(context + ".getReference()");
0347 handleProofCheckException(
0348 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0349 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0350 + rename.getReference(),
0351 getCurrentContext());
0352 } else {
0353 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
0354 rename.getOriginalSubjectVariable(),
0355 rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
0356 new Enumerator());
0357 final Element current = resolver.getNormalizedFormula(element);
0358 if (!EqualsUtility.equals(expected, current)) {
0359 ok = false;
0360 handleProofCheckException(
0361 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0362 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0363 + rename.getReference(),
0364 getDiffModuleContextOfProofLineFormula(i, expected));
0365 } else {
0366 ok = true;
0367 }
0368 }
0369 final RuleKey defined = checker.getRule(rename.getName());
0370 if (defined == null) {
0371 ok = false;
0372 handleProofCheckException(
0373 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0374 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0375 + rename.getName(),
0376 getCurrentContext());
0377 return ok;
0378 } else if (!supported.contains(defined.getVersion())) {
0379 ok = false;
0380 handleProofCheckException(
0381 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0382 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0383 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0384 getCurrentContext());
0385 return ok;
0386 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0387 ok = false;
0388 handleProofCheckException(
0389 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0390 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0391 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0392 getCurrentContext());
0393 return ok;
0394 }
0395 return ok;
0396 }
0397
0398 private boolean check(final SubstFree substFree, final int i, final Element element) {
0399 final String context = currentContext.getLocationWithinModule();
0400 boolean ok = true;
0401 final Element f = getNormalizedLocalProofLineReference(substFree.getReference());
0402 if (f == null) {
0403 ok = false;
0404 setLocationWithinModule(context + ".getReference()");
0405 handleProofCheckException(
0406 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0407 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0408 + substFree.getReference(),
0409 getCurrentContext());
0410 } else {
0411 final Element current = resolver.getNormalizedFormula(element);
0412 final Element expected = f.replace(substFree.getSubjectVariable(),
0413 resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
0414 if (!EqualsUtility.equals(current, expected)) {
0415 ok = false;
0416 handleProofCheckException(
0417 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0418 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0419 + substFree.getReference(),
0420 getDiffModuleContextOfProofLineFormula(i, expected));
0421 return ok;
0422 }
0423 }
0424 // check precondition: subject variable doesn't occur in a precondition
0425 if (FormulaUtility.containsOperatorVariable(conditions, substFree.getSubjectVariable())) {
0426 ok = false;
0427 setLocationWithinModule(context + ".getSubstituteFormula()");
0428 handleProofCheckException(
0429 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
0430 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
0431 getCurrentContext());
0432 return ok;
0433 }
0434 final RuleKey defined = checker.getRule(substFree.getName());
0435 if (defined == null) {
0436 ok = false;
0437 handleProofCheckException(
0438 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0439 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0440 + substFree.getName(),
0441 getCurrentContext());
0442 return ok;
0443 } else if (!supported.contains(defined.getVersion())) {
0444 ok = false;
0445 handleProofCheckException(
0446 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0447 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0448 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0449 getCurrentContext());
0450 return ok;
0451 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0452 ok = false;
0453 handleProofCheckException(
0454 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0455 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0456 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0457 getCurrentContext());
0458 return ok;
0459 }
0460 return ok;
0461 }
0462
0463 private boolean check(final SubstPred substPred, final int i, final Element element) {
0464 final String context = currentContext.getLocationWithinModule();
0465 boolean ok = true;
0466 final Element alpha = getNormalizedLocalProofLineReference(substPred.getReference());
0467 if (alpha == null) {
0468 ok = false;
0469 setLocationWithinModule(context + ".getReference()");
0470 handleProofCheckException(
0471 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0472 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0473 + substPred.getReference(),
0474 getCurrentContext());
0475 return ok;
0476 }
0477 final Element current = resolver.getNormalizedFormula(element);
0478 if (substPred.getSubstituteFormula() == null) {
0479 ok = false;
0480 handleProofCheckException(
0481 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
0482 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
0483 getCurrentContext());
0484 return ok;
0485 }
0486 final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
0487 final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
0488 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
0489 if (!EqualsUtility.equals(current, expected)) {
0490 ok = false;
0491 handleProofCheckException(
0492 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0493 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0494 + substPred.getReference(),
0495 getDiffModuleContextOfProofLineFormula(i, expected));
0496 return ok;
0497 }
0498 // check precondition: predicate variable p must have n pairwise different free subject
0499 // variables as arguments
0500 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
0501 if (predFree.size() != p.getList().size() - 1) {
0502 ok = false;
0503 setLocationWithinModule(context + ".getPredicateVariable()");
0504 handleProofCheckException(
0505 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0506 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0507 getDiffModuleContextOfProofLineFormula(i, expected));
0508 return ok;
0509 }
0510 for (int j = 1; j < p.getList().size(); j++) {
0511 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
0512 ok = false;
0513 setLocationWithinModule(context + ".getPredicateVariable()");
0514 handleProofCheckException(
0515 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0516 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0517 getCurrentContext());
0518 return ok;
0519 }
0520 }
0521 // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
0522 // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
0523 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
0524 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
0525 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
0526 ok = false;
0527 setLocationWithinModule(context + ".getSubstituteFormula()");
0528 handleProofCheckException(
0529 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
0530 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
0531 getCurrentContext());
0532 return ok;
0533 }
0534 // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
0535 // no bound variable of $\beta(x_1, \ldots, x_n)$
0536 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
0537 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
0538 ok = false;
0539 setLocationWithinModule(context + ".getSubstituteFormula()");
0540 handleProofCheckException(
0541 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
0542 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
0543 getCurrentContext());
0544 return ok;
0545 }
0546 // check precondition: $\sigma(...)$ dosn't occur in a precondition
0547 if (FormulaUtility.containsOperatorVariable(conditions, p)) {
0548 ok = false;
0549 setLocationWithinModule(context + ".getPredicateVariable()");
0550 handleProofCheckException(
0551 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
0552 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
0553 getCurrentContext());
0554 return ok;
0555 }
0556 // check precondition: resulting formula is well formed was already done by well formed
0557 // checker
0558
0559 final RuleKey defined = checker.getRule(substPred.getName());
0560 if (defined == null) {
0561 ok = false;
0562 handleProofCheckException(
0563 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0564 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0565 + substPred.getName(),
0566 getCurrentContext());
0567 return ok;
0568 } else if (!supported.contains(defined.getVersion())) {
0569 ok = false;
0570 handleProofCheckException(
0571 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0572 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0573 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0574 getCurrentContext());
0575 return ok;
0576 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0577 ok = false;
0578 handleProofCheckException(
0579 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0580 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0581 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0582 getCurrentContext());
0583 return ok;
0584 }
0585 return ok;
0586 }
0587
0588 private boolean check(final SubstFunc substFunc, final int i, final Element element) {
0589 final String context = currentContext.getLocationWithinModule();
0590 boolean ok = true;
0591 final Element alpha = getNormalizedLocalProofLineReference(substFunc.getReference());
0592 if (alpha == null) {
0593 ok = false;
0594 setLocationWithinModule(context + ".getReference()");
0595 handleProofCheckException(
0596 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0597 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0598 + substFunc.getReference(),
0599 getCurrentContext());
0600 return ok;
0601 }
0602 final Element current = resolver.getNormalizedFormula(element);
0603 if (substFunc.getSubstituteTerm() == null) {
0604 ok = false;
0605 handleProofCheckException(
0606 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
0607 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
0608 getCurrentContext());
0609 return ok;
0610 }
0611 final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
0612 final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
0613 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
0614 if (!EqualsUtility.equals(current, expected)) {
0615 ok = false;
0616 handleProofCheckException(
0617 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0618 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0619 + substFunc.getReference(),
0620 getDiffModuleContextOfProofLineFormula(i, expected));
0621 return ok;
0622 }
0623 // check precondition: function variable $\sigma$ must have n pairwise different free
0624 // subject variables as arguments
0625 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
0626 if (funcFree.size() != sigma.getList().size() - 1) {
0627 ok = false;
0628 setLocationWithinModule(context + ".getPredicateVariable()");
0629 handleProofCheckException(
0630 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0631 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0632 getDiffModuleContextOfProofLineFormula(i, expected));
0633 return ok;
0634 }
0635 for (int j = 1; j < sigma.getList().size(); j++) {
0636 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
0637 ok = false;
0638 setLocationWithinModule(context + ".getPredicateVariable()");
0639 handleProofCheckException(
0640 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0641 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0642 getCurrentContext());
0643 return ok;
0644 }
0645 }
0646 // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
0647 // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
0648 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
0649 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
0650 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
0651 ok = false;
0652 setLocationWithinModule(context + ".getSubstituteFormula()");
0653 handleProofCheckException(
0654 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
0655 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
0656 getCurrentContext());
0657 return ok;
0658 }
0659 // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
0660 // contains no bound variable of $\tau(x_1, \ldots, x_n)$
0661 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
0662 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
0663 ok = false;
0664 setLocationWithinModule(context + ".getSubstituteFormula()");
0665 handleProofCheckException(
0666 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
0667 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
0668 getCurrentContext());
0669 return ok;
0670 }
0671 // check precondition: $\sigma(...)$ dosn't occur in a precondition
0672 if (FormulaUtility.containsOperatorVariable(conditions, sigma)) {
0673 ok = false;
0674 setLocationWithinModule(context + ".getPredicateVariable()");
0675 handleProofCheckException(
0676 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
0677 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
0678 getCurrentContext());
0679 return ok;
0680 }
0681 // check precondition: resulting formula is well formed was already done by well formed
0682 // checker
0683
0684 final RuleKey defined = checker.getRule(substFunc.getName());
0685 if (defined == null) {
0686 ok = false;
0687 handleProofCheckException(
0688 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0689 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0690 + substFunc.getName(),
0691 getCurrentContext());
0692 return ok;
0693 } else if (!supported.contains(defined.getVersion())) {
0694 ok = false;
0695 handleProofCheckException(
0696 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0697 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0698 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0699 getCurrentContext());
0700 return ok;
0701 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0702 ok = false;
0703 handleProofCheckException(
0704 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0705 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0706 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0707 getCurrentContext());
0708 return ok;
0709 }
0710 return ok;
0711 }
0712
0713 private boolean check(final ModusPonens mp, final int i, final Element element) {
0714 final String context = currentContext.getLocationWithinModule();
0715 boolean ok = true;
0716 final Element f1 = getNormalizedLocalProofLineReference(mp.getReference1());
0717 if (f1 == null) {
0718 ok = false;
0719 setLocationWithinModule(context + ".getReference1()");
0720 handleProofCheckException(
0721 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0722 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0723 + mp.getReference1(),
0724 getCurrentContext());
0725 }
0726 final Element f2 = getNormalizedLocalProofLineReference(mp.getReference2());
0727 if (f2 == null) {
0728 ok = false;
0729 setLocationWithinModule(context + ".getReference2()");
0730 handleProofCheckException(
0731 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0732 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0733 + mp.getReference2(),
0734 getCurrentContext());
0735 }
0736 if (ok) {
0737 final Element current = getNormalizedFormula(element);
0738 if (!FormulaUtility.isImplication(f1)) {
0739 ok = false;
0740 setLocationWithinModule(context + ".getReference1()");
0741 handleProofCheckException(
0742 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
0743 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
0744 + mp.getReference1(),
0745 getCurrentContext());
0746 } else if (!f2.equals(f1.getList().getElement(0))) {
0747 ok = false;
0748 setLocationWithinModule(context + ".getReference2()");
0749 handleProofCheckException(
0750 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
0751 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
0752 + mp.getReference2(),
0753 getCurrentContext(),
0754 resolver.getReferenceContext(mp.getReference1()));
0755 } else if (!current.equals(f1.getList().getElement(1))) {
0756 ok = false;
0757 setLocationWithinModule(context + ".getReference1()");
0758 handleProofCheckException(
0759 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
0760 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
0761 + mp.getReference1(),
0762 getCurrentContext(),
0763 resolver.getReferenceContext(mp.getReference1()));
0764 } else {
0765 ok = true;
0766 }
0767 }
0768 final RuleKey defined = checker.getRule(mp.getName());
0769 if (defined == null) {
0770 ok = false;
0771 handleProofCheckException(
0772 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0773 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0774 + mp.getName(),
0775 getCurrentContext());
0776 return ok;
0777 } else if (!supported.contains(defined.getVersion())) {
0778 ok = false;
0779 handleProofCheckException(
0780 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0781 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0782 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0783 getCurrentContext());
0784 return ok;
0785 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0786 ok = false;
0787 handleProofCheckException(
0788 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0789 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0790 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0791 getCurrentContext());
0792 return ok;
0793 }
0794 return ok;
0795 }
0796
0797 private boolean check(final Universal universal, final int i, final Element element) {
0798 final String context = currentContext.getLocationWithinModule();
0799 boolean ok = true;
0800 final Element reference = getNormalizedLocalProofLineReference(universal.getReference());
0801 if (reference == null) {
0802 ok = false;
0803 setLocationWithinModule(context + ".getReference()");
0804 handleProofCheckException(
0805 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0806 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0807 + universal.getReference(),
0808 getCurrentContext());
0809 // } else if (!lineProved[n.intValue()]) {
0810 // ok = false;
0811 // setLocationWithinModule(context + ".getReference()");
0812 // handleProofCheckException(
0813 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
0814 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
0815 // + universal.getReference(),
0816 // getCurrentContext());
0817 } else {
0818 final Element current = getNormalizedFormula(element);
0819 if (!FormulaUtility.isImplication(current)) {
0820 ok = false;
0821 setLocationWithinModule(context + ".getReference()");
0822 handleProofCheckException(
0823 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
0824 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
0825 + universal.getReference(),
0826 getCurrentContext());
0827 return ok;
0828 }
0829 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
0830 ok = false;
0831 setLocationWithinModule(context + ".getSubjectVariable()");
0832 handleProofCheckException(
0833 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
0834 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
0835 getCurrentContext());
0836 return ok;
0837 }
0838 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
0839 expected.add(reference.getList().getElement(0));
0840 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
0841 uni.add(universal.getSubjectVariable());
0842 uni.add(reference.getList().getElement(1));
0843 expected.add(uni);
0844 // System.out.print("Expected: ");
0845 // ProofFinderUtility.println(expected);
0846 // System.out.print("Current : ");
0847 // ProofFinderUtility.println(current);
0848 if (!EqualsUtility.equals(current, expected)) {
0849 ok = false;
0850 handleProofCheckException(
0851 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0852 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0853 + universal.getReference(),
0854 getDiffModuleContextOfProofLineFormula(i, expected));
0855 return ok;
0856 }
0857 }
0858 final RuleKey defined = checker.getRule(universal.getName());
0859 if (defined == null) {
0860 ok = false;
0861 handleProofCheckException(
0862 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0863 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0864 + universal.getName(),
0865 getCurrentContext());
0866 return ok;
0867 } else if (!supported.contains(defined.getVersion())) {
0868 ok = false;
0869 handleProofCheckException(
0870 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0871 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0872 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0873 getCurrentContext());
0874 return ok;
0875 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0876 ok = false;
0877 handleProofCheckException(
0878 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0879 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0880 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0881 getCurrentContext());
0882 return ok;
0883 }
0884 return ok;
0885 }
0886
0887 private boolean check(final Existential existential, final int i, final Element element) {
0888 final String context = currentContext.getLocationWithinModule();
0889 boolean ok = true;
0890 final Element reference = getNormalizedLocalProofLineReference(existential.getReference());
0891 if (reference == null) {
0892 ok = false;
0893 setLocationWithinModule(context + ".getReference()");
0894 handleProofCheckException(
0895 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0896 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0897 + existential.getReference(),
0898 getCurrentContext());
0899 // } else if (!lineProved[n.intValue()]) {
0900 // ok = false;
0901 // setLocationWithinModule(context + ".getReference()");
0902 // handleProofCheckException(
0903 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
0904 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
0905 // + existential.getReference(),
0906 // getCurrentContext());
0907 } else {
0908 final Element current = getNormalizedFormula(element);
0909 if (!FormulaUtility.isImplication(current)) {
0910 ok = false;
0911 setLocationWithinModule(context + ".getReference()");
0912 handleProofCheckException(
0913 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
0914 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
0915 + existential.getReference(),
0916 getCurrentContext());
0917 return ok;
0918 }
0919 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
0920 ok = false;
0921 setLocationWithinModule(context + ".getSubjectVariable()");
0922 handleProofCheckException(
0923 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
0924 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
0925 getCurrentContext());
0926 return ok;
0927 }
0928 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
0929 final ElementList exi = new DefaultElementList(
0930 Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
0931 exi.add(existential.getSubjectVariable());
0932 exi.add(reference.getList().getElement(0));
0933 expected.add(exi);
0934 expected.add((reference.getList().getElement(1)));
0935 if (!EqualsUtility.equals(current, expected)) {
0936 ok = false;
0937 handleProofCheckException(
0938 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0939 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0940 + existential.getReference(),
0941 getDiffModuleContextOfProofLineFormula(i, expected));
0942 return ok;
0943 }
0944 }
0945 final RuleKey defined = checker.getRule(existential.getName());
0946 if (defined == null) {
0947 ok = false;
0948 handleProofCheckException(
0949 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0950 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0951 + existential.getName(),
0952 getCurrentContext());
0953 return ok;
0954 } else if (!supported.contains(defined.getVersion())) {
0955 ok = false;
0956 handleProofCheckException(
0957 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0958 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0959 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0960 getCurrentContext());
0961 return ok;
0962 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0963 ok = false;
0964 handleProofCheckException(
0965 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0966 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0967 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0968 getCurrentContext());
0969 return ok;
0970 }
0971 return ok;
0972 }
0973
0974 private boolean check(final ConditionalProof cp, final int i, final Element element) {
0975 final ModuleAddress address = currentContext.getModuleLocation();
0976 final String context = currentContext.getLocationWithinModule();
0977 // System.out.println(getCurrentContext());
0978 boolean ok = true;
0979 if (cp.getHypothesis() == null || cp.getHypothesis().getFormula() == null
0980 || cp.getHypothesis().getFormula().getElement() == null) {
0981 ok = false;
0982 setLocationWithinModule(context + ".getHypothesis()");
0983 handleProofCheckException(
0984 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
0985 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
0986 getCurrentContext());
0987 return ok;
0988 }
0989 if (cp.getFormalProofLineList() == null || cp.getFormalProofLineList().size() <= 0) {
0990 ok = false;
0991 setLocationWithinModule(context + ".getFormalProofLineList()");
0992 handleProofCheckException(
0993 BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE,
0994 BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT,
0995 getCurrentContext());
0996 return ok;
0997 }
0998 final ReferenceResolver newResolver = new ReferenceResolver() {
0999
1000 public Element getNormalizedFormula(final Element formula) {
1001 return ProofChecker2Impl.this.getNormalizedFormula(formula);
1002 }
1003
1004 public Element getNormalizedReferenceFormula(final String reference) {
1005 // System.out.println("Looking for " + reference);
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 // System.out.println("\t resolver looks for " + reference);
1037 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1038 // System.out.println("\t resolver found local " + reference);
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 // add hypothesis as new condition
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 // System.out.println("expected: ");
1092 // ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
1093 if (!EqualsUtility.equals(cp.getConclusion().getFormula().getElement(), expected)) {
1094 // System.out.println("found: ");
1095 // ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
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 * Have we any conditions. If yes we are within an conditional proof argument.
1159 *
1160 * @return Do we have conditions?
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 * Add new {@link ProofCheckException} to exception list.
1179 *
1180 * @param code Error code.
1181 * @param msg Error message.
1182 * @param context Error context.
1183 */
1184 private void handleProofCheckException(final int code, final String msg,
1185 final ModuleContext context) {
1186 // System.out.println(context);
1187 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
1188 final ProofCheckException ex = new ProofCheckException(code, msg, context);
1189 exceptions.add(ex);
1190 }
1191
1192 /**
1193 * Add new {@link ProofCheckException} to exception list.
1194 *
1195 * @param code Error code.
1196 * @param msg Error message.
1197 * @param context Error context.
1198 * @param referenceContext Reference context.
1199 */
1200 private void handleProofCheckException(final int code, final String msg,
1201 final ModuleContext context, final ModuleContext referenceContext) {
1202 // System.out.println(context);
1203 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
1204 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
1205 referenceContext);
1206 exceptions.add(ex);
1207 }
1208
1209 /**
1210 * Set location information where are we within the original module.
1211 *
1212 * @param locationWithinModule Location within module.
1213 */
1214 protected void setLocationWithinModule(final String locationWithinModule) {
1215 getCurrentContext().setLocationWithinModule(locationWithinModule);
1216 // FIXME 20110616 m31: use within JUnit test
1217 // try {
1218 // System.out.println("testing context " + locationWithinModule);
1219 // QedeqBo qedeq = KernelContext.getInstance().getQedeqBo(getCurrentContext().getModuleLocation());
1220 // DynamicGetter.get(qedeq.getQedeq(), getCurrentContext().getLocationWithinModule());
1221 // } catch (RuntimeException e) {
1222 // System.err.println(getCurrentContext().getLocationWithinModule());
1223 // throw e;
1224 // } catch (IllegalAccessException e) {
1225 // throw new RuntimeException(e);
1226 // } catch (InvocationTargetException e) {
1227 // throw new RuntimeException(e);
1228 // }
1229
1230 }
1231
1232 /**
1233 * Get current context within original.
1234 *
1235 * @return Current context.
1236 */
1237 protected final ModuleContext getCurrentContext() {
1238 return currentContext;
1239 }
1240
1241 public boolean isProvedFormula(final String reference) {
1242 if (label2line.containsKey(reference)) {
1243 return lineProved[((Integer) label2line.get(reference)).intValue()];
1244 }
1245 return resolver.isProvedFormula(reference);
1246 }
1247
1248 public Element getNormalizedReferenceFormula(final String reference) {
1249 // System.out.println("looking for " + reference);
1250 if (label2line.containsKey(reference)) {
1251 // System.out.println("found in local " + reference);
1252 return getNormalizedProofLine((Integer) label2line.get(reference));
1253 }
1254 // System.out.println("not found in local " + reference);
1255 return resolver.getNormalizedReferenceFormula(reference);
1256 }
1257
1258 public Element getNormalizedFormula(final Element element) {
1259 return resolver.getNormalizedFormula(element);
1260 }
1261
1262 public boolean isLocalProofLineReference(final String reference) {
1263 if (label2line.containsKey(reference)) {
1264 return true;
1265 }
1266 return resolver.isLocalProofLineReference(reference);
1267 }
1268
1269 public Element getNormalizedLocalProofLineReference(final String reference) {
1270 // System.out.println("\t resolver looks for " + reference);
1271 if (label2line.containsKey(reference)) {
1272 // System.out.println("\t resolver found local " + reference);
1273 return getNormalizedProofLine((Integer) label2line.get(reference));
1274 }
1275 // System.out.println("\t resolver asks super resolver for " + reference);
1276 final Element result = resolver.getNormalizedLocalProofLineReference(reference);
1277 // if (result == null) {
1278 // System.out.println("\t super resolver didn't find " + reference);
1279 // } else {
1280 // System.out.println("\t super resolver found " + reference);
1281 // }
1282 return result;
1283 }
1284
1285 public ModuleContext getReferenceContext(final String reference) {
1286 if (label2line.containsKey(reference)) {
1287 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
1288 moduleContext.getLocationWithinModule() + ".get("
1289 + ((Integer) label2line.get(reference)
1290 + ").getLabel()"));
1291 return lc;
1292 }
1293 return resolver.getReferenceContext(reference);
1294 }
1295
1296 }
|