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 <!--******************************************************************-->
29 <!-- (completely) Revisited: february 2001, Andrea Asperti -->
30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
31 <!--******************************************************************-->
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">
37 <xsl:include href="logic.xsl"/>
38 <xsl:include href="inductive.xsl"/>
39 <xsl:include href="rewrite.xsl"/>
40 <xsl:include href="diseq.xsl"/>
42 <!-- ************************* LOGIC *********************************-->
44 <!-- Proof objects -->
46 <xsl:key name="typeid" use="@of" match="TYPE"/>
48 <!-- These elements do not have inner type -->
49 <xsl:template match="PROD|SORT|MUTIND|instantiate" mode="noannot">
50 <xsl:apply-templates select="." mode="pure"/>
53 <!-- Atomic elements that have an inner type iff the expected type -->
54 <!-- is different from the synthesized type. -->
55 <xsl:template match="REL|VAR|META|CONST|MUTCONSTRUCT" mode="noannot">
56 <xsl:variable name="id" select="@id"/>
57 <xsl:variable name="innertype_available">
58 <xsl:for-each select="$InnerTypes">
59 <xsl:if test="key('typeid',$id)/*">
60 <xsl:text>yes</xsl:text>
65 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
66 <!--xsl:when test="@sort='Prop'"-->
67 <m:apply helm:xref="{@id}">
68 <m:csymbol>proof</m:csymbol>
69 <xsl:apply-templates mode="proof_transform" select="."/>
70 <xsl:for-each select="$InnerTypes">
71 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
76 <xsl:apply-templates select="." mode="pure"/>
81 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
83 <xsl:template match="LAMBDA" mode="noannot">
85 <xsl:when test="@sort='Prop'">
86 <xsl:apply-templates select="*[1]" mode="lambda_prop"/>
89 <!-- mode lambda is defined in content.xsl -->
90 <xsl:apply-templates select="*[1]" mode="lambda"/>
95 <xsl:template match="decl" mode="lambda_prop">
96 <xsl:variable name="id" select="@id"/>
97 <xsl:variable name="innertype_available">
98 <xsl:for-each select="$InnerTypes">
99 <xsl:if test="key('typeid',$id)/*">
100 <xsl:text>yes</xsl:text>
105 <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
106 <m:apply helm:xref="{@id}">
107 <m:csymbol>proof</m:csymbol>
108 <m:lambda helm:xref="{@id}">
111 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
114 <xsl:apply-templates select="*[1]" mode="noannot"/>
117 <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
119 <xsl:for-each select="$InnerTypes">
120 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
125 <m:lambda helm:xref="{@id}">
128 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
131 <xsl:apply-templates select="*[1]" mode="noannot"/>
134 <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
140 <xsl:template match="target" mode="lambda_prop">
141 <xsl:apply-templates select="*[1]" mode="noannot"/>
146 <xsl:template match="LETIN" mode="noannot">
148 <xsl:when test="@sort='Prop'">
149 <xsl:apply-templates select="*[1]" mode="letin_prop"/>
152 <!-- mode letin is defined in content.xsl -->
153 <xsl:apply-templates select="*[1]" mode="letin_pure"/>
158 <xsl:template match="def" mode="letin_prop">
159 <xsl:variable name="id" select="@id"/>
160 <xsl:variable name="innertype_available">
161 <xsl:for-each select="$InnerTypes">
162 <xsl:if test="key('typeid',$id)/*">
163 <xsl:text>yes</xsl:text>
168 <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
169 <m:apply helm:xref="{@id}">
170 <m:csymbol>proof</m:csymbol>
171 <m:apply helm:xref="{@id}">
172 <m:csymbol>let_in</m:csymbol>
175 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
178 <xsl:apply-templates select="*[1]" mode="noannot"/>
179 <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
181 <xsl:for-each select="$InnerTypes">
182 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
187 <m:apply helm:xref="{@id}">
188 <m:csymbol>let_in</m:csymbol>
191 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
194 <xsl:apply-templates select="*[1]" mode="noannot"/>
195 <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
201 <xsl:template match="target" mode="letin_prop">
202 <xsl:apply-templates select="*[1]" mode="noannot"/>
205 <!-- ALL these elements have inner type -->
206 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
207 <xsl:variable name="id" select="@id"/>
209 <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
210 <m:apply helm:xref="{@id}">
211 <m:csymbol>proof</m:csymbol>
212 <xsl:apply-templates mode="proof_transform" select="."/>
213 <xsl:for-each select="$InnerTypes">
214 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
220 <xsl:when test="name()='APPLY'">
221 <!-- This is the case of an applicative expression wich is not
222 a proof but could contains proofs...
223 MODE LETIN OR MODE PURE ??? Big question -->
224 <xsl:apply-templates select="." mode="pure"/>
227 <xsl:apply-templates select="." mode="pure"/>
234 <xsl:template mode="proof_transform" match="*">
236 <xsl:when test="name()='APPLY'">
237 <xsl:variable name="id" select="@id"/>
239 <xsl:when test="name(*[1])='CONST' or
240 (name(*[1])='instantiate' and name(*[1]/*[1])='CONST')">
241 <xsl:apply-templates mode="try_inductive" select="."/>
243 <!-- patch temporanea per la gestione di redex -->
244 <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2">
246 and *[2]/@sort='Prop'"> -->
247 <m:apply helm:xref="{@id}">
248 <m:csymbol>let_in</m:csymbol>
251 <xsl:call-template name="insert_subscript">
252 <xsl:with-param name="node_value">
253 <xsl:value-of select="*[1]/*[1]/@binder"/>
258 <xsl:apply-templates mode="noannot" select="*[2]"/>
259 <xsl:apply-templates mode="lambda_prop" select="*[1]/*[2]"/>
263 <xsl:apply-templates select="." mode="letin"/>
268 <xsl:apply-templates select="." mode="pure"/>
273 <xsl:template name="is_simple">
274 <xsl:param name="proof" select="/.."/>
275 <xsl:value-of select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
278 <xsl:template name="generate_side_proof">
279 <xsl:param name="proof" select="/.."/>
280 <xsl:param name="show_statement" select="1"/>
282 <xsl:variable name="is_simple">
283 <xsl:call-template name="is_simple">
284 <xsl:with-param name="proof" select="$proof"/>
287 <xsl:variable name="is_simple" select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
289 <xsl:when test="$is_simple">
291 <xsl:when test="name($proof)='APPLY'">
292 <xsl:apply-templates select="$proof" mode="letin"/>
295 <xsl:apply-templates select="$proof" mode="pure"/>
300 <xsl:variable name="id" select="@id"/>
301 <m:apply helm:xref="{@id}">
303 <xsl:when test="$show_statement = 1">
304 <m:csymbol>proof</m:csymbol>
307 <m:csymbol>side_proof</m:csymbol>
310 <xsl:apply-templates mode="proof_transform" select="$proof"/>
311 <xsl:for-each select="$InnerTypes">
312 <xsl:apply-templates mode="pure" select="key('typeid',$proof/@id)/*"/>
315 <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
320 <xsl:template match="APPLY" mode="letin">
321 <xsl:variable name="no_subproofs">
322 <xsl:variable name="stars">
323 <xsl:for-each select="*[@sort='Prop']">
324 <xsl:variable name="id" select="@id"/>
325 <xsl:variable name="innertype_available">
326 <xsl:for-each select="$InnerTypes">
327 <xsl:if test="key('typeid',$id)/*">
328 <xsl:text>yes</xsl:text>
332 <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
333 <!-- We generate one star for each subproof -->
334 <xsl:text>*</xsl:text>
338 <xsl:value-of select="string-length($stars)"/>
340 <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
342 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
343 <m:apply helm:xref="{@id}">
344 <m:csymbol>letin1</m:csymbol>
345 <xsl:for-each select="*[@sort='Prop']">
346 <xsl:variable name="id" select="@id"/>
347 <xsl:variable name="innertype_available">
348 <xsl:for-each select="$InnerTypes">
349 <xsl:if test="key('typeid',$id)/*">
350 <xsl:text>yes</xsl:text>
354 <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
355 <xsl:apply-templates mode="noannot" select="."/>
358 <!-- now re-process the application -->
359 <m:apply helm:xref="{@id}">
360 <m:csymbol>app</m:csymbol>
361 <!-- mode previous looks for siblings:
362 call with the first child -->
363 <xsl:apply-templates mode="previous" select="*[1]"/>
367 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
368 <m:apply helm:xref="{@id}">
369 <m:csymbol>letin</m:csymbol>
370 <!-- first process all subproofs (let-in) -->
371 <xsl:call-template name="gen_let"/>
372 <!-- now re-process the application -->
373 <m:apply helm:xref="{@id}">
374 <m:csymbol>app</m:csymbol>
375 <!-- mode flat looks for siblings: call with the first child -->
376 <xsl:apply-templates mode="flat" select="*[1]"/>
382 <xsl:when test="@sort='Prop'">
384 <m:csymbol>app</m:csymbol>
385 <xsl:apply-templates mode="erase" select="*[1]"/>
389 <xsl:apply-templates mode="pure" select="."/>
396 <xsl:template name="gen_let">
397 <xsl:param name="init_pos" select="1"/>
398 <xsl:param name="from" select="0"/>
399 <xsl:apply-templates mode="gen_let_aux" select="*[position() = ($from+1)]">
400 <xsl:with-param name="init_pos" select="$init_pos"/>
401 </xsl:apply-templates>
404 <xsl:template mode="gen_let_aux" match="*">
405 <xsl:param name="init_pos" select="1"/>
406 <xsl:variable name="id" select="@id"/>
407 <xsl:variable name="innertype_available">
408 <xsl:for-each select="$InnerTypes">
409 <xsl:if test="key('typeid',$id)/*">
410 <xsl:text>yes</xsl:text>
415 <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
417 <m:csymbol>let</m:csymbol>
418 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
419 <xsl:apply-templates mode="noannot" select="."/>
421 <xsl:if test="following-sibling::*[1]">
422 <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
423 <xsl:with-param name="init_pos" select="$init_pos+1"/>
424 </xsl:apply-templates>
428 <xsl:if test="following-sibling::*[1]">
429 <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
430 <xsl:with-param name="init_pos" select="$init_pos"/>
431 </xsl:apply-templates>
437 <!-- questa vecchia versione (di Claudio??) sembra bacata come un melone.
439 <xsl:template name="gen_let">
440 <xsl:param name="init_pos" select="0"/>
441 <xsl:param name="from" select="0"/>
442 <xsl:for-each select="*[position()>$from and @sort='Prop']">
443 <xsl:variable name="id" select="@id"/>
444 <xsl:variable name="innertype_available">
445 <xsl:for-each select="$InnerTypes">
446 <xsl:if test="key('typeid',$id)/*">
447 <xsl:text>yes</xsl:text>
451 <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
453 <m:csymbol>let</m:csymbol>
454 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position()+$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
455 <xsl:apply-templates mode="noannot" select="."/>
461 <xsl:template match="*" mode="erase">
463 <xsl:when test="@sort='Prop'
464 or name()='instantiate' or $naturalLanguage='no'">
465 <xsl:apply-templates mode="pure" select="."/>
471 <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
474 <xsl:template match="*" mode="previous">
475 <xsl:variable name="innertype_available">
476 <xsl:variable name="id" select="@id"/>
477 <xsl:for-each select="$InnerTypes">
478 <xsl:if test="key('typeid',$id)/*">
479 <xsl:text>yes</xsl:text>
484 <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
485 <m:ci>previous</m:ci>
488 <!-- forse bisognerebbe trattare solo l'elemento di testa -->
490 <xsl:when test="@sort='Prop'
491 or name()='instantiate' or $naturalLanguage='no'">
492 <xsl:apply-templates mode="pure" select="."/>
498 <!-- <xsl:apply-templates select="." mode="pure"/> -->
501 <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
504 <xsl:template match="*" mode="flat">
505 <xsl:param name="n" select="1"/>
506 <xsl:variable name="id" select="@id"/>
507 <xsl:variable name="innertype_available">
508 <xsl:for-each select="$InnerTypes">
509 <xsl:if test="key('typeid',$id)/*">
510 <xsl:text>yes</xsl:text>
515 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
517 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
519 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
520 <xsl:with-param name="n" select="$n+1"/>
521 </xsl:apply-templates>
525 <xsl:when test="name()='REL' or name()='instantiate' or @sort='Prop' or $naturalLanguage='no'">
526 <xsl:apply-templates mode="pure" select="."/>
532 <!-- <xsl:apply-templates mode="pure" select="."/> -->
533 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
534 <xsl:with-param name="n" select="$n"/>
535 </xsl:apply-templates>
540 <!-- Auxiliary functions -->
541 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
542 <!-- can replace the next template -->
543 <xsl:template name="get_name">
544 <xsl:param name="uri" select="''"/>
545 <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
547 <xsl:when test="contains($sub_after,'/')">
548 <xsl:call-template name="get_name">
549 <xsl:with-param name="uri" select="$sub_after"/>
553 <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>