helm/style/drop_coercions.xsl

   1 <?xml version="1.0"?>
   2 <!-- Copyright (C) 2000, HELM Team                                     -->
   3 <!--                                                                   -->
   4 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   5 <!-- Library of Mathematics, developed at the Computer Science         -->
   6 <!-- Department, University of Bologna, Italy.                         -->
   7 <!--                                                                   -->
   8 <!-- HELM is free software; you can redistribute it and/or             -->
   9 <!-- modify it under the terms of the GNU General Public License       -->
  10 <!-- as published by the Free Software Foundation; either version 2    -->
  11 <!-- of the License, or (at your option) any later version.            -->
  12 <!--                                                                   -->
  13 <!-- HELM is distributed in the hope that it will be useful,           -->
  14 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  15 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  16 <!-- GNU General Public License for more details.                      -->
  17 <!--                                                                   -->
  18 <!-- You should have received a copy of the GNU General Public License -->
  19 <!-- along with HELM; if not, write to the Free Software               -->
  20 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  21 <!-- MA  02111-1307, USA.                                              -->
  22 <!--                                                                   -->
  23 <!-- For details, see the HELM World-Wide-Web page,                    -->
  24 <!-- http://cs.unibo.it/helm/.                                         -->
  25
  26 <!--******************************************************************-->
  27 <!-- Coercions                                                        -->
  28 <!-- First draft: March 20 2001, Andrea Asperti                       -->
  29 <!--******************************************************************-->
  30
  31 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
  32
  33 <!-- ************************** LAMBDA ****************************** -->
  34
  35 <xsl:param name="CICURI" select="''"/>
  36 <xsl:param name="getterURL" select="''"/>
  37 <xsl:include href="getter.xsl"/>
  38 <xsl:include href="params.xsl"/>
  39
  40 <!-- coercions -->
  41
  42 <xsl:template match="APPLY[CONST[position()='1' and
  43          (@uri='cic:/Algebra/CSemiGroups/csg_crr.con' or
  44           @uri='cic:/Algebra/CMonoids/cm_crr.con' or
  45           @uri='cic:/Algebra/CGroups/cg_crr.con' or
  46           @uri='cic:/Algebra/CRings/cr_crr.con' or
  47           @uri='cic:/Algebra/CFields/cf_crr.con' or
  48           @uri='cic:/Algebra/COrdFields/cof_crr.con' or
  49           @uri='cic:/Algebra/CReals/crl_crr.con')]]">
  50   <xsl:apply-templates select="*[position()=last()]"/>
  51 </xsl:template>
  52
  53 <xsl:template match="APPLY[CONST[position()='1' and
  54    @uri='cic:/Algebra/CSetoids/CSetoid_functions/csf_fun.con']]">
  55      <xsl:variable name="no_params">
  56       <xsl:call-template name="get_no_params">
  57        <xsl:with-param name="first_uri" select="$CICURI"/>
  58        <xsl:with-param name="second_uri" select="CONST[1]/@uri"/>
  59       </xsl:call-template>
  60      </xsl:variable>
  61     <xsl:choose>
  62      <xsl:when test="(count(child::*) - number($no_params)) = 3">
  63       <xsl:choose>
  64        <xsl:when test="name(*[2+$no_params])='APPLY'">
  65         <APPLY id="{@id}" sort="{@sort}">
  66          <xsl:apply-templates select="*[2+$no_params]/*"/>
  67          <xsl:apply-templates select="*[3+$no_params]"/>
  68         </APPLY>
  69        </xsl:when>
  70        <xsl:otherwise>
  71         <APPLY id="{@id}" sort="{@sort}">
  72          <xsl:apply-templates select="*[2+$no_params]"/>
  73          <xsl:apply-templates select="*[3+$no_params]"/>
  74         </APPLY>
  75        </xsl:otherwise>
  76       </xsl:choose>
  77      </xsl:when>
  78      <xsl:otherwise>
  79       <APPLY id="{@id}" sort="{@sort}">
  80        <xsl:apply-templates select="*"/>
  81       </APPLY>
  82      </xsl:otherwise>
  83     </xsl:choose>
  84 </xsl:template>
  85
  86 <xsl:template match="APPLY[CONST[position()='1' and
  87    @uri='cic:/Algebra/CSetoids/CSetoid_functions/csbf_fun.con']]">
  88      <xsl:variable name="no_params">
  89       <xsl:call-template name="get_no_params">
  90        <xsl:with-param name="first_uri" select="$CICURI"/>
  91        <xsl:with-param name="second_uri" select="CONST[1]/@uri"/>
  92       </xsl:call-template>
  93      </xsl:variable>
  94     <xsl:choose>
  95      <xsl:when test="(count(child::*) - number($no_params)) = 4">
  96       <xsl:choose>
  97        <xsl:when test="name(*[2+$no_params])='APPLY'">
  98         <APPLY id="{@id}" sort="{@sort}">
  99          <xsl:apply-templates select="*[2+$no_params]/*"/>
 100          <xsl:apply-templates select="*[3+$no_params]"/>
 101          <xsl:apply-templates select="*[4+$no_params]"/>
 102         </APPLY>
 103        </xsl:when>
 104        <xsl:otherwise>
 105         <APPLY id="{@id}" sort="{@sort}">
 106          <xsl:apply-templates select="*[2+$no_params]"/>
 107          <xsl:apply-templates select="*[3+$no_params]"/>
 108          <xsl:apply-templates select="*[4+$no_params]"/>
 109         </APPLY>
 110        </xsl:otherwise>
 111       </xsl:choose>
 112      </xsl:when>
 113      <xsl:otherwise>
 114       <APPLY id="{@id}" sort="{@sort}">
 115        <xsl:apply-templates select="*"/>
 116       </APPLY>
 117      </xsl:otherwise>
 118     </xsl:choose>
 119 </xsl:template>
 120
 121 <xsl:template match="APPLY[CONST[position()='1' and
 122    @uri='cic:/Algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
 123      <xsl:variable name="no_params">
 124       <xsl:call-template name="get_no_params">
 125        <xsl:with-param name="first_uri" select="$CICURI"/>
 126        <xsl:with-param name="second_uri" select="CONST[1]/@uri"/>
 127       </xsl:call-template>
 128      </xsl:variable>
 129     <xsl:choose>
 130      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 131       <xsl:choose>
 132        <xsl:when test="name(*[2+$no_params])='APPLY'">
 133         <APPLY id="{@id}" sort="{@sort}">
 134          <xsl:apply-templates select="*[2+$no_params]/*"/>
 135          <xsl:apply-templates select="*[3+$no_params]"/>
 136          <xsl:apply-templates select="*[4+$no_params]"/>
 137         </APPLY>
 138        </xsl:when>
 139        <xsl:otherwise>
 140         <APPLY id="{@id}" sort="{@sort}">
 141          <xsl:apply-templates select="*[2+$no_params]"/>
 142          <xsl:apply-templates select="*[3+$no_params]"/>
 143          <xsl:apply-templates select="*[4+$no_params]"/>
 144         </APPLY>
 145        </xsl:otherwise>
 146       </xsl:choose>
 147      </xsl:when>
 148      <xsl:otherwise>
 149       <APPLY id="{@id}" sort="{@sort}">
 150        <xsl:apply-templates select="*"/>
 151       </APPLY>
 152      </xsl:otherwise>
 153     </xsl:choose>
 154 </xsl:template>
 155
 156 <xsl:template match="APPLY[CONST[position()='1' and
 157    @uri='cic:/Algebra/CRings/nat_injection/nring.con']]">
 158      <xsl:variable name="no_params">
 159       <xsl:call-template name="get_no_params">
 160        <xsl:with-param name="first_uri" select="$CICURI"/>
 161        <xsl:with-param name="second_uri" select="CONST[1]/@uri"/>
 162       </xsl:call-template>
 163      </xsl:variable>
 164     <xsl:choose>
 165      <xsl:when test="(count(child::*) - number($no_params)) = 2">
 166       <xsl:apply-templates select="*[2+$no_params]"/>
 167      </xsl:when>
 168      <xsl:otherwise>
 169       <APPLY id="{@id}" sort="{@sort}">
 170        <xsl:apply-templates select="*"/>
 171       </APPLY>
 172      </xsl:otherwise>
 173     </xsl:choose>
 174 </xsl:template>
 175
 176 <xsl:template match = "/|*">
 177   <xsl:copy>
 178    <xsl:copy-of select="@*"/>
 179    <xsl:apply-templates select="*"/>
 180   </xsl:copy>
 181 </xsl:template>
 182
 183
 184 </xsl:stylesheet>