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.se.visitor;
17
18 import org.qedeq.kernel.se.base.list.Atom;
19 import org.qedeq.kernel.se.base.list.Element;
20 import org.qedeq.kernel.se.base.list.ElementList;
21 import org.qedeq.kernel.se.base.module.Add;
22 import org.qedeq.kernel.se.base.module.Author;
23 import org.qedeq.kernel.se.base.module.AuthorList;
24 import org.qedeq.kernel.se.base.module.Axiom;
25 import org.qedeq.kernel.se.base.module.ChangedRule;
26 import org.qedeq.kernel.se.base.module.ChangedRuleList;
27 import org.qedeq.kernel.se.base.module.Chapter;
28 import org.qedeq.kernel.se.base.module.ChapterList;
29 import org.qedeq.kernel.se.base.module.Conclusion;
30 import org.qedeq.kernel.se.base.module.ConditionalProof;
31 import org.qedeq.kernel.se.base.module.Existential;
32 import org.qedeq.kernel.se.base.module.FormalProof;
33 import org.qedeq.kernel.se.base.module.FormalProofLine;
34 import org.qedeq.kernel.se.base.module.FormalProofLineList;
35 import org.qedeq.kernel.se.base.module.FormalProofList;
36 import org.qedeq.kernel.se.base.module.Formula;
37 import org.qedeq.kernel.se.base.module.FunctionDefinition;
38 import org.qedeq.kernel.se.base.module.Header;
39 import org.qedeq.kernel.se.base.module.Hypothesis;
40 import org.qedeq.kernel.se.base.module.Import;
41 import org.qedeq.kernel.se.base.module.ImportList;
42 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
43 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
44 import org.qedeq.kernel.se.base.module.Latex;
45 import org.qedeq.kernel.se.base.module.LatexList;
46 import org.qedeq.kernel.se.base.module.LinkList;
47 import org.qedeq.kernel.se.base.module.LiteratureItem;
48 import org.qedeq.kernel.se.base.module.LiteratureItemList;
49 import org.qedeq.kernel.se.base.module.Location;
50 import org.qedeq.kernel.se.base.module.LocationList;
51 import org.qedeq.kernel.se.base.module.ModusPonens;
52 import org.qedeq.kernel.se.base.module.Node;
53 import org.qedeq.kernel.se.base.module.PredicateDefinition;
54 import org.qedeq.kernel.se.base.module.Proof;
55 import org.qedeq.kernel.se.base.module.ProofList;
56 import org.qedeq.kernel.se.base.module.Proposition;
57 import org.qedeq.kernel.se.base.module.Qedeq;
58 import org.qedeq.kernel.se.base.module.Reason;
59 import org.qedeq.kernel.se.base.module.Rename;
60 import org.qedeq.kernel.se.base.module.Rule;
61 import org.qedeq.kernel.se.base.module.Section;
62 import org.qedeq.kernel.se.base.module.SectionList;
63 import org.qedeq.kernel.se.base.module.Specification;
64 import org.qedeq.kernel.se.base.module.Subsection;
65 import org.qedeq.kernel.se.base.module.SubsectionList;
66 import org.qedeq.kernel.se.base.module.SubstFree;
67 import org.qedeq.kernel.se.base.module.SubstFunc;
68 import org.qedeq.kernel.se.base.module.SubstPred;
69 import org.qedeq.kernel.se.base.module.Term;
70 import org.qedeq.kernel.se.base.module.Universal;
71 import org.qedeq.kernel.se.base.module.UsedByList;
72 import org.qedeq.kernel.se.common.ModuleContext;
73 import org.qedeq.kernel.se.common.ModuleDataException;
74
75 /**
76 * Traverse a QEDEQ module and visit all elements.
77 * All contained elements are called recursively.
78 * See {@link org.qedeq.kernel.se.visitor.QedeqVisitor}.
79 *
80 * @author Michael Meyling
81 */
82 public interface QedeqTraverser {
83
84
85 /**
86 * Get current context within original. Remember to use the copy constructor
87 * when trying to remember this context!
88 *
89 * @return Current context.
90 */
91 public ModuleContext getCurrentContext();
92
93
94 /**
95 * Start with the top structure of a QEDEQ module.
96 *
97 * @param qedeq Traverse this element. Must not be <code>null</code>.
98 * @throws ModuleDataException Severe error during occurred.
99 */
100 public void accept(final Qedeq qedeq) throws ModuleDataException;
101
102 /**
103 * Traverse header.
104 *
105 * @param header Traverse this element.
106 * @throws ModuleDataException Severe error during occurred.
107 */
108 public void accept(final Header header) throws ModuleDataException;
109
110 /**
111 * Traverse used by list.
112 *
113 * @param usedByList Traverse this element.
114 * @throws ModuleDataException Severe error during occurred.
115 */
116 public void accept(final UsedByList usedByList) throws ModuleDataException;
117
118 /**
119 * Traverse import list.
120 *
121 * @param importList Traverse this element.
122 * @throws ModuleDataException Severe error during occurred.
123 */
124 public void accept(final ImportList importList) throws ModuleDataException;
125
126 /**
127 * Traverse import.
128 *
129 * @param imp Traverse this element.
130 * @throws ModuleDataException Severe error during occurred.
131 */
132 public void accept(final Import imp) throws ModuleDataException;
133
134 /**
135 * Traverse specification.
136 *
137 * @param specification Traverse this element.
138 * @throws ModuleDataException Severe error during occurred.
139 */
140 public void accept(final Specification specification) throws ModuleDataException;
141
142 /**
143 * Traverse location list.
144 *
145 * @param locationList Traverse this element.
146 * @throws ModuleDataException Severe error during occurred.
147 */
148 public void accept(final LocationList locationList) throws ModuleDataException;
149
150 /**
151 * Traverse location.
152 *
153 * @param location Traverse this element.
154 * @throws ModuleDataException Severe error during occurred.
155 */
156 public void accept(final Location location) throws ModuleDataException;
157
158 /**
159 * Traverse author list.
160 *
161 * @param authorList Traverse this element.
162 * @throws ModuleDataException Severe error during occurred.
163 */
164 public void accept(final AuthorList authorList) throws ModuleDataException;
165
166 /**
167 * Traverse author.
168 *
169 * @param author Traverse this element.
170 * @throws ModuleDataException Severe error during occurred.
171 */
172 public void accept(final Author author) throws ModuleDataException;
173
174 /**
175 * Traverse chapter list.
176 *
177 * @param chapterList Traverse this element.
178 * @throws ModuleDataException Severe error during occurred.
179 */
180 public void accept(final ChapterList chapterList) throws ModuleDataException;
181
182 /**
183 * Traverse chapter.
184 *
185 * @param chapter Traverse this element.
186 * @throws ModuleDataException Severe error during occurred.
187 */
188 public void accept(final Chapter chapter) throws ModuleDataException;
189
190 /**
191 * Traverse literature item list.
192 *
193 * @param literatureItemList Traverse this element.
194 * @throws ModuleDataException Severe error during occurred.
195 */
196 public void accept(final LiteratureItemList literatureItemList) throws ModuleDataException;
197
198 /**
199 * Traverse literature item.
200 *
201 * @param literatureItem Traverse this element.
202 * @throws ModuleDataException Severe error during occurred.
203 */
204 public void accept(final LiteratureItem literatureItem) throws ModuleDataException;
205
206 /**
207 * Traverse section list.
208 *
209 * @param sectionList Traverse this element.
210 * @throws ModuleDataException Severe error during occurred.
211 */
212 public void accept(final SectionList sectionList) throws ModuleDataException;
213
214 /**
215 * Traverse section.
216 *
217 * @param section Traverse this element.
218 * @throws ModuleDataException Severe error during occurred.
219 */
220 public void accept(final Section section) throws ModuleDataException;
221
222 /**
223 * Traverse subsection list.
224 *
225 * @param subsectionList Traverse this element.
226 * @throws ModuleDataException Severe error during occurred.
227 */
228 public void accept(final SubsectionList subsectionList) throws ModuleDataException;
229
230 /**
231 * Traverse subsection list.
232 *
233 * @param subsection Traverse this element.
234 * @throws ModuleDataException Severe error during occurred.
235 */
236 public void accept(final Subsection subsection) throws ModuleDataException;
237
238 /**
239 * Traverse node.
240 *
241 * @param node Traverse this element.
242 * @throws ModuleDataException Severe error during occurred.
243 */
244 public void accept(final Node node) throws ModuleDataException;
245
246 /**
247 * Traverse axiom.
248 *
249 * @param axiom Traverse this element.
250 * @throws ModuleDataException Severe error during occurred.
251 */
252 public void accept(final Axiom axiom) throws ModuleDataException;
253
254 /**
255 * Traverse predicate definition.
256 *
257 * @param definition Traverse this element.
258 * @throws ModuleDataException Severe error during occurred.
259 */
260 public void accept(final PredicateDefinition definition) throws ModuleDataException;
261
262 /**
263 * Traverse initial predicate definition.
264 *
265 * @param definition Traverse this element.
266 * @throws ModuleDataException Severe error during occurred.
267 */
268 public void accept(final InitialPredicateDefinition definition) throws ModuleDataException;
269
270 /**
271 * Traverse initial function definition.
272 *
273 * @param definition Traverse this element.
274 * @throws ModuleDataException Severe error during occurred.
275 */
276 public void accept(final InitialFunctionDefinition definition) throws ModuleDataException;
277
278 /**
279 * Traverse function definition.
280 *
281 * @param definition Traverse this element.
282 * @throws ModuleDataException Severe error during occurred.
283 */
284 public void accept(final FunctionDefinition definition) throws ModuleDataException;
285
286 /**
287 * Traverse proposition.
288 *
289 * @param proposition Traverse this element.
290 * @throws ModuleDataException Severe error during occurred.
291 */
292 public void accept(final Proposition proposition) throws ModuleDataException;
293
294 /**
295 * Traverse rule.
296 *
297 * @param rule Traverse this element.
298 * @throws ModuleDataException Severe error during occurred.
299 */
300 public void accept(final Rule rule) throws ModuleDataException;
301
302 /**
303 * Traverse changed rule list.
304 *
305 * @param list Traverse this element.
306 * @throws ModuleDataException Severe error during occurred.
307 */
308 public void accept(final ChangedRuleList list) throws ModuleDataException;
309
310 /**
311 * Traverse changed rule.
312 *
313 * @param rule Traverse this element.
314 * @throws ModuleDataException Severe error during occurred.
315 */
316 public void accept(final ChangedRule rule) throws ModuleDataException;
317
318 /**
319 * Traverse link list.
320 *
321 * @param linkList Traverse this element.
322 * @throws ModuleDataException Severe error during occurred.
323 */
324 public void accept(final LinkList linkList) throws ModuleDataException;
325
326 /**
327 * Traverse formal proof list.
328 *
329 * @param proofList Traverse this element.
330 * @throws ModuleDataException Severe error during occurred.
331 */
332 public void accept(final FormalProofList proofList) throws ModuleDataException;
333
334 /**
335 * Traverse formal proof.
336 *
337 * @param proof Traverse this element.
338 * @throws ModuleDataException Severe error during occurred.
339 */
340 public void accept(final FormalProof proof) throws ModuleDataException;
341
342 /**
343 * Traverse formal proof list.
344 *
345 * @param proofLineList Traverse this element.
346 * @throws ModuleDataException Severe error during occurred.
347 */
348 public void accept(final FormalProofLineList proofLineList) throws ModuleDataException;
349
350 /**
351 * Traverse formal proof line.
352 *
353 * @param proofLine Traverse this element.
354 * @throws ModuleDataException Severe error during occurred.
355 */
356 public void accept(final FormalProofLine proofLine) throws ModuleDataException;
357
358 /**
359 * Traverse formal proof line reason.
360 *
361 * @param reason Traverse this element.
362 * @throws ModuleDataException Severe error during occurred.
363 */
364 public void accept(final Reason reason) throws ModuleDataException;
365
366 /**
367 * Traverse formal proof line reason.
368 *
369 * @param reason Traverse this element.
370 * @throws ModuleDataException Severe error during occurred.
371 */
372 public void accept(final ModusPonens reason) throws ModuleDataException;
373
374 /**
375 * Traverse formal proof line reason.
376 *
377 * @param reason Traverse this element.
378 * @throws ModuleDataException Severe error during occurred.
379 */
380 public void accept(final Add reason) throws ModuleDataException;
381
382 /**
383 * Traverse formal proof line reason.
384 *
385 * @param reason Traverse this element.
386 * @throws ModuleDataException Severe error during occurred.
387 */
388 public void accept(final Rename reason) throws ModuleDataException;
389
390 /**
391 * Traverse formal proof line reason.
392 *
393 * @param reason Traverse this element.
394 * @throws ModuleDataException Severe error during occurred.
395 */
396 public void accept(final SubstFree reason) throws ModuleDataException;
397
398 /**
399 * Traverse formal proof line reason.
400 *
401 * @param reason Traverse this element.
402 * @throws ModuleDataException Severe error during occurred.
403 */
404 public void accept(final SubstFunc reason) throws ModuleDataException;
405
406 /**
407 * Traverse formal proof line reason.
408 *
409 * @param reason Traverse this element.
410 * @throws ModuleDataException Severe error during occurred.
411 */
412 public void accept(final SubstPred reason) throws ModuleDataException;
413
414 /**
415 * Traverse formal proof line reason.
416 *
417 * @param reason Traverse this element.
418 * @throws ModuleDataException Severe error during occurred.
419 */
420 public void accept(final Existential reason) throws ModuleDataException;
421
422 /**
423 * Traverse formal proof line reason.
424 *
425 * @param reason Traverse this element.
426 * @throws ModuleDataException Severe error during occurred.
427 */
428 public void accept(final Universal reason) throws ModuleDataException;
429
430 /**
431 * Traverse formal proof line wit conditional proof.
432 *
433 * @param line Traverse this element.
434 * @throws ModuleDataException Severe error during occurred.
435 */
436 public void accept(final ConditionalProof line) throws ModuleDataException;
437
438 /**
439 * Traverse formal proof line hypothesis.
440 *
441 * @param hypothesis Traverse this element.
442 * @throws ModuleDataException Severe error during occurred.
443 */
444 public void accept(final Hypothesis hypothesis) throws ModuleDataException;
445
446 /**
447 * Traverse formal proof line conclusion.
448 *
449 * @param conclusion Traverse this element.
450 * @throws ModuleDataException Severe error during occurred.
451 */
452 public void accept(final Conclusion conclusion) throws ModuleDataException;
453
454 /**
455 * Traverse proof list.
456 *
457 * @param proofList Traverse this element.
458 * @throws ModuleDataException Severe error during occurred.
459 */
460 public void accept(final ProofList proofList) throws ModuleDataException;
461
462 /**
463 * Traverse proof.
464 *
465 * @param proof Traverse this element.
466 * @throws ModuleDataException Severe error during occurred.
467 */
468 public void accept(final Proof proof) throws ModuleDataException;
469
470 /**
471 * Traverse formula.
472 *
473 * @param formula Traverse this element.
474 * @throws ModuleDataException Severe error during occurred.
475 */
476 public void accept(final Formula formula) throws ModuleDataException;
477
478 /**
479 * Traverse term.
480 *
481 * @param term Traverse this element.
482 * @throws ModuleDataException Severe error during occurred.
483 */
484 public void accept(final Term term) throws ModuleDataException;
485
486 /**
487 * Traverse latex list.
488 *
489 * @param latexList Traverse this element.
490 * @throws ModuleDataException Severe error during occurred.
491 */
492 public void accept(final LatexList latexList) throws ModuleDataException;
493
494 /**
495 * Traverse latex.
496 *
497 * @param latex Traverse this element.
498 * @throws ModuleDataException Severe error during occurred.
499 */
500 public void accept(final Latex latex) throws ModuleDataException;
501
502 /**
503 * Traverse element.
504 *
505 * @param element Traverse this element.
506 * @throws ModuleDataException Severe error during occurred.
507 */
508 public void accept(final Element element) throws ModuleDataException;
509
510 /**
511 * Traverse atom.
512 *
513 * @param atom Traverse this element.
514 * @throws ModuleDataException Severe error during occurred.
515 */
516 public void accept(final Atom atom) throws ModuleDataException;
517
518 /**
519 * Traverse element list.
520 *
521 * @param list Traverse this element.
522 * @throws ModuleDataException Severe error during occurred.
523 */
524 public void accept(final ElementList list) throws ModuleDataException;
525
526 }