helm/style/params.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  28                               xmlns:m="http://www.w3.org/1998/Math/MathML">
  29
  30 <!--***********************************************************************-->
  31 <!-- auxiliary functions                                                   -->
  32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
  33 <!--***********************************************************************-->
  34
  35 <!--***********************************************************************-->
  36 <!-- get the name from a URI                                               -->
  37 <!--***********************************************************************-->
  38
  39 <!-- CSC: PROBLEMA: URI CHE NON CONTENGONO / ED INIZIANO CON cic: -->
  40 <xsl:template name="name_of_uri">
  41  <xsl:param name="uri" select="&quot;&quot;"/>
  42  <xsl:param name="extension" select="'.con'"/>
  43  <xsl:variable name="suffix" select="substring-after($uri, &quot;/&quot;)"/>
  44  <xsl:choose>
  45   <xsl:when test="$suffix = &quot;&quot;">
  46    <!-- CSC: PROBLEMA: .con PUO' APPARIRE ALL'INTERNO DELLE URI ===>
  47      SCRIVERE UNA FUNZIONE RICORSIVA CHE RISOLVA -->
  48    <xsl:value-of select="substring-before($uri,$extension)"/>
  49   </xsl:when>
  50   <xsl:otherwise>
  51    <xsl:call-template name="name_of_uri">
  52     <xsl:with-param name="uri" select="$suffix"/>
  53     <xsl:with-param name="extension" select="$extension"/>
  54    </xsl:call-template>
  55   </xsl:otherwise>
  56  </xsl:choose>
  57 </xsl:template>
  58
  59 <!--***********************************************************************-->
  60 <!-- erase common prefix from two uris                                     -->
  61 <!--***********************************************************************-->
  62
  63 <xsl:template name="common_prefix">
  64  <xsl:param name="first_uri" select="&quot;&quot;"/>
  65  <xsl:param name="second_uri" select="&quot;&quot;"/>
  66  <xsl:choose>
  67   <xsl:when test="(substring-before($first_uri,&quot;/&quot;) =
  68                 substring-before($second_uri,&quot;/&quot;) and
  69                 substring-after($second_uri,&quot;/&quot;) != &quot;&quot;)">
  70    <xsl:call-template name="common_prefix">
  71     <xsl:with-param
  72         name="first_uri" select="substring-after($first_uri,&quot;/&quot;)"/>
  73     <xsl:with-param
  74         name="second_uri" select="substring-after($second_uri,&quot;/&quot;)"/>    </xsl:call-template>
  75   </xsl:when>
  76   <xsl:otherwise>
  77    <xsl:call-template name="slash_counting">
  78     <xsl:with-param name="uri" select="$second_uri"/>
  79     <xsl:with-param name="counter" select="0"/>
  80    </xsl:call-template>
  81   </xsl:otherwise>
  82  </xsl:choose>
  83 </xsl:template>
  84
  85 <xsl:template name="slash_counting">
  86  <xsl:param name="uri" select="&quot;&quot;"/>
  87  <xsl:param name="counter" select="0"/>
  88  <xsl:choose>
  89   <xsl:when test="(substring-after($uri,&quot;/&quot;) != &quot;&quot;)">
  90    <xsl:call-template name="slash_counting">
  91     <xsl:with-param
  92         name="uri" select="substring-after($uri,&quot;/&quot;)"/>
  93     <xsl:with-param
  94         name="counter" select="$counter +1"/>
  95    </xsl:call-template>
  96   </xsl:when>
  97   <xsl:otherwise>
  98    <xsl:value-of select="$counter"/>
  99   </xsl:otherwise>
 100  </xsl:choose>
 101 </xsl:template>
 102
 103 <!-- path gives the path of a uri, up to the final name -->
 104 <xsl:template name="path">
 105  <xsl:param name="uri" select="&quot;&quot;"/>
 106  <xsl:param name="current_path" select="&quot;&quot;"/>
 107  <xsl:choose>
 108   <xsl:when test="(substring-after($uri,&quot;/&quot;) != &quot;&quot;)">
 109    <xsl:call-template name="path">
 110     <xsl:with-param
 111         name="uri" select="substring-after($uri,&quot;/&quot;)"/>
 112     <xsl:with-param
 113         name="current_path" select="concat($current_path,substring-before($uri,&quot;/&quot;),'/')"/>
 114    </xsl:call-template>
 115   </xsl:when>
 116   <xsl:otherwise>
 117    <xsl:value-of select="$current_path"/>
 118   </xsl:otherwise>
 119  </xsl:choose>
 120 </xsl:template>
 121
 122 <xsl:template name="blank_counting">
 123  <xsl:param name="string" select="&quot;&quot;"/>
 124  <xsl:param name="counter" select="0"/>
 125  <xsl:choose>
 126   <xsl:when test="(substring-after($string,&quot; &quot;) != &quot;&quot;)">
 127    <xsl:call-template name="blank_counting">
 128     <xsl:with-param
 129         name="string" select="substring-after($string,&quot; &quot;)"/>
 130     <xsl:with-param
 131         name="counter" select="$counter +1"/>
 132    </xsl:call-template>
 133   </xsl:when>
 134   <xsl:otherwise>
 135    <xsl:value-of select="$counter + 1"/>
 136   </xsl:otherwise>
 137  </xsl:choose>
 138 </xsl:template>
 139
 140 <xsl:template name="double_point_counting">
 141  <xsl:param name="string" select="&quot;&quot;"/>
 142  <xsl:param name="counter" select="0"/>
 143  <xsl:choose>
 144   <xsl:when test="(substring-after($string,&quot;:&quot;) != &quot;&quot;)">
 145    <xsl:call-template name="double_point_counting">
 146     <xsl:with-param
 147         name="string" select="substring-after($string,&quot;:&quot;)"/>
 148     <xsl:with-param
 149         name="counter" select="$counter +1"/>
 150    </xsl:call-template>
 151   </xsl:when>
 152   <xsl:otherwise>
 153    <xsl:value-of select="$counter"/>
 154   </xsl:otherwise>
 155  </xsl:choose>
 156 </xsl:template>
 157
 158 <xsl:template name="min">
 159  <xsl:param name="string" select="&quot;&quot;"/>
 160  <xsl:param name="counter" select="0"/>
 161  <xsl:choose>
 162   <xsl:when test="contains($string,concat($counter,&quot;:&quot;))
 163          or (0 > $counter)">
 164   <xsl:value-of select="$counter"/>
 165   </xsl:when>
 166   <xsl:otherwise>
 167    <xsl:call-template name="min">
 168     <xsl:with-param
 169         name="string" select="$string"/>
 170     <xsl:with-param
 171         name="counter" select="$counter -1"/>
 172    </xsl:call-template>
 173   </xsl:otherwise>
 174  </xsl:choose>
 175 </xsl:template>
 176
 177 <xsl:template name="get_no_params">
 178     <xsl:param name="first_uri" select="&quot;&quot;"/>
 179     <xsl:param name="second_uri" select="&quot;&quot;"/>
 180      <xsl:variable name="offset">
 181       <xsl:call-template name="common_prefix">
 182        <xsl:with-param name="first_uri" select="$first_uri"/>
 183        <xsl:with-param name="second_uri" select="$second_uri"/>
 184       </xsl:call-template>
 185      </xsl:variable>
 186      <xsl:choose>
 187       <xsl:when test="$offset > 0">
 188        <xsl:variable name="params">
 189         <xsl:variable name="second_url"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$second_uri"/></xsl:call-template></xsl:variable>
 190         <xsl:value-of
 191             select="document($second_url)/*/@params"/>
 192        </xsl:variable>
 193        <xsl:variable name="minimum">
 194         <xsl:call-template name="min">
 195          <xsl:with-param name="string" select="$params"/>
 196          <xsl:with-param name="counter" select="$offset - 1"/>
 197         </xsl:call-template>
 198        </xsl:variable>
 199        <xsl:choose>
 200         <xsl:when test="0 > $minimum">
 201          0
 202         </xsl:when>
 203         <xsl:otherwise>
 204          <xsl:variable name="relevant_params">
 205           <!-- the blank after : in the next line is essential -->
 206           <xsl:value-of
 207             select="substring-after($params,concat($minimum,&quot;: &quot;))"/>
 208          </xsl:variable>
 209          <xsl:variable name="tokens">
 210           <xsl:call-template name="blank_counting">
 211            <xsl:with-param name="string" select="$relevant_params"/>
 212            <xsl:with-param name="counter" select="0"/>
 213           </xsl:call-template>
 214          </xsl:variable>
 215          <xsl:variable name="separators">
 216           <xsl:call-template name="double_point_counting">
 217            <xsl:with-param name="string" select="$relevant_params"/>
 218            <xsl:with-param name="counter" select="0"/>
 219           </xsl:call-template>
 220          </xsl:variable>
 221          <xsl:value-of select="$tokens - $separators"/>
 222         </xsl:otherwise>
 223        </xsl:choose>
 224       </xsl:when>
 225       <xsl:otherwise>
 226       0
 227       </xsl:otherwise>
 228      </xsl:choose>
 229 </xsl:template>
 230
 231
 232 <!--***********************************************************************-->
 233 <!--  Insert a subscript if there is a number at the end of a ci element   -->
 234 <!--***********************************************************************-->
 235
 236 <xsl:template name="insert_subscript">
 237 <xsl:param name="node_value" select="&quot;&quot;"/>
 238 <xsl:param name="current_pos" select="1"/>
 239 <xsl:param name="start_pos" select="0"/>
 240     <xsl:choose>
 241     <xsl:when test="$current_pos &lt;= string-length(string($node_value))">
 242     <xsl:variable name="current_char"><xsl:value-of select="substring(string($node_value),$current_pos,1)"/></xsl:variable>
 243      <xsl:choose>
 244      <xsl:when test="(string($current_char) != &quot;0&quot;) and (string($current_char) != &quot;1&quot;) and (string($current_char) != &quot;2&quot;) and (string($current_char) != &quot;3&quot;) and (string($current_char) != &quot;4&quot;) and (string($current_char) != &quot;5&quot;) and (string($current_char) != &quot;6&quot;) and (string($current_char) !=  &quot;7&quot;) and (string($current_char) != &quot;8&quot;) and (string($current_char) != &quot;9&quot;)">
 245       <xsl:choose>
 246       <xsl:when test="$start_pos != 0">
 247        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="0"/></xsl:call-template>
 248       </xsl:when>
 249       <xsl:otherwise>
 250        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="$start_pos"/></xsl:call-template>
 251       </xsl:otherwise>
 252       </xsl:choose>
 253      </xsl:when>
 254      <xsl:otherwise>
 255       <xsl:choose>
 256       <xsl:when test="$start_pos = 0">
 257        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="$current_pos"/></xsl:call-template>
 258       </xsl:when>
 259       <xsl:otherwise>
 260        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="$start_pos"/></xsl:call-template>
 261       </xsl:otherwise>
 262       </xsl:choose>
 263      </xsl:otherwise>
 264      </xsl:choose>
 265     </xsl:when>
 266     <xsl:otherwise>
 267      <xsl:choose>
 268      <xsl:when test="$start_pos != 0">
 269       <m:msub>
 270        <m:mi><xsl:value-of select="substring(string($node_value),1,$start_pos -1)"/></m:mi>
 271        <m:mn><xsl:value-of select="substring(string($node_value),$start_pos)"/></m:mn>
 272        </m:msub>
 273      </xsl:when>
 274      <xsl:otherwise>
 275       <xsl:value-of select="$node_value"/>
 276      </xsl:otherwise>
 277      </xsl:choose>
 278     </xsl:otherwise>
 279     </xsl:choose>
 280 </xsl:template>
 281
 282
 283 <!--*******************************************-->
 284 <!--    ABSTRACTING PARAMETERS AND COUNTING    -->
 285 <!--*******************************************-->
 286 <!-- Si dimentica i CAST dei termini che astrae. Nel caso dell'astrazione -->
 287 <!-- dei lambda dei pattern del CASE, qualora i lambda non si trovino     -->
 288 <!-- nella forma weak-head, astrae solo i lambda che trova e restituisce  -->
 289 <!-- un corpo depurato da tutti i primi cast che precedono il termine     -->
 290 <!-- restituito.                                                          -->
 291
 292 <xsl:template match="*" mode="abstparams">
 293 <xsl:param name="noparams" select="0"/>
 294 <xsl:param name="target" select="0"/>
 295 <xsl:param name="binder">PROD</xsl:param>
 296     <xsl:choose>
 297     <xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)=&quot;CAST&quot;))">
 298      <xsl:choose>
 299      <xsl:when test="name(.) = string($binder)">
 300       <xsl:choose>
 301        <xsl:when test="$noparams >= count(decl)">
 302         <xsl:for-each select="decl">
 303          <xsl:if test="$target = 0">
 304           <xsl:choose>
 305           <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
 306            <m:ci>
 307             <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
 308            </m:ci>
 309           </xsl:when>
 310           <xsl:otherwise>
 311            <Param name="{@binder}">
 312             <xsl:apply-templates select="*[1]"/>
 313            </Param>
 314           </xsl:otherwise>
 315           </xsl:choose>
 316          </xsl:if>
 317         </xsl:for-each>
 318         <xsl:apply-templates select="target/*[1]" mode="abstparams">
 319          <xsl:with-param name="noparams" select="$noparams - count(decl)"/>
 320          <xsl:with-param name="target" select="$target"/>
 321          <xsl:with-param name="binder" select="$binder"/>
 322         </xsl:apply-templates>
 323        </xsl:when>
 324        <xsl:otherwise>
 325         <xsl:for-each select="decl[$noparams >= position()]">
 326          <xsl:if test="$target = 0">
 327           <xsl:choose>
 328           <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
 329            <m:ci>
 330             <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
 331            </m:ci>
 332           </xsl:when>
 333           <xsl:otherwise>
 334            <Param name="{@binder}">
 335             <xsl:apply-templates select="*[1]"/>
 336            </Param>
 337           </xsl:otherwise>
 338           </xsl:choose>
 339          </xsl:if>
 340         </xsl:for-each>
 341         <xsl:if test="$target = 1">
 342          <xsl:choose>
 343           <xsl:when test="name(.)=&quot;PROD&quot;">
 344            <xsl:apply-templates select="decl[position()=$noparams+1]" mode="prod"/>
 345           </xsl:when>
 346           <xsl:otherwise>
 347            <xsl:apply-templates select="decl[position()=$noparams+1]" mode="lambda_prop"/>
 348           </xsl:otherwise>
 349          </xsl:choose>
 350         </xsl:if>
 351        </xsl:otherwise>
 352       </xsl:choose>
 353      </xsl:when>
 354      <xsl:otherwise>
 355       <xsl:apply-templates select="term/*[1]" mode="abstparams">
 356        <xsl:with-param name="noparams" select="$noparams"/>
 357        <xsl:with-param name="target" select="$target"/>
 358        <xsl:with-param name="binder" select="$binder"/>
 359       </xsl:apply-templates>
 360      </xsl:otherwise>
 361      </xsl:choose>
 362     </xsl:when>
 363     <xsl:otherwise>
 364      <xsl:choose>
 365      <xsl:when test="($target = 1) and ($noparams != 0)">
 366       <m:apply>
 367       <m:csymbol>app</m:csymbol>
 368 <!-- Mancava modalita': sono all'interno di un termine -->
 369       <xsl:apply-templates select="." mode="pure"/>
 370       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
 371       </m:apply>
 372      </xsl:when>
 373      <xsl:otherwise>
 374       <xsl:choose>
 375       <xsl:when test="$noparams != 0">
 376       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
 377       </xsl:when>
 378       <xsl:otherwise>
 379        <xsl:if test="$target = 1">
 380 <!-- Mancava modalita': con target=1 posso provenire sia da un oggetto che da un termine -->
 381         <xsl:choose>
 382         <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
 383          <!-- CSC: era pure, ma deve essere noannot. Giusto, Irene? -->
 384          <xsl:apply-templates select="." mode="noannot"/>
 385         </xsl:when>
 386         <xsl:otherwise>
 387          <xsl:apply-templates select="."/>
 388         </xsl:otherwise>
 389         </xsl:choose>
 390        </xsl:if>
 391       </xsl:otherwise>
 392       </xsl:choose>
 393      </xsl:otherwise>
 394      </xsl:choose>
 395     </xsl:otherwise>
 396     </xsl:choose>
 397 </xsl:template>
 398
 399 <xsl:template name="printparam">
 400 <xsl:param name="noleft" select="0"/>
 401 <xsl:param name="number" select="1"/>
 402     <xsl:if test="$noleft != 0">
 403      <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value">$<xsl:value-of select="$number"/></xsl:with-param></xsl:call-template></m:ci>
 404      <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noleft - 1"/><xsl:with-param name="number" select="$number + 1"/></xsl:call-template>
 405     </xsl:if>
 406 </xsl:template>
 407
 408 <xsl:template match="*" mode="counting">
 409 <xsl:param name="noparams" select="0"/>
 410 <xsl:param name="count" select="0"/>
 411  <xsl:choose>
 412  <xsl:when test="name(.) = &quot;PROD&quot;">
 413   <xsl:apply-templates select="target/*[1]" mode="counting">
 414    <xsl:with-param name="noparams" select="$noparams"/>
 415    <xsl:with-param name="count" select="$count + count(decl)"/>
 416   </xsl:apply-templates>
 417  </xsl:when>
 418  <xsl:when test="name(.) = &quot;CAST&quot;">
 419   <xsl:apply-templates select="term/*[1]" mode="counting">
 420    <xsl:with-param name="noparams" select="$noparams"/>
 421    <xsl:with-param name="count" select="$count"/>
 422   </xsl:apply-templates>
 423  </xsl:when>
 424  <xsl:otherwise>
 425   <xsl:value-of select="$count - $noparams"/>
 426  </xsl:otherwise>
 427  </xsl:choose>
 428 </xsl:template>
 429
 430 </xsl:stylesheet>