View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">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 }