]> matita.cs.unibo.it Git - helm.git/blob - helm/style/params.xsl
b5b7f9b88ee7357497be3ec9d189cc76bf11245e
[helm.git] / helm / style / params.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 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
28                               xmlns:m="http://www.w3.org/1998/Math/MathML">
29
30 <!--***********************************************************************--> 
31 <!-- auxiliary functions                                                   -->
32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
33 <!--***********************************************************************--> 
34
35 <!--***********************************************************************-->
36 <!-- get the name from a URI                                               -->
37 <!--***********************************************************************-->
38
39 <!-- CSC: PROBLEMA: URI CHE NON CONTENGONO / ED INIZIANO CON cic: -->
40 <xsl:template name="name_of_uri">
41  <xsl:param name="uri" select="&quot;&quot;"/>
42  <xsl:variable name="suffix" select="substring-after($uri, &quot;/&quot;)"/>
43  <xsl:choose>
44   <xsl:when test="$suffix = &quot;&quot;">
45    <!-- CSC: PROBLEMA: .con PUO' APPARIRE ALL'INTERNO DELLE URI ===>
46      SCRIVERE UNA FUNZIONE RICORSIVA CHE RISOLVA -->
47    <xsl:value-of select="substring-before($uri,&quot;.con&quot;)"/>
48   </xsl:when>
49   <xsl:otherwise>
50    <xsl:call-template name="name_of_uri">
51     <xsl:with-param name="uri" select="$suffix"/>
52    </xsl:call-template>
53   </xsl:otherwise>
54  </xsl:choose>
55 </xsl:template>
56
57 <!--***********************************************************************-->
58 <!-- erase common prefix from two uris                                     -->
59 <!--***********************************************************************-->
60
61 <xsl:template name="common_prefix">
62  <xsl:param name="first_uri" select="&quot;&quot;"/>
63  <xsl:param name="second_uri" select="&quot;&quot;"/>
64  <xsl:choose>
65   <xsl:when test="(substring-before($first_uri,&quot;/&quot;) = 
66                 substring-before($second_uri,&quot;/&quot;) and 
67                 substring-after($second_uri,&quot;/&quot;) != &quot;&quot;)">
68    <xsl:call-template name="common_prefix">
69     <xsl:with-param 
70         name="first_uri" select="substring-after($first_uri,&quot;/&quot;)"/>
71     <xsl:with-param 
72         name="second_uri" select="substring-after($second_uri,&quot;/&quot;)"/>    </xsl:call-template>
73   </xsl:when>
74   <xsl:otherwise>
75    <xsl:call-template name="slash_counting">
76     <xsl:with-param name="uri" select="$second_uri"/>
77     <xsl:with-param name="counter" select="0"/>
78    </xsl:call-template>
79   </xsl:otherwise>   
80  </xsl:choose>
81 </xsl:template>
82
83 <xsl:template name="slash_counting">
84  <xsl:param name="uri" select="&quot;&quot;"/>
85  <xsl:param name="counter" select="0"/>
86  <xsl:choose>
87   <xsl:when test="(substring-after($uri,&quot;/&quot;) != &quot;&quot;)">
88    <xsl:call-template name="slash_counting">
89     <xsl:with-param 
90         name="uri" select="substring-after($uri,&quot;/&quot;)"/>
91     <xsl:with-param
92         name="counter" select="$counter +1"/> 
93    </xsl:call-template>
94   </xsl:when>
95   <xsl:otherwise>
96    <xsl:value-of select="$counter"/>
97   </xsl:otherwise>
98  </xsl:choose>   
99 </xsl:template>
100
101 <xsl:template name="blank_counting">
102  <xsl:param name="string" select="&quot;&quot;"/>
103  <xsl:param name="counter" select="0"/>
104  <xsl:choose>
105   <xsl:when test="(substring-after($string,&quot; &quot;) != &quot;&quot;)">
106    <xsl:call-template name="blank_counting">
107     <xsl:with-param 
108         name="string" select="substring-after($string,&quot; &quot;)"/>
109     <xsl:with-param 
110         name="counter" select="$counter +1"/> 
111    </xsl:call-template>
112   </xsl:when>
113   <xsl:otherwise>
114    <xsl:value-of select="$counter + 1"/>
115   </xsl:otherwise> 
116  </xsl:choose>  
117 </xsl:template>
118
119 <xsl:template name="double_point_counting">
120  <xsl:param name="string" select="&quot;&quot;"/>
121  <xsl:param name="counter" select="0"/>
122  <xsl:choose>
123   <xsl:when test="(substring-after($string,&quot;:&quot;) != &quot;&quot;)">
124    <xsl:call-template name="double_point_counting">
125     <xsl:with-param 
126         name="string" select="substring-after($string,&quot;:&quot;)"/>
127     <xsl:with-param 
128         name="counter" select="$counter +1"/> 
129    </xsl:call-template>
130   </xsl:when>
131   <xsl:otherwise>
132    <xsl:value-of select="$counter"/>
133   </xsl:otherwise> 
134  </xsl:choose>  
135 </xsl:template>
136
137 <xsl:template name="min">
138  <xsl:param name="string" select="&quot;&quot;"/>
139  <xsl:param name="counter" select="0"/>
140  <xsl:choose>
141   <xsl:when test="contains($string,concat($counter,&quot;:&quot;))
142          or (0 > $counter)">
143   <xsl:value-of select="$counter"/>
144   </xsl:when>
145   <xsl:otherwise>
146    <xsl:call-template name="min">
147     <xsl:with-param 
148         name="string" select="$string"/>
149     <xsl:with-param 
150         name="counter" select="$counter -1"/> 
151    </xsl:call-template>
152   </xsl:otherwise>
153  </xsl:choose>  
154 </xsl:template>
155
156 <xsl:template name="get_no_params">
157     <xsl:param name="first_uri" select="&quot;&quot;"/>
158     <xsl:param name="second_uri" select="&quot;&quot;"/>
159      <xsl:variable name="offset">
160       <xsl:call-template name="common_prefix">
161        <xsl:with-param name="first_uri" select="$first_uri"/>
162        <xsl:with-param name="second_uri" select="$second_uri"/>
163       </xsl:call-template>
164      </xsl:variable>
165      <xsl:choose>
166       <xsl:when test="$offset > 0">
167        <xsl:variable name="params"> 
168         <xsl:variable name="second_url"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$second_uri"/></xsl:call-template></xsl:variable>
169         <xsl:value-of 
170             select="document($second_url)/*/@params"/>
171        </xsl:variable>
172        <xsl:variable name="minimum">
173         <xsl:call-template name="min">
174          <xsl:with-param name="string" select="$params"/>
175          <xsl:with-param name="counter" select="$offset - 1"/>
176         </xsl:call-template>
177        </xsl:variable>
178        <xsl:choose>
179         <xsl:when test="0 > $minimum">
180          0
181         </xsl:when>
182         <xsl:otherwise>
183          <xsl:variable name="relevant_params">
184           <!-- the blank after : in the next line is essential -->
185           <xsl:value-of 
186             select="substring-after($params,concat($minimum,&quot;: &quot;))"/>
187          </xsl:variable>
188          <xsl:variable name="tokens">
189           <xsl:call-template name="blank_counting">
190            <xsl:with-param name="string" select="$relevant_params"/>
191            <xsl:with-param name="counter" select="0"/>
192           </xsl:call-template>
193          </xsl:variable>
194          <xsl:variable name="separators">
195           <xsl:call-template name="double_point_counting">
196            <xsl:with-param name="string" select="$relevant_params"/>
197            <xsl:with-param name="counter" select="0"/>
198           </xsl:call-template>
199          </xsl:variable>
200          <xsl:value-of select="$tokens - $separators"/>
201         </xsl:otherwise>
202        </xsl:choose>
203       </xsl:when>
204       <xsl:otherwise>
205       0
206       </xsl:otherwise>
207      </xsl:choose>
208 </xsl:template>
209
210
211 <!--***********************************************************************-->
212 <!--  Insert a subscript if there is a number at the end of a ci element   -->
213 <!--***********************************************************************-->
214
215 <xsl:template name="insert_subscript">
216 <xsl:param name="node_value" select="&quot;&quot;"/>
217 <xsl:param name="current_pos" select="1"/>
218 <xsl:param name="start_pos" select="0"/>
219     <xsl:choose>
220     <xsl:when test="$current_pos &lt;= string-length(string($node_value))">
221     <xsl:variable name="current_char"><xsl:value-of select="substring(string($node_value),$current_pos,1)"/></xsl:variable>
222      <xsl:choose>
223      <xsl:when test="(string($current_char) != &quot;0&quot;) and (string($current_char) != &quot;1&quot;) and (string($current_char) != &quot;2&quot;) and (string($current_char) != &quot;3&quot;) and (string($current_char) != &quot;4&quot;) and (string($current_char) != &quot;5&quot;) and (string($current_char) != &quot;6&quot;) and (string($current_char) !=  &quot;7&quot;) and (string($current_char) != &quot;8&quot;) and (string($current_char) != &quot;9&quot;)">
224       <xsl:choose> 
225       <xsl:when test="$start_pos != 0">
226        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="0"/></xsl:call-template>
227       </xsl:when> 
228       <xsl:otherwise>
229        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="$start_pos"/></xsl:call-template>
230       </xsl:otherwise>
231       </xsl:choose>
232      </xsl:when>
233      <xsl:otherwise>  
234       <xsl:choose>
235       <xsl:when test="$start_pos = 0">
236        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="$current_pos"/></xsl:call-template>
237       </xsl:when>
238       <xsl:otherwise>
239        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value" select="$node_value"/><xsl:with-param name="current_pos" select="$current_pos + 1"/><xsl:with-param name="start_pos" select="$start_pos"/></xsl:call-template>
240       </xsl:otherwise>
241       </xsl:choose>      
242      </xsl:otherwise>
243      </xsl:choose>
244     </xsl:when>
245     <xsl:otherwise>
246      <xsl:choose>
247      <xsl:when test="$start_pos != 0">
248       <m:msub>
249        <m:mi><xsl:value-of select="substring(string($node_value),1,$start_pos -1)"/></m:mi>
250        <m:mn><xsl:value-of select="substring(string($node_value),$start_pos)"/></m:mn>
251        </m:msub>
252      </xsl:when>
253      <xsl:otherwise>
254       <xsl:value-of select="$node_value"/>
255      </xsl:otherwise>
256      </xsl:choose>
257     </xsl:otherwise>    
258     </xsl:choose>
259 </xsl:template>
260
261
262 <!--*******************************************-->
263 <!--    ABSTRACTING PARAMETERS AND COUNTING    -->
264 <!--*******************************************-->
265 <!-- Si dimentica i CAST dei termini che astrae. Nel caso dell'astrazione -->
266 <!-- dei lambda dei pattern del CASE, qualora i lambda non si trovino     -->
267 <!-- nella forma weak-head, astrae solo i lambda che trova e restituisce  -->
268 <!-- un corpo depurato da tutti i primi cast che precedono il termine     -->
269 <!-- restituito.                                                          -->
270
271 <xsl:template match="*" mode="abstparams">
272 <xsl:param name="noparams" select="0"/>
273 <xsl:param name="target" select="0"/>
274 <xsl:param name="binder">PROD</xsl:param>
275     <xsl:choose>
276     <xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)=&quot;CAST&quot;))">
277      <xsl:choose>
278      <xsl:when test="name(.) = string($binder)">
279       <xsl:if test="$target = 0">
280        <xsl:choose>
281        <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
282         <m:ci>
283          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
284         </m:ci>
285        </xsl:when>
286        <xsl:otherwise> 
287         <Param name="{target/@binder}">
288          <xsl:apply-templates select="source"/>
289         </Param>
290        </xsl:otherwise>
291        </xsl:choose>
292       </xsl:if>
293       <xsl:apply-templates select="target/*[1]" mode="abstparams">
294        <xsl:with-param name="noparams" select="$noparams - 1"/>
295        <xsl:with-param name="target" select="$target"/>
296        <xsl:with-param name="binder" select="$binder"/>
297       </xsl:apply-templates>
298      </xsl:when>
299      <xsl:otherwise>
300       <xsl:apply-templates select="term/*[1]" mode="abstparams">
301        <xsl:with-param name="noparams" select="$noparams"/>
302        <xsl:with-param name="target" select="$target"/>
303        <xsl:with-param name="binder" select="$binder"/>
304       </xsl:apply-templates>
305      </xsl:otherwise>
306      </xsl:choose>
307     </xsl:when>
308     <xsl:otherwise> 
309      <xsl:choose>
310      <xsl:when test="($target = 1) and ($noparams != 0)">
311       <m:apply>
312       <m:csymbol>app</m:csymbol>
313 <!-- Mancava modalita': sono all'interno di un termine -->
314       <xsl:apply-templates select="." mode="pure"/>
315       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
316       </m:apply>
317      </xsl:when>
318      <xsl:otherwise>
319       <xsl:choose>
320       <xsl:when test="$noparams != 0">
321       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
322       </xsl:when>
323       <xsl:otherwise>
324        <xsl:if test="$target = 1">
325 <!-- Mancava modalita': con target=1 posso provenire sia da un oggetto che da un termine -->
326         <xsl:choose>
327         <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
328          <!-- CSC: era pure, ma deve essere noannot. Giusto, Irene? -->
329          <xsl:apply-templates select="." mode="noannot"/>
330         </xsl:when>
331         <xsl:otherwise>
332          <xsl:apply-templates select="."/>
333         </xsl:otherwise>
334         </xsl:choose>
335        </xsl:if>
336       </xsl:otherwise>
337       </xsl:choose>
338      </xsl:otherwise>
339      </xsl:choose>
340     </xsl:otherwise>
341     </xsl:choose>
342 </xsl:template>
343
344 <xsl:template name="printparam">
345 <xsl:param name="noleft" select="0"/>
346 <xsl:param name="number" select="1"/>
347     <xsl:if test="$noleft != 0">
348      <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value">$<xsl:value-of select="$number"/></xsl:with-param></xsl:call-template></m:ci>
349      <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noleft - 1"/><xsl:with-param name="number" select="$number + 1"/></xsl:call-template>  
350     </xsl:if>
351 </xsl:template>
352
353 <xsl:template match="*" mode="counting">
354 <xsl:param name="noparams" select="0"/>
355 <xsl:param name="count" select="0"/>
356  <xsl:choose>
357  <xsl:when test="name(.) = &quot;PROD&quot;">
358   <xsl:apply-templates select="target/*[1]" mode="counting">
359    <xsl:with-param name="noparams" select="$noparams"/>
360    <xsl:with-param name="count" select="$count + 1"/>
361   </xsl:apply-templates>
362  </xsl:when>
363  <xsl:when test="name(.) = &quot;CAST&quot;">
364   <xsl:apply-templates select="term/*[1]" mode="counting">
365    <xsl:with-param name="noparams" select="$noparams"/>
366    <xsl:with-param name="count" select="$count"/> 
367   </xsl:apply-templates>
368  </xsl:when>
369  <xsl:otherwise>
370   <xsl:value-of select="$count - $noparams"/>
371  </xsl:otherwise>
372  </xsl:choose>
373 </xsl:template>
374
375 </xsl:stylesheet>