001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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 org.qedeq.kernel.bo.common.ModuleReferenceList;
019 import org.qedeq.kernel.bo.logic.common.ClassOperatorAlreadyExistsException;
020 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
021 import org.qedeq.kernel.bo.logic.common.FunctionKey;
022 import org.qedeq.kernel.bo.logic.common.IdentityOperatorAlreadyExistsException;
023 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
024 import org.qedeq.kernel.bo.logic.common.PredicateKey;
025 import org.qedeq.kernel.bo.module.KernelQedeqBo;
026 import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
027 import org.qedeq.kernel.se.common.ModuleContext;
028 import org.qedeq.kernel.se.common.ModuleDataException;
029
030
031 /**
032 * Checks if a predicate or function constant is defined.
033 *
034 * @author Michael Meyling
035 */
036 public class ModuleConstantsExistenceCheckerImpl extends DefaultExistenceChecker
037 implements ModuleConstantsExistenceChecker {
038
039 /** QEDEQ module properties. */
040 private final KernelQedeqBo prop;
041
042 /** In this module the class operator is defined. */
043 private KernelQedeqBo classOperatorModule;
044
045 /** In this class the identityOperator is defined. */
046 private KernelQedeqBo identityOperatorModule;
047
048 /**
049 * Constructor.
050 *
051 * @param prop QEDEQ module properties object.
052 * @throws ModuleDataException Referenced QEDEQ modules are already inconsistent: they doesn't
053 * mix.
054 */
055 public ModuleConstantsExistenceCheckerImpl(final KernelQedeqBo prop) throws ModuleDataException {
056 super();
057 this.prop = prop;
058 init();
059 }
060
061 /**
062 * Check if required QEDEQ modules mix without problems. If for example the identity operator
063 * is defined in two different modules in two different ways we have got a problem.
064 * Also the basic properties (for example
065 * {@link ModuleConstantsExistenceCheckerImpl#setIdentityOperatorDefined(String,
066 * KernelQedeqBo, ModuleContext)} and
067 * {@link ModuleConstantsExistenceCheckerImpl#setClassOperatorModule(KernelQedeqBo)}) are set accordingly.
068 *
069 * @throws ModuleDataException Required modules doesn't mix.
070 */
071 public final void init() throws ModuleDataException {
072 clear();
073 final ModuleReferenceList list = prop.getRequiredModules();
074 for (int i = 0; i < list.size(); i++) {
075 final KernelQedeqBo bo = (KernelQedeqBo) list
076 .getQedeqBo(i);
077 if (bo.getExistenceChecker().identityOperatorExists()) {
078 final String identityOperator = list.getLabel(i) + "."
079 + bo.getExistenceChecker().getIdentityOperator();
080 setIdentityOperatorDefined(identityOperator, bo.getExistenceChecker().getIdentityOperatorModule(),
081 list.getModuleContext(i));
082 }
083 if (bo.getExistenceChecker().classOperatorExists()) {
084 setClassOperatorModule(bo.getExistenceChecker().getClassOperatorModule(),
085 list.getModuleContext(i));
086 }
087 }
088 }
089
090 public boolean predicateExists(final PredicateKey predicate) {
091 final String name = predicate.getName();
092 final String arguments = predicate.getArguments();
093 final int external = name.indexOf('.');
094 if (external < 0) {
095 return super.predicateExists(predicate);
096 }
097 final String label = name.substring(0, external);
098 final ModuleReferenceList ref = prop.getRequiredModules();
099
100 final KernelQedeqBo newProp = (KernelQedeqBo) ref
101 .getQedeqBo(label);
102 if (newProp == null) {
103 return false;
104 }
105 final String shortName = name.substring(external + 1);
106 return newProp.getExistenceChecker().predicateExists(new PredicateKey(shortName, arguments));
107 }
108
109 public boolean functionExists(final FunctionKey function) {
110 final String name = function.getName();
111 final String arguments = function.getArguments();
112 final int external = name.indexOf(".");
113 if (external < 0) {
114 return super.functionExists(function);
115 }
116 final String label = name.substring(0, external);
117 final ModuleReferenceList ref = prop.getRequiredModules();
118 final KernelQedeqBo newProp = (KernelQedeqBo) ref
119 .getQedeqBo(label);
120 if (newProp == null) {
121 return false;
122 }
123 final String shortName = name.substring(external + 1);
124 return newProp.getExistenceChecker().functionExists(new FunctionKey(shortName, arguments));
125 }
126
127 public boolean isInitialPredicate(final PredicateKey predicate) {
128 final String name = predicate.getName();
129 final String arguments = predicate.getArguments();
130 final int external = name.indexOf('.');
131 if (external < 0) {
132 return super.isInitialPredicate(predicate);
133 }
134 final String label = name.substring(0, external);
135 final ModuleReferenceList ref = prop.getRequiredModules();
136
137 final KernelQedeqBo newProp = (KernelQedeqBo) ref
138 .getQedeqBo(label);
139 if (newProp == null) {
140 return false;
141 }
142 final String shortName = name.substring(external + 1);
143 return newProp.getExistenceChecker().isInitialPredicate(new PredicateKey(shortName, arguments));
144 }
145
146 public boolean isInitialFunction(final FunctionKey function) {
147 final String name = function.getName();
148 final String arguments = function.getArguments();
149 final int external = name.indexOf('.');
150 if (external < 0) {
151 return super.isInitialFunction(function);
152 }
153 final String label = name.substring(0, external);
154 final ModuleReferenceList ref = prop.getRequiredModules();
155
156 final KernelQedeqBo newProp = (KernelQedeqBo) ref
157 .getQedeqBo(label);
158 if (newProp == null) {
159 return false;
160 }
161 final String shortName = name.substring(external + 1);
162 return newProp.getExistenceChecker().isInitialFunction(new FunctionKey(shortName, arguments));
163 }
164
165 public PredicateConstant get(final PredicateKey predicate) {
166 final String name = predicate.getName();
167 final String arguments = predicate.getArguments();
168 final int external = name.indexOf('.');
169 if (external < 0) {
170 return super.get(predicate);
171 }
172 final String label = name.substring(0, external);
173 final ModuleReferenceList ref = prop.getRequiredModules();
174
175 final KernelQedeqBo newProp = (KernelQedeqBo) ref
176 .getQedeqBo(label);
177 if (newProp == null) {
178 return null;
179 }
180 final String shortName = name.substring(external + 1);
181 return newProp.getExistenceChecker().get(new PredicateKey(shortName, arguments));
182 }
183
184 public FunctionConstant get(final FunctionKey function) {
185 final String name = function.getName();
186 final String arguments = function.getArguments();
187 final int external = name.indexOf(".");
188 if (external < 0) {
189 return super.get(function);
190 }
191 final String label = name.substring(0, external);
192 final ModuleReferenceList ref = prop.getRequiredModules();
193 final KernelQedeqBo newProp = (KernelQedeqBo) ref
194 .getQedeqBo(label);
195 if (newProp == null) {
196 return null;
197 }
198 final String shortName = name.substring(external + 1);
199 return newProp.getExistenceChecker().get(new FunctionKey(shortName, arguments));
200 }
201
202 /**
203 * Get QEDEQ module where given function constant is defined.
204 *
205 * @param function Function we look for.
206 * @return QEDEQ module where function constant is defined.
207 */
208 public KernelQedeqBo getQedeq(final FunctionKey function) {
209 final String name = function.getName();
210 final String arguments = function.getArguments();
211 final int external = name.indexOf(".");
212 if (external < 0) {
213 if (functionExists(function)) {
214 return prop;
215 } else {
216 return null;
217 }
218 }
219 final String label = name.substring(0, external);
220 final ModuleReferenceList ref = prop.getRequiredModules();
221 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label);
222 if (newProp == null) {
223 return newProp;
224 }
225 final String shortName = name.substring(external + 1);
226 return newProp.getExistenceChecker().getQedeq(new FunctionKey(shortName, arguments));
227 }
228
229 /**
230 * Get QEDEQ module where given predicate constant is defined.
231 *
232 * @param predicate Predicate we look for.
233 * @return QEDEQ module where predicate constant is defined.x
234 */
235 public KernelQedeqBo getQedeq(final PredicateKey predicate) {
236 final String name = predicate.getName();
237 final String arguments = predicate.getArguments();
238 final int external = name.indexOf(".");
239 if (external < 0) {
240 if (predicateExists(predicate)) {
241 return prop;
242 } else {
243 return null;
244 }
245 }
246 final String label = name.substring(0, external);
247 final ModuleReferenceList ref = prop.getRequiredModules();
248 final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(label);
249 if (newProp == null) {
250 return newProp;
251 }
252 final String shortName = name.substring(external + 1);
253 return newProp.getExistenceChecker().getQedeq(new PredicateKey(shortName, arguments));
254 }
255
256 public boolean classOperatorExists() {
257 return classOperatorModule != null;
258 }
259
260 /**
261 * Set the identity operator.
262 *
263 * @param identityOperator Operator name. Might be <code>null</code>.
264 * @param identityOperatorModule In this module the identity operator is defined.
265 * @param context Here we are within the module.
266 * @throws IdentityOperatorAlreadyExistsException Already defined.
267 */
268 public void setIdentityOperatorDefined(final String identityOperator,
269 final KernelQedeqBo identityOperatorModule, final ModuleContext context)
270 throws IdentityOperatorAlreadyExistsException {
271 if (this.identityOperatorModule != null && identityOperatorModule != null) {
272 if (!this.identityOperatorModule.equals(identityOperatorModule)) {
273 throw new IdentityOperatorAlreadyExistsException(LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_CODE,
274 LogicErrors.IDENTITY_OPERATOR_ALREADY_EXISTS_TEXT + " " + getIdentityOperator(), context);
275 }
276 } else {
277 this.identityOperatorModule = identityOperatorModule;
278 super.setIdentityOperatorDefined(identityOperator);
279 }
280 }
281
282 public KernelQedeqBo getClassOperatorModule() {
283 return classOperatorModule;
284 }
285
286 public KernelQedeqBo getIdentityOperatorModule() {
287 return identityOperatorModule;
288 }
289
290 /**
291 * Set if the class operator is already defined.
292 *
293 * @param classOperatorModule Module where class operator is defined.
294 * @param context Context where we try to set new class operator.
295 * @throws ClassOperatorAlreadyExistsException Operator already defined.
296 */
297 public void setClassOperatorModule(final KernelQedeqBo classOperatorModule,
298 final ModuleContext context) throws ClassOperatorAlreadyExistsException {
299 if (this.classOperatorModule != null && classOperatorModule != null) {
300 if (!this.classOperatorModule.equals(classOperatorModule)) {
301 throw new ClassOperatorAlreadyExistsException(123478,
302 "class operator already defined within " + this.classOperatorModule.getUrl(),
303 context);
304 }
305 } else {
306 this.classOperatorModule = classOperatorModule;
307 }
308 }
309
310 }
|