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