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.se.visitor;
017
018 import org.qedeq.kernel.se.base.list.Atom;
019 import org.qedeq.kernel.se.base.list.Element;
020 import org.qedeq.kernel.se.base.list.ElementList;
021 import org.qedeq.kernel.se.base.module.Add;
022 import org.qedeq.kernel.se.base.module.Author;
023 import org.qedeq.kernel.se.base.module.AuthorList;
024 import org.qedeq.kernel.se.base.module.Axiom;
025 import org.qedeq.kernel.se.base.module.ChangedRule;
026 import org.qedeq.kernel.se.base.module.ChangedRuleList;
027 import org.qedeq.kernel.se.base.module.Chapter;
028 import org.qedeq.kernel.se.base.module.ChapterList;
029 import org.qedeq.kernel.se.base.module.Conclusion;
030 import org.qedeq.kernel.se.base.module.ConditionalProof;
031 import org.qedeq.kernel.se.base.module.Existential;
032 import org.qedeq.kernel.se.base.module.FormalProof;
033 import org.qedeq.kernel.se.base.module.FormalProofLine;
034 import org.qedeq.kernel.se.base.module.FormalProofLineList;
035 import org.qedeq.kernel.se.base.module.FormalProofList;
036 import org.qedeq.kernel.se.base.module.Formula;
037 import org.qedeq.kernel.se.base.module.FunctionDefinition;
038 import org.qedeq.kernel.se.base.module.Header;
039 import org.qedeq.kernel.se.base.module.Hypothesis;
040 import org.qedeq.kernel.se.base.module.Import;
041 import org.qedeq.kernel.se.base.module.ImportList;
042 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
043 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
044 import org.qedeq.kernel.se.base.module.Latex;
045 import org.qedeq.kernel.se.base.module.LatexList;
046 import org.qedeq.kernel.se.base.module.LinkList;
047 import org.qedeq.kernel.se.base.module.LiteratureItem;
048 import org.qedeq.kernel.se.base.module.LiteratureItemList;
049 import org.qedeq.kernel.se.base.module.Location;
050 import org.qedeq.kernel.se.base.module.LocationList;
051 import org.qedeq.kernel.se.base.module.ModusPonens;
052 import org.qedeq.kernel.se.base.module.Node;
053 import org.qedeq.kernel.se.base.module.PredicateDefinition;
054 import org.qedeq.kernel.se.base.module.Proof;
055 import org.qedeq.kernel.se.base.module.ProofList;
056 import org.qedeq.kernel.se.base.module.Proposition;
057 import org.qedeq.kernel.se.base.module.Qedeq;
058 import org.qedeq.kernel.se.base.module.Reason;
059 import org.qedeq.kernel.se.base.module.Rename;
060 import org.qedeq.kernel.se.base.module.Rule;
061 import org.qedeq.kernel.se.base.module.Section;
062 import org.qedeq.kernel.se.base.module.SectionList;
063 import org.qedeq.kernel.se.base.module.Specification;
064 import org.qedeq.kernel.se.base.module.Subsection;
065 import org.qedeq.kernel.se.base.module.SubsectionList;
066 import org.qedeq.kernel.se.base.module.SubstFree;
067 import org.qedeq.kernel.se.base.module.SubstFunc;
068 import org.qedeq.kernel.se.base.module.SubstPred;
069 import org.qedeq.kernel.se.base.module.Term;
070 import org.qedeq.kernel.se.base.module.Universal;
071 import org.qedeq.kernel.se.base.module.UsedByList;
072 import org.qedeq.kernel.se.base.module.VariableList;
073 import org.qedeq.kernel.se.common.ModuleDataException;
074
075 /**
076 * Traverse a QEDEQ module and visit all elements.
077 * All contained elements are called recursively.
078 * See {@link org.qedeq.kernel.se.visitor.QedeqVisitor}.
079 *
080 * @author Michael Meyling
081 */
082 public interface QedeqTraverser {
083
084 /**
085 * Start with the top structure of a QEDEQ module.
086 *
087 * @param qedeq Traverse this element. Must not be <code>null</code>.
088 * @throws ModuleDataException Severe error during occurred.
089 */
090 public void accept(final Qedeq qedeq) throws ModuleDataException;
091
092 /**
093 * Traverse header.
094 *
095 * @param header Traverse this element.
096 * @throws ModuleDataException Severe error during occurred.
097 */
098 public void accept(final Header header) throws ModuleDataException;
099
100 /**
101 * Traverse used by list.
102 *
103 * @param usedByList Traverse this element.
104 * @throws ModuleDataException Severe error during occurred.
105 */
106 public void accept(final UsedByList usedByList) throws ModuleDataException;
107
108 /**
109 * Traverse import list.
110 *
111 * @param importList Traverse this element.
112 * @throws ModuleDataException Severe error during occurred.
113 */
114 public void accept(final ImportList importList) throws ModuleDataException;
115
116 /**
117 * Traverse import.
118 *
119 * @param imp Traverse this element.
120 * @throws ModuleDataException Severe error during occurred.
121 */
122 public void accept(final Import imp) throws ModuleDataException;
123
124 /**
125 * Traverse specification.
126 *
127 * @param specification Traverse this element.
128 * @throws ModuleDataException Severe error during occurred.
129 */
130 public void accept(final Specification specification) throws ModuleDataException;
131
132 /**
133 * Traverse location list.
134 *
135 * @param locationList Traverse this element.
136 * @throws ModuleDataException Severe error during occurred.
137 */
138 public void accept(final LocationList locationList) throws ModuleDataException;
139
140 /**
141 * Traverse location.
142 *
143 * @param location Traverse this element.
144 * @throws ModuleDataException Severe error during occurred.
145 */
146 public void accept(final Location location) throws ModuleDataException;
147
148 /**
149 * Traverse author list.
150 *
151 * @param authorList Traverse this element.
152 * @throws ModuleDataException Severe error during occurred.
153 */
154 public void accept(final AuthorList authorList) throws ModuleDataException;
155
156 /**
157 * Traverse author.
158 *
159 * @param author Traverse this element.
160 * @throws ModuleDataException Severe error during occurred.
161 */
162 public void accept(final Author author) throws ModuleDataException;
163
164 /**
165 * Traverse chapter list.
166 *
167 * @param chapterList Traverse this element.
168 * @throws ModuleDataException Severe error during occurred.
169 */
170 public void accept(final ChapterList chapterList) throws ModuleDataException;
171
172 /**
173 * Traverse chapter.
174 *
175 * @param chapter Traverse this element.
176 * @throws ModuleDataException Severe error during occurred.
177 */
178 public void accept(final Chapter chapter) throws ModuleDataException;
179
180 /**
181 * Traverse literature item list.
182 *
183 * @param literatureItemList Traverse this element.
184 * @throws ModuleDataException Severe error during occurred.
185 */
186 public void accept(final LiteratureItemList literatureItemList) throws ModuleDataException;
187
188 /**
189 * Traverse literature item.
190 *
191 * @param literatureItem Traverse this element.
192 * @throws ModuleDataException Severe error during occurred.
193 */
194 public void accept(final LiteratureItem literatureItem) throws ModuleDataException;
195
196 /**
197 * Traverse section list.
198 *
199 * @param sectionList Traverse this element.
200 * @throws ModuleDataException Severe error during occurred.
201 */
202 public void accept(final SectionList sectionList) throws ModuleDataException;
203
204 /**
205 * Traverse section.
206 *
207 * @param section Traverse this element.
208 * @throws ModuleDataException Severe error during occurred.
209 */
210 public void accept(final Section section) throws ModuleDataException;
211
212 /**
213 * Traverse subsection list.
214 *
215 * @param subsectionList Traverse this element.
216 * @throws ModuleDataException Severe error during occurred.
217 */
218 public void accept(final SubsectionList subsectionList) throws ModuleDataException;
219
220 /**
221 * Traverse subsection list.
222 *
223 * @param subsection Traverse this element.
224 * @throws ModuleDataException Severe error during occurred.
225 */
226 public void accept(final Subsection subsection) throws ModuleDataException;
227
228 /**
229 * Traverse node.
230 *
231 * @param node Traverse this element.
232 * @throws ModuleDataException Severe error during occurred.
233 */
234 public void accept(final Node node) throws ModuleDataException;
235
236 /**
237 * Traverse axiom.
238 *
239 * @param axiom Traverse this element.
240 * @throws ModuleDataException Severe error during occurred.
241 */
242 public void accept(final Axiom axiom) throws ModuleDataException;
243
244 /**
245 * Traverse predicate definition.
246 *
247 * @param definition Traverse this element.
248 * @throws ModuleDataException Severe error during occurred.
249 */
250 public void accept(final PredicateDefinition definition) throws ModuleDataException;
251
252 /**
253 * Traverse initial predicate definition.
254 *
255 * @param definition Traverse this element.
256 * @throws ModuleDataException Severe error during occurred.
257 */
258 public void accept(final InitialPredicateDefinition definition) throws ModuleDataException;
259
260 /**
261 * Traverse initial function definition.
262 *
263 * @param definition Traverse this element.
264 * @throws ModuleDataException Severe error during occurred.
265 */
266 public void accept(final InitialFunctionDefinition definition) throws ModuleDataException;
267
268 /**
269 * Traverse function definition.
270 *
271 * @param definition Traverse this element.
272 * @throws ModuleDataException Severe error during occurred.
273 */
274 public void accept(final FunctionDefinition definition) throws ModuleDataException;
275
276 /**
277 * Traverse proposition.
278 *
279 * @param proposition Traverse this element.
280 * @throws ModuleDataException Severe error during occurred.
281 */
282 public void accept(final Proposition proposition) throws ModuleDataException;
283
284 /**
285 * Traverse rule.
286 *
287 * @param rule Traverse this element.
288 * @throws ModuleDataException Severe error during occurred.
289 */
290 public void accept(final Rule rule) throws ModuleDataException;
291
292 /**
293 * Traverse changed rule list.
294 *
295 * @param list Traverse this element.
296 * @throws ModuleDataException Severe error during occurred.
297 */
298 public void accept(final ChangedRuleList list) throws ModuleDataException;
299
300 /**
301 * Traverse changed rule.
302 *
303 * @param rule Traverse this element.
304 * @throws ModuleDataException Severe error during occurred.
305 */
306 public void accept(final ChangedRule rule) throws ModuleDataException;
307
308 /**
309 * Traverse link list.
310 *
311 * @param linkList Traverse this element.
312 * @throws ModuleDataException Severe error during occurred.
313 */
314 public void accept(final LinkList linkList) throws ModuleDataException;
315
316 /**
317 * Traverse variable list.
318 *
319 * @param variableList Traverse this element.
320 * @throws ModuleDataException Severe error during occurred.
321 */
322 public void accept(final VariableList variableList) throws ModuleDataException;
323
324 /**
325 * Traverse formal proof list.
326 *
327 * @param proofList Traverse this element.
328 * @throws ModuleDataException Severe error during occurred.
329 */
330 public void accept(final FormalProofList proofList) throws ModuleDataException;
331
332 /**
333 * Traverse formal proof.
334 *
335 * @param proof Traverse this element.
336 * @throws ModuleDataException Severe error during occurred.
337 */
338 public void accept(final FormalProof proof) throws ModuleDataException;
339
340 /**
341 * Traverse formal proof list.
342 *
343 * @param proofLineList Traverse this element.
344 * @throws ModuleDataException Severe error during occurred.
345 */
346 public void accept(final FormalProofLineList proofLineList) throws ModuleDataException;
347
348 /**
349 * Traverse formal proof line.
350 *
351 * @param proofLine Traverse this element.
352 * @throws ModuleDataException Severe error during occurred.
353 */
354 public void accept(final FormalProofLine proofLine) throws ModuleDataException;
355
356 /**
357 * Traverse formal proof line reason.
358 *
359 * @param reason Traverse this element.
360 * @throws ModuleDataException Severe error during occurred.
361 */
362 public void accept(final Reason reason) throws ModuleDataException;
363
364 /**
365 * Traverse formal proof line reason.
366 *
367 * @param reason Traverse this element.
368 * @throws ModuleDataException Severe error during occurred.
369 */
370 public void accept(final ModusPonens reason) throws ModuleDataException;
371
372 /**
373 * Traverse formal proof line reason.
374 *
375 * @param reason Traverse this element.
376 * @throws ModuleDataException Severe error during occurred.
377 */
378 public void accept(final Add reason) throws ModuleDataException;
379
380 /**
381 * Traverse formal proof line reason.
382 *
383 * @param reason Traverse this element.
384 * @throws ModuleDataException Severe error during occurred.
385 */
386 public void accept(final Rename reason) throws ModuleDataException;
387
388 /**
389 * Traverse formal proof line reason.
390 *
391 * @param reason Traverse this element.
392 * @throws ModuleDataException Severe error during occurred.
393 */
394 public void accept(final SubstFree reason) throws ModuleDataException;
395
396 /**
397 * Traverse formal proof line reason.
398 *
399 * @param reason Traverse this element.
400 * @throws ModuleDataException Severe error during occurred.
401 */
402 public void accept(final SubstFunc reason) throws ModuleDataException;
403
404 /**
405 * Traverse formal proof line reason.
406 *
407 * @param reason Traverse this element.
408 * @throws ModuleDataException Severe error during occurred.
409 */
410 public void accept(final SubstPred reason) throws ModuleDataException;
411
412 /**
413 * Traverse formal proof line reason.
414 *
415 * @param reason Traverse this element.
416 * @throws ModuleDataException Severe error during occurred.
417 */
418 public void accept(final Existential reason) throws ModuleDataException;
419
420 /**
421 * Traverse formal proof line reason.
422 *
423 * @param reason Traverse this element.
424 * @throws ModuleDataException Severe error during occurred.
425 */
426 public void accept(final Universal reason) throws ModuleDataException;
427
428 /**
429 * Traverse formal proof line wit conditional proof.
430 *
431 * @param line Traverse this element.
432 * @throws ModuleDataException Severe error during occurred.
433 */
434 public void accept(final ConditionalProof line) throws ModuleDataException;
435
436 /**
437 * Traverse formal proof line hypothesis.
438 *
439 * @param hypothesis Traverse this element.
440 * @throws ModuleDataException Severe error during occurred.
441 */
442 public void accept(final Hypothesis hypothesis) throws ModuleDataException;
443
444 /**
445 * Traverse formal proof line conclusion.
446 *
447 * @param conclusion Traverse this element.
448 * @throws ModuleDataException Severe error during occurred.
449 */
450 public void accept(final Conclusion conclusion) throws ModuleDataException;
451
452 /**
453 * Traverse proof list.
454 *
455 * @param proofList Traverse this element.
456 * @throws ModuleDataException Severe error during occurred.
457 */
458 public void accept(final ProofList proofList) throws ModuleDataException;
459
460 /**
461 * Traverse proof.
462 *
463 * @param proof Traverse this element.
464 * @throws ModuleDataException Severe error during occurred.
465 */
466 public void accept(final Proof proof) throws ModuleDataException;
467
468 /**
469 * Traverse formula.
470 *
471 * @param formula Traverse this element.
472 * @throws ModuleDataException Severe error during occurred.
473 */
474 public void accept(final Formula formula) throws ModuleDataException;
475
476 /**
477 * Traverse term.
478 *
479 * @param term Traverse this element.
480 * @throws ModuleDataException Severe error during occurred.
481 */
482 public void accept(final Term term) throws ModuleDataException;
483
484 /**
485 * Traverse latex list.
486 *
487 * @param latexList Traverse this element.
488 * @throws ModuleDataException Severe error during occurred.
489 */
490 public void accept(final LatexList latexList) throws ModuleDataException;
491
492 /**
493 * Traverse latex.
494 *
495 * @param latex Traverse this element.
496 * @throws ModuleDataException Severe error during occurred.
497 */
498 public void accept(final Latex latex) throws ModuleDataException;
499
500 /**
501 * Traverse element.
502 *
503 * @param element Traverse this element.
504 * @throws ModuleDataException Severe error during occurred.
505 */
506 public void accept(final Element element) throws ModuleDataException;
507
508 /**
509 * Traverse atom.
510 *
511 * @param atom Traverse this element.
512 * @throws ModuleDataException Severe error during occurred.
513 */
514 public void accept(final Atom atom) throws ModuleDataException;
515
516 /**
517 * Traverse element list.
518 *
519 * @param list Traverse this element.
520 * @throws ModuleDataException Severe error during occurred.
521 */
522 public void accept(final ElementList list) throws ModuleDataException;
523
524 }
|