de.uka.ilkd.key.logic

Class Namespace<E extends Named>

java.lang.Object

de.uka.ilkd.key.logic.Namespace<E>

All Implemented Interfaces:

java.io.Serializable

public class Namespace<E extends Named>
extends java.lang.Object
implements java.io.Serializable

A Namespace keeps track of already used Names and the objects carrying these names. These objects have to implement the interface Named. It is possible to have nested namespaces in order to represent different visibility scopes.

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
private Namespace<E>	parent The fall-back namespace for symbols not present in this Namespace.
private boolean	sealed A namespace can be made immutable, this is called "sealing".
private static long	serialVersionUID
private java.util.Map<Name,E>	symbols The map that maps a name to a symbols of that name if it is defined in this Namespace.

Constructor Summary

Constructors

Constructor and Description
Namespace() Construct an empty Namespace without a parent namespace.
Namespace(Namespace<E> parent) Construct a Namespace that uses parent as a fallback for finding symbols not defined in this one.

Method Summary

Modifier and Type	Method and Description
void	add(E sym) Adds the object sym to this Namespace.
void	add(java.lang.Iterable<? extends E> list)
void	add(Namespace<E> source)
void	addSafely(E sym) Adds the object sym to this namespace.
void	addSafely(java.lang.Iterable<? extends E> names)
java.util.Collection<E>	allElements()
Namespace<E>	compress()
boolean	contains(E var)
Namespace<E>	copy()
java.util.Collection<E>	elements() returns list of the elements (not the keys) in this namespace (not about the one of the parent)
Namespace<E>	extended(E sym) creates a new Namespace that has this as parent, and contains an entry for sym.
Namespace<E>	extended(java.lang.Iterable<? extends E> ext)
void	flushToParent()
boolean	isEmpty()
boolean	isSealed()
E	lookup(Name name) looks if a registered object is declared in this namespace, if negative it asks its parent
E	lookup(java.lang.String name) Convenience method to look up.
protected E	lookupLocally(Name name)
Namespace<E>	parent() returns the fall-back Namespace of this Namespace, i.e. the one where symbols are looked up that are not found in this one.
void	remove(Name name) Remove a name from the namespace.
private void	reset()
void	seal()
<T extends E> void	set(ImmutableSet<T> names)
Namespace<E>	simplify()
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

parent

private Namespace<E extends Named> parent

The fall-back namespace for symbols not present in this Namespace.

symbols

private java.util.Map<Name,E extends Named> symbols

The map that maps a name to a symbols of that name if it is defined in this Namespace.

sealed

private boolean sealed

A namespace can be made immutable, this is called "sealing". This flag indicates whether this namespace has been sealed or not.

Constructor Detail

Namespace

public Namespace()

Construct an empty Namespace without a parent namespace.

Namespace

public Namespace(Namespace<E> parent)

Construct a Namespace that uses parent as a fallback for finding symbols not defined in this one.

Method Detail

add

public void add(E sym)

Adds the object sym to this Namespace. If an object with the same name is already there, it is quietly replaced by sym. Use addSafely() instead if possible. TODO:The problem of saving to localSym, symbols, and symbolRefs is not solved yet. (This is no longer self-explanatory. mu 2016) If the local table is empty, then the new symbol is added as "singleton map". This has been adapted from an earlier implementation, done for memory efficiency reasons: Many namespaces only contain a single element; no need to allocate a hash map. The hash map is only created when the 2nd element is added. This is not threadsafe.

add

public void add(Namespace<E> source)

add

public void add(java.lang.Iterable<? extends E> list)

addSafely

public void addSafely(E sym)

Adds the object sym to this namespace. Throws a runtime exception if an object with the same name is already there.

addSafely

public void addSafely(java.lang.Iterable<? extends E> names)

remove

public void remove(Name name)

Remove a name from the namespace. Removal is not delegated to the parent namespace.

Parameters:

name - non-null name whose symbol is to be removed.

lookupLocally

protected E lookupLocally(Name name)

extended

public Namespace<E> extended(E sym)

creates a new Namespace that has this as parent, and contains an entry for sym.

Returns:

the new Namespace

extended

public Namespace<E> extended(java.lang.Iterable<? extends E> ext)

lookup

public E lookup(Name name)

looks if a registered object is declared in this namespace, if negative it asks its parent

Parameters:

name - a Name representing the name of the symbol to look for

Returns:

Object with name "name" or null if no such an object has been found

lookup

public E lookup(java.lang.String name)

Convenience method to look up.

elements

public java.util.Collection<E> elements()

returns list of the elements (not the keys) in this namespace (not about the one of the parent)

Returns:

the list of the named objects

allElements

public java.util.Collection<E> allElements()

parent

public Namespace<E> parent()

returns the fall-back Namespace of this Namespace, i.e. the one where symbols are looked up that are not found in this one.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

copy

public Namespace<E> copy()

reset

private void reset()

set

public <T extends E> void set(ImmutableSet<T> names)

seal

public void seal()

isEmpty

public boolean isEmpty()

isSealed

public boolean isSealed()

simplify

public Namespace<E> simplify()

compress

public Namespace<E> compress()

contains

public boolean contains(E var)

flushToParent

public void flushToParent()