Index Query

Purpose

The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences allows for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.

Performing queries

The indexer contents are not directly accessible to other plug-ins. Queries are sent through a IIndexQuery object provided by the RodinCore plug-in.

What to query ?

Two types of information can be queried :

• declarations (IDeclaration)
• occurrences (IOccurrence)

A declaration is the unique identifier of an entity in the index repository. It consists in a handle of the declared element itself plus its user-defined name. Every occurrence refers to one single declaration.

Several query types can be performed, depending on the starting point :

• getting the declaration of a given element (as IInternalElement)
• getting the declarations of elements that match a given user-defined name (as String) in a given file
• getting the declarations of elements that occur, or could occur, in a given file
• getting occurrences of a given declaration (this declaration having been retrieved from a previous query)
• getting occurrences of a given declaration using propagation (see Propagation hereafter )

Thus, a declaration is the key to retrieve occurrences.

As the result might be too coarse, queries can be filtered out using various criterias (see IIndexQuery interface for more details).

Occurrences

An occurrence (IOccurrence) describes a location (IRodinLocation) and a kind of occurrence (IOccurrenceKind) of an element (referred to through its IDeclaration). For example, in Event-B, an occurrence could be:

location

in IAxiom 'a' (handle), in the PREDICATE_ATTRIBUTE, between characters 7 and 12

kind

REFERENCE

declaration

the ICarrierSet 's' (handle), named "set1"

Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level. See more in Event-B Indexers.

Propagation

Propagation is a way to get occurrences of several declarations, starting from one single declaration. In particular, it addresses cases where various declarations represent the same entity. The problem is that each declaration has separate occurrences. The propagation mechanism allows to get all occurrences of the entity, whatever the underlying declaration.

For example, in Event-B, a variable can be redeclared in a refining machine. In the index repository, each variable has a separate declaration and separate occurrences. However, it might be interesting in some cases to consider occurrences of the concrete variable as a subset of occurrences of the abstract one. The concept here is to 'propagate' the query about the abstract variable to occurrences of the concrete one. This is achievable in this case thanks to event-B propagators.

See more in Event-B Indexers Propagation.

Getting a valid result

The indexing system data is constantly evolving, as long as files get modified. Furthermore, as indexing is performed as a background operation, one cannot guess whether the indexing has completed or not. The system may also be updating its data, making it temporarily incoherent. Thus, the problem arises to ensure that the data is valid and up-to-date.

To that end, a method is provided by the IIndexQuery, that blocks the current thread until all planned files are indexed. Requests performed after that will thus return a valid result and benefit from the most up-to-date version of the data.

Query Examples

Here are a few examples of index queries. They are all implicitly preceded by the following code

 final IIndexQuery query = RodinCore.makeIndexQuery();
 query.waitUpToDate();

that creates the query object and waits until the index becomes up-to-date.

Occurrences of an element

Data :

• a handle 'var' of an IVariable

To get its declaration

final IDeclaration declVar = query.getDeclaration(var);

Remember to check for a null return value.

From that declaration, the user-defined name of the variable can be retrieved

final String userDefinedName = declVar.getName();

To get the occurrences of 'var'

final Set<IOccurrence> occurrences = query.getOccurrences(declVar);

Homonyms in a file

Data :

• a handle 'file' of an IRodinFile
• a name "foo"

Goal : getting declarations of all elements named "foo" that occur in 'file'

First, all declarations of all indexed elements that occur in 'file' are retrieved. Then a query filter on the name is used.

final Set<IDeclaration> declarations = query.getDeclarations(file);
query.filterName(declarations, "foo");

At the end, 'declarations' contains the declarations of all elements named "foo" occurring in 'file'.

Parameters of an event

Data :

• a handle 'file' of an IRodinFile
• a handle 'evt1' of an IEvent

Goal : getting the declarations of all parameters of 'evt1'

final Set<IDeclaration> declarations = query.getDeclarations(file);
query.filterType(declarations, IParameter.ELEMENT_TYPE);

final Set<IOccurrence> occurrences = query.getOccurrences(declarations);
query.filterKind(occurrences, EventBPlugin.DECLARATION);

final IInternalLocation evt1Location = RodinCore.getInternalLocation(evt1);
query.filterLocation(occurrences, evt1Location);

final Set<IDeclaration> paramsOfEvt1 = query.getDeclarations(occurrences);

We first get all declarations of elements that occur in 'file', and we filter them so as to keep only declarations of parameters.

We then get all occurrences of those parameters. We want parameters that have a DECLARATION occurrence in 'evt1'. To that aim, two filters are successively applied to the occurrences.

Finally we get the declarations (IDeclaration) associated with the filtered occurrences.

Query with propagation

Data :

• a handle 'var' to a IVariable

Goal : getting all occurrences of 'var' including occurrences in machines that redeclare 'var'.

final IDeclaration declaration = query.getDeclaration(var);
if (declaration != null) {
   final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration, EventBPlugin.getIdentifierPropagator());
   ...
}

Here, we start from the 'var' handle but of course, we could also have obtained its declaration by any other way (see other examples).

Returned occurrences can then be filtered, as usual.