helm/style/style_prima_del_linguaggio_naturale/reals.xsl

   1 <?xml version="1.0"?>
   2
   3 <!--******************************************************************-->
   4 <!-- Reals                                                            -->
   5 <!-- First draft: April 3 2000                                        -->
   6 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
   7 <!--******************************************************************-->
   8
   9 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  10                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  11                               xmlns:helm="http://www.cs.unibo.it/helm"
  12                               xmlns:xlink="http://www.w3.org/1999/xlink">
  13
  14 <!--******************************************************************-->
  15 <!-- Variable containing the absolute path of the CIC file            -->
  16 <!--******************************************************************-->
  17
  18 <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>
  19
  20 <!-- ************************* LOGIC *********************************-->
  21
  22 <!-- REALS -->
  23
  24 <!--
  25 <xsl:template match="CONST[attribute::uri='cic:/coq/REALS/Raxioms/R.con']" mode="noannot">
  26  <m:reals/>
  27 </xsl:template>
  28 -->
  29
  30 <!-- 0 e 1 -->
  31
  32 <xsl:template match="CONST[attribute::uri='cic:/coq/REALS/Raxioms/R0.con']" mode="noannot">
  33  <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
  34 </xsl:template>
  35
  36 <xsl:template match="CONST[attribute::uri='cic:/coq/REALS/Raxioms/R1.con']" mode="noannot">
  37  <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
  38 </xsl:template>
  39
  40
  41
  42 <!-- Unary Operations -->
  43
  44 <xsl:template match="APPLY[CONST[
  45  attribute::uri='cic:/coq/REALS/Raxioms/Ropp.con' or
  46  attribute::uri='cic:/coq/REALS/Rbasic_fun/Rabsolu.con' or
  47  attribute::uri='cic:/coq/REALS/Rfunctions/fact.con' or
  48  attribute::uri='cic:/coq/REALS/Rbase/Rsqr.con']]" mode="noannot">
  49     <xsl:choose>
  50      <xsl:when test="count(child::*) = 2">
  51       <xsl:variable name="elem">
  52        <xsl:choose>
  53         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Ropp.con'">
  54          <xsl:value-of select="'minus'"/>
  55         </xsl:when>
  56         <xsl:when test="CONST/@uri='cic:/coq/REALS/Rbasic_fun/Rabsolu.con'">
  57          <xsl:value-of select="'abs'"/>
  58         </xsl:when>
  59         <xsl:when test="CONST/@uri='cic:/coq/REALS/Rfunctions/fact.con'">
  60          <xsl:value-of select="'factorial'"/>
  61         </xsl:when>
  62         <xsl:when test="CONST/@uri='cic:/coq/REALS/Rbase/Rsqr.con'">
  63          <xsl:value-of select="'root'"/>
  64         </xsl:when>
  65        </xsl:choose>
  66       </xsl:variable>
  67       <m:apply helm:xref="{@id}">
  68        <xsl:element name="{concat('m:',$elem)}">
  69         <xsl:attribute name="definitionURL">
  70          <xsl:value-of select="CONST/@uri"/>
  71         </xsl:attribute>
  72         <xsl:attribute name="helm:xref">
  73          <xsl:value-of select="CONST/@id"/>
  74         </xsl:attribute>
  75        </xsl:element>
  76        <xsl:apply-templates select="*[2]" mode="noannot"/>
  77       </m:apply>
  78      </xsl:when>
  79      <xsl:otherwise>
  80       <xsl:apply-imports/>
  81      </xsl:otherwise>
  82     </xsl:choose>
  83 </xsl:template>
  84
  85 <xsl:template match="APPLY[CONST[
  86  attribute::uri='cic:/coq/REALS/Raxioms/Rinv.con']]" mode="noannot">
  87     <xsl:choose>
  88      <xsl:when test="count(child::*) = 2">
  89       <m:apply helm:xref="{@id}">
  90        <m:power/>
  91        <xsl:apply-templates select="*[2]" mode="noannot"/>
  92        <m:apply>
  93         <m:minus>
  94          <xsl:attribute name="definitionURL">
  95           <xsl:value-of select="CONST/@uri"/>
  96          </xsl:attribute>
  97         </m:minus>
  98         <xsl:attribute name="helm:xref">
  99          <xsl:value-of select="CONST/@id"/>
 100         </xsl:attribute>
 101         <m:cn>1</m:cn>
 102        </m:apply>
 103       </m:apply>
 104      </xsl:when>
 105      <xsl:otherwise>
 106       <xsl:apply-imports/>
 107      </xsl:otherwise>
 108     </xsl:choose>
 109 </xsl:template>
 110
 111 <!-- Binary Operations and Relations -->
 112
 113 <xsl:template match="APPLY[CONST[
 114  attribute::uri='cic:/coq/REALS/Raxioms/Rplus.con' or
 115  attribute::uri='cic:/coq/REALS/Raxioms/Rminus.con' or
 116  attribute::uri='cic:/coq/REALS/Raxioms/Rmult.con' or
 117  attribute::uri='cic:/coq/REALS/Raxioms/Rle.con' or
 118  attribute::uri='cic:/coq/REALS/Raxioms/Rlt.con' or
 119  attribute::uri='cic:/coq/REALS/Raxioms/Rge.con' or
 120  attribute::uri='cic:/coq/REALS/Raxioms/Rgt.con' or
 121  attribute::uri='cic:/coq/REALS/Rbasic_fun/Rmin.con' or
 122  attribute::uri='cic:/coq/REALS/Rfunctions/pow.con']]" mode="noannot">
 123     <xsl:choose>
 124      <xsl:when test="count(child::*) = 3">
 125       <xsl:variable name="elem">
 126        <xsl:choose>
 127         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rplus.con'">
 128          <xsl:value-of select="'plus'"/>
 129         </xsl:when>
 130         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rminus.con'">
 131          <xsl:value-of select="'minus'"/>
 132         </xsl:when>
 133         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rmult.con'">
 134          <xsl:value-of select="'times'"/>
 135         </xsl:when>
 136         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rle.con'">
 137          <xsl:value-of select="'leq'"/>
 138         </xsl:when>
 139         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rlt.con'">
 140          <xsl:value-of select="'lt'"/>
 141         </xsl:when>
 142         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rge.con'">
 143          <xsl:value-of select="'geq'"/>
 144         </xsl:when>
 145         <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rgt.con'">
 146          <xsl:value-of select="'gt'"/>
 147         </xsl:when>
 148         <xsl:when test="CONST/@uri='cic:/coq/REALS/Rbasic_fun/Rmin.con'">
 149          <xsl:value-of select="'min'"/>
 150         </xsl:when>
 151         <xsl:when test="CONST/@uri='cic:/coq/REALS/Rfunctions/pow.con'">
 152          <xsl:value-of select="'power'"/>
 153         </xsl:when>
 154        </xsl:choose>
 155       </xsl:variable>
 156       <m:apply helm:xref="{@id}">
 157        <xsl:element name="{concat('m:',$elem)}">
 158         <xsl:attribute name="definitionURL">
 159          <xsl:value-of select="CONST/@uri"/>
 160         </xsl:attribute>
 161         <xsl:attribute name="helm:xref">
 162          <xsl:value-of select="CONST/@id"/>
 163         </xsl:attribute>
 164        </xsl:element>
 165        <xsl:apply-templates select="*[2]" mode="noannot"/>
 166        <xsl:apply-templates select="*[3]" mode="noannot"/>
 167       </m:apply>
 168      </xsl:when>
 169      <xsl:otherwise>
 170       <xsl:apply-imports/>
 171      </xsl:otherwise>
 172     </xsl:choose>
 173 </xsl:template>
 174
 175 <!-- LIMIT -->
 176
 177 <xsl:template match="APPLY[CONST[
 178  attribute::uri='cic:/coq/REALS/Rlimit/limit1_in.con']]" mode="noannot">
 179     <xsl:choose>
 180      <xsl:when test="count(child::*) = 5">
 181       <m:apply>
 182        <m:eq/>
 183        <xsl:choose>
 184         <xsl:when test="name(*[2]) = 'LAMBDA'">
 185          <m:apply helm:xref="{@id}">
 186           <m:limit>
 187            <xsl:attribute name="definitionURL">
 188             <xsl:value-of select="CONST/@uri"/>
 189            </xsl:attribute>
 190            <xsl:attribute name="helm:xref">
 191             <xsl:value-of select="CONST/@id"/>
 192            </xsl:attribute>
 193           </m:limit>
 194           <m:bvar>
 195            <m:ci><xsl:value-of select="LAMBDA/target/@binder"/></m:ci>
 196           </m:bvar>
 197           <m:lowlimit>
 198            <xsl:apply-templates select="*[5]" mode="noannot"/>
 199           </m:lowlimit>
 200           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
 201          </m:apply>
 202         </xsl:when>
 203         <xsl:otherwise>
 204          <m:apply helm:xref="{@id}">
 205           <m:limit/>
 206           <m:bvar>
 207            <m:ci>$x</m:ci>
 208           </m:bvar>
 209           <m:lowlimit>
 210            <xsl:apply-templates select="*[5]" mode="noannot"/>
 211           </m:lowlimit>
 212           <m:apply>
 213            <m:csymbol>app</m:csymbol>
 214            <xsl:apply-templates select="*[2]" mode="noannot"/>
 215            <m:ci>$x</m:ci>
 216           </m:apply>
 217          </m:apply>
 218         </xsl:otherwise>
 219        </xsl:choose>
 220        <xsl:apply-templates select="*[4]" mode="noannot"/>
 221       </m:apply>
 222      </xsl:when>
 223      <xsl:otherwise>
 224       <xsl:apply-imports/>
 225      </xsl:otherwise>
 226     </xsl:choose>
 227 </xsl:template>
 228
 229 <!-- DIFFERENTIATION -->
 230
 231 <xsl:template match="APPLY[CONST[
 232  attribute::uri='cic:/coq/REALS/Rderiv/D_in.con']]" mode="noannot">
 233     <xsl:choose>
 234      <xsl:when test="count(child::*) = 4">
 235       <m:apply>
 236        <m:eq/>
 237        <xsl:choose>
 238         <xsl:when test="name(*[2]) = 'LAMBDA'">
 239          <m:apply helm:xref="{@id}">
 240           <m:diff >
 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:diff>
 248           <m:bvar>
 249            <m:ci><xsl:value-of select="LAMBDA[1]/target/@binder"/></m:ci>
 250           </m:bvar>
 251           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
 252          </m:apply>
 253         </xsl:when>
 254         <xsl:otherwise>
 255          <m:apply helm:xref="{@id}">
 256           <m:diff/>
 257           <m:bvar>
 258            <m:ci>$x</m:ci>
 259           </m:bvar>
 260           <m:apply>
 261            <m:csymbol>app</m:csymbol>
 262            <xsl:apply-templates select="*[2]" mode="noannot"/>
 263            <m:ci>$x</m:ci>
 264           </m:apply>
 265          </m:apply>
 266         </xsl:otherwise>
 267        </xsl:choose>
 268        <xsl:apply-templates select="*[4]" mode="noannot"/>
 269       </m:apply>
 270      </xsl:when>
 271      <xsl:otherwise>
 272       <xsl:apply-imports/>
 273      </xsl:otherwise>
 274     </xsl:choose>
 275 </xsl:template>
 276
 277 </xsl:stylesheet>