helm/style/reals.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 <!-- Reals                                                            -->
  29 <!-- First draft: April 3 2000                                        -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi          -->
  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                               xmlns:xlink="http://www.w3.org/1999/xlink">
  37
  38
  39 <!-- ************************* LOGIC *********************************-->
  40
  41 <!-- REALS -->
  42
  43 <!--
  44 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R.con']" mode="pure">
  45  <m:reals/>
  46 </xsl:template>
  47 -->
  48
  49 <!-- 0 e 1 -->
  50
  51 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R0.con']" mode="pure">
  52  <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
  53 </xsl:template>
  54
  55 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R1.con']" mode="pure">
  56  <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
  57 </xsl:template>
  58
  59 <!-- Unary Operations and power -->
  60
  61 <xsl:template match="APPLY[CONST[
  62  attribute::uri='cic:/Coq/Reals/Rdefinitions/Ropp.con' or
  63  attribute::uri='cic:/Coq/Reals/Rbasic_fun/Rabsolu.con' or
  64  attribute::uri='cic:/Coq/Reals/Rfunctions/fact.con' or
  65  attribute::uri='cic:/Coq/Reals/Rbase/Rsqr.con']]" mode="pure">
  66     <xsl:choose>
  67      <xsl:when test="count(child::*) = 2">
  68       <xsl:variable name="elem">
  69        <xsl:choose>
  70         <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Ropp.con'">
  71          <xsl:value-of select="'minus'"/>
  72         </xsl:when>
  73         <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rabsolu.con'">
  74          <xsl:value-of select="'abs'"/>
  75         </xsl:when>
  76         <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rfunctions/fact.con'">
  77          <xsl:value-of select="'factorial'"/>
  78         </xsl:when>
  79         <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbase/Rsqr.con'">
  80          <xsl:value-of select="'power'"/>
  81         </xsl:when>
  82        </xsl:choose>
  83       </xsl:variable>
  84       <m:apply helm:xref="{@id}">
  85        <xsl:element name="{concat('m:',$elem)}">
  86         <xsl:attribute name="definitionURL">
  87          <xsl:value-of select="CONST/@uri"/>
  88         </xsl:attribute>
  89         <xsl:attribute name="helm:xref">
  90          <xsl:value-of select="CONST/@id"/>
  91         </xsl:attribute>
  92        </xsl:element>
  93        <xsl:apply-templates select="*[2]" mode="noannot"/>
  94        <xsl:if test="string($elem)='power'">
  95         <m:cn><xsl:value-of select="*[2]/@value"/></m:cn>
  96        </xsl:if>
  97       </m:apply>
  98      </xsl:when>
  99      <xsl:otherwise>
 100       <xsl:apply-imports/>
 101      </xsl:otherwise>
 102     </xsl:choose>
 103 </xsl:template>
 104
 105 <xsl:template match="APPLY[CONST[
 106  attribute::uri='cic:/Coq/Reals/Rdefinitions/Rinv.con']]" mode="pure">
 107     <xsl:choose>
 108      <xsl:when test="count(child::*) = 2">
 109       <m:apply helm:xref="{@id}">
 110        <m:power/>
 111        <xsl:apply-templates select="*[2]" mode="noannot"/>
 112        <m:apply>
 113         <m:minus>
 114          <xsl:attribute name="definitionURL">
 115           <xsl:value-of select="CONST/@uri"/>
 116          </xsl:attribute>
 117          <xsl:attribute name="helm:xref">
 118           <xsl:value-of select="CONST/@id"/>
 119          </xsl:attribute>
 120         </m:minus>
 121         <m:cn>1</m:cn>
 122        </m:apply>
 123       </m:apply>
 124      </xsl:when>
 125      <xsl:otherwise>
 126       <xsl:apply-imports/>
 127      </xsl:otherwise>
 128     </xsl:choose>
 129 </xsl:template>
 130
 131 <!-- Binary Operations and Relations -->
 132
 133 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rle.con']" mode="pure">
 134    <xsl:call-template name="mk-mml-infix">
 135       <xsl:with-param name="c-tag" select="CONST"/>
 136       <xsl:with-param name="m-tag" select="'leq'"/>
 137    </xsl:call-template>
 138 </xsl:template>
 139
 140 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rlt.con']" mode="pure">
 141    <xsl:call-template name="mk-mml-infix">
 142       <xsl:with-param name="c-tag" select="CONST"/>
 143       <xsl:with-param name="m-tag" select="'lt'"/>
 144    </xsl:call-template>
 145 </xsl:template>
 146
 147 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con']" mode="pure">
 148    <xsl:call-template name="mk-mml-infix">
 149       <xsl:with-param name="c-tag" select="CONST"/>
 150       <xsl:with-param name="m-tag" select="'geq'"/>
 151    </xsl:call-template>
 152 </xsl:template>
 153
 154 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con']" mode="pure">
 155    <xsl:call-template name="mk-mml-infix">
 156       <xsl:with-param name="c-tag" select="CONST"/>
 157       <xsl:with-param name="m-tag" select="'gt'"/>
 158    </xsl:call-template>
 159 </xsl:template>
 160
 161 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rplus.con']" mode="pure">
 162    <xsl:call-template name="mk-mml-infix">
 163       <xsl:with-param name="c-tag" select="CONST"/>
 164       <xsl:with-param name="m-tag" select="'plus'"/>
 165    </xsl:call-template>
 166 </xsl:template>
 167
 168 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rminus.con']" mode="pure">
 169    <xsl:call-template name="mk-mml-infix">
 170       <xsl:with-param name="c-tag" select="CONST"/>
 171       <xsl:with-param name="m-tag" select="'minus'"/>
 172    </xsl:call-template>
 173 </xsl:template>
 174
 175 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rmult.con']" mode="pure">
 176    <xsl:call-template name="mk-mml-infix">
 177       <xsl:with-param name="c-tag" select="CONST"/>
 178       <xsl:with-param name="m-tag" select="'times'"/>
 179    </xsl:call-template>
 180 </xsl:template>
 181
 182 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rdiv.con']" mode="pure">
 183    <xsl:call-template name="mk-mml-infix">
 184       <xsl:with-param name="c-tag" select="CONST"/>
 185       <xsl:with-param name="m-tag" select="'divide'"/>
 186    </xsl:call-template>
 187 </xsl:template>
 188
 189 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con']" mode="pure">
 190    <xsl:call-template name="mk-mml-infix">
 191       <xsl:with-param name="c-tag" select="CONST"/>
 192       <xsl:with-param name="m-tag" select="'min'"/>
 193    </xsl:call-template>
 194 </xsl:template>
 195
 196 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmax.con']" mode="pure">
 197    <xsl:call-template name="mk-mml-infix">
 198       <xsl:with-param name="c-tag" select="CONST"/>
 199       <xsl:with-param name="m-tag" select="'max'"/>
 200    </xsl:call-template>
 201 </xsl:template>
 202
 203 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rfunctions/pow.con']" mode="pure">
 204    <xsl:call-template name="mk-mml-infix">
 205       <xsl:with-param name="c-tag" select="CONST"/>
 206       <xsl:with-param name="m-tag" select="'power'"/>
 207    </xsl:call-template>
 208 </xsl:template>
 209
 210 <!-- LIMIT -->
 211
 212 <xsl:template match="APPLY[CONST[
 213  attribute::uri='cic:/Coq/Reals/Rlimit/limit1_in.con']]" mode="pure">
 214     <xsl:choose>
 215      <xsl:when test="count(child::*) = 5">
 216       <m:apply>
 217        <m:eq/>
 218        <xsl:choose>
 219         <xsl:when test="name(*[2]) = 'LAMBDA'">
 220          <m:apply helm:xref="{@id}">
 221           <m:limit>
 222            <xsl:attribute name="definitionURL">
 223             <xsl:value-of select="CONST/@uri"/>
 224            </xsl:attribute>
 225            <xsl:attribute name="helm:xref">
 226             <xsl:value-of select="CONST/@id"/>
 227            </xsl:attribute>
 228           </m:limit>
 229           <m:bvar>
 230            <m:ci>
 231             <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template>
 232            </m:ci>
 233           </m:bvar>
 234           <m:lowlimit>
 235            <xsl:apply-templates select="*[5]" mode="noannot"/>
 236           </m:lowlimit>
 237           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
 238          </m:apply>
 239         </xsl:when>
 240         <xsl:otherwise>
 241          <m:apply helm:xref="{@id}">
 242           <m:limit>
 243             <xsl:attribute name="definitionURL">
 244              <xsl:value-of select="CONST/@uri"/>
 245             </xsl:attribute>
 246             <xsl:attribute name="helm:xref">
 247              <xsl:value-of select="CONST/@id"/>
 248             </xsl:attribute>
 249            </m:limit>
 250           <m:bvar>
 251            <m:ci>$x</m:ci>
 252           </m:bvar>
 253           <m:lowlimit>
 254            <xsl:apply-templates select="*[5]" mode="noannot"/>
 255           </m:lowlimit>
 256           <m:apply>
 257            <m:csymbol>app</m:csymbol>
 258            <xsl:apply-templates select="*[2]" mode="noannot"/>
 259            <m:ci>$x</m:ci>
 260           </m:apply>
 261          </m:apply>
 262         </xsl:otherwise>
 263        </xsl:choose>
 264        <xsl:apply-templates select="*[4]" mode="noannot"/>
 265       </m:apply>
 266      </xsl:when>
 267      <xsl:otherwise>
 268       <xsl:apply-imports/>
 269      </xsl:otherwise>
 270     </xsl:choose>
 271 </xsl:template>
 272
 273 <!-- DIFFERENTIATION -->
 274
 275 <xsl:template match="APPLY[CONST[
 276  attribute::uri='cic:/Coq/Reals/Rderiv/D_in.con']]" mode="pure">
 277     <xsl:choose>
 278      <xsl:when test="count(child::*) = 4">
 279       <m:apply>
 280        <m:eq/>
 281        <xsl:choose>
 282         <xsl:when test="name(*[2]) = 'LAMBDA'">
 283          <m:apply helm:xref="{@id}">
 284           <m:diff>
 285            <xsl:attribute name="definitionURL">
 286             <xsl:value-of select="CONST/@uri"/>
 287            </xsl:attribute>
 288            <xsl:attribute name="helm:xref">
 289             <xsl:value-of select="CONST/@id"/>
 290            </xsl:attribute>
 291           </m:diff>
 292           <m:bvar>
 293            <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA[1]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 294           </m:bvar>
 295           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
 296          </m:apply>
 297         </xsl:when>
 298         <xsl:otherwise>
 299          <m:apply helm:xref="{@id}">
 300           <m:diff/>
 301           <m:bvar>
 302            <m:ci>$x</m:ci>
 303           </m:bvar>
 304           <m:apply>
 305            <m:csymbol>app</m:csymbol>
 306            <xsl:apply-templates select="*[2]" mode="noannot"/>
 307            <m:ci>$x</m:ci>
 308           </m:apply>
 309          </m:apply>
 310         </xsl:otherwise>
 311        </xsl:choose>
 312        <xsl:apply-templates select="*[4]" mode="noannot"/>
 313       </m:apply>
 314      </xsl:when>
 315      <xsl:otherwise>
 316       <xsl:apply-imports/>
 317      </xsl:otherwise>
 318     </xsl:choose>
 319 </xsl:template>
 320
 321 </xsl:stylesheet>
 322
 323