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