0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2011, 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 return checkProof(con, formula, proof, checker, moduleContext, resolver);
0126 }
0127
0128 private LogicalCheckExceptionList checkProof(final ElementList conditions, final Element formula,
0129 final FormalProofLineList proof,
0130 final RuleChecker checker,
0131 final ModuleContext moduleContext,
0132 final ReferenceResolver resolver) {
0133 this.conditions = conditions;
0134 this.proof = proof;
0135 this.checker = checker;
0136 this.resolver = resolver;
0137 this.moduleContext = moduleContext;
0138 // use copy constructor for changing context
0139 currentContext = new ModuleContext(moduleContext);
0140 exceptions = new LogicalCheckExceptionList();
0141 final String context = moduleContext.getLocationWithinModule();
0142 lineProved = new boolean[proof.size()];
0143 label2line = new HashMap();
0144 for (int i = 0; i < proof.size(); i++) {
0145 boolean ok = true;
0146 setLocationWithinModule(context + ".get(" + i + ")");
0147 final FormalProofLine line = proof.get(i);
0148 if (line == null || line.getFormula() == null
0149 || line.getFormula().getElement() == null) {
0150 ok = false;
0151 handleProofCheckException(
0152 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
0153 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
0154 getCurrentContext());
0155 continue;
0156 }
0157 setLocationWithinModule(context + ".get(" + i + ").getReason()");
0158 final Reason reason = line.getReason();
0159 if (reason == null) {
0160 ok = false;
0161 handleProofCheckException(
0162 BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
0163 BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
0164 getCurrentContext());
0165 continue;
0166 }
0167 if (line.getLabel() != null && line.getLabel().length() > 0) {
0168 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
0169 addLocalLineLabel(i, line.getLabel());
0170 }
0171
0172 // check if the formula together with the conditions is well formed
0173 if (hasConditions()) {
0174 setLocationWithinModule(context + ".get(" + i + ").getFormula.getElement()");
0175 ElementList full = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
0176 if (conditions.size() > 1) {
0177 full.add(conditions);
0178 } else {
0179 full.add(conditions.getElement(0));
0180 }
0181 full.add(line.getFormula().getElement());
0182 FormulaChecker checkWf = new FormulaCheckerImpl(); // TODO 20110612 m31: use factory?
0183 final LogicalCheckExceptionList list = checkWf.checkFormula(full, getCurrentContext());
0184 if (list.size() > 0) {
0185 ok = false;
0186 handleProofCheckException(
0187 BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_CODE,
0188 BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT
0189 + list.get(0).getMessage(),
0190 getCurrentContext());
0191 continue;
0192 }
0193 }
0194
0195 // check if only defined rules are used
0196 // TODO 20110316 m31: this is a dirty trick to get the context of the reason
0197 // perhaps we can solve this more elegantly?
0198 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
0199 if (getReason.endsWith("Vo")) {
0200 getReason = getReason.substring(0, getReason.length() - 2) + "()";
0201 setLocationWithinModule(context + ".get(" + i + ").getReason()"
0202 + getReason);
0203 // System.out.println(getCurrentContext());
0204 }
0205 if (reason instanceof Add) {
0206 ok = check((Add) reason, i, line.getFormula().getElement());
0207 } else if (reason instanceof Rename) {
0208 ok = check((Rename) reason, i, line.getFormula().getElement());
0209 } else if (reason instanceof ModusPonens) {
0210 ok = check((ModusPonens) reason, i, line.getFormula().getElement());
0211 } else if (reason instanceof SubstFree) {
0212 ok = check((SubstFree) reason, i, line.getFormula().getElement());
0213 } else if (reason instanceof SubstPred) {
0214 ok = check((SubstPred) reason, i, line.getFormula().getElement());
0215 } else if (reason instanceof SubstFunc) {
0216 ok = check((SubstFunc) reason, i, line.getFormula().getElement());
0217 } else if (reason instanceof Universal) {
0218 ok = check((Universal) reason, i, line.getFormula().getElement());
0219 } else if (reason instanceof Existential) {
0220 ok = check((Existential) reason, i, line.getFormula().getElement());
0221 } else if (reason instanceof ConditionalProof) {
0222 setLocationWithinModule(context + ".get(" + i + ")");
0223 ok = check((ConditionalProof) reason, i, line.getFormula().getElement());
0224 } else {
0225 ok = false;
0226 handleProofCheckException(
0227 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
0228 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
0229 + reason.getName(),
0230 getCurrentContext());
0231 }
0232 lineProved[i] = ok;
0233 // check if last proof line is identical with proposition formula
0234 if (i == proof.size() - 1) {
0235 if (!formula.equals(line.getFormula().getElement())) {
0236 handleProofCheckException(
0237 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
0238 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT,
0239 getModuleContextOfProofLineFormula(i));
0240 }
0241 }
0242 }
0243 return exceptions;
0244 }
0245
0246 private void addLocalLineLabel(final int i, final String label) {
0247 if (label != null && label.length() > 0) {
0248 final Integer n = (Integer) label2line.get(label);
0249 if (n != null) {
0250 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
0251 moduleContext.getLocationWithinModule() + ".get("
0252 + ((Integer) label2line.get(label)
0253 + ").getLabel()"));
0254 handleProofCheckException(
0255 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
0256 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
0257 + label,
0258 getCurrentContext(),
0259 lc);
0260 } else {
0261 if (isLocalProofLineReference(label)) {
0262 handleProofCheckException(
0263 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
0264 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
0265 + label,
0266 getCurrentContext(),
0267 resolver.getReferenceContext(label));
0268 // System.out.println("we hava label already: " + label);
0269 // ProofFinderUtility.println(getNormalizedLocalProofLineReference(label));
0270 }
0271 }
0272 // System.out.println("adding label: " + label);
0273 label2line.put(label, new Integer(i));
0274 }
0275 }
0276
0277 private boolean check(final Add add, final int i, final Element element) {
0278 final String context = currentContext.getLocationWithinModule();
0279 boolean ok = true;
0280 if (add.getReference() == null) {
0281 ok = false;
0282 setLocationWithinModule(context + ".getReference()");
0283 handleProofCheckException(
0284 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
0285 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
0286 getCurrentContext());
0287 return ok;
0288 }
0289 if (!resolver.isProvedFormula(add.getReference())) {
0290 ok = false;
0291 setLocationWithinModule(context + ".getReference()");
0292 handleProofCheckException(
0293 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
0294 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
0295 + add.getReference(),
0296 getCurrentContext());
0297 return ok;
0298 }
0299 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
0300 final Element current = resolver.getNormalizedFormula(element);
0301 if (!EqualsUtility.equals(expected, current)) {
0302 ok = false;
0303 handleProofCheckException(
0304 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0305 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0306 + add.getReference(),
0307 getDiffModuleContextOfProofLineFormula(i, expected));
0308 return ok;
0309 }
0310 final RuleKey defined = checker.getRule(add.getName());
0311 if (defined == null) {
0312 ok = false;
0313 handleProofCheckException(
0314 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0315 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0316 + add.getName(),
0317 getCurrentContext());
0318 return ok;
0319 } else if (!supported.contains(defined.getVersion())) {
0320 ok = false;
0321 handleProofCheckException(
0322 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0323 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0324 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0325 getCurrentContext());
0326 return ok;
0327 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0328 ok = false;
0329 handleProofCheckException(
0330 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0331 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0332 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0333 getCurrentContext());
0334 return ok;
0335 }
0336 return ok;
0337 }
0338
0339 private boolean check(final Rename rename, final int i, final Element element) {
0340 final String context = currentContext.getLocationWithinModule();
0341 boolean ok = true;
0342 final Element f = getNormalizedLocalProofLineReference(rename.getReference());
0343 if (f == null) {
0344 ok = false;
0345 setLocationWithinModule(context + ".getReference()");
0346 handleProofCheckException(
0347 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0348 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0349 + rename.getReference(),
0350 getCurrentContext());
0351 } else {
0352 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
0353 rename.getOriginalSubjectVariable(),
0354 rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
0355 new Enumerator());
0356 final Element current = resolver.getNormalizedFormula(element);
0357 if (!EqualsUtility.equals(expected, current)) {
0358 ok = false;
0359 handleProofCheckException(
0360 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0361 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0362 + rename.getReference(),
0363 getDiffModuleContextOfProofLineFormula(i, expected));
0364 } else {
0365 ok = true;
0366 }
0367 }
0368 final RuleKey defined = checker.getRule(rename.getName());
0369 if (defined == null) {
0370 ok = false;
0371 handleProofCheckException(
0372 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0373 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0374 + rename.getName(),
0375 getCurrentContext());
0376 return ok;
0377 } else if (!supported.contains(defined.getVersion())) {
0378 ok = false;
0379 handleProofCheckException(
0380 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0381 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0382 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0383 getCurrentContext());
0384 return ok;
0385 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0386 ok = false;
0387 handleProofCheckException(
0388 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0389 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0390 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0391 getCurrentContext());
0392 return ok;
0393 }
0394 return ok;
0395 }
0396
0397 private boolean check(final SubstFree substFree, final int i, final Element element) {
0398 final String context = currentContext.getLocationWithinModule();
0399 boolean ok = true;
0400 final Element f = getNormalizedLocalProofLineReference(substFree.getReference());
0401 if (f == null) {
0402 ok = false;
0403 setLocationWithinModule(context + ".getReference()");
0404 handleProofCheckException(
0405 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0406 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0407 + substFree.getReference(),
0408 getCurrentContext());
0409 } else {
0410 final Element current = resolver.getNormalizedFormula(element);
0411 final Element expected = f.replace(substFree.getSubjectVariable(),
0412 resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
0413 if (!EqualsUtility.equals(current, expected)) {
0414 ok = false;
0415 handleProofCheckException(
0416 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0417 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0418 + substFree.getReference(),
0419 getDiffModuleContextOfProofLineFormula(i, expected));
0420 return ok;
0421 }
0422 }
0423 // check precondition: subject variable doesn't occur in a precondition
0424 if (FormulaUtility.containsOperatorVariable(conditions, substFree.getSubjectVariable())) {
0425 ok = false;
0426 setLocationWithinModule(context + ".getSubstituteFormula()");
0427 handleProofCheckException(
0428 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
0429 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
0430 getCurrentContext());
0431 return ok;
0432 }
0433 final RuleKey defined = checker.getRule(substFree.getName());
0434 if (defined == null) {
0435 ok = false;
0436 handleProofCheckException(
0437 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0438 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0439 + substFree.getName(),
0440 getCurrentContext());
0441 return ok;
0442 } else if (!supported.contains(defined.getVersion())) {
0443 ok = false;
0444 handleProofCheckException(
0445 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0446 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0447 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0448 getCurrentContext());
0449 return ok;
0450 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0451 ok = false;
0452 handleProofCheckException(
0453 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0454 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0455 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0456 getCurrentContext());
0457 return ok;
0458 }
0459 return ok;
0460 }
0461
0462 private boolean check(final SubstPred substPred, final int i, final Element element) {
0463 final String context = currentContext.getLocationWithinModule();
0464 boolean ok = true;
0465 final Element alpha = getNormalizedLocalProofLineReference(substPred.getReference());
0466 if (alpha == null) {
0467 ok = false;
0468 setLocationWithinModule(context + ".getReference()");
0469 handleProofCheckException(
0470 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0471 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0472 + substPred.getReference(),
0473 getCurrentContext());
0474 return ok;
0475 }
0476 final Element current = resolver.getNormalizedFormula(element);
0477 if (substPred.getSubstituteFormula() == null) {
0478 ok = false;
0479 handleProofCheckException(
0480 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
0481 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
0482 getCurrentContext());
0483 return ok;
0484 }
0485 final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
0486 final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
0487 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
0488 if (!EqualsUtility.equals(current, expected)) {
0489 ok = false;
0490 handleProofCheckException(
0491 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0492 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0493 + substPred.getReference(),
0494 getDiffModuleContextOfProofLineFormula(i, expected));
0495 return ok;
0496 }
0497 // check precondition: predicate variable p must have n pairwise different free subject
0498 // variables as arguments
0499 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
0500 if (predFree.size() != p.getList().size() - 1) {
0501 ok = false;
0502 setLocationWithinModule(context + ".getPredicateVariable()");
0503 handleProofCheckException(
0504 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0505 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0506 getDiffModuleContextOfProofLineFormula(i, expected));
0507 return ok;
0508 }
0509 for (int j = 1; j < p.getList().size(); j++) {
0510 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
0511 ok = false;
0512 setLocationWithinModule(context + ".getPredicateVariable()");
0513 handleProofCheckException(
0514 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0515 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0516 getCurrentContext());
0517 return ok;
0518 }
0519 }
0520 // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
0521 // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
0522 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
0523 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
0524 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
0525 ok = false;
0526 setLocationWithinModule(context + ".getSubstituteFormula()");
0527 handleProofCheckException(
0528 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
0529 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
0530 getCurrentContext());
0531 return ok;
0532 }
0533 // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
0534 // no bound variable of $\beta(x_1, \ldots, x_n)$
0535 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
0536 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
0537 ok = false;
0538 setLocationWithinModule(context + ".getSubstituteFormula()");
0539 handleProofCheckException(
0540 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
0541 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
0542 getCurrentContext());
0543 return ok;
0544 }
0545 // check precondition: $\sigma(...)$ dosn't occur in a precondition
0546 if (FormulaUtility.containsOperatorVariable(conditions, p)) {
0547 ok = false;
0548 setLocationWithinModule(context + ".getPredicateVariable()");
0549 handleProofCheckException(
0550 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
0551 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
0552 getCurrentContext());
0553 return ok;
0554 }
0555 // check precondition: resulting formula is well formed was already done by well formed
0556 // checker
0557
0558 final RuleKey defined = checker.getRule(substPred.getName());
0559 if (defined == null) {
0560 ok = false;
0561 handleProofCheckException(
0562 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0563 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0564 + substPred.getName(),
0565 getCurrentContext());
0566 return ok;
0567 } else if (!supported.contains(defined.getVersion())) {
0568 ok = false;
0569 handleProofCheckException(
0570 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0571 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0572 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0573 getCurrentContext());
0574 return ok;
0575 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0576 ok = false;
0577 handleProofCheckException(
0578 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0579 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0580 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0581 getCurrentContext());
0582 return ok;
0583 }
0584 return ok;
0585 }
0586
0587 private boolean check(final SubstFunc substFunc, final int i, final Element element) {
0588 final String context = currentContext.getLocationWithinModule();
0589 boolean ok = true;
0590 final Element alpha = getNormalizedLocalProofLineReference(substFunc.getReference());
0591 if (alpha == null) {
0592 ok = false;
0593 setLocationWithinModule(context + ".getReference()");
0594 handleProofCheckException(
0595 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0596 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0597 + substFunc.getReference(),
0598 getCurrentContext());
0599 return ok;
0600 }
0601 final Element current = resolver.getNormalizedFormula(element);
0602 if (substFunc.getSubstituteTerm() == null) {
0603 ok = false;
0604 handleProofCheckException(
0605 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
0606 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
0607 getCurrentContext());
0608 return ok;
0609 }
0610 final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
0611 final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
0612 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
0613 if (!EqualsUtility.equals(current, expected)) {
0614 ok = false;
0615 handleProofCheckException(
0616 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0617 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0618 + substFunc.getReference(),
0619 getDiffModuleContextOfProofLineFormula(i, expected));
0620 return ok;
0621 }
0622 // check precondition: function variable $\sigma$ must have n pairwise different free
0623 // subject variables as arguments
0624 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
0625 if (funcFree.size() != sigma.getList().size() - 1) {
0626 ok = false;
0627 setLocationWithinModule(context + ".getPredicateVariable()");
0628 handleProofCheckException(
0629 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0630 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0631 getDiffModuleContextOfProofLineFormula(i, expected));
0632 return ok;
0633 }
0634 for (int j = 1; j < sigma.getList().size(); j++) {
0635 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
0636 ok = false;
0637 setLocationWithinModule(context + ".getPredicateVariable()");
0638 handleProofCheckException(
0639 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
0640 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
0641 getCurrentContext());
0642 return ok;
0643 }
0644 }
0645 // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
0646 // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
0647 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
0648 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
0649 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
0650 ok = false;
0651 setLocationWithinModule(context + ".getSubstituteFormula()");
0652 handleProofCheckException(
0653 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
0654 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
0655 getCurrentContext());
0656 return ok;
0657 }
0658 // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
0659 // contains no bound variable of $\tau(x_1, \ldots, x_n)$
0660 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
0661 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
0662 ok = false;
0663 setLocationWithinModule(context + ".getSubstituteFormula()");
0664 handleProofCheckException(
0665 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
0666 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
0667 getCurrentContext());
0668 return ok;
0669 }
0670 // check precondition: $\sigma(...)$ dosn't occur in a precondition
0671 if (FormulaUtility.containsOperatorVariable(conditions, sigma)) {
0672 ok = false;
0673 setLocationWithinModule(context + ".getPredicateVariable()");
0674 handleProofCheckException(
0675 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
0676 BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
0677 getCurrentContext());
0678 return ok;
0679 }
0680 // check precondition: resulting formula is well formed was already done by well formed
0681 // checker
0682
0683 final RuleKey defined = checker.getRule(substFunc.getName());
0684 if (defined == null) {
0685 ok = false;
0686 handleProofCheckException(
0687 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0688 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0689 + substFunc.getName(),
0690 getCurrentContext());
0691 return ok;
0692 } else if (!supported.contains(defined.getVersion())) {
0693 ok = false;
0694 handleProofCheckException(
0695 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0696 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0697 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0698 getCurrentContext());
0699 return ok;
0700 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0701 ok = false;
0702 handleProofCheckException(
0703 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0704 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0705 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0706 getCurrentContext());
0707 return ok;
0708 }
0709 return ok;
0710 }
0711
0712 private boolean check(final ModusPonens mp, final int i, final Element element) {
0713 final String context = currentContext.getLocationWithinModule();
0714 boolean ok = true;
0715 final Element f1 = getNormalizedLocalProofLineReference(mp.getReference1());
0716 if (f1 == null) {
0717 ok = false;
0718 setLocationWithinModule(context + ".getReference1()");
0719 handleProofCheckException(
0720 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0721 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0722 + mp.getReference1(),
0723 getCurrentContext());
0724 }
0725 final Element f2 = getNormalizedLocalProofLineReference(mp.getReference2());
0726 if (f2 == null) {
0727 ok = false;
0728 setLocationWithinModule(context + ".getReference2()");
0729 handleProofCheckException(
0730 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0731 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0732 + mp.getReference2(),
0733 getCurrentContext());
0734 }
0735 if (ok) {
0736 final Element current = getNormalizedFormula(element);
0737 if (!FormulaUtility.isImplication(f1)) {
0738 ok = false;
0739 setLocationWithinModule(context + ".getReference1()");
0740 handleProofCheckException(
0741 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
0742 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
0743 + mp.getReference1(),
0744 getCurrentContext());
0745 } else if (!f2.equals(f1.getList().getElement(0))) {
0746 ok = false;
0747 setLocationWithinModule(context + ".getReference2()");
0748 handleProofCheckException(
0749 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
0750 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
0751 + mp.getReference2(),
0752 getCurrentContext(),
0753 resolver.getReferenceContext(mp.getReference1()));
0754 } else if (!current.equals(f1.getList().getElement(1))) {
0755 ok = false;
0756 setLocationWithinModule(context + ".getReference1()");
0757 handleProofCheckException(
0758 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
0759 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
0760 + mp.getReference1(),
0761 getCurrentContext(),
0762 resolver.getReferenceContext(mp.getReference1()));
0763 } else {
0764 ok = true;
0765 }
0766 }
0767 final RuleKey defined = checker.getRule(mp.getName());
0768 if (defined == null) {
0769 ok = false;
0770 handleProofCheckException(
0771 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0772 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0773 + mp.getName(),
0774 getCurrentContext());
0775 return ok;
0776 } else if (!supported.contains(defined.getVersion())) {
0777 ok = false;
0778 handleProofCheckException(
0779 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0780 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0781 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0782 getCurrentContext());
0783 return ok;
0784 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0785 ok = false;
0786 handleProofCheckException(
0787 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0788 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0789 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0790 getCurrentContext());
0791 return ok;
0792 }
0793 return ok;
0794 }
0795
0796 private boolean check(final Universal universal, final int i, final Element element) {
0797 final String context = currentContext.getLocationWithinModule();
0798 boolean ok = true;
0799 final Element reference = getNormalizedLocalProofLineReference(universal.getReference());
0800 if (reference == null) {
0801 ok = false;
0802 setLocationWithinModule(context + ".getReference()");
0803 handleProofCheckException(
0804 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0805 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0806 + universal.getReference(),
0807 getCurrentContext());
0808 // } else if (!lineProved[n.intValue()]) {
0809 // ok = false;
0810 // setLocationWithinModule(context + ".getReference()");
0811 // handleProofCheckException(
0812 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
0813 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
0814 // + universal.getReference(),
0815 // getCurrentContext());
0816 } else {
0817 final Element current = getNormalizedFormula(element);
0818 if (!FormulaUtility.isImplication(current)) {
0819 ok = false;
0820 setLocationWithinModule(context + ".getReference()");
0821 handleProofCheckException(
0822 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
0823 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
0824 + universal.getReference(),
0825 getCurrentContext());
0826 return ok;
0827 }
0828 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
0829 ok = false;
0830 setLocationWithinModule(context + ".getSubjectVariable()");
0831 handleProofCheckException(
0832 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
0833 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
0834 getCurrentContext());
0835 return ok;
0836 }
0837 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
0838 expected.add(reference.getList().getElement(0));
0839 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
0840 uni.add(universal.getSubjectVariable());
0841 uni.add(reference.getList().getElement(1));
0842 expected.add(uni);
0843 // System.out.print("Expected: ");
0844 // ProofFinderUtility.println(expected);
0845 // System.out.print("Current : ");
0846 // ProofFinderUtility.println(current);
0847 if (!EqualsUtility.equals(current, expected)) {
0848 ok = false;
0849 handleProofCheckException(
0850 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0851 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0852 + universal.getReference(),
0853 getDiffModuleContextOfProofLineFormula(i, expected));
0854 return ok;
0855 }
0856 }
0857 final RuleKey defined = checker.getRule(universal.getName());
0858 if (defined == null) {
0859 ok = false;
0860 handleProofCheckException(
0861 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0862 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0863 + universal.getName(),
0864 getCurrentContext());
0865 return ok;
0866 } else if (!supported.contains(defined.getVersion())) {
0867 ok = false;
0868 handleProofCheckException(
0869 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0870 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0871 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0872 getCurrentContext());
0873 return ok;
0874 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0875 ok = false;
0876 handleProofCheckException(
0877 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0878 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0879 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0880 getCurrentContext());
0881 return ok;
0882 }
0883 return ok;
0884 }
0885
0886 private boolean check(final Existential existential, final int i, final Element element) {
0887 final String context = currentContext.getLocationWithinModule();
0888 boolean ok = true;
0889 final Element reference = getNormalizedLocalProofLineReference(existential.getReference());
0890 if (reference == null) {
0891 ok = false;
0892 setLocationWithinModule(context + ".getReference()");
0893 handleProofCheckException(
0894 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
0895 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
0896 + existential.getReference(),
0897 getCurrentContext());
0898 // } else if (!lineProved[n.intValue()]) {
0899 // ok = false;
0900 // setLocationWithinModule(context + ".getReference()");
0901 // handleProofCheckException(
0902 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
0903 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
0904 // + existential.getReference(),
0905 // getCurrentContext());
0906 } else {
0907 final Element current = getNormalizedFormula(element);
0908 if (!FormulaUtility.isImplication(current)) {
0909 ok = false;
0910 setLocationWithinModule(context + ".getReference()");
0911 handleProofCheckException(
0912 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
0913 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
0914 + existential.getReference(),
0915 getCurrentContext());
0916 return ok;
0917 }
0918 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
0919 ok = false;
0920 setLocationWithinModule(context + ".getSubjectVariable()");
0921 handleProofCheckException(
0922 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
0923 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
0924 getCurrentContext());
0925 return ok;
0926 }
0927 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
0928 final ElementList exi = new DefaultElementList(
0929 Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
0930 exi.add(existential.getSubjectVariable());
0931 exi.add(reference.getList().getElement(0));
0932 expected.add(exi);
0933 expected.add((reference.getList().getElement(1)));
0934 if (!EqualsUtility.equals(current, expected)) {
0935 ok = false;
0936 handleProofCheckException(
0937 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
0938 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
0939 + existential.getReference(),
0940 getDiffModuleContextOfProofLineFormula(i, expected));
0941 return ok;
0942 }
0943 }
0944 final RuleKey defined = checker.getRule(existential.getName());
0945 if (defined == null) {
0946 ok = false;
0947 handleProofCheckException(
0948 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
0949 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
0950 + existential.getName(),
0951 getCurrentContext());
0952 return ok;
0953 } else if (!supported.contains(defined.getVersion())) {
0954 ok = false;
0955 handleProofCheckException(
0956 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
0957 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
0958 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
0959 getCurrentContext());
0960 return ok;
0961 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
0962 ok = false;
0963 handleProofCheckException(
0964 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
0965 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
0966 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
0967 getCurrentContext());
0968 return ok;
0969 }
0970 return ok;
0971 }
0972
0973 private boolean check(final ConditionalProof cp, final int i, final Element element) {
0974 final ModuleAddress address = currentContext.getModuleLocation();
0975 final String context = currentContext.getLocationWithinModule();
0976 // System.out.println(getCurrentContext());
0977 boolean ok = true;
0978 if (cp.getHypothesis() == null || cp.getHypothesis().getFormula() == null
0979 || cp.getHypothesis().getFormula().getElement() == null) {
0980 ok = false;
0981 setLocationWithinModule(context + ".getHypothesis()");
0982 handleProofCheckException(
0983 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
0984 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
0985 getCurrentContext());
0986 return ok;
0987 }
0988 if (cp.getFormalProofLineList() == null || cp.getFormalProofLineList().size() <= 0) {
0989 ok = false;
0990 setLocationWithinModule(context + ".getFormalProofLineList()");
0991 handleProofCheckException(
0992 BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE,
0993 BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT,
0994 getCurrentContext());
0995 return ok;
0996 }
0997 final ReferenceResolver newResolver = new ReferenceResolver() {
0998
0999 public Element getNormalizedFormula(final Element formula) {
1000 return ProofChecker2Impl.this.getNormalizedFormula(formula);
1001 }
1002
1003 public Element getNormalizedReferenceFormula(final String reference) {
1004 // System.out.println("Looking for " + reference);
1005 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1006 return resolver.getNormalizedFormula(cp.getHypothesis().getFormula()
1007 .getElement());
1008 }
1009 return ProofChecker2Impl.this.getNormalizedReferenceFormula(reference);
1010 }
1011
1012 public boolean isProvedFormula(final String reference) {
1013 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1014 return true;
1015 }
1016 return ProofChecker2Impl.this.isProvedFormula(reference);
1017 }
1018
1019 public boolean isLocalProofLineReference(final String reference) {
1020 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1021 return true;
1022 }
1023 return ProofChecker2Impl.this.isLocalProofLineReference(reference);
1024 }
1025
1026 public ModuleContext getReferenceContext(final String reference) {
1027 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1028 return new ModuleContext(address, context
1029 + ".getHypothesis().getLabel()");
1030 }
1031 return ProofChecker2Impl.this.getReferenceContext(reference);
1032 }
1033
1034 public Element getNormalizedLocalProofLineReference(final String reference) {
1035 // System.out.println("\t resolver looks for " + reference);
1036 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1037 // System.out.println("\t resolver found local " + reference);
1038 return resolver.getNormalizedFormula(
1039 cp.getHypothesis().getFormula().getElement());
1040 }
1041 return ProofChecker2Impl.this.getNormalizedLocalProofLineReference(reference);
1042 }
1043
1044 };
1045 final int last = cp.getFormalProofLineList().size() - 1;
1046 setLocationWithinModule(context + ".getFormalProofLineList().get(" + last + ")");
1047 final FormalProofLine line = cp.getFormalProofLineList().get(last);
1048 if (line == null || line.getFormula() == null
1049 || line.getFormula().getElement() == null) {
1050 ok = false;
1051 handleProofCheckException(
1052 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1053 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1054 getCurrentContext());
1055 return ok;
1056 }
1057 final Element lastFormula = resolver.getNormalizedFormula(line.getFormula().getElement());
1058 final ElementList newConditions = (ElementList) conditions.copy();
1059 // add hypothesis as new condition
1060 newConditions.add(cp.getHypothesis().getFormula().getElement());
1061 setLocationWithinModule(context + ".getFormalProofLineList()");
1062 final LogicalCheckExceptionList eList = (new ProofChecker2Impl()).checkProof(
1063 newConditions, lastFormula, cp.getFormalProofLineList(), checker, getCurrentContext(),
1064 newResolver);
1065 exceptions.add(eList);
1066 ok = eList.size() == 0;
1067 setLocationWithinModule(context + ".getConclusion()");
1068 if (cp.getConclusion() == null || cp.getConclusion().getFormula() == null
1069 || cp.getConclusion().getFormula().getElement() == null) {
1070 ok = false;
1071 handleProofCheckException(
1072 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1073 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1074 getCurrentContext());
1075 return ok;
1076 }
1077 final Element c = resolver.getNormalizedFormula(cp.getConclusion().getFormula().getElement());
1078 setLocationWithinModule(context + ".getConclusion().getFormula().getElement()");
1079 if (!FormulaUtility.isImplication(c)) {
1080 ok = false;
1081 handleProofCheckException(
1082 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
1083 BasicProofErrors.IMPLICATION_EXPECTED_TEXT,
1084 getCurrentContext());
1085 return ok;
1086 }
1087 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
1088 expected.add(cp.getHypothesis().getFormula().getElement());
1089 expected.add(lastFormula);
1090 // System.out.println("expected: ");
1091 // ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
1092 if (!EqualsUtility.equals(cp.getConclusion().getFormula().getElement(), expected)) {
1093 // System.out.println("found: ");
1094 // ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
1095 ok = false;
1096 handleProofCheckException(
1097 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_CODE,
1098 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_TEXT,
1099 getDiffModuleContextOfProofLineFormula(i, expected));
1100 return ok;
1101 }
1102 final RuleKey defined = checker.getRule(cp.getName());
1103 if (defined == null) {
1104 ok = false;
1105 handleProofCheckException(
1106 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
1107 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
1108 + cp.getName(),
1109 getCurrentContext());
1110 return ok;
1111 } else if (!supported.contains(defined.getVersion())) {
1112 ok = false;
1113 handleProofCheckException(
1114 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
1115 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
1116 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
1117 getCurrentContext());
1118 return ok;
1119 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
1120 ok = false;
1121 handleProofCheckException(
1122 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
1123 BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
1124 + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
1125 getCurrentContext());
1126 return ok;
1127 }
1128 return ok;
1129 }
1130
1131 private ModuleContext getModuleContextOfProofLineFormula(final int i) {
1132 if (proof.get(i) instanceof ConditionalProof) {
1133 return new ModuleContext(moduleContext.getModuleLocation(),
1134 moduleContext.getLocationWithinModule() + ".get(" + i
1135 + ").getConclusion().getFormula().getElement()");
1136 }
1137 return new ModuleContext(moduleContext.getModuleLocation(),
1138 moduleContext.getLocationWithinModule() + ".get(" + i
1139 + ").getFormula().getElement()");
1140 }
1141
1142 private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
1143 final Element expected) {
1144 final String diff = FormulaUtility.getDifferenceLocation(
1145 proof.get(i).getFormula().getElement(), expected);
1146 if (proof.get(i) instanceof ConditionalProof) {
1147 return new ModuleContext(moduleContext.getModuleLocation(),
1148 moduleContext.getLocationWithinModule() + ".get(" + i
1149 + ").getConclusion().getFormula().getElement()" + diff);
1150 }
1151 return new ModuleContext(moduleContext.getModuleLocation(),
1152 moduleContext.getLocationWithinModule() + ".get(" + i
1153 + ").getFormula().getElement()" + diff);
1154 }
1155
1156 /**
1157 * Have we any conditions. If yes we are within an conditional proof argument.
1158 *
1159 * @return Do we have conditions?
1160 */
1161 private boolean hasConditions() {
1162 return conditions.size() > 0;
1163 }
1164
1165 private Element getNormalizedProofLine(final Integer n) {
1166 if (n == null) {
1167 return null;
1168 }
1169 int i = n.intValue();
1170 if (i < 0 || i >= proof.size()) {
1171 return null;
1172 }
1173 return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
1174 }
1175
1176 /**
1177 * Add new {@link ProofCheckException} to exception list.
1178 *
1179 * @param code Error code.
1180 * @param msg Error message.
1181 * @param context Error context.
1182 */
1183 private void handleProofCheckException(final int code, final String msg,
1184 final ModuleContext context) {
1185 // System.out.println(context);
1186 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
1187 final ProofCheckException ex = new ProofCheckException(code, msg, context);
1188 exceptions.add(ex);
1189 }
1190
1191 /**
1192 * Add new {@link ProofCheckException} to exception list.
1193 *
1194 * @param code Error code.
1195 * @param msg Error message.
1196 * @param context Error context.
1197 * @param referenceContext Reference context.
1198 */
1199 private void handleProofCheckException(final int code, final String msg,
1200 final ModuleContext context, final ModuleContext referenceContext) {
1201 // System.out.println(context);
1202 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
1203 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
1204 referenceContext);
1205 exceptions.add(ex);
1206 }
1207
1208 /**
1209 * Set location information where are we within the original module.
1210 *
1211 * @param locationWithinModule Location within module.
1212 */
1213 protected void setLocationWithinModule(final String locationWithinModule) {
1214 getCurrentContext().setLocationWithinModule(locationWithinModule);
1215 // FIXME 20110616 m31: use within JUnit test
1216 // try {
1217 // System.out.println("testing context " + locationWithinModule);
1218 // QedeqBo qedeq = KernelContext.getInstance().getQedeqBo(getCurrentContext().getModuleLocation());
1219 // DynamicGetter.get(qedeq.getQedeq(), getCurrentContext().getLocationWithinModule());
1220 // } catch (RuntimeException e) {
1221 // System.err.println(getCurrentContext().getLocationWithinModule());
1222 // throw e;
1223 // } catch (IllegalAccessException e) {
1224 // throw new RuntimeException(e);
1225 // } catch (InvocationTargetException e) {
1226 // throw new RuntimeException(e);
1227 // }
1228
1229 }
1230
1231 /**
1232 * Get current context within original.
1233 *
1234 * @return Current context.
1235 */
1236 protected final ModuleContext getCurrentContext() {
1237 return currentContext;
1238 }
1239
1240 public boolean isProvedFormula(final String reference) {
1241 if (label2line.containsKey(reference)) {
1242 return lineProved[((Integer) label2line.get(reference)).intValue()];
1243 }
1244 return resolver.isProvedFormula(reference);
1245 }
1246
1247 public Element getNormalizedReferenceFormula(final String reference) {
1248 // System.out.println("looking for " + reference);
1249 if (label2line.containsKey(reference)) {
1250 // System.out.println("found in local " + reference);
1251 return getNormalizedProofLine((Integer) label2line.get(reference));
1252 }
1253 // System.out.println("not found in local " + reference);
1254 return resolver.getNormalizedReferenceFormula(reference);
1255 }
1256
1257 public Element getNormalizedFormula(final Element element) {
1258 return resolver.getNormalizedFormula(element);
1259 }
1260
1261 public boolean isLocalProofLineReference(final String reference) {
1262 if (label2line.containsKey(reference)) {
1263 return true;
1264 }
1265 return resolver.isLocalProofLineReference(reference);
1266 }
1267
1268 public Element getNormalizedLocalProofLineReference(final String reference) {
1269 // System.out.println("\t resolver looks for " + reference);
1270 if (label2line.containsKey(reference)) {
1271 // System.out.println("\t resolver found local " + reference);
1272 return getNormalizedProofLine((Integer) label2line.get(reference));
1273 }
1274 // System.out.println("\t resolver asks super resolver for " + reference);
1275 final Element result = resolver.getNormalizedLocalProofLineReference(reference);
1276 // if (result == null) {
1277 // System.out.println("\t super resolver didn't find " + reference);
1278 // } else {
1279 // System.out.println("\t super resolver found " + reference);
1280 // }
1281 return result;
1282 }
1283
1284 public ModuleContext getReferenceContext(final String reference) {
1285 if (label2line.containsKey(reference)) {
1286 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
1287 moduleContext.getLocationWithinModule() + ".get("
1288 + ((Integer) label2line.get(reference)
1289 + ").getLabel()"));
1290 return lc;
1291 }
1292 return resolver.getReferenceContext(reference);
1293 }
1294
1295 }
|