From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Dec 2002 17:04:13 +0000 (+0000)
Subject: Ring partially ported to the new library. But I am completely sure that
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=570d0db41452928eac92a00dc63f0b360d2c816b;p=helm.git

Ring partially ported to the new library. But I am completely sure that
this is not the notation we need for ring. To be changed...
---

diff --git a/helm/style/ring.xsl b/helm/style/ring.xsl
index 4a2848c26..5136e77d5 100644
--- a/helm/style/ring.xsl
+++ b/helm/style/ring.xsl
@@ -4,12 +4,12 @@
                               xmlns:m="http://www.w3.org/1998/Math/MathML"
                               xmlns:helm="http://www.cs.unibo.it/helm">
 			      
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con']" mode="pure">
+<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">
    <xsl:choose>
-      <xsl:when test="count(child::*) > 1">
+      <xsl:when test="count(child::*) = 2">
          <m:apply helm:xref="{@id}">
             <m:csymbol>app</m:csymbol>
-            <xsl:apply-templates mode="noannot" select="*[1]"/>
+            <xsl:apply-templates mode="noannot" select="*[1]/*[1]"/>
             <m:ci>...</m:ci>
          </m:apply>
       </xsl:when>
@@ -19,12 +19,12 @@
    </xsl:choose>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_ap.con']" mode="pure">
+<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">
    <xsl:choose>
-      <xsl:when test="count(child::*) = 9">
+      <xsl:when test="count(child::*) = 2">
          <xsl:call-template name="start-interp">
-	    <xsl:with-param name="rtree" select="*[9]"/>
-            <xsl:with-param name="atree" select="*[8]"/>
+	    <xsl:with-param name="rtree" select="*[2]"/>
+            <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
 	 </xsl:call-template>
       </xsl:when>
       <xsl:otherwise>
@@ -33,16 +33,15 @@
    </xsl:choose>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_sacs.con']" mode="pure">
+<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">
    <xsl:choose>
-      <xsl:when test="count(child::*) = 9 and *[APPLY and position()=9]
-                      [CONST/@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con']">
+      <xsl:when test="count(child::*) = 2 and *[APPLY and position()=2][CONST/@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con']">
          <m:apply helm:xref="{@id}">
             <m:csymbol>app</m:csymbol>
-            <xsl:apply-templates mode="noannot" select="*[9]/*[1]"/>
+            <xsl:apply-templates mode="noannot" select="*[2]/*[1]"/>
             <xsl:call-template name="start-interp">
-	       <xsl:with-param name="rtree" select="*[9]/*[2]"/>
-               <xsl:with-param name="atree" select="*[8]"/>
+	       <xsl:with-param name="rtree" select="*[2]/*[2]"/>
+            <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
 	    </xsl:call-template>
          </m:apply>
       </xsl:when>
@@ -54,28 +53,34 @@
 
 <!-- **************************  abstract polinomials rendering ************************ -->
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' 
-                                    and @noConstr='1']]" mode="interp">
+<xsl:template match="*" mode="interp">
+ <m:apply>
+  <m:ci>ERROR INTERP:</m:ci>
+  <xsl:apply-templates select="." mode="noannot"/>
+ </m:apply>
+</xsl:template>
+
+<!-- APVar -->
+<!-- CSC: ??????????? -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/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/apolynomial.ind' 
-                                    and @noConstr='2']]" mode="interp">
-   <xsl:param name="atree"/>
-   <xsl:apply-templates mode="noannot" select="."/>
+<!-- AP0 -->
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='2']" mode="interp">
+ <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' 
-                                    and @noConstr='3']]" mode="interp">
-   <xsl:param name="atree"/>
-   <xsl:apply-templates mode="noannot" select="."/>
+<!-- AP1 -->
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='3']" mode="interp">
+ <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' 
-                                    and @noConstr='4']]" mode="interp">
+<!-- APplus -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='4']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:call-template name="mk-mml-op-interp">
       <xsl:with-param name="arity" select="2"/>
@@ -85,8 +90,8 @@
    </xsl:call-template>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' 
-                                    and @noConstr='5']]" mode="interp">
+<!-- APmult -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='5']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:call-template name="mk-mml-op-interp">
       <xsl:with-param name="arity" select="2"/>
@@ -96,8 +101,8 @@
    </xsl:call-template>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' 
-                                    and @noConstr='6']]" mode="interp">
+<!-- APopp -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='6']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:call-template name="mk-mml-op-interp">
       <xsl:with-param name="arity" select="1"/>
@@ -107,24 +112,21 @@
    </xsl:call-template> 
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' 
-                                    and @noConstr='1']]" mode="interp">
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/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/index.ind' 
-                                    and @noConstr='2']]" mode="interp">
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/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/index.ind' 
-                              and @noConstr='3']" mode="interp">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' and @noConstr='3']" mode="interp">
    <xsl:param name="atree"/>
    <xsl:apply-templates select="$atree/*[3]" mode="noannot"/>
 </xsl:template>