001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.logic;
017
018 import java.util.HashMap;
019 import java.util.Iterator;
020 import java.util.Map;
021 import java.util.Set;
022
023 import org.qedeq.kernel.bo.common.ModuleReferenceList;
024 import org.qedeq.kernel.bo.logic.common.ClassOperatorAlreadyExistsException;
025 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
026 import org.qedeq.kernel.bo.logic.common.FunctionKey;
027 import org.qedeq.kernel.bo.logic.common.IdentityOperatorAlreadyExistsException;
028 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
029 import org.qedeq.kernel.bo.logic.common.PredicateKey;
030 import org.qedeq.kernel.bo.module.KernelQedeqBo;
031 import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
032 import org.qedeq.kernel.se.base.module.Rule;
033 import org.qedeq.kernel.se.common.IllegalModuleDataException;
034 import org.qedeq.kernel.se.common.ModuleContext;
035 import org.qedeq.kernel.se.common.ModuleDataException;
036 import org.qedeq.kernel.se.common.RuleKey;
037
038
039 /**
040 * Checks if a predicate or function constant is defined.
041 *
042 * @author Michael Meyling
043 */
044 public class ModuleConstantsExistenceCheckerImpl extends DefaultExistenceChecker
045 implements ModuleConstantsExistenceChecker {
046
047 /** QEDEQ module properties. */
048 private final KernelQedeqBo prop;
049
050 /** In this module the class operator is defined. */
051 private KernelQedeqBo classOperatorModule;
052
053 /** In this class the identityOperator is defined. */
054 private KernelQedeqBo identityOperatorModule;
055
056 /**
057 * Constructor.
058 *
059 * @param prop QEDEQ module properties object.
060 * @throws ModuleDataException Referenced QEDEQ modules are already inconsistent: they doesn't
061 * mix.
062 */
063 public ModuleConstantsExistenceCheckerImpl(final KernelQedeqBo prop) throws ModuleDataException {
064 super();
065 this.prop = prop;
066 init();
067 }
068
069 /**
070 * Check if required QEDEQ modules mix without problems. If for example the identity operator
071 * is defined in two different modules in two different ways we have got a problem.
072 * Also the basic properties (for example
073 * {@link ModuleConstantsExistenceCheckerImpl#setIdentityOperatorDefined(String,
074 * KernelQedeqBo, ModuleContext)} and
075 * {@link ModuleConstantsExistenceCheckerImpl#setClassOperatorModule(KernelQedeqBo)}) are set accordingly.
076 *
077 * @throws ModuleDataException Required modules doesn't mix.
078 */
079 public final void init() throws ModuleDataException {
080 clear();
081 final ModuleReferenceList list = prop.getRequiredModules();
082 final Map rules = new HashMap();
083 for (int i = 0; i < list.size(); i++) {
084 final KernelQedeqBo bo = (KernelQedeqBo) list
085 .getQedeqBo(i);
086 if (bo.getExistenceChecker().identityOperatorExists()) {
087 final String identityOperator = list.getLabel(i) + "."
088 + bo.getExistenceChecker().getIdentityOperator();
089 setIdentityOperatorDefined(identityOperator,
090 bo.getExistenceChecker().getIdentityOperatorModule(),
091 list.getModuleContext(i));
092 }
093 if (bo.getExistenceChecker().classOperatorExists()) {
094 setClassOperatorModule(bo.getExistenceChecker().getClassOperatorModule(),
095 list.getModuleContext(i));
096 }
097 final Map cut = bo.getExistenceChecker().getRules();
098 final Iterator iter = cut.keySet().iterator();
099 while (iter.hasNext()) {
100 final RuleKey key = (RuleKey) iter.next();
101 if (rules.containsKey(key) && !rules.get(key).equals(cut.get(key))) {
102 throw new IllegalModuleDataException(
103 LogicErrors.RULE_DEFINITIONS_DONT_MIX_CODE,
104 LogicErrors.RULE_DEFINITIONS_DONT_MIX_TEXT + key + " in "
105 + ((KernelQedeqBo) rules.get(key)).getLabels().getRuleContext(key),
106 list.getModuleContext(i),
107 ((KernelQedeqBo) getQedeq(key)).getLabels().getRuleContext(key));
108 }
109 }
110 rules.putAll(bo.getExistenceChecker().getRules());
111 }
112 }
113
114 public boolean predicateExists(final PredicateKey predicate) {
115 final String name = predicate.getName();
116 final String arguments = predicate.getArguments();
117 final int external = name.indexOf('.');
118 if (external < 0) {
119 return super.predicateExists(predicate);
120 }
121 final String label = name.substring(0, external);
122 final ModuleReferenceList ref = prop.getRequiredModules();
123
124 final KernelQedeqBo newProp = (KernelQedeqBo) ref
125 .getQedeqBo(label);
126 if (newProp == null) {
127 return false;
128 }
129 final String shortName = name.substring(external + 1);
130 return newProp.getExistenceChecker().predicateExists(new PredicateKey(shortName, arguments));
131 }
132
133 public boolean functionExists(final FunctionKey function) {
134 final String name = function.getName();
135 final String arguments = function.getArguments();
136 final int external = name.indexOf(".");
137 if (external < 0) {
138 return super.functionExists(function);
139 }
140 final String label = name.substring(0, external);
141 final ModuleReferenceList ref = prop.getRequiredModules();
142 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label);
143 if (newProp == null) {
144 return false;
145 }
146 final String shortName = name.substring(external + 1);
147 return newProp.getExistenceChecker().functionExists(new FunctionKey(shortName, arguments));
148 }
149
150 public boolean isInitialPredicate(final PredicateKey predicate) {
151 final String name = predicate.getName();
152 final String arguments = predicate.getArguments();
153 final int external = name.indexOf('.');
154 if (external < 0) {
155 return super.isInitialPredicate(predicate);
156 }
157 final String label = name.substring(0, external);
158 final ModuleReferenceList ref = prop.getRequiredModules();
159
160 final KernelQedeqBo newProp = (KernelQedeqBo) ref
161 .getQedeqBo(label);
162 if (newProp == null) {
163 return false;
164 }
165 final String shortName = name.substring(external + 1);
166 return newProp.getExistenceChecker().isInitialPredicate(
167 new PredicateKey(shortName, arguments));
168 }
169
170 public boolean isInitialFunction(final FunctionKey function) {
171 final String name = function.getName();
172 final String arguments = function.getArguments();
173 final int external = name.indexOf('.');
174 if (external < 0) {
175 return super.isInitialFunction(function);
176 }
177 final String label = name.substring(0, external);
178 final ModuleReferenceList ref = prop.getRequiredModules();
179
180 final KernelQedeqBo newProp = (KernelQedeqBo) ref
181 .getQedeqBo(label);
182 if (newProp == null) {
183 return false;
184 }
185 final String shortName = name.substring(external + 1);
186 return newProp.getExistenceChecker().isInitialFunction(
187 new FunctionKey(shortName, arguments));
188 }
189
190 public PredicateConstant get(final PredicateKey predicate) {
191 final String name = predicate.getName();
192 final String arguments = predicate.getArguments();
193 final int external = name.indexOf('.');
194 if (external < 0) {
195 return super.get(predicate);
196 }
197 final String label = name.substring(0, external);
198 final ModuleReferenceList ref = prop.getRequiredModules();
199
200 final KernelQedeqBo newProp = (KernelQedeqBo) ref
201 .getQedeqBo(label);
202 if (newProp == null) {
203 return null;
204 }
205 final String shortName = name.substring(external + 1);
206 return newProp.getExistenceChecker().get(new PredicateKey(shortName, arguments));
207 }
208
209 public FunctionConstant get(final FunctionKey function) {
210 final String name = function.getName();
211 final String arguments = function.getArguments();
212 final int external = name.indexOf(".");
213 if (external < 0) {
214 return super.get(function);
215 }
216 final String label = name.substring(0, external);
217 final ModuleReferenceList ref = prop.getRequiredModules();
218 final KernelQedeqBo newProp = (KernelQedeqBo) ref
219 .getQedeqBo(label);
220 if (newProp == null) {
221 return null;
222 }
223 final String shortName = name.substring(external + 1);
224 return newProp.getExistenceChecker().get(new FunctionKey(shortName, arguments));
225 }
226
227 /**
228 * Get QEDEQ module where given function constant is defined.
229 *
230 * @param function Function we look for.
231 * @return QEDEQ module where function constant is defined.
232 */
233 public KernelQedeqBo getQedeq(final FunctionKey function) {
234 final String name = function.getName();
235 final String arguments = function.getArguments();
236 final int external = name.indexOf(".");
237 if (external < 0) {
238 if (functionExists(function)) {
239 return prop;
240 } else {
241 return null;
242 }
243 }
244 final String label = name.substring(0, external);
245 final ModuleReferenceList ref = prop.getRequiredModules();
246 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label);
247 if (newProp == null) {
248 return newProp;
249 }
250 final String shortName = name.substring(external + 1);
251 return newProp.getExistenceChecker().getQedeq(new FunctionKey(shortName, arguments));
252 }
253
254 /**
255 * Get QEDEQ module where given predicate constant is defined.
256 *
257 * @param predicate Predicate we look for.
258 * @return QEDEQ module where predicate constant is defined.x
259 */
260 public KernelQedeqBo getQedeq(final PredicateKey predicate) {
261 final String name = predicate.getName();
262 final String arguments = predicate.getArguments();
263 final int external = name.indexOf(".");
264 if (external < 0) {
265 if (predicateExists(predicate)) {
266 return prop;
267 } else {
268 return null;
269 }
270 }
271 final String label = name.substring(0, external);
272 final ModuleReferenceList ref = prop.getRequiredModules();
273 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label);
274 if (newProp == null) {
275 return newProp;
276 }
277 final String shortName = name.substring(external + 1);
278 return newProp.getExistenceChecker().getQedeq(new PredicateKey(shortName, arguments));
279 }
280
281 public RuleKey getRuleKey(final String ruleName) {
282 RuleKey ruleKey = prop.getLabels().getRuleKey(ruleName);
283 final ModuleReferenceList ref = prop.getRequiredModules();
284 for (int i = 0; i < ref.size(); i++) {
285 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
286 final RuleKey found = newProp.getExistenceChecker().getRuleKey(ruleName);
287 if (found != null && found.getVersion() != null && (ruleKey == null
288 || ruleKey.getVersion() == null
289 || 0 < found.getVersion().compareTo(ruleKey.getVersion()))) {
290 ruleKey = found;
291 }
292 }
293 return ruleKey;
294 }
295
296 public RuleKey getParentRuleKey(final String ruleName) {
297 RuleKey ruleKey = null;
298 final ModuleReferenceList ref = prop.getRequiredModules();
299 for (int i = 0; i < ref.size(); i++) {
300 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
301 final RuleKey found = newProp.getExistenceChecker().getRuleKey(ruleName);
302 if (found != null && found.getVersion() != null && (ruleKey == null
303 || ruleKey.getVersion() == null
304 || 0 < found.getVersion().compareTo(ruleKey.getVersion()))) {
305 ruleKey = found;
306 }
307 }
308 return ruleKey;
309 }
310
311 public Rule get(final RuleKey ruleKey) {
312 final Rule local = super.get(ruleKey);
313 if (null != local) {
314 return local;
315 }
316 final ModuleReferenceList ref = prop.getRequiredModules();
317 for (int i = 0; i < ref.size(); i++) {
318 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
319 final Rule found = (newProp.getExistenceChecker().get(ruleKey));
320 if (found != null) {
321 return found;
322 }
323 }
324 return null;
325 }
326
327 public Map getRules() {
328 final Map result = new HashMap();
329 final Set keys = prop.getLabels().getRuleDefinitions().keySet();
330 final Iterator iter = keys.iterator();
331 while (iter.hasNext()) {
332 result.put(iter.next(), prop);
333 }
334 final ModuleReferenceList ref = prop.getRequiredModules();
335 for (int i = 0; i < ref.size(); i++) {
336 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
337 result.putAll(newProp.getExistenceChecker().getRules());
338 }
339 return result;
340 }
341
342 /**
343 * Get QEDEQ module where given rule is defined.
344 *
345 * @param ruleKey Rule we look for.
346 * @return QEDEQ module where rule is defined. Could be <code>null</code>.
347 */
348 public KernelQedeqBo getQedeq(final RuleKey ruleKey) {
349 if (super.get(ruleKey) != null) {
350 return prop;
351 }
352 final ModuleReferenceList ref = prop.getRequiredModules();
353 for (int i = 0; i < ref.size(); i++) {
354 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
355 final KernelQedeqBo found = (newProp.getExistenceChecker().getQedeq(ruleKey));
356 if (found != null) {
357 return found;
358 }
359 }
360 return null;
361 }
362
363 public boolean classOperatorExists() {
364 return classOperatorModule != null;
365 }
366
367 /**
368 * Set the identity operator.
369 *
370 * @param identityOperator Operator name. Might be <code>null</code>.
371 * @param identityOperatorModule In this module the identity operator is defined.
372 * @param context Here we are within the module.
373 * @throws IdentityOperatorAlreadyExistsException Already defined.
374 */
375 public void setIdentityOperatorDefined(final String identityOperator,
376 final KernelQedeqBo identityOperatorModule, final ModuleContext context)
377 throws IdentityOperatorAlreadyExistsException {
378 if (this.identityOperatorModule != null && identityOperatorModule != null) {
379 if (!this.identityOperatorModule.equals(identityOperatorModule)) {
380 throw new IdentityOperatorAlreadyExistsException(
381 LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_CODE,
382 LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_TEXT + " " + getIdentityOperator(),
383 context);
384 }
385 } else {
386 this.identityOperatorModule = identityOperatorModule;
387 super.setIdentityOperatorDefined(identityOperator);
388 }
389 }
390
391 public KernelQedeqBo getClassOperatorModule() {
392 return classOperatorModule;
393 }
394
395 public KernelQedeqBo getIdentityOperatorModule() {
396 return identityOperatorModule;
397 }
398
399 /**
400 * Set if the class operator is already defined.
401 *
402 * @param classOperatorModule Module where class operator is defined.
403 * @param context Context where we try to set new class operator.
404 * @throws ClassOperatorAlreadyExistsException Operator already defined.
405 */
406 public void setClassOperatorModule(final KernelQedeqBo classOperatorModule,
407 final ModuleContext context) throws ClassOperatorAlreadyExistsException {
408 if (this.classOperatorModule != null && classOperatorModule != null) {
409 // FIXME 20130109 m31: why do we have this if question? If we define
410 // the class operator twice in the same module we also want to get an error!
411 if (!this.classOperatorModule.equals(classOperatorModule)) {
412 throw new ClassOperatorAlreadyExistsException(
413 LogicErrors.CLASS_OPERATOR_ALREADY_DEFINED_CODE,
414 LogicErrors.CLASS_OPERATOR_ALREADY_DEFINED_TEXT
415 + this.classOperatorModule.getUrl(),
416 context);
417 }
418 } else {
419 this.classOperatorModule = classOperatorModule;
420 }
421 }
422
423 }
|