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