]> matita.cs.unibo.it Git - helm.git/blob - style/reals.xsl
made executable again
[helm.git] / style / reals.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 <!-- Reals                                                            -->
29 <!-- First draft: April 3 2000                                        -->
30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi          -->
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
38 <!-- ************************* LOGIC *********************************-->
39
40 <!-- REALS -->
41
42 <!--
43 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R.con']" mode="pure">
44  <m:reals/>
45 </xsl:template>
46 -->
47
48 <!-- 0 e 1 -->
49
50 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R0.con']" mode="pure">
51  <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
52 </xsl:template>
53
54 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R1.con']" mode="pure">
55  <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
56 </xsl:template>
57
58 <!-- Unary Operations and power -->
59
60 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Ropp.con']" mode="pure">
61    <xsl:call-template name="mk-mml-op-noannot">
62       <xsl:with-param name="arity" select="1"/>
63       <xsl:with-param name="c-tag" select="CONST"/>
64       <xsl:with-param name="m-tag" select="'minus'"/>
65    </xsl:call-template>
66 </xsl:template>
67
68 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rabsolu.con']" mode="pure">
69    <xsl:call-template name="mk-mml-op-noannot">
70       <xsl:with-param name="arity" select="1"/>
71       <xsl:with-param name="c-tag" select="CONST"/>
72       <xsl:with-param name="m-tag" select="'abs'"/>
73    </xsl:call-template>
74 </xsl:template>
75
76 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rfunctions/fact.con']" mode="pure">
77    <xsl:call-template name="mk-mml-op-noannot">
78       <xsl:with-param name="arity" select="1"/>
79       <xsl:with-param name="c-tag" select="CONST"/>
80       <xsl:with-param name="m-tag" select="'factorial'"/>
81    </xsl:call-template>
82 </xsl:template>
83
84 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbase/Rsqr.con']" mode="pure">
85    <xsl:variable name="mbody">
86       <xsl:apply-templates select="*[2]" mode="noannot"/>
87       <m:cn>2</m:cn>
88    </xsl:variable>
89    <xsl:call-template name="out-mml-op">
90       <xsl:with-param name="arity" select="1"/>
91       <xsl:with-param name="c-tag" select="CONST"/>
92       <xsl:with-param name="m-tag" select="'power'"/>
93       <xsl:with-param name="mbody" select="$mbody"/>
94    </xsl:call-template>
95 </xsl:template>
96
97 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rinv.con']" mode="pure">
98    <xsl:variable name="mbody1">
99       <xsl:apply-templates select="*[2]" mode="noannot"/>
100       <xsl:variable name="mbody2">
101          <m:cn>1</m:cn>
102       </xsl:variable>
103       <xsl:call-template name="out-mml-op">
104          <xsl:with-param name="arity" select="1"/>
105          <xsl:with-param name="c-tag" select="CONST"/>
106          <xsl:with-param name="m-tag" select="'minus'"/>
107          <xsl:with-param name="mbody" select="$mbody2"/>
108       </xsl:call-template>
109    </xsl:variable>
110    <xsl:call-template name="out-mml-op">
111       <xsl:with-param name="arity" select="1"/>
112       <xsl:with-param name="c-tag" select="CONST"/>
113       <xsl:with-param name="m-tag" select="'power'"/>
114       <xsl:with-param name="mbody" select="$mbody1"/>
115    </xsl:call-template>
116 </xsl:template>
117
118 <!-- Binary Operations and Relations -->
119
120 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rle.con']" mode="pure">
121    <xsl:call-template name="mk-mml-op-noannot">
122       <xsl:with-param name="arity" select="2"/>
123       <xsl:with-param name="c-tag" select="CONST"/>
124       <xsl:with-param name="m-tag" select="'leq'"/>
125    </xsl:call-template>
126 </xsl:template>
127
128 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rlt.con']" mode="pure">
129    <xsl:call-template name="mk-mml-op-noannot">
130       <xsl:with-param name="arity" select="2"/>
131       <xsl:with-param name="c-tag" select="CONST"/>
132       <xsl:with-param name="m-tag" select="'lt'"/>
133    </xsl:call-template>
134 </xsl:template>
135
136 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con']" mode="pure">
137    <xsl:call-template name="mk-mml-op-noannot">
138       <xsl:with-param name="arity" select="2"/>
139       <xsl:with-param name="c-tag" select="CONST"/>
140       <xsl:with-param name="m-tag" select="'geq'"/>
141    </xsl:call-template>
142 </xsl:template>
143
144 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con']" mode="pure">
145    <xsl:call-template name="mk-mml-op-noannot">
146       <xsl:with-param name="arity" select="2"/>
147       <xsl:with-param name="c-tag" select="CONST"/>
148       <xsl:with-param name="m-tag" select="'gt'"/>
149    </xsl:call-template>
150 </xsl:template>
151
152 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rplus.con']" mode="pure">
153    <xsl:call-template name="mk-mml-op-noannot">
154       <xsl:with-param name="arity" select="2"/>
155       <xsl:with-param name="c-tag" select="CONST"/>
156       <xsl:with-param name="m-tag" select="'plus'"/>
157    </xsl:call-template>
158 </xsl:template>
159
160 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rminus.con']" mode="pure">
161    <xsl:call-template name="mk-mml-op-noannot">
162       <xsl:with-param name="arity" select="2"/>
163       <xsl:with-param name="c-tag" select="CONST"/>
164       <xsl:with-param name="m-tag" select="'minus'"/>
165    </xsl:call-template>
166 </xsl:template>
167
168 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rmult.con']" mode="pure">
169    <xsl:call-template name="mk-mml-op-noannot">
170       <xsl:with-param name="arity" select="2"/>
171       <xsl:with-param name="c-tag" select="CONST"/>
172       <xsl:with-param name="m-tag" select="'times'"/>
173    </xsl:call-template>
174 </xsl:template>
175
176 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rdiv.con']" mode="pure">
177    <xsl:call-template name="mk-mml-op-noannot">
178       <xsl:with-param name="arity" select="2"/>
179       <xsl:with-param name="c-tag" select="CONST"/>
180       <xsl:with-param name="m-tag" select="'divide'"/>
181    </xsl:call-template>
182 </xsl:template>
183
184 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con']" mode="pure">
185    <xsl:call-template name="mk-mml-op-noannot">
186       <xsl:with-param name="arity" select="2"/>
187       <xsl:with-param name="c-tag" select="CONST"/>
188       <xsl:with-param name="m-tag" select="'min'"/>
189    </xsl:call-template>
190 </xsl:template>
191
192 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmax.con']" mode="pure">
193    <xsl:call-template name="mk-mml-op-noannot">
194       <xsl:with-param name="arity" select="2"/>
195       <xsl:with-param name="c-tag" select="CONST"/>
196       <xsl:with-param name="m-tag" select="'max'"/>
197    </xsl:call-template>
198 </xsl:template>
199
200 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rfunctions/pow.con']" mode="pure">
201    <xsl:call-template name="mk-mml-op-noannot">
202       <xsl:with-param name="arity" select="2"/>
203       <xsl:with-param name="c-tag" select="CONST"/>
204       <xsl:with-param name="m-tag" select="'power'"/>
205    </xsl:call-template>
206 </xsl:template>
207
208 <!-- LIMIT -->
209
210 <xsl:template match="APPLY[CONST[
211  attribute::uri='cic:/Coq/Reals/Rlimit/limit1_in.con']]" mode="pure">
212     <xsl:choose>
213      <xsl:when test="count(child::*) = 5">
214       <m:apply>
215        <m:eq/>
216        <xsl:choose>
217         <xsl:when test="name(*[2]) = 'LAMBDA'">
218          <m:apply helm:xref="{@id}">
219           <m:limit>
220            <xsl:attribute name="definitionURL">
221             <xsl:value-of select="CONST/@uri"/> 
222            </xsl:attribute>
223            <xsl:attribute name="helm:xref">
224             <xsl:value-of select="CONST/@id"/>
225            </xsl:attribute>
226           </m:limit>
227           <m:bvar>
228            <m:ci>
229             <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template>
230            </m:ci>
231           </m:bvar>
232           <m:lowlimit>
233            <xsl:apply-templates select="*[5]" mode="noannot"/>
234           </m:lowlimit>
235           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
236          </m:apply>
237         </xsl:when>
238         <xsl:otherwise>
239          <m:apply helm:xref="{@id}">
240           <m:limit>
241             <xsl:attribute name="definitionURL">
242              <xsl:value-of select="CONST/@uri"/> 
243             </xsl:attribute>
244             <xsl:attribute name="helm:xref">
245              <xsl:value-of select="CONST/@id"/>
246             </xsl:attribute>
247            </m:limit>
248           <m:bvar>
249            <m:ci>$x</m:ci>
250           </m:bvar>
251           <m:lowlimit>
252            <xsl:apply-templates select="*[5]" mode="noannot"/>
253           </m:lowlimit>
254           <m:apply>
255            <m:csymbol>app</m:csymbol>
256            <xsl:apply-templates select="*[2]" mode="noannot"/>
257            <m:ci>$x</m:ci>
258           </m:apply>
259          </m:apply>
260         </xsl:otherwise>
261        </xsl:choose>
262        <xsl:apply-templates select="*[4]" mode="noannot"/>
263       </m:apply>
264      </xsl:when>
265      <xsl:otherwise>
266       <xsl:apply-imports/>
267      </xsl:otherwise>
268     </xsl:choose>
269 </xsl:template>
270
271 <!-- DIFFERENTIATION -->
272
273 <xsl:template match="APPLY[CONST[
274  attribute::uri='cic:/Coq/Reals/Rderiv/D_in.con']]" mode="pure">
275     <xsl:choose>
276      <xsl:when test="count(child::*) = 4">
277       <m:apply>
278        <m:eq/>
279        <xsl:choose>
280         <xsl:when test="name(*[2]) = 'LAMBDA'">
281          <m:apply helm:xref="{@id}">
282           <m:diff>
283            <xsl:attribute name="definitionURL">
284             <xsl:value-of select="CONST/@uri"/> 
285            </xsl:attribute>
286            <xsl:attribute name="helm:xref">
287             <xsl:value-of select="CONST/@id"/>
288            </xsl:attribute>
289           </m:diff>
290           <m:bvar>
291            <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA[1]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
292           </m:bvar>
293           <xsl:apply-templates select="*[2]/target" mode="noannot"/>
294          </m:apply>
295         </xsl:when>
296         <xsl:otherwise>
297          <m:apply helm:xref="{@id}">
298           <m:diff/>
299           <m:bvar>
300            <m:ci>$x</m:ci>
301           </m:bvar>
302           <m:apply>
303            <m:csymbol>app</m:csymbol>
304            <xsl:apply-templates select="*[2]" mode="noannot"/>
305            <m:ci>$x</m:ci>
306           </m:apply>
307          </m:apply>
308         </xsl:otherwise>
309        </xsl:choose>
310        <xsl:apply-templates select="*[4]" mode="noannot"/>
311       </m:apply>
312      </xsl:when>
313      <xsl:otherwise>
314       <xsl:apply-imports/>
315      </xsl:otherwise>
316     </xsl:choose>
317 </xsl:template>
318
319 </xsl:stylesheet>