helm/style/algebra.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 <!-- Algebra                                                          -->
  29 <!-- First draft: October 2001                                        -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi          -->
  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
  37
  38 <!-- ************************* ALGEBRA *********************************-->
  39
  40
  41
  42 <!-- 0 and 1 -->
  43
  44 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSemiGroups/csg_unit.con']" mode="pure">
  45  <m:ci definitionURL="{CONST/@uri}" helm:xref="{@id}">0</m:ci>
  46 </xsl:template>
  47
  48 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_one.con']" mode="pure">
  49  <m:ci definitionURL="{CONST/@uri}" helm:xref="{@id}">1</m:ci>
  50 </xsl:template>
  51
  52 <!-- Unary Operations -->
  53
  54 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CGroups/cg_inv.con']" mode="pure">
  55    <xsl:call-template name="mk-mml-op-noannot">
  56       <xsl:with-param name="arity" select="1"/>
  57       <xsl:with-param name="hide" select="1"/>
  58       <xsl:with-param name="c-tag" select="CONST"/>
  59       <xsl:with-param name="m-tag" select="'minus'"/>
  60    </xsl:call-template>
  61 </xsl:template>
  62
  63 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CMetricFields/CMetric_Fields/cmf_abs.con']" mode="pure">
  64    <xsl:call-template name="mk-mml-op-noannot">
  65       <xsl:with-param name="hide" select="1"/>
  66       <xsl:with-param name="c-tag" select="CONST"/>
  67       <xsl:with-param name="m-tag" select="'abs'"/>
  68    </xsl:call-template>
  69 </xsl:template>
  70
  71 <!-- inv (uri errata)
  72 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp.con']" mode="pure">
  73    <xsl:variable name="mbody1">
  74       <xsl:apply-templates select="*[2]" mode="noannot"/>
  75       <xsl:variable name="mbody2">
  76          <m:cn>1</m:cn>
  77       </xsl:variable>
  78       <xsl:call-template name="out-mml-op">
  79          <xsl:with-param name="arity" select="1"/>
  80          <xsl:with-param name="c-tag" select="CONST"/>
  81          <xsl:with-param name="m-tag" select="'minus'"/>
  82          <xsl:with-param name="mbody" select="$mbody2"/>
  83       </xsl:call-template>
  84    </xsl:variable>
  85    <xsl:call-template name="out-mml-op">
  86       <xsl:with-param name="arity" select="1"/>
  87       <xsl:with-param name="c-tag" select="CONST"/>
  88       <xsl:with-param name="m-tag" select="'power'"/>
  89       <xsl:with-param name="mbody" select="$mbody1"/>
  90    </xsl:call-template>
  91 </xsl:template>
  92 -->
  93
  94 <!-- Binary Operations and Relations -->
  95
  96 <!-- setoid equality -->
  97
  98 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSetoids/cs_eq.con']" mode="pure">
  99    <xsl:call-template name="mk-mml-op-noannot">
 100       <xsl:with-param name="hide" select="1"/>
 101       <xsl:with-param name="c-tag" select="CONST"/>
 102       <xsl:with-param name="m-tag" select="'eq'"/>
 103    </xsl:call-template>
 104 </xsl:template>
 105
 106 <!-- apart -->
 107
 108 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSetoids/cs_ap.con']" mode="pure">
 109    <xsl:call-template name="mk-mml-op-noannot">
 110       <xsl:with-param name="hide" select="1"/>
 111       <xsl:with-param name="c-tag" select="CONST"/>
 112       <xsl:with-param name="m-tag" select="'neq'"/>
 113    </xsl:call-template>
 114 </xsl:template>
 115
 116 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/leEq.con']" mode="pure">
 117    <xsl:call-template name="mk-mml-op-noannot">
 118       <xsl:with-param name="hide" select="1"/>
 119       <xsl:with-param name="arity" select="2"/>
 120       <xsl:with-param name="c-tag" select="CONST"/>
 121       <xsl:with-param name="m-tag" select="'leq'"/>
 122    </xsl:call-template>
 123 </xsl:template>
 124
 125 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/cof_less.con']" mode="pure">
 126    <xsl:call-template name="mk-mml-op-noannot">
 127       <xsl:with-param name="hide" select="1"/>
 128       <xsl:with-param name="c-tag" select="CONST"/>
 129       <xsl:with-param name="m-tag" select="'lt'"/>
 130    </xsl:call-template>
 131 </xsl:template>
 132
 133 <!--
 134 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con']" mode="pure">
 135    <xsl:call-template name="mk-mml-op-noannot">
 136       <xsl:with-param name="arity" select="2"/>
 137       <xsl:with-param name="c-tag" select="CONST"/>
 138       <xsl:with-param name="m-tag" select="'geq'"/>
 139    </xsl:call-template>
 140 </xsl:template>
 141
 142 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con']" mode="pure">
 143    <xsl:call-template name="mk-mml-op-noannot">
 144       <xsl:with-param name="arity" select="2"/>
 145       <xsl:with-param name="c-tag" select="CONST"/>
 146       <xsl:with-param name="m-tag" select="'gt'"/>
 147    </xsl:call-template>
 148 </xsl:template>
 149 -->
 150
 151 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_plus.con' or
 152 CONST/@uri='cic:/Algebra/CSemiGroups/csg_op.con']" mode="pure">
 153    <xsl:call-template name="mk-mml-op-noannot">
 154       <xsl:with-param name="hide" select="1"/>
 155       <xsl:with-param name="c-tag" select="CONST"/>
 156       <xsl:with-param name="m-tag" select="'plus'"/>
 157    </xsl:call-template>
 158 </xsl:template>
 159
 160 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_minus.con' or
 161  CONST/@uri='cic:/Algebra/CGroups/cg_minus.con']" mode="pure">
 162    <xsl:call-template name="mk-mml-op-noannot">
 163       <xsl:with-param name="hide" select="1"/>
 164       <xsl:with-param name="c-tag" select="CONST"/>
 165       <xsl:with-param name="m-tag" select="'minus'"/>
 166    </xsl:call-template>
 167 </xsl:template>
 168
 169 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_mult.con']" mode="pure">
 170    <xsl:call-template name="mk-mml-op-noannot">
 171       <xsl:with-param name="hide" select="1"/>
 172       <xsl:with-param name="c-tag" select="CONST"/>
 173       <xsl:with-param name="m-tag" select="'times'"/>
 174    </xsl:call-template>
 175 </xsl:template>
 176
 177 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CFields/cf_div.con']" mode="pure">
 178    <xsl:call-template name="mk-mml-op-noannot">
 179       <xsl:with-param name="arity" select="2"/>
 180       <xsl:with-param name="hide" select="1"/>
 181       <xsl:with-param name="c-tag" select="CONST"/>
 182       <xsl:with-param name="m-tag" select="'divide'"/>
 183    </xsl:call-template>
 184 </xsl:template>
 185
 186 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/Ring_constructions/nzpro.con' and count(*)='4']" mode="pure">
 187    <xsl:apply-templates select="*[3]" mode="pure"/>
 188 </xsl:template>
 189
 190 <!--
 191 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con']" mode="pure">
 192    <xsl:call-template name="mk-mml-op-noannot">
 193       <xsl:with-param name="arity" select="2"/>
 194       <xsl:with-param name="c-tag" select="CONST"/>
 195       <xsl:with-param name="m-tag" select="'min'"/>
 196    </xsl:call-template>
 197 </xsl:template>
 198
 199 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmax.con']" mode="pure">
 200    <xsl:call-template name="mk-mml-op-noannot">
 201       <xsl:with-param name="arity" select="2"/>
 202       <xsl:with-param name="c-tag" select="CONST"/>
 203       <xsl:with-param name="m-tag" select="'max'"/>
 204    </xsl:call-template>
 205 </xsl:template>
 206 -->
 207
 208
 209 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp.con']" mode="pure">
 210    <xsl:variable name="no_params">
 211      <xsl:call-template name="get_no_params">
 212       <xsl:with-param name="first_uri" select="$CICURI"/>
 213       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 214      </xsl:call-template>
 215     </xsl:variable>
 216    <xsl:call-template name="mk-mml-op-noannot">
 217       <xsl:with-param name="hide" select="$no_params"/>
 218       <xsl:with-param name="c-tag" select="CONST"/>
 219       <xsl:with-param name="m-tag" select="'power'"/>
 220    </xsl:call-template>
 221 </xsl:template>
 222
 223 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp_op.con' or CONST/@uri='cic:/Algebra/Expon/Zexp_def/zexp.con']" mode="pure">
 224    <xsl:variable name="no_params">
 225      <xsl:call-template name="get_no_params">
 226       <xsl:with-param name="first_uri" select="$CICURI"/>
 227       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 228      </xsl:call-template>
 229    </xsl:variable>
 230    <xsl:variable name="mbody">
 231     <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
 232     <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
 233    </xsl:variable>
 234    <xsl:call-template name="out-mml-op">
 235       <xsl:with-param name="hide" select="$no_params"/>
 236       <xsl:with-param name="arity" select="2"/>
 237       <xsl:with-param name="c-tag" select="CONST"/>
 238       <xsl:with-param name="m-tag" select="'power'"/>
 239       <xsl:with-param name="mbody" select="$mbody"/>
 240    </xsl:call-template>
 241 </xsl:template>
 242
 243 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/absSmall.con']" mode="pure">
 244    <xsl:variable name="mbody">
 245       <m:apply helm:xref="{@id}">
 246        <m:abs definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 247        <xsl:apply-templates select="*[4]" mode="noannot"/>
 248       </m:apply>
 249       <xsl:apply-templates select="*[3]" mode="noannot"/>
 250    </xsl:variable>
 251    <xsl:call-template name="out-mml-op">
 252       <xsl:with-param name="hide" select="1"/>
 253       <xsl:with-param name="arity" select="2"/>
 254       <xsl:with-param name="c-tag" select="CONST"/>
 255       <xsl:with-param name="m-tag" select="'lt'"/>
 256       <xsl:with-param name="mbody" select="$mbody"/>
 257    </xsl:call-template>
 258 </xsl:template>
 259
 260 <xsl:template match="APPLY[CONST[
 261  attribute::uri='cic:/Algebra/COrdFields/OrdField_Cauchy/seqLimit.con']]" mode="pure">
 262     <xsl:variable name="no_params">
 263      <xsl:call-template name="get_no_params">
 264       <xsl:with-param name="first_uri" select="$CICURI"/>
 265       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 266      </xsl:call-template>
 267     </xsl:variable>
 268     <xsl:choose>
 269      <xsl:when test="count(child::*) = 3+$no_params">
 270       <m:apply helm:xref="{@id}">
 271        <m:eq definitionURL="{CONST/@uri}" helm:xref="{@id}" />
 272        <xsl:choose>
 273         <xsl:when test="name(*[2+$no_params]) = 'LAMBDA'">
 274          <m:apply helm:xref="{CONST/@id}">
 275           <m:limit definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 276           <m:bvar>
 277            <m:ci>
 278             <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>
 279            </m:ci>
 280           </m:bvar>
 281           <m:lowlimit>
 282            <m:infinity/>
 283           </m:lowlimit>
 284           <xsl:apply-templates select="*[2+$no_params]/target/*[1]" mode="noannot"/>
 285          </m:apply>
 286         </xsl:when>
 287         <xsl:otherwise>
 288          <m:apply helm:xref="{CONST/@id}">
 289           <m:limit definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 290           <m:bvar>
 291            <m:ci>$x</m:ci>
 292           </m:bvar>
 293           <m:lowlimit>
 294            <m:infinity/>
 295           </m:lowlimit>
 296           <m:apply>
 297            <m:csymbol>app</m:csymbol>
 298            <xsl:apply-templates select="*[2+$no_params]" 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="*[3+$no_params]" 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:template match="APPLY[CONST[
 314  attribute::uri='cic:/Algebra/CSums/Sums/sum0.con']]" mode="pure">
 315     <xsl:variable name="no_params">
 316      <xsl:call-template name="get_no_params">
 317       <xsl:with-param name="first_uri" select="$CICURI"/>
 318       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 319      </xsl:call-template>
 320     </xsl:variable>
 321     <xsl:choose>
 322      <xsl:when test="count(child::*) = 3+$no_params">
 323        <xsl:choose>
 324         <xsl:when test="name(*[3+$no_params]) = 'LAMBDA'">
 325          <m:apply helm:xref="{CONST/@id}">
 326           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 327           <m:bvar>
 328            <m:ci>
 329             <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>
 330            </m:ci>
 331           </m:bvar>
 332           <m:condition>
 333            <m:apply>
 334             <m:lt/>
 335             <m:ci>
 336              <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>
 337             </m:ci>
 338             <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
 339            </m:apply>
 340           </m:condition>
 341           <xsl:apply-templates select="*[3+$no_params]/target/*[1]" mode="noannot"/>
 342          </m:apply>
 343         </xsl:when>
 344         <xsl:otherwise>
 345          <m:apply helm:xref="{CONST/@id}">
 346           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 347           <m:bvar>
 348            <m:ci>$x</m:ci>
 349           </m:bvar>
 350           <m:condition>
 351            <m:apply>
 352             <m:lt/>
 353             <m:ci>$x</m:ci>
 354             <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
 355            </m:apply>
 356           </m:condition>
 357           <m:apply>
 358            <m:csymbol>app</m:csymbol>
 359            <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 360            <m:ci>$x</m:ci>
 361           </m:apply>
 362          </m:apply>
 363         </xsl:otherwise>
 364        </xsl:choose>
 365      </xsl:when>
 366      <xsl:otherwise>
 367       <xsl:apply-imports/>
 368      </xsl:otherwise>
 369     </xsl:choose>
 370 </xsl:template>
 371
 372 <!-- sum -->
 373 <xsl:template match="APPLY[CONST[
 374  attribute::uri='cic:/Algebra/CSums/Sums/sum.con']]" mode="pure">
 375     <xsl:variable name="no_params">
 376      <xsl:call-template name="get_no_params">
 377       <xsl:with-param name="first_uri" select="$CICURI"/>
 378       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 379      </xsl:call-template>
 380     </xsl:variable>
 381     <xsl:choose>
 382      <xsl:when test="count(child::*) = 4+$no_params">
 383        <xsl:choose>
 384         <xsl:when test="name(*[4+$no_params]) = 'LAMBDA'">
 385          <m:apply helm:xref="{CONST/@id}">
 386           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 387           <m:bvar>
 388            <m:ci>
 389             <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>
 390            </m:ci>
 391           </m:bvar>
 392           <m:lowlimit>
 393            <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
 394           </m:lowlimit>
 395           <m:uplimit>
 396            <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
 397           </m:uplimit>
 398           <xsl:apply-templates select="*[4+$no_params]/target/*[1]" mode="noannot"/>
 399          </m:apply>
 400         </xsl:when>
 401         <xsl:otherwise>
 402          <m:apply helm:xref="{CONST/@id}">
 403           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 404           <m:bvar>
 405            <m:ci>$x</m:ci>
 406           </m:bvar>
 407           <m:lowlimit>
 408            <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
 409           </m:lowlimit>
 410           <m:uplimit>
 411            <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
 412           </m:uplimit>
 413           <m:apply>
 414            <m:csymbol>app</m:csymbol>
 415            <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 416            <m:ci>$x</m:ci>
 417           </m:apply>
 418          </m:apply>
 419         </xsl:otherwise>
 420        </xsl:choose>
 421      </xsl:when>
 422      <xsl:otherwise>
 423       <xsl:apply-imports/>
 424      </xsl:otherwise>
 425     </xsl:choose>
 426 </xsl:template>
 427
 428 <!-- polynomials -->
 429
 430 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CPolynomials/CPoly_CRing_ctd/cpoly_apply_fun.con']" mode="pure">
 431    <xsl:variable name="no_params">
 432      <xsl:call-template name="get_no_params">
 433       <xsl:with-param name="first_uri" select="$CICURI"/>
 434       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 435      </xsl:call-template>
 436     </xsl:variable>
 437     <xsl:choose>
 438      <xsl:when test="count(child::*) = 3+$no_params">
 439       <m:apply>
 440        <m:csymbol>app</m:csymbol>
 441        <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
 442        <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
 443       </m:apply>
 444      </xsl:when>
 445      <xsl:otherwise>
 446       <xsl:apply-imports/>
 447      </xsl:otherwise>
 448     </xsl:choose>
 449 </xsl:template>
 450
 451 </xsl:stylesheet>
 452
 453