]> matita.cs.unibo.it Git - helm.git/blob - style/algebra.xsl
made executable again
[helm.git] / style / algebra.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 <!-- Algebra                                                          -->
29 <!-- First draft: October 2001                                        -->
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 <!-- ************************* ALGEBRA *********************************-->
39
40
41
42 <!-- 0 and 1 -->
43
44 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSemiGroups/csg_unit.con']" mode="pure">
45  <m:ci definitionURL="{CONST/@uri}" helm:xref="{@id}">0</m:ci>
46 </xsl:template>
47
48 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_one.con']" mode="pure">
49  <m:ci definitionURL="{CONST/@uri}" helm:xref="{@id}">1</m:ci>
50 </xsl:template>
51
52 <!-- Unary Operations -->
53
54 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CGroups/cg_inv.con']" mode="pure">
55    <xsl:call-template name="mk-mml-op-noannot">
56       <xsl:with-param name="arity" select="1"/>
57       <xsl:with-param name="hide" select="1"/>
58       <xsl:with-param name="c-tag" select="CONST"/>
59       <xsl:with-param name="m-tag" select="'minus'"/>
60    </xsl:call-template>
61 </xsl:template>
62
63 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CMetricFields/CMetric_Fields/cmf_abs.con']" mode="pure">
64    <xsl:call-template name="mk-mml-op-noannot">
65       <xsl:with-param name="hide" select="1"/>
66       <xsl:with-param name="c-tag" select="CONST"/>
67       <xsl:with-param name="m-tag" select="'abs'"/>
68    </xsl:call-template>
69 </xsl:template>
70
71 <!-- inv (uri errata)
72 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp.con']" mode="pure">
73    <xsl:variable name="mbody1">
74       <xsl:apply-templates select="*[2]" mode="noannot"/>
75       <xsl:variable name="mbody2">
76          <m:cn>1</m:cn>
77       </xsl:variable>
78       <xsl:call-template name="out-mml-op">
79          <xsl:with-param name="arity" select="1"/>
80          <xsl:with-param name="c-tag" select="CONST"/>
81          <xsl:with-param name="m-tag" select="'minus'"/>
82          <xsl:with-param name="mbody" select="$mbody2"/>
83       </xsl:call-template>
84    </xsl:variable>
85    <xsl:call-template name="out-mml-op">
86       <xsl:with-param name="arity" select="1"/>
87       <xsl:with-param name="c-tag" select="CONST"/>
88       <xsl:with-param name="m-tag" select="'power'"/>
89       <xsl:with-param name="mbody" select="$mbody1"/>
90    </xsl:call-template>
91 </xsl:template>
92 -->
93
94 <!-- Binary Operations and Relations -->
95
96 <!-- setoid equality -->
97
98 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSetoids/cs_eq.con']" mode="pure">
99    <xsl:call-template name="mk-mml-op-noannot">
100       <xsl:with-param name="hide" select="1"/>
101       <xsl:with-param name="c-tag" select="CONST"/>
102       <xsl:with-param name="m-tag" select="'eq'"/>
103    </xsl:call-template>
104 </xsl:template>
105
106 <!-- apart -->
107
108 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSetoids/cs_ap.con']" mode="pure">
109    <xsl:call-template name="mk-mml-op-noannot">
110       <xsl:with-param name="hide" select="1"/>
111       <xsl:with-param name="c-tag" select="CONST"/>
112       <xsl:with-param name="m-tag" select="'neq'"/>
113    </xsl:call-template>
114 </xsl:template>
115
116 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/leEq.con']" mode="pure">
117    <xsl:call-template name="mk-mml-op-noannot">
118       <xsl:with-param name="hide" select="1"/>
119       <xsl:with-param name="arity" select="2"/>
120       <xsl:with-param name="c-tag" select="CONST"/>
121       <xsl:with-param name="m-tag" select="'leq'"/>
122    </xsl:call-template>
123 </xsl:template>
124
125 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/cof_less.con']" mode="pure">
126    <xsl:call-template name="mk-mml-op-noannot">
127       <xsl:with-param name="hide" select="1"/>
128       <xsl:with-param name="c-tag" select="CONST"/>
129       <xsl:with-param name="m-tag" select="'lt'"/>
130    </xsl:call-template>
131 </xsl:template>
132
133 <!--
134 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con']" mode="pure">
135    <xsl:call-template name="mk-mml-op-noannot">
136       <xsl:with-param name="arity" select="2"/>
137       <xsl:with-param name="c-tag" select="CONST"/>
138       <xsl:with-param name="m-tag" select="'geq'"/>
139    </xsl:call-template>
140 </xsl:template>
141
142 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con']" mode="pure">
143    <xsl:call-template name="mk-mml-op-noannot">
144       <xsl:with-param name="arity" select="2"/>
145       <xsl:with-param name="c-tag" select="CONST"/>
146       <xsl:with-param name="m-tag" select="'gt'"/>
147    </xsl:call-template>
148 </xsl:template>
149 -->
150
151 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_plus.con' or
152 CONST/@uri='cic:/Algebra/CSemiGroups/csg_op.con']" mode="pure">
153    <xsl:call-template name="mk-mml-op-noannot">
154       <xsl:with-param name="hide" select="1"/>
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:/Algebra/CRings/cr_minus.con' or
161  CONST/@uri='cic:/Algebra/CGroups/cg_minus.con']" mode="pure">
162    <xsl:call-template name="mk-mml-op-noannot">
163       <xsl:with-param name="hide" select="1"/>
164       <xsl:with-param name="c-tag" select="CONST"/>
165       <xsl:with-param name="m-tag" select="'minus'"/>
166    </xsl:call-template>
167 </xsl:template>
168
169 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_mult.con']" mode="pure">
170    <xsl:call-template name="mk-mml-op-noannot">
171       <xsl:with-param name="hide" select="1"/>
172       <xsl:with-param name="c-tag" select="CONST"/>
173       <xsl:with-param name="m-tag" select="'times'"/>
174    </xsl:call-template>
175 </xsl:template>
176
177 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CFields/cf_div.con']" mode="pure">
178    <xsl:call-template name="mk-mml-op-noannot">
179       <xsl:with-param name="arity" select="2"/>
180       <xsl:with-param name="hide" select="1"/>
181       <xsl:with-param name="c-tag" select="CONST"/>
182       <xsl:with-param name="m-tag" select="'divide'"/>
183    </xsl:call-template>
184 </xsl:template>
185
186 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/Ring_constructions/nzpro.con' and count(*)='4']" mode="pure">
187    <xsl:apply-templates select="*[3]" mode="pure"/>
188 </xsl:template>
189
190 <!-- 
191 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con']" mode="pure">
192    <xsl:call-template name="mk-mml-op-noannot">
193       <xsl:with-param name="arity" select="2"/>
194       <xsl:with-param name="c-tag" select="CONST"/>
195       <xsl:with-param name="m-tag" select="'min'"/>
196    </xsl:call-template>
197 </xsl:template>
198
199 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmax.con']" mode="pure">
200    <xsl:call-template name="mk-mml-op-noannot">
201       <xsl:with-param name="arity" select="2"/>
202       <xsl:with-param name="c-tag" select="CONST"/>
203       <xsl:with-param name="m-tag" select="'max'"/>
204    </xsl:call-template>
205 </xsl:template>
206 -->
207
208
209 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp.con']" mode="pure">
210    <xsl:variable name="no_params">
211      <xsl:call-template name="get_no_params">
212       <xsl:with-param name="first_uri" select="$CICURI"/>
213       <xsl:with-param name="second_uri" select="CONST/@uri"/>
214      </xsl:call-template>
215     </xsl:variable>
216    <xsl:call-template name="mk-mml-op-noannot">
217       <xsl:with-param name="hide" select="$no_params"/>
218       <xsl:with-param name="c-tag" select="CONST"/>
219       <xsl:with-param name="m-tag" select="'power'"/>
220    </xsl:call-template>
221 </xsl:template>
222
223 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp_op.con' or CONST/@uri='cic:/Algebra/Expon/Zexp_def/zexp.con']" mode="pure">
224    <xsl:variable name="no_params">
225      <xsl:call-template name="get_no_params">
226       <xsl:with-param name="first_uri" select="$CICURI"/>
227       <xsl:with-param name="second_uri" select="CONST/@uri"/>
228      </xsl:call-template>
229    </xsl:variable>
230    <xsl:variable name="mbody">
231     <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
232     <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
233    </xsl:variable>
234    <xsl:call-template name="out-mml-op">
235       <xsl:with-param name="hide" select="$no_params"/>
236       <xsl:with-param name="arity" select="2"/>
237       <xsl:with-param name="c-tag" select="CONST"/>
238       <xsl:with-param name="m-tag" select="'power'"/>
239       <xsl:with-param name="mbody" select="$mbody"/>
240    </xsl:call-template>
241 </xsl:template>
242
243 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/absSmall.con']" mode="pure">
244    <xsl:variable name="mbody">
245       <m:apply helm:xref="{@id}">
246        <m:abs definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
247        <xsl:apply-templates select="*[4]" mode="noannot"/>
248       </m:apply>
249       <xsl:apply-templates select="*[3]" mode="noannot"/>
250    </xsl:variable>
251    <xsl:call-template name="out-mml-op">
252       <xsl:with-param name="hide" select="1"/>
253       <xsl:with-param name="arity" select="2"/>
254       <xsl:with-param name="c-tag" select="CONST"/>
255       <xsl:with-param name="m-tag" select="'lt'"/>
256       <xsl:with-param name="mbody" select="$mbody"/>
257    </xsl:call-template>
258 </xsl:template>
259
260 <xsl:template match="APPLY[CONST[
261  attribute::uri='cic:/Algebra/COrdFields/OrdField_Cauchy/seqLimit.con']]" mode="pure">
262     <xsl:variable name="no_params">
263      <xsl:call-template name="get_no_params">
264       <xsl:with-param name="first_uri" select="$CICURI"/>
265       <xsl:with-param name="second_uri" select="CONST/@uri"/>
266      </xsl:call-template>
267     </xsl:variable>
268     <xsl:choose>
269      <xsl:when test="count(child::*) = 3+$no_params">
270       <m:apply helm:xref="{@id}">
271        <m:eq definitionURL="{CONST/@uri}" helm:xref="{@id}" />
272        <xsl:choose>
273         <xsl:when test="name(*[2+$no_params]) = 'LAMBDA'">
274          <m:apply helm:xref="{CONST/@id}">
275           <m:limit definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
276           <m:bvar>
277            <m:ci>
278             <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>
279            </m:ci>
280           </m:bvar>
281           <m:lowlimit>
282            <m:infinity/>
283           </m:lowlimit>
284           <xsl:apply-templates select="*[2+$no_params]/target/*[1]" mode="noannot"/>
285          </m:apply>
286         </xsl:when>
287         <xsl:otherwise>
288          <m:apply helm:xref="{CONST/@id}">
289           <m:limit definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
290           <m:bvar>
291            <m:ci>$x</m:ci>
292           </m:bvar>
293           <m:lowlimit>
294            <m:infinity/>
295           </m:lowlimit>
296           <m:apply>
297            <m:csymbol>app</m:csymbol>
298            <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
299            <m:ci>$x</m:ci>
300           </m:apply>
301          </m:apply>
302         </xsl:otherwise>
303        </xsl:choose>
304        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
305       </m:apply>
306      </xsl:when>
307      <xsl:otherwise>
308       <xsl:apply-imports/>
309      </xsl:otherwise>
310     </xsl:choose>
311 </xsl:template>
312
313 <xsl:template match="APPLY[CONST[
314  attribute::uri='cic:/Algebra/CSums/Sums/sum0.con']]" mode="pure">
315     <xsl:variable name="no_params">
316      <xsl:call-template name="get_no_params">
317       <xsl:with-param name="first_uri" select="$CICURI"/>
318       <xsl:with-param name="second_uri" select="CONST/@uri"/>
319      </xsl:call-template>
320     </xsl:variable>
321     <xsl:choose>
322      <xsl:when test="count(child::*) = 3+$no_params">
323        <xsl:choose>
324         <xsl:when test="name(*[3+$no_params]) = 'LAMBDA'">
325          <m:apply helm:xref="{CONST/@id}">
326           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
327           <m:bvar>
328            <m:ci>
329             <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>
330            </m:ci>
331           </m:bvar>
332           <m:condition>
333            <m:apply>
334             <m:lt/>
335             <m:ci>
336              <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>
337             </m:ci>
338             <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
339            </m:apply>
340           </m:condition>
341           <xsl:apply-templates select="*[3+$no_params]/target/*[1]" mode="noannot"/>
342          </m:apply>
343         </xsl:when>
344         <xsl:otherwise>
345          <m:apply helm:xref="{CONST/@id}">
346           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
347           <m:bvar>
348            <m:ci>$x</m:ci>
349           </m:bvar>
350           <m:condition>
351            <m:apply>
352             <m:lt/>
353             <m:ci>$x</m:ci>
354             <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
355            </m:apply>
356           </m:condition>
357           <m:apply>
358            <m:csymbol>app</m:csymbol>
359            <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
360            <m:ci>$x</m:ci>
361           </m:apply>
362          </m:apply>
363         </xsl:otherwise>
364        </xsl:choose>
365      </xsl:when>
366      <xsl:otherwise>
367       <xsl:apply-imports/>
368      </xsl:otherwise>
369     </xsl:choose>
370 </xsl:template>
371
372 <!-- sum -->
373 <xsl:template match="APPLY[CONST[
374  attribute::uri='cic:/Algebra/CSums/Sums/sum.con']]" mode="pure">
375     <xsl:variable name="no_params">
376      <xsl:call-template name="get_no_params">
377       <xsl:with-param name="first_uri" select="$CICURI"/>
378       <xsl:with-param name="second_uri" select="CONST/@uri"/>
379      </xsl:call-template>
380     </xsl:variable>
381     <xsl:choose>
382      <xsl:when test="count(child::*) = 4+$no_params">
383        <xsl:choose>
384         <xsl:when test="name(*[4+$no_params]) = 'LAMBDA'">
385          <m:apply helm:xref="{CONST/@id}">
386           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
387           <m:bvar>
388            <m:ci>
389             <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>
390            </m:ci>
391           </m:bvar>
392           <m:lowlimit>
393            <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
394           </m:lowlimit>
395           <m:uplimit>
396            <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
397           </m:uplimit>
398           <xsl:apply-templates select="*[4+$no_params]/target/*[1]" mode="noannot"/>
399          </m:apply>
400         </xsl:when>
401         <xsl:otherwise>
402          <m:apply helm:xref="{CONST/@id}">
403           <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
404           <m:bvar>
405            <m:ci>$x</m:ci>
406           </m:bvar>
407           <m:lowlimit>
408            <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
409           </m:lowlimit>
410           <m:uplimit>
411            <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
412           </m:uplimit>
413           <m:apply>
414            <m:csymbol>app</m:csymbol>
415            <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
416            <m:ci>$x</m:ci>
417           </m:apply>
418          </m:apply>
419         </xsl:otherwise>
420        </xsl:choose>
421      </xsl:when>
422      <xsl:otherwise>
423       <xsl:apply-imports/>
424      </xsl:otherwise>
425     </xsl:choose>
426 </xsl:template>
427
428 <!-- polynomials -->
429
430 <xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CPolynomials/CPoly_CRing_ctd/cpoly_apply_fun.con']" mode="pure">
431    <xsl:variable name="no_params">
432      <xsl:call-template name="get_no_params">
433       <xsl:with-param name="first_uri" select="$CICURI"/>
434       <xsl:with-param name="second_uri" select="CONST/@uri"/>
435      </xsl:call-template>
436     </xsl:variable>
437     <xsl:choose>
438      <xsl:when test="count(child::*) = 3+$no_params">
439       <m:apply>
440        <m:csymbol>app</m:csymbol>
441        <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
442        <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
443       </m:apply>
444      </xsl:when>
445      <xsl:otherwise>
446       <xsl:apply-imports/>
447      </xsl:otherwise>
448     </xsl:choose>
449 </xsl:template>
450
451 </xsl:stylesheet>
452
453