helm/style/proofs.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 <!--******************************************************************-->
  28 <!-- Basic Logic                                                      -->
  29 <!-- (completely) Revisited: february 2001, Andrea Asperti            -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
  31 <!--******************************************************************-->
  32
  33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  34                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  35                               xmlns:helm="http://www.cs.unibo.it/helm">
  36
  37 <xsl:include href="logic.xsl"/>
  38 <xsl:include href="inductive.xsl"/>
  39 <xsl:include href="rewrite.xsl"/>
  40 <xsl:include href="diseq.xsl"/>
  41
  42 <!-- ************************* LOGIC *********************************-->
  43
  44 <!-- Proof objects -->
  45
  46 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  47 <xsl:key name="typeid" use="@of" match="TYPE"/>
  48
  49 <!-- These elements do not have inner type -->
  50 <xsl:template match="PROD|SORT|MUTIND|instantiate" mode="noannot">
  51  <xsl:apply-templates select="." mode="pure"/>
  52 </xsl:template>
  53
  54 <!-- Atomic elements that have an inner type iff the expected type -->
  55 <!-- is different from the synthesized type.                       -->
  56 <xsl:template match="REL|VAR|META|CONST|MUTCONSTRUCT" mode="noannot">
  57  <xsl:variable name="id" select="@id"/>
  58  <xsl:variable name="innertype_available">
  59   <xsl:for-each select="$InnerTypes">
  60    <xsl:if test="key('typeid',$id)/*">
  61     <xsl:text>yes</xsl:text>
  62    </xsl:if>
  63   </xsl:for-each>
  64  </xsl:variable>
  65  <xsl:choose>
  66   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
  67    <!--xsl:when test="@sort='Prop'"-->
  68    <m:apply helm:xref="{@id}">
  69     <m:csymbol>proof</m:csymbol>
  70     <xsl:apply-templates mode="proof_transform" select="."/>
  71     <xsl:for-each select="$InnerTypes">
  72      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
  73     </xsl:for-each>
  74    </m:apply>
  75   </xsl:when>
  76   <xsl:otherwise>
  77    <xsl:apply-templates select="." mode="pure"/>
  78   </xsl:otherwise>
  79  </xsl:choose>
  80 </xsl:template>
  81
  82 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
  83
  84 <xsl:template match="LAMBDA" mode="noannot">
  85  <xsl:choose>
  86   <xsl:when test="@sort='Prop'">
  87    <xsl:apply-templates select="*[1]" mode="lambda_prop"/>
  88   </xsl:when>
  89   <xsl:otherwise>
  90    <!-- mode lambda is defined in content.xsl -->
  91    <xsl:apply-templates select="*[1]" mode="lambda"/>
  92   </xsl:otherwise>
  93  </xsl:choose>
  94 </xsl:template>
  95
  96 <xsl:template match="decl" mode="lambda_prop">
  97  <xsl:variable name="id" select="@id"/>
  98  <xsl:variable name="innertype_available">
  99   <xsl:for-each select="$InnerTypes">
 100    <xsl:if test="key('typeid',$id)/*">
 101     <xsl:text>yes</xsl:text>
 102    </xsl:if>
 103   </xsl:for-each>
 104  </xsl:variable>
 105  <xsl:choose>
 106   <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
 107    <m:apply helm:xref="{@id}">
 108     <m:csymbol>proof</m:csymbol>
 109     <m:lambda helm:xref="{@id}">
 110      <m:bvar>
 111       <m:ci>
 112        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
 113       </m:ci>
 114       <m:type>
 115        <xsl:apply-templates select="*[1]" mode="noannot"/>
 116       </m:type>
 117      </m:bvar>
 118      <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
 119     </m:lambda>
 120     <xsl:for-each select="$InnerTypes">
 121      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
 122     </xsl:for-each>
 123    </m:apply>
 124   </xsl:when>
 125   <xsl:otherwise>
 126    <m:lambda helm:xref="{@id}">
 127     <m:bvar>
 128      <m:ci>
 129       <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
 130      </m:ci>
 131      <m:type>
 132       <xsl:apply-templates select="*[1]" mode="noannot"/>
 133      </m:type>
 134     </m:bvar>
 135     <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
 136    </m:lambda>
 137   </xsl:otherwise>
 138  </xsl:choose>
 139 </xsl:template>
 140
 141 <xsl:template match="target" mode="lambda_prop">
 142  <xsl:apply-templates select="*[1]" mode="noannot"/>
 143 </xsl:template>
 144
 145 <!-- LETIN -->
 146
 147 <xsl:template match="LETIN" mode="noannot">
 148  <xsl:choose>
 149   <xsl:when test="@sort='Prop'">
 150    <xsl:apply-templates select="*[1]" mode="letin_prop"/>
 151   </xsl:when>
 152   <xsl:otherwise>
 153    <!-- mode letin is defined in content.xsl -->
 154    <xsl:apply-templates select="*[1]" mode="letin_pure"/>
 155   </xsl:otherwise>
 156  </xsl:choose>
 157 </xsl:template>
 158
 159 <xsl:template match="def" mode="letin_prop">
 160  <xsl:variable name="id" select="@id"/>
 161  <xsl:variable name="innertype_available">
 162   <xsl:for-each select="$InnerTypes">
 163    <xsl:if test="key('typeid',$id)/*">
 164     <xsl:text>yes</xsl:text>
 165    </xsl:if>
 166   </xsl:for-each>
 167  </xsl:variable>
 168  <xsl:choose>
 169   <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
 170    <m:apply helm:xref="{@id}">
 171     <m:csymbol>proof</m:csymbol>
 172     <m:apply helm:xref="{@id}">
 173      <m:csymbol>let_in</m:csymbol>
 174      <m:bvar>
 175       <m:ci>
 176        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
 177       </m:ci>
 178      </m:bvar>
 179      <xsl:apply-templates select="*[1]" mode="noannot"/>
 180      <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
 181     </m:apply>
 182     <xsl:for-each select="$InnerTypes">
 183      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
 184     </xsl:for-each>
 185    </m:apply>
 186   </xsl:when>
 187   <xsl:otherwise>
 188    <m:apply helm:xref="{@id}">
 189     <m:csymbol>let_in</m:csymbol>
 190     <m:bvar>
 191      <m:ci>
 192       <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
 193      </m:ci>
 194     </m:bvar>
 195     <xsl:apply-templates select="*[1]" mode="noannot"/>
 196     <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
 197    </m:apply>
 198   </xsl:otherwise>
 199  </xsl:choose>
 200 </xsl:template>
 201
 202 <xsl:template match="target" mode="letin_prop">
 203  <xsl:apply-templates select="*[1]" mode="noannot"/>
 204 </xsl:template>
 205
 206 <!-- ALL these elements have inner type -->
 207 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
 208  <xsl:variable name="id" select="@id"/>
 209  <xsl:choose>
 210   <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
 211    <m:apply helm:xref="{@id}">
 212     <m:csymbol>proof</m:csymbol>
 213     <xsl:apply-templates mode="proof_transform" select="."/>
 214     <xsl:for-each select="$InnerTypes">
 215      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
 216     </xsl:for-each>
 217    </m:apply>
 218   </xsl:when>
 219   <xsl:otherwise>
 220    <xsl:choose>
 221     <xsl:when test="name()='APPLY'">
 222      <!-- This is the case of an applicative expression wich is not
 223           a proof but could contains proofs...
 224           MODE LETIN OR MODE PURE ??? Big question -->
 225      <xsl:apply-templates select="." mode="pure"/>
 226     </xsl:when>
 227     <xsl:otherwise>
 228      <xsl:apply-templates select="." mode="pure"/>
 229     </xsl:otherwise>
 230    </xsl:choose>
 231   </xsl:otherwise>
 232  </xsl:choose>
 233 </xsl:template>
 234
 235 <xsl:template mode="proof_transform" match="*">
 236  <xsl:choose>
 237   <xsl:when test="name()='APPLY'">
 238    <xsl:variable name="id" select="@id"/>
 239    <xsl:choose>
 240     <xsl:when test="name(*[1])='CONST' or
 241       (name(*[1])='instantiate' and name(*[1]/*[1])='CONST')">
 242      <xsl:apply-templates mode="try_inductive" select="."/>
 243     </xsl:when>
 244     <!-- patch temporanea per la gestione di redex -->
 245     <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2">
 246     <!-- old
 247          and *[2]/@sort='Prop'"> -->
 248      <m:apply helm:xref="{@id}">
 249       <m:csymbol>let_in</m:csymbol>
 250       <m:bvar>
 251        <m:ci>
 252         <xsl:call-template name="insert_subscript">
 253          <xsl:with-param name="node_value">
 254           <xsl:value-of select="*[1]/*[1]/@binder"/>
 255          </xsl:with-param>
 256         </xsl:call-template>
 257        </m:ci>
 258       </m:bvar>
 259       <xsl:apply-templates mode="noannot" select="*[2]"/>
 260       <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
 261      </m:apply>
 262     </xsl:when>
 263     <xsl:otherwise>
 264      <xsl:apply-templates select="." mode="letin"/>
 265     </xsl:otherwise>
 266    </xsl:choose>
 267   </xsl:when>
 268   <xsl:otherwise>
 269    <xsl:apply-templates select="." mode="pure"/>
 270   </xsl:otherwise>
 271  </xsl:choose>
 272 </xsl:template>
 273
 274 <xsl:template name="is_simple">
 275  <xsl:param name="proof" select="/.."/>
 276  <xsl:value-of select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
 277 </xsl:template>
 278
 279 <xsl:template name="generate_side_proof">
 280  <xsl:param name="proof" select="/.."/>
 281  <xsl:param name="show_statement" select="1"/>
 282 <!--
 283  <xsl:variable name="is_simple">
 284   <xsl:call-template name="is_simple">
 285    <xsl:with-param name="proof" select="$proof"/>
 286   </xsl:call-template>
 287  </xsl:variable> -->
 288 <xsl:variable name="is_simple" select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
 289  <xsl:choose>
 290   <xsl:when test="$is_simple">
 291    <xsl:choose>
 292     <xsl:when test="name($proof)='APPLY'">
 293      <xsl:apply-templates select="$proof" mode="letin"/>
 294     </xsl:when>
 295     <xsl:otherwise>
 296      <xsl:apply-templates select="$proof" mode="pure"/>
 297     </xsl:otherwise>
 298    </xsl:choose>
 299   </xsl:when>
 300   <xsl:otherwise>
 301    <xsl:variable name="id" select="@id"/>
 302    <m:apply helm:xref="{@id}">
 303     <xsl:choose>
 304      <xsl:when test="$show_statement = 1">
 305       <m:csymbol>proof</m:csymbol>
 306      </xsl:when>
 307      <xsl:otherwise>
 308       <m:csymbol>side_proof</m:csymbol>
 309      </xsl:otherwise>
 310     </xsl:choose>
 311     <xsl:apply-templates mode="proof_transform" select="$proof"/>
 312     <xsl:for-each select="$InnerTypes">
 313      <xsl:apply-templates mode="pure" select="key('typeid',$proof/@id)/*"/>
 314     </xsl:for-each>
 315    </m:apply>
 316    <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
 317   </xsl:otherwise>
 318  </xsl:choose>
 319 </xsl:template>
 320
 321 <xsl:template match="APPLY" mode="letin">
 322    <xsl:variable name="no_subproofs">
 323     <xsl:variable name="stars">
 324      <xsl:for-each select="*[@sort='Prop']">
 325       <xsl:variable name="id" select="@id"/>
 326       <xsl:variable name="innertype_available">
 327        <xsl:for-each select="$InnerTypes">
 328         <xsl:if test="key('typeid',$id)/*">
 329          <xsl:text>yes</xsl:text>
 330         </xsl:if>
 331        </xsl:for-each>
 332       </xsl:variable>
 333       <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
 334        <!-- We generate one star for each subproof -->
 335        <xsl:text>*</xsl:text>
 336       </xsl:if>
 337      </xsl:for-each>
 338     </xsl:variable>
 339     <xsl:value-of select="string-length($stars)"/>
 340    </xsl:variable>
 341    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
 342    <xsl:choose>
 343     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
 344      <m:apply helm:xref="{@id}">
 345       <m:csymbol>letin1</m:csymbol>
 346       <xsl:for-each select="*[@sort='Prop']">
 347        <xsl:variable name="id" select="@id"/>
 348        <xsl:variable name="innertype_available">
 349         <xsl:for-each select="$InnerTypes">
 350          <xsl:if test="key('typeid',$id)/*">
 351           <xsl:text>yes</xsl:text>
 352          </xsl:if>
 353         </xsl:for-each>
 354        </xsl:variable>
 355        <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
 356         <xsl:apply-templates mode="noannot" select="."/>
 357        </xsl:if>
 358       </xsl:for-each>
 359       <!-- now re-process the application -->
 360       <m:apply helm:xref="{@id}">
 361        <m:csymbol>app</m:csymbol>
 362        <!-- mode previous looks for siblings:
 363             call with the first child -->
 364        <xsl:apply-templates mode="previous" select="*[1]"/>
 365       </m:apply>
 366      </m:apply>
 367     </xsl:when>
 368     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
 369      <m:apply helm:xref="{@id}">
 370       <m:csymbol>letin</m:csymbol>
 371       <!-- first process all subproofs (let-in) -->
 372       <xsl:call-template name="gen_let"/>
 373       <!-- now re-process the application  -->
 374       <m:apply helm:xref="{@id}">
 375        <m:csymbol>app</m:csymbol>
 376        <!-- mode flat looks for siblings: call with the first child -->
 377        <xsl:apply-templates mode="flat" select="*[1]"/>
 378       </m:apply>
 379      </m:apply>
 380     </xsl:when>
 381     <xsl:otherwise>
 382      <xsl:choose>
 383      <xsl:when test="@sort='Prop'">
 384       <m:apply>
 385        <m:csymbol>app</m:csymbol>
 386        <xsl:apply-templates mode="erase" select="*[1]"/>
 387       </m:apply>
 388      </xsl:when>
 389      <xsl:otherwise>
 390       <xsl:apply-templates mode="pure" select="."/>
 391      </xsl:otherwise>
 392      </xsl:choose>
 393     </xsl:otherwise>
 394    </xsl:choose>
 395 </xsl:template>
 396
 397
 398 <xsl:template name="gen_let">
 399  <xsl:param name="init_pos" select="1"/>
 400  <xsl:param name="from" select="0"/>
 401   <xsl:apply-templates mode="gen_let_aux" select="*[position() = ($from+1)]">
 402    <xsl:with-param name="init_pos" select="$init_pos"/>
 403   </xsl:apply-templates>
 404 </xsl:template>
 405
 406 <xsl:template mode="gen_let_aux" match="*">
 407  <xsl:param name="init_pos" select="1"/>
 408  <xsl:variable name="id" select="@id"/>
 409  <xsl:variable name="innertype_available">
 410   <xsl:for-each select="$InnerTypes">
 411    <xsl:if test="key('typeid',$id)/*">
 412     <xsl:text>yes</xsl:text>
 413    </xsl:if>
 414   </xsl:for-each>
 415  </xsl:variable>
 416  <xsl:choose>
 417   <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
 418    <m:apply>
 419     <m:csymbol>let</m:csymbol>
 420     <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
 421     <xsl:apply-templates mode="noannot" select="."/>
 422    </m:apply>
 423    <xsl:if test="following-sibling::*[1]">
 424     <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
 425      <xsl:with-param name="init_pos" select="$init_pos+1"/>
 426     </xsl:apply-templates>
 427    </xsl:if>
 428   </xsl:when>
 429   <xsl:otherwise>
 430    <xsl:if test="following-sibling::*[1]">
 431     <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
 432      <xsl:with-param name="init_pos" select="$init_pos"/>
 433     </xsl:apply-templates>
 434    </xsl:if>
 435   </xsl:otherwise>
 436  </xsl:choose>
 437 </xsl:template>
 438
 439 <!-- questa vecchia versione (di Claudio??) sembra bacata come un melone.
 440
 441 <xsl:template name="gen_let">
 442  <xsl:param name="init_pos" select="0"/>
 443  <xsl:param name="from" select="0"/>
 444       <xsl:for-each select="*[position()>$from and @sort='Prop']">
 445        <xsl:variable name="id" select="@id"/>
 446        <xsl:variable name="innertype_available">
 447         <xsl:for-each select="$InnerTypes">
 448          <xsl:if test="key('typeid',$id)/*">
 449           <xsl:text>yes</xsl:text>
 450          </xsl:if>
 451         </xsl:for-each>
 452        </xsl:variable>
 453        <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
 454         <m:apply>
 455          <m:csymbol>let</m:csymbol>
 456          <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position()+$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
 457          <xsl:apply-templates mode="noannot" select="."/>
 458         </m:apply>
 459        </xsl:if>
 460       </xsl:for-each>
 461 </xsl:template> -->
 462
 463 <xsl:template match="*" mode="erase">
 464   <xsl:choose>
 465    <xsl:when test="@sort='Prop'
 466                    or name()='instantiate' or $naturalLanguage='no'">
 467     <xsl:apply-templates mode="pure" select="."/>
 468    </xsl:when>
 469    <xsl:otherwise>
 470     <m:ci>.</m:ci>
 471    </xsl:otherwise>
 472    </xsl:choose>
 473  <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
 474 </xsl:template>
 475
 476 <xsl:template match="*" mode="previous">
 477  <xsl:variable name="innertype_available">
 478   <xsl:variable name="id" select="@id"/>
 479   <xsl:for-each select="$InnerTypes">
 480    <xsl:if test="key('typeid',$id)/*">
 481     <xsl:text>yes</xsl:text>
 482    </xsl:if>
 483   </xsl:for-each>
 484  </xsl:variable>
 485  <xsl:choose>
 486   <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
 487    <m:ci>previous</m:ci>
 488   </xsl:when>
 489   <xsl:otherwise>
 490    <!-- forse bisognerebbe trattare solo l'elemento di testa -->
 491    <xsl:choose>
 492    <xsl:when test="@sort='Prop'
 493                    or name()='instantiate' or $naturalLanguage='no'">
 494     <xsl:apply-templates mode="pure" select="."/>
 495    </xsl:when>
 496    <xsl:otherwise>
 497     <m:ci>.</m:ci>
 498    </xsl:otherwise>
 499    </xsl:choose>
 500    <!-- <xsl:apply-templates select="." mode="pure"/> -->
 501   </xsl:otherwise>
 502  </xsl:choose>
 503  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 504 </xsl:template>
 505
 506 <xsl:template match="*" mode="flat">
 507  <xsl:param name="n" select="1"/>
 508  <xsl:variable name="id" select="@id"/>
 509  <xsl:variable name="innertype_available">
 510   <xsl:for-each select="$InnerTypes">
 511    <xsl:if test="key('typeid',$id)/*">
 512     <xsl:text>yes</xsl:text>
 513    </xsl:if>
 514   </xsl:for-each>
 515  </xsl:variable>
 516  <xsl:choose>
 517   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
 518    <m:ci>
 519     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
 520    </m:ci>
 521    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 522     <xsl:with-param name="n" select="$n+1"/>
 523    </xsl:apply-templates>
 524   </xsl:when>
 525   <xsl:otherwise>
 526    <xsl:choose>
 527     <xsl:when test="name()='REL' or name()='instantiate' or @sort='Prop' or $naturalLanguage='no'">
 528      <xsl:apply-templates mode="pure" select="."/>
 529     </xsl:when>
 530     <xsl:otherwise>
 531      <m:ci>.</m:ci>
 532     </xsl:otherwise>
 533    </xsl:choose>
 534    <!-- <xsl:apply-templates mode="pure" select="."/> -->
 535    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 536     <xsl:with-param name="n" select="$n"/>
 537    </xsl:apply-templates>
 538   </xsl:otherwise>
 539  </xsl:choose>
 540 </xsl:template>
 541
 542 <!-- Auxiliary functions -->
 543 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
 544 <!-- can replace the next template                                    -->
 545 <xsl:template name="get_name">
 546  <xsl:param name="uri" select="''"/>
 547  <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
 548  <xsl:choose>
 549   <xsl:when test="contains($sub_after,'/')">
 550    <xsl:call-template name="get_name">
 551     <xsl:with-param name="uri" select="$sub_after"/>
 552    </xsl:call-template>
 553   </xsl:when>
 554   <xsl:otherwise>
 555    <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
 556   </xsl:otherwise>
 557  </xsl:choose>
 558 </xsl:template>
 559
 560
 561 </xsl:stylesheet>