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"/> -->
47 <xsl:key name="typeid" use="@of" match="TYPE"/>
49 <!-- These elements do not have inner type -->
50 <xsl:template match="PROD|SORT|MUTIND|instantiate" mode="noannot">
51 <xsl:apply-templates select="." mode="pure"/>
54 <!-- Atomic elements that have an inner type iff the expected type -->
55 <!-- is different from the synthesized type. -->
56 <xsl:template match="REL|VAR|META|CONST|MUTCONSTRUCT" mode="noannot">
57 <xsl:variable name="id" select="@id"/>
58 <xsl:variable name="innertype_available">
59 <xsl:for-each select="$InnerTypes">
60 <xsl:if test="key('typeid',$id)/*">
61 <xsl:text>yes</xsl:text>
66 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
67 <!--xsl:when test="@sort='Prop'"-->
68 <m:apply helm:xref="{@id}">
69 <m:csymbol>proof</m:csymbol>
70 <xsl:apply-templates mode="proof_transform" select="."/>
71 <xsl:for-each select="$InnerTypes">
72 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
77 <xsl:apply-templates select="." mode="pure"/>
82 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
84 <xsl:template match="LAMBDA" mode="noannot">
86 <xsl:when test="@sort='Prop'">
87 <xsl:apply-templates select="*[1]" mode="lambda_prop"/>
90 <!-- mode lambda is defined in content.xsl -->
91 <xsl:apply-templates select="*[1]" mode="lambda"/>
96 <xsl:template match="decl" mode="lambda_prop">
97 <xsl:variable name="id" select="@id"/>
98 <xsl:variable name="innertype_available">
99 <xsl:for-each select="$InnerTypes">
100 <xsl:if test="key('typeid',$id)/*">
101 <xsl:text>yes</xsl:text>
106 <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
107 <m:apply helm:xref="{@id}">
108 <m:csymbol>proof</m:csymbol>
109 <m:lambda helm:xref="{@id}">
112 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
115 <xsl:apply-templates select="*[1]" mode="noannot"/>
118 <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
120 <xsl:for-each select="$InnerTypes">
121 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
126 <m:lambda helm:xref="{@id}">
129 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
132 <xsl:apply-templates select="*[1]" mode="noannot"/>
135 <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
141 <xsl:template match="target" mode="lambda_prop">
142 <xsl:apply-templates select="*[1]" mode="noannot"/>
147 <xsl:template match="LETIN" mode="noannot">
149 <xsl:when test="@sort='Prop'">
150 <xsl:apply-templates select="*[1]" mode="letin_prop"/>
153 <!-- mode letin is defined in content.xsl -->
154 <xsl:apply-templates select="*[1]" mode="letin_pure"/>
159 <xsl:template match="def" mode="letin_prop">
160 <xsl:variable name="id" select="@id"/>
161 <xsl:variable name="innertype_available">
162 <xsl:for-each select="$InnerTypes">
163 <xsl:if test="key('typeid',$id)/*">
164 <xsl:text>yes</xsl:text>
169 <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
170 <m:apply helm:xref="{@id}">
171 <m:csymbol>proof</m:csymbol>
172 <m:apply helm:xref="{@id}">
173 <m:csymbol>let_in</m:csymbol>
176 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
179 <xsl:apply-templates select="*[1]" mode="noannot"/>
180 <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
182 <xsl:for-each select="$InnerTypes">
183 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
188 <m:apply helm:xref="{@id}">
189 <m:csymbol>let_in</m:csymbol>
192 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
195 <xsl:apply-templates select="*[1]" mode="noannot"/>
196 <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
202 <xsl:template match="target" mode="letin_prop">
203 <xsl:apply-templates select="*[1]" mode="noannot"/>
206 <!-- ALL these elements have inner type -->
207 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
208 <xsl:variable name="id" select="@id"/>
210 <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
211 <m:apply helm:xref="{@id}">
212 <m:csymbol>proof</m:csymbol>
213 <xsl:apply-templates mode="proof_transform" select="."/>
214 <xsl:for-each select="$InnerTypes">
215 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
221 <xsl:when test="name()='APPLY'">
222 <!-- This is the case of an applicative expression wich is not
223 a proof but could contains proofs...
224 MODE LETIN OR MODE PURE ??? Big question -->
225 <xsl:apply-templates select="." mode="pure"/>
228 <xsl:apply-templates select="." mode="pure"/>
235 <xsl:template mode="proof_transform" match="*">
237 <xsl:when test="name()='APPLY'">
238 <xsl:variable name="id" select="@id"/>
240 <xsl:when test="name(*[1])='CONST' or
241 (name(*[1])='instantiate' and name(*[1]/*[1])='CONST')">
242 <xsl:apply-templates mode="try_inductive" select="."/>
244 <!-- patch temporanea per la gestione di redex -->
245 <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2">
247 and *[2]/@sort='Prop'"> -->
248 <m:apply helm:xref="{@id}">
249 <m:csymbol>let_in</m:csymbol>
252 <xsl:call-template name="insert_subscript">
253 <xsl:with-param name="node_value">
254 <xsl:value-of select="*[1]/*[1]/@binder"/>
259 <xsl:apply-templates mode="noannot" select="*[2]"/>
260 <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
264 <xsl:apply-templates select="." mode="letin"/>
269 <xsl:apply-templates select="." mode="pure"/>
274 <xsl:template name="is_simple">
275 <xsl:param name="proof" select="/.."/>
276 <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))"/>
279 <xsl:template name="generate_side_proof">
280 <xsl:param name="proof" select="/.."/>
281 <xsl:param name="show_statement" select="1"/>
283 <xsl:variable name="is_simple">
284 <xsl:call-template name="is_simple">
285 <xsl:with-param name="proof" select="$proof"/>
288 <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))"/>
290 <xsl:when test="$is_simple">
292 <xsl:when test="name($proof)='APPLY'">
293 <xsl:apply-templates select="$proof" mode="letin"/>
296 <xsl:apply-templates select="$proof" mode="pure"/>
301 <xsl:variable name="id" select="@id"/>
302 <m:apply helm:xref="{@id}">
304 <xsl:when test="$show_statement = 1">
305 <m:csymbol>proof</m:csymbol>
308 <m:csymbol>side_proof</m:csymbol>
311 <xsl:apply-templates mode="proof_transform" select="$proof"/>
312 <xsl:for-each select="$InnerTypes">
313 <xsl:apply-templates mode="pure" select="key('typeid',$proof/@id)/*"/>
316 <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
321 <xsl:template match="APPLY" mode="letin">
322 <xsl:variable name="no_subproofs">
323 <xsl:variable name="stars">
324 <xsl:for-each select="*[@sort='Prop']">
325 <xsl:variable name="id" select="@id"/>
326 <xsl:variable name="innertype_available">
327 <xsl:for-each select="$InnerTypes">
328 <xsl:if test="key('typeid',$id)/*">
329 <xsl:text>yes</xsl:text>
333 <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')">
334 <!-- We generate one star for each subproof -->
335 <xsl:text>*</xsl:text>
339 <xsl:value-of select="string-length($stars)"/>
341 <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
343 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
344 <m:apply helm:xref="{@id}">
345 <m:csymbol>letin1</m:csymbol>
346 <xsl:for-each select="*[@sort='Prop']">
347 <xsl:variable name="id" select="@id"/>
348 <xsl:variable name="innertype_available">
349 <xsl:for-each select="$InnerTypes">
350 <xsl:if test="key('typeid',$id)/*">
351 <xsl:text>yes</xsl:text>
355 <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')">
356 <xsl:apply-templates mode="noannot" select="."/>
359 <!-- now re-process the application -->
360 <m:apply helm:xref="{@id}">
361 <m:csymbol>app</m:csymbol>
362 <!-- mode previous looks for siblings:
363 call with the first child -->
364 <xsl:apply-templates mode="previous" select="*[1]"/>
368 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
369 <m:apply helm:xref="{@id}">
370 <m:csymbol>letin</m:csymbol>
371 <!-- first process all subproofs (let-in) -->
372 <xsl:call-template name="gen_let"/>
373 <!-- now re-process the application -->
374 <m:apply helm:xref="{@id}">
375 <m:csymbol>app</m:csymbol>
376 <!-- mode flat looks for siblings: call with the first child -->
377 <xsl:apply-templates mode="flat" select="*[1]"/>
383 <xsl:when test="@sort='Prop'">
385 <m:csymbol>app</m:csymbol>
386 <xsl:apply-templates mode="erase" select="*[1]"/>
390 <xsl:apply-templates mode="pure" select="."/>
398 <xsl:template name="gen_let">
399 <xsl:param name="init_pos" select="1"/>
400 <xsl:param name="from" select="0"/>
401 <xsl:apply-templates mode="gen_let_aux" select="*[position() = ($from+1)]">
402 <xsl:with-param name="init_pos" select="$init_pos"/>
403 </xsl:apply-templates>
406 <xsl:template mode="gen_let_aux" match="*">
407 <xsl:param name="init_pos" select="1"/>
408 <xsl:variable name="id" select="@id"/>
409 <xsl:variable name="innertype_available">
410 <xsl:for-each select="$InnerTypes">
411 <xsl:if test="key('typeid',$id)/*">
412 <xsl:text>yes</xsl:text>
417 <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'))">
419 <m:csymbol>let</m:csymbol>
420 <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>
421 <xsl:apply-templates mode="noannot" select="."/>
423 <xsl:if test="following-sibling::*[1]">
424 <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
425 <xsl:with-param name="init_pos" select="$init_pos+1"/>
426 </xsl:apply-templates>
430 <xsl:if test="following-sibling::*[1]">
431 <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
432 <xsl:with-param name="init_pos" select="$init_pos"/>
433 </xsl:apply-templates>
439 <!-- questa vecchia versione (di Claudio??) sembra bacata come un melone.
441 <xsl:template name="gen_let">
442 <xsl:param name="init_pos" select="0"/>
443 <xsl:param name="from" select="0"/>
444 <xsl:for-each select="*[position()>$from and @sort='Prop']">
445 <xsl:variable name="id" select="@id"/>
446 <xsl:variable name="innertype_available">
447 <xsl:for-each select="$InnerTypes">
448 <xsl:if test="key('typeid',$id)/*">
449 <xsl:text>yes</xsl:text>
453 <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')">
455 <m:csymbol>let</m:csymbol>
456 <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>
457 <xsl:apply-templates mode="noannot" select="."/>
463 <xsl:template match="*" mode="erase">
465 <xsl:when test="@sort='Prop'
466 or name()='instantiate' or $naturalLanguage='no'">
467 <xsl:apply-templates mode="pure" select="."/>
473 <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
476 <xsl:template match="*" mode="previous">
477 <xsl:variable name="innertype_available">
478 <xsl:variable name="id" select="@id"/>
479 <xsl:for-each select="$InnerTypes">
480 <xsl:if test="key('typeid',$id)/*">
481 <xsl:text>yes</xsl:text>
486 <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'))">
487 <m:ci>previous</m:ci>
490 <!-- forse bisognerebbe trattare solo l'elemento di testa -->
492 <xsl:when test="@sort='Prop'
493 or name()='instantiate' or $naturalLanguage='no'">
494 <xsl:apply-templates mode="pure" select="."/>
500 <!-- <xsl:apply-templates select="." mode="pure"/> -->
503 <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
506 <xsl:template match="*" mode="flat">
507 <xsl:param name="n" select="1"/>
508 <xsl:variable name="id" select="@id"/>
509 <xsl:variable name="innertype_available">
510 <xsl:for-each select="$InnerTypes">
511 <xsl:if test="key('typeid',$id)/*">
512 <xsl:text>yes</xsl:text>
517 <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'))">
519 <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>
521 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
522 <xsl:with-param name="n" select="$n+1"/>
523 </xsl:apply-templates>
527 <xsl:when test="name()='REL' or name()='instantiate' or @sort='Prop' or $naturalLanguage='no'">
528 <xsl:apply-templates mode="pure" select="."/>
534 <!-- <xsl:apply-templates mode="pure" select="."/> -->
535 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
536 <xsl:with-param name="n" select="$n"/>
537 </xsl:apply-templates>
542 <!-- Auxiliary functions -->
543 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
544 <!-- can replace the next template -->
545 <xsl:template name="get_name">
546 <xsl:param name="uri" select="''"/>
547 <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
549 <xsl:when test="contains($sub_after,'/')">
550 <xsl:call-template name="get_name">
551 <xsl:with-param name="uri" select="$sub_after"/>
555 <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>