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 will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.

Performing requests

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

What to request ?

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 element itself plus its user-defined name. An occurrence always 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 has been retrieved from a previous query)
• getting occurrences of a given declaration using propagation (#Propagation)

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.

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.