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