1 | package org.qedeq.kernel.se.visitor; |
2 | |
3 | |
4 | /** |
5 | * Contains various counter values for a {@link org.qedeq.kernel.se.base.module.Qedeq}. |
6 | * |
7 | * @author Michael Meyling |
8 | */ |
9 | public class QedeqNumbers { |
10 | |
11 | /** Number of imports. */ |
12 | private int imports; |
13 | |
14 | /** Number of chapters. */ |
15 | private int chapters; |
16 | |
17 | /** Number of subsections (within current chapter). */ |
18 | private int sections; |
19 | |
20 | /** Number of subsections (within current section). */ |
21 | private int subsectionsAndNodes; |
22 | |
23 | /** Import we currently work on (or lastly visited). */ |
24 | private int importNumber; |
25 | |
26 | /** Chapter numbering currently on? */ |
27 | private boolean chapterNumbering; |
28 | |
29 | /** Chapter number the node is within. */ |
30 | private int chapterNumber; |
31 | |
32 | /** Absolute chapter number the node is within. Includes chapters with no numbers. */ |
33 | private int absoluteChapterNumber; |
34 | |
35 | /** Section numbering currently on? */ |
36 | private boolean sectionNumbering; |
37 | |
38 | /** Section number the node is within. */ |
39 | private int sectionNumber; |
40 | |
41 | /** Absolute section number the node is within. Includes sections with no numbers. */ |
42 | private int absoluteSectionNumber; |
43 | |
44 | /** Sub section number for section. */ |
45 | private int subsectionNumber; |
46 | |
47 | /** Node number the node for section. */ |
48 | private int nodeNumber; |
49 | |
50 | /** Axioms before node (including this one). */ |
51 | private int axiomNumber; |
52 | |
53 | /** Function definitions before node (including this one). */ |
54 | private int functionDefinitionNumber; |
55 | |
56 | /** Predicate definitions before node (including this one). */ |
57 | private int predicateDefinitionNumber; |
58 | |
59 | /** Propositions before node (including this one). */ |
60 | private int propositionNumber; |
61 | |
62 | /** Rule definitions before node (including this one). */ |
63 | private int ruleNumber; |
64 | |
65 | /** No further numbering will be done. */ |
66 | private boolean finished; |
67 | |
68 | /** |
69 | * Constructor. |
70 | * |
71 | * @param imports Number of imported QEDEQ modules. |
72 | * @param chapters Number of chapters in QEDEQ module. |
73 | */ |
74 | public QedeqNumbers(final int imports, final int chapters) { |
75 | this.imports = imports; |
76 | this.chapters = chapters; |
77 | } |
78 | |
79 | /** |
80 | * Copy constructor. |
81 | * |
82 | * @param original Original to copy values from. |
83 | */ |
84 | public QedeqNumbers(final QedeqNumbers original) { |
85 | imports = original.imports; |
86 | chapters = original.chapters; |
87 | sections = original.sections; |
88 | subsectionsAndNodes = original.subsectionsAndNodes; |
89 | importNumber = original.importNumber; |
90 | chapterNumbering = original.chapterNumbering; |
91 | chapterNumber = original.chapterNumber; |
92 | absoluteChapterNumber = original.absoluteChapterNumber; |
93 | sectionNumbering = original.sectionNumbering; |
94 | nodeNumber = original.nodeNumber; |
95 | sectionNumber = original.sectionNumber; |
96 | absoluteSectionNumber = original.absoluteSectionNumber; |
97 | subsectionNumber = original.subsectionNumber; |
98 | axiomNumber = original.axiomNumber; |
99 | functionDefinitionNumber = original.functionDefinitionNumber; |
100 | predicateDefinitionNumber = original.predicateDefinitionNumber; |
101 | propositionNumber = original.propositionNumber; |
102 | ruleNumber = original.ruleNumber; |
103 | finished = original.finished; |
104 | } |
105 | |
106 | /** |
107 | * Last import number. |
108 | * |
109 | * @return Import number. |
110 | */ |
111 | public int getImportNumber() { |
112 | return importNumber; |
113 | } |
114 | |
115 | /** |
116 | * Increase import number. |
117 | */ |
118 | public void increaseImportNumber() { |
119 | importNumber++; |
120 | } |
121 | |
122 | /** |
123 | * Chapter number the node is within. |
124 | * |
125 | * @return Chapter number. |
126 | */ |
127 | public int getChapterNumber() { |
128 | return chapterNumber; |
129 | } |
130 | |
131 | /** |
132 | * Increase chapter number. |
133 | * |
134 | * @param sections Number of subsections in new chapter. |
135 | * @param chapterNumbering Chapter numbering on? |
136 | */ |
137 | public void increaseChapterNumber(final int sections, final boolean chapterNumbering) { |
138 | this.chapterNumbering = chapterNumbering; |
139 | absoluteChapterNumber++; |
140 | if (chapterNumbering) { |
141 | chapterNumber++; |
142 | } |
143 | this.sections = sections; |
144 | this.subsectionsAndNodes = 0; |
145 | this.sectionNumber = 0; |
146 | this.absoluteSectionNumber = 0; |
147 | this.sectionNumbering = true; |
148 | this.subsectionNumber = 0; |
149 | this.nodeNumber = 0; |
150 | } |
151 | |
152 | /** |
153 | * Is chapter numbering currently on? |
154 | * |
155 | * @return Chapter numbering is on. |
156 | */ |
157 | public boolean isChapterNumbering() { |
158 | return chapterNumbering; |
159 | } |
160 | |
161 | /** |
162 | * Absolute chapter number the node is within. This includes chapters with no numbers. |
163 | * |
164 | * @return Chapter number. |
165 | */ |
166 | public int getAbsoluteChapterNumber() { |
167 | return absoluteChapterNumber; |
168 | } |
169 | |
170 | /** |
171 | * Section number the node is within. |
172 | * |
173 | * @return Section number. |
174 | */ |
175 | public int getSectionNumber() { |
176 | return sectionNumber; |
177 | } |
178 | |
179 | /** |
180 | * Increase chapter number. |
181 | * |
182 | * @param subsectionsAndNodes Number of subsections and nodes for current section. |
183 | * @param sectionNumbering Should this section be numbered? |
184 | */ |
185 | public void increaseSectionNumber(final int subsectionsAndNodes, |
186 | final boolean sectionNumbering) { |
187 | this.subsectionsAndNodes = subsectionsAndNodes; |
188 | this.sectionNumbering = sectionNumbering; |
189 | absoluteSectionNumber++; |
190 | if (sectionNumbering) { |
191 | sectionNumber++; |
192 | } |
193 | subsectionNumber = 0; |
194 | nodeNumber = 0; |
195 | } |
196 | |
197 | /** |
198 | * Absolute section number the node is within. This includes sections with no numbers. |
199 | * |
200 | * @return Section number. |
201 | */ |
202 | public int getAbsoluteSectionNumber() { |
203 | return absoluteSectionNumber; |
204 | } |
205 | |
206 | /** |
207 | * Is section numbering currently on? |
208 | * |
209 | * @return Section numbering is on. |
210 | */ |
211 | public boolean isSectionNumbering() { |
212 | return sectionNumbering; |
213 | } |
214 | |
215 | /** |
216 | * Sub section number within section. |
217 | * |
218 | * @return Sub section number. |
219 | */ |
220 | public int getSubsectionNumber() { |
221 | return subsectionNumber; |
222 | } |
223 | |
224 | /** |
225 | * Increase subsection number. |
226 | */ |
227 | public void increaseSubsectionNumber() { |
228 | subsectionNumber++; |
229 | } |
230 | |
231 | /** |
232 | * Node number within section. |
233 | * |
234 | * @return Node number. |
235 | */ |
236 | public int getNodeNumber() { |
237 | return nodeNumber; |
238 | } |
239 | |
240 | /** |
241 | * Increase node number. |
242 | */ |
243 | public void increaseNodeNumber() { |
244 | nodeNumber++; |
245 | } |
246 | |
247 | /** |
248 | * Get number of axioms before node (including this one). |
249 | * |
250 | * @return Number of axioms before node (including this one). |
251 | */ |
252 | public int getAxiomNumber() { |
253 | return axiomNumber; |
254 | } |
255 | |
256 | /** |
257 | * Increase number of axioms before node (including this one). |
258 | */ |
259 | public void increaseAxiomNumber() { |
260 | axiomNumber++; |
261 | } |
262 | |
263 | /** |
264 | * Get number of function definitions before node (including this one). |
265 | * |
266 | * @return Number function definitions before node (including this one). |
267 | */ |
268 | public int getFunctionDefinitionNumber() { |
269 | return functionDefinitionNumber; |
270 | } |
271 | |
272 | /** |
273 | * Increase number of function definitions before node (including this one). |
274 | */ |
275 | public void increaseFunctionDefinitionNumber() { |
276 | functionDefinitionNumber++; |
277 | } |
278 | |
279 | /** |
280 | * Get number of predicate definitions before node (including this one). |
281 | * |
282 | * @return Number of predicate definitions before node (including this one). |
283 | */ |
284 | public int getPredicateDefinitionNumber() { |
285 | return predicateDefinitionNumber; |
286 | } |
287 | |
288 | /** |
289 | * Increase number of predicate definitions before node (including this one). |
290 | */ |
291 | public void increasePredicateDefinitionNumber() { |
292 | predicateDefinitionNumber++; |
293 | } |
294 | |
295 | /** |
296 | * Get number of Propositions before node (including this one). |
297 | * |
298 | * @return Get number of Propositions before node (including this one). |
299 | */ |
300 | public int getPropositionNumber() { |
301 | return propositionNumber; |
302 | } |
303 | |
304 | /** |
305 | * Increase number of predicate definitions before node (including this one). |
306 | */ |
307 | public void increasePropositionNumber() { |
308 | propositionNumber++; |
309 | } |
310 | |
311 | /** |
312 | * Get number of rule definitions before node (including this one). |
313 | * |
314 | * @return Number of rule definitions before node (including this one). |
315 | */ |
316 | public int getRuleNumber() { |
317 | return ruleNumber; |
318 | } |
319 | |
320 | /** |
321 | * Increase number of rule definitions before node (including this one). |
322 | */ |
323 | public void increaseRuleNumber() { |
324 | ruleNumber++; |
325 | } |
326 | |
327 | /** |
328 | * Is there nothing more to be numbered? |
329 | * |
330 | * @return There will be no more number changes. |
331 | */ |
332 | public boolean isFinished() { |
333 | return finished; |
334 | } |
335 | |
336 | /** |
337 | * Set if numbering has ended. |
338 | * |
339 | * @param finished Will there be no more number changes? |
340 | */ |
341 | public void setFinished(final boolean finished) { |
342 | this.finished = finished; |
343 | } |
344 | |
345 | /** |
346 | * Get calculated visit percentage. |
347 | * This is a monotonically nondecreasing visit function. |
348 | * |
349 | * @return Value between 0 and 100. |
350 | */ |
351 | public double getVisitPercentage() { |
352 | if (finished) { |
353 | return 100; |
354 | } |
355 | double result = (double) (importNumber) / (imports + 1) / (chapters + 3); |
356 | result += (double) (absoluteChapterNumber) / (chapters + 3); |
357 | result += (double) (absoluteSectionNumber) / (sections + 2) / (chapters + 3); |
358 | result += (double) (subsectionNumber + nodeNumber) |
359 | / (subsectionsAndNodes + 2) / (sections + 2) / (chapters + 3); |
360 | return 100 * result; |
361 | } |
362 | |
363 | public boolean equals(final Object compare) { |
364 | if (!(compare instanceof QedeqNumbers)) { |
365 | return false; |
366 | } |
367 | final QedeqNumbers other = (QedeqNumbers) compare; |
368 | return imports == other.imports && importNumber == other.importNumber |
369 | && chapterNumbering == other.chapterNumbering |
370 | && absoluteChapterNumber == other.absoluteChapterNumber |
371 | && sectionNumbering == other.sectionNumbering |
372 | && sections == other.sections |
373 | && absoluteSectionNumber == other.absoluteSectionNumber |
374 | && subsectionNumber == other.subsectionNumber |
375 | && nodeNumber == other.nodeNumber |
376 | && axiomNumber == other.axiomNumber |
377 | && propositionNumber == other.propositionNumber |
378 | && predicateDefinitionNumber == other.predicateDefinitionNumber |
379 | && functionDefinitionNumber == other.functionDefinitionNumber |
380 | && ruleNumber == other.ruleNumber; |
381 | } |
382 | |
383 | public int hashCode() { |
384 | return imports ^ (importNumber * 4) |
385 | ^ (chapters * 16) ^ (absoluteChapterNumber * 64) |
386 | ^ (sections * 256) ^ (absoluteSectionNumber * 1024) |
387 | ^ (subsectionsAndNodes * 4096) ^ (nodeNumber * 16384) ^ (subsectionNumber * 65536) |
388 | ^ (axiomNumber * 262144) ^ (propositionNumber * 1048576) |
389 | ^ (predicateDefinitionNumber * 4194304) |
390 | ^ (functionDefinitionNumber * 16777216) ^ (ruleNumber * 67108864); |
391 | } |
392 | |
393 | public String toString() { |
394 | return "(" + importNumber + "/" + imports + " I) " |
395 | + "(" + absoluteChapterNumber + "/" + chapters + " C) " |
396 | + "(" + absoluteSectionNumber + "/" + sections + " S) " |
397 | + "(" + (subsectionNumber + nodeNumber) + "/" + subsectionsAndNodes + ")"; |
398 | } |
399 | |
400 | } |