org.qedeq.kernel.se.visitor
Class QedeqNotNullTraverser

java.lang.Object
  org.qedeq.kernel.se.visitor.QedeqNotNullTraverser

All Implemented Interfaces:

ServiceCompleteness, QedeqTraverser

public class QedeqNotNullTraverser
extends java.lang.Object
implements QedeqTraverser, ServiceCompleteness

Traverse QEDEQ module. Calls visitors of QedeqVisitor for non null arguments.

Author:

Michael Meyling

Constructor Summary

QedeqNotNullTraverser(ModuleAddress globalContext)
Constructor.

QedeqNotNullTraverser(ModuleAddress globalContext, QedeqVisitor visitor)
Constructor.

Method Summary

void	accept(Add reason) Traverse formal proof line reason.
void	accept(Atom atom) Traverse atom.
void	accept(Author author) Traverse author.
void	accept(AuthorList authorList) Traverse author list.
void	accept(Axiom axiom) Traverse axiom.
void	accept(ChangedRule rule) Traverse changed rule.
void	accept(ChangedRuleList list) Traverse changed rule list.
void	accept(Chapter chapter) Traverse chapter.
void	accept(ChapterList chapterList) Traverse chapter list.
void	accept(Conclusion conclusion) Traverse formal proof line conclusion.
void	accept(ConditionalProof reason) Traverse formal proof line wit conditional proof.
void	accept(Element element) Traverse element.
void	accept(ElementList list) Traverse element list.
void	accept(Existential reason) Traverse formal proof line reason.
void	accept(FormalProof proof) Traverse formal proof.
void	accept(FormalProofLine proofLine) Traverse formal proof line.
void	accept(FormalProofLineList proofLineList) Traverse formal proof list.
void	accept(FormalProofList proofList) Traverse formal proof list.
void	accept(Formula formula) Traverse formula.
void	accept(FunctionDefinition definition) Traverse function definition.
void	accept(Header header) Traverse header.
void	accept(Hypothesis hypothesis) Traverse formal proof line hypothesis.
void	accept(Import imp) Traverse import.
void	accept(ImportList importList) Traverse import list.
void	accept(InitialFunctionDefinition definition) Traverse initial function definition.
void	accept(InitialPredicateDefinition definition) Traverse initial predicate definition.
void	accept(Latex latex) Traverse latex.
void	accept(LatexList latexList) Traverse latex list.
void	accept(LinkList linkList) Traverse link list.
void	accept(LiteratureItem item) Traverse literature item.
void	accept(LiteratureItemList literatureItemList) Traverse literature item list.
void	accept(Location location) Traverse location.
void	accept(LocationList locationList) Traverse location list.
void	accept(ModusPonens reason) Traverse formal proof line reason.
void	accept(Node node) Traverse node.
void	accept(PredicateDefinition definition) Traverse predicate definition.
void	accept(Proof proof) Traverse proof.
void	accept(ProofList proofList) Traverse proof list.
void	accept(Proposition proposition) Traverse proposition.
void	accept(Qedeq qedeq) Start with the top structure of a QEDEQ module.
void	accept(Reason reason) Traverse formal proof line reason.
void	accept(Rename reason) Traverse formal proof line reason.
void	accept(Rule rule) Traverse rule.
void	accept(Section section) Traverse section.
void	accept(SectionList sectionList) Traverse section list.
void	accept(Specification specification) Traverse specification.
void	accept(Subsection subsection) Traverse subsection list.
void	accept(SubsectionList subsectionList) Traverse subsection list.
void	accept(SubstFree reason) Traverse formal proof line reason.
void	accept(SubstFunc reason) Traverse formal proof line reason.
void	accept(SubstPred reason) Traverse formal proof line reason.
void	accept(Term term) Traverse term.
void	accept(Universal reason) Traverse formal proof line reason.
void	accept(UsedByList usedByList) Traverse used by list.
boolean	getBlocked() Is further traversing blocked?
ModuleContext	getCurrentContext() Get current context within original.
QedeqNumbers	getCurrentNumbers() Get copy of current counters.
RuleKey	getLocalRuleKey(java.lang.String name) Get current (QEDEQ module local) rule version for given rule name.
java.lang.String	getLocationDescription() Get readable description of current location.
Node	getNode() Get node that is currently parsed.
double	getVisitPercentage() Get calculated visit percentage.
void	setBlocked(boolean blocked) Set if further traverse is blocked.
void	setLocationWithinModule(java.lang.String locationWithinModule) Set location information where are we within the original module.
void	setVisitor(QedeqVisitor visitor) Set visitor.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

