From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 3 Apr 2001 14:58:57 +0000 (+0000)
Subject: abstract polinomials
X-Git-Tag: v0_1_2~38
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e8c7d0435c1f0de182d341f6e6f8e0d7412eefac

abstract polinomials
---

diff --git a/helm/style/ring.xsl b/helm/style/ring.xsl
new file mode 100644
index 000000000..98306fcd4
--- /dev/null
+++ b/helm/style/ring.xsl
@@ -0,0 +1,133 @@
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm"
+                              xmlns:xlink="http://www.w3.org/1999/xlink">
+			      
+<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con']" mode="pure">
+   <xsl:choose>
+      <xsl:when test="count(child::*) > 1">
+         <m:apply helm:xref="{@id}">
+            <m:csymbol>app</m:csymbol>
+            <xsl:apply-templates mode="noannot" select="*[1]"/>
+            <m:ci>...</m:ci>
+         </m:apply>
+      </xsl:when>
+      <xsl:otherwise>
+         <xsl:apply-imports/>
+      </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con']" mode="pure">
+   <xsl:choose>
+      <xsl:when test="count(child::*) = 9">
+         <xsl:call-template name="start-interp">
+	    <xsl:with-param name="rtree" select="*[9]"/>
+            <xsl:with-param name="atree" select="*[8]"/>
+	 </xsl:call-template>
+      </xsl:when>
+      <xsl:otherwise>
+         <xsl:apply-imports/>
+      </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con']" mode="pure">
+   <xsl:choose>
+      <xsl:when test="count(child::*) = 9 and *[APPLY and position()=9]
+                      [CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con']">
+         <m:apply helm:xref="{@id}">
+            <m:csymbol>app</m:csymbol>
+            <xsl:apply-templates mode="noannot" select="*[9]/*[1]"/>
+            <xsl:call-template name="start-interp">
+	       <xsl:with-param name="rtree" select="*[9]/*[2]"/>
+               <xsl:with-param name="atree" select="*[8]"/>
+	    </xsl:call-template>
+         </m:apply>
+      </xsl:when>
+      <xsl:otherwise>
+         <xsl:apply-imports/>
+      </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<!-- **************************  abstract polinomials rendering ************************ -->
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
+                                    and @noConstr='1']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:apply-templates select="*[2]" mode="interp">
+      <xsl:with-param name="atree" select="$atree"/>
+   </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
+                                    and @noConstr='2']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:apply-templates mode="noannot" select="."/>
+</xsl:template>
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
+                                    and @noConstr='3']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:apply-templates mode="noannot" select="."/>
+</xsl:template>
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
+                                    and @noConstr='4']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:call-template name="mkmml-op-interp">
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="MUTCONSTRUCT"/>
+      <xsl:with-param name="m-tag" select="'plus'"/>
+      <xsl:with-param name="atree" select="$atree"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
+                                    and @noConstr='5']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:call-template name="mkmml-op-interp">
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="MUTCONSTRUCT"/>
+      <xsl:with-param name="m-tag" select="'times'"/>
+      <xsl:with-param name="atree" select="$atree"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
+                                    and @noConstr='6']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:call-template name="mkmml-op-interp">
+      <xsl:with-param name="arity" select="1"/>
+      <xsl:with-param name="c-tag" select="MUTCONSTRUCT"/>
+      <xsl:with-param name="m-tag" select="'minus'"/>
+      <xsl:with-param name="atree" select="$atree"/>
+   </xsl:call-template> 
+</xsl:template>
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind' 
+                                    and @noConstr='1']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:apply-templates select="*[2]" mode="interp">
+      <xsl:with-param name="atree" select="$atree/*[4]"/>
+   </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind' 
+                                    and @noConstr='2']]" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:apply-templates select="*[2]" mode="interp"> 
+      <xsl:with-param name="atree" select="$atree/*[5]"/>
+   </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind' 
+                              and @noConstr='3']" mode="interp">
+   <xsl:param name="atree"/>
+   <xsl:apply-templates select="$atree/*[3]" mode="noannot"/>
+</xsl:template>
+
+</xsl:stylesheet>