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">
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">
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]"/>
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">
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()]"/>
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">
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()]"/>
54 <!-- ************************** abstract polinomials rendering ************************ -->
56 <xsl:template match="*" mode="interp">
58 <m:ci>ERROR INTERP:</m:ci>
59 <xsl:apply-templates select="." mode="noannot"/>
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>
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>
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>
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"/>
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"/>
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"/>
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>
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>
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"/>