| 1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
| 2 | * |
| 3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
| 4 | * |
| 5 | * "Hilbert II" is free software; you can redistribute |
| 6 | * it and/or modify it under the terms of the GNU General Public |
| 7 | * License as published by the Free Software Foundation; either |
| 8 | * version 2 of the License, or (at your option) any later version. |
| 9 | * |
| 10 | * This program is distributed in the hope that it will be useful, |
| 11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| 13 | * GNU General Public License for more details. |
| 14 | */ |
| 15 | |
| 16 | package org.qedeq.kernel.bo.service.logic; |
| 17 | |
| 18 | import java.util.HashMap; |
| 19 | import java.util.Iterator; |
| 20 | import java.util.Map; |
| 21 | |
| 22 | import org.qedeq.base.io.Parameters; |
| 23 | import org.qedeq.base.io.Version; |
| 24 | import org.qedeq.base.trace.Trace; |
| 25 | import org.qedeq.base.utility.EqualsUtility; |
| 26 | import org.qedeq.base.utility.StringUtility; |
| 27 | import org.qedeq.kernel.bo.log.QedeqLog; |
| 28 | import org.qedeq.kernel.bo.logic.FormulaCheckerFactoryImpl; |
| 29 | import org.qedeq.kernel.bo.logic.common.ExistenceChecker; |
| 30 | import org.qedeq.kernel.bo.logic.common.FormulaCheckerFactory; |
| 31 | import org.qedeq.kernel.bo.logic.common.FormulaUtility; |
| 32 | import org.qedeq.kernel.bo.logic.common.FunctionConstant; |
| 33 | import org.qedeq.kernel.bo.logic.common.FunctionKey; |
| 34 | import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList; |
| 35 | import org.qedeq.kernel.bo.logic.common.PredicateConstant; |
| 36 | import org.qedeq.kernel.bo.logic.common.PredicateKey; |
| 37 | import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl; |
| 38 | import org.qedeq.kernel.bo.module.InternalModuleServiceCall; |
| 39 | import org.qedeq.kernel.bo.module.InternalServiceJob; |
| 40 | import org.qedeq.kernel.bo.module.KernelModuleReferenceList; |
| 41 | import org.qedeq.kernel.bo.module.KernelQedeqBo; |
| 42 | import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker; |
| 43 | import org.qedeq.kernel.bo.service.basis.ControlVisitor; |
| 44 | import org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor; |
| 45 | import org.qedeq.kernel.bo.service.dependency.LoadRequiredModulesPlugin; |
| 46 | import org.qedeq.kernel.se.base.list.Element; |
| 47 | import org.qedeq.kernel.se.base.list.ElementList; |
| 48 | import org.qedeq.kernel.se.base.module.Axiom; |
| 49 | import org.qedeq.kernel.se.base.module.ChangedRule; |
| 50 | import org.qedeq.kernel.se.base.module.ChangedRuleList; |
| 51 | import org.qedeq.kernel.se.base.module.ConditionalProof; |
| 52 | import org.qedeq.kernel.se.base.module.FormalProof; |
| 53 | import org.qedeq.kernel.se.base.module.FormalProofLine; |
| 54 | import org.qedeq.kernel.se.base.module.FormalProofLineList; |
| 55 | import org.qedeq.kernel.se.base.module.Formula; |
| 56 | import org.qedeq.kernel.se.base.module.FunctionDefinition; |
| 57 | import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
| 58 | import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
| 59 | import org.qedeq.kernel.se.base.module.PredicateDefinition; |
| 60 | import org.qedeq.kernel.se.base.module.Proposition; |
| 61 | import org.qedeq.kernel.se.base.module.Reason; |
| 62 | import org.qedeq.kernel.se.base.module.Rule; |
| 63 | import org.qedeq.kernel.se.base.module.Specification; |
| 64 | import org.qedeq.kernel.se.base.module.SubstFree; |
| 65 | import org.qedeq.kernel.se.base.module.SubstFunc; |
| 66 | import org.qedeq.kernel.se.base.module.SubstPred; |
| 67 | import org.qedeq.kernel.se.common.CheckLevel; |
| 68 | import org.qedeq.kernel.se.common.IllegalModuleDataException; |
| 69 | import org.qedeq.kernel.se.common.ModuleDataException; |
| 70 | import org.qedeq.kernel.se.common.ModuleService; |
| 71 | import org.qedeq.kernel.se.common.RuleKey; |
| 72 | import org.qedeq.kernel.se.common.SourceFileException; |
| 73 | import org.qedeq.kernel.se.common.SourceFileExceptionList; |
| 74 | import org.qedeq.kernel.se.dto.list.ElementSet; |
| 75 | import org.qedeq.kernel.se.state.WellFormedState; |
| 76 | import org.qedeq.kernel.se.visitor.InterruptException; |
| 77 | |
| 78 | |
| 79 | /** |
| 80 | * Checks if all formulas of a QEDEQ module are well formed. |
| 81 | * This plugin assumes all required modules are loaded! |
| 82 | * |
| 83 | * @author Michael Meyling |
| 84 | */ |
| 85 | public final class WellFormedCheckerExecutor extends ControlVisitor implements ModuleServicePluginExecutor { |
| 86 | |
| 87 | /** This class. */ |
| 88 | private static final Class CLASS = WellFormedCheckerExecutor.class; |
| 89 | |
| 90 | /** Class definition via formula rule key. */ |
| 91 | private static final RuleKey CLASS_DEFINITION_VIA_FORMULA_RULE |
| 92 | = new RuleKey("CLASS_DEFINITION_BY_FORMULA", "1.00.00"); |
| 93 | |
| 94 | /** Existence checker for predicate and function constants and rules. */ |
| 95 | private ModuleConstantsExistenceCheckerImpl existence; |
| 96 | |
| 97 | /** Factory for generating new checkers. */ |
| 98 | private FormulaCheckerFactory checkerFactory = null; |
| 99 | |
| 100 | /** |
| 101 | * Constructor. |
| 102 | * |
| 103 | * @param plugin This plugin we work for. |
| 104 | * @param qedeq QEDEQ BO object. |
| 105 | * @param parameters Parameters. |
| 106 | */ |
| 107 | WellFormedCheckerExecutor(final ModuleService plugin, final KernelQedeqBo qedeq, |
| 108 | final Parameters parameters) { |
| 109 | super(plugin, qedeq); |
| 110 | final String method = "QedeqBoFormalLogicChecker(Plugin, KernelQedeqBo, Map)"; |
| 111 | final String checkerFactoryClass = parameters.getString("checkerFactory"); |
| 112 | if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) { |
| 113 | try { |
| 114 | Class cl = Class.forName(checkerFactoryClass); |
| 115 | checkerFactory = (FormulaCheckerFactory) cl.newInstance(); |
| 116 | } catch (ClassNotFoundException e) { |
| 117 | Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class not in class path: " |
| 118 | + checkerFactoryClass, e); |
| 119 | } catch (InstantiationException e) { |
| 120 | Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class could not be instanciated: " |
| 121 | + checkerFactoryClass, e); |
| 122 | } catch (IllegalAccessException e) { |
| 123 | Trace.fatal(CLASS, this, method, |
| 124 | "Programming error, access for instantiation failed for model: " |
| 125 | + checkerFactoryClass, e); |
| 126 | } catch (RuntimeException e) { |
| 127 | Trace.fatal(CLASS, this, method, |
| 128 | "Programming error, instantiation failed for model: " + checkerFactoryClass, e); |
| 129 | } |
| 130 | } |
| 131 | // fallback is the default checker factory |
| 132 | if (checkerFactory == null) { |
| 133 | checkerFactory = new FormulaCheckerFactoryImpl(); |
| 134 | } |
| 135 | } |
| 136 | |
| 137 | public Object executePlugin(final InternalModuleServiceCall call, final Object data) throws InterruptException { |
| 138 | if (getKernelQedeqBo().isWellFormed()) { |
| 139 | return Boolean.TRUE; |
| 140 | } |
| 141 | QedeqLog.getInstance().logRequest( |
| 142 | "Check logical well formedness", getKernelQedeqBo().getUrl()); |
| 143 | if (!getKernelQedeqBo().hasLoadedRequiredModules()) { |
| 144 | getServices().executePlugin(call.getInternalServiceProcess(), |
| 145 | LoadRequiredModulesPlugin.class.getName(), getKernelQedeqBo(), null); |
| 146 | } |
| 147 | if (!getKernelQedeqBo().hasLoadedRequiredModules()) { |
| 148 | final String msg = "Check of logical well formedness failed"; |
| 149 | QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(), |
| 150 | "Not all required modules could be loaded."); |
| 151 | return Boolean.FALSE; |
| 152 | } |
| 153 | getKernelQedeqBo().setWellFormedProgressState(WellFormedState.STATE_EXTERNAL_CHECKING); |
| 154 | getKernelQedeqBo().getLabels().resetNodesToWellFormedUnchecked(); |
| 155 | final SourceFileExceptionList sfl = new SourceFileExceptionList(); |
| 156 | final Map rules = new HashMap(); // map RuleKey to KernelQedeqBo |
| 157 | final KernelModuleReferenceList list = getKernelQedeqBo().getKernelRequiredModules(); |
| 158 | for (int i = 0; i < list.size(); i++) { |
| 159 | Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i)); |
| 160 | getServices().checkWellFormedness(call.getInternalServiceProcess(), list.getKernelQedeqBo(i)); |
| 161 | if (!list.getKernelQedeqBo(i).isWellFormed()) { |
| 162 | ModuleDataException md = new CheckRequiredModuleException( |
| 163 | LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE, |
| 164 | LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT |
| 165 | + list.getQedeqBo(i).getModuleAddress(), |
| 166 | list.getModuleContext(i)); |
| 167 | sfl.add(getKernelQedeqBo().createSourceFileException(getService(), md)); |
| 168 | } |
| 169 | final ModuleConstantsExistenceChecker existenceChecker |
| 170 | = list.getKernelQedeqBo(i).getExistenceChecker(); |
| 171 | if (existenceChecker != null) { |
| 172 | final Iterator iter = existenceChecker.getRules().keySet().iterator(); |
| 173 | while (iter.hasNext()) { |
| 174 | final RuleKey key = (RuleKey) iter.next(); |
| 175 | final KernelQedeqBo newQedeq = existenceChecker.getQedeq(key); |
| 176 | final KernelQedeqBo previousQedeq = (KernelQedeqBo) rules.get(key); |
| 177 | if (previousQedeq != null && !newQedeq.equals(previousQedeq)) { |
| 178 | ModuleDataException md = new CheckRequiredModuleException( |
| 179 | LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_CODE, |
| 180 | LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_TEXT |
| 181 | + key + " " + previousQedeq.getUrl() + " " + newQedeq.getUrl(), |
| 182 | list.getModuleContext(i)); |
| 183 | sfl.add(getKernelQedeqBo().createSourceFileException(getService(), md)); |
| 184 | } else { |
| 185 | rules.put(key, newQedeq); |
| 186 | } |
| 187 | } |
| 188 | } |
| 189 | } |
| 190 | // has at least one import errors? |
| 191 | if (sfl.size() > 0) { |
| 192 | getKernelQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_EXTERNAL_CHECKING_FAILED, sfl); |
| 193 | final String msg = "Check of logical well formedness failed"; |
| 194 | QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(), |
| 195 | StringUtility.replace(sfl.getMessage(), "\n", "\n\t")); |
| 196 | return Boolean.FALSE; |
| 197 | } |
| 198 | getKernelQedeqBo().setWellFormedProgressState(WellFormedState.STATE_INTERNAL_CHECKING); |
| 199 | |
| 200 | try { |
| 201 | traverse(call.getInternalServiceProcess()); |
| 202 | } catch (SourceFileExceptionList e) { |
| 203 | getKernelQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_INTERNAL_CHECKING_FAILED, e); |
| 204 | getKernelQedeqBo().setExistenceChecker(existence); |
| 205 | final String msg = "Check of logical well formedness failed"; |
| 206 | QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(), |
| 207 | StringUtility.replace(sfl.getMessage(), "\n", "\n\t")); |
| 208 | return Boolean.FALSE; |
| 209 | } |
| 210 | getKernelQedeqBo().setWellFormed(existence); |
| 211 | QedeqLog.getInstance().logSuccessfulReply( |
| 212 | "Check of logical well formedness successful", getKernelQedeqBo().getUrl()); |
| 213 | return Boolean.TRUE; |
| 214 | } |
| 215 | |
| 216 | public void traverse(final InternalServiceJob process) throws SourceFileExceptionList { |
| 217 | try { |
| 218 | this.existence = new ModuleConstantsExistenceCheckerImpl(getKernelQedeqBo()); |
| 219 | } catch (ModuleDataException me) { |
| 220 | addError(me); |
| 221 | throw getErrorList(); |
| 222 | } |
| 223 | super.traverse(process); |
| 224 | |
| 225 | // check if we have the important module parts |
| 226 | setLocationWithinModule(""); |
| 227 | if (getKernelQedeqBo().getQedeq().getHeader() == null) { |
| 228 | addError(new IllegalModuleDataException( |
| 229 | LogicErrors.MODULE_HAS_NO_HEADER_CODE, |
| 230 | LogicErrors.MODULE_HAS_NO_HEADER_TEXT, |
| 231 | getCurrentContext())); |
| 232 | } |
| 233 | if (getKernelQedeqBo().getQedeq().getHeader().getSpecification() == null) { |
| 234 | addError(new IllegalModuleDataException( |
| 235 | LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_CODE, |
| 236 | LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_TEXT, |
| 237 | getCurrentContext())); |
| 238 | } |
| 239 | } |
| 240 | |
| 241 | public void visitEnter(final Specification specification) throws ModuleDataException { |
| 242 | if (specification == null) { |
| 243 | return; |
| 244 | } |
| 245 | final String context = getCurrentContext().getLocationWithinModule(); |
| 246 | // we start checking if we have a correct version format |
| 247 | setLocationWithinModule(context + ".getRuleVersion()"); |
| 248 | final String version = specification.getRuleVersion(); |
| 249 | try { |
| 250 | new Version(version); |
| 251 | } catch (RuntimeException e) { |
| 252 | addError(new IllegalModuleDataException( |
| 253 | LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE, |
| 254 | LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(), |
| 255 | getCurrentContext())); |
| 256 | } |
| 257 | } |
| 258 | |
| 259 | public void visitEnter(final Axiom axiom) throws ModuleDataException { |
| 260 | if (axiom == null) { |
| 261 | return; |
| 262 | } |
| 263 | final String context = getCurrentContext().getLocationWithinModule(); |
| 264 | // we start checking |
| 265 | getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
| 266 | if (axiom.getFormula() != null) { |
| 267 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 268 | final Formula formula = axiom.getFormula(); |
| 269 | LogicalCheckExceptionList list = |
| 270 | checkerFactory.createFormulaChecker().checkFormula( |
| 271 | formula.getElement(), getCurrentContext(), existence); |
| 272 | for (int i = 0; i < list.size(); i++) { |
| 273 | addError(list.get(i)); |
| 274 | } |
| 275 | } else { |
| 276 | getNodeBo().setWellFormed(CheckLevel.FAILURE); |
| 277 | } |
| 278 | // if we found no errors this node is ok |
| 279 | if (!getNodeBo().isNotWellFormed()) { |
| 280 | getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
| 281 | } |
| 282 | setLocationWithinModule(context); |
| 283 | setBlocked(true); |
| 284 | } |
| 285 | |
| 286 | public void visitLeave(final Axiom axiom) { |
| 287 | setBlocked(false); |
| 288 | } |
| 289 | |
| 290 | public void visitEnter(final PredicateDefinition definition) |
| 291 | throws ModuleDataException { |
| 292 | if (definition == null) { |
| 293 | return; |
| 294 | } |
| 295 | final String context = getCurrentContext().getLocationWithinModule(); |
| 296 | // we start checking |
| 297 | getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
| 298 | final PredicateKey predicateKey = new PredicateKey(definition.getName(), |
| 299 | definition.getArgumentNumber()); |
| 300 | // we misuse a do loop to be able to break |
| 301 | do { |
| 302 | if (existence.predicateExists(predicateKey)) { |
| 303 | addError(new IllegalModuleDataException( |
| 304 | LogicErrors.PREDICATE_ALREADY_DEFINED_CODE, |
| 305 | LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicateKey, |
| 306 | getCurrentContext())); |
| 307 | break; |
| 308 | } |
| 309 | if (definition.getFormula() == null) { |
| 310 | addError(new IllegalModuleDataException( |
| 311 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
| 312 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
| 313 | getCurrentContext())); |
| 314 | break; |
| 315 | } |
| 316 | final Element completeFormula = definition.getFormula().getElement(); |
| 317 | if (completeFormula == null) { |
| 318 | addError(new IllegalModuleDataException( |
| 319 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
| 320 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
| 321 | getCurrentContext())); |
| 322 | break; |
| 323 | } |
| 324 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 325 | if (completeFormula.isAtom()) { |
| 326 | addError(new IllegalModuleDataException( |
| 327 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
| 328 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
| 329 | getCurrentContext())); |
| 330 | break; |
| 331 | } |
| 332 | final ElementList equi = completeFormula.getList(); |
| 333 | final String operator = equi.getOperator(); |
| 334 | if (!operator.equals(FormulaCheckerImpl.EQUIVALENCE_OPERATOR) |
| 335 | || equi.size() != 2) { |
| 336 | addError(new IllegalModuleDataException( |
| 337 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
| 338 | LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
| 339 | getCurrentContext())); |
| 340 | break; |
| 341 | } |
| 342 | setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(0)"); |
| 343 | if (equi.getElement(0).isAtom()) { |
| 344 | addError(new IllegalModuleDataException( |
| 345 | LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE, |
| 346 | LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT, |
| 347 | getCurrentContext())); |
| 348 | break; |
| 349 | } |
| 350 | final ElementList predicate = equi.getElement(0).getList(); |
| 351 | if (predicate.getOperator() != FormulaCheckerImpl.PREDICATE_CONSTANT) { |
| 352 | addError(new IllegalModuleDataException( |
| 353 | LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE, |
| 354 | LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT, |
| 355 | getCurrentContext())); |
| 356 | break; |
| 357 | } |
| 358 | final Element definingFormula = equi.getElement(1); |
| 359 | |
| 360 | final ElementSet free = FormulaUtility.getFreeSubjectVariables(definingFormula); |
| 361 | for (int i = 0; i < predicate.size(); i++) { |
| 362 | setLocationWithinModule(context |
| 363 | + ".getFormula().getElement().getList().getElement(0).getList().getElement(" + i + ")"); |
| 364 | if (i == 0) { |
| 365 | if (!predicate.getElement(0).isAtom() |
| 366 | || !EqualsUtility.equals(definition.getName(), |
| 367 | predicate.getElement(0).getAtom().getString())) { |
| 368 | addError(new IllegalModuleDataException( |
| 369 | LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_CODE, |
| 370 | LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_TEXT |
| 371 | + StringUtility.quote(definition.getName()) + " - " |
| 372 | + StringUtility.quote(predicate.getElement(0).getAtom().getString()), |
| 373 | getCurrentContext())); |
| 374 | continue; |
| 375 | } |
| 376 | } else if (!FormulaUtility.isSubjectVariable(predicate.getElement(i))) { |
| 377 | addError(new IllegalModuleDataException( |
| 378 | LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE, |
| 379 | LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT + predicate.getElement(i), |
| 380 | getCurrentContext())); |
| 381 | continue; |
| 382 | } |
| 383 | setLocationWithinModule(context |
| 384 | + ".getFormula().getElement().getList().getElement(1)"); |
| 385 | if (i != 0 && !free.contains(predicate.getElement(i))) { |
| 386 | addError(new IllegalModuleDataException( |
| 387 | LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE, |
| 388 | LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT + predicate.getElement(i), |
| 389 | getCurrentContext())); |
| 390 | } |
| 391 | } |
| 392 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 393 | if (predicate.size() - 1 != free.size()) { |
| 394 | addError(new IllegalModuleDataException( |
| 395 | LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE, |
| 396 | LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT, |
| 397 | getCurrentContext())); |
| 398 | } |
| 399 | setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"); |
| 400 | final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula( |
| 401 | definingFormula, getCurrentContext(), existence); |
| 402 | for (int i = 0; i < list.size(); i++) { |
| 403 | addError(list.get(i)); |
| 404 | } |
| 405 | if (list.size() > 0) { |
| 406 | break; |
| 407 | } |
| 408 | setLocationWithinModule(context + ".getFormula().getElement().getList()"); |
| 409 | final PredicateConstant constant = new PredicateConstant(predicateKey, |
| 410 | equi, getCurrentContext()); |
| 411 | setLocationWithinModule(context); |
| 412 | if (existence.predicateExists(predicateKey)) { |
| 413 | addError(new IllegalModuleDataException( |
| 414 | LogicErrors.PREDICATE_ALREADY_DEFINED_CODE, |
| 415 | LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT |
| 416 | + predicateKey, getCurrentContext())); |
| 417 | break; |
| 418 | } |
| 419 | // a final check, we don't expect any new errors here, but hey - we want to be very sure! |
| 420 | if (!getNodeBo().isNotWellFormed()) { |
| 421 | existence.add(constant); |
| 422 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 423 | final LogicalCheckExceptionList errorlist = checkerFactory.createFormulaChecker() |
| 424 | .checkFormula(completeFormula, getCurrentContext(), existence); |
| 425 | for (int i = 0; i < errorlist.size(); i++) { |
| 426 | addError(errorlist.get(i)); |
| 427 | } |
| 428 | } |
| 429 | } while (false); |
| 430 | |
| 431 | // check if we just found the identity operator |
| 432 | setLocationWithinModule(context); |
| 433 | if ("2".equals(predicateKey.getArguments()) |
| 434 | && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) { |
| 435 | existence.setIdentityOperatorDefined(predicateKey.getName(), |
| 436 | getKernelQedeqBo(), getCurrentContext()); |
| 437 | } |
| 438 | // if we found no errors this node is ok |
| 439 | if (!getNodeBo().isNotWellFormed()) { |
| 440 | getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
| 441 | } |
| 442 | setBlocked(true); |
| 443 | } |
| 444 | |
| 445 | public void visitLeave(final PredicateDefinition definition) { |
| 446 | setBlocked(false); |
| 447 | } |
| 448 | |
| 449 | public void visitEnter(final InitialPredicateDefinition definition) |
| 450 | throws ModuleDataException { |
| 451 | if (definition == null) { |
| 452 | return; |
| 453 | } |
| 454 | final String context = getCurrentContext().getLocationWithinModule(); |
| 455 | // we start checking |
| 456 | getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
| 457 | final PredicateKey predicateKey = new PredicateKey( |
| 458 | definition.getName(), definition.getArgumentNumber()); |
| 459 | setLocationWithinModule(context); |
| 460 | if (existence.predicateExists(predicateKey)) { |
| 461 | addError(new IllegalModuleDataException( |
| 462 | LogicErrors.PREDICATE_ALREADY_DEFINED_CODE, |
| 463 | LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT |
| 464 | + predicateKey, getCurrentContext())); |
| 465 | } |
| 466 | existence.add(definition); |
| 467 | // check if we just found the identity operator |
| 468 | if ("2".equals(predicateKey.getArguments()) |
| 469 | && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) { |
| 470 | existence.setIdentityOperatorDefined(predicateKey.getName(), |
| 471 | getKernelQedeqBo(), getCurrentContext()); |
| 472 | } |
| 473 | // if we found no errors this node is ok |
| 474 | if (!getNodeBo().isNotWellFormed()) { |
| 475 | getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
| 476 | } |
| 477 | setBlocked(true); |
| 478 | } |
| 479 | |
| 480 | public void visitLeave(final InitialPredicateDefinition definition) { |
| 481 | setBlocked(false); |
| 482 | } |
| 483 | |
| 484 | public void visitEnter(final InitialFunctionDefinition definition) |
| 485 | throws ModuleDataException { |
| 486 | if (definition == null) { |
| 487 | return; |
| 488 | } |
| 489 | final String context = getCurrentContext().getLocationWithinModule(); |
| 490 | // we start checking |
| 491 | getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
| 492 | final FunctionKey function = new FunctionKey(definition.getName(), |
| 493 | definition.getArgumentNumber()); |
| 494 | if (existence.functionExists(function)) { |
| 495 | addError(new IllegalModuleDataException( |
| 496 | LogicErrors.FUNCTION_ALREADY_DEFINED_CODE, |
| 497 | LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT + function, |
| 498 | getCurrentContext())); |
| 499 | } |
| 500 | existence.add(definition); |
| 501 | setLocationWithinModule(context); |
| 502 | // if we found no errors this node is ok |
| 503 | if (!getNodeBo().isNotWellFormed()) { |
| 504 | getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
| 505 | } |
| 506 | setBlocked(true); |
| 507 | } |
| 508 | |
| 509 | public void visitLeave(final InitialFunctionDefinition definition) { |
| 510 | setBlocked(false); |
| 511 | } |
| 512 | |
| 513 | public void visitEnter(final FunctionDefinition definition) |
| 514 | throws ModuleDataException { |
| 515 | if (definition == null) { |
| 516 | return; |
| 517 | } |
| 518 | final String context = getCurrentContext().getLocationWithinModule(); |
| 519 | // we start checking |
| 520 | getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
| 521 | final FunctionKey function = new FunctionKey(definition.getName(), |
| 522 | definition.getArgumentNumber()); |
| 523 | // we misuse a do loop to be able to break |
| 524 | do { |
| 525 | if (existence.functionExists(function)) { |
| 526 | addError(new IllegalModuleDataException( |
| 527 | LogicErrors.FUNCTION_ALREADY_DEFINED_CODE, |
| 528 | LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT |
| 529 | + function, getCurrentContext())); |
| 530 | break; |
| 531 | } |
| 532 | if (definition.getFormula() == null) { |
| 533 | addError(new IllegalModuleDataException( |
| 534 | LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE, |
| 535 | LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT, |
| 536 | getCurrentContext())); |
| 537 | break; |
| 538 | } |
| 539 | final Formula formulaArgument = definition.getFormula(); |
| 540 | setLocationWithinModule(context + ".getFormula()"); |
| 541 | if (formulaArgument.getElement() == null || formulaArgument.getElement().isAtom()) { |
| 542 | addError(new IllegalModuleDataException( |
| 543 | LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE, |
| 544 | LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT, |
| 545 | getCurrentContext())); |
| 546 | break; |
| 547 | } |
| 548 | final ElementList formula = formulaArgument.getElement().getList(); |
| 549 | setLocationWithinModule(context + ".getFormula().getElement().getList()"); |
| 550 | if (!existence.identityOperatorExists()) { |
| 551 | addError(new IllegalModuleDataException( |
| 552 | LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE, |
| 553 | LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT, |
| 554 | getCurrentContext())); |
| 555 | break; |
| 556 | } |
| 557 | if (!FormulaCheckerImpl.PREDICATE_CONSTANT.equals(formula.getOperator())) { |
| 558 | addError(new IllegalModuleDataException( |
| 559 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
| 560 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
| 561 | getCurrentContext())); |
| 562 | break; |
| 563 | } |
| 564 | if (formula.size() != 3) { |
| 565 | addError(new IllegalModuleDataException( |
| 566 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
| 567 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
| 568 | getCurrentContext())); |
| 569 | break; |
| 570 | } |
| 571 | if (!formula.getElement(0).isAtom()) { |
| 572 | addError(new IllegalModuleDataException( |
| 573 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
| 574 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
| 575 | getCurrentContext())); |
| 576 | break; |
| 577 | } |
| 578 | if (!EqualsUtility.equals(existence.getIdentityOperator(), |
| 579 | formula.getElement(0).getAtom().getString())) { |
| 580 | addError(new IllegalModuleDataException( |
| 581 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
| 582 | LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
| 583 | getCurrentContext())); |
| 584 | break; |
| 585 | } |
| 586 | setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"); |
| 587 | if (formula.getElement(1).isAtom()) { |
| 588 | addError(new IllegalModuleDataException( |
| 589 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
| 590 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
| 591 | getCurrentContext())); |
| 592 | break; |
| 593 | } |
| 594 | final ElementList functionConstant = formula.getElement(1).getList(); |
| 595 | if (!FormulaCheckerImpl.FUNCTION_CONSTANT.equals(functionConstant.getOperator())) { |
| 596 | addError(new IllegalModuleDataException( |
| 597 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
| 598 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
| 599 | getCurrentContext())); |
| 600 | break; |
| 601 | } |
| 602 | setLocationWithinModule(context |
| 603 | + ".getFormula().getElement().getList().getElement(1).getList()"); |
| 604 | final int size = functionConstant.size(); |
| 605 | if (!("" + (size - 1)).equals(definition.getArgumentNumber())) { |
| 606 | addError(new IllegalModuleDataException( |
| 607 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
| 608 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
| 609 | getCurrentContext())); |
| 610 | break; |
| 611 | } |
| 612 | setLocationWithinModule(context |
| 613 | + ".getFormula().getElement().getList().getElement(1).getList().getElement(0)"); |
| 614 | if (!functionConstant.getElement(0).isAtom()) { |
| 615 | addError(new IllegalModuleDataException( |
| 616 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
| 617 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
| 618 | getCurrentContext())); |
| 619 | break; |
| 620 | } |
| 621 | if (!EqualsUtility.equals(definition.getName(), |
| 622 | functionConstant.getElement(0).getAtom().getString())) { |
| 623 | addError(new IllegalModuleDataException( |
| 624 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
| 625 | LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
| 626 | getCurrentContext())); |
| 627 | break; |
| 628 | } |
| 629 | setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)"); |
| 630 | if (formula.getElement(2).isAtom()) { |
| 631 | addError(new IllegalModuleDataException( |
| 632 | LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_CODE, |
| 633 | LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_TEXT, |
| 634 | getCurrentContext())); |
| 635 | break; |
| 636 | } |
| 637 | final ElementList term = formula.getElement(2).getList(); |
| 638 | setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"); |
| 639 | final ElementSet free = FormulaUtility.getFreeSubjectVariables(term); |
| 640 | if (size - 1 != free.size()) { |
| 641 | addError(new IllegalModuleDataException( |
| 642 | LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE, |
| 643 | LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT, |
| 644 | getCurrentContext())); |
| 645 | break; |
| 646 | } |
| 647 | if (functionConstant.getElement(0).isList() |
| 648 | || !EqualsUtility.equals(function.getName(), |
| 649 | functionConstant.getElement(0).getAtom().getString())) { |
| 650 | addError(new IllegalModuleDataException( |
| 651 | LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_CODE, |
| 652 | LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_TEXT |
| 653 | + function.getName(), getCurrentContext())); |
| 654 | } |
| 655 | for (int i = 1; i < size; i++) { |
| 656 | setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)" |
| 657 | + ".getList().getElement(" + i + ")"); |
| 658 | if (!FormulaUtility.isSubjectVariable(functionConstant.getElement(i))) { |
| 659 | addError(new IllegalModuleDataException( |
| 660 | LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE, |
| 661 | LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT |
| 662 | + functionConstant.getElement(i), getCurrentContext())); |
| 663 | } |
| 664 | if (!free.contains(functionConstant.getElement(i))) { |
| 665 | addError(new IllegalModuleDataException( |
| 666 | LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE, |
| 667 | LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT |
| 668 | + functionConstant.getElement(i), getCurrentContext())); |
| 669 | } |
| 670 | } |
| 671 | setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)"); |
| 672 | final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker() |
| 673 | .checkTerm(term, getCurrentContext(), existence); |
| 674 | for (int i = 0; i < list.size(); i++) { |
| 675 | addError(list.get(i)); |
| 676 | } |
| 677 | if (list.size() > 0) { |
| 678 | break; |
| 679 | } |
| 680 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 681 | // if we found no errors |
| 682 | if (!getNodeBo().isNotWellFormed()) { |
| 683 | existence.add(new FunctionConstant(function, formula, getCurrentContext())); |
| 684 | // a final check, we don't expect any new errors here, but hey - we want to be very sure! |
| 685 | final LogicalCheckExceptionList listComplete = checkerFactory.createFormulaChecker() |
| 686 | .checkFormula(formulaArgument.getElement(), getCurrentContext(), existence); |
| 687 | for (int i = 0; i < listComplete.size(); i++) { |
| 688 | addError(listComplete.get(i)); |
| 689 | } |
| 690 | } |
| 691 | } while (false); |
| 692 | setLocationWithinModule(context); |
| 693 | // if we found no errors this node is ok |
| 694 | if (!getNodeBo().isNotWellFormed()) { |
| 695 | getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
| 696 | } |
| 697 | setBlocked(true); |
| 698 | } |
| 699 | |
| 700 | public void visitLeave(final FunctionDefinition definition) { |
| 701 | setBlocked(false); |
| 702 | } |
| 703 | |
| 704 | public void visitEnter(final Proposition proposition) |
| 705 | throws ModuleDataException { |
| 706 | if (proposition == null) { |
| 707 | return; |
| 708 | } |
| 709 | final String context = getCurrentContext().getLocationWithinModule(); |
| 710 | // we start checking |
| 711 | getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
| 712 | if (proposition.getFormula() != null) { |
| 713 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 714 | final Formula formula = proposition.getFormula(); |
| 715 | LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula( |
| 716 | formula.getElement(), getCurrentContext(), existence); |
| 717 | for (int i = 0; i < list.size(); i++) { |
| 718 | addError(list.get(i)); |
| 719 | } |
| 720 | } else { // no formula |
| 721 | getNodeBo().setWellFormed(CheckLevel.FAILURE); |
| 722 | } |
| 723 | if (proposition.getFormalProofList() != null) { |
| 724 | for (int i = 0; i < proposition.getFormalProofList().size(); i++) { |
| 725 | final FormalProof proof = proposition.getFormalProofList().get(i); |
| 726 | if (proof != null) { |
| 727 | final FormalProofLineList list = proof.getFormalProofLineList(); |
| 728 | setLocationWithinModule(context + ".getFormalProofList().get(" |
| 729 | + i + ").getFormalProofLineList()"); |
| 730 | checkFormalProof(list); |
| 731 | } |
| 732 | } |
| 733 | } |
| 734 | setLocationWithinModule(context); |
| 735 | // if we found no errors this node is ok |
| 736 | if (!getNodeBo().isNotWellFormed()) { |
| 737 | getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
| 738 | } |
| 739 | setBlocked(true); |
| 740 | } |
| 741 | |
| 742 | /** |
| 743 | * Check formal proof formulas. |
| 744 | * |
| 745 | * @param list List of lines. |
| 746 | */ |
| 747 | private void checkFormalProof(final FormalProofLineList list) { |
| 748 | final String context = getCurrentContext().getLocationWithinModule(); |
| 749 | if (list != null) { |
| 750 | for (int i = 0; i < list.size(); i++) { |
| 751 | final FormalProofLine line = list.get(i); |
| 752 | setLocationWithinModule(context + ".get(" + i + ")"); |
| 753 | checkProofLine(line); |
| 754 | } |
| 755 | } |
| 756 | } |
| 757 | |
| 758 | /** |
| 759 | * Check well-formedness of proof lines. |
| 760 | * |
| 761 | * @param line Check formulas and terms of this proof line. |
| 762 | */ |
| 763 | private void checkProofLine(final FormalProofLine line) { |
| 764 | if (line instanceof ConditionalProof) { |
| 765 | checkProofLine((ConditionalProof) line); |
| 766 | return; |
| 767 | } |
| 768 | final String context = getCurrentContext().getLocationWithinModule(); |
| 769 | LogicalCheckExceptionList elist = new LogicalCheckExceptionList(); |
| 770 | if (line != null) { |
| 771 | final Formula formula = line.getFormula(); |
| 772 | if (formula != null) { |
| 773 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 774 | elist = checkerFactory.createFormulaChecker().checkFormula( |
| 775 | formula.getElement(), getCurrentContext(), existence); |
| 776 | for (int k = 0; k < elist.size(); k++) { |
| 777 | addError(elist.get(k)); |
| 778 | } |
| 779 | } |
| 780 | final Reason reason = line.getReason(); |
| 781 | if (reason != null) { |
| 782 | if (reason instanceof SubstFree) { |
| 783 | final SubstFree subst = (SubstFree) reason; |
| 784 | if (subst.getSubstFree().getSubstituteTerm() != null) { |
| 785 | setLocationWithinModule(context |
| 786 | + ".getReason().getSubstFree().getSubstituteTerm()"); |
| 787 | elist = checkerFactory.createFormulaChecker().checkTerm( |
| 788 | subst.getSubstFree().getSubstituteTerm(), |
| 789 | getCurrentContext(), existence); |
| 790 | } |
| 791 | } else if (reason instanceof SubstPred) { |
| 792 | final SubstPred subst = (SubstPred) reason; |
| 793 | if (subst.getSubstPred().getSubstituteFormula() != null) { |
| 794 | setLocationWithinModule(context |
| 795 | + ".getReason().getSubstPred().getSubstituteFormula()"); |
| 796 | elist = checkerFactory.createFormulaChecker().checkFormula( |
| 797 | subst.getSubstPred().getSubstituteFormula(), |
| 798 | getCurrentContext(), existence); |
| 799 | } |
| 800 | } else if (reason instanceof SubstFunc) { |
| 801 | final SubstFunc subst = (SubstFunc) reason; |
| 802 | if (subst.getSubstFunc().getSubstituteTerm() != null) { |
| 803 | setLocationWithinModule(context |
| 804 | + ".getReason().getSubstFunc().getSubstituteTerm()"); |
| 805 | elist = checkerFactory.createFormulaChecker().checkTerm( |
| 806 | subst.getSubstFunc().getSubstituteTerm(), |
| 807 | getCurrentContext(), existence); |
| 808 | } |
| 809 | } |
| 810 | for (int k = 0; k < elist.size(); k++) { |
| 811 | addError(elist.get(k)); |
| 812 | } |
| 813 | } |
| 814 | } |
| 815 | } |
| 816 | |
| 817 | /** |
| 818 | * Check well-formedness of proof lines. |
| 819 | * |
| 820 | * @param line Check formulas and terms of this proof line. |
| 821 | */ |
| 822 | private void checkProofLine(final ConditionalProof line) { |
| 823 | final String context = getCurrentContext().getLocationWithinModule(); |
| 824 | LogicalCheckExceptionList elist = new LogicalCheckExceptionList(); |
| 825 | if (line != null) { |
| 826 | { |
| 827 | final Formula formula = line.getFormula(); |
| 828 | if (formula != null && formula.getElement() != null) { |
| 829 | setLocationWithinModule(context + ".getFormula().getElement()"); |
| 830 | elist = checkerFactory.createFormulaChecker().checkFormula( |
| 831 | formula.getElement(), getCurrentContext(), existence); |
| 832 | for (int k = 0; k < elist.size(); k++) { |
| 833 | addError(elist.get(k)); |
| 834 | } |
| 835 | } |
| 836 | } |
| 837 | if (line.getHypothesis() != null) { |
| 838 | final Formula formula = line.getHypothesis().getFormula();; |
| 839 | if (formula != null && formula.getElement() != null) { |
| 840 | setLocationWithinModule(context |
| 841 | + ".getHypothesis().getFormula().getElement()"); |
| 842 | elist = checkerFactory.createFormulaChecker().checkFormula( |
| 843 | formula.getElement(), getCurrentContext(), existence); |
| 844 | for (int k = 0; k < elist.size(); k++) { |
| 845 | addError(elist.get(k)); |
| 846 | } |
| 847 | } |
| 848 | } |
| 849 | if (line.getFormalProofLineList() != null) { |
| 850 | setLocationWithinModule(context + ".getFormalProofLineList()"); |
| 851 | checkFormalProof(line.getFormalProofLineList()); |
| 852 | } |
| 853 | if (line.getConclusion() != null) { |
| 854 | final Formula formula = line.getConclusion().getFormula();; |
| 855 | if (formula != null && formula.getElement() != null) { |
| 856 | setLocationWithinModule(context |
| 857 | + ".getConclusion().getFormula().getElement()"); |
| 858 | elist = checkerFactory.createFormulaChecker().checkFormula( |
| 859 | formula.getElement(), getCurrentContext(), existence); |
| 860 | for (int k = 0; k < elist.size(); k++) { |
| 861 | addError(elist.get(k)); |
| 862 | } |
| 863 | } |
| 864 | } |
| 865 | } |
| 866 | } |
| 867 | |
| 868 | public void visitLeave(final Proposition definition) { |
| 869 | setBlocked(false); |
| 870 | } |
| 871 | |
| 872 | public void visitEnter(final Rule rule) throws ModuleDataException { |
| 873 | final String context = getCurrentContext().getLocationWithinModule(); |
| 874 | // we start checking |
| 875 | getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
| 876 | final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion()); |
| 877 | if (rule.getName() != null && rule.getName().length() > 0 && rule.getVersion() != null |
| 878 | && rule.getVersion().length() > 0) { |
| 879 | try { |
| 880 | setLocationWithinModule(context + ".getVersion()"); |
| 881 | new Version(rule.getVersion()); |
| 882 | } catch (RuntimeException e) { |
| 883 | addError(new IllegalModuleDataException( |
| 884 | LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE, |
| 885 | LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(), |
| 886 | getCurrentContext())); |
| 887 | } |
| 888 | if (existence.ruleExists(ruleKey)) { |
| 889 | addError(new IllegalModuleDataException( |
| 890 | LogicErrors.RULE_ALREADY_DEFINED_CODE, |
| 891 | LogicErrors.RULE_ALREADY_DEFINED_TEXT |
| 892 | + ruleKey + " " + existence.getQedeq(ruleKey).getUrl(), |
| 893 | getCurrentContext())); |
| 894 | } else { |
| 895 | if (CLASS_DEFINITION_VIA_FORMULA_RULE.equals(ruleKey)) { |
| 896 | // FIXME 20080114 m31: check if this rule can be proposed |
| 897 | // are the preconditions for using this rule fulfilled? |
| 898 | existence.setClassOperatorModule(getKernelQedeqBo(), |
| 899 | getCurrentContext()); |
| 900 | } |
| 901 | existence.add(ruleKey, rule); |
| 902 | } |
| 903 | if (rule.getChangedRuleList() != null) { |
| 904 | final ChangedRuleList list = rule.getChangedRuleList(); |
| 905 | for (int i = 0; i < list.size(); i++) { |
| 906 | setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ")"); |
| 907 | final ChangedRule r = list.get(i); |
| 908 | if (r == null || r.getName() == null || r.getName().length() <= 0 |
| 909 | || r.getVersion() == null || r.getVersion().length() <= 0) { |
| 910 | addError(new IllegalModuleDataException( |
| 911 | LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE, |
| 912 | LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT |
| 913 | + (r == null ? "null" : r.getName() + " [" + r.getVersion() + "]"), |
| 914 | getCurrentContext())); |
| 915 | continue; |
| 916 | } |
| 917 | setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()"); |
| 918 | final String ruleName = r.getName(); |
| 919 | final String ruleVersion = r.getVersion(); |
| 920 | try { |
| 921 | new Version(ruleVersion); |
| 922 | } catch (RuntimeException e) { |
| 923 | addError(new IllegalModuleDataException( |
| 924 | LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE, |
| 925 | LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(), |
| 926 | getCurrentContext())); |
| 927 | } |
| 928 | RuleKey key1 = getLocalRuleKey(ruleName); |
| 929 | if (key1 == null) { |
| 930 | key1 = existence.getParentRuleKey(ruleName); |
| 931 | } |
| 932 | if (key1 == null) { |
| 933 | addError(new IllegalModuleDataException( |
| 934 | LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_CODE, |
| 935 | LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_TEXT |
| 936 | + ruleName, getCurrentContext())); |
| 937 | } else { |
| 938 | final RuleKey key2 = new RuleKey(ruleName, ruleVersion); |
| 939 | if (existence.ruleExists(key2)) { |
| 940 | addError(new IllegalModuleDataException( |
| 941 | LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_CODE, |
| 942 | LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_TEXT |
| 943 | + ruleName, getCurrentContext(), getKernelQedeqBo().getLabels() |
| 944 | .getRuleContext(key2))); |
| 945 | } else { |
| 946 | try { |
| 947 | if (!Version.less(key1.getVersion(), key2.getVersion())) { |
| 948 | addError(new IllegalModuleDataException( |
| 949 | LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_CODE, |
| 950 | LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_TEXT |
| 951 | + key1 + " " + key2, getCurrentContext(), getKernelQedeqBo().getLabels() |
| 952 | .getRuleContext(key2))); |
| 953 | } |
| 954 | } catch (RuntimeException e) { |
| 955 | addError(new IllegalModuleDataException( |
| 956 | LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_CODE, |
| 957 | LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_TEXT |
| 958 | + key1 + " " + key2, getCurrentContext(), getKernelQedeqBo().getLabels() |
| 959 | .getRuleContext(key2))); |
| 960 | } |
| 961 | } |
| 962 | existence.add(key2, rule); |
| 963 | } |
| 964 | } |
| 965 | } |
| 966 | } else { |
| 967 | addError(new IllegalModuleDataException( |
| 968 | LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE, |
| 969 | LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT |
| 970 | + ruleKey, getCurrentContext())); |
| 971 | } |
| 972 | // if we found no errors this node is ok |
| 973 | if (!getNodeBo().isNotWellFormed()) { |
| 974 | getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
| 975 | } |
| 976 | setBlocked(true); |
| 977 | } |
| 978 | |
| 979 | public void visitLeave(final Rule rule) { |
| 980 | setBlocked(false); |
| 981 | } |
| 982 | |
| 983 | protected void addError(final ModuleDataException me) { |
| 984 | if (getNodeBo() != null) { |
| 985 | getNodeBo().setWellFormed(CheckLevel.FAILURE); |
| 986 | } |
| 987 | super.addError(me); |
| 988 | } |
| 989 | |
| 990 | protected void addError(final SourceFileException me) { |
| 991 | if (getNodeBo() != null) { |
| 992 | getNodeBo().setWellFormed(CheckLevel.FAILURE); |
| 993 | } |
| 994 | super.addError(me); |
| 995 | } |
| 996 | |
| 997 | } |