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