imported>Maria |
imported>Laurent |
| Line 1: |
Line 1: |
| − | ==Purpose==
| + | A part of the Rodin 3.0 development aims to strengthen the AST library. This page explains the choices we have done during this step. |
| − | The purpose of the Single View Design is to present everything in a single view in Rodin.
| |
| | | | |
| − | ==Specification== | + | == Type Environment == |
| − | The Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] that is provided by Eclipse.
| |
| | | | |
| − | [[Image:MasterDetails.jpg]]
| + | Type environments have changed in Rodin 3.0 in order to reinforce their good |
| | + | use and their robustness. |
| | | | |
| − | ===The Navigator===
| + | First of all, we have added a new mechanism to add given sets implicitly introduced by types when new elements are added. |
| − | The navigator is the part on the left that contains a tree. It presents all projects and their contents. The users can choose between to ways how the machines and contexts will be presented:
| |
| − | *A simple structure where all machines and contexts are presented on the same level
| |
| − | *A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.
| |
| | | | |
| − | ===The Details===
| + | Then, we have added a new interface to represent inferred type environments. |
| − | The details part is situated on the right and may contain several tabs. The content of each tab may depend on the selection in the navigator. Currently the only tab that exists is the statistics tab. It is possible to add new custom tabs.
| + | These environments are the ones that are returned in the result of the |
| | + | typecheck methods of Formula and Expression. |
| | | | |
| − | ====Statistics====
| + | Finally we have added mechanism to separate mutable and immutable type |
| − | The statistics tab presents information about the state of the proof obligations of the selected node in the navigator.
| + | environments by creating two children interfaces of the type environment |
| | + | interface, {{class|ITypeEnvironmentBuilder}} and |
| | + | {{class|ISealedTypeEnvironment}}. This mechanism provides a strong guarantee |
| | + | that a type environment will not be modified if necessary and allows at the |
| | + | same time to be flexible when needed (see [[Rodin 3.0 Plug-in Migration |
| | + | Guide]] for more information). |
| | | | |
| − | ==User guide== | + | == Type Checking == |
| − | ===Customizing the Navigator===
| + | The type checking step has been strengthened to avoid that the type checker accepts given types implicitly introducing given sets incompatibles with the type environment and thus free identifiers. It also allowed to detect and correct a new occurrence of the bug #635 (old name #3574565) that was leading to an incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success. |
| − | Click on the little triangle in the upper right corner of the navigator view and select ''Customize View''. This opens a dialog that allows you to choose ''Filters'' and ''Content''.
| |
| | | | |
| − | [[Image:Customize.jpg]]
| + | Regarding the legibility for identifiers no modification has been done, that is to say that if the same name is used for a free and bound identifier then the bound identifier will be renamed since it is identified by its de Bruijn number. |
| | | | |
| − | ====Content====
| + | The modification of the type checking step introduces the following modifications: |
| − | Here you can choose what content should be shown in the navigator.
| + | * In the ''typecheck()'' procedure of nodes, we now analyse the type of the nodes that could introduce new given sets and add those given sets to the resulting inferred type environment. It guarantees that incompatible free identifiers names or given sets are not introduced. |
| − | *'''Resources''': All projects, files and folder (keep this one checked!). | + | * In the ''synthesize()'' procedure, that is executed a first time at node creation and a second time during solving types step, we now add the given sets introduced by given types as free identifiers on concerned nodes. As a consequence if a given set and a free identifier have a name conflict it will also be detected during this step. Particularly it will provide a way to detect and raise an {{class|IllegalArgumentException}} when an invalid type is provided at node creation. |
| − | *'''Working Sets''': Allows you to see the working sets as top level elements. If you're not familiar with working sets, consult [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.user/concepts/cworkset.htm eclipse help].
| + | * If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary. |
| − | *'''Simple Context Structure''': Lists all contexts of a project. | |
| − | *'''Complex Context Structure''': Lists all contexts of a project. Contexts that extend another context are attached to it as children in the tree. Contexts that are seen by a machine are attached to the machine as children. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
| |
| − | *'''Simple Machines Structure''': Lists all machines of a project. | |
| − | *'''Complex Context Structure''': Lists all machines of a project. Machines that refine another machine are attached to it as children in the tree. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
| |
| − | *'''Carrier Sets'''
| |
| − | *'''Constants'''
| |
| − | *'''Variables'''
| |
| − | *'''Axioms'''
| |
| − | *'''Invariants'''
| |
| − | *'''Theorems'''
| |
| − | *'''Events'''
| |
| − | *'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.
| |
| | | | |
| − | Here's an example of what the same projects looks like once using the complex machine and context structure (left) and once using the simple version (right).
| + | == AST nodes construction == |
| | + | AST nodes construction is possible using {{class|FormulaFactory}} methods (direct access to constructors is now explicitly forbidden) and has been strengthened by verifying that arguments provided are valid regarding constructed node. Those verifications are documented with the exceptions raised when conditions on arguments are not respected. It allows to avoid exceptions raised later for which source is more complicated to locate. |
| | | | |
| − | [[Image:Complex.jpg]][[Image:Simple.jpg]] | + | [[Category:Design]] |
| − | | + | [[Category:Developer documentation]] |
| − | ====Filters====
| |
| − | The filters let you choose what to hide in the navigator.
| |
| − | *'''File extensions''': There are various filters to hide certain types of files.
| |
| − | *'''All files and folders''': Hides all files and subfolders.
| |
| − | *'''Non Rodin Projects''': Hides all non Rodin projects. Also hides closed Rodin Projects.
| |
| − | *'''Closed Projects''': Hides all closed projects.
| |
| − | | |
| − | There are some additional filters that can be found on top of the navigator:
| |
| − | | |
| − | [[Image:PoFilters.JPG]]
| |
| − | | |
| − | Enter a text into the field and only proof obligations containing the string will be shown. If you push the green button, all discharged proof obligations will be hidden.
| |
| − | | |
| − | ===Statistics===
| |
| − | The content displayed in the statistics tab depends on the selection in the navigator. Generally it shows an overview of the status of all proof obligations of the selected elements and a more detailed view below (if available). If a project is selected this means that in the overview the statistics for all proof obligations of that project are shown. In the detailed viewed each machine and context is listed with their own statistics. If you double click on an element in the detailed view, the corresponding element will be selected in the navigator.
| |
| − | | |
| − | It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.
| |
| − | | |
| − | ==Developer guide==
| |
| − | ===Extending Single View Design===
| |
| − | Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] and [http://help.eclipse.org/stable/index.jsp?topic=/org.eclipse.platform.doc.isv/guide/forms_master_details.htm the Master/Details pattern]. The part on the left (the navigator) is the master part. You can add custom filters, content providers and action providers in a plug-in of your own. Add the extension <code>org.eclipse.ui.navigator.viewer</code>. There you can add viewerContentBindings and viewerActionBindings with viewerId <code>fr.systerel.explorer.navigator.view</code>. This binds your custom content, actions and filters to the navigator. The part on the right is the details part. You can add tabs of your own by extending <code>fr.systerel.explorer.masterDetails</code>.
| |
| − | | |
| − | In the picture you can see what types the nodes in the navigator have.
| |
| − | | |
| − | [[Image:Tree.jpg]]
| |
| − | | |
| − | ====Adding a content provider to the navigator====
| |
| − | To add a custom content provider you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new navigatorContent. Example: You want to add a new child under the IMachineFile nodes. Define a navigatorContent and add triggerPoints. There you add a new <code>instanceof</code> with value <code>org.eventb.core.IMachineFile</code>. The priority of the navigatorContent decides in what order the content is shown with respect to other content providers. (For example the content provider for the variables has a higher priority than the one for invariants, that's why the variables appear before the invariants in the tree.) You need to provide a contentProvider and a labelProvider class. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your navigatorContent in your viewerContentBindings.
| |
| − | | |
| − | <code>
| |
| − | <extension
| |
| − | point="org.eclipse.ui.navigator.navigatorContent">
| |
| − | <navigatorContent
| |
| − | contentProvider="example.ContentProvider"
| |
| − | id="example.navigatorContent"
| |
| − | labelProvider="example.LabelProvider"
| |
| − | name="Example Content">
| |
| − | <triggerPoints>
| |
| − | <instanceof
| |
| − | value="org.eventb.core.IMachineFile">
| |
| − | </instanceof>
| |
| − | </triggerPoints>
| |
| − | </navigatorContent>
| |
| − | </extension>
| |
| − | </code>
| |
| − | | |
| − | <code>
| |
| − | <extension
| |
| − | point="org.eclipse.ui.navigator.viewer">
| |
| − | <viewerContentBinding
| |
| − | viewerId="fr.systerel.explorer.navigator.view">
| |
| − | <includes>
| |
| − | <contentExtension
| |
| − | pattern="example.navigatorContent">
| |
| − | </contentExtension>
| |
| − | </includes>
| |
| − | </viewerContentBinding>
| |
| − | </extension>
| |
| − | </code>
| |
| − | | |
| − | ====Adding a filter to the navigator====
| |
| − | To add a custom filter you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new commonFilter. You can either provide an implementation for <code>ViewerFilter</code> or use xml filterExpressions. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your commonFilter in your viewerContentBindings.
| |
| − | | |
| − | ====Adding an action provider to the navigator====
| |
| − | To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings.
| |
| − | | |
| − | ====Adding a tab with custom content to the details part====
| |
| − | To add a custom tab use the <code>fr.systerel.explorer.masterDetails</code> extension. Add a new detailsTab and provide a class that implements <code>INavigatorDetailsTab</code>.
| |
| − | | |
| − | [[Category:Work in progress]] | |
A part of the Rodin 3.0 development aims to strengthen the AST library. This page explains the choices we have done during this step.
Type Environment
Type environments have changed in Rodin 3.0 in order to reinforce their good
use and their robustness.
First of all, we have added a new mechanism to add given sets implicitly introduced by types when new elements are added.
Then, we have added a new interface to represent inferred type environments.
These environments are the ones that are returned in the result of the
typecheck methods of Formula and Expression.
Finally we have added mechanism to separate mutable and immutable type
environments by creating two children interfaces of the type environment
interface, ITypeEnvironmentBuilder and
ISealedTypeEnvironment. This mechanism provides a strong guarantee
that a type environment will not be modified if necessary and allows at the
same time to be flexible when needed (see [[Rodin 3.0 Plug-in Migration
Guide]] for more information).
Type Checking
The type checking step has been strengthened to avoid that the type checker accepts given types implicitly introducing given sets incompatibles with the type environment and thus free identifiers. It also allowed to detect and correct a new occurrence of the bug #635 (old name #3574565) that was leading to an incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.
Regarding the legibility for identifiers no modification has been done, that is to say that if the same name is used for a free and bound identifier then the bound identifier will be renamed since it is identified by its de Bruijn number.
The modification of the type checking step introduces the following modifications:
- In the typecheck() procedure of nodes, we now analyse the type of the nodes that could introduce new given sets and add those given sets to the resulting inferred type environment. It guarantees that incompatible free identifiers names or given sets are not introduced.
- In the synthesize() procedure, that is executed a first time at node creation and a second time during solving types step, we now add the given sets introduced by given types as free identifiers on concerned nodes. As a consequence if a given set and a free identifier have a name conflict it will also be detected during this step. Particularly it will provide a way to detect and raise an IllegalArgumentException when an invalid type is provided at node creation.
- If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.
AST nodes construction
AST nodes construction is possible using FormulaFactory methods (direct access to constructors is now explicitly forbidden) and has been strengthened by verifying that arguments provided are valid regarding constructed node. Those verifications are documented with the exceptions raised when conditions on arguments are not respected. It allows to avoid exceptions raised later for which source is more complicated to locate.
