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         </m:minus>
 125         <xsl:attribute name="helm:xref">
 126          <xsl:value-of select="CONST/@id"/>
 127         </xsl:attribute>
 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           <m:bvar>
 236            <m:ci>$x</m:ci>
 237           </m:bvar>
 238           <m:lowlimit>
 239            <xsl:apply-templates select="*[5]" mode="noannot"/>
 240           </m:lowlimit>
 241           <m:apply>
 242            <m:csymbol>app</m:csymbol>
 243            <xsl:apply-templates select="*[2]" mode="noannot"/>
 244            <m:ci>$x</m:ci>
 245           </m:apply>
 246          </m:apply>
 247         </xsl:otherwise>
 248        </xsl:choose>
 249        <xsl:apply-templates select="*[4]" mode="noannot"/>
 250       </m:apply>
 251      </xsl:when>
 252      <xsl:otherwise>
 253       <xsl:apply-imports/>
 254      </xsl:otherwise>
 255     </xsl:choose>
 256 </xsl:template>
 257
 258 <!-- DIFFERENTIATION -->
 259
 260 <xsl:template match="APPLY[CONST[
 261  attribute::uri='cic:/Coq/Reals/Rderiv/D_in.con']]" mode="pure">
 262     <xsl:choose>
 263      <xsl:when test="count(child::*) = 4">
 264       <m:apply>
 265        <m:eq/>
 266        <xsl:choose>
 267         <xsl:when test="name(*[2]) = 'LAMBDA'">
 268          <m:apply helm:xref="{@id}">
 269           <m:diff >
 270            <xsl:attribute name="definitionURL">
 271             <xsl:value-of select="CONST/@uri"/>
 272            </xsl:attribute>
 273            <xsl:attribute name="helm:xref">
 274             <xsl:value-of select="CONST/@id"/>
 275            </xsl:attribute>
 276           </m:diff>
 277           <m:bvar>
 278            <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>
 279           </m:bvar>
 280           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
 281          </m:apply>
 282         </xsl:when>
 283         <xsl:otherwise>
 284          <m:apply helm:xref="{@id}">
 285           <m:diff/>
 286           <m:bvar>
 287            <m:ci>$x</m:ci>
 288           </m:bvar>
 289           <m:apply>
 290            <m:csymbol>app</m:csymbol>
 291            <xsl:apply-templates select="*[2]" mode="noannot"/>
 292            <m:ci>$x</m:ci>
 293           </m:apply>
 294          </m:apply>
 295         </xsl:otherwise>
 296        </xsl:choose>
 297        <xsl:apply-templates select="*[4]" mode="noannot"/>
 298       </m:apply>
 299      </xsl:when>
 300      <xsl:otherwise>
 301       <xsl:apply-imports/>
 302      </xsl:otherwise>
 303     </xsl:choose>
 304 </xsl:template>
 305
 306 </xsl:stylesheet>