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 <!-- ************************* LOGIC *********************************-->
  38
  39 <!-- Proof objects -->
  40
  41 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  42
  43 <!-- ALL this elements does not have inner type -->
  44 <xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
  45 <xsl:apply-templates select="." mode="pure"/>
  46 </xsl:template>
  47
  48 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
  49
  50 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
  51 <xsl:template match="LAMBDA" mode="noannot">
  52  <xsl:variable name="id" select="@id"/>
  53  <xsl:choose>
  54   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and name(../..) != 'LAMBDA'">
  55    <m:apply helm:xref="{@id}">
  56     <m:csymbol>proof</m:csymbol>
  57     <xsl:apply-templates mode="proof_transform" select="."/>
  58     <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
  59     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
  60    </m:apply>
  61   </xsl:when>
  62   <xsl:otherwise>
  63    <xsl:apply-templates select="." mode="pure"/>
  64   </xsl:otherwise>
  65  </xsl:choose>
  66 </xsl:template>
  67
  68 <!-- ALL these elements have inner type -->
  69 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  70  <xsl:variable name="id" select="@id"/>
  71  <xsl:choose>
  72   <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
  73    <m:apply helm:xref="{@id}">
  74     <m:csymbol>proof</m:csymbol>
  75     <xsl:apply-templates mode="proof_transform" select="."/>
  76     <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
  77     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
  78    </m:apply>
  79   </xsl:when>
  80   <xsl:otherwise>
  81    <xsl:choose>
  82     <xsl:when test="name()='APPLY'">
  83      <xsl:apply-templates select="." mode="letin"/>
  84     </xsl:when>
  85     <xsl:otherwise>
  86      <xsl:apply-templates select="." mode="pure"/>
  87     </xsl:otherwise>
  88    </xsl:choose>
  89   </xsl:otherwise>
  90  </xsl:choose>
  91 </xsl:template>
  92
  93 <!-- si presuppone che il tipo induttivo non sia mutuamente
  94      induttivo. Bisognerebbe andare a vedere l'utlimo parametro
  95      del presunto "principio di induzione", tirare fuori il tipo induttivo
  96      e vedere se il suo nome coincide con il prefisso di _ind.
  97      Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
  98      parametro di nat_double_ind e' di tipo nat, e nat e' diverso
  99      da nat_double. Per ora, verifico solo l'esistenza di nat_double,
 100      ma questo, benche' non porti ad errore, non copre tutti i
 101      casi per quelli mutuamente induttivi -->
 102
 103 <xsl:template mode="try_inductive" match="APPLY">
 104    <xsl:variable name="id" select="@id"/>
 105    <xsl:choose>
 106     <xsl:when test="CONST[1]">
 107      <xsl:variable name="uri" select="CONST[1]/@uri"/>
 108      <xsl:choose>
 109       <xsl:when test="contains($uri,'_ind.con')">
 110        <xsl:variable name="ind_uri"
 111          select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
 112        <xsl:variable name="inductive_def"
 113      select="document(concat(string($absPath),$ind_uri))/InductiveDefinition"/>
 114        <!-- check if the corresponding inductive definition actually
 115             exists -->
 116        <xsl:choose>
 117         <xsl:when test="$inductive_def">
 118          <xsl:variable name="ind_name">
 119           <xsl:call-template name="get_name">
 120            <xsl:with-param name="uri" select="$uri"/>
 121           </xsl:call-template>
 122          </xsl:variable>
 123          <xsl:variable name="no_params">
 124           <xsl:call-template name="get_no_params">
 125            <xsl:with-param name="first_uri" select="$CICURI"/>
 126            <xsl:with-param name="second_uri" select="$uri"/>
 127           </xsl:call-template>
 128          </xsl:variable>
 129          <xsl:apply-templates mode="inductive" select=".">
 130           <xsl:with-param name="inductive_def_uri"
 131            select="$ind_uri"/>
 132           <xsl:with-param name="inductive_def"
 133            select="$inductive_def"/>
 134           <xsl:with-param name="section_params" select="$no_params"/>
 135           <xsl:with-param name="inductive_def_index" select="1"/>
 136           <xsl:with-param name="inductive_def_name" select="$ind_name"/>
 137          </xsl:apply-templates>
 138         </xsl:when>
 139         <xsl:otherwise>
 140          <xsl:apply-templates mode="letin" select="."/>
 141         </xsl:otherwise>
 142        </xsl:choose>
 143       </xsl:when>
 144       <xsl:otherwise>
 145        <xsl:apply-templates mode="letin" select="."/>
 146       </xsl:otherwise>
 147      </xsl:choose>
 148     </xsl:when>
 149     <xsl:otherwise>
 150      <xsl:apply-templates mode="letin" select="."/>
 151     </xsl:otherwise>
 152    </xsl:choose>
 153 </xsl:template>
 154
 155
 156 <xsl:template mode="proof_transform" match="*">
 157  <xsl:choose>
 158   <xsl:when test="name()='APPLY'">
 159    <xsl:variable name="id" select="@id"/>
 160    <xsl:choose>
 161     <!-- NATIND 3 parametri -->
 162     <xsl:when test="CONST[attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con']              and count(child::*) = 4">
 163      <m:apply>
 164       <m:csymbol>nat_ind</m:csymbol>
 165       <xsl:apply-templates mode="noannot" select="*[3]"/>
 166       <xsl:apply-templates mode="noannot" select="*[4]"/>
 167      </m:apply>
 168     </xsl:when>
 169     <!-- NATIND 4 parametri (nuova versione) -->
 170     <!--
 171     <xsl:when test="CONST[
 172  attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con']
 173  and count(child::*) = 5
 174  and name(*[4])='LAMBDA'
 175  and name(*[4]/target/*[1])='LAMBDA'">
 176      <m:apply>
 177       <m:csymbol>nat_ind_complete</m:csymbol>
 178       <xsl:apply-templates mode="noannot" select="*[5]"/>
 179       <xsl:apply-templates mode="noannot" select="*[3]"/>
 180       <m:ci><xsl:value-of select="*[4]/target/@binder"/></m:ci>
 181       <m:ci><xsl:value-of select="*[4]/target/*[1]/target/@binder"/></m:ci>
 182       <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/source/*"/>
 183       <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/target/*"/>
 184      </m:apply>
 185     </xsl:when>
 186     -->
 187     <!-- EQUALITY -->
 188     <xsl:when test="CONST[
 189  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 190  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 191  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 192  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 193  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 194       <m:apply>
 195        <m:csymbol>rw_step</m:csymbol>
 196        <xsl:apply-templates mode="noannot" select="*[5]"/>
 197        <xsl:apply-templates mode="pure" select="*[3]"/>
 198        <xsl:apply-templates mode="pure" select="*[6]"/>
 199        <xsl:apply-templates mode="proof_transform" select="*[7]"/>
 200       </m:apply>
 201     </xsl:when>
 202     <!-- EQUALITY with extra-parameters -->
 203     <xsl:when test="CONST[
 204  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 205  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 206  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 207  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 208  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
 209       <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 210       <xsl:choose>
 211        <xsl:when test="$no_extraproofs=0">
 212         <m:apply>
 213          <m:csymbol>rewrite_and_apply</m:csymbol>
 214          <m:apply>
 215           <m:csymbol>rw_step</m:csymbol>
 216           <xsl:apply-templates mode="noannot" select="*[5]"/>
 217           <xsl:apply-templates mode="pure" select="*[3]"/>
 218           <xsl:apply-templates mode="pure" select="*[6]"/>
 219           <xsl:apply-templates mode="pure" select="*[7]"/>
 220          </m:apply>
 221          <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
 222         </m:apply>
 223        </xsl:when>
 224        <xsl:otherwise>
 225         <xsl:choose>
 226          <xsl:when test="*[5]/@sort='Prop'">
 227           <m:apply helm:xref="{@id}">
 228            <m:csymbol>letin</m:csymbol>
 229            <m:apply>
 230             <m:csymbol>let</m:csymbol>
 231             <m:ci>
 232              <xsl:call-template name="insert_subscript">
 233               <xsl:with-param name="node_value" select="'h1'"/>
 234              </xsl:call-template>
 235             </m:ci>
 236             <xsl:apply-templates mode="noannot" select="*[5]"/>
 237            </m:apply>
 238            <xsl:call-template name="gen_let">
 239             <xsl:with-param name="init_pos" select="1"/>
 240             <xsl:with-param name="from" select="7"/>
 241            </xsl:call-template>
 242            <m:apply>
 243             <m:csymbol>rewrite_and_apply</m:csymbol>
 244             <m:apply>
 245              <m:csymbol>rw_step</m:csymbol>
 246              <m:ci>
 247               <xsl:call-template name="insert_subscript">
 248                <xsl:with-param name="node_value" select="'h1'"/>
 249               </xsl:call-template>
 250              </m:ci>
 251              <xsl:apply-templates mode="pure" select="*[3]"/>
 252              <xsl:apply-templates mode="pure" select="*[6]"/>
 253              <xsl:apply-templates mode="pure" select="*[7]"/>
 254             </m:apply>
 255             <xsl:apply-templates mode="flat" select="*[8]">
 256              <xsl:with-param name="n">
 257               <xsl:value-of select="2"/>
 258              </xsl:with-param>
 259             </xsl:apply-templates>
 260            </m:apply>
 261           </m:apply>
 262          </xsl:when>
 263          <xsl:otherwise>
 264           <m:apply helm:xref="{@id}">
 265            <m:csymbol>letin</m:csymbol>
 266            <xsl:call-template name="gen_let">
 267             <xsl:with-param name="init_pos" select="0"/>
 268             <xsl:with-param name="form" select="7"/>
 269            </xsl:call-template>
 270            <m:apply>
 271             <m:csymbol>rewrite_and_apply</m:csymbol>
 272             <m:apply>
 273              <m:csymbol>rw_step</m:csymbol>
 274              <xsl:apply-templates mode="pure" select="*[5]"/>
 275              <xsl:apply-templates mode="pure" select="*[3]"/>
 276              <xsl:apply-templates mode="pure" select="*[6]"/>
 277              <xsl:apply-templates mode="pure" select="*[7]"/>
 278             </m:apply>
 279             <xsl:apply-templates mode="flat" select="*[8]">
 280              <xsl:with-param name="n">
 281               <xsl:value-of select="1"/>
 282              </xsl:with-param>
 283             </xsl:apply-templates>
 284            </m:apply>
 285           </m:apply>
 286          </xsl:otherwise>
 287         </xsl:choose>
 288        </xsl:otherwise>
 289       </xsl:choose>
 290     </xsl:when>
 291     <!-- False_ind -->
 292     <xsl:when test="CONST[
 293      attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
 294      count(child::*) = 3">
 295      <m:apply helm:xref="{@id}">
 296        <m:csymbol>false_ind</m:csymbol>
 297        <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
 298        <xsl:apply-templates mode="noannot" select="*[3]"/>
 299      </m:apply>
 300     </xsl:when>
 301     <!-- gestire meglio il caso di and_ind quando la prova
 302          non e' della forma \x.\y.M -->
 303     <xsl:when test="CONST[
 304  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 305  and count(child::*) = 6
 306  and name(*[5])='LAMBDA'
 307  and name(*[5]/target/*[1])='LAMBDA'">
 308       <m:apply helm:xref="{@id}">
 309        <m:csymbol>and_ind</m:csymbol>
 310        <xsl:apply-templates mode="noannot" select="*[6]"/>
 311        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 312        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 313        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 314        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 315        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 316       </m:apply>
 317     </xsl:when>
 318     <xsl:when test="CONST[
 319  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 320  and count(child::*) = 7">
 321       <xsl:choose>
 322        <xsl:when test="name(*[5])='LAMBDA'
 323                  and name(*[6])='LAMBDA'">
 324         <xsl:variable name="definition_url"
 325             select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
 326         <m:apply helm:xref="{@id}">
 327          <m:csymbol>full_or_ind</m:csymbol>
 328          <xsl:apply-templates mode="noannot" select="*[7]"/>
 329          <xsl:apply-templates mode="pure"
 330               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 331          <m:apply>
 332           <m:csymbol>left_case</m:csymbol>
 333           <m:bvar>
 334            <m:ci>
 335             <xsl:value-of select="*[5]/target/@binder"/>
 336            </m:ci>
 337            <m:type>
 338             <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
 339            </m:type>
 340           </m:bvar>
 341           <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
 342          </m:apply>
 343          <m:apply>
 344           <m:csymbol>right_case</m:csymbol>
 345           <m:bvar>
 346            <m:ci>
 347             <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
 348            </m:ci>
 349            <m:type>
 350             <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
 351            </m:type>
 352           </m:bvar>
 353           <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
 354          </m:apply>
 355         </m:apply>
 356        </xsl:when>
 357        <xsl:otherwise>
 358         <m:apply helm:xref="{@id}">
 359          <m:csymbol>or_ind</m:csymbol>
 360          <xsl:apply-templates mode="noannot" select="*[7]"/>
 361          <xsl:apply-templates mode="pure"
 362               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 363          <xsl:apply-templates mode="pure" select="*[5]"/>
 364          <xsl:apply-templates mode="pure" select="*[6]"/>
 365         </m:apply>
 366        </xsl:otherwise>
 367       </xsl:choose>
 368     </xsl:when>
 369     <!-- ex_ind, exT_ind -->
 370       <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 371       CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 372  and count(child::*) = 6
 373  and name(*[5])='LAMBDA'
 374  and name(*[5]/target/*[1])='LAMBDA'">
 375       <m:apply helm:xref="{@id}">
 376        <m:csymbol>ex_ind</m:csymbol>
 377        <xsl:apply-templates mode="noannot" select="*[6]"/>
 378        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 379        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 380        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 381        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 382        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 383       </m:apply>
 384     </xsl:when>
 385     <xsl:when test="name(*[1])='CONST'">
 386      <xsl:apply-templates mode="try_inductive" select="."/>
 387     </xsl:when>
 388     <!-- patch temporanea per la gestione di redex -->
 389     <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
 390          and *[2]/@sort='Prop'">
 391      <m:apply helm:xref="{@id}">
 392       <m:csymbol>letin</m:csymbol>
 393       <m:apply>
 394        <m:csymbol>let</m:csymbol>
 395        <m:ci>
 396         <xsl:call-template name="insert_subscript">
 397          <xsl:with-param name="node_value">
 398           <xsl:value-of select="*[1]/target/@binder"/>
 399          </xsl:with-param>
 400         </xsl:call-template>
 401        </m:ci>
 402        <xsl:apply-templates mode="noannot" select="*[2]"/>
 403       </m:apply>
 404       <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
 405      </m:apply>
 406     </xsl:when>
 407     <xsl:otherwise>
 408      <xsl:apply-templates select="." mode="letin"/>
 409     </xsl:otherwise>
 410    </xsl:choose>
 411   </xsl:when>
 412   <xsl:otherwise>
 413    <xsl:apply-templates select="." mode="pure"/>
 414   </xsl:otherwise>
 415  </xsl:choose>
 416 </xsl:template>
 417
 418
 419 <xsl:template match="APPLY" mode="letin">
 420    <xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 421    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
 422    <xsl:choose>
 423     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
 424      <m:apply helm:xref="{@id}">
 425       <m:csymbol>letin1</m:csymbol>
 426       <xsl:apply-templates mode="noannot" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
 427       <!-- now re-process the application -->
 428       <m:apply helm:xref="{@id}">
 429        <m:csymbol>app</m:csymbol>
 430        <!-- mode previous looks for siblings:
 431             call with the first child -->
 432        <xsl:apply-templates mode="previous" select="*[1]"/>
 433       </m:apply>
 434      </m:apply>
 435     </xsl:when>
 436     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
 437      <m:apply helm:xref="{@id}">
 438       <m:csymbol>letin</m:csymbol>
 439       <!-- first process all subproofs (let-in) -->
 440       <xsl:call-template name="gen_let"/>
 441       <!-- now re-process the application  -->
 442       <m:apply helm:xref="{@id}">
 443        <m:csymbol>app</m:csymbol>
 444        <!-- mode flat looks for siblings: call with the first child -->
 445        <xsl:apply-templates mode="flat" select="*[1]"/>
 446       </m:apply>
 447      </m:apply>
 448     </xsl:when>
 449     <xsl:otherwise>
 450      <xsl:apply-templates mode="pure" select="."/>
 451     </xsl:otherwise>
 452    </xsl:choose>
 453 </xsl:template>
 454
 455 <xsl:template name="gen_let">
 456  <xsl:param name="init_pos" select="0"/>
 457  <xsl:param name="from" select="0"/>
 458       <xsl:for-each select="*[position()>$from and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]">
 459        <m:apply>
 460         <m:csymbol>let</m:csymbol>
 461         <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>
 462         <xsl:apply-templates mode="noannot" select="."/>
 463        </m:apply>
 464       </xsl:for-each>
 465 </xsl:template>
 466
 467 <xsl:template match="*" mode="previous">
 468  <xsl:choose>
 469   <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'))">
 470    <m:ci>previous</m:ci>
 471   </xsl:when>
 472   <xsl:otherwise>
 473    <xsl:apply-templates select="." mode="pure"/>
 474   </xsl:otherwise>
 475  </xsl:choose>
 476  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 477 </xsl:template>
 478
 479 <xsl:template match="*" mode="flat">
 480  <xsl:param name="n" select="1"/>
 481  <xsl:variable name="id" select="@id"/>
 482  <xsl:choose>
 483   <!-- <xsl:when test="key('typeid',@id)"> -->
 484   <!-- <xsl:when test="$InnerTypes/InnerTypes/TYPE[@of=$id]"> -->
 485   <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')">
 486    <m:ci>
 487     <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>
 488    </m:ci>
 489    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 490     <xsl:with-param name="n" select="$n+1"/>
 491    </xsl:apply-templates>
 492   </xsl:when>
 493   <xsl:otherwise>
 494    <xsl:apply-templates mode="pure" select="."/>
 495    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 496     <xsl:with-param name="n" select="$n"/>
 497    </xsl:apply-templates>
 498   </xsl:otherwise>
 499  </xsl:choose>
 500 </xsl:template>
 501
 502 <!-- Auxiliary functions -->
 503 <xsl:template name="get_name">
 504  <xsl:param name="uri" select="''"/>
 505  <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
 506  <xsl:choose>
 507   <xsl:when test="contains($sub_after,'/')">
 508    <xsl:call-template name="get_name">
 509     <xsl:with-param name="uri" select="$sub_after"/>
 510    </xsl:call-template>
 511   </xsl:when>
 512   <xsl:otherwise>
 513    <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
 514   </xsl:otherwise>
 515  </xsl:choose>
 516 </xsl:template>
 517
 518 <!-- <xsl:template match="APPLY[CONST[
 519  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 520     <xsl:choose>
 521      <xsl:when test="count(child::*) > 4">
 522       <m:apply helm:xref="{@id}">
 523        <m:csymbol>app</m:csymbol>
 524        <xsl:apply-templates mode="pure" select="*[1]"/>
 525        <m:ci>*</m:ci>
 526        <m:ci>*</m:ci>
 527        <m:ci>*</m:ci>
 528        <xsl:apply-templates mode="flat" select="*[5]"/>
 529       </m:apply>
 530      </xsl:when>
 531      <xsl:otherwise>
 532       <m:apply helm:xref="{@id}">
 533        <m:csymbol>app</m:csymbol>
 534        <xsl:apply-templates mode="flat" select="*[1]"/>
 535       </m:apply>
 536      </xsl:otherwise>
 537     </xsl:choose>
 538 </xsl:template>  -->
 539
 540
 541 </xsl:stylesheet>
 542
 543
 544
 545
 546
 547