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'">
 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="proof_transform" select="*[1]/target/*[1]"/>
 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
 397 <xsl:template name="gen_let">
 398  <xsl:param name="init_pos" select="1"/>
 399  <xsl:param name="from" select="0"/>
 400   <xsl:apply-templates mode="gen_let_aux" select="*[position() = ($from+1)]">
 401    <xsl:with-param name="init_pos" select="$init_pos"/>
 402   </xsl:apply-templates>
 403 </xsl:template>
 404
 405 <xsl:template mode="gen_let_aux" match="*">
 406  <xsl:param name="init_pos" select="1"/>
 407  <xsl:variable name="id" select="@id"/>
 408  <xsl:variable name="innertype_available">
 409   <xsl:for-each select="$InnerTypes">
 410    <xsl:if test="key('typeid',$id)/*">
 411     <xsl:text>yes</xsl:text>
 412    </xsl:if>
 413   </xsl:for-each>
 414  </xsl:variable>
 415  <xsl:choose>
 416   <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'))">
 417    <m:apply>
 418     <m:csymbol>let</m:csymbol>
 419     <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>
 420     <xsl:apply-templates mode="noannot" select="."/>
 421    </m:apply>
 422    <xsl:if test="following-sibling::*[1]">
 423     <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
 424      <xsl:with-param name="init_pos" select="$init_pos+1"/>
 425     </xsl:apply-templates>
 426    </xsl:if>
 427   </xsl:when>
 428   <xsl:otherwise>
 429    <xsl:if test="following-sibling::*[1]">
 430     <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
 431      <xsl:with-param name="init_pos" select="$init_pos"/>
 432     </xsl:apply-templates>
 433    </xsl:if>
 434   </xsl:otherwise>
 435  </xsl:choose>
 436 </xsl:template>
 437
 438 <!-- questa vecchia versione (di Claudio??) sembra bacata come un melone.
 439
 440 <xsl:template name="gen_let">
 441  <xsl:param name="init_pos" select="0"/>
 442  <xsl:param name="from" select="0"/>
 443       <xsl:for-each select="*[position()>$from and @sort='Prop']">
 444        <xsl:variable name="id" select="@id"/>
 445        <xsl:variable name="innertype_available">
 446         <xsl:for-each select="$InnerTypes">
 447          <xsl:if test="key('typeid',$id)/*">
 448           <xsl:text>yes</xsl:text>
 449          </xsl:if>
 450         </xsl:for-each>
 451        </xsl:variable>
 452        <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')">
 453         <m:apply>
 454          <m:csymbol>let</m:csymbol>
 455          <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>
 456          <xsl:apply-templates mode="noannot" select="."/>
 457         </m:apply>
 458        </xsl:if>
 459       </xsl:for-each>
 460 </xsl:template> -->
 461
 462 <xsl:template match="*" mode="erase">
 463   <xsl:choose>
 464    <xsl:when test="@sort='Prop'
 465                    or name()='instantiate' or $naturalLanguage='no'">
 466     <xsl:apply-templates mode="pure" select="."/>
 467    </xsl:when>
 468    <xsl:otherwise>
 469     <m:ci>.</m:ci>
 470    </xsl:otherwise>
 471    </xsl:choose>
 472  <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
 473 </xsl:template>
 474
 475 <xsl:template match="*" mode="previous">
 476  <xsl:variable name="innertype_available">
 477   <xsl:variable name="id" select="@id"/>
 478   <xsl:for-each select="$InnerTypes">
 479    <xsl:if test="key('typeid',$id)/*">
 480     <xsl:text>yes</xsl:text>
 481    </xsl:if>
 482   </xsl:for-each>
 483  </xsl:variable>
 484  <xsl:choose>
 485   <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'))">
 486    <m:ci>previous</m:ci>
 487   </xsl:when>
 488   <xsl:otherwise>
 489    <!-- forse bisognerebbe trattare solo l'elemento di testa -->
 490    <xsl:choose>
 491    <xsl:when test="@sort='Prop'
 492                    or name()='instantiate' or $naturalLanguage='no'">
 493     <xsl:apply-templates mode="pure" select="."/>
 494    </xsl:when>
 495    <xsl:otherwise>
 496     <m:ci>.</m:ci>
 497    </xsl:otherwise>
 498    </xsl:choose>
 499    <!-- <xsl:apply-templates select="." mode="pure"/> -->
 500   </xsl:otherwise>
 501  </xsl:choose>
 502  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 503 </xsl:template>
 504
 505 <xsl:template match="*" mode="flat">
 506  <xsl:param name="n" select="1"/>
 507  <xsl:variable name="id" select="@id"/>
 508  <xsl:variable name="innertype_available">
 509   <xsl:for-each select="$InnerTypes">
 510    <xsl:if test="key('typeid',$id)/*">
 511     <xsl:text>yes</xsl:text>
 512    </xsl:if>
 513   </xsl:for-each>
 514  </xsl:variable>
 515  <xsl:choose>
 516   <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'))">
 517    <m:ci>
 518     <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>
 519    </m:ci>
 520    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 521     <xsl:with-param name="n" select="$n+1"/>
 522    </xsl:apply-templates>
 523   </xsl:when>
 524   <xsl:otherwise>
 525    <xsl:choose>
 526     <xsl:when test="name()='REL' or name()='instantiate' or @sort='Prop' or $naturalLanguage='no'">
 527      <xsl:apply-templates mode="pure" select="."/>
 528     </xsl:when>
 529     <xsl:otherwise>
 530      <m:ci>.</m:ci>
 531     </xsl:otherwise>
 532    </xsl:choose>
 533    <!-- <xsl:apply-templates mode="pure" select="."/> -->
 534    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 535     <xsl:with-param name="n" select="$n"/>
 536    </xsl:apply-templates>
 537   </xsl:otherwise>
 538  </xsl:choose>
 539 </xsl:template>
 540
 541 <!-- Auxiliary functions -->
 542 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
 543 <!-- can replace the next template                                    -->
 544 <xsl:template name="get_name">
 545  <xsl:param name="uri" select="''"/>
 546  <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
 547  <xsl:choose>
 548   <xsl:when test="contains($sub_after,'/')">
 549    <xsl:call-template name="get_name">
 550     <xsl:with-param name="uri" select="$sub_after"/>
 551    </xsl:call-template>
 552   </xsl:when>
 553   <xsl:otherwise>
 554    <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
 555   </xsl:otherwise>
 556  </xsl:choose>
 557 </xsl:template>
 558
 559
 560 </xsl:stylesheet>