<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="prefix0" 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="$prefix0"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <!--xsl:if test="string($prefix) != " " "-->
+ <xsl:variable name="string1" select="concat($string,', ', $prefix)"/>
+ <!--/xsl:if-->
+ <xsl:choose>
+ <xsl:when test="$suffix = """>
+ <xsl:value-of select="substring-after(concat($string1, ' '),',')"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="$suffix"/>
+ <xsl:with-param name="string" select="$string1"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
<!-- CIC OBJECTS -->
<xsl:template match="Sequent"> <!-- For Sequents there are no annotations -->
</Sequent>
</xsl:template>
-<xsl:template match="Definition" mode="noannot">
+<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>
- <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>
</xsl:otherwise>
</xsl:choose> -->
<body>
- <xsl:apply-templates select="body/*[1]"/>
+ <m:ci definitionURL="{$ConstantBodyUrl}">click here</m:ci>
</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}" helm:xref="{@id}">
<xsl:for-each select="*">
<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>