helm/style/proofs.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--******************************************************************-->
  28 <!-- Basic Logic                                                      -->
  29 <!-- (completely) Revisited: february 2001, Andrea Asperti            -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
  31 <!--******************************************************************-->
  32
  33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  34                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  35                               xmlns:helm="http://www.cs.unibo.it/helm">
  36
  37 <!-- ************************* LOGIC *********************************-->
  38
  39 <!-- Proof objects -->
  40
  41 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  42
  43 <!-- ALL this elements does not have inner type -->
  44 <xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
  45 <xsl:apply-templates select="." mode="pure"/>
  46 </xsl:template>
  47
  48 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
  49
  50 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
  51 <xsl:template match="LAMBDA" mode="noannot">
  52  <xsl:variable name="id" select="@id"/>
  53  <xsl:choose>
  54   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and name(../..) != 'LAMBDA'">
  55    <m:apply helm:xref="{@id}">
  56     <m:csymbol>proof</m:csymbol>
  57     <xsl:apply-templates mode="proof_transform" select="."/>
  58     <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
  59     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
  60    </m:apply>
  61   </xsl:when>
  62   <xsl:otherwise>
  63    <xsl:apply-templates select="." mode="pure"/>
  64   </xsl:otherwise>
  65  </xsl:choose>
  66 </xsl:template>
  67
  68 <!-- ALL these elements have inner type -->
  69 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  70  <xsl:variable name="id" select="@id"/>
  71  <xsl:choose>
  72   <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
  73    <m:apply helm:xref="{@id}">
  74     <m:csymbol>proof</m:csymbol>
  75     <xsl:apply-templates mode="proof_transform" select="."/>
  76     <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
  77     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
  78    </m:apply>
  79   </xsl:when>
  80   <xsl:otherwise>
  81    <xsl:choose>
  82     <xsl:when test="name()='APPLY'">
  83      <xsl:apply-templates select="." mode="letin"/>
  84     </xsl:when>
  85     <xsl:otherwise>
  86      <xsl:apply-templates select="." mode="pure"/>
  87     </xsl:otherwise>
  88    </xsl:choose>
  89   </xsl:otherwise>
  90  </xsl:choose>
  91 </xsl:template>
  92
  93 <xsl:template mode="try_inductive" match="APPLY">
  94    <xsl:variable name="id" select="@id"/>
  95    <xsl:choose>
  96     <xsl:when test="CONST[1]">
  97      <xsl:variable name="uri" select="CONST[1]/@uri"/>
  98      <xsl:choose>
  99       <xsl:when test="contains($uri,'_ind.con')">
 100        <xsl:variable name="ind_name">
 101         <xsl:call-template name="get_name">
 102          <xsl:with-param name="uri" select="$uri"/>
 103         </xsl:call-template>
 104        </xsl:variable>
 105        <xsl:variable name="ind_uri"
 106          select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
 107        <xsl:variable name="no_params">
 108         <xsl:call-template name="get_no_params">
 109          <xsl:with-param name="first_uri" select="$CICURI"/>
 110          <xsl:with-param name="second_uri" select="$uri"/>
 111         </xsl:call-template>
 112        </xsl:variable>
 113        <xsl:apply-templates mode="inductive" select=".">
 114         <xsl:with-param name="inductive_def_uri"
 115          select="$ind_uri"/>
 116         <xsl:with-param name="section_params" select="$no_params"/>
 117         <xsl:with-param name="inductive_def_index" select="1"/>
 118         <xsl:with-param name="inductive_def_name" select="$ind_name"/>
 119        </xsl:apply-templates>
 120       </xsl:when>
 121       <xsl:otherwise>
 122        <xsl:apply-templates mode="letin" select="."/>
 123       </xsl:otherwise>
 124      </xsl:choose>
 125     </xsl:when>
 126     <xsl:otherwise>
 127      <xsl:apply-templates mode="letin" select="."/>
 128     </xsl:otherwise>
 129    </xsl:choose>
 130 </xsl:template>
 131
 132
 133 <xsl:template mode="proof_transform" match="*">
 134    <xsl:variable name="id" select="@id"/>
 135    <xsl:choose>
 136     <!-- NATIND 3 parametri -->
 137     <xsl:when test="name()='APPLY' and CONST[
 138  attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 4">
 139      <m:apply>
 140       <m:csymbol>nat_ind</m:csymbol>
 141       <xsl:apply-templates mode="noannot" select="*[3]"/>
 142       <xsl:apply-templates mode="noannot" select="*[4]"/>
 143      </m:apply>
 144     </xsl:when>
 145     <!-- NATIND 4 parametri (nuova versione) -->
 146     <!--
 147     <xsl:when test="name()='APPLY' and CONST[
 148  attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con']
 149  and count(child::*) = 5
 150  and name(*[4])='LAMBDA'
 151  and name(*[4]/target/*[1])='LAMBDA'">
 152      <m:apply>
 153       <m:csymbol>nat_ind_complete</m:csymbol>
 154       <xsl:apply-templates mode="noannot" select="*[5]"/>
 155       <xsl:apply-templates mode="noannot" select="*[3]"/>
 156       <m:ci><xsl:value-of select="*[4]/target/@binder"/></m:ci>
 157       <m:ci><xsl:value-of select="*[4]/target/*[1]/target/@binder"/></m:ci>
 158       <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/source/*"/>
 159       <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/target/*"/>
 160      </m:apply>
 161     </xsl:when>
 162     -->
 163     <!-- EQUALITY -->
 164     <xsl:when test="name()= 'APPLY' and CONST[
 165  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 166  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 167  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 168  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 169  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 170       <m:apply>
 171        <m:csymbol>rw_step</m:csymbol>
 172        <xsl:apply-templates mode="noannot" select="*[5]"/>
 173        <xsl:apply-templates mode="pure" select="*[3]"/>
 174        <xsl:apply-templates mode="pure" select="*[6]"/>
 175        <xsl:apply-templates mode="pure" select="*[7]"/>
 176       </m:apply>
 177     </xsl:when>
 178     <!-- EQUALITY with extra-parameters -->
 179     <xsl:when test="name()= 'APPLY' and 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:apply-templates mode="pure" select="*[7]"/>
 196          </m:apply>
 197          <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
 198         </m:apply>
 199        </xsl:when>
 200        <xsl:otherwise>
 201         <xsl:choose>
 202          <xsl:when test="*[5]/@sort='Prop'">
 203           <m:apply helm:xref="{@id}">
 204            <m:csymbol>letin</m:csymbol>
 205            <m:apply>
 206             <m:csymbol>let</m:csymbol>
 207             <m:ci>
 208              <xsl:call-template name="insert_subscript">
 209               <xsl:with-param name="node_value" select="'h1'"/>
 210              </xsl:call-template>
 211             </m:ci>
 212             <xsl:apply-templates mode="noannot" select="*[5]"/>
 213            </m:apply>
 214            <xsl:call-template name="gen_let">
 215             <xsl:with-param name="init_pos" select="1"/>
 216             <xsl:with-param name="from" select="7"/>
 217            </xsl:call-template>
 218            <m:apply>
 219             <m:csymbol>rewrite_and_apply</m:csymbol>
 220             <m:apply>
 221              <m:csymbol>rw_step</m:csymbol>
 222              <m:ci>
 223               <xsl:call-template name="insert_subscript">
 224                <xsl:with-param name="node_value" select="'h1'"/>
 225               </xsl:call-template>
 226              </m:ci>
 227              <xsl:apply-templates mode="pure" select="*[3]"/>
 228              <xsl:apply-templates mode="pure" select="*[6]"/>
 229              <xsl:apply-templates mode="pure" select="*[7]"/>
 230             </m:apply>
 231             <xsl:apply-templates mode="flat" select="*[8]">
 232              <xsl:with-param name="n">
 233               <xsl:value-of select="2"/>
 234              </xsl:with-param>
 235             </xsl:apply-templates>
 236            </m:apply>
 237           </m:apply>
 238          </xsl:when>
 239          <xsl:otherwise>
 240           <m:apply helm:xref="{@id}">
 241            <m:csymbol>letin</m:csymbol>
 242            <xsl:call-template name="gen_let">
 243             <xsl:with-param name="init_pos" select="0"/>
 244             <xsl:with-param name="form" select="7"/>
 245            </xsl:call-template>
 246            <m:apply>
 247             <m:csymbol>rewrite_and_apply</m:csymbol>
 248             <m:apply>
 249              <m:csymbol>rw_step</m:csymbol>
 250              <xsl:apply-templates mode="pure" select="*[5]"/>
 251              <xsl:apply-templates mode="pure" select="*[3]"/>
 252              <xsl:apply-templates mode="pure" select="*[6]"/>
 253              <xsl:apply-templates mode="pure" select="*[7]"/>
 254             </m:apply>
 255             <xsl:apply-templates mode="flat" select="*[8]">
 256              <xsl:with-param name="n">
 257               <xsl:value-of select="1"/>
 258              </xsl:with-param>
 259             </xsl:apply-templates>
 260            </m:apply>
 261           </m:apply>
 262          </xsl:otherwise>
 263         </xsl:choose>
 264        </xsl:otherwise>
 265       </xsl:choose>
 266     </xsl:when>
 267     <!-- False_ind -->
 268     <xsl:when test="name()= 'APPLY' and CONST[
 269      attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
 270      count(child::*) = 3">
 271      <m:apply helm:xref="{@id}">
 272        <m:csymbol>false_ind</m:csymbol>
 273        <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
 274        <xsl:apply-templates mode="noannot" select="*[3]"/>
 275      </m:apply>
 276     </xsl:when>
 277     <!-- gestire meglio il caso di and_ind quando la prova
 278          non e' della forma \x.\y.M -->
 279     <xsl:when test="name()= 'APPLY' and CONST[
 280  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 281  and count(child::*) = 6
 282  and name(*[5])='LAMBDA'
 283  and name(*[5]/target/*[1])='LAMBDA'">
 284       <m:apply helm:xref="{@id}">
 285        <m:csymbol>and_ind</m:csymbol>
 286        <xsl:apply-templates mode="noannot" select="*[6]"/>
 287        <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>
 288        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 289        <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>
 290        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 291        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 292       </m:apply>
 293     </xsl:when>
 294     <xsl:when test="name()= 'APPLY' and CONST[
 295  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 296  and count(child::*) = 7">
 297       <xsl:choose>
 298        <xsl:when test="name(*[5])='LAMBDA'
 299                  and name(*[6])='LAMBDA'">
 300         <xsl:variable name="definition_url"
 301             select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
 302         <m:apply helm:xref="{@id}">
 303          <m:csymbol>full_or_ind</m:csymbol>
 304          <xsl:apply-templates mode="noannot" select="*[7]"/>
 305          <xsl:apply-templates mode="pure"
 306               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 307          <m:apply>
 308           <m:csymbol>left_case</m:csymbol>
 309           <m:bvar>
 310            <m:ci>
 311             <xsl:value-of select="*[5]/target/@binder"/>
 312            </m:ci>
 313            <m:type>
 314             <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
 315            </m:type>
 316           </m:bvar>
 317           <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
 318          </m:apply>
 319          <m:apply>
 320           <m:csymbol>right_case</m:csymbol>
 321           <m:bvar>
 322            <m:ci>
 323             <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
 324            </m:ci>
 325            <m:type>
 326             <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
 327            </m:type>
 328           </m:bvar>
 329           <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
 330          </m:apply>
 331         </m:apply>
 332        </xsl:when>
 333        <xsl:otherwise>
 334         <m:apply helm:xref="{@id}">
 335          <m:csymbol>or_ind</m:csymbol>
 336          <xsl:apply-templates mode="noannot" select="*[7]"/>
 337          <xsl:apply-templates mode="pure"
 338               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 339          <xsl:apply-templates mode="pure" select="*[5]"/>
 340          <xsl:apply-templates mode="pure" select="*[6]"/>
 341         </m:apply>
 342        </xsl:otherwise>
 343       </xsl:choose>
 344     </xsl:when>
 345     <!-- ex_ind, exT_ind -->
 346       <xsl:when test="name()= 'APPLY'
 347  and (CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 348       CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 349  and count(child::*) = 6
 350  and name(*[5])='LAMBDA'
 351  and name(*[5]/target/*[1])='LAMBDA'">
 352       <m:apply helm:xref="{@id}">
 353        <m:csymbol>ex_ind</m:csymbol>
 354        <xsl:apply-templates mode="noannot" select="*[6]"/>
 355        <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>
 356        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 357        <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>
 358        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 359        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 360       </m:apply>
 361     </xsl:when>
 362     <xsl:when test="(name()='APPLY') and (name(*[1])='CONST')">
 363      <xsl:apply-templates mode="try_inductive" select="."/>
 364     </xsl:when>
 365     <xsl:otherwise>
 366       <xsl:choose>
 367        <xsl:when test="name()='APPLY'">
 368         <xsl:apply-templates select="." mode="letin"/>
 369        </xsl:when>
 370        <xsl:otherwise>
 371         <xsl:apply-templates select="." mode="pure"/>
 372        </xsl:otherwise>
 373       </xsl:choose>
 374     </xsl:otherwise>
 375    </xsl:choose>
 376 </xsl:template>
 377
 378
 379 <xsl:template match="APPLY" mode="letin">
 380    <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')])"/>
 381    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
 382    <xsl:choose>
 383     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
 384      <m:apply helm:xref="{@id}">
 385       <m:csymbol>letin1</m:csymbol>
 386       <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')]"/>
 387       <!-- now re-process the application -->
 388       <m:apply helm:xref="{@id}">
 389        <m:csymbol>app</m:csymbol>
 390        <!-- mode previous looks for siblings:
 391             call with the first child -->
 392        <xsl:apply-templates mode="previous" select="*[1]"/>
 393       </m:apply>
 394      </m:apply>
 395     </xsl:when>
 396     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
 397      <m:apply helm:xref="{@id}">
 398       <m:csymbol>letin</m:csymbol>
 399       <!-- first process all subproofs (let-in) -->
 400       <xsl:call-template name="gen_let"/>
 401       <!-- now re-process the application  -->
 402       <m:apply helm:xref="{@id}">
 403        <m:csymbol>app</m:csymbol>
 404        <!-- mode flat looks for siblings: call with the first child -->
 405        <xsl:apply-templates mode="flat" select="*[1]"/>
 406       </m:apply>
 407      </m:apply>
 408     </xsl:when>
 409     <xsl:otherwise>
 410      <xsl:apply-templates mode="pure" select="."/>
 411     </xsl:otherwise>
 412    </xsl:choose>
 413 </xsl:template>
 414
 415 <xsl:template name="gen_let">
 416  <xsl:param name="init_pos" select="0"/>
 417  <xsl:param name="from" select="0"/>
 418       <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')]">
 419        <m:apply>
 420         <m:csymbol>let</m:csymbol>
 421         <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>
 422         <xsl:apply-templates mode="noannot" select="."/>
 423        </m:apply>
 424       </xsl:for-each>
 425 </xsl:template>
 426
 427 <xsl:template match="*" mode="previous">
 428  <xsl:choose>
 429   <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'))">
 430    <m:ci>previous</m:ci>
 431   </xsl:when>
 432   <xsl:otherwise>
 433    <xsl:apply-templates select="." mode="pure"/>
 434   </xsl:otherwise>
 435  </xsl:choose>
 436  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 437 </xsl:template>
 438
 439 <xsl:template match="*" mode="flat">
 440  <xsl:param name="n" select="1"/>
 441  <xsl:variable name="id" select="@id"/>
 442  <xsl:choose>
 443   <!-- <xsl:when test="key('typeid',@id)"> -->
 444   <!-- <xsl:when test="$InnerTypes/InnerTypes/TYPE[@of=$id]"> -->
 445   <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')">
 446    <m:ci>
 447     <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>
 448    </m:ci>
 449    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 450     <xsl:with-param name="n" select="$n+1"/>
 451    </xsl:apply-templates>
 452   </xsl:when>
 453   <xsl:otherwise>
 454    <xsl:apply-templates mode="pure" select="."/>
 455    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 456     <xsl:with-param name="n" select="$n"/>
 457    </xsl:apply-templates>
 458   </xsl:otherwise>
 459  </xsl:choose>
 460 </xsl:template>
 461
 462 <!-- Auxiliary functions -->
 463 <xsl:template name="get_name">
 464  <xsl:param name="uri" select="''"/>
 465  <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
 466  <xsl:choose>
 467   <xsl:when test="contains($sub_after,'/')">
 468    <xsl:call-template name="get_name">
 469     <xsl:with-param name="uri" select="$sub_after"/>
 470    </xsl:call-template>
 471   </xsl:when>
 472   <xsl:otherwise>
 473    <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
 474   </xsl:otherwise>
 475  </xsl:choose>
 476 </xsl:template>
 477
 478 <!-- <xsl:template match="APPLY[CONST[
 479  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 480     <xsl:choose>
 481      <xsl:when test="count(child::*) > 4">
 482       <m:apply helm:xref="{@id}">
 483        <m:csymbol>app</m:csymbol>
 484        <xsl:apply-templates mode="pure" select="*[1]"/>
 485        <m:ci>*</m:ci>
 486        <m:ci>*</m:ci>
 487        <m:ci>*</m:ci>
 488        <xsl:apply-templates mode="flat" select="*[5]"/>
 489       </m:apply>
 490      </xsl:when>
 491      <xsl:otherwise>
 492       <m:apply helm:xref="{@id}">
 493        <m:csymbol>app</m:csymbol>
 494        <xsl:apply-templates mode="flat" select="*[1]"/>
 495       </m:apply>
 496      </xsl:otherwise>
 497     </xsl:choose>
 498 </xsl:template>  -->
 499
 500
 501 </xsl:stylesheet>
 502
 503
 504
 505
 506
 507