de.uka.ilkd.key.rule.match.vm

Class TermNavigator

java.lang.Object

de.uka.ilkd.key.rule.match.vm.TermNavigator

public class TermNavigator
extends java.lang.Object

An iterator that walks in first-depth order through the term. It allows to jump to siblings.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	TermNavigator.MutablePair A mutable tuple of two types

Field Summary

Fields

Modifier and Type	Field and Description
private static int	POOL_SIZE
private java.util.ArrayDeque<TermNavigator.MutablePair>	stack top element on stack contains always the pair whose first component is the element to be returned by #next() while the second points to the child to be visited next (or equals the arity of the first component if no such child exists) For all elements on the stack that are not the top element the second component is less than the arity of the term in the first component
private static java.util.ArrayDeque<TermNavigator>	TERM_NAVIGATOR_POOL TERM_NAVIGATOR_POOL of TermNavigator as these are created very often and short-living we reuse them as far as possible The used TermNavigator have to be explicitly released by the user via release()

Constructor Summary

Constructors

Modifier	Constructor and Description
private	TermNavigator()
private	TermNavigator(Term term)

Method Summary

Modifier and Type	Method and Description
static TermNavigator	get(Term term) returns a pooled TermNavigator or a new one if the TERM_NAVIGATOR_POOL is currently empty The used TermNavigator have to be explicitly released by the user via release()
Term	getCurrentSubterm()
void	gotoNext()
private void	gotoNextHelper()
void	gotoNextSibling()
boolean	hasNext()
boolean	hasNextSibling()
void	release()

Methods inherited from class java.lang.Object

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

Field Detail

POOL_SIZE

private static final int POOL_SIZE

See Also:

Constant Field Values

TERM_NAVIGATOR_POOL

private static java.util.ArrayDeque<TermNavigator> TERM_NAVIGATOR_POOL

TERM_NAVIGATOR_POOL of TermNavigator as these are created very often and short-living we reuse them as far as possible The used TermNavigator have to be explicitly released by the user via release()

stack

private final java.util.ArrayDeque<TermNavigator.MutablePair> stack

top element on stack contains always the pair whose first component is the element to be returned by #next() while the second points to the child to be visited next (or equals the arity of the first component if no such child exists) For all elements on the stack that are not the top element the second component is less than the arity of the term in the first component

Constructor Detail

TermNavigator

private TermNavigator()

TermNavigator

private TermNavigator(Term term)

Method Detail

get

public static TermNavigator get(Term term)

returns a pooled TermNavigator or a new one if the TERM_NAVIGATOR_POOL is currently empty The used TermNavigator have to be explicitly released by the user via release()

Returns:

a pooled TermNavigator or a new one if the TERM_NAVIGATOR_POOL is currently empty

hasNext

public boolean hasNext()

hasNextSibling

public boolean hasNextSibling()

getCurrentSubterm

public Term getCurrentSubterm()

gotoNextHelper

private void gotoNextHelper()

gotoNext

public void gotoNext()

gotoNextSibling

public void gotoNextSibling()

release

public void release()