QedeqNotNullTraverser

public QedeqNotNullTraverser(ModuleAddress globalContext,
                             QedeqVisitor visitor)

Constructor.

Parameters:

globalContext - Module location information.

visitor - These methods are called if a node is visited.

QedeqNotNullTraverser

public QedeqNotNullTraverser(ModuleAddress globalContext)

Constructor.

Parameters:

globalContext - Module location information.

Method Detail

setVisitor

public void setVisitor(QedeqVisitor visitor)

Set visitor.

Parameters:

visitor - These methods are called if a node is visited.

accept

public void accept(Qedeq qedeq)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Start with the top structure of a QEDEQ module.

Specified by:

accept in interface QedeqTraverser

Parameters:

qedeq - Traverse this element. Must not be null.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Header header)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse header.

Specified by:

accept in interface QedeqTraverser

Parameters:

header - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(UsedByList usedByList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse used by list.

Specified by:

accept in interface QedeqTraverser

Parameters:

usedByList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ImportList importList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse import list.

Specified by:

accept in interface QedeqTraverser

Parameters:

importList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Import imp)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse import.

Specified by:

accept in interface QedeqTraverser

Parameters:

imp - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Specification specification)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse specification.

Specified by:

accept in interface QedeqTraverser

Parameters:

specification - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(LocationList locationList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse location list.

Specified by:

accept in interface QedeqTraverser

Parameters:

locationList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Location location)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse location.

Specified by:

accept in interface QedeqTraverser

Parameters:

location - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(AuthorList authorList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse author list.

Specified by:

accept in interface QedeqTraverser

Parameters:

authorList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Author author)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse author.

Specified by:

accept in interface QedeqTraverser

Parameters:

author - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ChapterList chapterList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse chapter list.

Specified by:

accept in interface QedeqTraverser

Parameters:

chapterList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Chapter chapter)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse chapter.

Specified by:

accept in interface QedeqTraverser

Parameters:

chapter - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(LiteratureItemList literatureItemList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse literature item list.

Specified by:

accept in interface QedeqTraverser

Parameters:

literatureItemList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(LiteratureItem item)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse literature item.

Specified by:

accept in interface QedeqTraverser

Parameters:

item - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(SectionList sectionList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse section list.

Specified by:

accept in interface QedeqTraverser

Parameters:

sectionList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Section section)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse section.

Specified by:

accept in interface QedeqTraverser

Parameters:

section - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(SubsectionList subsectionList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse subsection list.

Specified by:

accept in interface QedeqTraverser

Parameters:

subsectionList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Subsection subsection)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse subsection list.

Specified by:

accept in interface QedeqTraverser

Parameters:

subsection - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Node node)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse node.

Specified by:

accept in interface QedeqTraverser

Parameters:

node - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Axiom axiom)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse axiom.

Specified by:

accept in interface QedeqTraverser

Parameters:

axiom - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(PredicateDefinition definition)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse predicate definition.

Specified by:

accept in interface QedeqTraverser

Parameters:

definition - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(InitialPredicateDefinition definition)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse initial predicate definition.

Specified by:

accept in interface QedeqTraverser

Parameters:

definition - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(InitialFunctionDefinition definition)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse initial function definition.

Specified by:

accept in interface QedeqTraverser

Parameters:

definition - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(FunctionDefinition definition)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse function definition.

Specified by:

accept in interface QedeqTraverser

Parameters:

definition - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Proposition proposition)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse proposition.

Specified by:

accept in interface QedeqTraverser

Parameters:

proposition - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Rule rule)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse rule.

Specified by:

accept in interface QedeqTraverser

Parameters:

