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