]> matita.cs.unibo.it Git - helm.git/blob - helm/meta_style/positive.xsl
removed an ancient debugging message
[helm.git] / helm / meta_style / positive.xsl
1 <?xml version="1.0"?>
2
3 <!-- Copyright (C) 2000, HELM Team                                     -->
4 <!--                                                                   -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
6 <!-- Library of Mathematics, developed at the Computer Science         -->
7 <!-- Department, University of Bologna, Italy.                         -->
8 <!--                                                                   -->
9 <!-- HELM is free software; you can redistribute it and/or             -->
10 <!-- modify it under the terms of the GNU General Public License       -->
11 <!-- as published by the Free Software Foundation; either version 2    -->
12 <!-- of the License, or (at your option) any later version.            -->
13 <!--                                                                   -->
14 <!-- HELM is distributed in the hope that it will be useful,           -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
17 <!-- GNU General Public License for more details.                      -->
18 <!--                                                                   -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software               -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
22 <!-- MA  02111-1307, USA.                                              -->
23 <!--                                                                   -->
24 <!-- For details, see the HELM World-Wide-Web page,                    -->
25 <!-- http://cs.unibo.it/helm/.                                         -->
26
27 <!--******************************************************************--> 
28 <!-- Arithmetics                                                      -->
29 <!-- First draft: March 20 2001, Ferruccio Guidi                      -->
30 <!-- Zarith: July 2001, Andrea Asperti                                -->
31 <!--******************************************************************-->
32
33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
34                               xmlns:m="http://www.w3.org/1998/Math/MathML"
35                               xmlns:helm="http://www.cs.unibo.it/helm">
36
37 <!-- ************************** ARITHMETICS ****************************** -->
38
39 <!-- S and O -->
40 <xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
41    <xsl:apply-templates select="*[2]" mode="succ">
42     <xsl:with-param name="n" select="1"/>
43     <xsl:with-param name="iden" select="@id"/>
44    </xsl:apply-templates>
45 </xsl:template>
46
47 <xsl:template match="*" mode="succ">
48  <xsl:param name="n" select="0"/>
49  <xsl:param name="iden" select="''"/>
50  <xsl:choose>
51   <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT'
52 and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
53    <xsl:apply-templates select="*[2]" mode="succ">
54     <xsl:with-param name="n" select="$n +1"/>
55     <xsl:with-param name="iden" select="$iden"/>
56    </xsl:apply-templates>
57   </xsl:when>
58   <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='1'">
59    <m:cn helm:xref="{$iden}"><xsl:value-of select="$n"/></m:cn>
60   </xsl:when>
61   <xsl:otherwise>
62    <m:apply helm:xref="{$iden}">
63     <m:plus/>
64     <m:cn><xsl:value-of select="$n"/></m:cn>
65     <xsl:apply-templates select="." mode="pure"/>
66    </m:apply>
67   </xsl:otherwise>
68  </xsl:choose>
69 </xsl:template>
70
71
72 <!-- **************************** Zarith ******************************** -->
73
74
75
76 <xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
77    <xsl:apply-templates select="*[2]" mode="Zpositive">
78     <xsl:with-param name="base" select="0"/>
79     <xsl:with-param name="exp" select="1"/>
80     <xsl:with-param name="iden" select="*[2]/@id"/>
81    </xsl:apply-templates>
82 </xsl:template>
83  
84 <xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
85    <m:apply helm:xref="{@id}">
86     <m:minus definitionURL="{*[1]/@uri}" helm:xref="{*[1]/@id}"/>
87     <xsl:apply-templates select="*[2]" mode="Zpositive">
88      <xsl:with-param name="base" select="0"/>
89      <xsl:with-param name="exp" select="1"/>
90      <xsl:with-param name="iden" select="*[2]/@id"/>
91     </xsl:apply-templates>
92    </m:apply>
93 </xsl:template>
94
95 <xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='1']" mode="pure">
96    <m:ci definitionURL="{@uri}" helm:xref="{@id}">0</m:ci>
97 </xsl:template>
98
99 <!-- prova di notazione per positive -->
100
101 <xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind']]" mode="pure">
102    <xsl:apply-templates select="." mode="Zpositive">
103     <xsl:with-param name="base" select="0"/>
104     <xsl:with-param name="exp" select="1"/>
105     <xsl:with-param name="iden" select="@id"/>
106    </xsl:apply-templates>
107 </xsl:template>
108
109 <xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3']" mode="pure">
110  <m:ci definitionURL="{@uri}" helm:xref="{@id}">1</m:ci>
111 </xsl:template> 
112
113 <xsl:template match="*" mode="Zpositive">
114  <xsl:param name="base" select="0"/>
115  <xsl:param name="exp" select="1"/>
116  <xsl:param name="iden" select="''"/>
117  <xsl:choose>
118   <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT'
119 and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='1']">
120    <xsl:apply-templates select="*[2]" mode="Zpositive">
121     <xsl:with-param name="base" select="$base + $exp"/>
122     <xsl:with-param name="exp" select="2 * $exp"/>
123     <xsl:with-param name="iden" select="$iden"/>
124    </xsl:apply-templates>
125   </xsl:when>
126   <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT' 
127 and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='2']">
128    <xsl:apply-templates select="*[2]" mode="Zpositive">
129     <xsl:with-param name="base" select="$base"/>
130     <xsl:with-param name="exp" select="2 * $exp"/>
131     <xsl:with-param name="iden" select="$iden"/>
132    </xsl:apply-templates>
133   </xsl:when>
134   <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3'">
135    <m:ci helm:xref="{$iden}"><xsl:value-of select="$base + $exp"/></m:ci>
136   </xsl:when>
137   <xsl:otherwise>
138    <xsl:choose>
139     <xsl:when test="$base = 0">
140      <xsl:choose>
141       <xsl:when test="$exp = 1">
142        <xsl:apply-templates select="." mode="pure"/>
143       </xsl:when>
144       <xsl:otherwise>
145        <m:apply helm:xref="{$iden}">
146         <m:times/>
147         <m:ci><xsl:value-of select="$exp"/></m:ci>
148         <xsl:apply-templates select="." mode="pure"/>
149        </m:apply>
150       </xsl:otherwise>
151      </xsl:choose>
152     </xsl:when>
153     <xsl:otherwise>
154      <m:apply helm:xref="{$iden}">
155       <m:plus/>
156       <m:ci><xsl:value-of select="$base"/></m:ci>
157       <xsl:choose>
158        <xsl:when test="$exp = 1">
159         <xsl:apply-templates select="." mode="pure"/>
160        </xsl:when>
161        <xsl:otherwise>
162         <m:apply helm:xref="{$iden}">
163          <m:times/>
164          <m:ci><xsl:value-of select="$exp"/></m:ci>
165          <xsl:apply-templates select="." mode="pure"/>
166         </m:apply>
167        </xsl:otherwise>
168       </xsl:choose>
169      </m:apply>
170     </xsl:otherwise>
171    </xsl:choose>
172   </xsl:otherwise>
173  </xsl:choose>
174 </xsl:template>
175
176
177 </xsl:stylesheet>