<xsl:apply-templates select="*[1]"/>
</xsl:template>
+
+<!-- FUNZIONI AUSILIARIE -->
+
+<xsl:template name="name_of_uri_bis">
+ <xsl:param name="uri" select=""""/>
+ <xsl:variable name="suffix" select="substring-after($uri, "/")"/>
+ <xsl:choose>
+ <xsl:when test="$suffix = """>
+ <xsl:value-of select="substring-before($uri,".var")"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="name_of_uri_bis">
+ <xsl:with-param name="uri" select="$suffix"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="var_name">
+ <xsl:param name="uri"/>
+ <xsl:param name="string" select=""""/>
+ <xsl:variable name="prefix" select="substring-before($uri, " ")"/>
+ <xsl:variable name="suffix" select="substring-after($uri, " ")"/>
+ <xsl:variable name="prefix">
+ <xsl:call-template name="name_of_uri_bis">
+ <xsl:with-param name="uri" select="$prefix"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <!--xsl:if test="string($prefix) != " " "-->
+ <xsl:variable name="string" select="concat($string,', ', $prefix)"/>
+ <!--/xsl:if-->
+ <xsl:choose>
+ <xsl:when test="$suffix = """>
+ <xsl:value-of select="substring-after(concat($string, ' '),',')"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="$suffix"/>
+ <xsl:with-param name="string" select="$string"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
<!-- CIC OBJECTS -->
-<xsl:template match="Definition" mode="noannot">
+<xsl:template match="Sequent"> <!-- For Sequents there are no annotations -->
+ <Sequent helm:xref="{@id}" no="{@no}">
+ <xsl:for-each select="Decl|Def|Hidden">
+ <xsl:copy>
+ <xsl:attribute name="name">
+ <xsl:value-of select="@name"/>
+ </xsl:attribute>
+ <xsl:attribute name="helm:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ <xsl:apply-templates select="*[1]"/>
+ </xsl:copy>
+ </xsl:for-each>
+ <Goal>
+ <xsl:apply-templates select="Goal/*[1]"/>
+ </Goal>
+ </Sequent>
+</xsl:template>
+
+<xsl:template match="ConstantType" mode="noannot">
<Definition name="{@name}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<Params>
- <xsl:value-of select="@params"/>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+ </xsl:call-template>
</Params>
</xsl:if>
<!-- <xsl:choose>
</body>
</xsl:otherwise>
</xsl:choose> -->
- <body>
- <xsl:apply-templates select="body/*[1]"/>
- </body>
+ <body/>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="./*[1]"/>
</type>
</Definition>
</xsl:template>
-<xsl:template match="Axiom" mode="noannot">
- <Axiom name="{@name}" helm:xref="{@id}">
+<xsl:template match="ConstantBody" mode= "noannot">
+ <Definition name="{@for}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<Params>
- <xsl:value-of select="@params"/>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+ </xsl:call-template>
</Params>
</xsl:if>
+ <body>
+ <xsl:apply-templates select="./*[1]"/>
+ </body>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
</type>
- </Axiom>
+ </Definition>
</xsl:template>
+
<xsl:template match="CurrentProof" mode="noannot">
- <CurrentProof name="{@name}" helm:xref="{@id}">
+ <CurrentProof name="{@of}" helm:xref="{@id}">
<xsl:for-each select="Conjecture">
- <Conjecture no="./{@no}">
- <xsl:apply-templates select="."/>
+ <Conjecture no="{@no}" helm:xref="{@id}">
+ <xsl:for-each select="*">
+ <xsl:copy>
+ <xsl:copy-of select="@of"/>
+ <xsl:attribute name="helm:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ <xsl:apply-templates select="*"/>
+ </xsl:copy>
+ </xsl:for-each>
</Conjecture>
</xsl:for-each>
<body>
<xsl:apply-templates select="body/*[1]"/>
</body>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
</type>
</CurrentProof>
</xsl:template>