rule - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ChangedRuleList list)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse changed rule list.

Specified by:

accept in interface QedeqTraverser

Parameters:

list - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ChangedRule rule)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse changed rule.

Specified by:

accept in interface QedeqTraverser

Parameters:

rule - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(LinkList linkList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse link list.

Specified by:

accept in interface QedeqTraverser

Parameters:

linkList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ProofList proofList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse proof list.

Specified by:

accept in interface QedeqTraverser

Parameters:

proofList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Proof proof)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse proof.

Specified by:

accept in interface QedeqTraverser

Parameters:

proof - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(FormalProofList proofList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof list.

Specified by:

accept in interface QedeqTraverser

Parameters:

proofList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(FormalProof proof)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof.

Specified by:

accept in interface QedeqTraverser

Parameters:

proof - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(FormalProofLineList proofLineList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof list.

Specified by:

accept in interface QedeqTraverser

Parameters:

proofLineList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(FormalProofLine proofLine)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line.

Specified by:

accept in interface QedeqTraverser

Parameters:

proofLine - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Reason reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ModusPonens reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Add reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Rename reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(SubstFree reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(SubstFunc reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(SubstPred reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Existential reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Universal reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line reason.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ConditionalProof reason)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line wit conditional proof.

Specified by:

accept in interface QedeqTraverser

Parameters:

reason - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Hypothesis hypothesis)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line hypothesis.

Specified by:

accept in interface QedeqTraverser

Parameters:

hypothesis - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Conclusion conclusion)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formal proof line conclusion.

Specified by:

accept in interface QedeqTraverser

Parameters:

conclusion - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Formula formula)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse formula.

Specified by:

accept in interface QedeqTraverser

Parameters:

formula - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Term term)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse term.

Specified by:

accept in interface QedeqTraverser

Parameters:

term - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Element element)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse element.

Specified by:

accept in interface QedeqTraverser

Parameters:

element - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Atom atom)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse atom.

Specified by:

accept in interface QedeqTraverser

Parameters:

atom - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(ElementList list)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse element list.

Specified by:

accept in interface QedeqTraverser

Parameters:

list - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(LatexList latexList)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse latex list.

Specified by:

accept in interface QedeqTraverser

Parameters:

latexList - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

accept

public void accept(Latex latex)
            throws ModuleDataException

Description copied from interface: QedeqTraverser

Traverse latex.

Specified by:

accept in interface QedeqTraverser

Parameters:

latex - Traverse this element.

Throws:

ModuleDataException - Severe error during occurred.

getNode

public Node getNode()

Get node that is currently parsed. Might be null.

Returns:

QEDEQ node were are currently in.

setLocationWithinModule

public void setLocationWithinModule(java.lang.String locationWithinModule)

Set location information where are we within the original module.

Parameters:

locationWithinModule - Location within module.

getCurrentContext

public final ModuleContext getCurrentContext()

Description copied from interface: QedeqTraverser

Get current context within original. Remember to use the copy constructor when trying to remember this context!

Specified by:

getCurrentContext in interface QedeqTraverser

Returns:

Current context.

getBlocked

public final boolean getBlocked()

Is further traversing blocked?

Returns:

Is further traversing blocked?

setBlocked

public final void setBlocked(boolean blocked)

Set if further traverse is blocked.

Parameters:

blocked - Further transversion?

getVisitPercentage

public double getVisitPercentage()

Get calculated visit percentage.

Specified by:

getVisitPercentage in interface ServiceCompleteness

Returns:

Value between 0 and 100.

getLocationDescription

public java.lang.String getLocationDescription()

Description copied from interface: ServiceCompleteness

Get readable description of current location.

Specified by:

getLocationDescription in interface ServiceCompleteness

Returns:

Description.

getCurrentNumbers

public QedeqNumbers getCurrentNumbers()

Get copy of current counters.

Returns:

Values of various counters.

getLocalRuleKey

public RuleKey getLocalRuleKey(java.lang.String name)

Get current (QEDEQ module local) rule version for given rule name.

Parameters:

name - Rule name

Returns:

Current (local) rule version. Might be null.