helm/style/ring.xsl

   1 <?xml version="1.0"?>
   2
   3 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
   4                               xmlns:m="http://www.w3.org/1998/Math/MathML"
   5                               xmlns:helm="http://www.cs.unibo.it/helm"
   6                               xmlns:xlink="http://www.w3.org/1999/xlink">
   7
   8 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con']" mode="pure">
   9    <xsl:choose>
  10       <xsl:when test="count(child::*) > 1">
  11          <m:apply helm:xref="{@id}">
  12             <m:csymbol>app</m:csymbol>
  13             <xsl:apply-templates mode="noannot" select="*[1]"/>
  14             <m:ci>...</m:ci>
  15          </m:apply>
  16       </xsl:when>
  17       <xsl:otherwise>
  18          <xsl:apply-imports/>
  19       </xsl:otherwise>
  20    </xsl:choose>
  21 </xsl:template>
  22
  23 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con']" mode="pure">
  24    <xsl:choose>
  25       <xsl:when test="count(child::*) = 9">
  26          <xsl:call-template name="start-interp">
  27             <xsl:with-param name="rtree" select="*[9]"/>
  28             <xsl:with-param name="atree" select="*[8]"/>
  29          </xsl:call-template>
  30       </xsl:when>
  31       <xsl:otherwise>
  32          <xsl:apply-imports/>
  33       </xsl:otherwise>
  34    </xsl:choose>
  35 </xsl:template>
  36
  37 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con']" mode="pure">
  38    <xsl:choose>
  39       <xsl:when test="count(child::*) = 9 and *[APPLY and position()=9]
  40                       [CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con']">
  41          <m:apply helm:xref="{@id}">
  42             <m:csymbol>app</m:csymbol>
  43             <xsl:apply-templates mode="noannot" select="*[9]/*[1]"/>
  44             <xsl:call-template name="start-interp">
  45                <xsl:with-param name="rtree" select="*[9]/*[2]"/>
  46                <xsl:with-param name="atree" select="*[8]"/>
  47             </xsl:call-template>
  48          </m:apply>
  49       </xsl:when>
  50       <xsl:otherwise>
  51          <xsl:apply-imports/>
  52       </xsl:otherwise>
  53    </xsl:choose>
  54 </xsl:template>
  55
  56 <!-- **************************  abstract polinomials rendering ************************ -->
  57
  58 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
  59                                     and @noConstr='1']]" mode="interp">
  60    <xsl:param name="atree"/>
  61    <xsl:apply-templates select="*[2]" mode="interp">
  62       <xsl:with-param name="atree" select="$atree"/>
  63    </xsl:apply-templates>
  64 </xsl:template>
  65
  66 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
  67                                     and @noConstr='2']]" mode="interp">
  68    <xsl:param name="atree"/>
  69    <xsl:apply-templates mode="noannot" select="."/>
  70 </xsl:template>
  71
  72 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
  73                                     and @noConstr='3']]" mode="interp">
  74    <xsl:param name="atree"/>
  75    <xsl:apply-templates mode="noannot" select="."/>
  76 </xsl:template>
  77
  78 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
  79                                     and @noConstr='4']]" mode="interp">
  80    <xsl:param name="atree"/>
  81    <xsl:call-template name="mkmml-op-interp">
  82       <xsl:with-param name="arity" select="2"/>
  83       <xsl:with-param name="c-tag" select="MUTCONSTRUCT"/>
  84       <xsl:with-param name="m-tag" select="'plus'"/>
  85       <xsl:with-param name="atree" select="$atree"/>
  86    </xsl:call-template>
  87 </xsl:template>
  88
  89 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
  90                                     and @noConstr='5']]" mode="interp">
  91    <xsl:param name="atree"/>
  92    <xsl:call-template name="mkmml-op-interp">
  93       <xsl:with-param name="arity" select="2"/>
  94       <xsl:with-param name="c-tag" select="MUTCONSTRUCT"/>
  95       <xsl:with-param name="m-tag" select="'times'"/>
  96       <xsl:with-param name="atree" select="$atree"/>
  97    </xsl:call-template>
  98 </xsl:template>
  99
 100 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
 101                                     and @noConstr='6']]" mode="interp">
 102    <xsl:param name="atree"/>
 103    <xsl:call-template name="mkmml-op-interp">
 104       <xsl:with-param name="arity" select="1"/>
 105       <xsl:with-param name="c-tag" select="MUTCONSTRUCT"/>
 106       <xsl:with-param name="m-tag" select="'minus'"/>
 107       <xsl:with-param name="atree" select="$atree"/>
 108    </xsl:call-template>
 109 </xsl:template>
 110
 111 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind'
 112                                     and @noConstr='1']]" mode="interp">
 113    <xsl:param name="atree"/>
 114    <xsl:apply-templates select="*[2]" mode="interp">
 115       <xsl:with-param name="atree" select="$atree/*[4]"/>
 116    </xsl:apply-templates>
 117 </xsl:template>
 118
 119 <xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind'
 120                                     and @noConstr='2']]" mode="interp">
 121    <xsl:param name="atree"/>
 122    <xsl:apply-templates select="*[2]" mode="interp">
 123       <xsl:with-param name="atree" select="$atree/*[5]"/>
 124    </xsl:apply-templates>
 125 </xsl:template>
 126
 127 <xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind'
 128                               and @noConstr='3']" mode="interp">
 129    <xsl:param name="atree"/>
 130    <xsl:apply-templates select="$atree/*[3]" mode="noannot"/>
 131 </xsl:template>
 132
 133 </xsl:stylesheet>