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 | import java.util.Set; |
22 | |
23 | import org.qedeq.kernel.bo.common.ModuleReferenceList; |
24 | import org.qedeq.kernel.bo.logic.common.ClassOperatorAlreadyExistsException; |
25 | import org.qedeq.kernel.bo.logic.common.FunctionConstant; |
26 | import org.qedeq.kernel.bo.logic.common.FunctionKey; |
27 | import org.qedeq.kernel.bo.logic.common.IdentityOperatorAlreadyExistsException; |
28 | import org.qedeq.kernel.bo.logic.common.PredicateConstant; |
29 | import org.qedeq.kernel.bo.logic.common.PredicateKey; |
30 | import org.qedeq.kernel.bo.module.KernelQedeqBo; |
31 | import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker; |
32 | import org.qedeq.kernel.se.base.module.Rule; |
33 | import org.qedeq.kernel.se.common.IllegalModuleDataException; |
34 | import org.qedeq.kernel.se.common.ModuleContext; |
35 | import org.qedeq.kernel.se.common.ModuleDataException; |
36 | import org.qedeq.kernel.se.common.RuleKey; |
37 | |
38 | |
39 | /** |
40 | * Checks if a predicate or function constant is defined. |
41 | * |
42 | * @author Michael Meyling |
43 | */ |
44 | public class ModuleConstantsExistenceCheckerImpl extends DefaultExistenceChecker |
45 | implements ModuleConstantsExistenceChecker { |
46 | |
47 | /** QEDEQ module properties. */ |
48 | private final KernelQedeqBo prop; |
49 | |
50 | /** In this module the class operator is defined. */ |
51 | private KernelQedeqBo classOperatorModule; |
52 | |
53 | /** In this class the identityOperator is defined. */ |
54 | private KernelQedeqBo identityOperatorModule; |
55 | |
56 | /** |
57 | * Constructor. |
58 | * |
59 | * @param prop QEDEQ module properties object. |
60 | * @throws ModuleDataException Referenced QEDEQ modules are already inconsistent: they doesn't |
61 | * mix. |
62 | */ |
63 | public ModuleConstantsExistenceCheckerImpl(final KernelQedeqBo prop) throws ModuleDataException { |
64 | super(); |
65 | this.prop = prop; |
66 | init(); |
67 | } |
68 | |
69 | /** |
70 | * Check if required QEDEQ modules mix without problems. If for example the identity operator |
71 | * is defined in two different modules in two different ways we have got a problem. |
72 | * Also the basic properties (for example |
73 | * {@link ModuleConstantsExistenceCheckerImpl#setIdentityOperatorDefined(String, |
74 | * KernelQedeqBo, ModuleContext)} and |
75 | * {@link ModuleConstantsExistenceCheckerImpl#setClassOperatorModule(KernelQedeqBo)}) are set accordingly. |
76 | * |
77 | * @throws ModuleDataException Required modules doesn't mix. |
78 | */ |
79 | public final void init() throws ModuleDataException { |
80 | clear(); |
81 | final ModuleReferenceList list = prop.getRequiredModules(); |
82 | final Map rules = new HashMap(); |
83 | for (int i = 0; i < list.size(); i++) { |
84 | final KernelQedeqBo bo = (KernelQedeqBo) list |
85 | .getQedeqBo(i); |
86 | if (bo.getExistenceChecker().identityOperatorExists()) { |
87 | final String identityOperator = list.getLabel(i) + "." |
88 | + bo.getExistenceChecker().getIdentityOperator(); |
89 | setIdentityOperatorDefined(identityOperator, |
90 | bo.getExistenceChecker().getIdentityOperatorModule(), |
91 | list.getModuleContext(i)); |
92 | } |
93 | if (bo.getExistenceChecker().classOperatorExists()) { |
94 | setClassOperatorModule(bo.getExistenceChecker().getClassOperatorModule(), |
95 | list.getModuleContext(i)); |
96 | } |
97 | final Map cut = bo.getExistenceChecker().getRules(); |
98 | final Iterator iter = cut.entrySet().iterator(); |
99 | while (iter.hasNext()) { |
100 | final Map.Entry entry = (Map.Entry) iter.next(); |
101 | final RuleKey key = (RuleKey) entry.getKey(); |
102 | if (rules.containsKey(key) && !rules.get(key).equals(entry.getValue())) { |
103 | throw new IllegalModuleDataException( |
104 | LogicErrors.RULE_DEFINITIONS_DONT_MIX_CODE, |
105 | LogicErrors.RULE_DEFINITIONS_DONT_MIX_TEXT + key + " in " |
106 | + ((KernelQedeqBo) rules.get(key)).getLabels().getRuleContext(key), |
107 | list.getModuleContext(i), |
108 | getQedeq(key).getLabels().getRuleContext(key)); |
109 | } |
110 | } |
111 | rules.putAll(bo.getExistenceChecker().getRules()); |
112 | } |
113 | } |
114 | |
115 | public boolean predicateExists(final PredicateKey predicate) { |
116 | final String name = predicate.getName(); |
117 | final String arguments = predicate.getArguments(); |
118 | final int external = name.indexOf('.'); |
119 | if (external < 0) { |
120 | return super.predicateExists(predicate); |
121 | } |
122 | final String label = name.substring(0, external); |
123 | final ModuleReferenceList ref = prop.getRequiredModules(); |
124 | |
125 | final KernelQedeqBo newProp = (KernelQedeqBo) ref |
126 | .getQedeqBo(label); |
127 | if (newProp == null) { |
128 | return false; |
129 | } |
130 | final String shortName = name.substring(external + 1); |
131 | return newProp.getExistenceChecker().predicateExists(new PredicateKey(shortName, arguments)); |
132 | } |
133 | |
134 | public boolean functionExists(final FunctionKey function) { |
135 | final String name = function.getName(); |
136 | final String arguments = function.getArguments(); |
137 | final int external = name.indexOf("."); |
138 | if (external < 0) { |
139 | return super.functionExists(function); |
140 | } |
141 | final String label = name.substring(0, external); |
142 | final ModuleReferenceList ref = prop.getRequiredModules(); |
143 | final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label); |
144 | if (newProp == null) { |
145 | return false; |
146 | } |
147 | final String shortName = name.substring(external + 1); |
148 | return newProp.getExistenceChecker().functionExists(new FunctionKey(shortName, arguments)); |
149 | } |
150 | |
151 | public boolean isInitialPredicate(final PredicateKey predicate) { |
152 | final String name = predicate.getName(); |
153 | final String arguments = predicate.getArguments(); |
154 | final int external = name.indexOf('.'); |
155 | if (external < 0) { |
156 | return super.isInitialPredicate(predicate); |
157 | } |
158 | final String label = name.substring(0, external); |
159 | final ModuleReferenceList ref = prop.getRequiredModules(); |
160 | |
161 | final KernelQedeqBo newProp = (KernelQedeqBo) ref |
162 | .getQedeqBo(label); |
163 | if (newProp == null) { |
164 | return false; |
165 | } |
166 | final String shortName = name.substring(external + 1); |
167 | return newProp.getExistenceChecker().isInitialPredicate( |
168 | new PredicateKey(shortName, arguments)); |
169 | } |
170 | |
171 | public boolean isInitialFunction(final FunctionKey function) { |
172 | final String name = function.getName(); |
173 | final String arguments = function.getArguments(); |
174 | final int external = name.indexOf('.'); |
175 | if (external < 0) { |
176 | return super.isInitialFunction(function); |
177 | } |
178 | final String label = name.substring(0, external); |
179 | final ModuleReferenceList ref = prop.getRequiredModules(); |
180 | |
181 | final KernelQedeqBo newProp = (KernelQedeqBo) ref |
182 | .getQedeqBo(label); |
183 | if (newProp == null) { |
184 | return false; |
185 | } |
186 | final String shortName = name.substring(external + 1); |
187 | return newProp.getExistenceChecker().isInitialFunction( |
188 | new FunctionKey(shortName, arguments)); |
189 | } |
190 | |
191 | public PredicateConstant get(final PredicateKey predicate) { |
192 | final String name = predicate.getName(); |
193 | final String arguments = predicate.getArguments(); |
194 | final int external = name.indexOf('.'); |
195 | if (external < 0) { |
196 | return super.get(predicate); |
197 | } |
198 | final String label = name.substring(0, external); |
199 | final ModuleReferenceList ref = prop.getRequiredModules(); |
200 | |
201 | final KernelQedeqBo newProp = (KernelQedeqBo) ref |
202 | .getQedeqBo(label); |
203 | if (newProp == null) { |
204 | return null; |
205 | } |
206 | final String shortName = name.substring(external + 1); |
207 | return newProp.getExistenceChecker().get(new PredicateKey(shortName, arguments)); |
208 | } |
209 | |
210 | public FunctionConstant get(final FunctionKey function) { |
211 | final String name = function.getName(); |
212 | final String arguments = function.getArguments(); |
213 | final int external = name.indexOf("."); |
214 | if (external < 0) { |
215 | return super.get(function); |
216 | } |
217 | final String label = name.substring(0, external); |
218 | final ModuleReferenceList ref = prop.getRequiredModules(); |
219 | final KernelQedeqBo newProp = (KernelQedeqBo) ref |
220 | .getQedeqBo(label); |
221 | if (newProp == null) { |
222 | return null; |
223 | } |
224 | final String shortName = name.substring(external + 1); |
225 | return newProp.getExistenceChecker().get(new FunctionKey(shortName, arguments)); |
226 | } |
227 | |
228 | /** |
229 | * Get QEDEQ module where given function constant is defined. |
230 | * |
231 | * @param function Function we look for. |
232 | * @return QEDEQ module where function constant is defined. |
233 | */ |
234 | public KernelQedeqBo getQedeq(final FunctionKey function) { |
235 | final String name = function.getName(); |
236 | final String arguments = function.getArguments(); |
237 | final int external = name.indexOf("."); |
238 | if (external < 0) { |
239 | if (functionExists(function)) { |
240 | return prop; |
241 | } |
242 | return null; |
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 | } |
268 | return null; |
269 | } |
270 | final String label = name.substring(0, external); |
271 | final ModuleReferenceList ref = prop.getRequiredModules(); |
272 | final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label); |
273 | if (newProp == null) { |
274 | return newProp; |
275 | } |
276 | final String shortName = name.substring(external + 1); |
277 | return newProp.getExistenceChecker().getQedeq(new PredicateKey(shortName, arguments)); |
278 | } |
279 | |
280 | public RuleKey getRuleKey(final String ruleName) { |
281 | RuleKey ruleKey = prop.getLabels().getRuleKey(ruleName); |
282 | final ModuleReferenceList ref = prop.getRequiredModules(); |
283 | for (int i = 0; i < ref.size(); i++) { |
284 | final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i); |
285 | final RuleKey found = newProp.getExistenceChecker().getRuleKey(ruleName); |
286 | if (found != null && found.getVersion() != null && (ruleKey == null |
287 | || ruleKey.getVersion() == null |
288 | || 0 < found.getVersion().compareTo(ruleKey.getVersion()))) { |
289 | ruleKey = found; |
290 | } |
291 | } |
292 | return ruleKey; |
293 | } |
294 | |
295 | public RuleKey getParentRuleKey(final String ruleName) { |
296 | RuleKey ruleKey = null; |
297 | final ModuleReferenceList ref = prop.getRequiredModules(); |
298 | for (int i = 0; i < ref.size(); i++) { |
299 | final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i); |
300 | final RuleKey found = newProp.getExistenceChecker().getRuleKey(ruleName); |
301 | if (found != null && found.getVersion() != null && (ruleKey == null |
302 | || ruleKey.getVersion() == null |
303 | || 0 < found.getVersion().compareTo(ruleKey.getVersion()))) { |
304 | ruleKey = found; |
305 | } |
306 | } |
307 | return ruleKey; |
308 | } |
309 | |
310 | public Rule get(final RuleKey ruleKey) { |
311 | final Rule local = super.get(ruleKey); |
312 | if (null != local) { |
313 | return local; |
314 | } |
315 | final ModuleReferenceList ref = prop.getRequiredModules(); |
316 | for (int i = 0; i < ref.size(); i++) { |
317 | final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i); |
318 | final Rule found = (newProp.getExistenceChecker().get(ruleKey)); |
319 | if (found != null) { |
320 | return found; |
321 | } |
322 | } |
323 | return null; |
324 | } |
325 | |
326 | public Map getRules() { |
327 | final Map result = new HashMap(); |
328 | final Set keys = prop.getLabels().getRuleDefinitions().keySet(); |
329 | final Iterator iter = keys.iterator(); |
330 | while (iter.hasNext()) { |
331 | result.put(iter.next(), prop); |
332 | } |
333 | final ModuleReferenceList ref = prop.getRequiredModules(); |
334 | for (int i = 0; i < ref.size(); i++) { |
335 | final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i); |
336 | result.putAll(newProp.getExistenceChecker().getRules()); |
337 | } |
338 | return result; |
339 | } |
340 | |
341 | /** |
342 | * Get QEDEQ module where given rule is defined. |
343 | * |
344 | * @param ruleKey Rule we look for. |
345 | * @return QEDEQ module where rule is defined. Could be <code>null</code>. |
346 | */ |
347 | public KernelQedeqBo getQedeq(final RuleKey ruleKey) { |
348 | if (super.get(ruleKey) != null) { |
349 | return prop; |
350 | } |
351 | final ModuleReferenceList ref = prop.getRequiredModules(); |
352 | for (int i = 0; i < ref.size(); i++) { |
353 | final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i); |
354 | final KernelQedeqBo found = (newProp.getExistenceChecker().getQedeq(ruleKey)); |
355 | if (found != null) { |
356 | return found; |
357 | } |
358 | } |
359 | return null; |
360 | } |
361 | |
362 | public boolean classOperatorExists() { |
363 | return classOperatorModule != null; |
364 | } |
365 | |
366 | /** |
367 | * Set the identity operator. |
368 | * |
369 | * @param identityOperator Operator name. Might be <code>null</code>. |
370 | * @param identityOperatorModule In this module the identity operator is defined. |
371 | * @param context Here we are within the module. |
372 | * @throws IdentityOperatorAlreadyExistsException Already defined. |
373 | */ |
374 | public void setIdentityOperatorDefined(final String identityOperator, |
375 | final KernelQedeqBo identityOperatorModule, final ModuleContext context) |
376 | throws IdentityOperatorAlreadyExistsException { |
377 | if (this.identityOperatorModule != null && identityOperatorModule != null) { |
378 | if (!this.identityOperatorModule.equals(identityOperatorModule)) { |
379 | throw new IdentityOperatorAlreadyExistsException( |
380 | LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_CODE, |
381 | LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_TEXT + " " + getIdentityOperator(), |
382 | context); |
383 | } |
384 | } else { |
385 | this.identityOperatorModule = identityOperatorModule; |
386 | super.setIdentityOperatorDefined(identityOperator); |
387 | } |
388 | } |
389 | |
390 | public KernelQedeqBo getClassOperatorModule() { |
391 | return classOperatorModule; |
392 | } |
393 | |
394 | public KernelQedeqBo getIdentityOperatorModule() { |
395 | return identityOperatorModule; |
396 | } |
397 | |
398 | /** |
399 | * Set if the class operator is already defined. |
400 | * |
401 | * @param classOperatorModule Module where class operator is defined. |
402 | * @param context Context where we try to set new class operator. |
403 | * @throws ClassOperatorAlreadyExistsException Operator already defined. |
404 | */ |
405 | public void setClassOperatorModule(final KernelQedeqBo classOperatorModule, |
406 | final ModuleContext context) throws ClassOperatorAlreadyExistsException { |
407 | if (this.classOperatorModule != null && classOperatorModule != null) { |
408 | // FIXME 20130109 m31: why do we have this if question? If we define |
409 | // the class operator twice in the same module we also want to get an error! |
410 | if (!this.classOperatorModule.equals(classOperatorModule)) { |
411 | throw new ClassOperatorAlreadyExistsException( |
412 | LogicErrors.CLASS_OPERATOR_ALREADY_DEFINED_CODE, |
413 | LogicErrors.CLASS_OPERATOR_ALREADY_DEFINED_TEXT |
414 | + this.classOperatorModule.getUrl(), |
415 | context); |
416 | } |
417 | } else { |
418 | this.classOperatorModule = classOperatorModule; |
419 | } |
420 | } |
421 | |
422 | } |