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