3 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
4 xmlns:m="http://www.w3.org/1998/Math/MathML"
5 xmlns:helm="http://www.cs.unibo.it/helm"
6 xmlns:oxsl="http://www.w3.org/1999/XSL/TransformAlias">
8 <xsl:output method="xml"/>
10 <xsl:namespace-alias stylesheet-prefix="oxsl" result-prefix="xsl"/>
12 <xsl:template match="OpList">
13 <xsl:comment> Copyright (C) 2000, HELM Team </xsl:comment>
14 <xsl:comment> </xsl:comment>
15 <xsl:comment> This file is part of HELM, an Hypertextual, Electronic </xsl:comment>
16 <xsl:comment> Library of Mathematics, developed at the Computer Science </xsl:comment>
17 <xsl:comment> Department, University of Bologna, Italy. </xsl:comment>
18 <xsl:comment> </xsl:comment>
19 <xsl:comment> HELM is free software; you can redistribute it and/or </xsl:comment>
20 <xsl:comment> modify it under the terms of the GNU General Public License </xsl:comment>
21 <xsl:comment> as published by the Free Software Foundation; either version 2 </xsl:comment>
22 <xsl:comment> of the License, or (at your option) any later version. </xsl:comment>
23 <xsl:comment> </xsl:comment>
24 <xsl:comment> HELM is distributed in the hope that it will be useful, </xsl:comment>
25 <xsl:comment> but WITHOUT ANY WARRANTY; without even the implied warranty of </xsl:comment>
26 <xsl:comment> MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the </xsl:comment>
27 <xsl:comment> GNU General Public License for more details. </xsl:comment>
28 <xsl:comment> </xsl:comment>
29 <xsl:comment> You should have received a copy of the GNU General Public License </xsl:comment>
30 <xsl:comment> along with HELM; if not, write to the Free Software </xsl:comment>
31 <xsl:comment> Foundation, Inc., 59 Temple Place - Suite 330, Boston, </xsl:comment>
32 <xsl:comment> MA 02111-1307, USA. </xsl:comment>
33 <xsl:comment> </xsl:comment>
34 <xsl:comment> For details, see the HELM World-Wide-Web page, </xsl:comment>
35 <xsl:comment> http://cs.unibo.it/helm/. </xsl:comment>
37 <oxsl:stylesheet version="1.0">
38 <xsl:apply-templates/>
42 <xsl:template match="import">
43 <oxsl:import href="{@href}"/>
46 <xsl:template match="include">
47 <oxsl:include href="{@href}"/>
51 <xsl:template match="Operator|NotOperator">
52 <xsl:variable name="uri">
53 <xsl:call-template name="remove_white_spaces">
54 <xsl:with-param name="uri" select="@uri"/>
58 <xsl:variable name="not">
60 <xsl:when test="name() = 'Operator'">false</xsl:when>
61 <xsl:otherwise>true</xsl:otherwise>
65 <xsl:variable name="const">
66 <xsl:value-of select="@arity = 0 and @hide = 0 and @cook = 'false'"/>
70 <xsl:when test="$const = 'true' and $not = 'true'">
71 <xsl:call-template name="out_comment">
72 <xsl:with-param name="name" select="concat($uri,': "not" cannot be applyed to a constant operator')"/>
76 <!-- All uris in uri1 list (if not empty) have CONST c-tag -->
77 <xsl:variable name="uri1">
78 <xsl:call-template name="select_uris">
79 <xsl:with-param name="uris" select="$uri"/>
80 <xsl:with-param name="c-tag" select="'CONST'"/>
84 <!-- All uris in uri2 list (if not empty) have MUTIND c-tag -->
85 <xsl:variable name="uri2">
86 <xsl:call-template name="select_uris">
87 <xsl:with-param name="uris" select="$uri"/>
88 <xsl:with-param name="c-tag" select="'MUTIND'"/>
92 <xsl:if test="$uri1 != ''">
93 <xsl:call-template name="out_template">
94 <xsl:with-param name="name" select="@name"/>
95 <xsl:with-param name="not" select="$not"/>
96 <xsl:with-param name="uri" select="$uri1"/>
97 <xsl:with-param name="hide" select="@hide"/>
98 <xsl:with-param name="arity" select="@arity"/>
99 <xsl:with-param name="m-tag" select="@m-tag"/>
100 <xsl:with-param name="c-tag" select="'CONST'"/>
101 <xsl:with-param name="const" select="$const"/>
103 <xsl:if test="@cook = 'true'">
104 <xsl:call-template name="out_template">
105 <xsl:with-param name="name" select="@name"/>
106 <xsl:with-param name="not" select="$not"/>
107 <xsl:with-param name="uri" select="$uri1"/>
108 <xsl:with-param name="cook" select="@cook"/>
109 <xsl:with-param name="hide" select="@hide"/>
110 <xsl:with-param name="arity" select="@arity"/>
111 <xsl:with-param name="m-tag" select="@m-tag"/>
112 <xsl:with-param name="c-tag" select="'CONST'"/>
117 <xsl:if test="$uri2 != ''">
118 <xsl:call-template name="out_template">
119 <xsl:with-param name="name" select="@name"/>
120 <xsl:with-param name="not" select="$not"/>
121 <xsl:with-param name="uri" select="$uri2"/>
122 <xsl:with-param name="hide" select="@hide"/>
123 <xsl:with-param name="arity" select="@arity"/>
124 <xsl:with-param name="m-tag" select="@m-tag"/>
125 <xsl:with-param name="c-tag" select="'MUTIND'"/>
126 <xsl:with-param name="const" select="$const"/>
128 <xsl:if test="@cook = 'true'">
129 <xsl:call-template name="out_template">
130 <xsl:with-param name="name" select="@name"/>
131 <xsl:with-param name="not" select="$not"/>
132 <xsl:with-param name="uri" select="$uri2"/>
133 <xsl:with-param name="cook" select="@cook"/>
134 <xsl:with-param name="hide" select="@hide"/>
135 <xsl:with-param name="arity" select="@arity"/>
136 <xsl:with-param name="m-tag" select="@m-tag"/>
137 <xsl:with-param name="c-tag" select="'MUTIND'"/>
145 <xsl:template match="OpSet|NotOpSet">
146 <xsl:variable name="uri">
147 <xsl:call-template name="remove_white_spaces">
148 <xsl:with-param name="uri" select="@uri"/>
152 <xsl:variable name="not">
154 <xsl:when test="name() = 'OpSet'">false</xsl:when>
155 <xsl:otherwise>true</xsl:otherwise>
159 <xsl:variable name="const">
160 <xsl:value-of select="*[name() = 'Case']/@arity = 0 and @hide = 0 and @cook = 'false'"/>
164 <xsl:when test="$const = 'true' and $not = 'true'">
165 <xsl:call-template name="out_comment">
166 <xsl:with-param name="name" select="concat($uri,': "not" cannot be applyed to a constant operator')"/>
169 <xsl:when test="$const = 'true'">
170 <xsl:call-template name="out_comment">
171 <xsl:with-param name="name" select="concat($uri,': cannot be specified a constant operator when using OpSet element')"/>
175 <xsl:variable name="uri1">
176 <xsl:call-template name="select_uris">
177 <xsl:with-param name="uris" select="$uri"/>
178 <xsl:with-param name="c-tag" select="'CONST'"/>
182 <xsl:variable name="uri2">
183 <xsl:call-template name="select_uris">
184 <xsl:with-param name="uris" select="$uri"/>
185 <xsl:with-param name="c-tag" select="'MUTIND'"/>
189 <xsl:if test="$uri1 != ''">
190 <xsl:call-template name="out_template_set">
191 <xsl:with-param name="name" select="@name"/>
192 <xsl:with-param name="not" select="$not"/>
193 <xsl:with-param name="uri" select="$uri1"/>
194 <xsl:with-param name="hide" select="@hide"/>
195 <xsl:with-param name="m-tag" select="@m-tag"/>
196 <xsl:with-param name="c-tag" select="'CONST'"/>
198 <xsl:if test="@cook = 'true'">
199 <xsl:call-template name="out_template_set">
200 <xsl:with-param name="name" select="@name"/>
201 <xsl:with-param name="not" select="$not"/>
202 <xsl:with-param name="uri" select="$uri1"/>
203 <xsl:with-param name="cook" select="@cook"/>
204 <xsl:with-param name="hide" select="@hide"/>
205 <xsl:with-param name="m-tag" select="@m-tag"/>
206 <xsl:with-param name="c-tag" select="'CONST'"/>
211 <xsl:if test="$uri2 != ''">
212 <xsl:call-template name="out_template_set">
213 <xsl:with-param name="name" select="@name"/>
214 <xsl:with-param name="not" select="$not"/>
215 <xsl:with-param name="uri" select="$uri2"/>
216 <xsl:with-param name="hide" select="@hide"/>
217 <xsl:with-param name="m-tag" select="@m-tag"/>
218 <xsl:with-param name="c-tag" select="'MUTIND'"/>
220 <xsl:if test="@cook = 'true'">
221 <xsl:call-template name="out_template_set">
222 <xsl:with-param name="name" select="@name"/>
223 <xsl:with-param name="not" select="$not"/>
224 <xsl:with-param name="uri" select="$uri2"/>
225 <xsl:with-param name="cook" select="@cook"/>
226 <xsl:with-param name="hide" select="@hide"/>
227 <xsl:with-param name="m-tag" select="@m-tag"/>
228 <xsl:with-param name="c-tag" select="'MUTIND'"/>
236 <!-- *********************************************************************** -->
237 <!-- MAIN FUNCTIONS -->
238 <!-- *********************************************************************** -->
241 <xsl:template name="out_template">
242 <xsl:param name="name"/>
243 <xsl:param name="not" select="'false'"/>
244 <xsl:param name="uri"/>
245 <xsl:param name="cook" select="'false'"/>
246 <xsl:param name="hide" select="0"/>
247 <xsl:param name="arity" select="0"/>
248 <xsl:param name="m-tag"/>
249 <xsl:param name="c-tag"/>
250 <xsl:param name="const" select="'false'"/>
252 <xsl:variable name="match">
253 <xsl:variable name="match_op">
254 <xsl:call-template name="out_match_op">
255 <xsl:with-param name="not" select="$not"/>
256 <xsl:with-param name="uri" select="$uri"/>
257 <xsl:with-param name="cook" select="$cook"/>
258 <xsl:with-param name="c-tag" select="$c-tag"/>
262 <xsl:variable name="match_child">
263 <xsl:if test="$const = 'false'">
265 <!-- if the operator has been concatenated with not, the root apply node must have only two child -->
266 <xsl:when test="$not = 'true'">
267 <xsl:value-of select="concat(' and count(*) = 2 and count(*[2]/*) = ',$arity + $hide + 1)"/>
270 <xsl:value-of select="concat(' and count(*) = ',$arity + $hide + 1)"/>
277 <xsl:when test="$const = 'false'">
278 <xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
281 <xsl:value-of select="$match_op"/>
287 <xsl:call-template name="out_comment">
288 <xsl:with-param name="name" select="$name"/>
291 <oxsl:template match="{$match}" mode="pure">
292 <xsl:call-template name="out_body">
293 <xsl:with-param name="c-tag" select="$c-tag"/>
294 <xsl:with-param name="m-tag" select="$m-tag"/>
295 <xsl:with-param name="cook" select="$cook"/>
296 <xsl:with-param name="hide" select="$hide"/>
297 <xsl:with-param name="arity" select="$arity"/>
298 <xsl:with-param name="not" select="$not"/>
299 <xsl:with-param name="const" select="$const"/>
304 <xsl:template name="out_template_set">
305 <xsl:param name="name"/>
306 <xsl:param name="not" select="'false'"/>
307 <xsl:param name="cook" select="'false'"/>
308 <xsl:param name="uri"/>
309 <xsl:param name="hide" select="0"/>
310 <xsl:param name="m-tag"/>
311 <xsl:param name="c-tag"/>
313 <xsl:variable name="match">
314 <xsl:variable name="match_op">
315 <xsl:call-template name="out_match_op">
316 <xsl:with-param name="not" select="$not"/>
317 <xsl:with-param name="cook" select="$cook"/>
318 <xsl:with-param name="uri" select="$uri"/>
319 <xsl:with-param name="c-tag" select="$c-tag"/>
323 <xsl:variable name="match_child">
324 <xsl:if test="$not = 'true'"> and count(*) = 2</xsl:if>
327 <xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
330 <xsl:variable name="apply_not">
331 <xsl:if test="$not = 'true'">*[2]/</xsl:if>
336 <xsl:call-template name="out_comment">
337 <xsl:with-param name="name" select="$name"/>
340 <oxsl:template match="{$match}" mode="pure">
342 <xsl:for-each select="Case">
343 <oxsl:when test="{concat('count(',$apply_not,'*) = ',@arity + $hide + 1)}">
344 <xsl:call-template name="out_body">
345 <xsl:with-param name="c-tag" select="$c-tag"/>
346 <xsl:with-param name="m-tag" select="$m-tag"/>
347 <xsl:with-param name="cook" select="$cook"/>
348 <xsl:with-param name="hide" select="$hide"/>
349 <xsl:with-param name="arity" select="@arity"/>
350 <xsl:with-param name="not" select="$not"/>
355 <oxsl:apply-imports/>
361 <xsl:template name="out_comment">
362 <xsl:param name="name"/>
363 <xsl:if test="$name">
365 <xsl:value-of select="concat(' ',$name,' ')"/>
370 <!-- Returns a regular expression with matching operators -->
371 <xsl:template name="out_match_op">
372 <xsl:param name="not" select="'false'"/>
373 <xsl:param name="uri"/>
374 <xsl:param name="cook" select="'false'"/>
375 <xsl:param name="c-tag"/>
377 <xsl:variable name="instantiate">
378 <xsl:if test="$cook = 'true'">instantiate/</xsl:if>
381 <!-- application with not operator -->
382 <xsl:variable name="app_not">
383 <xsl:if test="$not = 'true'">CONST[@uri='cic:/Coq/Init/Logic/not.con'] and </xsl:if>
386 <xsl:variable name="uris">
387 <xsl:call-template name="test_on_uris">
388 <xsl:with-param name="uris" select="$uri"/>
392 <xsl:variable name="app_op">
393 <xsl:if test="$not = 'true'">APPLY[</xsl:if>
394 <xsl:value-of select="concat($instantiate,$c-tag,'[',$uris,']')"/>
395 <xsl:if test="$not = 'true'">]</xsl:if>
398 <xsl:value-of select="concat($app_not,$app_op)"/>
401 <xsl:template name="out_params">
402 <xsl:param name="params" select="1"/>
403 <xsl:param name="hide" select="0"/>
404 <xsl:param name="not" select="'false'"/>
405 <xsl:param name="mode" select="'noannot'"/>
406 <xsl:param name="arity" select="0"/>
408 <xsl:if test="$params <= $arity">
409 <xsl:variable name="param">
410 <xsl:call-template name="param">
411 <xsl:with-param name="id" select="$params"/>
412 <xsl:with-param name="not" select="$not"/>
413 <xsl:with-param name="hide" select="$hide"/>
417 <oxsl:apply-templates select="{$param}" mode="{$mode}"/>
419 <xsl:call-template name="out_params">
420 <xsl:with-param name="params" select="$params + 1"/>
421 <xsl:with-param name="hide" select="$hide"/>
422 <xsl:with-param name="not" select="$not"/>
423 <xsl:with-param name="mode" select="$mode"/>
424 <xsl:with-param name="arity" select="$arity"/>
429 <xsl:template name="out_body">
430 <xsl:param name="c-tag"/>
431 <xsl:param name="cook" select="'false'"/>
432 <xsl:param name="m-tag"/>
433 <xsl:param name="hide" select="0"/>
434 <xsl:param name="arity" select="0"/>
435 <xsl:param name="not" select="'false'"/>
436 <xsl:param name="const" select="'false'"/>
439 <!-- SIMPLE TRANSFORMATIONS -->
440 <xsl:when test="count(*) = 0">
441 <xsl:variable name="xref">
442 <xsl:if test="$const = 'false'">{@id}</xsl:if>
445 <xsl:variable name="definitionURL">
446 <xsl:call-template name="op_uri_attr">
447 <xsl:with-param name="not" select="$not"/>
448 <xsl:with-param name="cook" select="$cook"/>
449 <xsl:with-param name="c-tag" select="$c-tag"/>
450 <xsl:with-param name="const" select="$const"/>
454 <xsl:variable name="helm:xref">
455 <xsl:call-template name="op_id_attr">
456 <xsl:with-param name="not" select="$not"/>
457 <xsl:with-param name="cook" select="$cook"/>
458 <xsl:with-param name="c-tag" select="$c-tag"/>
459 <xsl:with-param name="const" select="$const"/>
464 <m:apply helm:xref="{$xref}">
466 <xsl:element name="{concat('m:',$m-tag)}">
467 <xsl:attribute name="definitionURL">
468 <xsl:value-of select="$definitionURL"/>
470 <xsl:attribute name="helm:xref">
471 <xsl:value-of select="$helm:xref"/>
475 <xsl:call-template name="out_params">
476 <xsl:with-param name="hide" select="$hide"/>
477 <xsl:with-param name="not" select="$not"/>
478 <xsl:with-param name="arity" select="$arity"/>
482 <!-- COMPLEX TRANSFORMATIONS -->
484 <xsl:apply-templates>
485 <xsl:with-param name="c-tag" select="$c-tag"/>
486 <xsl:with-param name="cook" select="$cook"/>
487 <xsl:with-param name="hide" select="$hide"/>
488 <xsl:with-param name="arity" select="$arity"/>
489 <xsl:with-param name="not" select="$not"/>
490 <xsl:with-param name="const" select="$const"/>
491 </xsl:apply-templates>
497 <xsl:template name="out_mvar">
498 <xsl:param name="vname"/>
502 <xsl:when test="(ancestor-or-self::*[preceding-sibling::*[(name() = 'mbvar') and (@name = $vname)]]/preceding-sibling::*[(name() = 'mbvar') and (@name = $vname)])[position() = last()]">
503 <oxsl:value-of select="{concat('$bvar_',$vname)}"/>
506 <xsl:value-of select="$vname"/>
513 <xsl:template name="out_choose_binder">
514 <xsl:param name="binded_params" select="''"/>
515 <xsl:param name="not" select="'false'"/>
516 <xsl:param name="hide" select="0"/>
517 <xsl:param name="binder"/>
519 <xsl:if test="$binded_params != ''">
521 <xsl:when test="contains($binded_params,'+')">
522 <xsl:call-template name="out_choose_binder">
523 <xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
524 <xsl:with-param name="not" select="$not"/>
525 <xsl:with-param name="hide" select="$hide"/>
526 <xsl:with-param name="binder" select="$binder"/>
529 <xsl:call-template name="out_choose_binder">
530 <xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
531 <xsl:with-param name="not" select="$not"/>
532 <xsl:with-param name="hide" select="$hide"/>
533 <xsl:with-param name="binder" select="$binder"/>
537 <xsl:variable name="param">
538 <xsl:call-template name="param">
539 <xsl:with-param name="id" select="$binded_params"/>
540 <xsl:with-param name="not" select="$not"/>
541 <xsl:with-param name="hide" select="$hide"/>
545 <oxsl:when test="{concat('name(',$param,') = ',"'LAMBDA'")}">
546 <oxsl:value-of select="{concat($param,$binder)}"/>
554 <!-- *********************************************************************** -->
555 <!-- META LANGUAGE FOR MathML -->
556 <!-- *********************************************************************** -->
558 <xsl:template match="mapp">
559 <xsl:param name="c-tag"/>
560 <xsl:param name="cook" select="'false'"/>
561 <xsl:param name="hide" select="0"/>
562 <xsl:param name="arity" select="0"/>
563 <xsl:param name="not" select="'false'"/>
564 <xsl:param name="const" select="'false'"/>
566 <xsl:variable name="helm:xref">
568 <xsl:when test="@xref">
569 <xsl:call-template name="set_attribute">
570 <xsl:with-param name="attr" select="@xref"/>
571 <xsl:with-param name="c-tag" select="$c-tag"/>
572 <xsl:with-param name="cook" select="$cook"/>
573 <xsl:with-param name="hide" select="$hide"/>
574 <xsl:with-param name="arity" select="$arity"/>
575 <xsl:with-param name="not" select="$not"/>
576 <xsl:with-param name="const" select="$const"/>
580 <xsl:if test="$const = 'false'">{@id}</xsl:if>
585 <m:apply helm:xref="{$helm:xref}">
586 <xsl:call-template name="copy_attributes">
587 <xsl:with-param name="cook" select="$cook"/>
588 <xsl:with-param name="c-tag" select="$c-tag"/>
589 <xsl:with-param name="hide" select="$hide"/>
590 <xsl:with-param name="arity" select="$arity"/>
591 <xsl:with-param name="not" select="$not"/>
592 <xsl:with-param name="const" select="$const"/>
593 <xsl:with-param name="ignore" select="'xref'"/>
596 <xsl:apply-templates>
597 <xsl:with-param name="c-tag" select="$c-tag"/>
598 <xsl:with-param name="cook" select="$cook"/>
599 <xsl:with-param name="hide" select="$hide"/>
600 <xsl:with-param name="arity" select="$arity"/>
601 <xsl:with-param name="not" select="$not"/>
602 <xsl:with-param name="const" select="$const"/>
603 </xsl:apply-templates>
607 <xsl:template match="mop">
608 <xsl:param name="c-tag"/>
609 <xsl:param name="cook" select="'false'"/>
610 <xsl:param name="hide" select="0"/>
611 <xsl:param name="arity" select="0"/>
612 <xsl:param name="not" select="'false'"/>
613 <xsl:param name="const" select="'false'"/>
615 <!-- set definitonURL attribute -->
616 <xsl:variable name="definitionURL">
618 <xsl:when test="@definitionURL">
619 <xsl:call-template name="set_attribute">
620 <xsl:with-param name="attr" select="@definitionURL"/>
621 <xsl:with-param name="cook" select="$cook"/>
622 <xsl:with-param name="c-tag" select="$c-tag"/>
623 <xsl:with-param name="hide" select="$hide"/>
624 <xsl:with-param name="arity" select="$arity"/>
625 <xsl:with-param name="not" select="$not"/>
626 <xsl:with-param name="const" select="$const"/>
630 <xsl:call-template name="op_uri_attr">
631 <xsl:with-param name="not" select="$not"/>
632 <xsl:with-param name="cook" select="$cook"/>
633 <xsl:with-param name="c-tag" select="$c-tag"/>
634 <xsl:with-param name="const" select="$const"/>
640 <!-- set helm:xref attribute -->
641 <xsl:variable name="helm:xref">
643 <xsl:when test="@xref">
644 <xsl:call-template name="set_attribute">
645 <xsl:with-param name="attr" select="@xref"/>
646 <xsl:with-param name="cook" select="$cook"/>
647 <xsl:with-param name="c-tag" select="$c-tag"/>
648 <xsl:with-param name="hide" select="$hide"/>
649 <xsl:with-param name="arity" select="$arity"/>
650 <xsl:with-param name="not" select="$not"/>
651 <xsl:with-param name="const" select="$const"/>
655 <xsl:call-template name="op_id_attr">
656 <xsl:with-param name="not" select="$not"/>
657 <xsl:with-param name="cook" select="$cook"/>
658 <xsl:with-param name="c-tag" select="$c-tag"/>
659 <xsl:with-param name="const" select="$const"/>
665 <xsl:element name="{concat('m:',@tag)}">
666 <xsl:attribute name="definitionURL">
667 <xsl:value-of select="$definitionURL"/>
669 <xsl:attribute name="helm:xref">
670 <xsl:value-of select="$helm:xref"/>
673 <xsl:call-template name="copy_attributes">
674 <xsl:with-param name="cook" select="$cook"/>
675 <xsl:with-param name="c-tag" select="$c-tag"/>
676 <xsl:with-param name="hide" select="$hide"/>
677 <xsl:with-param name="arity" select="$arity"/>
678 <xsl:with-param name="not" select="$not"/>
679 <xsl:with-param name="const" select="$const"/>
680 <xsl:with-param name="ignore" select="'xref + definitionURL + tag'"/>
683 <xsl:apply-templates>
684 <xsl:with-param name="c-tag" select="$c-tag"/>
685 <xsl:with-param name="cook" select="$cook"/>
686 <xsl:with-param name="hide" select="$hide"/>
687 <xsl:with-param name="arity" select="$arity"/>
688 <xsl:with-param name="not" select="$not"/>
689 <xsl:with-param name="const" select="$const"/>
690 </xsl:apply-templates>
695 <xsl:template match="param">
696 <xsl:param name="hide" select="0"/>
697 <xsl:param name="not" select="'false'"/>
699 <xsl:variable name="param">
700 <xsl:call-template name="param">
701 <xsl:with-param name="id" select="@id"/>
702 <xsl:with-param name="not" select="$not"/>
703 <xsl:with-param name="hide" select="$hide"/>
708 <xsl:when test="@bvar">
710 <oxsl:when test="{concat('name(',$param,') = ',"'LAMBDA'")}">
711 <oxsl:apply-templates select="{concat($param,'/target')}" mode="{@mode}"/>
715 <m:csymbol>app</m:csymbol>
716 <oxsl:apply-templates select="{$param}" mode="{@mode}"/>
718 <xsl:value-of select="@bvar"/>
725 <oxsl:apply-templates select="{$param}" mode="{@mode}"/>
731 <xsl:template match="m:*">
732 <xsl:param name="c-tag"/>
733 <xsl:param name="cook" select="'false'"/>
734 <xsl:param name="hide" select="0"/>
735 <xsl:param name="arity" select="0"/>
736 <xsl:param name="not" select="'false'"/>
737 <xsl:param name="const" select="'false'"/>
740 <xsl:call-template name="copy_attributes">
741 <xsl:with-param name="cook" select="$cook"/>
742 <xsl:with-param name="c-tag" select="$c-tag"/>
743 <xsl:with-param name="hide" select="$hide"/>
744 <xsl:with-param name="arity" select="$arity"/>
745 <xsl:with-param name="not" select="$not"/>
746 <xsl:with-param name="const" select="$const"/>
749 <xsl:apply-templates>
750 <xsl:with-param name="c-tag" select="$c-tag"/>
751 <xsl:with-param name="cook" select="$cook"/>
752 <xsl:with-param name="hide" select="$hide"/>
753 <xsl:with-param name="arity" select="$arity"/>
754 <xsl:with-param name="not" select="$not"/>
755 <xsl:with-param name="const" select="$const"/>
756 </xsl:apply-templates>
761 <xsl:template match="mbvar">
762 <xsl:param name="c-tag"/>
763 <xsl:param name="cook" select="'false'"/>
764 <xsl:param name="hide" select="0"/>
765 <xsl:param name="arity" select="0"/>
766 <xsl:param name="not" select="'false'"/>
767 <xsl:param name="const" select="'false'"/>
769 <xsl:variable name="binded_params">
770 <xsl:call-template name="get_binded_params">
771 <xsl:with-param name="var" select="@name"/>
772 <xsl:with-param name="node" select="following-sibling::*"/>
776 <xsl:variable name="test">
777 <xsl:call-template name="test_on_lambda">
778 <xsl:with-param name="binded_params" select="$binded_params"/>
779 <xsl:with-param name="not" select="$not"/>
780 <xsl:with-param name="hide" select="$hide"/>
784 <xsl:variable name="binder">/decl/@binder</xsl:variable>
787 <xsl:when test="$binded_params != ''">
788 <oxsl:variable name="{concat('bvar_',@name)}">
790 <!-- one or more lambdas exist -->
791 <oxsl:when test="{$test}">
793 <!-- binded params > 1 (more than 1 lambda) -->
794 <xsl:when test="contains($binded_params,'+')">
795 <oxsl:variable name="binder">
797 <xsl:call-template name="out_choose_binder">
798 <xsl:with-param name="binded_params" select="$binded_params"/>
799 <xsl:with-param name="not" select="$not"/>
800 <xsl:with-param name="hide" select="$hide"/>
801 <xsl:with-param name="binder" select="$binder"/>
805 <oxsl:call-template name="insert_subscript">
806 <oxsl:with-param name="node_value" select="$binder"/>
807 </oxsl:call-template>
809 <!-- binded parms = 1 (1 lambda) -->
811 <xsl:variable name="param">
812 <xsl:call-template name="param">
813 <xsl:with-param name="id" select="$binded_params"/>
814 <xsl:with-param name="not" select="$not"/>
815 <xsl:with-param name="hide" select="$hide"/>
819 <oxsl:call-template name="insert_subscript">
820 <oxsl:with-param name="node_value" select="{concat($param,$binder)}"/>
821 </oxsl:call-template>
825 <!-- no one lambda -->
827 <xsl:value-of select="@name"/>
834 <oxsl:value-of select="{concat('$bvar_',@name)}"/>
836 <xsl:apply-templates>
837 <xsl:with-param name="c-tag" select="$c-tag"/>
838 <xsl:with-param name="cook" select="$cook"/>
839 <xsl:with-param name="hide" select="$hide"/>
840 <xsl:with-param name="arity" select="$arity"/>
841 <xsl:with-param name="not" select="$not"/>
842 <xsl:with-param name="const" select="$const"/>
843 </xsl:apply-templates>
849 <xsl:value-of select="@name"/>
851 <xsl:apply-templates>
852 <xsl:with-param name="c-tag" select="$c-tag"/>
853 <xsl:with-param name="cook" select="$cook"/>
854 <xsl:with-param name="hide" select="$hide"/>
855 <xsl:with-param name="arity" select="$arity"/>
856 <xsl:with-param name="not" select="$not"/>
857 <xsl:with-param name="const" select="$const"/>
858 </xsl:apply-templates>
866 <xsl:template match="mvar">
867 <xsl:call-template name="out_mvar">
868 <xsl:with-param name="vname" select="@name"/>
873 <!-- *********************************************************************** -->
874 <!-- AUXILIARY FUNCTIONS -->
875 <!-- *********************************************************************** -->
878 <!-- Returns a value if all uris in the list have the same c-tag -->
879 <xsl:template name="get_c_tag">
880 <xsl:param name="uri" select="''"/>
882 <xsl:if test="$uri != ''">
884 <xsl:when test="contains($uri,'|')">
885 <xsl:variable name="c-tag1">
886 <xsl:call-template name="get_c_tag">
887 <xsl:with-param name="uri" select="substring-before($uri,'|')"/>
891 <xsl:variable name="c-tag2">
892 <xsl:call-template name="get_c_tag">
893 <xsl:with-param name="uri" select="substring-after($uri,'|')"/>
897 <xsl:if test="$c-tag1 = $c-tag2">
898 <xsl:value-of select="$c-tag1"/>
903 <xsl:when test="substring($uri,string-length($uri)-3) = '.con'">CONST</xsl:when>
904 <xsl:when test="substring($uri,string-length($uri)-3) = '.ind'">MUTIND</xsl:when>
911 <!-- Creates a list selecting uris according to c-tag specified -->
912 <xsl:template name="select_uris">
913 <xsl:param name="uris" select="''"/>
914 <xsl:param name="c-tag"/>
916 <xsl:if test="$uris != ''">
918 <xsl:when test="contains($uris,'|')">
919 <xsl:variable name="list1">
920 <xsl:call-template name="select_uris">
921 <xsl:with-param name="uris" select="substring-before($uris,'|')"/>
922 <xsl:with-param name="c-tag" select="$c-tag"/>
926 <xsl:variable name="list2">
927 <xsl:call-template name="select_uris">
928 <xsl:with-param name="uris" select="substring-after($uris,'|')"/>
929 <xsl:with-param name="c-tag" select="$c-tag"/>
934 <xsl:when test="$list1 != '' and $list2 != ''">
935 <xsl:value-of select="concat($list1,'|',$list2)"/>
937 <xsl:when test="$list1 != '' and $list2 = ''">
938 <xsl:value-of select="$list1"/>
940 <xsl:when test="$list1 = '' and $list2 != ''">
941 <xsl:value-of select="$list2"/>
946 <xsl:variable name="c-tag1">
947 <xsl:call-template name="get_c_tag">
948 <xsl:with-param name="uri" select="$uris"/>
952 <xsl:if test="$c-tag1 = $c-tag">
953 <xsl:value-of select="$uris"/>
960 <!-- Returns a xpath expression matching on uri attributes -->
961 <xsl:template name="test_on_uris">
962 <xsl:param name="uris" select="''"/>
964 <xsl:if test="$uris != ''">
966 <xsl:when test="contains($uris,'|')">
967 <xsl:variable name="expr1">
968 <xsl:call-template name="test_on_uris">
969 <xsl:with-param name="uris" select="substring-before($uris,'|')"/>
973 <xsl:variable name="expr2">
974 <xsl:call-template name="test_on_uris">
975 <xsl:with-param name="uris" select="substring-after($uris,'|')"/>
979 <xsl:value-of select="concat($expr1,' or ',$expr2)"/>
982 <xsl:value-of select="concat('@uri=',"'",$uris,"'")"/>
988 <!-- Returns a xpath expression testing on LAMBDA node existence -->
989 <xsl:template name="test_on_lambda">
990 <xsl:param name="binded_params" select="''"/>
991 <xsl:param name="not" select="'false'"/>
992 <xsl:param name="hide" select="0"/>
994 <xsl:if test="$binded_params != ''">
996 <xsl:when test="contains($binded_params,'+')">
997 <xsl:variable name="expr1">
998 <xsl:call-template name="test_on_lambda">
999 <xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
1000 <xsl:with-param name="not" select="$not"/>
1001 <xsl:with-param name="hide" select="$hide"/>
1002 </xsl:call-template>
1005 <xsl:variable name="expr2">
1006 <xsl:call-template name="test_on_lambda">
1007 <xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
1008 <xsl:with-param name="not" select="$not"/>
1009 <xsl:with-param name="hide" select="$hide"/>
1010 </xsl:call-template>
1013 <xsl:value-of select="concat($expr1,' or ',$expr2)"/>
1016 <xsl:variable name="param">
1017 <xsl:call-template name="param">
1018 <xsl:with-param name="id" select="$binded_params"/>
1019 <xsl:with-param name="not" select="$not"/>
1020 <xsl:with-param name="hide" select="$hide"/>
1021 </xsl:call-template>
1024 <xsl:value-of select="concat('name(',$param,') = ',"'LAMBDA'")"/>
1030 <!-- Removes white spaces from uris list -->
1031 <xsl:template name="remove_white_spaces">
1032 <xsl:param name="uri" select="''"/>
1034 <xsl:if test="$uri != ''">
1036 <xsl:when test="contains($uri,'|')">
1037 <xsl:variable name="uri1">
1038 <xsl:call-template name="remove_white_spaces">
1039 <xsl:with-param name="uri" select="substring-before($uri,'|')"/>
1040 </xsl:call-template>
1043 <xsl:variable name="uri2">
1044 <xsl:call-template name="remove_white_spaces">
1045 <xsl:with-param name="uri" select="substring-after($uri,'|')"/>
1046 </xsl:call-template>
1049 <xsl:value-of select="concat($uri1,'|',$uri2)"/>
1052 <xsl:value-of select="normalize-space($uri)"/>
1059 Returns a list of params id attributes concatenated with '+'.
1060 The params'id attribute are selected according to the value of bindig variable 'var'
1062 <xsl:template name="get_binded_params">
1063 <xsl:param name="var"/>
1064 <xsl:param name="node"/>
1066 <xsl:if test="count($node) != 0">
1068 <!-- another variable declaration with same name -->
1069 <xsl:when test="($node[1][name() = 'mbvar']) and ($node[1][@name = $var])"></xsl:when>
1070 <!-- a binded param -->
1071 <xsl:when test="($node[1][name() = 'param']) and ($node[1][@bvar = $var])">
1072 <!-- search on siblings -->
1073 <xsl:variable name="siblings_params">
1074 <xsl:call-template name="get_binded_params">
1075 <xsl:with-param name="var" select="$var"/>
1076 <xsl:with-param name="node" select="$node[position() > 1]"/>
1077 </xsl:call-template>
1080 <xsl:when test="$siblings_params != ''">
1081 <xsl:value-of select="concat($node[1]/@id,'+',$siblings_params)"/>
1084 <xsl:value-of select="$node[1]/@id"/>
1089 <!-- search on siblings -->
1090 <xsl:variable name="siblings_params">
1091 <xsl:call-template name="get_binded_params">
1092 <xsl:with-param name="var" select="$var"/>
1093 <xsl:with-param name="node" select="$node[position() > 1]"/>
1094 </xsl:call-template>
1096 <!-- search on children -->
1097 <xsl:variable name="children_params">
1098 <xsl:call-template name="get_binded_params">
1099 <xsl:with-param name="var" select="$var"/>
1100 <xsl:with-param name="node" select="$node[1]/child::*"/>
1101 </xsl:call-template>
1105 <xsl:when test="$children_params != '' and $siblings_params != ''">
1106 <xsl:value-of select="concat($children_params,'+',$siblings_params)"/>
1108 <xsl:when test="$children_params != '' and $siblings_params = ''">
1109 <xsl:value-of select="$children_params"/>
1111 <xsl:when test="$children_params = '' and $siblings_params != ''">
1112 <xsl:value-of select="$siblings_params"/>
1120 <!-- Returns a xpath string with the location of the parameter with the id specified -->
1121 <xsl:template name="param">
1122 <xsl:param name="id"/>
1123 <xsl:param name="not" select="'false'"/>
1124 <xsl:param name="hide" select="0"/>
1126 <xsl:variable name="apply_not">
1127 <xsl:if test="$not = 'true'">*[2]/</xsl:if>
1130 <xsl:value-of select="concat($apply_not,'*[',$id + $hide + 1,']')"/>
1133 <!-- Returns a xpath string with the location of the operator uri attribute -->
1134 <xsl:template name="op_uri_attr">
1135 <xsl:param name="not" select="'false'"/>
1136 <xsl:param name="cook" select="'false'"/>
1137 <xsl:param name="c-tag"/>
1138 <xsl:param name="const" select="'false'"/>
1140 <xsl:call-template name="op_attr">
1141 <xsl:with-param name="attr_type" select="'@uri'"/>
1142 <xsl:with-param name="not" select="$not"/>
1143 <xsl:with-param name="cook" select="$cook"/>
1144 <xsl:with-param name="c-tag" select="$c-tag"/>
1145 <xsl:with-param name="const" select="$const"/>
1146 </xsl:call-template>
1149 <!-- Returns a xpath string with the location of the operator id attribute -->
1150 <xsl:template name="op_id_attr">
1151 <xsl:param name="not" select="'false'"/>
1152 <xsl:param name="cook" select="'false'"/>
1153 <xsl:param name="c-tag"/>
1154 <xsl:param name="const" select="'false'"/>
1156 <xsl:call-template name="op_attr">
1157 <xsl:with-param name="attr_type" select="'@id'"/>
1158 <xsl:with-param name="not" select="$not"/>
1159 <xsl:with-param name="cook" select="$cook"/>
1160 <xsl:with-param name="c-tag" select="$c-tag"/>
1161 <xsl:with-param name="const" select="$const"/>
1162 </xsl:call-template>
1166 <!-- Returns a xpath string with the location of the operator uri or id attribute -->
1167 <xsl:template name="op_attr">
1168 <xsl:param name="attr_type"/>
1169 <xsl:param name="not" select="'false'"/>
1170 <xsl:param name="cook" select="'false'"/>
1171 <xsl:param name="c-tag"/>
1172 <xsl:param name="const" select="'false'"/>
1174 <xsl:variable name="instantiate">
1175 <xsl:if test="$cook = 'true'">instantiate/</xsl:if>
1178 <xsl:variable name="apply">
1179 <xsl:if test="$not = 'true'">APPLY/</xsl:if>
1183 <xsl:when test="$const = 'true'">
1184 <xsl:value-of select="concat('{',$attr_type,'}')"/>
1187 <xsl:value-of select="concat('{',$apply,$instantiate,$c-tag,'/',$attr_type,'}')"/>
1192 <xsl:template name="copy_attributes">
1193 <xsl:param name="cook" select="'false'"/>
1194 <xsl:param name="c-tag"/>
1195 <xsl:param name="hide" select="0"/>
1196 <xsl:param name="arity" select="0"/>
1197 <xsl:param name="not" select="'false'"/>
1198 <xsl:param name="const" select="'false'"/>
1199 <xsl:param name="ignore" select="''"/>
1201 <xsl:variable name="test">
1202 <xsl:call-template name="test_on_attributes">
1203 <xsl:with-param name="names" select="$ignore"/>
1204 </xsl:call-template>
1207 <xsl:for-each select="@*">
1208 <xsl:if test="contains($test,concat('+',name(),'+')) = false()">
1209 <xsl:variable name="name">
1211 <xsl:when test="name() = 'xref'">helm:xref</xsl:when>
1213 <xsl:value-of select="name()"/>
1218 <xsl:attribute name="{$name}">
1219 <xsl:call-template name="set_attribute">
1220 <xsl:with-param name="attr" select="."/>
1221 <xsl:with-param name="cook" select="$cook"/>
1222 <xsl:with-param name="c-tag" select="$c-tag"/>
1223 <xsl:with-param name="hide" select="$hide"/>
1224 <xsl:with-param name="arity" select="$arity"/>
1225 <xsl:with-param name="not" select="$not"/>
1226 <xsl:with-param name="const" select="$const"/>
1227 </xsl:call-template>
1233 <xsl:template name="test_on_attributes">
1234 <xsl:param name="names" select="''"/>
1237 <xsl:when test="contains($names,'+')">
1238 <xsl:variable name="name">
1239 <xsl:call-template name="test_on_attributes">
1240 <xsl:with-param name="names" select="normalize-space(substring-after($names,'+'))"/>
1241 </xsl:call-template>
1244 <xsl:value-of select="concat('+',normalize-space(substring-before($names,'+')),$name)"/>
1247 <xsl:value-of select="concat('+',normalize-space($names),'+')"/>
1252 <xsl:template name="set_attribute">
1253 <xsl:param name="attr"/>
1254 <xsl:param name="c-tag"/>
1255 <xsl:param name="cook" select="'false'"/>
1256 <xsl:param name="hide" select="0"/>
1257 <xsl:param name="arity" select="0"/>
1258 <xsl:param name="not" select="'false'"/>
1259 <xsl:param name="const" select="'false'"/>
1262 <xsl:when test="$attr = '$APP-ID'">
1263 <xsl:if test="$const = 'false'">{@id}</xsl:if>
1265 <xsl:when test="$attr = '$OP-ID' or $attr = '$OP-URI'">
1266 <xsl:variable name="attr_type">
1268 <xsl:when test="$attr = '$OP-ID'">@id</xsl:when>
1269 <xsl:otherwise>@uri</xsl:otherwise>
1273 <xsl:call-template name="op_attr">
1274 <xsl:with-param name="attr_type" select="$attr_type"/>
1275 <xsl:with-param name="not" select="$not"/>
1276 <xsl:with-param name="cook" select="$cook"/>
1277 <xsl:with-param name="c-tag" select="$c-tag"/>
1278 <xsl:with-param name="const" select="$const"/>
1279 </xsl:call-template>
1282 <xsl:value-of select="$attr"/>