Index Query - Revision history

imported>Laurent at 09:31, 10 March 2009

2009-03-10T09:31:51Z

← Older revision		Revision as of 09:31, 10 March 2009
Line 9:		Line 9:
	===What to query ?===		===What to query ?===

	Two types of information can be queried :		Two types of information can be queried:
	* declarations ({{class\|IDeclaration}})		* declarations ({{class\|IDeclaration}})
	* occurrences ({{class\|IOccurrence}})		* occurrences ({{class\|IOccurrence}})
Line 17:		Line 17:
	Every occurrence refers to one single declaration.		Every occurrence refers to one single declaration.

	Several query types can be performed, depending on the starting point :		Several query types can be performed, depending on the starting point:
	* getting the declaration of a given element (as {{class\|IInternalElement}})		* getting the declaration of a given element (as {{class\|IInternalElement}})
	* getting the declarations of elements that match a given user-defined name (as {{class\|String}}) in a given file		* getting the declarations of elements that match a given user-defined name (as {{class\|String}}) in a given file
Line 65:		Line 65:
	===Occurrences of an element===		===Occurrences of an element===

	Input Data :		Input Data:
	* a handle 'var' of an IVariable		* a handle 'var' of an IVariable

Line 84:		Line 84:
	===Homonyms in a file===		===Homonyms in a file===

	Input Data :		Input Data:
	* a handle 'file' of an {{class\|IRodinFile}}		* a handle 'file' of an {{class\|IRodinFile}}
	* a name "foo"		* a name "foo"

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

Line 101:		Line 101:
	===Parameters of an event===		===Parameters of an event===

	Input Data :		Input Data:
	* a handle 'file' of an {{class\|IRodinFile}}		* a handle 'file' of an {{class\|IRodinFile}}
	* a handle 'evt1' of an {{class\|IEvent}}		* a handle 'evt1' of an {{class\|IEvent}}

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

Line 129:		Line 129:
	===Query with propagation===		===Query with propagation===

	Input Data :		Input Data:
	* a handle 'var' to a {{class\|IVariable}}		* a handle 'var' to a {{class\|IVariable}}

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

imported>Laurent: /* Query with propagation */

2009-03-10T09:29:24Z

Query with propagation

← Older revision		Revision as of 09:29, 10 March 2009
Line 129:		Line 129:
	===Query with propagation===		===Query with propagation===

	Data :		Input Data :
	* a handle 'var' to a {{class\|IVariable}}		* a handle 'var' to a {{class\|IVariable}}

imported>Laurent: /* Query Examples */

2009-03-10T09:29:05Z

Query Examples

← Older revision		Revision as of 09:29, 10 March 2009
Line 57:		Line 57:

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


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


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


	===Occurrences of an element===		===Occurrences of an element===

	Data :		Input Data :
	* a handle 'var' of an IVariable		* a handle 'var' of an IVariable

Line 87:		Line 84:
	===Homonyms in a file===		===Homonyms in a file===

	Data :		Input Data :
	* a handle 'file' of an {{class\|IRodinFile}}		* a handle 'file' of an {{class\|IRodinFile}}
	* a name "foo"		* a name "foo"
Line 93:		Line 90:
	Goal :		Goal :
	getting declarations of all elements named "foo" that occur in 'file'		getting declarations of all elements named "foo" that occur in 'file'


	First, all declarations of all indexed elements that occur in 'file' are retrieved.		First, all declarations of all indexed elements that occur in 'file' are retrieved.
Line 105:		Line 101:
	===Parameters of an event===		===Parameters of an event===

	Data :		Input Data :
	* a handle 'file' of an {{class\|IRodinFile}}		* a handle 'file' of an {{class\|IRodinFile}}
	* a handle 'evt1' of an {{class\|IEvent}}		* a handle 'evt1' of an {{class\|IEvent}}
Line 142:		Line 138:
	final IDeclaration declaration = query.getDeclaration(var);		final IDeclaration declaration = query.getDeclaration(var);
	if (declaration != null) {		if (declaration != null) {
	final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration, EventBPlugin.getIdentifierPropagator());		final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration,
			EventBPlugin.getIdentifierPropagator());
	...		...
	}		}

