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 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 }
241 return null;
242 }
243 final String label = name.substring(0, external);
244 final ModuleReferenceList ref = prop.getRequiredModules();
245 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label);
246 if (newProp == null) {
247 return newProp;
248 }
249 final String shortName = name.substring(external + 1);
250 return newProp.getExistenceChecker().getQedeq(new FunctionKey(shortName, arguments));
251 }
252
253 /**
254 * Get QEDEQ module where given predicate constant is defined.
255 *
256 * @param predicate Predicate we look for.
257 * @return QEDEQ module where predicate constant is defined.x
258 */
259 public KernelQedeqBo getQedeq(final PredicateKey predicate) {
260 final String name = predicate.getName();
261 final String arguments = predicate.getArguments();
262 final int external = name.indexOf(".");
263 if (external < 0) {
264 if (predicateExists(predicate)) {
265 return prop;
266 }
267 return null;
268 }
269 final String label = name.substring(0, external);
270 final ModuleReferenceList ref = prop.getRequiredModules();
271 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label);
272 if (newProp == null) {
273 return newProp;
274 }
275 final String shortName = name.substring(external + 1);
276 return newProp.getExistenceChecker().getQedeq(new PredicateKey(shortName, arguments));
277 }
278
279 public RuleKey getRuleKey(final String ruleName) {
280 RuleKey ruleKey = prop.getLabels().getRuleKey(ruleName);
281 final ModuleReferenceList ref = prop.getRequiredModules();
282 for (int i = 0; i < ref.size(); i++) {
283 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
284 final RuleKey found = newProp.getExistenceChecker().getRuleKey(ruleName);
285 if (found != null && found.getVersion() != null && (ruleKey == null
286 || ruleKey.getVersion() == null
287 || 0 < found.getVersion().compareTo(ruleKey.getVersion()))) {
288 ruleKey = found;
289 }
290 }
291 return ruleKey;
292 }
293
294 public RuleKey getParentRuleKey(final String ruleName) {
295 RuleKey ruleKey = null;
296 final ModuleReferenceList ref = prop.getRequiredModules();
297 for (int i = 0; i < ref.size(); i++) {
298 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
299 final RuleKey found = newProp.getExistenceChecker().getRuleKey(ruleName);
300 if (found != null && found.getVersion() != null && (ruleKey == null
301 || ruleKey.getVersion() == null
302 || 0 < found.getVersion().compareTo(ruleKey.getVersion()))) {
303 ruleKey = found;
304 }
305 }
306 return ruleKey;
307 }
308
309 public Rule get(final RuleKey ruleKey) {
310 final Rule local = super.get(ruleKey);
311 if (null != local) {
312 return local;
313 }
314 final ModuleReferenceList ref = prop.getRequiredModules();
315 for (int i = 0; i < ref.size(); i++) {
316 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
317 final Rule found = (newProp.getExistenceChecker().get(ruleKey));
318 if (found != null) {
319 return found;
320 }
321 }
322 return null;
323 }
324
325 public Map getRules() {
326 final Map result = new HashMap();
327 final Set keys = prop.getLabels().getRuleDefinitions().keySet();
328 final Iterator iter = keys.iterator();
329 while (iter.hasNext()) {
330 result.put(iter.next(), prop);
331 }
332 final ModuleReferenceList ref = prop.getRequiredModules();
333 for (int i = 0; i < ref.size(); i++) {
334 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
335 result.putAll(newProp.getExistenceChecker().getRules());
336 }
337 return result;
338 }
339
340 /**
341 * Get QEDEQ module where given rule is defined.
342 *
343 * @param ruleKey Rule we look for.
344 * @return QEDEQ module where rule is defined. Could be <code>null</code>.
345 */
346 public KernelQedeqBo getQedeq(final RuleKey ruleKey) {
347 if (super.get(ruleKey) != null) {
348 return prop;
349 }
350 final ModuleReferenceList ref = prop.getRequiredModules();
351 for (int i = 0; i < ref.size(); i++) {
352 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
353 final KernelQedeqBo found = (newProp.getExistenceChecker().getQedeq(ruleKey));
354 if (found != null) {
355 return found;
356 }
357 }
358 return null;
359 }
360
361 public boolean classOperatorExists() {
362 return classOperatorModule != null;
363 }
364
365 /**
366 * Set the identity operator.
367 *
368 * @param identityOperator Operator name. Might be <code>null</code>.
369 * @param identityOperatorModule In this module the identity operator is defined.
370 * @param context Here we are within the module.
371 * @throws IdentityOperatorAlreadyExistsException Already defined.
372 */
373 public void setIdentityOperatorDefined(final String identityOperator,
374 final KernelQedeqBo identityOperatorModule, final ModuleContext context)
375 throws IdentityOperatorAlreadyExistsException {
376 if (this.identityOperatorModule != null && identityOperatorModule != null) {
377 if (!this.identityOperatorModule.equals(identityOperatorModule)) {
378 throw new IdentityOperatorAlreadyExistsException(
379 LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_CODE,
380 LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_TEXT + " " + getIdentityOperator(),
381 context);
382 }
383 } else {
384 this.identityOperatorModule = identityOperatorModule;
385 super.setIdentityOperatorDefined(identityOperator);
386 }
387 }
388
389 public KernelQedeqBo getClassOperatorModule() {
390 return classOperatorModule;
391 }
392
393 public KernelQedeqBo getIdentityOperatorModule() {
394 return identityOperatorModule;
395 }
396
397 /**
398 * Set if the class operator is already defined.
399 *
400 * @param classOperatorModule Module where class operator is defined.
401 * @param context Context where we try to set new class operator.
402 * @throws ClassOperatorAlreadyExistsException Operator already defined.
403 */
404 public void setClassOperatorModule(final KernelQedeqBo classOperatorModule,
405 final ModuleContext context) throws ClassOperatorAlreadyExistsException {
406 if (this.classOperatorModule != null && classOperatorModule != null) {
407 // FIXME 20130109 m31: why do we have this if question? If we define
408 // the class operator twice in the same module we also want to get an error!
409 if (!this.classOperatorModule.equals(classOperatorModule)) {
410 throw new ClassOperatorAlreadyExistsException(
411 LogicErrors.CLASS_OPERATOR_ALREADY_DEFINED_CODE,
412 LogicErrors.CLASS_OPERATOR_ALREADY_DEFINED_TEXT
413 + this.classOperatorModule.getUrl(),
414 context);
415 }
416 } else {
417 this.classOperatorModule = classOperatorModule;
418 }
419 }
420
421 }
|