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