- xhtbl: we added the construction + to place several keys in one cell

- basic_2_src: corrected and updated to use the operator +

diff --git a/helm/www/lambda_delta/BTM.html b/helm/www/lambda_delta/BTM.html
index f7ad182885dc51c9bdf54e68a9094725e0a88445..a08104cb2a30aff06e87f2017bb24e971988d541 100644 (file)
--- a/helm/www/lambda_delta/BTM.html
+++ b/helm/www/lambda_delta/BTM.html
@@ -18,8 +18,8 @@
    <div class="text">This table shows how the first 45 positive integers
          are distributed in the four classes.
    </div>
-   <div class="text"/>
+   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">class</td><td class="snns text grey">contents</td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component orange">p</td><td class="snns text orange"><br/></td><td class="snnn number orange">1</td><td class="snnn number orange">4</td><td class="snnn number orange">7</td><td class="snnn number orange">10</td><td class="snnn number orange">13</td><td class="snnn number orange">16</td><td class="snnn number orange">19</td><td class="snnn number orange">22</td><td class="snnn number orange">25</td><td class="snnn number orange">28</td><td class="snnn number orange">31</td><td class="snnn number orange">34</td><td class="snnn number orange">37</td><td class="snnn number orange">40</td><td class="ssnn number orange">43</td></tr><tr><td class="snns component green">q</td><td class="snns text green"><br/></td><td class="snnn number green">5</td><td class="snnn number green">11</td><td class="snnn number green">15</td><td class="snnn number green">17</td><td class="snnn number green">23</td><td class="snnn number green">29</td><td class="snnn number green">33</td><td class="snnn number green">35</td><td class="snnn number green">41</td><td class="snnn number green">45</td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="ssnn number green"><br/></td></tr><tr><td class="snns component sky">s</td><td class="snns text sky"><br/></td><td class="snnn number sky">2</td><td class="snnn number sky">6</td><td class="snnn number sky">8</td><td class="snnn number sky">14</td><td class="snnn number sky">18</td><td class="snnn number sky">20</td><td class="snnn number sky">24</td><td class="snnn number sky">26</td><td class="snnn number sky">32</td><td class="snnn number sky">38</td><td class="snnn number sky">42</td><td class="snnn number sky">44</td><td class="snnn number sky"><br/></td><td class="snnn number sky"><br/></td><td class="ssnn number sky"><br/></td></tr><tr><td class="snss component magenta">t</td><td class="snss text magenta"><br/></td><td class="snsn number magenta">3</td><td class="snsn number magenta">9</td><td class="snsn number magenta">12</td><td class="snsn number magenta">21</td><td class="snsn number magenta">27</td><td class="snsn number magenta">30</td><td class="snsn number magenta">36</td><td class="snsn number magenta">39</td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="sssn number magenta"><br/></td></tr></tbody></table></div>
 
-   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-10-13T23:29:26+02:00</div>
+   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-10-15T17:11:10+02:00</div>
 </body>
 </html>

diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html
index 3000958e89746558337a5f48ce7e4b41ce28435e..7c16c7d4bdbc303b02ab89a82fd9370d1a136e01 100644 (file)
--- a/helm/www/lambda_delta/apps_2.html
+++ b/helm/www/lambda_delta/apps_2.html
@@ -51,12 +51,12 @@
         The notation for the relations or functions introduced in each file
         is shown in parentheses (? are placeholders).
    </div>
-   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component orange">MLTT1</td><td class="snns plane orange"><br/></td><td class="snns file orange">genv_primitive</td><td class="ssnn file orange">judgement</td></tr><tr><td class="snns component red">functional</td><td class="snns plane red">reduction and type machine</td><td class="snns file red">rtm</td><td class="ssnn file red">rtm_step ( ? ⇨ ? )</td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">unfold</td><td class="snss file red">lift ( ↑[?,?] ? )</td><td class="sssn file red">subst ( [?←?] ? )</td></tr></tbody></table></div>
+   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component orange">MLTT1</td><td class="snns plane orange"/><td class="snns file orange">genv_primitive</td><td class="ssnn file orange">judgement</td></tr><tr><td class="snns component red">functional</td><td class="snns plane red">reduction and type machine</td><td class="snns file red">rtm</td><td class="ssnn file red">rtm_step ( ? ⇨ ? )</td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">unfold</td><td class="snss file red">lift ( ↑[?,?] ? )</td><td class="sssn file red">subst ( [?←?] ? )</td></tr></tbody></table></div>
 
    <div class="head2">Physical Structure of the Specification</div>
    <div class="text">The source files are grouped in directories,
          one for each component.
    </div>
