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.module;
017
018 import java.util.Map;
019
020 import org.qedeq.kernel.bo.logic.common.ClassOperatorAlreadyExistsException;
021 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
022 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
023 import org.qedeq.kernel.bo.logic.common.FunctionKey;
024 import org.qedeq.kernel.bo.logic.common.IdentityOperatorAlreadyExistsException;
025 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
026 import org.qedeq.kernel.bo.logic.common.PredicateKey;
027 import org.qedeq.kernel.se.base.module.Rule;
028 import org.qedeq.kernel.se.common.ModuleContext;
029 import org.qedeq.kernel.se.common.RuleKey;
030
031 /**
032 * Contains methods for existence checking of various operands.
033 *
034 * @author Michael Meyling
035 */
036 public interface ModuleConstantsExistenceChecker extends ExistenceChecker {
037
038 public boolean predicateExists(final PredicateKey predicate);
039
040 public boolean functionExists(final FunctionKey function);
041
042 /**
043 * Get QEDEQ module where given function constant is defined.
044 *
045 * @param function Function we look for.
046 * @return QEDEQ module where function constant is defined.
047 */
048 public KernelQedeqBo getQedeq(final FunctionKey function);
049
050 /**
051 * Get QEDEQ module where given predicate constant is defined.
052 *
053 * @param predicate Predicate we look for.
054 * @return QEDEQ module where predicate constant is defined.x
055 */
056 public KernelQedeqBo getQedeq(final PredicateKey predicate);
057
058 /**
059 * Get QEDEQ module where given rule is defined.
060 *
061 * @param ruleKey Rule we look for.
062 * @return QEDEQ module where rule is defined.x
063 */
064 public KernelQedeqBo getQedeq(final RuleKey ruleKey);
065
066 /**
067 * Get maximum rule version that is defined in this or an imported module.
068 *
069 * @param ruleName Rule we look for.
070 * @return Rule key with maximum version.x
071 */
072 public RuleKey getRuleKey(final String ruleName);
073
074 /**
075 * Get maximum rule version that is defined in an imported module.
076 *
077 * @param ruleName Rule we look for.
078 * @return Rule key with maximum version.
079 */
080 public RuleKey getParentRuleKey(final String ruleName);
081
082 /**
083 * Get map of all {@link RuleKey}s defined in this module or in one of the imported ones.
084 *
085 * @return Map of all defined rule keys mapping from {@link RuleKey} to {@link KernelQedeqBo}.
086 */
087 public Map getRules();
088
089 public boolean classOperatorExists();
090
091 /**
092 * Set the identity operator.
093 *
094 * @param identityOperator Operator name. Might be <code>null</code>.
095 * @param identityOperatorModule In this module the identity operator is defined.
096 * @param context Here we are within the module.
097 * @throws IdentityOperatorAlreadyExistsException Already defined.
098 */
099 public void setIdentityOperatorDefined(final String identityOperator,
100 final KernelQedeqBo identityOperatorModule,
101 final ModuleContext context)
102 throws IdentityOperatorAlreadyExistsException;
103
104 /**
105 * Set if the class operator is already defined.
106 *
107 * @param classOperatorModule Module where class operator is defined.
108 * @param context Context where we try to set new class operator.
109 * @throws ClassOperatorAlreadyExistsException Operator already defined.
110 */
111 public void setClassOperatorModule(
112 final KernelQedeqBo classOperatorModule,
113 final ModuleContext context)
114 throws ClassOperatorAlreadyExistsException;
115
116 /**
117 * Get QEDEQ module where the class operator is defined within.
118 *
119 * @return Class operator defining module.
120 */
121 public KernelQedeqBo getClassOperatorModule();
122
123 /**
124 * Get QEDEQ module where the identity operator is defined within.
125 *
126 * @return Identity operator defining module.
127 */
128 public KernelQedeqBo getIdentityOperatorModule();
129
130 /**
131 * Get predicate constant definition.
132 *
133 * @param predicate Get definition of this predicate.
134 * @return Definition.
135 */
136 public PredicateConstant get(final PredicateKey predicate);
137
138 /**
139 * Get predicate constant definition.
140 *
141 * @param name Name of predicate.
142 * @param arguments Arguments of predicate.
143 * @return Definition. Might be <code>null</code>.
144 */
145 public PredicateConstant getPredicate(final String name, final int arguments);
146
147 /**
148 * Get function constant definition.
149 *
150 * @param function Get definition of this predicate.
151 * @return Definition. Might be <code>null</code>.
152 */
153 public FunctionConstant get(final FunctionKey function);
154
155 /**
156 * Get function constant definition.
157 *
158 * @param name Name of function.
159 * @param arguments Arguments of function.
160 * @return Definition. Might be <code>null</code>.
161 */
162 public FunctionConstant getFunction(final String name, final int arguments);
163
164 /**
165 * Get rule declaration.
166 *
167 * @param ruleKey Get definition of this rule.
168 * @return Rule. Might be <code>null</code>.
169 */
170 public Rule get(final RuleKey ruleKey);
171
172 }
|