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">
6 <!--***********************************************************************-->
7 <!-- From MathML content to HTML -->
8 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
9 <!--***********************************************************************-->
12 <xsl:include href="html_init.xsl"/>
13 <xsl:include href="html_set.xsl"/>
14 <xsl:include href="html_reals.xsl"/>
17 <!-- <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>-->
18 <xsl:variable name="header" select="document('http://localhost:8081/conf')/html_link"/>
20 <xsl:variable name="showcast" select="0"/>
23 <!--***********************************************************************-->
24 <!-- HTML Head and Body -->
25 <!--***********************************************************************-->
27 <xsl:output method="html"/>
29 <xsl:variable name="framewidth" select="36"/>
31 <xsl:template match="/">
32 <xsl:param name="current_indent" select="0"/>
37 <xsl:with-param name="current_indent" select="0"/>
38 </xsl:apply-templates>
43 <!--***********************************************************************-->
45 <!--***********************************************************************-->
47 <xsl:template name="make_indent">
48 <xsl:param name="current_indent" select="0"/>
49 <xsl:if test="$current_indent > 0">
50 <xsl:text> </xsl:text>
51 <xsl:call-template name="make_indent">
52 <xsl:with-param name="current_indent" select="$current_indent - 1"/>
57 <!-- Syntactic Sugar -->
59 <xsl:template match="m:type">
60 <xsl:param name="current_indent" select="0"/>
62 <xsl:with-param name="current_indent"
63 select="$current_indent"/>
64 </xsl:apply-templates>
67 <xsl:template match="m:condition">
68 <xsl:param name="current_indent" select="0"/>
70 <xsl:with-param name="current_indent"
71 select="$current_indent"/>
72 </xsl:apply-templates>
75 <xsl:template match="m:math">
76 <xsl:param name="current_indent" select="0"/>
78 <xsl:with-param name="current_indent"
79 select="$current_indent"/>
80 </xsl:apply-templates>
85 <xsl:template match="m:apply[m:csymbol]">
86 <xsl:param name="current_indent" select="0"/>
87 <xsl:param name="width" select="$framewidth"/>
88 <xsl:variable name="name">
89 <xsl:value-of select="m:csymbol"/>
91 <xsl:variable name="charlength">
92 <xsl:apply-templates select="m:csymbol" mode="charcount"/>
94 <!-- <xsl:value-of select="$current_indent"/> -->
95 <!-- <xsl:value-of select="$charlength"/> -->
97 <xsl:when test="$name='prod'">
99 <xsl:when test="$charlength > $framewidth">
101 <FONT FACE="symbol" SIZE="+2" color="blue">P</FONT>
102 <xsl:apply-templates select="m:bvar/m:ci"/>
103 <xsl:text>:</xsl:text>
104 <xsl:apply-templates select="m:bvar/m:type">
105 <xsl:with-param name="current_indent"
106 select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
107 </xsl:apply-templates><BR/>
108 <xsl:call-template name="make_indent">
109 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
111 <xsl:text>.</xsl:text>
112 <xsl:apply-templates select="*[position()=3]">
113 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
114 </xsl:apply-templates>
118 <FONT FACE="symbol" SIZE="+2" color="blue">P</FONT>
119 <xsl:apply-templates select="m:bvar/m:ci"/>
120 <xsl:text>:</xsl:text>
121 <xsl:apply-templates select="m:bvar/m:type"/>
122 <xsl:text>.</xsl:text>
123 <xsl:apply-templates select="*[position()=3]"/>
127 <xsl:when test="$name='arrow'">
129 <xsl:when test="$charlength > $framewidth">
130 <xsl:text>(</xsl:text>
131 <xsl:apply-templates select="*[position()=2]">
132 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
133 </xsl:apply-templates>
135 <xsl:call-template name="make_indent">
136 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
139 <FONT FACE="symbol" SIZE="+2" color="blue">®</FONT>
140 <xsl:apply-templates select="*[position()=3]">
141 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
142 </xsl:apply-templates>
143 <xsl:text>)</xsl:text>
146 <xsl:text>(</xsl:text>
147 <xsl:apply-templates select="*[position()=2]"/>
149 <FONT FACE="symbol" SIZE="+2" color="blue">®</FONT>
150 <xsl:apply-templates select="*[position()=3]"/>
151 <xsl:text>)</xsl:text>
155 <xsl:when test="$name='app'">
157 <xsl:when test="$charlength > $framewidth">
158 <xsl:text>(</xsl:text>
159 <xsl:apply-templates select="*[position()=2]">
160 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
161 </xsl:apply-templates>
162 <xsl:for-each select="*[position()>2]">
164 <xsl:call-template name="make_indent">
165 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
167 <xsl:apply-templates select=".">
168 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
169 </xsl:apply-templates>
171 <xsl:text>)</xsl:text>
174 <xsl:text>(</xsl:text>
175 <xsl:apply-templates select="*[position()=2]"/>
176 <xsl:for-each select="*[position()>2]">
177 <xsl:text> </xsl:text>
178 <xsl:apply-templates select="."/>
180 <xsl:text>)</xsl:text>
184 <xsl:when test="$name='cast'">
186 <xsl:when test="$showcast = 1">
188 <xsl:when test="$charlength > $framewidth">
189 <xsl:text>(</xsl:text>
190 <xsl:apply-templates select="*[position()=2]">
191 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
192 </xsl:apply-templates><BR/>
193 <xsl:call-template name="make_indent">
194 <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
195 <xsl:text>:></xsl:text>
196 <xsl:apply-templates select="*[position()=3]">
197 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
198 </xsl:apply-templates>
199 <xsl:text>)</xsl:text>
202 <xsl:text>(</xsl:text>
203 <xsl:apply-templates select="*[position()=2]"/>
204 <xsl:text>:></xsl:text>
205 <xsl:apply-templates select="*[position()=3]"/>
206 <xsl:text>)</xsl:text>
211 <xsl:apply-templates select="*[position()=2]">
212 <xsl:with-param name="current_indent" select="$current_indent"/>
213 </xsl:apply-templates>
217 <xsl:when test="$name='Prop'">
218 <xsl:text>Prop</xsl:text>
220 <xsl:when test="$name='Set'">
221 <xsl:text>Set</xsl:text>
223 <xsl:when test="$name='Type'">
224 <xsl:text>Type</xsl:text>
226 <xsl:when test="$name='mutcase'">
228 <xsl:when test="$charlength > $framewidth">
229 <xsl:text><</xsl:text>
230 <xsl:apply-templates select="*[position()=2]">
231 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
232 </xsl:apply-templates>
233 <xsl:text>> </xsl:text>
234 <xsl:text>CASE </xsl:text>
235 <xsl:apply-templates select="*[position()=3]">
236 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
237 </xsl:apply-templates>
238 <xsl:text> OF </xsl:text>
239 <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
241 <xsl:call-template name="make_indent">
242 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
245 <xsl:when test="position() = 1">
246 <xsl:text>  </xsl:text>
249 <xsl:text>| </xsl:text>
252 <xsl:apply-templates select="."/>
253 <FONT FACE="symbol" SIZE="+2" color="green">Þ</FONT>
254 <xsl:apply-templates select="following-sibling::*[position()= 1]">
255 <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
256 </xsl:apply-templates>
260 <xsl:text><</xsl:text>
261 <xsl:apply-templates select="*[position()=2]"/>
262 <xsl:text>> </xsl:text>
263 <xsl:text>CASE </xsl:text>
264 <xsl:apply-templates select="*[position()=3]"/>
265 <xsl:text> OF </xsl:text>
266 <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
268 <xsl:when test="not(position() = 1)">
269 <xsl:text> | </xsl:text>
272 <xsl:apply-templates select="."/>
273 <FONT FACE="symbol" SIZE="+2" color="green">Þ</FONT>
274 <xsl:apply-templates select="following-sibling::*[position()= 1]">
275 <xsl:with-param name="current_indent" select="$current_indent + 2 + string-length()"/>
276 </xsl:apply-templates>
281 <xsl:when test="$name='fix'">
283 <xsl:when test="$charlength > $framewidth">
284 <xsl:text>FIX</xsl:text>
285 <xsl:value-of select="m:ci"/>
286 <xsl:text>{</xsl:text>
287 <xsl:for-each select="m:bvar">
289 <xsl:call-template name="make_indent">
290 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
292 <xsl:value-of select="m:ci"/>
293 <xsl:text>:</xsl:text>
294 <xsl:apply-templates select="m:type">
295 <xsl:with-param name="current_indent"
296 select="$current_indent + 5 + string-length(m:ci)"/>
297 </xsl:apply-templates>
299 <xsl:call-template name="make_indent">
300 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
302 <xsl:text>:=</xsl:text>
303 <xsl:apply-templates select="following-sibling::*[position() = 1]">
304 <xsl:with-param name="current_indent" select="$current_indent +2"/>
305 </xsl:apply-templates>
308 <xsl:call-template name="make_indent">
309 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
311 <xsl:text>}</xsl:text>
314 <xsl:text>FIX</xsl:text>
315 <xsl:value-of select="m:ci"/>
316 <xsl:text>{</xsl:text>
317 <xsl:for-each select="m:bvar">
318 <xsl:value-of select="m:ci"/>
319 <xsl:text>:</xsl:text>
320 <xsl:apply-templates select="m:type"/>
321 <xsl:text>:=</xsl:text>
322 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
324 <xsl:when test="position()=last()">
325 <xsl:text>}</xsl:text>
328 <xsl:text>;</xsl:text>
335 <xsl:when test="$name='cofix'">
337 <xsl:when test="($charlength + 10) > $framewidth">
338 <xsl:text>COFIX</xsl:text>
339 <xsl:value-of select="m:ci"/>
340 <xsl:text>{</xsl:text>
342 <xsl:call-template name="make_indent">
343 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
345 <xsl:for-each select="m:bvar">
346 <xsl:value-of select="m:ci"/>
347 <xsl:text>:</xsl:text>
348 <xsl:apply-templates select="m:type">
349 <xsl:with-param name="current_indent"
350 select="$current_indent + 5 + string-length(m:ci)"/>
351 </xsl:apply-templates>
353 <xsl:call-template name="make_indent">
354 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
356 <xsl:text>:=</xsl:text>
357 <xsl:apply-templates select="following-sibling::*[position() = 1]">
358 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
359 </xsl:apply-templates>
363 <xsl:call-template name="make_indent">
364 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
366 <xsl:text>}</xsl:text>
369 <xsl:text>COFIX</xsl:text>
370 <xsl:value-of select="m:ci"/>
371 <xsl:text>{</xsl:text>
372 <xsl:for-each select="m:bvar">
373 <xsl:value-of select="m:ci"/>
374 <xsl:text>:</xsl:text>
375 <xsl:apply-templates select="m:type"/>
376 <xsl:text>:=</xsl:text>
377 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
379 <xsl:when test="position()=last()">
380 <xsl:text>}</xsl:text>
383 <xsl:text>;</xsl:text>
396 <xsl:template match="m:lambda">
397 <xsl:param name="current_indent" select="0"/>
398 <xsl:variable name="charlength">
399 <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
400 <!-- <xsl:apply-templates select="." mode="charcount"/> -->
402 <!-- <xsl:value-of select="$charlength"/> -->
404 <xsl:when test="$charlength > $framewidth">
406 <FONT FACE="symbol" SIZE="+2" color="red">l</FONT>
407 <xsl:apply-templates select="m:bvar/m:ci"/>
408 <xsl:text>:</xsl:text>
409 <xsl:apply-templates select="m:bvar/m:type">
410 <xsl:with-param name="current_indent"
411 select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
412 </xsl:apply-templates><BR/>
413 <xsl:call-template name="make_indent">
414 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
416 <xsl:text>.</xsl:text>
417 <xsl:apply-templates select="*[position()=2]">
418 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
419 </xsl:apply-templates>
423 <FONT FACE="symbol" SIZE="+2" color="red">l</FONT>
424 <xsl:apply-templates select="m:bvar/m:ci"/>
425 <xsl:text>:</xsl:text>
426 <xsl:apply-templates select="m:bvar/m:type"/>
427 <xsl:text>.</xsl:text>
428 <xsl:apply-templates select="*[position()=2]"/>
434 <xsl:template match="m:ci">
436 <xsl:when test="boolean(@definitionURL)">
437 <!-- CSC: non bisogna piu' utilizzare la url, bensi' la uri -->
438 <!-- <xsl:variable name="url">
439 <xsl:value-of select="concat(string($absPath),
443 <xsl:attribute name="href">
444 <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
446 <xsl:apply-templates/>
450 <xsl:value-of select="."/>
457 <xsl:template match="m:ci|m:csymbol" mode="charcount">
458 <xsl:param name="incurrent_length" select="0"/>
460 <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
461 <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
463 <xsl:when test="string($siblength) = """>
464 <xsl:value-of select="$incurrent_length + string-length()"/>
467 <xsl:value-of select="number($siblength)"/>
472 <xsl:value-of select="$incurrent_length + string-length()"/>
477 <xsl:template match="*" mode="charcount">
478 <xsl:param name="incurrent_length" select="0"/>
480 <xsl:when test="count(child::*) = 0">
481 <xsl:value-of select="$incurrent_length"/>
484 <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
486 <xsl:when test="$framewidth >= number($childlength)">
487 <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$childlength"/></xsl:apply-templates></xsl:variable>
489 <xsl:when test="string($siblength) = """>
490 <xsl:value-of select="number($childlength)"/>
493 <xsl:value-of select="number($siblength)"/>
498 <xsl:value-of select="number($childlength)"/>
506 <!--***********************************************************************-->
508 <!--***********************************************************************-->
512 <xsl:template match="Definition">
513 <xsl:param name="current_indent" select="0"/>
515 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
517 <xsl:call-template name="make_indent">
518 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
520 <xsl:apply-templates select="type/*[1]">
521 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
522 </xsl:apply-templates><BR/>
524 <xsl:call-template name="make_indent">
525 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
527 <xsl:apply-templates select="body/*[1]">
528 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
529 </xsl:apply-templates>
535 <xsl:template match="Axiom">
536 <xsl:param name="current_indent" select="0"/>
538 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
539 TYPE = <xsl:apply-templates select="type/*[1]">
540 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
541 </xsl:apply-templates>
545 <!-- UNFINISHED PROOF -->
547 <xsl:template match="CurrentProof">
548 <xsl:param name="current_indent" select="0"/>
550 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
551 THESIS: <xsl:apply-templates select="type/*[1]">
552 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
553 </xsl:apply-templates><BR/>
555 <xsl:for-each select="Conjecture">
557 <xsl:call-template name="make_indent">
558 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
560 <xsl:value-of select="./@no"/> :
561 <xsl:apply-templates select="./*[1]">
562 <xsl:with-param name="current_indent" select="$current_indent + 11"/>
563 </xsl:apply-templates>
567 <xsl:apply-templates select="body/*[1]">
568 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
569 </xsl:apply-templates>
573 <!-- MUTUAL INDUCTIVE DEFINITION -->
575 <xsl:template match="InductiveDefinition">
576 <xsl:param name="current_indent" select="0"/>
578 <xsl:for-each select="InductiveType">
580 <xsl:when test="position() = 1">
582 <xsl:when test="string(./@inductive) = "true"">
586 COINDUCTIVE DEFINITION
594 <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != """><xsl:value-of select="../Params"/></xsl:if>)
596 <xsl:if test="string(../Param) != """>
597 <xsl:for-each select="../Param">
598 <xsl:value-of select="./@name"/>
600 <xsl:apply-templates select="*"/>
605 <xsl:apply-templates select="./arity/*[1]">
606 <xsl:with-param name="current_indent" select="$current_indent + 9"/>
607 </xsl:apply-templates> <BR/>
609 <xsl:for-each select="./Constructor">
611 <xsl:call-template name="make_indent">
612 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
615 <xsl:when test="position() = 1">
616 <xsl:text>  </xsl:text>
619 <xsl:text>| </xsl:text>
622 <xsl:value-of select="./@name"/>
623 <xsl:text>: </xsl:text>
624 <xsl:apply-templates select="./*[1]">
625 <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
626 </xsl:apply-templates>
634 <xsl:template match="Variable">
635 <xsl:param name="current_indent" select="0"/>
637 VARIABLE <xsl:value-of select="@name"/><BR/>
638 TYPE = <xsl:apply-templates select="type/*[1]">
639 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
640 </xsl:apply-templates>
644 <!--***********************************************************************-->
646 <!--***********************************************************************-->
650 <xsl:template match="SECTION">
651 <xsl:param name="current_indent" select="0"/>
652 <h1>BEGIN OF SECTION</h1>
653 <xsl:apply-templates/>
654 <h1>END OF SECTION</h1>