-   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-10-13T23:29:26+02:00</div>
+   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-10-15T17:11:10+02:00</div>
 </body>
 </html>

diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html
index 108da399f7e74507ffeede80cbdb4cf8703b1ea6..13150ff4978822d3f35ccf1cd8f2f454aab36fff 100644 (file)
--- a/helm/www/lambda_delta/basic_2.html
+++ b/helm/www/lambda_delta/basic_2.html
@@ -29,7 +29,7 @@
    <div class="text">Here is a numerical acount of the specification's contents
          and its timeline.
    </div>
-   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">199</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">739801</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">70</td><td class="snns plane green">lemmas</td><td class="snnn number green">880</td><td class="snns plane green">total</td><td class="ssnn number green">950</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">40</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">72</td><td class="snss plane yellow">total</td><td class="sssn number yellow">112</td></tr></tbody></table></div>
+   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">198</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">733870</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">70</td><td class="snns plane green">lemmas</td><td class="snnn number green">879</td><td class="snns plane green">total</td><td class="ssnn number green">949</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">40</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">72</td><td class="snss plane yellow">total</td><td class="sssn number yellow">112</td></tr></tbody></table></div>
    <ul><li><span class="date">In progress.</span>
          Context-sensitive subject equivalence
         for native type assignment.
@@ -74,12 +74,12 @@
         The notation for the relations or functions introduced in each file
         is shown in parentheses (? are placeholders).
    </div>
