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