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:call-template name="generate_side_proof">
 173         <xsl:with-param name="proof" select="*[7]"/>
 174        </xsl:call-template>
 175        <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
 176       </m:apply>
 177     </xsl:when>
 178     <!-- EQUALITY with extra-parameters -->
 179     <xsl:when test="CONST[
 180  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 181  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 182  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 183  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 184  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
 185       <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')])"/>
 186       <xsl:choose>
 187        <xsl:when test="$no_extraproofs=0">
 188         <m:apply>
 189          <m:csymbol>rewrite_and_apply</m:csymbol>
 190          <m:apply>
 191           <m:csymbol>rw_step</m:csymbol>
 192           <xsl:apply-templates mode="noannot" select="*[5]"/>
 193           <xsl:apply-templates mode="pure" select="*[3]"/>
 194           <xsl:apply-templates mode="pure" select="*[6]"/>
 195           <xsl:call-template name="generate_side_proof">
 196            <xsl:with-param name="proof" select="*[7]"/>
 197            </xsl:call-template>
 198           <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 199          </m:apply>
 200          <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
 201         </m:apply>
 202        </xsl:when>
 203        <xsl:otherwise>
 204         <xsl:choose>
 205          <xsl:when test="*[5]/@sort='Prop'">
 206           <m:apply helm:xref="{@id}">
 207            <m:csymbol>letin</m:csymbol>
 208            <m:apply>
 209             <m:csymbol>let</m:csymbol>
 210             <m:ci>
 211              <xsl:call-template name="insert_subscript">
 212               <xsl:with-param name="node_value" select="'h1'"/>
 213              </xsl:call-template>
 214             </m:ci>
 215             <xsl:apply-templates mode="noannot" select="*[5]"/>
 216            </m:apply>
 217            <xsl:call-template name="gen_let">
 218             <xsl:with-param name="init_pos" select="1"/>
 219             <xsl:with-param name="from" select="7"/>
 220            </xsl:call-template>
 221            <m:apply>
 222             <m:csymbol>rewrite_and_apply</m:csymbol>
 223             <m:apply>
 224              <m:csymbol>rw_step</m:csymbol>
 225              <m:ci>
 226               <xsl:call-template name="insert_subscript">
 227                <xsl:with-param name="node_value" select="'h1'"/>
 228               </xsl:call-template>
 229              </m:ci>
 230              <xsl:apply-templates mode="pure" select="*[3]"/>
 231              <xsl:apply-templates mode="pure" select="*[6]"/>
 232              <xsl:call-template name="generate_side_proof">
 233               <xsl:with-param name="proof" select="*[7]"/>
 234              </xsl:call-template>
 235              <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 236             </m:apply>
 237             <xsl:apply-templates mode="flat" select="*[8]">
 238              <xsl:with-param name="n">
 239               <xsl:value-of select="2"/>
 240              </xsl:with-param>
 241             </xsl:apply-templates>
 242            </m:apply>
 243           </m:apply>
 244          </xsl:when>
 245          <xsl:otherwise>
 246           <m:apply helm:xref="{@id}">
 247            <m:csymbol>letin</m:csymbol>
 248            <xsl:call-template name="gen_let">
 249             <xsl:with-param name="init_pos" select="0"/>
 250             <xsl:with-param name="form" select="7"/>
 251            </xsl:call-template>
 252            <m:apply>
 253             <m:csymbol>rewrite_and_apply</m:csymbol>
 254             <m:apply>
 255              <m:csymbol>rw_step</m:csymbol>
 256              <xsl:apply-templates mode="pure" select="*[5]"/>
 257              <xsl:apply-templates mode="pure" select="*[3]"/>
 258              <xsl:apply-templates mode="pure" select="*[6]"/>
 259              <xsl:call-template name="generate_side_proof">
 260               <xsl:with-param name="proof" select="*[7]"/>
 261              </xsl:call-template>
 262              <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 263             </m:apply>
 264             <xsl:apply-templates mode="flat" select="*[8]">
 265              <xsl:with-param name="n">
 266               <xsl:value-of select="1"/>
 267              </xsl:with-param>
 268             </xsl:apply-templates>
 269            </m:apply>
 270           </m:apply>
 271          </xsl:otherwise>
 272         </xsl:choose>
 273        </xsl:otherwise>
 274       </xsl:choose>
 275     </xsl:when>
 276     <!-- False_ind -->
 277     <xsl:when test="CONST[
 278      attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
 279      count(child::*) = 3">
 280      <m:apply helm:xref="{@id}">
 281        <m:csymbol>false_ind</m:csymbol>
 282        <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
 283        <xsl:apply-templates mode="noannot" select="*[3]"/>
 284      </m:apply>
 285     </xsl:when>
 286     <!-- gestire meglio il caso di and_ind quando la prova
 287          non e' della forma \x.\y.M -->
 288     <xsl:when test="CONST[
 289  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 290  and count(child::*) = 6
 291  and name(*[5])='LAMBDA'
 292  and name(*[5]/target/*[1])='LAMBDA'">
 293       <m:apply helm:xref="{@id}">
 294        <m:csymbol>and_ind</m:csymbol>
 295        <xsl:apply-templates mode="noannot" select="*[6]"/>
 296        <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>
 297        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 298        <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>
 299        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 300        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 301       </m:apply>
 302     </xsl:when>
 303     <xsl:when test="CONST[
 304  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 305  and count(child::*) = 7">
 306       <xsl:choose>
 307        <xsl:when test="name(*[5])='LAMBDA'
 308                  and name(*[6])='LAMBDA'">
 309         <xsl:variable name="definition_url"
 310             select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
 311         <m:apply helm:xref="{@id}">
 312          <m:csymbol>full_or_ind</m:csymbol>
 313          <xsl:apply-templates mode="noannot" select="*[7]"/>
 314          <xsl:apply-templates mode="pure"
 315               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 316          <m:apply>
 317           <m:csymbol>left_case</m:csymbol>
 318           <m:bvar>
 319            <m:ci>
 320             <xsl:value-of select="*[5]/target/@binder"/>
 321            </m:ci>
 322            <m:type>
 323             <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
 324            </m:type>
 325           </m:bvar>
 326           <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
 327          </m:apply>
 328          <m:apply>
 329           <m:csymbol>right_case</m:csymbol>
 330           <m:bvar>
 331            <m:ci>
 332             <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
 333            </m:ci>
 334            <m:type>
 335             <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
 336            </m:type>
 337           </m:bvar>
 338           <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
 339          </m:apply>
 340         </m:apply>
 341        </xsl:when>
 342        <xsl:otherwise>
 343         <m:apply helm:xref="{@id}">
 344          <m:csymbol>or_ind</m:csymbol>
 345          <xsl:apply-templates mode="noannot" select="*[7]"/>
 346          <xsl:apply-templates mode="pure"
 347               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 348          <xsl:apply-templates mode="pure" select="*[5]"/>
 349          <xsl:apply-templates mode="pure" select="*[6]"/>
 350         </m:apply>
 351        </xsl:otherwise>
 352       </xsl:choose>
 353     </xsl:when>
 354     <!-- ex_ind, exT_ind -->
 355       <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 356       CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 357  and count(child::*) = 6
 358  and name(*[5])='LAMBDA'
 359  and name(*[5]/target/*[1])='LAMBDA'">
 360       <m:apply helm:xref="{@id}">
 361        <m:csymbol>ex_ind</m:csymbol>
 362        <xsl:apply-templates mode="noannot" select="*[6]"/>
 363        <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>
 364        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 365        <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>
 366        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 367        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 368       </m:apply>
 369     </xsl:when>
 370     <xsl:when test="name(*[1])='CONST'">
 371      <xsl:apply-templates mode="try_inductive" select="."/>
 372     </xsl:when>
 373     <!-- patch temporanea per la gestione di redex -->
 374     <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
 375          and *[2]/@sort='Prop'">
 376      <m:apply helm:xref="{@id}">
 377       <m:csymbol>letin</m:csymbol>
 378       <m:apply>
 379        <m:csymbol>let</m:csymbol>
 380        <m:ci>
 381         <xsl:call-template name="insert_subscript">
 382          <xsl:with-param name="node_value">
 383           <xsl:value-of select="*[1]/target/@binder"/>
 384          </xsl:with-param>
 385         </xsl:call-template>
 386        </m:ci>
 387        <xsl:apply-templates mode="noannot" select="*[2]"/>
 388       </m:apply>
 389       <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
 390      </m:apply>
 391     </xsl:when>
 392     <xsl:otherwise>
 393      <xsl:apply-templates select="." mode="letin"/>
 394     </xsl:otherwise>
 395    </xsl:choose>
 396   </xsl:when>
 397   <xsl:when test="name()='LAMBDA'">
 398    <xsl:choose>
 399      <xsl:when test="(name(target/*[1])='APPLY'  and
 400       name(target/*[1]/*[1])='CONST' and
 401       (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 402        target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 403        target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
 404       and count(target/*[1]/*) = 8
 405       and name(target/*[1]/*[8])='REL'
 406       and target/@binder = target/*[1]/*[8]/@binder )">
 407       <m:apply>
 408        <m:csymbol>rw_step</m:csymbol>
 409        <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
 410        <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
 411        <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
 412        <xsl:call-template name="generate_side_proof">
 413         <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
 414        </xsl:call-template>
 415        <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
 416       </m:apply>
 417      </xsl:when>
 418      <xsl:otherwise>
 419       <xsl:apply-templates mode="pure" select="."/>
 420      </xsl:otherwise>
 421     </xsl:choose>
 422    </xsl:when>
 423   <xsl:otherwise>
 424    <xsl:apply-templates select="." mode="pure"/>
 425   </xsl:otherwise>
 426  </xsl:choose>
 427 </xsl:template>
 428
 429 <xsl:template name="is_simple">
 430  <xsl:param name="proof" select="/.."/>
 431  <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))"/>
 432 </xsl:template>
 433
 434 <xsl:template name="generate_side_proof">
 435  <xsl:param name="proof" select="/.."/>
 436 <!--
 437  <xsl:variable name="is_simple">
 438   <xsl:call-template name="is_simple">
 439    <xsl:with-param name="proof" select="$proof"/>
 440   </xsl:call-template>
 441  </xsl:variable> -->
 442 <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))"/>
 443  <xsl:choose>
 444   <xsl:when test="$is_simple">
 445    <xsl:choose>
 446     <xsl:when test="name($proof)='APPLY'">
 447      <xsl:apply-templates select="$proof" mode="letin"/>
 448     </xsl:when>
 449     <xsl:otherwise>
 450      <xsl:apply-templates select="$proof" mode="pure"/>
 451     </xsl:otherwise>
 452    </xsl:choose>
 453   </xsl:when>
 454   <xsl:otherwise>
 455    <xsl:apply-templates select="$proof" mode="noannot"/>
 456   </xsl:otherwise>
 457  </xsl:choose>
 458 </xsl:template>
 459
 460 <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')])"/>
 461
 462 <xsl:template match="APPLY" mode="letin">
 463    <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')])"/>
 464    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
 465    <xsl:choose>
 466     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
 467      <m:apply helm:xref="{@id}">
 468       <m:csymbol>letin1</m:csymbol>
 469       <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')]"/>
 470       <!-- now re-process the application -->
 471       <m:apply helm:xref="{@id}">
 472        <m:csymbol>app</m:csymbol>
 473        <!-- mode previous looks for siblings:
 474             call with the first child -->
 475        <xsl:apply-templates mode="previous" select="*[1]"/>
 476       </m:apply>
 477      </m:apply>
 478     </xsl:when>
 479     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
 480      <m:apply helm:xref="{@id}">
 481       <m:csymbol>letin</m:csymbol>
 482       <!-- first process all subproofs (let-in) -->
 483       <xsl:call-template name="gen_let"/>
 484       <!-- now re-process the application  -->
 485       <m:apply helm:xref="{@id}">
 486        <m:csymbol>app</m:csymbol>
 487        <!-- mode flat looks for siblings: call with the first child -->
 488        <xsl:apply-templates mode="flat" select="*[1]"/>
 489       </m:apply>
 490      </m:apply>
 491     </xsl:when>
 492     <xsl:otherwise>
 493      <xsl:choose>
 494      <xsl:when test="@sort='Prop'">
 495       <m:apply>
 496        <m:csymbol>app</m:csymbol>
 497        <xsl:apply-templates mode="erase" select="*[1]"/>
 498       </m:apply>
 499      </xsl:when>
 500      <xsl:otherwise>
 501       <xsl:apply-templates mode="pure" select="."/>
 502      </xsl:otherwise>
 503      </xsl:choose>
 504     </xsl:otherwise>
 505    </xsl:choose>
 506 </xsl:template>
 507
 508 <xsl:template name="gen_let">
 509  <xsl:param name="init_pos" select="0"/>
 510  <xsl:param name="from" select="0"/>
 511       <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')]">
 512        <m:apply>
 513         <m:csymbol>let</m:csymbol>
 514         <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>
 515         <xsl:apply-templates mode="noannot" select="."/>
 516        </m:apply>
 517       </xsl:for-each>
 518 </xsl:template>
 519
 520 <xsl:template match="*" mode="erase">
 521   <xsl:choose>
 522    <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
 523     <xsl:apply-templates mode="pure" select="."/>
 524    </xsl:when>
 525    <xsl:otherwise>
 526     <m:ci>.</m:ci>
 527    </xsl:otherwise>
 528    </xsl:choose>
 529  <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
 530 </xsl:template>
 531
 532 <xsl:template match="*" mode="previous">
 533  <xsl:choose>
 534   <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')">
 535    <m:ci>previous</m:ci>
 536   </xsl:when>
 537   <xsl:otherwise>
 538    <!-- forse bisognerebbe trattare solo l'elemento di testa -->
 539    <xsl:choose>
 540    <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
 541     <xsl:apply-templates mode="pure" select="."/>
 542    </xsl:when>
 543    <xsl:otherwise>
 544     <m:ci>.</m:ci>
 545    </xsl:otherwise>
 546    </xsl:choose>
 547    <!-- <xsl:apply-templates select="." mode="pure"/> -->
 548   </xsl:otherwise>
 549  </xsl:choose>
 550  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 551 </xsl:template>
 552
 553 <xsl:template match="*" mode="flat">
 554  <xsl:param name="n" select="1"/>
 555  <xsl:variable name="id" select="@id"/>
 556  <xsl:choose>
 557   <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')">
 558    <m:ci>
 559     <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>
 560    </m:ci>
 561    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 562     <xsl:with-param name="n" select="$n+1"/>
 563    </xsl:apply-templates>
 564   </xsl:when>
 565   <xsl:otherwise>
 566    <xsl:choose>
 567     <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
 568      <xsl:apply-templates mode="pure" select="."/>
 569     </xsl:when>
 570     <xsl:otherwise>
 571      <m:ci>.</m:ci>
 572     </xsl:otherwise>
 573    </xsl:choose>
 574    <!-- <xsl:apply-templates mode="pure" select="."/> -->
 575    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 576     <xsl:with-param name="n" select="$n"/>
 577    </xsl:apply-templates>
 578   </xsl:otherwise>
 579  </xsl:choose>
 580 </xsl:template>
 581
 582 <!-- Auxiliary functions -->
 583 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
 584 <!-- can replace the next template                                    -->
 585 <xsl:template name="get_name">
 586  <xsl:param name="uri" select="''"/>
 587  <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
 588  <xsl:choose>
 589   <xsl:when test="contains($sub_after,'/')">
 590    <xsl:call-template name="get_name">
 591     <xsl:with-param name="uri" select="$sub_after"/>
 592    </xsl:call-template>
 593   </xsl:when>
 594   <xsl:otherwise>
 595    <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
 596   </xsl:otherwise>
 597  </xsl:choose>
 598 </xsl:template>
 599
 600 <!-- <xsl:template match="APPLY[CONST[
 601  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 602     <xsl:choose>
 603      <xsl:when test="count(child::*) > 4">
 604       <m:apply helm:xref="{@id}">
 605        <m:csymbol>app</m:csymbol>
 606        <xsl:apply-templates mode="pure" select="*[1]"/>
 607        <m:ci>*</m:ci>
 608        <m:ci>*</m:ci>
 609        <m:ci>*</m:ci>
 610        <xsl:apply-templates mode="flat" select="*[5]"/>
 611       </m:apply>
 612      </xsl:when>
 613      <xsl:otherwise>
 614       <m:apply helm:xref="{@id}">
 615        <m:csymbol>app</m:csymbol>
 616        <xsl:apply-templates mode="flat" select="*[1]"/>
 617       </m:apply>
 618      </xsl:otherwise>
 619     </xsl:choose>
 620 </xsl:template>  -->
 621
 622
 623 </xsl:stylesheet>