https://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&feed=atom&action=historyStrengthening the AST Library for Rodin 3.0 - Revision history2024-03-29T10:00:25ZRevision history for this page on the wikiMediaWiki 1.33.3https://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9528&oldid=previmported>Vinmont: /* AST nodes construction */2013-02-15T16:07:42Z<p><span dir="auto"><span class="autocomment">AST nodes construction</span></span></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 16:07, 15 February 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l31" >Line 31:</td>
<td colspan="2" class="diff-lineno">Line 31:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">=== Enforcement of conditions on arguments ===</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">Moreover </del>AST nodes and types are now keeping a reference on the factory that was used to build them <del class="diffchange diffchange-inline">and </del>AST library enforces that they have been built <del class="diffchange diffchange-inline">by </del>the same formula factory<del class="diffchange diffchange-inline">. Then we now avoid incoherent </del>nodes and types <del class="diffchange diffchange-inline">by construction regarding their formula factory </del>that <del class="diffchange diffchange-inline">could have lead</del>, <del class="diffchange diffchange-inline">e.g.</del>, <del class="diffchange diffchange-inline">to use reserved words </del>in a <del class="diffchange diffchange-inline">part </del>of a formula <del class="diffchange diffchange-inline">as a free identifier name </del>in <del class="diffchange diffchange-inline">another part</del>.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins class="diffchange diffchange-inline">=== Enforcement of formula factory equality ===</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins class="diffchange diffchange-inline">First of all, </ins>AST nodes and types are now keeping a reference on the factory that was used to build them <ins class="diffchange diffchange-inline">which avoid the multiplication of factories passed as parameter in the rest of the code.</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins class="diffchange diffchange-inline">Then, the </ins>AST library enforces that they have been built <ins class="diffchange diffchange-inline">with </ins>the <ins class="diffchange diffchange-inline">exact </ins>same formula factory <ins class="diffchange diffchange-inline">which forbids to mix </ins>nodes and types <ins class="diffchange diffchange-inline">coming from different factories. We made this decision on the fact </ins>that, <ins class="diffchange diffchange-inline">in most cases</ins>, <ins class="diffchange diffchange-inline">this restriction is not important as all formulas are always </ins>in <ins class="diffchange diffchange-inline">the same language. As </ins>a <ins class="diffchange diffchange-inline">consequence we prevent the construction </ins>of a formula <ins class="diffchange diffchange-inline">with incoherent factories in its children but we also forbid the construction with different factories that are compatible. This last option has been rejected because the performance cost was important to enforce the compatibility </ins>in <ins class="diffchange diffchange-inline">addition to the precedent arguments exposed</ins>.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td></tr>
</table>imported>Vinmonthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9527&oldid=previmported>Vinmont at 09:35, 13 February 20132013-02-13T09:35:56Z<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 09:35, 13 February 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l32" >Line 32:</td>
<td colspan="2" class="diff-lineno">Line 32:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">Moreover AST nodes and types are now keeping a reference on the factory that was used to build them and AST library enforces that they have been built by the same formula factory. Then we now avoid incoherent nodes and types by construction regarding their formula factory that could have lead, e.g., to use reserved words in a part of a formula as a free identifier name in another part.</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td></tr>
</table>imported>Vinmonthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9526&oldid=previmported>Laurent: /* Type Checking */2013-02-12T17:56:57Z<p><span dir="auto"><span class="autocomment">Type Checking</span></span></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 17:56, 12 February 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l21" >Line 21:</td>
<td colspan="2" class="diff-lineno">Line 21:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>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 <del class="diffchange diffchange-inline">on a </del>incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>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 <ins class="diffchange diffchange-inline">to an </ins>incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>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 <del class="diffchange diffchange-inline">identifiers </del>then the bound identifier will be renamed since it is identified by its Bruijn number.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>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 <ins class="diffchange diffchange-inline">identifier </ins>then the bound identifier will be renamed since it is identified by its <ins class="diffchange diffchange-inline">de </ins>Bruijn number.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>The modification of the type checking step introduces the following modifications:</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>The modification of the type checking step introduces the following modifications:</div></td></tr>
</table>imported>Laurenthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9525&oldid=previmported>Laurent: /* Type Environment */2013-02-12T17:54:50Z<p><span dir="auto"><span class="autocomment">Type Environment</span></span></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 17:54, 12 February 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l2" >Line 2:</td>
<td colspan="2" class="diff-lineno">Line 2:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Environment ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Environment ==</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. </div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>First of all we <del class="diffchange diffchange-inline">add </del>a new mechanism to add given sets implicitly introduced by types when new elements are added.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Type environments have changed in Rodin 3.0 in order to reinforce their good</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Then we <del class="diffchange diffchange-inline">create the inferred type environment Java type </del>to <del class="diffchange diffchange-inline">could differentiate a classical type environment and an </del>inferred <del class="diffchange diffchange-inline">one which now references its initial </del>type <del class="diffchange diffchange-inline">environment</del>. <del class="diffchange diffchange-inline">This type is now used </del>in the <del class="diffchange diffchange-inline">type checking </del>result. <del class="diffchange diffchange-inline">Since an inferred type environment content depends on its initial type environment it was a necessary modification to could express all possible inferred type environments.</del></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>use and their robustness. </div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Finally we <del class="diffchange diffchange-inline">add </del>mechanism to separate mutable and immutable type 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 <del class="diffchange diffchange-inline">it is </del>needed (see [[Rodin 3.0 Plug-in Migration Guide]] for more information).</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>First of all<ins class="diffchange diffchange-inline">, </ins>we <ins class="diffchange diffchange-inline">have added </ins>a new mechanism to add given sets implicitly introduced by types when new elements are added.</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Then<ins class="diffchange diffchange-inline">, </ins>we <ins class="diffchange diffchange-inline">have added a new interface </ins>to <ins class="diffchange diffchange-inline">represent </ins>inferred type <ins class="diffchange diffchange-inline">environments</ins>.</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins class="diffchange diffchange-inline">These environments are the ones that are returned </ins>in the result <ins class="diffchange diffchange-inline">of the</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins class="diffchange diffchange-inline">typecheck methods of Formula and Expression</ins>.</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Finally we <ins class="diffchange diffchange-inline">have added </ins>mechanism to separate mutable and immutable type</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>environments by creating two children interfaces of the type environment</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>interface, {{class|ITypeEnvironmentBuilder}} and</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>{{class|ISealedTypeEnvironment}}. This mechanism provides a strong guarantee</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>that a type environment will not be modified if necessary and allows at the</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>same time to be flexible when needed (see [[Rodin 3.0 Plug-in Migration</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Guide]] for more information).</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td></tr>
</table>imported>Laurenthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9524&oldid=previmported>Vinmont: /* AST nodes construction */2013-01-15T10:44:47Z<p><span dir="auto"><span class="autocomment">AST nodes construction</span></span></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 10:44, 15 January 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l18" >Line 18:</td>
<td colspan="2" class="diff-lineno">Line 18:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>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 <del class="diffchange diffchange-inline">allow </del>to avoid exceptions raised later for which source is more complicated to locate.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>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 <ins class="diffchange diffchange-inline">allows </ins>to avoid exceptions raised later for which source is more complicated to locate.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td></tr>
</table>imported>Vinmonthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9523&oldid=previmported>Vinmont: /* AST nodes construction */2013-01-14T10:40:30Z<p><span dir="auto"><span class="autocomment">AST nodes construction</span></span></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 10:40, 14 January 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l18" >Line 18:</td>
<td colspan="2" class="diff-lineno">Line 18:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== AST nodes construction ==</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>AST nodes construction is possible using FormulaFactory methods (direct access to constructors is now explicitly forbidden) and has been strengthened by verifying arguments provided <del class="diffchange diffchange-inline">and that given types provided was </del>valid regarding constructed node <del class="diffchange diffchange-inline">type</del>. Those verifications <del class="diffchange diffchange-inline">is provided </del>with <del class="diffchange diffchange-inline">documentation explicit </del>exceptions raised when conditions on arguments are not respected<del class="diffchange diffchange-inline">, it allows </del>to <del class="diffchange diffchange-inline">improve exceptions meaning and </del>avoid <del class="diffchange diffchange-inline">further </del>exceptions for which source is more complicated to <del class="diffchange diffchange-inline">understand</del>.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>AST nodes construction is possible using <ins class="diffchange diffchange-inline">{{class|</ins>FormulaFactory<ins class="diffchange diffchange-inline">}} </ins>methods (direct access to constructors is now explicitly forbidden) and has been strengthened by verifying <ins class="diffchange diffchange-inline">that </ins>arguments provided <ins class="diffchange diffchange-inline">are </ins>valid regarding constructed node. Those verifications <ins class="diffchange diffchange-inline">are documented </ins>with <ins class="diffchange diffchange-inline">the </ins>exceptions raised when conditions on arguments are not respected<ins class="diffchange diffchange-inline">. It allow </ins>to avoid exceptions <ins class="diffchange diffchange-inline">raised later </ins>for which source is more complicated to <ins class="diffchange diffchange-inline">locate</ins>.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td></tr>
</table>imported>Vinmonthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9522&oldid=previmported>Vinmont at 10:31, 14 January 20132013-01-14T10:31:57Z<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 10:31, 14 January 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l8" >Line 8:</td>
<td colspan="2" class="diff-lineno">Line 8:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del style="font-weight: bold; text-decoration: none;"></del></div></td><td colspan="2"> </td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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 on a incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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 on a incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l17" >Line 17:</td>
<td colspan="2" class="diff-lineno">Line 16:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* 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.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* 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.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">== AST nodes construction ==</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">AST nodes construction is possible using FormulaFactory methods (direct access to constructors is now explicitly forbidden) and has been strengthened by verifying arguments provided and that given types provided was valid regarding constructed node type. Those verifications is provided with documentation explicit exceptions raised when conditions on arguments are not respected, it allows to improve exceptions meaning and avoid further exceptions for which source is more complicated to understand.</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td></tr>
</table>imported>Vinmonthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9521&oldid=previmported>Vinmont: /* Type Checking */2013-01-14T09:03:49Z<p><span dir="auto"><span class="autocomment">Type Checking</span></span></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 09:03, 14 January 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l9" >Line 9:</td>
<td colspan="2" class="diff-lineno">Line 9:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>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 free identifiers. It also allowed to detect and correct a new occurrence of the bug #635 (old name #3574565) that was leading on a incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>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 <ins class="diffchange diffchange-inline">thus </ins>free identifiers. It also allowed to detect and correct a new occurrence of the bug #635 (old name #3574565) that was leading on a incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>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 identifiers then the bound identifier will be renamed since it is <del class="diffchange diffchange-inline">idenfied </del>by its Bruijn number.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>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 identifiers then the bound identifier will be renamed since it is <ins class="diffchange diffchange-inline">identified </ins>by its Bruijn number.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>The modification of the type checking step introduces the following modifications:</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>The modification of the type checking step introduces the following modifications:</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* 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 <del class="diffchange diffchange-inline"> allow to guarantee </del>that incompatible free identifiers names are not introduced <del class="diffchange diffchange-inline">regarding given sets</del>.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* 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 <ins class="diffchange diffchange-inline">guarantees </ins>that incompatible free identifiers names <ins class="diffchange diffchange-inline">or given sets </ins>are not introduced.</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* 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 given set and a free identifier have a name conflict it will be detected during this step <del class="diffchange diffchange-inline">(but since </del>it <del class="diffchange diffchange-inline">could normally occur in the solving type step, the ''typecheck()'' procedure must have already reported this conflict).</del></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* 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 <ins class="diffchange diffchange-inline">a </ins>given set and a free identifier have a name conflict it will <ins class="diffchange diffchange-inline">also </ins>be detected during this step<ins class="diffchange diffchange-inline">. Particularly </ins>it <ins class="diffchange diffchange-inline">will provide a way to detect </ins>and <ins class="diffchange diffchange-inline">raise an {{class|IllegalArgumentException}} when an invalid </ins>type is <ins class="diffchange diffchange-inline">provided at node creation</ins>.</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">* In the ''FreeIdentifier.synthesize()'' procedure if the free identifier name </del>and <del class="diffchange diffchange-inline">its type introduces a given set name conflict, then its given </del>type is <del class="diffchange diffchange-inline">ignored and can result in a type checking failure</del>.</div></td><td colspan="2"> </td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Design]]</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:Developer documentation]]</div></td></tr>
</table>imported>Vinmonthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9520&oldid=previmported>Vinmont: /* Type Environment */2013-01-14T08:48:37Z<p><span dir="auto"><span class="autocomment">Type Environment</span></span></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 08:48, 14 January 2013</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l4" >Line 4:</td>
<td colspan="2" class="diff-lineno">Line 4:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. </div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. </div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>First of all we add a new mechanism to add given sets implicitly introduced by types when new elements are added.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>First of all we add a new mechanism to add given sets implicitly introduced by types when new elements are added.</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Then we create the inferred type environment Java type to could differentiate inferred <del class="diffchange diffchange-inline">environment </del>which now references its initial type environment<del class="diffchange diffchange-inline">, this </del>type is now used <del class="diffchange diffchange-inline">for </del>the type checking result. Since an inferred type environment content depends on its initial type environment it was a necessary modification to could express all possible inferred type environments.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Then we create the inferred type environment Java type to could differentiate <ins class="diffchange diffchange-inline">a classical type environment and an </ins>inferred <ins class="diffchange diffchange-inline">one </ins>which now references its initial type environment<ins class="diffchange diffchange-inline">. This </ins>type is now used <ins class="diffchange diffchange-inline">in </ins>the type checking result. Since an inferred type environment content depends on its initial type environment it was a necessary modification to could express all possible inferred type environments.</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Finally we add mechanism to separate mutable and immutable type 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 <del class="diffchange diffchange-inline">allow </del>at the same time to be flexible when needed (see [[Rodin 3.0 Plug-in Migration Guide]] for more information).</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Finally we add mechanism to separate mutable and immutable type 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 <ins class="diffchange diffchange-inline">allows </ins>at the same time to be flexible when <ins class="diffchange diffchange-inline">it is </ins>needed (see [[Rodin 3.0 Plug-in Migration Guide]] for more information).</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Type Checking ==</div></td></tr>
</table>imported>Vinmonthttps://wiki.event-b.org/index.php?title=Strengthening_the_AST_Library_for_Rodin_3.0&diff=9519&oldid=previmported>Vinmont: Created page with "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..."2013-01-07T10:02:05Z<p>Created page with "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..."</p>
<p><b>New page</b></p><div>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.<br />
<br />
== Type Environment ==<br />
Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. <br />
First of all we add a new mechanism to add given sets implicitly introduced by types when new elements are added.<br />
Then we create the inferred type environment Java type to could differentiate inferred environment which now references its initial type environment, this type is now used for the type checking result. Since an inferred type environment content depends on its initial type environment it was a necessary modification to could express all possible inferred type environments.<br />
Finally we add mechanism to separate mutable and immutable type 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 allow at the same time to be flexible when needed (see [[Rodin 3.0 Plug-in Migration Guide]] for more information).<br />
<br />
== Type Checking ==<br />
<br />
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 free identifiers. It also allowed to detect and correct a new occurrence of the bug #635 (old name #3574565) that was leading on a incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.<br />
<br />
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 identifiers then the bound identifier will be renamed since it is idenfied by its Bruijn number.<br />
<br />
The modification of the type checking step introduces the following modifications:<br />
* 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 allow to guarantee that incompatible free identifiers names are not introduced regarding given sets.<br />
* 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 given set and a free identifier have a name conflict it will be detected during this step (but since it could normally occur in the solving type step, the ''typecheck()'' procedure must have already reported this conflict).<br />
* In the ''FreeIdentifier.synthesize()'' procedure if the free identifier name and its type introduces a given set name conflict, then its given type is ignored and can result in a type checking failure.<br />
* If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.<br />
<br />
[[Category:Design]]<br />
[[Category:Developer documentation]]</div>imported>Vinmont