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.module;
17
18 import java.util.Map;
19
20 import org.qedeq.kernel.bo.logic.common.ClassOperatorAlreadyExistsException;
21 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
22 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
23 import org.qedeq.kernel.bo.logic.common.FunctionKey;
24 import org.qedeq.kernel.bo.logic.common.IdentityOperatorAlreadyExistsException;
25 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
26 import org.qedeq.kernel.bo.logic.common.PredicateKey;
27 import org.qedeq.kernel.se.base.module.Rule;
28 import org.qedeq.kernel.se.common.ModuleContext;
29 import org.qedeq.kernel.se.common.RuleKey;
30
31 /**
32 * Contains methods for existence checking of various operands.
33 *
34 * @author Michael Meyling
35 */
36 public interface ModuleConstantsExistenceChecker extends ExistenceChecker {
37
38 public boolean predicateExists(final PredicateKey predicate);
39
40 public boolean functionExists(final FunctionKey function);
41
42 /**
43 * Get QEDEQ module where given function constant is defined.
44 *
45 * @param function Function we look for.
46 * @return QEDEQ module where function constant is defined.
47 */
48 public KernelQedeqBo getQedeq(final FunctionKey function);
49
50 /**
51 * Get QEDEQ module where given predicate constant is defined.
52 *
53 * @param predicate Predicate we look for.
54 * @return QEDEQ module where predicate constant is defined.x
55 */
56 public KernelQedeqBo getQedeq(final PredicateKey predicate);
57
58 /**
59 * Get QEDEQ module where given rule is defined.
60 *
61 * @param ruleKey Rule we look for.
62 * @return QEDEQ module where rule is defined.x
63 */
64 public KernelQedeqBo getQedeq(final RuleKey ruleKey);
65
66 /**
67 * Get maximum rule version that is defined in this or an imported module.
68 *
69 * @param ruleName Rule we look for.
70 * @return Rule key with maximum version.x
71 */
72 public RuleKey getRuleKey(final String ruleName);
73
74 /**
75 * Get maximum rule version that is defined in an imported module.
76 *
77 * @param ruleName Rule we look for.
78 * @return Rule key with maximum version.
79 */
80 public RuleKey getParentRuleKey(final String ruleName);
81
82 /**
83 * Get map of all {@link RuleKey}s defined in this module or in one of the imported ones.
84 *
85 * @return Map of all defined rule keys mapping from {@link RuleKey} to {@link KernelQedeqBo}.
86 */
87 public Map getRules();
88
89 public boolean classOperatorExists();
90
91 /**
92 * Set the identity operator.
93 *
94 * @param identityOperator Operator name. Might be <code>null</code>.
95 * @param identityOperatorModule In this module the identity operator is defined.
96 * @param context Here we are within the module.
97 * @throws IdentityOperatorAlreadyExistsException Already defined.
98 */
99 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 }