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="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
  76    </m:apply>
  77   </xsl:when>
  78   <xsl:otherwise>
  79    <xsl:choose>
  80     <xsl:when test="name()='APPLY'">
  81      <xsl:apply-templates select="." mode="letin"/>
  82     </xsl:when>
  83     <xsl:otherwise>
  84      <xsl:apply-templates select="." mode="pure"/>
  85     </xsl:otherwise>
  86    </xsl:choose>
  87   </xsl:otherwise>
  88  </xsl:choose>
  89 </xsl:template>
  90
  91 <xsl:template mode="proof_transform" match="*">
  92    <xsl:variable name="id" select="@id"/>
  93    <xsl:choose>
  94     <!-- NATIND 3 parametri -->
  95     <xsl:when test="name()='APPLY' and CONST[
  96  attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 4">
  97      <m:apply>
  98       <m:csymbol>nat_ind</m:csymbol>
  99       <xsl:apply-templates mode="noannot" select="*[3]"/>
 100       <xsl:apply-templates mode="noannot" select="*[4]"/>
 101      </m:apply>
 102     </xsl:when>
 103     <!-- NATIND 4 parametri -->
 104     <xsl:when test="name()='APPLY' and CONST[
 105  attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 5">
 106      <m:apply>
 107       <m:csymbol>nat_ind</m:csymbol>
 108       <xsl:apply-templates mode="noannot" select="*[3]"/>
 109       <xsl:apply-templates mode="noannot" select="*[4]"/>
 110      </m:apply>
 111     </xsl:when>
 112     <!-- EQUALITY -->
 113     <xsl:when test="name()= 'APPLY' and CONST[
 114  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 115  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 116  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 117       <m:apply>
 118        <m:csymbol>rw_step</m:csymbol>
 119        <xsl:apply-templates mode="noannot" select="*[5]"/>
 120        <xsl:apply-templates mode="pure" select="*[3]"/>
 121        <xsl:apply-templates mode="pure" select="*[6]"/>
 122        <xsl:apply-templates mode="pure" select="*[7]"/>
 123       </m:apply>
 124     </xsl:when>
 125     <!-- EQUALITY with extra-parameters -->
 126     <xsl:when test="name()= 'APPLY' and CONST[
 127  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 128  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 129  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
 130       <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')])"/>
 131       <xsl:choose>
 132        <xsl:when test="$no_extraproofs=0">
 133         <m:apply>
 134          <m:csymbol>rewrite_and_apply</m:csymbol>
 135          <m:apply>
 136           <m:csymbol>rw_step</m:csymbol>
 137           <xsl:apply-templates mode="noannot" select="*[5]"/>
 138           <xsl:apply-templates mode="pure" select="*[3]"/>
 139           <xsl:apply-templates mode="pure" select="*[6]"/>
 140           <xsl:apply-templates mode="pure" select="*[7]"/>
 141          </m:apply>
 142          <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
 143         </m:apply>
 144        </xsl:when>
 145        <xsl:otherwise>
 146         <xsl:choose>
 147          <xsl:when test="*[5]/@sort='Prop'">
 148           <m:apply helm:xref="{@id}">
 149            <m:csymbol>letin</m:csymbol>
 150            <m:apply>
 151             <m:csymbol>let</m:csymbol>
 152             <m:ci>
 153              <xsl:call-template name="insert_subscript">
 154               <xsl:with-param name="node_value" select="'h1'"/>
 155              </xsl:call-template>
 156             </m:ci>
 157             <xsl:apply-templates mode="noannot" select="*[5]"/>
 158            </m:apply>
 159            <xsl:call-template name="gen_let">
 160             <xsl:with-param name="init_pos" select="1"/>
 161             <xsl:with-param name="from" select="7"/>
 162            </xsl:call-template>
 163            <m:apply>
 164             <m:csymbol>rewrite_and_apply</m:csymbol>
 165             <m:apply>
 166              <m:csymbol>rw_step</m:csymbol>
 167              <m:ci>
 168               <xsl:call-template name="insert_subscript">
 169                <xsl:with-param name="node_value" select="'h1'"/>
 170               </xsl:call-template>
 171              </m:ci>
 172              <xsl:apply-templates mode="pure" select="*[3]"/>
 173              <xsl:apply-templates mode="pure" select="*[6]"/>
 174              <xsl:apply-templates mode="pure" select="*[7]"/>
 175             </m:apply>
 176             <xsl:apply-templates mode="flat" select="*[8]">
 177              <xsl:with-param name="n">
 178               <xsl:value-of select="2"/>
 179              </xsl:with-param>
 180             </xsl:apply-templates>
 181            </m:apply>
 182           </m:apply>
 183          </xsl:when>
 184          <xsl:otherwise>
 185           <m:apply helm:xref="{@id}">
 186            <m:csymbol>letin</m:csymbol>
 187            <xsl:call-template name="gen_let">
 188             <xsl:with-param name="init_pos" select="0"/>
 189             <xsl:with-param name="form" select="7"/>
 190            </xsl:call-template>
 191            <m:apply>
 192             <m:csymbol>rewrite_and_apply</m:csymbol>
 193             <m:apply>
 194              <m:csymbol>rw_step</m:csymbol>
 195              <xsl:apply-templates mode="pure" select="*[5]"/>
 196              <xsl:apply-templates mode="pure" select="*[3]"/>
 197              <xsl:apply-templates mode="pure" select="*[6]"/>
 198              <xsl:apply-templates mode="pure" select="*[7]"/>
 199             </m:apply>
 200             <xsl:apply-templates mode="flat" select="*[8]">
 201              <xsl:with-param name="n">
 202               <xsl:value-of select="1"/>
 203              </xsl:with-param>
 204             </xsl:apply-templates>
 205            </m:apply>
 206           </m:apply>
 207          </xsl:otherwise>
 208         </xsl:choose>
 209        </xsl:otherwise>
 210       </xsl:choose>
 211     </xsl:when>
 212     <!-- gestire meglio il caso di and_ind quando la prova
 213          non e' della forma \x.\y.M -->
 214     <xsl:when test="name()= 'APPLY' and CONST[
 215  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 216  and count(child::*) = 6
 217  and name(*[5])='LAMBDA'
 218  and name(*[5]/target/*[1])='LAMBDA'">
 219       <m:apply helm:xref="{@id}">
 220        <m:csymbol>and_ind</m:csymbol>
 221        <xsl:apply-templates mode="noannot" select="*[6]"/>
 222        <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>
 223        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 224        <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>
 225        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 226        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 227       </m:apply>
 228     </xsl:when>
 229     <xsl:when test="name()= 'APPLY' and CONST[
 230  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 231  and count(child::*) = 7">
 232      <m:apply helm:xref="{@id}">
 233       <m:csymbol>or_ind</m:csymbol>
 234       <xsl:apply-templates mode="noannot" select="*[7]"/>
 235       <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 236       <xsl:apply-templates mode="pure" select="*[5]"/>
 237       <xsl:apply-templates mode="pure" select="*[6]"/>
 238      </m:apply>
 239     </xsl:when>
 240     <!-- ex_ind, exT_ind -->
 241       <xsl:when test="name()= 'APPLY'
 242  and (CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 243       CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 244  and count(child::*) = 6
 245  and name(*[5])='LAMBDA'
 246  and name(*[5]/target/*[1])='LAMBDA'">
 247       <m:apply helm:xref="{@id}">
 248        <m:csymbol>ex_ind</m:csymbol>
 249        <xsl:apply-templates mode="noannot" select="*[6]"/>
 250        <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>
 251        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 252        <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>
 253        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 254        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 255       </m:apply>
 256     </xsl:when>
 257     <xsl:otherwise>
 258       <xsl:choose>
 259        <xsl:when test="name()='APPLY'">
 260         <xsl:apply-templates select="." mode="letin"/>
 261        </xsl:when>
 262        <xsl:otherwise>
 263         <xsl:apply-templates select="." mode="pure"/>
 264        </xsl:otherwise>
 265       </xsl:choose>
 266     </xsl:otherwise>
 267    </xsl:choose>
 268 </xsl:template>
 269
 270
 271 <xsl:template match="APPLY" mode="letin">
 272    <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')])"/>
 273    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
 274    <xsl:choose>
 275     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
 276      <m:apply helm:xref="{@id}">
 277       <m:csymbol>letin1</m:csymbol>
 278       <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')]"/>
 279       <!-- now re-process the application -->
 280       <m:apply helm:xref="{@id}">
 281        <m:csymbol>app</m:csymbol>
 282        <!-- mode previous looks for siblings:
 283             call with the first child -->
 284        <xsl:apply-templates mode="previous" select="*[1]"/>
 285       </m:apply>
 286      </m:apply>
 287     </xsl:when>
 288     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
 289      <m:apply helm:xref="{@id}">
 290       <m:csymbol>letin</m:csymbol>
 291       <!-- first process all subproofs (let-in) -->
 292       <xsl:call-template name="gen_let"/>
 293       <!-- now re-process the application  -->
 294       <m:apply helm:xref="{@id}">
 295        <m:csymbol>app</m:csymbol>
 296        <!-- mode flat looks for siblings: call with the first child -->
 297        <xsl:apply-templates mode="flat" select="*[1]"/>
 298       </m:apply>
 299      </m:apply>
 300     </xsl:when>
 301     <xsl:otherwise>
 302      <xsl:apply-templates mode="pure" select="."/>
 303     </xsl:otherwise>
 304    </xsl:choose>
 305 </xsl:template>
 306
 307 <xsl:template name="gen_let">
 308  <xsl:param name="init_pos" select="0"/>
 309  <xsl:param name="from" select="0"/>
 310       <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')]">
 311        <m:apply>
 312         <m:csymbol>let</m:csymbol>
 313         <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>
 314         <xsl:apply-templates mode="noannot" select="."/>
 315        </m:apply>
 316       </xsl:for-each>
 317 </xsl:template>
 318
 319 <xsl:template match="*" mode="previous">
 320  <xsl:choose>
 321   <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'))">
 322    <m:ci>previous</m:ci>
 323   </xsl:when>
 324   <xsl:otherwise>
 325    <xsl:apply-templates select="." mode="pure"/>
 326   </xsl:otherwise>
 327  </xsl:choose>
 328  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 329 </xsl:template>
 330
 331 <xsl:template match="*" mode="flat">
 332  <xsl:param name="n" select="1"/>
 333  <xsl:variable name="id" select="@id"/>
 334  <xsl:choose>
 335   <!-- <xsl:when test="key('typeid',@id)"> -->
 336   <!-- <xsl:when test="$InnerTypes/InnerTypes/TYPE[@of=$id]"> -->
 337   <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')">
 338    <m:ci>
 339     <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>
 340    </m:ci>
 341    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 342     <xsl:with-param name="n" select="$n+1"/>
 343    </xsl:apply-templates>
 344   </xsl:when>
 345   <xsl:otherwise>
 346    <xsl:apply-templates mode="pure" select="."/>
 347    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 348     <xsl:with-param name="n" select="$n"/>
 349    </xsl:apply-templates>
 350   </xsl:otherwise>
 351  </xsl:choose>
 352 </xsl:template>
 353
 354
 355 <!-- <xsl:template match="APPLY[CONST[
 356  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 357     <xsl:choose>
 358      <xsl:when test="count(child::*) > 4">
 359       <m:apply helm:xref="{@id}">
 360        <m:csymbol>app</m:csymbol>
 361        <xsl:apply-templates mode="pure" select="*[1]"/>
 362        <m:ci>*</m:ci>
 363        <m:ci>*</m:ci>
 364        <m:ci>*</m:ci>
 365        <xsl:apply-templates mode="flat" select="*[5]"/>
 366       </m:apply>
 367      </xsl:when>
 368      <xsl:otherwise>
 369       <m:apply helm:xref="{@id}">
 370        <m:csymbol>app</m:csymbol>
 371        <xsl:apply-templates mode="flat" select="*[1]"/>
 372       </m:apply>
 373      </xsl:otherwise>
 374     </xsl:choose>
 375 </xsl:template>  -->
 376
 377
 378 </xsl:stylesheet>
 379
 380
 381
 382
 383
 384