imported>Laurent: /* Query Examples */

2009-03-10T09:19:19Z

Query Examples

← Older revision		Revision as of 09:19, 10 March 2009
Line 63:		Line 63:


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

imported>Laurent: /* Performing queries */

2009-03-10T09:17:10Z

Performing queries

← Older revision		Revision as of 09:17, 10 March 2009
Line 5:		Line 5:
	==Performing queries==		==Performing queries==

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

	===What to query ?===		===What to query ?===
Line 14:		Line 14:

	A declaration is the unique identifier of an entity in the index repository.		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.		It consists in a handle of the declared element itself plus its user-defined name.
	An occurrence ~~always~~ refers to one single declaration.		Every occurrence refers to one single declaration.

	Several query types can be performed, depending on the starting point :		Several query types can be performed, depending on the starting point :
Line 21:		Line 21:
	* getting the declarations of elements that match a given user-defined name (as {{class\|String}}) in a given file		* getting the declarations of elements that match a given user-defined name (as {{class\|String}}) in a given file
	* getting the declarations of elements that occur, or could occur, 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 (this declaration having been retrieved from a previous query)
	* getting occurrences of a given declaration using propagation (see [[#Propagation\|Propagation]] hereafter )		* getting occurrences of a given declaration using propagation (see [[#Propagation\|Propagation]] hereafter )

Line 44:		Line 44:
	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.		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.		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]].		See more in [[Event-B Indexers#Propagation\|Event-B Indexers Propagation]].

	===Getting a valid result===		===Getting a valid result===

imported>Laurent: /* Purpose */

2009-03-10T09:11:26Z

Purpose

← Older revision		Revision as of 09:11, 10 March 2009
Line 1:		Line 1:
	==Purpose==		==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.		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==		==Performing queries==

imported>Nicolas: /* Propagation */

2009-03-05T07:44:33Z

Propagation

← Older revision		Revision as of 07:44, 5 March 2009
Line 46:		Line 46:
	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.		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]].		See more in [[Event-B Indexers#Propagation]].


	===Getting a valid result===		===Getting a valid result===

imported>Mathieu: /* Occurrences */

2009-03-03T22:08:05Z

Occurrences

← Older revision		Revision as of 22:08, 3 March 2009
Line 33:		Line 33:
	For example, in Event-B, an occurrence could be:		For example, in Event-B, an occurrence could be:

	; location: in IAxiom 'a' (handle), in the PREDICATE_ATTRIBUTE, between characters 7 and 12		; location: in {{class\|IAxiom}} 'a' (handle), in the PREDICATE_ATTRIBUTE, between characters 7 and 12
	; kind: REFERENCE		; kind: REFERENCE
	; declaration: the ICarrierSet 's' (handle), named "set1"		; declaration: the {{class\|ICarrierSet}} 's' (handle), named "set1"

	Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level.		Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level.

imported>Mathieu: /* What to query ? */

2009-03-03T22:06:52Z

What to query ?

← Older revision		Revision as of 22:06, 3 March 2009
Line 22:		Line 22:
	* getting the declarations of elements that occur, or could occur, 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 (this declaration has been retrieved from a previous query)
	* getting occurrences of a given declaration using propagation ([[#Propagation]])		* getting occurrences of a given declaration using propagation (see [[#Propagation\|Propagation]] hereafter )

	Thus, a declaration is the key to retrieve occurrences.		Thus, a declaration is the key to retrieve occurrences.

imported>Nicolas: /* Query with propagation */

2009-03-03T16:45:39Z

Query with propagation

← Older revision		Revision as of 16:45, 3 March 2009
Line 142:		Line 142:
	<pre>		<pre>
	final IDeclaration declaration = query.getDeclaration(var);		final IDeclaration declaration = query.getDeclaration(var);
			if (declaration != null) {
	final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration, EventBPlugin.getIdentifierPropagator());		final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration, EventBPlugin.getIdentifierPropagator());
			...
			}
	</pre>		</pre>