No longer in use. The official repository for the

[helm.git] / helm / style / ring.xsl

diff --git a/helm/style/ring.xsl b/helm/style/ring.xsl
deleted file mode 100644 (file)
index 5136e77..0000000
--- a/helm/style/ring.xsl
+++ /dev/null
@@ -1,134 +0,0 @@
-<?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">
-                             
-<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::*) = 2">
-         <m:apply helm:xref="{@id}">
-            <m:csymbol>app</m:csymbol>
-            <xsl:apply-templates mode="noannot" select="*[1]/*[1]"/>
-            <m:ci>...</m:ci>
-         </m:apply>
-      </xsl:when>
-      <xsl:otherwise>
-         <xsl:apply-imports/>
-      </xsl:otherwise>
-   </xsl:choose>
-</xsl:template>
-
-<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::*) = 2">
-         <xsl:call-template name="start-interp">
-           <xsl:with-param name="rtree" select="*[2]"/>
-            <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
-        </xsl:call-template>
-      </xsl:when>
-      <xsl:otherwise>
-         <xsl:apply-imports/>
-      </xsl:otherwise>
-   </xsl:choose>
-</xsl:template>
-
-<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::*) = 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="*[2]/*[1]"/>
-            <xsl:call-template name="start-interp">
-              <xsl:with-param name="rtree" select="*[2]/*[2]"/>
-            <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
-           </xsl:call-template>
-         </m:apply>
-      </xsl:when>
-      <xsl:otherwise>
-         <xsl:apply-imports/>
-      </xsl:otherwise>
-   </xsl:choose>
-</xsl:template>
-
-<!-- **************************  abstract polinomials rendering ************************ -->
-
-<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>
-
-<!-- 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>
-
-<!-- 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>
-
-<!-- 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"/>
-      <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>
-
-<!-- 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"/>
-      <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>
-
-<!-- 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"/>
-      <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/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: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:param name="atree"/>
-   <xsl:apply-templates select="$atree/*[3]" mode="noannot"/>
-</xsl:template>
-
-</xsl:stylesheet>