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