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