3 <!--******************************************************************-->
5 <!-- First draft: April 3 2000 -->
6 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
7 <!--******************************************************************-->
9 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
10 xmlns:m="http://www.w3.org/1998/Math/MathML"
11 xmlns:helm="http://www.cs.unibo.it/helm"
12 xmlns:xlink="http://www.w3.org/1999/xlink">
14 <!--******************************************************************-->
15 <!-- Variable containing the absolute path of the CIC file -->
16 <!--******************************************************************-->
18 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
20 <!-- ************************* LOGIC *********************************-->
25 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R.con']" mode="pure">
32 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R0.con']" mode="pure">
33 <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
36 <xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R1.con']" mode="pure">
37 <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
42 <!-- Unary Operations -->
44 <xsl:template match="APPLY[CONST[
45 attribute::uri='cic:/Coq/Reals/Rdefinitions/Ropp.con' or
46 attribute::uri='cic:/Coq/Reals/Rbasic_fun/Rabsolu.con' or
47 attribute::uri='cic:/Coq/Reals/Rfunctions/fact.con' or
48 attribute::uri='cic:/Coq/Reals/Rbase/Rsqr.con']]" mode="pure">
50 <xsl:when test="count(child::*) = 2">
51 <xsl:variable name="elem">
53 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Ropp.con'">
54 <xsl:value-of select="'minus'"/>
56 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rabsolu.con'">
57 <xsl:value-of select="'abs'"/>
59 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rfunctions/fact.con'">
60 <xsl:value-of select="'factorial'"/>
62 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbase/Rsqr.con'">
63 <xsl:value-of select="'root'"/>
67 <m:apply helm:xref="{@id}">
68 <xsl:element name="{concat('m:',$elem)}">
69 <xsl:attribute name="definitionURL">
70 <xsl:value-of select="CONST/@uri"/>
72 <xsl:attribute name="helm:xref">
73 <xsl:value-of select="CONST/@id"/>
76 <xsl:apply-templates select="*[2]" mode="noannot"/>
85 <xsl:template match="APPLY[CONST[
86 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rinv.con']]" mode="pure">
88 <xsl:when test="count(child::*) = 2">
89 <m:apply helm:xref="{@id}">
91 <xsl:apply-templates select="*[2]" mode="noannot"/>
94 <xsl:attribute name="definitionURL">
95 <xsl:value-of select="CONST/@uri"/>
98 <xsl:attribute name="helm:xref">
99 <xsl:value-of select="CONST/@id"/>
111 <!-- Binary Operations and Relations -->
113 <xsl:template match="APPLY[CONST[
114 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rplus.con' or
115 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rminus.con' or
116 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rmult.con' or
117 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rle.con' or
118 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rlt.con' or
119 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rge.con' or
120 attribute::uri='cic:/Coq/Reals/Rdefinitions/Rgt.con' or
121 attribute::uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con' or
122 attribute::uri='cic:/Coq/Reals/Rfunctions/pow.con']]" mode="pure">
124 <xsl:when test="count(child::*) = 3">
125 <xsl:variable name="elem">
127 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'">
128 <xsl:value-of select="'plus'"/>
130 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rminus.con'">
131 <xsl:value-of select="'minus'"/>
133 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rmult.con'">
134 <xsl:value-of select="'times'"/>
136 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rle.con'">
137 <xsl:value-of select="'leq'"/>
139 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rlt.con'">
140 <xsl:value-of select="'lt'"/>
142 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con'">
143 <xsl:value-of select="'geq'"/>
145 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con'">
146 <xsl:value-of select="'gt'"/>
148 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con'">
149 <xsl:value-of select="'min'"/>
151 <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rfunctions/pow.con'">
152 <xsl:value-of select="'power'"/>
156 <m:apply helm:xref="{@id}">
157 <xsl:element name="{concat('m:',$elem)}">
158 <xsl:attribute name="definitionURL">
159 <xsl:value-of select="CONST/@uri"/>
161 <xsl:attribute name="helm:xref">
162 <xsl:value-of select="CONST/@id"/>
165 <xsl:apply-templates select="*[2]" mode="noannot"/>
166 <xsl:apply-templates select="*[3]" mode="noannot"/>
177 <xsl:template match="APPLY[CONST[
178 attribute::uri='cic:/Coq/Reals/Rlimit/limit1_in.con']]" mode="pure">
180 <xsl:when test="count(child::*) = 5">
184 <xsl:when test="name(*[2]) = 'LAMBDA'">
185 <m:apply helm:xref="{@id}">
187 <xsl:attribute name="definitionURL">
188 <xsl:value-of select="CONST/@uri"/>
190 <xsl:attribute name="helm:xref">
191 <xsl:value-of select="CONST/@id"/>
195 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
198 <xsl:apply-templates select="*[5]" mode="noannot"/>
200 <xsl:apply-templates select="*[2]/target" mode="noannot"/>
204 <m:apply helm:xref="{@id}">
210 <xsl:apply-templates select="*[5]" mode="noannot"/>
213 <m:csymbol>app</m:csymbol>
214 <xsl:apply-templates select="*[2]" mode="noannot"/>
220 <xsl:apply-templates select="*[4]" mode="noannot"/>
229 <!-- DIFFERENTIATION -->
231 <xsl:template match="APPLY[CONST[
232 attribute::uri='cic:/Coq/Reals/Rderiv/D_in.con']]" mode="pure">
234 <xsl:when test="count(child::*) = 4">
238 <xsl:when test="name(*[2]) = 'LAMBDA'">
239 <m:apply helm:xref="{@id}">
241 <xsl:attribute name="definitionURL">
242 <xsl:value-of select="CONST/@uri"/>
244 <xsl:attribute name="helm:xref">
245 <xsl:value-of select="CONST/@id"/>
249 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA[1]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
251 <xsl:apply-templates select="*[2]/target" mode="noannot"/>
255 <m:apply helm:xref="{@id}">
261 <m:csymbol>app</m:csymbol>
262 <xsl:apply-templates select="*[2]" mode="noannot"/>
268 <xsl:apply-templates select="*[4]" mode="noannot"/>