"Recursive" notation for Z.

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

diff --git a/helm/style/arith.xsl b/helm/style/arith.xsl
index 6393d272280229930af40d0345ec8db7c27e0d84..e436df28c5cc6a72c62b40a765a803f88a19df8f 100644 (file)
--- a/helm/style/arith.xsl
+++ b/helm/style/arith.xsl
@@ -183,4 +183,101 @@
    </xsl:call-template>
 </xsl:template>
 
+<!-- POS, NEG e ZERO -->
+
+<xsl:template match="APPLY[MUTCONSTRUCT[position()=1 and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
+   <xsl:apply-templates select="*[2]" mode="Zpositive">
+    <xsl:with-param name="base" select="0"/>
+    <xsl:with-param name="exp" select="1"/>
+    <xsl:with-param name="iden" select="*[2]/@id"/>
+   </xsl:apply-templates>
+</xsl:template>
+ 
+<xsl:template match="APPLY[MUTCONSTRUCT[position()=1 and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
+   <m:apply helm:xref="{@id}">
+    <m:minus definitionURL="{*[1]/@uri}" helm:xref="{*[1]/@id}"/>
+    <xsl:apply-templates select="*[2]" mode="Zpositive">
+     <xsl:with-param name="base" select="0"/>
+     <xsl:with-param name="exp" select="1"/>
+     <xsl:with-param name="iden" select="*[2]/@id"/>
+    </xsl:apply-templates>
+   </m:apply>
+</xsl:template>
+
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='1']" mode="pure">
+   <m:ci definitionURL="{@uri}" helm:xref="{@id}">0</m:ci>
+</xsl:template>
+
+<!-- prova di notazione per positive -->
+
+<xsl:template match="APPLY[MUTCONSTRUCT[position()=1 and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind']]" mode="pure">
+   <xsl:apply-templates select="." mode="Zpositive">
+    <xsl:with-param name="base" select="0"/>
+    <xsl:with-param name="exp" select="1"/>
+    <xsl:with-param name="iden" select="@id"/>
+   </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="*" mode="Zpositive">
+ <xsl:param name="base" select="0"/>
+ <xsl:param name="exp" select="1"/>
+ <xsl:param name="iden" select="''"/>
+ <xsl:choose>
+  <xsl:when test="name()='APPLY' and MUTCONSTRUCT[position()=1 and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='1']">
+   <xsl:apply-templates select="*[2]" mode="Zpositive">
+    <xsl:with-param name="base" select="$base + $exp"/>
+    <xsl:with-param name="exp" select="2 * $exp"/>
+    <xsl:with-param name="iden" select="$iden"/>
+   </xsl:apply-templates>
+  </xsl:when>
+  <xsl:when test="name()='APPLY' and MUTCONSTRUCT[position()=1 and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='2']">
+   <xsl:apply-templates select="*[2]" mode="Zpositive">
+    <xsl:with-param name="base" select="$base"/>
+    <xsl:with-param name="exp" select="2 * $exp"/>
+    <xsl:with-param name="iden" select="$iden"/>
+   </xsl:apply-templates>
+  </xsl:when>
+  <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3'">
+   <m:ci helm:xref="{$iden}"><xsl:value-of select="$base + $exp"/></m:ci>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:choose>
+    <xsl:when test="$base = 0">
+     <xsl:choose>
+      <xsl:when test="$exp = 1">
+       <m:ci helm:xref="{$iden}"><xsl:value-of select="$exp"/></m:ci>
+      </xsl:when>
+      <xsl:otherwise>
+       <m:apply helm:xref="{$iden}">
+        <m:times/>
+        <m:ci><xsl:value-of select="$exp"/></m:ci>
+        <xsl:apply-templates select="." mode="pure"/>
+       </m:apply>
+      </xsl:otherwise>
+     </xsl:choose>
+    </xsl:when>
+    <xsl:otherwise>
+     <m:apply helm:xref="{$iden}">
+      <m:plus/>
+      <m:ci><xsl:value-of select="$base"/></m:ci>
+      <xsl:choose>
+       <xsl:when test="$exp = 1">
+        <m:ci><xsl:value-of select="$exp"/></m:ci>
+       </xsl:when>
+       <xsl:otherwise>
+        <m:apply helm:xref="{$iden}">
+         <m:times/>
+         <m:ci><xsl:value-of select="$exp"/></m:ci>
+         <xsl:apply-templates select="." mode="pure"/>
+        </m:apply>
+       </xsl:otherwise>
+      </xsl:choose>
+     </m:apply>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
 </xsl:stylesheet>