3 <!--******************************************************************-->
4 <!-- XSLT version 0.1 of CIC objects to objects and MathML content: -->
5 <!-- First draft: March 21 2000, Irene Schena -->
6 <!--******************************************************************-->
8 <!--******************************************************************-->
9 <!-- MANCA: gestione annotation e linking -->
10 <!--******************************************************************-->
12 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
13 xmlns:m="http://www.w3.org/1998/Math/MathML"
14 xmlns:helm="http://www.cs.unibo.it/helm">
16 <xsl:import href="content.xsl"/>
20 <xsl:template match="cicxml">
21 <xsl:variable name="url"><xsl:value-of select="@baseurl"/></xsl:variable>
22 <xsl:variable name="stylesheet"><xsl:value-of select="@stylesheet"/></xsl:variable>
23 <xsl:processing-instruction name="cocoon-format">type="text/xml"</xsl:processing-instruction>
24 <xsl:processing-instruction name="xml-stylesheet">href="<xsl:value-of select='concat($url,$stylesheet)'/>" type="text/xsl"</xsl:processing-instruction>
25 <xsl:processing-instruction name="cocoon-process">type="xslt"</xsl:processing-instruction>
26 <xsl:apply-templates select="*[1]"/>
31 <xsl:template match="Definition" mode="noannot">
32 <Definition name="{@name}" helm:xref="{@id}">
33 <xsl:if test="string(@params) != """>
35 <xsl:value-of select="@params"/>
39 <xsl:apply-templates select="body"/>
42 <xsl:apply-templates select="type"/>
47 <xsl:template match="Axiom" mode="noannot">
48 <Axiom name="{@name}" helm:xref="{@id}">
49 <xsl:if test="string(@params) != """>
51 <xsl:value-of select="@params"/>
55 <xsl:apply-templates select="type"/>
60 <xsl:template match="CurrentProof" mode="noannot">
61 <CurrentProof name="{@name}" helm:xref="{@id}">
62 <xsl:for-each select="Conjecture">
63 <Conjecture no="./{@no}">
64 <xsl:apply-templates select="."/>
68 <xsl:apply-templates select="body"/>
71 <xsl:apply-templates select="type"/>
76 <xsl:template match="InductiveDefinition" mode="noannot">
77 <InductiveDefinition helm:xref="{@id}">
78 <xsl:if test="string(@params) != """>
80 <xsl:value-of select="@params"/>
83 <xsl:if test="string(@noParams) != 0">
84 <xsl:apply-templates select="InductiveType/arity/*[1]" mode="abstparams">
85 <xsl:with-param name="noparams" select="@noParams"/>
86 </xsl:apply-templates>
88 <xsl:for-each select="InductiveType">
89 <InductiveType name="{./@name}" inductive="{./@inductive}">
91 <xsl:apply-templates select="./arity/*[1]" mode="abstparams">
92 <xsl:with-param name="noparams" select="../@noParams"/>
93 <xsl:with-param name="target" select="1"/>
94 </xsl:apply-templates>
96 <xsl:for-each select="./Constructor">
97 <Constructor name="{./@name}">
98 <xsl:apply-templates select="./*[1]" mode="abstparams">
99 <xsl:with-param name="noparams" select="../../@noParams"/>
100 <xsl:with-param name="target" select="1"/>
101 </xsl:apply-templates>
106 </InductiveDefinition>
109 <xsl:template match="Variable" mode="noannot">
110 <Variable name="{@name}" helm:xref="{@id}">
112 <xsl:apply-templates select="type"/>
117 <!--*******************************************-->
118 <!-- ABSTRACTING PARAMETERS AND COUNTING -->
119 <!--*******************************************-->
120 <!-- Si dimentica i CAST dei termini che astrae. Nel caso dell'astrazione -->
121 <!-- dei lambda dei pattern del CASE, qualora i lambda non si trovino -->
122 <!-- nella forma weak-head, astrae solo i lambda che trova e restituisce -->
123 <!-- un corpo depurato da tutti i primi cast che precedono il termine -->
126 <xsl:template match="*" mode="abstparams">
127 <xsl:param name="noparams" select="0"/>
128 <xsl:param name="target" select="0"/>
129 <xsl:param name="binder">PROD</xsl:param>
131 <xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)="CAST"))">
133 <xsl:when test="name(.) = string($binder)">
134 <xsl:if test="$target = 0">
136 <xsl:when test="string($binder) = "LAMBDA"">
138 <xsl:value-of select="target/@binder"/>
142 <Param name="{target/@binder}">
143 <xsl:apply-templates select="source" mode="noannot"/>
148 <xsl:apply-templates select="target/*[1]" mode="abstparams">
149 <xsl:with-param name="noparams" select="$noparams - 1"/>
150 <xsl:with-param name="target" select="$target"/>
151 <xsl:with-param name="binder" select="$binder"/>
152 </xsl:apply-templates>
155 <xsl:apply-templates select="term/*[1]" mode="abstparams">
156 <xsl:with-param name="noparams" select="$noparams"/>
157 <xsl:with-param name="target" select="$target"/>
158 <xsl:with-param name="binder" select="$binder"/>
159 </xsl:apply-templates>
165 <xsl:when test="($target = 1) and ($noparams != 0)">
167 <m:csymbol>app</m:csymbol>
168 <xsl:apply-templates select="." mode="noannot"/>
169 <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
174 <xsl:when test="$noparams != 0">
175 <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
178 <xsl:if test="$target = 1">
179 <xsl:apply-templates select="." mode="noannot"/>
189 <xsl:template name="printparam">
190 <xsl:param name="noleft" select="0"/>
191 <xsl:param name="number" select="1"/>
192 <xsl:if test="$noleft != 0">
193 <m:ci>$<xsl:value-of select="$number"/></m:ci>
194 <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noleft - 1"/><xsl:with-param name="number" select="$number + 1"/></xsl:call-template>
198 <xsl:template match="*" mode="counting">
199 <xsl:param name="noparams" select="0"/>
200 <xsl:param name="count" select="0"/>
202 <xsl:when test="name(.) = "PROD"">
203 <xsl:apply-templates select="target/*[1]" mode="counting">
204 <xsl:with-param name="noparams" select="$noparams"/>
205 <xsl:with-param name="count" select="$count + 1"/>
206 </xsl:apply-templates>
208 <xsl:when test="name(.) = "CAST"">
209 <xsl:apply-templates select="term/*[1]" mode="counting">
210 <xsl:with-param name="noparams" select="$noparams"/>
211 <xsl:with-param name="count" select="$count"/>
212 </xsl:apply-templates>
215 <xsl:value-of select="$count - $noparams"/>