3 <!-- Copyright (C) 2000, HELM Team -->
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. -->
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. -->
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. -->
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. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <xsl:stylesheet version="0.1" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
29 <xsl:param name="CICURI" select="''"/>
31 <!-- <xsl:output method="html"/> -->
32 <xsl:output method="xml"/>
35 <xsl:template match="/">
37 <xsl:text>
</xsl:text>
38 <xsl:apply-templates select="*"/>
45 <!-- AGGIUNGERE cic: alle uri nei file Theory -->
48 <xsl:template match="InductiveDefinition">
49 <!-- The case of Inductive Definitions is peculiar due to REL -->
50 <!-- Before reading this part, first look at the otherwise case -->
51 <xsl:variable name="block" select="."/>
52 <xsl:for-each select="InductiveType">
53 <xsl:variable name="noType" select="position()"/>
54 <xsl:for-each select="Constructor/*[1]">
55 <xsl:variable name="noConstr" select="position()"/>
56 <xsl:variable name="my_uri"
57 select="concat($CICURI,'#','xpointer(1/',$noType,'/',$noConstr,
59 <xsl:comment><xsl:value-of select="concat($CICURI,'#','xpointer(1/',$noType,')')"/></xsl:comment>
60 <xsl:text>
</xsl:text>
61 <main uri="{$my_uri}"/>
62 <xsl:text>
</xsl:text>
63 <xsl:variable name="inside_concl">
64 <xsl:call-template name="look_for_main">
65 <xsl:with-param name="current" select="."/>
68 <xsl:call-template name="build_pairs">
69 <xsl:with-param name="uri" select="$my_uri"/>
70 <xsl:with-param name="list" select="$inside_concl"/>
71 <xsl:with-param name="kind" select="'in_conclusion'"/>
73 <xsl:variable name="main_hypothesis">
74 <xsl:call-template name="look_for_main_hypothesis_of_constructor">
75 <xsl:with-param name="current" select="."/>
76 <xsl:with-param name="list" select="''"/>
77 <xsl:with-param name="inductive_block" select="$block"/>
78 <xsl:with-param name="inductive_uri" select="$CICURI"/>
81 <xsl:call-template name="build_pairs">
82 <xsl:with-param name="uri" select="$my_uri"/>
83 <xsl:with-param name="list" select="$main_hypothesis"/>
84 <xsl:with-param name="kind" select="'main_hypothesis'"/>
86 <xsl:variable name="inside_hypothesis">
87 <xsl:call-template name="look_for_hypothesis">
88 <xsl:with-param name="current" select="."/>
89 <xsl:with-param name="list" select="''"/>
90 <xsl:with-param name="not_in" select="$main_hypothesis"/>
93 <xsl:call-template name="build_pairs">
94 <xsl:with-param name="uri" select="$my_uri"/>
95 <xsl:with-param name="list" select="$inside_hypothesis"/>
96 <xsl:with-param name="kind" select="'in_hypothesis'"/>
102 <xsl:template match="Definition|Axiom|CurrentProof|Variable">
103 <!-- Definition, Axiom, CurrentProof and Variable -->
104 <!-- all of them have a type -->
105 <!-- first look for the main target of the type -->
106 <!-- inside_concl contains the list of all identifiers occurring -->
107 <!-- in the main target of the type. The main identifiers, if it -->
108 <!-- exists, is in head position, separated by a comma form the -->
109 <!-- other elements. All other elements are separated by a semicolon -->
110 <xsl:variable name="inside_concl">
111 <xsl:call-template name="look_for_main">
112 <xsl:with-param name="current" select="type/*[1]"/>
115 <!-- variable main contains the (possibly empty) uri of the "main"
117 <xsl:variable name="main" select="substring-before($inside_concl,',')"/>
119 <xsl:when test="$main = ''">
120 <xsl:call-template name="build_pairs">
121 <xsl:with-param name="uri" select="$CICURI"/>
122 <xsl:with-param name="list" select="$inside_concl"/>
123 <xsl:with-param name="kind" select="'in_conclusion'"/>
127 <xsl:comment><xsl:value-of select="$main"/></xsl:comment>
128 <xsl:text>
</xsl:text>
129 <main uri="{$CICURI}"/>
130 <xsl:text>
</xsl:text>
131 <xsl:call-template name="build_pairs">
132 <xsl:with-param name="uri" select="$CICURI"/>
133 <xsl:with-param name="list" select="substring-after($inside_concl,',')"/>
134 <xsl:with-param name="kind" select="'in_conclusion'"/>
138 <!-- now look for the main identifiers inside the hipothesis -->
139 <xsl:variable name="main_hypothesis">
140 <xsl:call-template name="look_for_main_hypothesis">
141 <xsl:with-param name="current" select="type/*[1]"/>
142 <xsl:with-param name="list" select="''"/>
145 <xsl:call-template name="build_pairs">
146 <xsl:with-param name="uri" select="$CICURI"/>
147 <xsl:with-param name="list" select="$main_hypothesis"/>
148 <xsl:with-param name="kind" select="'main_hypothesis'"/>
150 <!-- now look for the all other identifiers inside the hipothesis -->
151 <xsl:variable name="inside_hypothesis">
152 <xsl:call-template name="look_for_hypothesis">
153 <xsl:with-param name="current" select="type/*[1]"/>
154 <xsl:with-param name="list" select="''"/>
155 <xsl:with-param name="not_in" select="$main_hypothesis"/>
158 <xsl:call-template name="build_pairs">
159 <xsl:with-param name="uri" select="$CICURI"/>
160 <xsl:with-param name="list" select="$inside_hypothesis"/>
161 <xsl:with-param name="kind" select="'in_hypothesis'"/>
163 <!-- Definition, Axiom, CurrentProof and Variable possibly -->
166 <xsl:variable name="inside_body">
167 <xsl:call-template name="list_all">
168 <xsl:with-param name="node" select="body/*[1]"/>
169 <xsl:with-param name="not_in" select="concat($inside_hypothesis,';',$main_hypothesis,';',$inside_concl)"/>
172 <xsl:call-template name="build_pairs">
173 <xsl:with-param name="uri" select="$CICURI"/>
174 <xsl:with-param name="list" select="$inside_body"/>
175 <xsl:with-param name="kind" select="'in_body'"/>
180 <!-- look_for_main recursively descend along the type looking for -->
181 <!-- the main target. Then returns the list of all identifiers occurring -->
182 <!-- in it. The main identifiers, if it exists, is in head position, -->
183 <!-- separated by a comma form the other elements. -->
184 <!-- All other elements are separated by a semicolon -->
186 <xsl:template name="look_for_main">
187 <xsl:param name="current" select="/.."/>
189 <xsl:when test="name($current) = 'PROD'">
190 <xsl:call-template name="look_for_main">
191 <xsl:with-param name="current" select="$current/target/*[1]"/>
195 <xsl:variable name="main">
197 <xsl:when test="name($current) = 'APPLY'">
198 <xsl:call-template name="get_expanded_name">
199 <xsl:with-param name="node" select="$current/*[1]"/>
203 <xsl:call-template name="get_expanded_name">
204 <xsl:with-param name="node" select="$current"/>
210 <xsl:when test="$main != ''">
211 <xsl:value-of select="$main"/><xsl:text>,</xsl:text>
212 <xsl:call-template name="list_all">
213 <xsl:with-param name="node" select="$current"/>
214 <xsl:with-param name="not_in" select="$main"/>
218 <xsl:call-template name="list_all">
219 <xsl:with-param name="node" select="$current"/>
220 <xsl:with-param name="not_in" select="''"/>
228 <!-- in case "node" is a CONST, MUTIND or MUTCONSTRUCT, the -->
229 <!-- function get_expanded_name returns the (expanded) uri of the -->
230 <!-- node. Otherwise it returns an empty string -->
232 <xsl:template name="get_expanded_name">
233 <xsl:param name="node" select="/.."/>
235 <xsl:when test="name($node)='CONST'">
236 <xsl:value-of select="$node/@uri"/>
238 <xsl:when test="name($node)='MUTIND'">
239 <xsl:variable name="noType" select="$node/@noType + 1"/>
240 <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
243 <xsl:when test="name($node)='MUTCONSTRUCT'">
244 <xsl:variable name="noType" select="$node/@noType + 1"/>
245 <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
246 $noType,'/',$node/@noConstr,')')"/>
252 <xsl:template name="get_expanded_name_with_rel_case">
253 <xsl:param name="node" select="/.."/>
254 <xsl:param name="inductive_block" select="/.."/>
255 <xsl:param name="inductive_uri" select="''"/>
257 <xsl:when test="name($node)='CONST'">
258 <xsl:value-of select="$node/@uri"/>
260 <xsl:when test="name($node)='MUTIND'">
261 <xsl:variable name="noType" select="$node/@noType + 1"/>
262 <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
265 <xsl:when test="name($node)='MUTCONSTRUCT'">
266 <xsl:variable name="noType" select="$node/@noType + 1"/>
267 <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
268 $noType,'/',$node/@noConstr,')')"/>
270 <xsl:when test="name($node)='REL'">
271 <xsl:variable name="binder" select="$node/@binder"/>
272 <xsl:if test="$inductive_block/InductiveType[@name=$binder]">
273 <xsl:variable name="position">
274 <xsl:for-each select="$inductive_block/InductiveType">
275 <xsl:if test="@name=$binder">
276 <xsl:value-of select="position()"/>
280 <xsl:value-of select="concat($inductive_uri,'#','xpointer(1/',
287 <!-- The function look_for_main_hypothesis returns the list of all
288 the uris of identifiers occurring in head position of some
289 of the hypothesis -->
291 <xsl:template name="look_for_main_hypothesis">
292 <xsl:param name="current" select="/.."/>
293 <xsl:param name="list" select="''"/>
295 <xsl:when test="name($current) = 'PROD'">
296 <xsl:variable name="source" select="$current/source/*[1]"/>
297 <xsl:variable name="main">
299 <xsl:when test="name($source) = 'APPLY'">
300 <xsl:call-template name="get_expanded_name">
301 <xsl:with-param name="node" select="$source/*[1]"/>
305 <xsl:call-template name="get_expanded_name">
306 <xsl:with-param name="node" select="$source"/>
312 <xsl:when test="($main != '') and (not(contains($list,$main)))">
313 <xsl:call-template name="look_for_main_hypothesis">
314 <xsl:with-param name="current" select="$current/target/*[1]"/>
315 <xsl:with-param name="list" select="concat($main,';',$list)"/>
319 <xsl:call-template name="look_for_main_hypothesis">
320 <xsl:with-param name="current" select="$current/target/*[1]"/>
321 <xsl:with-param name="list" select="$list"/>
327 <xsl:value-of select="$list"/>
332 <xsl:template name="look_for_main_hypothesis_of_constructor">
333 <xsl:param name="current" select="/.."/>
334 <xsl:param name="list" select="''"/>
335 <xsl:param name="inductive_block" select="/.."/>
336 <xsl:param name="inductive_uri" select="''"/>
338 <xsl:when test="name($current) = 'PROD'">
339 <xsl:variable name="source" select="$current/source/*[1]"/>
340 <xsl:variable name="main">
342 <xsl:when test="name($source) = 'APPLY'">
343 <xsl:call-template name="get_expanded_name_with_rel_case">
344 <xsl:with-param name="node" select="$source/*[1]"/>
345 <xsl:with-param name="inductive_block" select="$inductive_block"/>
346 <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
350 <xsl:call-template name="get_expanded_name_with_rel_case">
351 <xsl:with-param name="node" select="$source"/>
352 <xsl:with-param name="inductive_block" select="$inductive_block"/>
353 <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
359 <xsl:when test="($main != '') and (not(contains($list,$main)))">
360 <xsl:call-template name="look_for_main_hypothesis_of_constructor">
361 <xsl:with-param name="current" select="$current/target/*[1]"/>
362 <xsl:with-param name="list" select="concat($main,';',$list)"/>
363 <xsl:with-param name="inductive_block" select="$inductive_block"/>
364 <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
368 <xsl:call-template name="look_for_main_hypothesis_of_constructor">
369 <xsl:with-param name="current" select="$current/target/*[1]"/>
370 <xsl:with-param name="list" select="$list"/>
371 <xsl:with-param name="inductive_block" select="$inductive_block"/>
372 <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
378 <xsl:value-of select="$list"/>
383 <!-- look_for_hypothesis returns the list of uris of all other
384 identifiers occurring inside the hypothesis -->
386 <xsl:template name="look_for_hypothesis">
387 <xsl:param name="current" select="/.."/>
388 <xsl:param name="list" select="''"/>
389 <xsl:param name="not_in" select="''"/>
391 <xsl:when test="name($current) = 'PROD'">
392 <xsl:variable name="source" select="$current/source/*[1]"/>
393 <xsl:variable name="add_to_list">
394 <xsl:call-template name="list_all">
395 <xsl:with-param name="node" select="$source"/>
396 <xsl:with-param name="not_in" select="$not_in"/>
399 <xsl:call-template name="look_for_hypothesis">
400 <xsl:with-param name="current" select="$current/target/*[1]"/>
401 <xsl:with-param name="list" select="concat($list,$add_to_list)"/>
402 <xsl:with-param name="not_in" select="concat($not_in,$add_to_list)"/>
406 <xsl:value-of select="$list"/>
411 <!-- list_all returns a list of all uris of CONST, MUTIND, and MUTCONSTRUCT -->
412 <!-- elements appearing inside a given node, and not already contained -->
413 <!-- in the not_in list -->
415 <xsl:template name="list_all">
416 <xsl:param name="node" select="/.."/>
417 <xsl:param name="not_in" select="''"/>
418 <xsl:variable name="all">
420 <xsl:when test="$not_in = ''">
421 <xsl:for-each select="$node//*[name()='CONST' or name()='MUTIND' or name()='MUTCONSTRUCT']">
422 <xsl:sort select="@uri"/>
423 <xsl:sort select="@noType"/>
424 <xsl:sort select="@noConstr"/>
425 <xsl:call-template name="get_expanded_name">
426 <xsl:with-param name="node" select="."/>
428 <xsl:text>;</xsl:text>
432 <xsl:for-each select="$node//*[(name()='CONST' and not(contains($not_in,@uri))) or (name()='MUTIND' and not(contains($not_in,concat(@uri,'#','xpointer(1/',@noType + 1,')')))) or (name()='MUTCONSTRUCT' and not(contains($not_in,concat(@uri,'#','xpointer(1/',@noType + 1,'/'
433 ,@noConstr,')'))))]">
434 <xsl:sort select="@uri"/>
435 <xsl:sort select="@noType"/>
436 <xsl:sort select="@noConstr"/>
437 <xsl:call-template name="get_expanded_name">
438 <xsl:with-param name="node" select="."/>
440 <xsl:text>;</xsl:text>
445 <xsl:call-template name="drop_repetitions">
446 <xsl:with-param name="head" select="''"/>
447 <xsl:with-param name="tail" select="$all"/>
451 <!-- This is a different possible implementation of list_all -->
452 <!-- It seems to be less effective than the previous one -->
454 <xsl:template name="list_all">
455 <xsl:param name="node" select="/.."/>
456 <xsl:param name="not_in" select="''"/>
457 <xsl:apply-templates select="$node/*[1]" mode="list_all">
458 <xsl:with-param name="not_in" select="$not_in"/>
459 </xsl:apply-templates>
462 <xsl:template match="*" mode="list_all">
463 <xsl:param name="not_in" select="''"/>
464 <xsl:variable name="uri_to_add">
466 <xsl:when test="name()='CONST' and not(contains($not_in,@uri))">
467 <xsl:value-of select="@uri"/><xsl:text>;</xsl:text>
469 <xsl:when test="name()='MUTIND' and not(contains($not_in,concat(@uri,'#',@noType)))">
470 <xsl:value-of select="concat(@uri,'#',@noType)"/><xsl:text>;</xsl:text>
472 <xsl:when test="name()='MUTCONSTRUCT' and not(contains($not_in,concat(@uri,'#',@noType,'#',@noConstr)))">
473 <xsl:value-of select="concat(@uri,'#',@noType,'#',@noConstr)"/><xsl:text>;</xsl:text>
477 <xsl:value-of select="$uri_to_add"/>
478 <xsl:variable name="child_list">
479 <xsl:if test="count(child::*) != 0">
480 <xsl:apply-templates select="*[1]" mode="list_all">
481 <xsl:with-param name="not_in" select="concat($not_in,$uri_to_add)"/>
482 </xsl:apply-templates>
485 <xsl:value-of select="$child_list"/>
486 <xsl:if test="count(following-sibling::*) != 0">
487 <xsl:apply-templates select="following-sibling::*[1]" mode="list_all">
488 <xsl:with-param name="not_in" select="concat($not_in,$uri_to_add,$child_list)"/>
489 </xsl:apply-templates>
494 <!-- The drop_repetitions function drops all repeated strigs in a -->
495 <!-- ORDERED list of strings separated by semicolons -->
497 <xsl:template name="drop_repetitions">
498 <xsl:param name="head" select="''"/>
499 <xsl:param name="tail" select="''"/>
500 <xsl:if test="not($tail = '')">
501 <xsl:variable name="newhead" select="substring-before($tail,';')"/>
502 <xsl:variable name="newtail" select="substring-after($tail,';')"/>
503 <xsl:if test="not($newhead = $head)">
504 <xsl:value-of select="$newhead"/><xsl:text>;</xsl:text>
506 <xsl:call-template name="drop_repetitions">
507 <xsl:with-param name="head" select="$newhead"/>
508 <xsl:with-param name="tail" select="$newtail"/>
513 <!-- the function build_pairs takes in input a uri (uri), -->
514 <!-- a list of uris (list) and a "kind" string, and returns -->
515 <!-- a list of xml elements name "kind containing as first -->
516 <!-- attribute an element of the list and as second attribute -->
517 <!-- the given uri -->
518 <xsl:template name="build_pairs">
519 <xsl:param name="uri" select="''"/>
520 <xsl:param name="list" select="''"/>
521 <xsl:param name="kind" select="''"/>
522 <xsl:if test="$list != ''">
523 <xsl:variable name="head" select="substring-before($list,';')"/>
524 <xsl:variable name="tail" select="substring-after($list,';')"/>
525 <xsl:comment><xsl:value-of select="$head"/></xsl:comment>
526 <xsl:text>
</xsl:text>
527 <xsl:element name="{$kind}">
528 <xsl:attribute name="uri"><xsl:value-of select="$uri"/></xsl:attribute>
530 <xsl:text>
</xsl:text>
531 <xsl:call-template name="build_pairs">
532 <xsl:with-param name="uri" select="$uri"/>
533 <xsl:with-param name="list" select="$tail"/>
534 <xsl:with-param name="kind" select="$kind"/>