| java.lang.Object
 de.uka.ilkd.key.logic.Namespace
All known Subclasses: de.uka.ilkd.key.logic.AtPreNamespace,
| Namespace | | public class Namespace implements java.io.Serializable(Code) | | A Namespace keeps track of already used
Name s 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. An instance of Namespace can
operate in normal and protocoled mode, where the protocoled mode
keeps track of all new added names since the last call of
Namespace.startProtocol .
|
| Field Summary | |
| protected Named | localSym
One defined symbol. | | protected int | numLocalSyms
The number of symbols defined in this namespace. | | protected Namespace | parent
The fall-back namespace for symbols not present in this
Namespace. | | protected HashMapFromNameToNamed | protocol
| | protected HashMapFromNameToNamed | symbols
The hashmap that maps a name to a symbols of that name if it
is defined in this Namespace. |
| Constructor Summary | |
| public | Namespace()
Construct an empty Namespace without a parent namespace. | | public | Namespace(HashMapFromNameToNamed protocol)
Construct an empty Namespace with protocol protocol
and without a parent namespace. | | public | Namespace(Namespace parent)
Construct a Namespace that uses parent as a fallback
for finding symbols not defined in this one. | | public | Namespace(Namespace parent, Named sym)
Construct a Namespace that uses parent as a fallback
for finding symbols not defined in this one. |
| localSym | | protected Named localSym(Code) | | One defined symbol. Many Namespaces, e.g. those generated when
a quantified formula is parsed, define only one new symbol,
and it would be a waste of time and space to create a hashmap for that.
So
Namespace.symbols is only initialized when there is more than one
symbol in this namespace. Otherwise, localSym contains
that symbol.
|
| numLocalSyms | | protected int numLocalSyms(Code) | | The number of symbols defined in this namespace. This is different
from symbols.size() because symbols might be null if
there is only one symbol in this Namespace.
|
| parent | | protected Namespace parent(Code) | | The fall-back namespace for symbols not present in this
Namespace.
|
| protocol | | protected HashMapFromNameToNamed protocol(Code) | | Additions can be "recorded" here
|
| symbols | | protected HashMapFromNameToNamed symbols(Code) | | The hashmap that maps a name to a symbols of that name if it
is defined in this Namespace.
|
| Namespace | | public Namespace()(Code) | | Construct an empty Namespace without a parent namespace.
|
| Namespace | | public Namespace(HashMapFromNameToNamed protocol)(Code) | | Construct an empty Namespace with protocol protocol
and without a parent namespace.
|
| Namespace | | public Namespace(Namespace parent)(Code) | | Construct a Namespace that uses parent as a fallback
for finding symbols not defined in this one.
|
| Namespace | | public Namespace(Namespace parent, Named sym)(Code) | | Construct a Namespace that uses parent as a fallback
for finding symbols not defined in this one. Put an entry for
sym in this one.
|
| add | | public void add(Named sym)(Code) | | 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.
|
| add | | public void add(ListOfNamed l)(Code) | | |
| addSafely | | public void addSafely(Named sym)(Code) | | Adds the object sym to this namespace.
Throws a runtime exception if an object with the same name is
already there.
|
| allElements | | public ListOfNamed allElements()(Code) | | |
| elements | | public ListOfNamed elements()(Code) | | returns list of the elements (not the keys) in this
namespace (not about the one of the parent)
the list of the named objects |
| extended | | public Namespace extended(Named sym)(Code) | | creates a new Namespace that has this as parent, and contains
an entry for sym.
the new Namespace |
| getProtocolled | | public IteratorOfNamed getProtocolled()(Code) | | gets symbols added since last startProtocol();
resets the protocol
|
| lookup | | public Named lookup(Name name)(Code) | | 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 Object with name "name" or null if no such an objecthas been found |
| parent | | public Namespace parent()(Code) | | returns the fall-back Namespace of this Namespace, i.e. the one
where symbols are looked up that are not found in this one.
|
| reset | | public void reset()(Code) | | |
| startProtocol | | public void startProtocol()(Code) | | "remember" all additions from now on
|
|
|