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