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="mkmml-op-noannot">
 135       <xsl:with-param name="arity" select="2"/>
 136       <xsl:with-param name="c-tag" select="CONST"/>
 137       <xsl:with-param name="m-tag" select="'leq'"/>
 138    </xsl:call-template>
 139 </xsl:template>
 140
 141 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rlt.con']" mode="pure">
 142    <xsl:call-template name="mkmml-op-noannot">
 143       <xsl:with-param name="arity" select="2"/>
 144       <xsl:with-param name="c-tag" select="CONST"/>
 145       <xsl:with-param name="m-tag" select="'lt'"/>
 146    </xsl:call-template>
 147 </xsl:template>
 148
 149 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con']" mode="pure">
 150    <xsl:call-template name="mkmml-op-noannot">
 151       <xsl:with-param name="arity" select="2"/>
 152       <xsl:with-param name="c-tag" select="CONST"/>
 153       <xsl:with-param name="m-tag" select="'geq'"/>
 154    </xsl:call-template>
 155 </xsl:template>
 156
 157 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con']" mode="pure">
 158    <xsl:call-template name="mkmml-op-noannot">
 159       <xsl:with-param name="arity" select="2"/>
 160       <xsl:with-param name="c-tag" select="CONST"/>
 161       <xsl:with-param name="m-tag" select="'gt'"/>
 162    </xsl:call-template>
 163 </xsl:template>
 164
 165 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rplus.con']" mode="pure">
 166    <xsl:call-template name="mkmml-op-noannot">
 167       <xsl:with-param name="arity" select="2"/>
 168       <xsl:with-param name="c-tag" select="CONST"/>
 169       <xsl:with-param name="m-tag" select="'plus'"/>
 170    </xsl:call-template>
 171 </xsl:template>
 172
 173 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rminus.con']" mode="pure">
 174    <xsl:call-template name="mkmml-op-noannot">
 175       <xsl:with-param name="arity" select="2"/>
 176       <xsl:with-param name="c-tag" select="CONST"/>
 177       <xsl:with-param name="m-tag" select="'minus'"/>
 178    </xsl:call-template>
 179 </xsl:template>
 180
 181 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rmult.con']" mode="pure">
 182    <xsl:call-template name="mkmml-op-noannot">
 183       <xsl:with-param name="arity" select="2"/>
 184       <xsl:with-param name="c-tag" select="CONST"/>
 185       <xsl:with-param name="m-tag" select="'times'"/>
 186    </xsl:call-template>
 187 </xsl:template>
 188
 189 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rdiv.con']" mode="pure">
 190    <xsl:call-template name="mkmml-op-noannot">
 191       <xsl:with-param name="arity" select="2"/>
 192       <xsl:with-param name="c-tag" select="CONST"/>
 193       <xsl:with-param name="m-tag" select="'divide'"/>
 194    </xsl:call-template>
 195 </xsl:template>
 196
 197 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con']" mode="pure">
 198    <xsl:call-template name="mkmml-op-noannot">
 199       <xsl:with-param name="arity" select="2"/>
 200       <xsl:with-param name="c-tag" select="CONST"/>
 201       <xsl:with-param name="m-tag" select="'min'"/>
 202    </xsl:call-template>
 203 </xsl:template>
 204
 205 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmax.con']" mode="pure">
 206    <xsl:call-template name="mkmml-op-noannot">
 207       <xsl:with-param name="arity" select="2"/>
 208       <xsl:with-param name="c-tag" select="CONST"/>
 209       <xsl:with-param name="m-tag" select="'max'"/>
 210    </xsl:call-template>
 211 </xsl:template>
 212
 213 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rfunctions/pow.con']" mode="pure">
 214    <xsl:call-template name="mkmml-op-noannot">
 215       <xsl:with-param name="arity" select="2"/>
 216       <xsl:with-param name="c-tag" select="CONST"/>
 217       <xsl:with-param name="m-tag" select="'power'"/>
 218    </xsl:call-template>
 219 </xsl:template>
 220
 221 <!-- LIMIT -->
 222
 223 <xsl:template match="APPLY[CONST[
 224  attribute::uri='cic:/Coq/Reals/Rlimit/limit1_in.con']]" mode="pure">
 225     <xsl:choose>
 226      <xsl:when test="count(child::*) = 5">
 227       <m:apply>
 228        <m:eq/>
 229        <xsl:choose>
 230         <xsl:when test="name(*[2]) = 'LAMBDA'">
 231          <m:apply helm:xref="{@id}">
 232           <m:limit>
 233            <xsl:attribute name="definitionURL">
 234             <xsl:value-of select="CONST/@uri"/>
 235            </xsl:attribute>
 236            <xsl:attribute name="helm:xref">
 237             <xsl:value-of select="CONST/@id"/>
 238            </xsl:attribute>
 239           </m:limit>
 240           <m:bvar>
 241            <m:ci>
 242             <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>
 243            </m:ci>
 244           </m:bvar>
 245           <m:lowlimit>
 246            <xsl:apply-templates select="*[5]" mode="noannot"/>
 247           </m:lowlimit>
 248           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
 249          </m:apply>
 250         </xsl:when>
 251         <xsl:otherwise>
 252          <m:apply helm:xref="{@id}">
 253           <m:limit>
 254             <xsl:attribute name="definitionURL">
 255              <xsl:value-of select="CONST/@uri"/>
 256             </xsl:attribute>
 257             <xsl:attribute name="helm:xref">
 258              <xsl:value-of select="CONST/@id"/>
 259             </xsl:attribute>
 260            </m:limit>
 261           <m:bvar>
 262            <m:ci>$x</m:ci>
 263           </m:bvar>
 264           <m:lowlimit>
 265            <xsl:apply-templates select="*[5]" mode="noannot"/>
 266           </m:lowlimit>
 267           <m:apply>
 268            <m:csymbol>app</m:csymbol>
 269            <xsl:apply-templates select="*[2]" mode="noannot"/>
 270            <m:ci>$x</m:ci>
 271           </m:apply>
 272          </m:apply>
 273         </xsl:otherwise>
 274        </xsl:choose>
 275        <xsl:apply-templates select="*[4]" mode="noannot"/>
 276       </m:apply>
 277      </xsl:when>
 278      <xsl:otherwise>
 279       <xsl:apply-imports/>
 280      </xsl:otherwise>
 281     </xsl:choose>
 282 </xsl:template>
 283
 284 <!-- DIFFERENTIATION -->
 285
 286 <xsl:template match="APPLY[CONST[
 287  attribute::uri='cic:/Coq/Reals/Rderiv/D_in.con']]" mode="pure">
 288     <xsl:choose>
 289      <xsl:when test="count(child::*) = 4">
 290       <m:apply>
 291        <m:eq/>
 292        <xsl:choose>
 293         <xsl:when test="name(*[2]) = 'LAMBDA'">
 294          <m:apply helm:xref="{@id}">
 295           <m:diff>
 296            <xsl:attribute name="definitionURL">
 297             <xsl:value-of select="CONST/@uri"/>
 298            </xsl:attribute>
 299            <xsl:attribute name="helm:xref">
 300             <xsl:value-of select="CONST/@id"/>
 301            </xsl:attribute>
 302           </m:diff>
 303           <m:bvar>
 304            <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>
 305           </m:bvar>
 306           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
 307          </m:apply>
 308         </xsl:when>
 309         <xsl:otherwise>
 310          <m:apply helm:xref="{@id}">
 311           <m:diff/>
 312           <m:bvar>
 313            <m:ci>$x</m:ci>
 314           </m:bvar>
 315           <m:apply>
 316            <m:csymbol>app</m:csymbol>
 317            <xsl:apply-templates select="*[2]" mode="noannot"/>
 318            <m:ci>$x</m:ci>
 319           </m:apply>
 320          </m:apply>
 321         </xsl:otherwise>
 322        </xsl:choose>
 323        <xsl:apply-templates select="*[4]" mode="noannot"/>
 324       </m:apply>
 325      </xsl:when>
 326      <xsl:otherwise>
 327       <xsl:apply-imports/>
 328      </xsl:otherwise>
 329     </xsl:choose>
 330 </xsl:template>
 331
 332 </xsl:stylesheet>
 333
 334