-   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">dynamic typing</td><td class="snns plane prune">stratified native validity</td><td class="snns file prune">snv ( ⦃?,?⦄ ⊩ ? :[?] )</td><td class="snnn file prune">snv_lift</td><td class="snnn file prune">snv_aaa</td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">equivalence</td><td class="snns plane blue">context-sensitive equivalence</td><td class="snns file blue">lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )</td><td class="snnn file blue">lfpcs_aaa</td><td class="snnn file blue">lfpcs_lfprs</td><td class="snnn file blue">lfpcs_lfpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="nnns plane blue"><br/></td><td class="snns file blue">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file blue">cpcs_ltpss</td><td class="snnn file blue">cpcs_delift</td><td class="snnn file blue">cpcs_aaa</td><td class="snnn file blue">cpcs_ltpr</td><td class="snnn file blue">cpcs_cprs</td><td class="snnn file blue">cpcs_cpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">conversion</td><td class="snns plane sky">context-sensitive conversion</td><td class="snns file sky">lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )</td><td class="snnn file sky">lfpc_lfpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="nnns component sky"><br/></td><td class="nnns plane sky"><br/></td><td class="snns file sky">cpc ( ? ⊢ ? ⬌ ? )</td><td class="snnn file sky">cpc_cpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">computation</td><td class="snns plane cyan">extended computation</td><td class="snns file cyan">xprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )</td><td class="snnn file cyan">xprs_lift</td><td class="snnn file cyan">xprs_aaa</td><td class="snnn file cyan">xprs_cprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">weakly normalizing computation</td><td class="snns file cyan">cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )</td><td class="snnn file cyan">cpe_cpe</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">strongly normalizing computation</td><td class="snns file cyan">csn_vector ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_cpr_vector</td><td class="snnn file cyan">csn_tstc_vector</td><td class="snnn file cyan">csn_aaa</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">csn ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_alt ( ? ⊢ ⬊⬊* ? )</td><td class="snnn file cyan">csn_lift</td><td class="snnn file cyan">csn_cpr</td><td class="snnn file cyan">csn_lfpr</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-sensitive computation</td><td class="snns file cyan">lfprs ( ⦃?⦄ ➡* ⦃?⦄ )</td><td class="snnn file cyan">lfprs_aaa</td><td class="snnn file cyan">lfprs_cprs</td><td class="snnn file cyan">lfprs_lfprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file cyan">cprs_lift</td><td class="snnn file cyan">cprs_delift</td><td class="snnn file cyan">cprs_aaa</td><td class="snnn file cyan">cprs_ltpr</td><td class="snnn file cyan">cprs_lfpr</td><td class="snnn file cyan">cprs_cprs</td><td class="snnn file cyan">cprs_lfprs</td><td class="snnn file cyan">cprs_tstc</td><td class="ssnn file cyan">cprs_tstc_vector</td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-free computation</td><td class="snns file cyan">ltprs ( ? ➡* ? )</td><td class="snnn file cyan">ltprs_alt ( ? ➡➡* ? )</td><td class="snnn file cyan">ltprs_ldrop</td><td class="snnn file cyan">ltprs_ltprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">tprs ( ? ➡* ?)</td><td class="snnn file cyan">tprs_lift</td><td class="snnn file cyan">tprs_tprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td><td class="snns file cyan">lsubc ( ? ⊑[?] ? )</td><td class="snnn file cyan">lsubc_ldrop</td><td class="snnn file cyan">lsubc_ldrops</td><td class="snnn file cyan">lsubc_lsuba</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">support for abstract computation properties</td><td class="snns file cyan">acp</td><td class="snnn file cyan">acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )</td><td class="snnn file cyan">acp_aaa</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">reducibility</td><td class="snns plane water">extended reduction</td><td class="snns file water">xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )</td><td class="snnn file water">xpr_lift</td><td class="snnn file water">xpr_aaa</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive focalized reduction</td><td class="snns file water">cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">cnfpr_ltpss</td><td class="snnn file water">cfpr_aaa</td><td class="snnn file water">cfpr_cpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free focalized reduction</td><td class="snns file water">lfpr ( ⦃?⦄ ➡ ⦃?⦄ )</td><td class="snnn file water">lfpr_aaa</td><td class="snnn file water">lfpr_cpr</td><td class="snnn file water">lfpr_fpr</td><td class="snnn file water">lfpr_lfpr</td><td class="snnn file water">lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">fpr_cpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive normal forms</td><td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td><td class="snnn file water">cnf_lift</td><td class="snnn file water">cnf_cif</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reduction</td><td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file water">cpr_lift</td><td class="snnn file water">cpr_tpss</td><td class="snnn file water">cpr_ltpss</td><td class="snnn file water">cpr_delift</td><td class="snnn file water">cpr_aaa</td><td class="snnn file water">cpr_ltpr</td><td class="snnn file water">cpr_cpr</td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reducible forms</td><td class="snns file water">crf ( ? ⊢ 𝐑⦃?⦄ )</td><td class="snnn file water">crf_append</td><td class="snnn file water">cif ( ? ⊢ 𝐈⦃?⦄ )</td><td class="snnn file water">cif_append</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free normal forms</td><td class="snns file water">thnf ( 𝐇𝐍⦃?⦄ )</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free reduction</td><td class="snns file water">ltpr ( ? ➡ ? )</td><td class="snnn file water">ltpr_ldrop</td><td class="snnn file water">ltpr_tps</td><td class="snnn file water">ltpr_ltpss_dx</td><td class="snnn file water">ltpr_ltpss_sn</td><td class="snnn file water">ltpr_aaa</td><td class="snnn file water">ltpr_ltpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">tpr ( ? ➡ ? )</td><td class="snnn file water">tpr_lift</td><td class="snnn file water">tpr_tpss</td><td class="snnn file water">tpr_delift</td><td class="snnn file water">tpr_tpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">unwind</td><td class="snns plane green"><br/></td><td class="snns file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">local env. ref. for stratified static type assignment</td><td class="snns file grass">lsubss ( ? ⁝⊑ ? )</td><td class="snnn file grass">lsubss_ldrop</td><td class="snnn file grass">lsubss_ssta</td><td class="snnn file grass">lsubss_lsubss</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">stratified static type assignment</td><td class="snns file grass">ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )</td><td class="snnn file grass">ssta_lift</td><td class="snnn file grass">ssta_ltpss_dx</td><td class="snnn file grass">ssta_ltpss_sn</td><td class="snnn file grass">ssta_aaa</td><td class="snnn file grass">ssta_ssta</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ⁝⊑ ? )</td><td class="snnn file grass">lsuba_ldrop</td><td class="snnn file grass">lsuba_aaa</td><td class="snnn file grass">lsuba_lsuba</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⊢ ? ⁝ ? )</td><td class="snnn file grass">aaa_lift</td><td class="snnn file grass">aaa_lifts</td><td class="snnn file grass">aaa_ltpss_dx</td><td class="snnn file grass">aaa_ltpss_sn</td><td class="snnn file grass">aaa_aaa</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass">sd</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">basic local env. thinning</td><td class="snns file yellow">thin ( ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">thin_ldrop</td><td class="snnn file yellow">thin_delift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">inverse basic term relocation</td><td class="snns file yellow">delift ( ? ⊢ ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift</td><td class="snnn file yellow">delift_tpss</td><td class="snnn file yellow">delift_ltpss</td><td class="snnn file yellow">delift_delift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss_sn ( ? ⊢ ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_sn_ldrop</td><td class="snnn file yellow">ltpss_sn_tps</td><td class="snnn file yellow">ltpss_sn_tpss</td><td class="snnn file yellow">ltpss_sn_ltpss_sn</td><td class="snnn file yellow">ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">ltpss_dx ( ? ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_dx_ldrop</td><td class="snnn file yellow">ltpss_dx_tps</td><td class="snnn file yellow">ltpss_dx_tpss</td><td class="snnn file yellow">ltpss_dx_ltpss_dx</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⊢ ? ▶*[?,?] ? )</td><td class="snnn file yellow">tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop</td><td class="snnn file yellow">ldrops_ldrops</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift</td><td class="snnn file yellow">lifts_lifts</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td><td class="snnn file yellow">gr2_gr2</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">tps ( ? ⊢ ? ▶[?,?] ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_append</td><td class="snnn file orange">ldrop_lpx</td><td class="snnn file orange">ldrop_sfr</td><td class="snnn file orange">ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">local env. ref. for substitution</td><td class="snns file orange">lsubs ( ? ≼[?,?] ? )</td><td class="snnn file orange">(lsubs_lsubs)</td><td class="snnn file orange">lsubs_sfr ( ≽[?,?] ? )</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">same head term form</td><td class="snns file red">tshf ( ? ≈ ? )</td><td class="snnn file red">(tshf_tshf)</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc</td><td class="snnn file red">tstc_vector</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @@ ? )</td><td class="snnn file red">cl_weight ( #{?,?} )</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( #{?} )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="snnn file red">lenv_append ( ? @@ ? )</td><td class="snnn file red">lenv_px</td><td class="snnn file red">lenv_px_bi</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( #{?} )</td><td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td><td class="snnn file red">term_vector</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
+   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">dynamic typing</td><td class="snns plane prune">stratified native validity</td><td class="snns file prune">snv ( ⦃?,?⦄ ⊩ ? :[?] )</td><td class="snnn file prune">snv_lift snv_aaa</td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">equivalence</td><td class="snns plane blue">focalized equivalence</td><td class="snns file blue">lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )</td><td class="snnn file blue">lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="snns plane blue">context-sensitive equivalence</td><td class="snns file blue">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file blue">cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">conversion</td><td class="snns plane sky">focalized conversion</td><td class="snns file sky">lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )</td><td class="snnn file sky">lfpc_lfpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="nnns component sky"><br/></td><td class="snns plane sky">context-sensitive conversion</td><td class="snns file sky">cpc ( ? ⊢ ? ⬌ ? )</td><td class="snnn file sky">cpc_cpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">computation</td><td class="snns plane cyan">extended computation</td><td class="snns file cyan">xprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )</td><td class="snnn file cyan">xprs_lift xprs_aaa xprs_cprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">weakly normalizing computation</td><td class="snns file cyan">cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )</td><td class="snnn file cyan">cpe_cpe</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">strongly normalizing computation</td><td class="snns file cyan">csn_vector ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_cpr_vector csn_tstc_vector csn_aaa</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">csn ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_alt ( ? ⊢ ⬊⬊* ? )</td><td class="snnn file cyan">csn_lift csn_cpr csn_lfpr</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">focalized computation</td><td class="snns file cyan">lfprs ( ⦃?⦄ ➡* ⦃?⦄ )</td><td class="snnn file cyan">lfprs_aaa lfprs_cprs lfprs_lfprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-sensitive computation</td><td class="snns file cyan">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file cyan">cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-free computation</td><td class="snns file cyan">ltprs ( ? ➡* ? )</td><td class="snnn file cyan">ltprs_alt ( ? ➡➡* ? )</td><td class="snnn file cyan">ltprs_ldrop ltprs_ltprs</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">tprs ( ? ➡* ?)</td><td class="snnn file cyan">tprs_lift tprs_tprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td><td class="snns file cyan">lsubc ( ? ⊑[?] ? )</td><td class="snnn file cyan">lsubc_ldrop lsubc_ldrops lsubc_lsuba</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">support for abstract computation properties</td><td class="snns file cyan">acp</td><td class="snnn file cyan">acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )</td><td class="snnn file cyan">acp_aaa</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">reducibility</td><td class="snns plane water">extended reduction</td><td class="snns file water">xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )</td><td class="snnn file water">xpr_lift xpr_aaa</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive focalized reduction</td><td class="snns file water">cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">cnfpr_ltpss cfpr_aaa cfpr_cpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free focalized reduction</td><td class="snns file water">lfpr ( ⦃?⦄ ➡ ⦃?⦄ )</td><td class="snnn file water">lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )</td><td class="snnn file water">lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr</td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">fpr_cpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive normal forms</td><td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td><td class="snnn file water">cnf_lift cnf_cif</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reduction</td><td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file water">cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reducible forms</td><td class="snns file water">crf ( ? ⊢ 𝐑⦃?⦄ )</td><td class="snnn file water">crf_append</td><td class="snnn file water">cif ( ? ⊢ 𝐈⦃?⦄ )</td><td class="snnn file water">cif_append</td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free normal forms</td><td class="snns file water">thnf ( 𝐇𝐍⦃?⦄ )</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free reduction</td><td class="snns file water">ltpr ( ? ➡ ? )</td><td class="snnn file water">ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">tpr ( ? ➡ ? )</td><td class="snnn file water">tpr_lift tpr_tpss tpr_delift tpr_tpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">unwind</td><td class="snns plane green"/><td class="snns file green"/><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">local env. ref. for stratified static type assignment</td><td class="snns file grass">lsubss ( ? ⁝⊑ ? )</td><td class="snnn file grass">lsubss_ldrop lsubss_ssta lsubss_lsubss</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">stratified static type assignment</td><td class="snns file grass">ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )</td><td class="snnn file grass">ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ⁝⊑ ? )</td><td class="snnn file grass">lsuba_ldrop lsuba_aaa lsuba_lsuba</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⊢ ? ⁝ ? )</td><td class="snnn file grass">aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass">sd</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">basic local env. thinning</td><td class="snns file yellow">thin ( ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">thin_ldrop thin_delift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">inverse basic term relocation</td><td class="snns file yellow">delift ( ? ⊢ ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift delift_tpss delift_ltpss delift_delift</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss_sn ( ? ⊢ ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">ltpss_dx ( ? ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⊢ ? ▶*[?,?] ? )</td><td class="snnn file yellow">tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop ldrops_ldrops</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift lifts_lifts</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td><td class="snnn file yellow">gr2_gr2</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">tps ( ? ⊢ ? ▶[?,?] ? )</td><td class="snnn file orange">tps_lift tps_tps</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">local env. ref. for substitution</td><td class="snns file orange">lsubs ( ? ≼[?,?] ? )</td><td class="snnn file orange">(lsubs_lsubs)</td><td class="snnn file orange">lsubs_sfr ( ≽[?,?] ? )</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">same head term form</td><td class="snns file red">tshf ( ? ≈ ? )</td><td class="snnn file red">(tshf_tshf)</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc tstc_vector</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @@ ? )</td><td class="snnn file red">cl_weight ( #{?,?} )</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( #{?} )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="snnn file red">lenv_append ( ? @@ ? )</td><td class="ssnn file red">lenv_px lenv_px_bi</td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( #{?} )</td><td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td><td class="snnn file red">term_vector</td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
 
    <div class="head2">Physical Structure of the Specification</div>
    <div class="text">The source files are grouped in directories,
          one for each component.
    </div>
-   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-10-13T23:29:26+02:00</div>
+   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-10-15T17:11:10+02:00</div>
 </body>
 </html>

diff --git a/helm/www/lambda_delta/bin/xhtbl/matrix.ml b/helm/www/lambda_delta/bin/xhtbl/matrix.ml
index 9b3bb94437640ec5af9cdbb9122053565c5f0535..4769a54574886ab91c35ba3d0db2aaf558ceef42 100644 (file)
--- a/helm/www/lambda_delta/bin/xhtbl/matrix.ml
+++ b/helm/www/lambda_delta/bin/xhtbl/matrix.ml
@@ -3,9 +3,9 @@ module A = Array
 module T = Table
 
 type cell = {
-   ck: string;   (* contents *)
-   cc: T.css;    (* css classes *)
-   cb: T.border; (* border *)
+   ck: string list; (* contents *)
+   cc: T.css;       (* css classes *)
+   cb: T.border;    (* border *)
 }
 
 type matrix = {
@@ -15,7 +15,7 @@ type matrix = {
 }
 
 let empty = {
-   ck = ""; cc = []; cb = T.border false;
+   ck = []; cc = []; cb = T.border false;
 }
 
 let make ts = {
@@ -23,8 +23,8 @@ let make ts = {
    m = A.make_matrix ts.T.rf ts.T.cf empty;
 }
 
-let set_key m y x k = 
-   m.m.(y).(x) <- {m.m.(y).(x) with ck = k}
+let set_key m y x kl = 
+   m.m.(y).(x) <- {m.m.(y).(x) with ck = kl}
 
 let set_css m y x c = 
    m.m.(y).(x) <- {m.m.(y).(x) with cc = c @ m.m.(y).(x).cc}

diff --git a/helm/www/lambda_delta/bin/xhtbl/pass2.ml b/helm/www/lambda_delta/bin/xhtbl/pass2.ml
index 8ec358123a1b0fea100e3f99d32aaf19ee109074..68cc7ba9990d35e045cb6a3ea0c174fb7e3620cb 100644 (file)
--- a/helm/www/lambda_delta/bin/xhtbl/pass2.ml
+++ b/helm/www/lambda_delta/bin/xhtbl/pass2.ml
@@ -47,8 +47,8 @@ let place b sts tts =
       {sts with T.y = sts.T.y + tts.T.rf}
 
 let set_key st t = match t.T.te with
-   | T.Key (T.Text s) -> M.set_key st.tm t.T.ts.T.y t.T.ts.T.x s  
-   | _                -> ()
+   | T.Key (T.Text sl) -> M.set_key st.tm t.T.ts.T.y t.T.ts.T.x sl  
+   | _                 -> ()
 
 let set_css st t =
    let rec aux y x =

diff --git a/helm/www/lambda_delta/bin/xhtbl/table.ml b/helm/www/lambda_delta/bin/xhtbl/table.ml
index a7fdf19fab1a4a318ee0155d066c6f6c9be26148..e363cd4347b18864ae9b1e0405cd20c4353782e1 100644 (file)
--- a/helm/www/lambda_delta/bin/xhtbl/table.ml
+++ b/helm/www/lambda_delta/bin/xhtbl/table.ml
@@ -17,7 +17,7 @@ type border = {
    w: bool; (* west *)
 }
 
-type key = Text of string
+type key = Text of string list
          | Glue of int option
 
 type table = {

diff --git a/helm/www/lambda_delta/bin/xhtbl/textLexer.mll b/helm/www/lambda_delta/bin/xhtbl/textLexer.mll
index 2ed6742c954bfbf70a1903cbda4e59b148cc54f5..7557e7bb80f5ee317f34a18620fabc67b19bb697 100644 (file)
--- a/helm/www/lambda_delta/bin/xhtbl/textLexer.mll
+++ b/helm/www/lambda_delta/bin/xhtbl/textLexer.mll
@@ -22,6 +22,7 @@ rule token = parse
    | "["      { out "["; TP.OB                  }
    | "]"      { out "]"; TP.CB                  }   
    | "*"      { out "*"; TP.SR                  }
+   | "+"      { out "+"; TP.PS                  }
    | "name"   { out "name"; TP.NAME             }   
    | "table"  { out "table"; TP.TABLE           }
    | "class"  { out "class"; TP.CSS             }

diff --git a/helm/www/lambda_delta/bin/xhtbl/textParser.mly b/helm/www/lambda_delta/bin/xhtbl/textParser.mly
index 6be4398132159bd77317f19b76245c172239ebec..333d3421f2fa27a3f0c89db7f395266ebe793ee0 100644 (file)
--- a/helm/www/lambda_delta/bin/xhtbl/textParser.mly
+++ b/helm/www/lambda_delta/bin/xhtbl/textParser.mly
@@ -15,17 +15,25 @@ let mk_atom s rs =
 
 %token <int> NUM
 %token <string> TEXT 
-%token NAME TABLE CSS SR OC CC OB CB EOF
+%token NAME TABLE CSS SR OC CC OB CB PS EOF
 
 %start script
 %type <(string * Table.table * Css.atoms) list> script
 
 %%
 
+text:
+   | TEXT { $1 }
+
+texts:
+  | text          { [$1]     }
+  | text PS texts { $1 :: $3 }
+;
+
 key:
-   | TEXT { T.Text $1        }
-   | SR   { T.Glue None      }
-   | NUM  { T.Glue (Some $1) }
+   | texts { T.Text $1        }
+   | SR    { T.Glue None      }
+   | NUM   { T.Glue (Some $1) }
 ;
 
 css:

diff --git a/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml b/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml
index 969713aacd934e4d5ec8885e55d045001730c01a..54995e96bb967591d04b536907bde5322e093955 100644 (file)
--- a/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml
+++ b/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml
@@ -1,3 +1,4 @@
+module L = List
 module P = Printf
 module S = String
 
@@ -41,7 +42,9 @@ let css tc =
    P.sprintf "\"%s\"" (S.concat " " tc)
 
 let key = function
-   | T.Text s        -> P.sprintf "\"%s\"" s
+   | T.Text sl       ->
+      let map s = P.sprintf "\"%s\"" s in
+      S.concat " + " (L.map map sl)
    | T.Glue None     -> "*"
    | T.Glue (Some i) -> P.sprintf "%u" i
 

diff --git a/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml
index 17f24671c376af30edcbc7591bf2e48f89dd274a..3583c2f7536e95d045a4dd0776bbf81d4169b8c2 100644 (file)
--- a/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml
+++ b/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml
@@ -23,7 +23,7 @@ let border cell =
    str :: cell.M.cc
 
 let key cell =
-   if cell.M.ck = "" then "<br/>" else cell.M.ck
+   if cell.M.ck = [] then "<br/>" else S.concat " " cell.M.ck
 
 let ind i = S.make (2 * i) ' '
 

diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl
index 40c29fa13d47b5b432575771b3b568164792a524..d92b37403e0a23ec7db6f78759b04dc12ab680bc 100644 (file)
--- a/helm/www/lambda_delta/web/home/basic_2_src.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl
@@ -40,24 +40,30 @@ table {
         ]
 *)
         [ { "stratified native validity" * } {
-             [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" "snv_aaa" * ]
+             [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" * ]
           }
         ]
      }
    ]
    class "blue"
    [ { "equivalence" * } {
+        [ { "focalized equivalence" * } {
+             [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
+          }
+        ]
         [ { "context-sensitive equivalence" * } {
-             [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" "lfpcs_lfprs" "lfpcs_lfpcs" * ]
-             [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss" "cpcs_delift" "cpcs_aaa" "cpcs_ltpr" "cpcs_cprs" "cpcs_cpcs" * ]
+             [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ]
           }
         ]
      }
    ]
    class "sky"
    [ { "conversion" * } {
-        [ { "context-sensitive conversion" * } {
+        [ { "focalized conversion" * } {
              [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]        
+          }
+        ]
+        [ { "context-sensitive conversion" * } {
              [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
           }
         ]
@@ -66,7 +72,7 @@ table {
    class "cyan"
    [ { "computation" * } {
         [ { "extended computation" * } {
-             [ "xprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )" "xprs_lift" "xprs_aaa" "xprs_cprs" * ]
+             [ "xprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )" "xprs_lift" + "xprs_aaa" + "xprs_cprs" * ]
           }
         ]
         [ { "weakly normalizing computation" * } {
@@ -74,22 +80,25 @@ table {
           }
         ]
         [ { "strongly normalizing computation" * } {
-             [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ]
-             [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" "csn_cpr" "csn_lfpr" * ]
+             [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" + "csn_tstc_vector" + "csn_aaa" * ]
+             [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ]
+          }
+        ]
+        [ { "focalized computation" * } {
+             [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_cprs" + "lfprs_lfprs" * ]
           }
         ]
         [ { "context-sensitive computation" * } {
-             [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" "lfprs_cprs" "lfprs_lfprs" * ]
-             [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_delift" "cprs_aaa" "cprs_ltpr" "cprs_lfpr" "cprs_cprs" "cprs_lfprs" "cprs_tstc" "cprs_tstc_vector" * ]
+             [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
           }
         ]
         [ { "context-free computation" * } {
-             [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" "ltprs_ltprs" * ]
-             [ "tprs ( ? ➡* ?)" "tprs_lift" "tprs_tprs" * ]
+             [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" + "ltprs_ltprs" * ]
+             [ "tprs ( ? ➡* ?)" "tprs_lift" + "tprs_tprs" * ]
           }
         ]
         [ { "local env. ref. for abstract candidates of reducibility" * } {
-             [ "lsubc ( ? ⊑[?] ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ]
+             [ "lsubc ( ? ⊑[?] ? )" "lsubc_ldrop" + "lsubc_ldrops" + "lsubc_lsuba" * ]
           }
         ]
         [ { "support for abstract computation properties" * } {
@@ -101,24 +110,24 @@ table {
    class "water"
    [ { "reducibility" * } {
         [ { "extended reduction" * } {
-             [ "xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )" "xpr_lift" "xpr_aaa" * ]
+             [ "xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )" "xpr_lift" + "xpr_aaa" * ]
           }
         ]
         [ { "context-sensitive focalized reduction" * } {
-             [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" "cfpr_aaa" "cfpr_cpr" * ]
+             [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" * ]
           }
         ]
         [ { "context-free focalized reduction" * } {
-             [ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_aaa" "lfpr_cpr" "lfpr_fpr" "lfpr_lfpr" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" * ]
+             [ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" "lfpr_aaa" + "lfpr_cpr" + "lfpr_fpr" + "lfpr_lfpr" * ]
              [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" * ]
           }
         ]
         [ { "context-sensitive normal forms" * } {
-             [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" "cnf_cif" * ]
+             [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
           }
         ]       
         [ { "context-sensitive reduction" * } {
-             [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_tpss" "cpr_ltpss" "cpr_delift" "cpr_aaa" "cpr_ltpr" "cpr_cpr" * ]
+             [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ]
           }
         ]
         [ { "context-sensitive reducible forms" * } {
@@ -130,8 +139,8 @@ table {
           }
         ]
         [ { "context-free reduction" * } {
-             [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" "ltpr_ltpss_dx" "ltpr_ltpss_sn" "ltpr_aaa" "ltpr_ltpr" * ]
-             [ "tpr ( ? ➡ ? )"  "tpr_lift" "tpr_tpss" "tpr_delift" "tpr_tpr" * ]
+             [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
+             [ "tpr ( ? ➡ ? )"  "tpr_lift" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
           }
         ]
      }
@@ -153,19 +162,19 @@ table {
    class "grass"
    [ { "static typing" * } {
         [ { "local env. ref. for stratified static type assignment" * } {
-             [ "lsubss ( ? ⁝⊑ ? )" "lsubss_ldrop" "lsubss_ssta" "lsubss_lsubss" * ]
+             [ "lsubss ( ? ⁝⊑ ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
           }
         ]
         [ { "stratified static type assignment" * } {
-             [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" "ssta_ltpss_dx" "ssta_ltpss_sn" "ssta_aaa" "ssta_ssta" * ]
+             [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ]
           }
         ]
         [ { "local env. ref. for atomic arity assignment" * } {
-             [ "lsuba ( ? ⁝⊑ ? )" "lsuba_ldrop" "lsuba_aaa" "lsuba_lsuba" * ]
+             [ "lsuba ( ? ⁝⊑ ? )" "lsuba_ldrop" + "lsuba_aaa" + "lsuba_lsuba" * ]
           }
         ]
         [ { "atomic arity assignment" * } {
-             [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss_dx" "aaa_ltpss_sn" "aaa_aaa" * ]
+             [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_ltpss_dx" + "aaa_ltpss_sn" + "aaa_aaa" * ]
           }
         ]
         [ { "parameters" * } {
@@ -177,26 +186,26 @@ table {
    class "yellow"
    [ { "unfold" * } {
         [ { "basic local env. thinning" * } {
-             [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" "thin_delift" * ]
+             [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ]
           }
         ]        
         [ { "inverse basic term relocation" * } {
-             [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" "delift_tpss" "delift_ltpss" "delift_delift" * ]
+             [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ]
           }
         ]
         [ { "partial unfold" * } {
-             [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_ldrop" "ltpss_sn_tps" "ltpss_sn_tpss" "ltpss_sn_ltpss_sn" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" * ]
-             [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" "ltpss_dx_tps" "ltpss_dx_tpss" "ltpss_dx_ltpss_dx" * ]
+             [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ]
+             [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ]
              [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
           }
         ]
         [ { "generic local env. slicing" * } { 
-             [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ]
+             [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
           }
         ]
         [ { "generic term relocation" * } {
              [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
-             [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ] 
+             [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] 
           }
         ]
         [ { "support for generic relocation" * } { 
@@ -208,7 +217,7 @@ table {
    class "orange"   
    [ { "substitution" * } { 
         [ { "parallel substitution" * } {
-             [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" "tps_tps" * ]
+             [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ]
           }
         ]
         [ { "global env. slicing" * } {
@@ -216,7 +225,7 @@ table {
           }
         ]
         [ { "basic local env. slicing" * } {
-             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" "ldrop_lpx" "ldrop_sfr" "ldrop_ldrop" * ]
+             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_sfr" + "ldrop_ldrop" * ]
           }
         ]
         [ { "local env. ref. for substitution" * } {
@@ -237,7 +246,7 @@ table {
           }
         ]
         [ { "same top term constructor" * } {
-             [ "tstc ( ? ≃ ? )" "tstc_tstc" "tstc_vector" * ]
+             [ "tstc ( ? ≃ ? )" "tstc_tstc" + "tstc_vector" * ]
           }
         ]
         [ { "closures" * } {
@@ -246,7 +255,7 @@ table {
         ]
         [ { "internal syntax" * } {
              [ "genv" * ]
-             [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" "lenv_px_bi" * ]
+             [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_bi" * ]
              [ "term" "term_weight ( #{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
              [ "item" * ]
           }