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