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