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 <!-- First draft: April 3 2000                                        -->
  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
  38 <!-- ************************* LOGIC *********************************-->
  39
  40 <!-- Proof objects -->
  41
  42 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  43
  44 <!-- ALL this elements does not have inner type -->
  45 <xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
  46 <xsl:apply-templates select="." mode="pure"/>
  47 </xsl:template>
  48
  49 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
  50 <xsl:template match="LAMBDA" mode="noannot">
  51  <xsl:variable name="id" select="@id"/>
  52  <xsl:choose>
  53   <xsl:when test="//InnerTypes and @sort='Prop' and name(../..) != 'LAMBDA'">
  54   <!-- <xsl:when test="@sort='Prop' and //InnerTypes/TYPE[@of=$id]"> -->
  55    <xsl:call-template name="has_inner_type"/>
  56   </xsl:when>
  57   <xsl:otherwise>
  58    <xsl:apply-templates select="." mode="pure"/>
  59   </xsl:otherwise>
  60  </xsl:choose>
  61 </xsl:template>
  62
  63 <!-- ALL this elements have inner type -->
  64 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  65  <xsl:choose>
  66   <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
  67   <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
  68   <xsl:when test="//InnerTypes and @sort='Prop'">
  69    <xsl:call-template name="has_inner_type"/>
  70   </xsl:when>
  71   <xsl:otherwise>
  72    <xsl:apply-templates select="." mode="pure"/>
  73   </xsl:otherwise>
  74  </xsl:choose>
  75 </xsl:template>
  76
  77 <xsl:template name="has_inner_type">
  78    <xsl:variable name="id" select="@id"/>
  79    <xsl:choose>
  80     <xsl:when test="name()= 'APPLY' and CONST[
  81  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
  82  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
  83      <m:apply helm:xref="{@id}">
  84       <m:csymbol>thread</m:csymbol>
  85       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
  86       <m:apply>
  87        <m:csymbol>rw_step</m:csymbol>
  88        <xsl:apply-templates mode="pure" select="*[3]"/>
  89        <xsl:apply-templates mode="pure" select="*[6]"/>
  90        <xsl:apply-templates mode="pure" select="*[7]"/>
  91       </m:apply>
  92       <xsl:apply-templates mode="thread" select="*[5]"/>
  93      </m:apply>
  94     </xsl:when>
  95     <!-- gestire meglio il caso di and_ind quando la prova
  96          non e' della forma \x.\y.M -->
  97     <xsl:when test="name()= 'APPLY' and CONST[
  98  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
  99  and count(child::*) = 6
 100  and name(*[5])='LAMBDA'
 101  and name(*[5]/target/*[1])='LAMBDA'">
 102      <m:apply helm:xref="{@id}">
 103       <m:csymbol>and_ind</m:csymbol>
 104       <xsl:apply-templates mode="noannot" select="*[6]"/>
 105       <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>
 106       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 107       <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>
 108       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 109       <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
 110      </m:apply>
 111     </xsl:when>
 112     <xsl:when test="name()= 'APPLY' and CONST[
 113  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 114  and count(child::*) = 7">
 115      <m:apply helm:xref="{@id}">
 116       <m:csymbol>or_ind</m:csymbol>
 117       <xsl:apply-templates mode="noannot" select="*[7]"/>
 118       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 119       <xsl:apply-templates mode="pure" select="*[5]"/>
 120       <xsl:apply-templates mode="pure" select="*[6]"/>
 121      </m:apply>
 122     </xsl:when>
 123     <!-- ex_ind, exT_ind -->
 124     <xsl:when test="name()= 'APPLY'
 125  and (CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 126       CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 127  and count(child::*) = 6
 128  and name(*[5])='LAMBDA'
 129  and name(*[5]/target/*[1])='LAMBDA'">
 130      <m:apply helm:xref="{@id}">
 131       <m:csymbol>ex_ind</m:csymbol>
 132       <xsl:apply-templates mode="noannot" select="*[6]"/>
 133       <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>
 134       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 135       <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>
 136       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 137       <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
 138      </m:apply>
 139     </xsl:when>
 140     <!-- Threads -->
 141     <!-- <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1"> -->
 142     <xsl:when test="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 1">
 143      <m:apply helm:xref="{@id}">
 144       <m:csymbol>thread</m:csymbol>
 145       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 146       <m:apply>
 147        <m:csymbol>app</m:csymbol>
 148        <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 149       </m:apply>
 150       <xsl:apply-templates mode="thread" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
 151      </m:apply>
 152     </xsl:when>
 153     <xsl:otherwise>
 154      <m:apply helm:xref="{@id}">
 155       <m:csymbol>proof</m:csymbol>
 156       <xsl:apply-templates select="." mode="pure"/>
 157       <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
 158       <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]/*" mode="pure"/>
 159      </m:apply>
 160     </xsl:otherwise>
 161    </xsl:choose>
 162 </xsl:template>
 163
 164 <xsl:template match="*" mode="copy-of-no-prop">
 165  <xsl:choose>
 166   <!-- <xsl:when test="@id = //InnerTypes/TYPE/@of"> -->
 167   <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
 168    <m:ci>previous</m:ci>
 169   </xsl:when>
 170   <xsl:otherwise>
 171    <xsl:apply-templates select="." mode="pure"/>
 172   </xsl:otherwise>
 173  </xsl:choose>
 174  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
 175 </xsl:template>
 176
 177 <xsl:template match="*" mode="thread">
 178   <xsl:choose>
 179    <xsl:when test="name()= 'APPLY' and CONST[
 180  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 181  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 182     <xsl:variable name="id" select="@id"/>
 183      <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 184      <m:apply>
 185       <m:csymbol>rw_step</m:csymbol>
 186       <xsl:apply-templates mode="pure" select="*[3]"/>
 187       <xsl:apply-templates mode="pure" select="*[6]"/>
 188       <xsl:apply-templates mode="pure" select="*[7]"/>
 189      </m:apply>
 190      <xsl:apply-templates mode="thread" select="*[5]"/>
 191    </xsl:when>
 192 <!--**** Patch temporanea, per il problema dei threads ***-->
 193 <xsl:when test="(name()= 'APPLY' and
 194  (CONST[attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] or
 195   CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 196   CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 197  and count(child::*) = 6
 198  and name(*[5])='LAMBDA'
 199  and name(*[5]/target/*[1])='LAMBDA')
 200  or
 201 (name()= 'APPLY' and CONST[
 202  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 203  and count(child::*) = 7)">
 204  <xsl:apply-templates mode="noannot" select="."/>
 205 </xsl:when>
 206 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
 207    <xsl:when test="//InnerTypes and count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 1">
 208        <xsl:variable name="id" select="@id"/>
 209        <m:apply helm:xref="{@id}">
 210         <m:csymbol>thread</m:csymbol>
 211         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 212         <m:apply>
 213          <m:csymbol>app</m:csymbol>
 214          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 215         </m:apply>
 216         <!-- <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/> -->
 217         <xsl:apply-templates mode="thread" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
 218        </m:apply>
 219    </xsl:when>
 220    <xsl:otherwise>
 221     <xsl:apply-templates mode="noannot" select="."/>
 222    </xsl:otherwise>
 223   </xsl:choose>
 224 </xsl:template>
 225
 226
 227 <!-- Basic proof operators -->
 228
 229 <!-- non del tutto soddisfacente, ma .... -->
 230 <xsl:template match="APPLY[CONST[
 231  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 232  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
 233     <xsl:choose>
 234      <xsl:when test="count(child::*) > 7">
 235       <xsl:variable name="id" select="@id"/>
 236       <xsl:variable name="ideqp" select="*[7]/@id"/>
 237       <xsl:variable name="idsubp" select="*[5]/@id"/>
 238 <!--
 239       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
 240       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
 241 -->
 242       <xsl:variable name="leteqp" select="boolean(*[7][@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 243       <xsl:variable name="letsubp" select="boolean(*[5][@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 244       <m:apply helm:xref="{@id}">
 245        <m:csymbol>rewrite_and_apply</m:csymbol>
 246        <m:apply>
 247         <m:csymbol>rw_step</m:csymbol>
 248         <xsl:apply-templates mode="pure" select="*[3]"/>
 249         <xsl:apply-templates mode="pure" select="*[6]"/>
 250         <xsl:choose>
 251          <xsl:when test="$leteqp">
 252           <xsl:choose>
 253            <xsl:when test="$letsubp">
 254             <m:ci>
 255              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
 256             </m:ci>
 257            </xsl:when>
 258            <xsl:otherwise>
 259             <m:ci>
 260              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 261             </m:ci>
 262            </xsl:otherwise>
 263           </xsl:choose>
 264          </xsl:when>
 265          <xsl:otherwise>
 266           <xsl:apply-templates mode="pure" select="*[7]"/>
 267          </xsl:otherwise>
 268         </xsl:choose>
 269        </m:apply>
 270       <xsl:choose>
 271        <xsl:when test="$letsubp">
 272         <m:ci>
 273          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 274         </m:ci>
 275        </xsl:when>
 276        <xsl:otherwise>
 277         <xsl:apply-templates mode="pure" select="*[5]"/>
 278        </xsl:otherwise>
 279       </xsl:choose>
 280       <xsl:apply-templates mode="flat" select="*[8]">
 281        <xsl:with-param name="n">
 282         <xsl:value-of select="1+$letsubp+$leteqp"/>
 283        </xsl:with-param>
 284       </xsl:apply-templates>
 285      </m:apply>
 286     </xsl:when>
 287     <xsl:otherwise>
 288      <m:apply helm:xref="{@id}">
 289       <m:csymbol>app</m:csymbol>
 290       <xsl:apply-templates mode="flat" select="*[1]"/>
 291      </m:apply>
 292     </xsl:otherwise>
 293    </xsl:choose>
 294 </xsl:template>
 295
 296 <xsl:template match="APPLY[CONST[
 297  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 298     <xsl:choose>
 299      <xsl:when test="count(child::*) > 4">
 300       <m:apply helm:xref="{@id}">
 301        <m:csymbol>app</m:csymbol>
 302        <xsl:apply-templates mode="pure" select="*[1]"/>
 303        <m:ci>*</m:ci>
 304        <m:ci>*</m:ci>
 305        <m:ci>*</m:ci>
 306        <xsl:apply-templates mode="flat" select="*[5]"/>
 307       </m:apply>
 308      </xsl:when>
 309      <xsl:otherwise>
 310       <m:apply helm:xref="{@id}">
 311        <m:csymbol>app</m:csymbol>
 312        <xsl:apply-templates mode="flat" select="*[1]"/>
 313       </m:apply>
 314      </xsl:otherwise>
 315     </xsl:choose>
 316 </xsl:template>
 317
 318
 319 </xsl:stylesheet>
 320
 321
 322
 323
 324
 325