<xsl:template match="LETIN" mode="pure">
- <xsl:apply-templates select="*[1]" mode="letin"/>
+ <xsl:apply-templates select="*[1]" mode="letin_pure"/>
</xsl:template>
+<!-- Andrea: mode letin already exists in proofs.xsl, with a
+ different meaning -->
-<xsl:template match="def" mode="letin">
+<xsl:template match="def" mode="letin_pure">
<m:apply helm:xref="{@id}">
<m:csymbol>let_in</m:csymbol>
<m:bvar>
</m:ci>
</m:bvar>
<xsl:apply-templates select="*[1]" mode="noannot"/>
- <xsl:apply-templates select="following-sibling::*[1]" mode="letin"/>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="letin_pure"/>
</m:apply>
</xsl:template>
-<xsl:template match="target" mode="letin">
+<xsl:template match="target" mode="letin_pure">
<xsl:apply-templates select="*[1]" mode="noannot"/>
</xsl:template>
<m:csymbol>inst</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[1]" />
<xsl:for-each select="arg">
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:with-param></xsl:call-template></m:ci>
+ <xsl:variable name="base_path">
+ <xsl:call-template name="path">
+ <xsl:with-param name="uri" select="../*[1]/@uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="varUri" select="concat($base_path,@relUri)"/>
+ <m:ci definitionURL="{$varUri}">
+ <xsl:call-template name="insert_subscript">
+ <xsl:with-param name="node_value">
+ <xsl:call-template name="name_of_uri">
+ <xsl:with-param name="uri" select="$varUri"/>
+ <xsl:with-param name="extension" select="'.var'"/>
+ </xsl:call-template>
+ </xsl:with-param>
+ </xsl:call-template>
+ </m:ci>
<xsl:apply-templates mode ="noannot" select="*[1]" />
</xsl:for-each>
</m:apply>
<xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
<xsl:variable name="fontsymbol">
<xsl:choose>
+ <xsl:when test="$symbol = 'append'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'iff'">
+ <xsl:value-of select="'«'"/>
+ </xsl:when>
<xsl:when test="$symbol = 'forall'">
<xsl:value-of select="'"'"/>
</xsl:when>
<xsl:otherwise>
<xsl:variable name="unicodesymbol">
<xsl:choose>
+ <xsl:when test="$symbol = 'append'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'iff'">
+ <xsl:value-of select="'↔'"/>
+ </xsl:when>
<xsl:when test="$symbol = 'forall'">
<xsl:value-of select="'∀'"/>
</xsl:when>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
<xsl:text>)</xsl:text>
</xsl:when>
+ <!-- IFF -->
+ <xsl:when test="$name='iff'">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <!-- APPEND -->
+ <xsl:when test="$name='append'">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
<!-- APP -->
<xsl:when test="$name='app'">
<xsl:text>(</xsl:text>
</xsl:when>
<xsl:when test="$name='inst'">
- <xsl:apply-templates select="*[1]" mode="inline"/>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
<FONT color="blue">{</FONT>
- <xsl:text>trjsh</xsl:text>
- <xsl:apply-templates select="*[2]" mode="args"/>
+ <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+ <xsl:apply-templates select="following-sibling::*[position() = 1]" mode="inline"/>
+ <FONT color="blue">/</FONT>
+ <xsl:if test="name()='m:ci'">
+ <a href="{@definitionURL}">
+ <xsl:apply-templates/>
+ </a>
+ </xsl:if>
+ <!-- <xsl:apply-templates select="." mode="inline"/> -->
+ </xsl:for-each>
<FONT color="blue">}</FONT>
</xsl:when>
+
<!-- FIX -->
<xsl:when test="$name='fix'">
<FONT color="red">FIX</FONT>
<!-- <xsl:value-of select="$charlength"/> -->
<xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
<xsl:choose>
+ <!-- inst -->
+ <xsl:when test="$name='inst'">
+ <xsl:apply-templates select="." mode="inline"/>
+ </xsl:when>
<!-- FORALL -->
<xsl:when test="$name='forall'">
<xsl:choose>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- IFF -->
+ <xsl:when test="$name='iff'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <!-- -> -->
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="inline" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <!-- APPEND -->
+ <xsl:when test="$name='append'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <!-- -> -->
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="inline" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
<!-- APP -->
<xsl:when test="$name='app'">
<xsl:choose>
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
 
+ <xsl:if test="*[4]">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">we proved </FONT>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">and by delta equivalence</FONT>
+ <xsl:apply-templates select="*[position()=5]">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </xsl:apply-templates>
+ </xsl:if>
</span>
<xsl:choose>
<xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:call-template>\
- <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we proved</a>\
+ <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we obtain</a>\
</span>\
');
document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
</script>
</xsl:otherwise>
</xsl:choose>
- <xsl:apply-templates select="*[position()=3]">
+ <xsl:apply-templates select="*[position()=last()]">
<xsl:with-param name="current_indent" select="$current_indent + 16"/>
</xsl:apply-templates>
</xsl:when>
--- /dev/null
+<?xml version="1.0"?>
+
+<!-- Copyright (C) 2000, HELM Team -->
+<!-- -->
+<!-- This file is part of HELM, an Hypertextual, Electronic -->
+<!-- Library of Mathematics, developed at the Computer Science -->
+<!-- Department, University of Bologna, Italy. -->
+<!-- -->
+<!-- HELM is free software; you can redistribute it and/or -->
+<!-- modify it under the terms of the GNU General Public License -->
+<!-- as published by the Free Software Foundation; either version 2 -->
+<!-- of the License, or (at your option) any later version. -->
+<!-- -->
+<!-- HELM is distributed in the hope that it will be useful, -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
+<!-- GNU General Public License for more details. -->
+<!-- -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
+<!-- MA 02111-1307, USA. -->
+<!-- -->
+<!-- For details, see the HELM World-Wide-Web page, -->
+<!-- http://cs.unibo.it/helm/. -->
+
+<!--******************************************************************-->
+<!-- Disequalities -->
+<!-- (completely) Revisited: november 2002, Andrea Asperti -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:m="http://www.w3.org/1998/Math/MathML"
+ xmlns:helm="http://www.cs.unibo.it/helm">
+
+<!-- ************************* LOGIC *********************************-->
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[2]"/>
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[2]"/>
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="diseq" match="*">
+ <xsl:param name="rel" select="'eq'"/>
+ <xsl:choose>
+ <xsl:when test="name()='APPLY'">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:choose>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- REALS -->
+ <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6">
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6">
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:element name="{concat('m:',$rel)}"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:element name="{concat('m:',$rel)}"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
+</xsl:stylesheet>
<!-- coercions -->
<xsl:template match="APPLY[CONST[position()='1' and
- (@uri='cic:/Algebra/CSemiGroups/csg_crr.con' or
- @uri='cic:/Algebra/CMonoids/cm_crr.con' or
- @uri='cic:/Algebra/CGroups/cg_crr.con' or
- @uri='cic:/Algebra/CRings/cr_crr.con' or
- @uri='cic:/Algebra/CFields/cf_crr.con' or
- @uri='cic:/Algebra/COrdFields/cof_crr.con' or
- @uri='cic:/Algebra/CReals/crl_crr.con')]]">
+ (@uri='cic:/Algebra/algebra/CSemiGroups/csg_crr.con' or
+ @uri='cic:/Algebra/algebra/CMonoids/cm_crr.con' or
+ @uri='cic:/Algebra/algebra/CGroups/cg_crr.con' or
+ @uri='cic:/Algebra/algebra/CRings/cr_crr.con' or
+ @uri='cic:/Algebra/algebra/CFields/cf_crr.con' or
+ @uri='cic:/Algebra/algebra/COrdFields/cof_crr.con' or
+ @uri='cic:/Algebra/reals/CReals/crl_crr.con')]]">
<xsl:apply-templates select="*[position()=last()]"/>
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CSetoids/CSetoid_functions/csf_fun.con']]">
+ @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csf_fun.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CSetoids/CSetoid_functions/csbf_fun.con']]">
+ @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csbf_fun.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
+ @uri='cic:/Algebra/algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CRings/nat_injection/nring.con']]">
+ @uri='cic:/Algebra/algebra/CRings/nat_injection/nring.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
<xsl:include href="basic.xsl"/>
<xsl:include href="arith.xsl"/> <!-- FG -->
<xsl:include href="set.xsl"/>
+<xsl:include href="list.xsl"/>
<xsl:include href="reals.xsl"/>
<xsl:include href="ring.xsl"/> <!-- FG -->
<xsl:include href="algebra.xsl"/>
<!--******************************************************************-->
<!-- XSLT version 0.1 of CIC inductive objects to MathML content: -->
+<!-- Completely revisited: November 2002, Andrea asperti -->
<!-- First draft: March 2001, Andrea asperti -->
<!--******************************************************************-->
xmlns:m="http://www.w3.org/1998/Math/MathML"
xmlns:helm="http://www.cs.unibo.it/helm">
+<!-- try_inductive essentially checks if the head constant is an
+ invocation of an induction principle.
+ Si presuppone che il tipo induttivo non sia mutuamente
+ induttivo. Bisognerebbe andare a vedere l'utlimo parametro
+ del presunto "principio di induzione", tirare fuori il tipo induttivo
+ e vedere se il suo nome coincide con il prefisso di _ind.
+ Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
+ parametro di nat_double_ind e' di tipo nat, e nat e' diverso
+ da nat_double. Per ora, verifico solo l'esistenza di nat_double,
+ ma questo, benche' non porti ad errore, non copre tutti i
+ casi per quelli mutuamente induttivi -->
+
+
+<xsl:template mode="try_inductive" match="APPLY">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:choose>
+ <xsl:when test="CONST[1]">
+ <xsl:variable name="uri" select="CONST[1]/@uri"/>
+ <xsl:choose>
+ <xsl:when test="contains($uri,'_ind.con')">
+ <xsl:variable name="ind_uri"
+ select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
+ <xsl:variable name="inductive_def"
+ select="document($InductiveTypeUrl)/InductiveDefinition"/>
+ <xsl:choose>
+ <xsl:when test="$inductive_def">
+ <xsl:variable name="ind_name">
+ <xsl:call-template name="get_name">
+ <xsl:with-param name="uri" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:apply-templates mode="inductive" select=".">
+ <xsl:with-param name="inductive_def_uri"
+ select="$ind_uri"/>
+ <xsl:with-param name="inductive_def" select="$inductive_def"/>
+ <xsl:with-param name="inductive_def_index" select="1"/>
+ <xsl:with-param name="inductive_def_name" select="$ind_name"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="." mode="letin"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="." mode="letin"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="." mode="letin"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
<xsl:template mode="inductive" match="APPLY">
<xsl:param name="inductive_def_uri" select="''"/>
<xsl:param name="inductive_def" select="/.."/>
<xsl:param name="inductive_def_index" select="1"/>
<xsl:param name="inductive_def_name" select="''"/>
- <xsl:param name="section_params" select="0"/>
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
<!-- expected_args_type contains the types of the arguments expected by
the induction principle -->
- <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
<xsl:variable name="expected_args_types"
- select="document($InductiveTypeUrl)/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
+ select="document($InductiveTypeUrl)/ConstantType/PROD/decl/*[1]"/>
<xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
- <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
+ <xsl:variable name="actual_arguments" select="*[position()>1]"/>
<!-- First check that the induction principle is applied to the
expected number of arguments -->
<xsl:choose>
<xsl:when test="string($argsOK) = 'true'">
<!-- arguments are in the expected form: we create a
"by_induction" content element -->
- <!-- no_params is the number of paramters in square brackets -->
+ <!-- no_params is the number of parameters in square brackets -->
<xsl:variable name="no_params"
select="$inductive_def/@noParams"/>
<!-- the inductive property is the first argument following
is the uri of the inductive definition -->
<m:ci><xsl:value-of select="$inductive_def_uri"/></m:ci>
<!-- next, we have the inductive property, currently not
- used for rendering (it could be omitted??) -->
+ used for rendering (it could be omitted ??) -->
<xsl:apply-templates mode="pure" select="$inductive_property"/>
<!-- each case has its own "inductive_case" element -->
<!-- the inductive case element is composed by:
<m:csymbol>case_lhs</m:csymbol>
<m:ci definitionURL="{$inductive_def_uri}">
<xsl:value-of select="@name"/>
- </m:ci>
+ </m:ci>
<xsl:call-template name="get_constructor_args">
- <xsl:with-param name="no_params"
- select="$no_params"/>
- <xsl:with-param name="constructor_arity"
- select="*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$current_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
+ <xsl:with-param name="constructor_args"
+ select="PROD/decl[position()> $no_params]"/>
+ <xsl:with-param name="actual_args"
+ select="$current_arg/decl"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ </xsl:call-template>
</m:apply>
<m:apply>
<m:csymbol>induction_hypothesis</m:csymbol>
<xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="no_params"
- select="$no_params"/>
- <xsl:with-param name="constructor_arity"
- select="*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$current_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="PROD/decl[position()> $no_params]"/>
+ <xsl:with-param name="actual_args"
+ select="$current_arg/decl"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</m:apply>
- <xsl:call-template name="get_body">
- <xsl:with-param name="no_params"
- select="$no_params"/>
- <xsl:with-param name="constructor_arity"
- select="*[1]"/>
- <xsl:with-param name="actual_arg" select="$current_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
+ <xsl:choose>
+ <xsl:when test="count(PROD/decl) > $no_params">
+ <!-- in this case the actual_arg must be a LAMBDA -->
+ <xsl:call-template name="get_body">
+ <xsl:with-param name="constructor_args"
+ select="PROD/decl[position()>$no_params]"/>
+ <xsl:with-param name="actual_args" select="$current_arg/decl"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ <xsl:with-param name="target"
+ select="$current_arg/target/*[1]"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="noannot" select="$current_arg"/>
+ </xsl:otherwise>
+ </xsl:choose>
</m:apply>
</xsl:for-each>
<!-- the inductive argument is the last argument of extra-args -->
If this is not the case, not good rendering looks possible.
Check_args returns a boolean.
-->
+
+
<xsl:template name="check_args">
<xsl:param name="arg_types" select="/.."/>
<xsl:param name="actual_args" select="/.."/>
<xsl:value-of select="$bool_var"/>
</xsl:when>
<xsl:otherwise>
- <xsl:variable name="no_expected_arg_of_arg">
- <xsl:apply-templates mode="count_arity" select="$arg_types[1]">
- <xsl:with-param name="what" select="'PROD'"/>
- </xsl:apply-templates>
- </xsl:variable>
- <xsl:variable name="no_actual_abst_of_arg">
- <xsl:apply-templates mode="count_arity" select="$actual_args[1]">
- <xsl:with-param name="what" select="'LAMBDA'"/>
- </xsl:apply-templates>
- </xsl:variable>
- <!-- REPLACE WITH EQUALITY ???? -->
+ <xsl:variable name="no_expected_arg_of_arg"
+ select="count($arg_types[1]/PROD/decl)"/>
+ <xsl:variable name="no_actual_abst_of_arg"
+ select="count($actual_args[1]/LAMBDA/decl)"/>
<xsl:variable name="test_arg"
select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/>
<xsl:call-template name="check_args">
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
-</xsl:template>
+</xsl:template>
-<!-- count_arity counts the number of head lambda (or prod) -->
-<xsl:template mode="count_arity" match="*">
- <xsl:param name="what" select="'LAMBDA'"/>
- <xsl:param name="num" select="0"/>
- <!-- MANCANO I CAST ??? -->
- <xsl:choose>
- <xsl:when test="name(.) = $what">
- <xsl:apply-templates mode="count_arity" select="target/*[1]">
- <xsl:with-param name="what" select="$what"/>
- <xsl:with-param name="num" select="$num+1"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:value-of select="$num"/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
<!-- The following three functions are essentially identical
in their recursive structure.
single one without a conversion from document tree fragments
to node-sets.
-->
+
<xsl:template name="get_constructor_args">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
- <xsl:if test="name($constructor_arity)='PROD'">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:if test="$constructor_args">
<m:bvar>
- <m:ci><xsl:value-of select="$actual_arg/target/@binder"/></m:ci>
+ <m:ci><xsl:value-of select="$actual_args[1]/@binder"/></m:ci>
<m:type>
- <xsl:apply-templates mode="pure" select="$actual_arg/source/*[1]"/>
+ <xsl:apply-templates mode="pure" select="$actual_args[1]/*"/>
</m:type>
</m:bvar>
<xsl:choose>
- <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+ <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
<xsl:call-template name="get_constructor_args">
<xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/LAMBDA/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>2]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="get_constructor_args">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>1]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:if>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_constructor_args">
- <xsl:with-param name="no_params" select="$no_params - 1"/>
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
+</xsl:template>
<xsl:template name="get_induction_hypothesis">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
- <xsl:if test="name($constructor_arity)='PROD'">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:if test="$constructor_args">
<xsl:choose>
- <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+ <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
<m:bvar>
<m:ci>
- <xsl:value-of select="$actual_arg/target/LAMBDA/target/@binder"/>
+ <xsl:value-of select="$actual_args[2]/@binder"/>
</m:ci>
<m:type>
<xsl:apply-templates mode="pure"
- select="$actual_arg/target/LAMBDA/source"/>
+ select="$actual_args[2]/*"/>
</m:type>
</m:bvar>
<xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/LAMBDA/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>2]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>1]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:if>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="no_params" select="$no_params - 1"/>
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
</xsl:template>
<xsl:template name="get_body">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:param name="target" select="/.."/>
<xsl:choose>
- <xsl:when test="name($constructor_arity)='PROD'">
- <xsl:choose>
- <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
- <xsl:call-template name="get_body">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/LAMBDA/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_body">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="noannot" select="$actual_arg"/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_body">
- <xsl:with-param name="no_params" select="$no_params - 1"/>
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
+ <xsl:when test="$constructor_args">
+ <xsl:choose>
+ <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
+ <xsl:call-template name="get_body">
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()> 1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()> 2]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ <xsl:with-param name="target"
+ select="$target"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="get_body">
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()> 1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()> 1]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ <xsl:with-param name="target"
+ select="$target"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:choose>
+ <xsl:when test="$actual_args">
+ <xsl:apply-templates select="$actual_args[1]" mode="lambda_prop"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="noannot" select="$target"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:otherwise>
</xsl:choose>
-</xsl:template>
+</xsl:template>
</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0"?>
+
+<!-- Copyright (C) 2000, HELM Team -->
+<!-- -->
+<!-- This file is part of HELM, an Hypertextual, Electronic -->
+<!-- Library of Mathematics, developed at the Computer Science -->
+<!-- Department, University of Bologna, Italy. -->
+<!-- -->
+<!-- HELM is free software; you can redistribute it and/or -->
+<!-- modify it under the terms of the GNU General Public License -->
+<!-- as published by the Free Software Foundation; either version 2 -->
+<!-- of the License, or (at your option) any later version. -->
+<!-- -->
+<!-- HELM is distributed in the hope that it will be useful, -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
+<!-- GNU General Public License for more details. -->
+<!-- -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
+<!-- MA 02111-1307, USA. -->
+<!-- -->
+<!-- For details, see the HELM World-Wide-Web page, -->
+<!-- http://cs.unibo.it/helm/. -->
+
+<!--******************************************************************-->
+<!-- Basic Logic -->
+<!-- (completely) Revisited: november 2002, Andrea Asperti -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:m="http://www.w3.org/1998/Math/MathML"
+ xmlns:helm="http://www.cs.unibo.it/helm">
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and count(child::*) = 3]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>false_ind</m:csymbol>
+ <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ </m:apply>
+</xsl:template>
+
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/and_ind.con'] and
+ count(child::*) = 6 and name(*[5])='LAMBDA' and
+ count(*[5]/decl) = 2]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>and_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[6]"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
+ <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/or_ind.con']
+ and count(child::*) = 7 and
+ name(*[5])='LAMBDA' and count(*[5]/decl) = 1 and
+ name(*[6])='LAMBDA' and count(*[6]/decl) = 1 ]">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="definition_url"
+ select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>full_or_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[7]"/>
+ <xsl:for-each select="$InnerTypes">
+ <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+ </xsl:for-each>
+ <m:apply>
+ <m:csymbol>left_case</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:value-of select="*[5]/*[1]/@binder"/>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
+ </m:apply>
+ <m:apply>
+ <m:csymbol>right_case</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates mode="pure" select="*[6]/*[1]/*"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates mode="noannot" select="*[6]/target"/>
+ </m:apply>
+ </m:apply>
+
+<!-- da tertminare
+ </xsl:when>
+ <xsl:otherwise>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>or_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[7]"/>
+ <xsl:for-each select="$InnerTypes">
+ <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+ </xsl:for-each>
+ <xsl:apply-templates mode="pure" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ </m:apply>
+ </xsl:otherwise>
+ </xsl:choose>
+-->
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'] and
+ count(child::*) = 6 and
+ name(*[5])='LAMBDA' and count(*[5]/decl) = 2 ]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>ex_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[6]"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
+ <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
+ </m:apply>
+</xsl:template>
+
+</xsl:stylesheet>
+
</xsl:template>
<xsl:template match="ConstantType" mode="noannot">
+ <xsl:variable name="ConstantBodyUrl"
+ select="concat($BaseCICURI,'.body')"/>
<Definition name="{@name}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<Params>
</body>
</xsl:otherwise>
</xsl:choose> -->
- <body/>
+ <body>
+ <m:ci definitionURL="{$ConstantBodyUrl}">click here</m:ci>
+ </body>
<type>
<xsl:apply-templates select="./*[1]"/>
</type>
<!-- CSC: PROBLEMA: URI CHE NON CONTENGONO / ED INIZIANO CON cic: -->
<xsl:template name="name_of_uri">
<xsl:param name="uri" select=""""/>
+ <xsl:param name="extension" select="'.con'"/>
<xsl:variable name="suffix" select="substring-after($uri, "/")"/>
<xsl:choose>
<xsl:when test="$suffix = """>
<!-- CSC: PROBLEMA: .con PUO' APPARIRE ALL'INTERNO DELLE URI ===>
SCRIVERE UNA FUNZIONE RICORSIVA CHE RISOLVA -->
- <xsl:value-of select="substring-before($uri,".con")"/>
+ <xsl:value-of select="substring-before($uri,$extension)"/>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="name_of_uri">
<xsl:with-param name="uri" select="$suffix"/>
+ <xsl:with-param name="extension" select="$extension"/>
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:choose>
</xsl:template>
+<!-- path gives the path of a uri, up to the final name -->
+<xsl:template name="path">
+ <xsl:param name="uri" select=""""/>
+ <xsl:param name="current_path" select=""""/>
+ <xsl:choose>
+ <xsl:when test="(substring-after($uri,"/") != "")">
+ <xsl:call-template name="path">
+ <xsl:with-param
+ name="uri" select="substring-after($uri,"/")"/>
+ <xsl:with-param
+ name="current_path" select="concat($current_path,substring-before($uri,"/"),'/')"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$current_path"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
<xsl:template name="blank_counting">
<xsl:param name="string" select=""""/>
<xsl:param name="counter" select="0"/>
xmlns:m="http://www.w3.org/1998/Math/MathML"
xmlns:helm="http://www.cs.unibo.it/helm">
+<xsl:include href="logic.xsl"/>
+<xsl:include href="inductive.xsl"/>
+<xsl:include href="rewrite.xsl"/>
+<xsl:include href="diseq.xsl"/>
+
<!-- ************************* LOGIC *********************************-->
<!-- Proof objects -->
<!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
-<!-- LAMBDA has inner type only if it is not nested inside another lambda -->
<xsl:template match="LAMBDA" mode="noannot">
- <xsl:variable name="id" select="decl/@id"/>
+ <xsl:choose>
+ <xsl:when test="@sort='Prop'">
+ <xsl:apply-templates select="*[1]" mode="lambda_prop"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <!-- mode lambda is defined in content.xsl -->
+ <xsl:apply-templates select="*[1]" mode="lambda"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="decl" mode="lambda_prop">
+ <xsl:variable name="id" select="@id"/>
<xsl:variable name="innertype_available">
<xsl:for-each select="$InnerTypes">
<xsl:if test="key('typeid',$id)/*">
</xsl:if>
</xsl:for-each>
</xsl:variable>
- <!--xsl:value-of select="concat('NL: ',$naturalLanguage,' IA: ',$innertype_available)"/-->
<xsl:choose>
- <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
- <m:apply helm:xref="{decl/@id}">
+ <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
+ <m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
- <xsl:apply-templates mode="proof_transform" select="."/>
+ <m:lambda helm:xref="{@id}">
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
+ </m:lambda>
<xsl:for-each select="$InnerTypes">
<xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
</xsl:for-each>
</m:apply>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates select="." mode="pure"/>
+ <m:lambda helm:xref="{@id}">
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
+ </m:lambda>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
-<!-- ALL these elements have inner type -->
-<xsl:template match="LETIN|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="target" mode="lambda_prop">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+<!-- LETIN -->
+
+<xsl:template match="LETIN" mode="noannot">
+ <xsl:choose>
+ <xsl:when test="@sort='Prop'">
+ <xsl:apply-templates select="*[1]" mode="letin_prop"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <!-- mode letin is defined in content.xsl -->
+ <xsl:apply-templates select="*[1]" mode="letin_pure"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="def" mode="letin_prop">
<xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+ <xsl:for-each select="$InnerTypes">
+ <xsl:if test="key('typeid',$id)/*">
+ <xsl:text>yes</xsl:text>
+ </xsl:if>
+ </xsl:for-each>
+ </xsl:variable>
<xsl:choose>
- <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
+ <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
<m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
- <xsl:apply-templates mode="proof_transform" select="."/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>let_in</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ </m:bvar>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
+ </m:apply>
<xsl:for-each select="$InnerTypes">
<xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
</xsl:for-each>
</m:apply>
</xsl:when>
<xsl:otherwise>
- <xsl:choose>
- <xsl:when test="name()='APPLY'">
- <!-- This is the case of an applicative expression wich is not
- a proof but could contains proofs...
- MODE LETIN OR MODE PURE ??? Big question -->
- <xsl:apply-templates select="." mode="pure"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates select="." mode="pure"/>
- </xsl:otherwise>
- </xsl:choose>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>let_in</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ </m:bvar>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
+ </m:apply>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
-<!-- si presuppone che il tipo induttivo non sia mutuamente
- induttivo. Bisognerebbe andare a vedere l'ultimo parametro
- del presunto "principio di induzione", tirare fuori il tipo induttivo
- e vedere se il suo nome coincide con il prefisso di _ind.
- Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
- parametro di nat_double_ind e' di tipo nat, e nat e' diverso
- da nat_double. Per ora, verifico solo l'esistenza di nat_double,
- ma questo, benche' non porti ad errore, non copre tutti i
- casi per quelli mutuamente induttivi -->
-
-<xsl:template mode="try_inductive" match="APPLY">
- <xsl:variable name="id" select="@id"/>
- <xsl:choose>
- <xsl:when test="CONST[1]">
- <xsl:variable name="uri" select="CONST[1]/@uri"/>
- <xsl:choose>
- <xsl:when test="contains($uri,'_ind.con')">
- <xsl:variable name="ind_uri"
- select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
- <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
- <xsl:variable name="inductive_def"
- select="document($InductiveTypeUrl)/InductiveDefinition"/>
- <!-- check if the corresponding inductive definition actually
- exists -->
- <xsl:choose>
- <xsl:when test="$inductive_def">
- <xsl:variable name="ind_name">
- <xsl:call-template name="get_name">
- <xsl:with-param name="uri" select="$uri"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:variable name="no_params">
- <xsl:call-template name="get_no_params">
- <xsl:with-param name="first_uri" select="$CICURI"/>
- <xsl:with-param name="second_uri" select="$uri"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:apply-templates mode="inductive" select=".">
- <xsl:with-param name="inductive_def_uri"
- select="$ind_uri"/>
- <xsl:with-param name="inductive_def"
- select="$inductive_def"/>
- <xsl:with-param name="section_params" select="$no_params"/>
- <xsl:with-param name="inductive_def_index" select="1"/>
- <xsl:with-param name="inductive_def_name" select="$ind_name"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="letin" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="letin" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="letin" select="."/>
- </xsl:otherwise>
- </xsl:choose>
+<xsl:template match="target" mode="letin_prop">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
</xsl:template>
-<xsl:template mode="eq_transitive" match="*">
- <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
+<!-- ALL these elements have inner type -->
+<xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
+ <xsl:variable name="id" select="@id"/>
<xsl:choose>
- <xsl:when test="name()='APPLY'">
- <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
- <xsl:variable name="id" select="@id"/>
- <xsl:choose>
- <!-- ricordarsi di trattare il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/eq_transitive_unfolded.con'] and count(child::*) = 7">
- <!-- <m:ci>eccomi-3</m:ci> -->
- <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
+ <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>proof</m:csymbol>
+ <xsl:apply-templates mode="proof_transform" select="."/>
+ <xsl:for-each select="$InnerTypes">
+ <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
+ </xsl:for-each>
+ </m:apply>
</xsl:when>
<xsl:otherwise>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template mode="diseq" match="*">
- <xsl:param name="rel" select="'eq'"/>
- <xsl:choose>
- <xsl:when test="name()='APPLY'">
- <xsl:variable name="id" select="@id"/>
<xsl:choose>
- <!-- ricordarsi di trattare il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_transitive.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdl.con'] and count(child::*) = 7">
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algerba/COrdFields/leEq_less_trans.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
+ <xsl:when test="name()='APPLY'">
+ <!-- This is the case of an applicative expression wich is not
+ a proof but could contains proofs...
+ MODE LETIN OR MODE PURE ??? Big question -->
+ <xsl:apply-templates select="." mode="pure"/>
</xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_leEq_trans.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdr.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_transitive_unfolded.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdr.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdl.con'] and count(child::*) = 7">
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- </xsl:when>
- <!--
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]"/>
- <m:eq/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <m:eq/>
- <xsl:apply-templates mode="diseq" select="*[7]"/>
- </xsl:when>
- -->
<xsl:otherwise>
- <xsl:element name="{concat('m:',$rel)}"/>
- <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
+ <xsl:apply-templates select="." mode="pure"/>
</xsl:otherwise>
</xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:element name="{concat('m:',$rel)}"/>
- <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<xsl:when test="name()='APPLY'">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
- <!-- Algebra equality (eq_transitive_unfolded) -->
- <!-- It requires a special mode "eq_transitive"-->
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/eq_transitive_unfolded.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>eq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <!-- Algebra disequalities -->
- <!-- It requires a special mode "diseq"-->
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_transitive.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdl.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_less_trans.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_leEq_trans.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdr.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_transitive_unfolded.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdr.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdl.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- </m:apply>
- </xsl:when>
- <!-- EQUALITY -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
- </m:apply>
- </xsl:when>
- <!-- EQUALITY with extra-parameters -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
- <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
- <xsl:choose>
- <xsl:when test="$no_extraproofs=0">
- <m:apply>
- <m:csymbol>rewrite_and_apply</m:csymbol>
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
- </m:apply>
- <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <xsl:choose>
- <xsl:when test="*[5]/@sort='Prop'">
- <m:apply helm:xref="{@id}">
- <m:csymbol>letin</m:csymbol>
- <m:apply>
- <m:csymbol>let</m:csymbol>
- <m:ci>
- <xsl:call-template name="insert_subscript">
- <xsl:with-param name="node_value" select="'h1'"/>
- </xsl:call-template>
- </m:ci>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- <xsl:call-template name="gen_let">
- <xsl:with-param name="init_pos" select="1"/>
- <xsl:with-param name="from" select="7"/>
- </xsl:call-template>
- <m:apply>
- <m:csymbol>rewrite_and_apply</m:csymbol>
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <m:ci>
- <xsl:call-template name="insert_subscript">
- <xsl:with-param name="node_value" select="'h1'"/>
- </xsl:call-template>
- </m:ci>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
- </m:apply>
- <xsl:apply-templates mode="flat" select="*[8]">
- <xsl:with-param name="n">
- <xsl:value-of select="2"/>
- </xsl:with-param>
- </xsl:apply-templates>
- </m:apply>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <m:apply helm:xref="{@id}">
- <m:csymbol>letin</m:csymbol>
- <xsl:call-template name="gen_let">
- <xsl:with-param name="init_pos" select="0"/>
- <xsl:with-param name="form" select="7"/>
- </xsl:call-template>
- <m:apply>
- <m:csymbol>rewrite_and_apply</m:csymbol>
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="pure" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
- </m:apply>
- <xsl:apply-templates mode="flat" select="*[8]">
- <xsl:with-param name="n">
- <xsl:value-of select="1"/>
- </xsl:with-param>
- </xsl:apply-templates>
- </m:apply>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <!-- False_ind -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
- count(child::*) = 3">
- <m:apply helm:xref="{@id}">
- <m:csymbol>false_ind</m:csymbol>
- <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- </m:apply>
- </xsl:when>
- <!-- gestire meglio il caso di and_ind quando la prova
- non e' della forma \x.\y.M -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/and_ind.con']
- and count(child::*) = 6
- and name(*[5])='LAMBDA'">
- <m:apply helm:xref="{@id}">
- <m:csymbol>and_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[6]"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
- <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/or_ind.con']
- and count(child::*) = 7">
- <xsl:choose>
- <xsl:when test="name(*[5])='LAMBDA'
- and name(*[6])='LAMBDA'">
- <xsl:variable name="definition_url"
- select="'cic:/Coq/Init/Logic/or.ind'"/>
- <m:apply helm:xref="{@id}">
- <m:csymbol>full_or_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[7]"/>
- <xsl:for-each select="$InnerTypes">
- <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
- </xsl:for-each>
- <m:apply>
- <m:csymbol>left_case</m:csymbol>
- <m:bvar>
- <m:ci>
- <xsl:value-of select="*[5]/*[1]/@binder"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates mode="pure" select="*[5]/*[1]/*[1]"/>
- </m:type>
- </m:bvar>
- <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
- </m:apply>
- <m:apply>
- <m:csymbol>right_case</m:csymbol>
- <m:bvar>
- <m:ci>
- <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates mode="pure" select="*[6]/*[1]/*[1]"/>
- </m:type>
- </m:bvar>
- <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
- </m:apply>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <m:apply helm:xref="{@id}">
- <m:csymbol>or_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[7]"/>
- <xsl:for-each select="$InnerTypes">
- <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
- </xsl:for-each>
- <xsl:apply-templates mode="pure" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <!-- ex_ind, exT_ind -->
- <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
- CONST[attribute::uri='cic:/Coq/Init/Logic/ex_ind.con'])
- and count(child::*) = 6
- and name(*[5])='LAMBDA'
- and name(*[5]/*[2])='decl'">
- <m:apply helm:xref="{@id}">
- <m:csymbol>ex_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[6]"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
- <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
- </m:apply>
- </xsl:when>
<xsl:when test="name(*[1])='CONST'">
<xsl:apply-templates mode="try_inductive" select="."/>
</xsl:when>
<!-- patch temporanea per la gestione di redex -->
- <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
- and *[2]/@sort='Prop'">
+ <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2">
+ <!-- old
+ and *[2]/@sort='Prop'"> -->
<m:apply helm:xref="{@id}">
- <m:csymbol>letin</m:csymbol>
- <m:apply>
- <m:csymbol>let</m:csymbol>
+ <m:csymbol>let_in</m:csymbol>
+ <m:bvar>
<m:ci>
<xsl:call-template name="insert_subscript">
<xsl:with-param name="node_value">
</xsl:with-param>
</xsl:call-template>
</m:ci>
- <xsl:apply-templates mode="noannot" select="*[2]"/>
- </m:apply>
+ </m:bvar>
+ <xsl:apply-templates mode="noannot" select="*[2]"/>
<xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
</m:apply>
</xsl:when>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
- <xsl:when test="name()='LAMBDA'">
- <xsl:choose>
- <xsl:when test="(name(target/*[1])='APPLY' and
- name(target/*[1]/*[1])='CONST' and
- (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
- and count(target/*[1]/*) = 8
- and name(target/*[1]/*[8])='REL'
- and target/@binder = target/*[1]/*[8]/@binder )">
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
- <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
- <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="pure" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
<xsl:otherwise>
<xsl:apply-templates select="." mode="pure"/>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
+
+<xsl:template name="gen_let">
+ <xsl:param name="init_pos" select="1"/>
+ <xsl:param name="from" select="0"/>
+ <xsl:apply-templates mode="gen_let_aux" select="*[position() = ($from+1)]">
+ <xsl:with-param name="init_pos" select="$init_pos"/>
+ </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template mode="gen_let_aux" match="*">
+ <xsl:param name="init_pos" select="1"/>
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+ <xsl:for-each select="$InnerTypes">
+ <xsl:if test="key('typeid',$id)/*">
+ <xsl:text>yes</xsl:text>
+ </xsl:if>
+ </xsl:for-each>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when 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')">
+ <m:apply>
+ <m:csymbol>let</m:csymbol>
+ <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>
+ <xsl:apply-templates mode="noannot" select="."/>
+ </m:apply>
+ <xsl:if test="following-sibling::*[1]">
+ <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
+ <xsl:with-param name="init_pos" select="$init_pos+1"/>
+ </xsl:apply-templates>
+ </xsl:if>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:if test="following-sibling::*[1]">
+ <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
+ <xsl:with-param name="init_pos" select="$init_pos"/>
+ </xsl:apply-templates>
+ </xsl:if>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- questa vecchia versione (di Claudio??) sembra bacata come un melone.
+
<xsl:template name="gen_let">
<xsl:param name="init_pos" select="0"/>
<xsl:param name="from" select="0"/>
</m:apply>
</xsl:if>
</xsl:for-each>
-</xsl:template>
+</xsl:template> -->
<xsl:template match="*" mode="erase">
<xsl:choose>
- <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:when test="@sort='Prop'
+ or name()='instantiate' or $naturalLanguage='no'">
<xsl:apply-templates mode="pure" select="."/>
</xsl:when>
<xsl:otherwise>
<xsl:otherwise>
<!-- forse bisognerebbe trattare solo l'elemento di testa -->
<xsl:choose>
- <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:when test="@sort='Prop'
+ or name()='instantiate' or $naturalLanguage='no'">
<xsl:apply-templates mode="pure" select="."/>
</xsl:when>
<xsl:otherwise>
</xsl:when>
<xsl:otherwise>
<xsl:choose>
- <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
+ <xsl:when test="name()='REL' or name()='instantiate' or @sort='Prop' or $naturalLanguage='no'">
<xsl:apply-templates mode="pure" select="."/>
</xsl:when>
<xsl:otherwise>
</xsl:choose>
</xsl:template>
-<!-- <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
- <xsl:choose>
- <xsl:when test="count(child::*) > 4">
- <m:apply helm:xref="{@id}">
- <m:csymbol>app</m:csymbol>
- <xsl:apply-templates mode="pure" select="*[1]"/>
- <m:ci>*</m:ci>
- <m:ci>*</m:ci>
- <m:ci>*</m:ci>
- <xsl:apply-templates mode="flat" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <m:apply helm:xref="{@id}">
- <m:csymbol>app</m:csymbol>
- <xsl:apply-templates mode="flat" select="*[1]"/>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template> -->
-
</xsl:stylesheet>
--- /dev/null
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
+<!-- GNU General Public License for more details. -->
+<!-- -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
+<!-- MA 02111-1307, USA. -->
+<!-- -->
+<!-- For details, see the HELM World-Wide-Web page, -->
+<!-- http://cs.unibo.it/helm/. -->
+
+<!--******************************************************************-->
+<!-- Basic Logic -->
+<!-- (completely) Revisited: february 2001, Andrea Asperti -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:m="http://www.w3.org/1998/Math/MathML"
+ xmlns:helm="http://www.cs.unibo.it/helm">
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7]">
+ <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
+ <xsl:choose>
+ <xsl:when test="$no_extraproofs=0">
+ <m:apply>
+ <m:csymbol>rewrite_and_apply</m:csymbol>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+ <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:choose>
+ <xsl:when test="*[5]/@sort='Prop'">
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>letin</m:csymbol>
+ <m:apply>
+ <m:csymbol>let</m:csymbol>
+ <m:ci>
+ <xsl:call-template name="insert_subscript">
+ <xsl:with-param name="node_value" select="'h1'"/>
+ </xsl:call-template>
+ </m:ci>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ <xsl:call-template name="gen_let">
+ <xsl:with-param name="init_pos" select="1"/>
+ <xsl:with-param name="from" select="7"/>
+ </xsl:call-template>
+ <m:apply>
+ <m:csymbol>rewrite_and_apply</m:csymbol>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <m:ci>
+ <xsl:call-template name="insert_subscript">
+ <xsl:with-param name="node_value" select="'h1'"/>
+ </xsl:call-template>
+ </m:ci>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+ <xsl:apply-templates mode="flat" select="*[8]">
+ <xsl:with-param name="n">
+ <xsl:value-of select="2"/>
+ </xsl:with-param>
+ </xsl:apply-templates>
+ </m:apply>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>letin</m:csymbol>
+ <xsl:call-template name="gen_let">
+ <xsl:with-param name="init_pos" select="0"/>
+ <xsl:with-param name="form" select="7"/>
+ </xsl:call-template>
+ <m:apply>
+ <m:csymbol>rewrite_and_apply</m:csymbol>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="pure" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+ <xsl:apply-templates mode="flat" select="*[8]">
+ <xsl:with-param name="n">
+ <xsl:value-of select="1"/>
+ </xsl:with-param>
+ </xsl:apply-templates>
+ </m:apply>
+ </m:apply>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+</xsl:stylesheet>
\ No newline at end of file
<xsl:variable name="ConstantTypeUrl"><xsl:call-template name="makeURL4InnerTypes"><xsl:with-param name="uri" select="$BaseCICURI"/></xsl:call-template></xsl:variable>
<xsl:variable name="AnnotationsUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$AnnotationsUri"/></xsl:call-template></xsl:variable>
+
<!-- WARNING: Using lazy evaluation: $CICURI.* may not exist, but -->
<!-- document() is called only by need!!! -->
<xsl:variable name="InnerTypes" select="document($InnerTypesUrl)"/>
<xsl:include href="headercontent.xsl"/>
<xsl:include href="proofs.xsl"/>
-<xsl:include href="inductive.xsl"/>
<xsl:variable name="showproof" select="0"/>
</xsl:stylesheet>
+
+
+
+
+
+
+
+
content.xsl
content_to_html.xsl
contentlib.xsl
+diseq.xsl
drop_coercions.xsl
expandobj.xsl
genmmlid.xsl
lambda.xsl
link.xsl
links_library.xsl
+logic.xsl
mk_dep_graph.xsl
mk_meta_and_dep_graph.xsl
mk_meta_graph.xsl
objtheorycontent.xsl
params.xsl
proofs.xsl
+rewrite.xsl
ricerca.xsl
ring.xsl
rootcontent.xsl
projects / helm.git / commitdiff