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">
13 <!--******************************************************************-->
14 <!-- Variable containing the absolute path of the CIC file -->
15 <!--******************************************************************-->
17 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
19 <!-- ************************* LOGIC *********************************-->
23 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Conjunction/and.ind'] and (count(child::*) = 3)]" mode="pure">
24 <m:apply helm:xref="{@id}">
25 <m:and definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
26 <xsl:apply-templates select="*[2]" mode="noannot"/>
27 <xsl:apply-templates select="*[3]" mode="noannot"/>
33 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Disjunction/or.ind'] and (count(child::*) = 3)]" mode="pure">
34 <m:apply helm:xref="{@id}">
35 <m:or definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
36 <xsl:apply-templates select="*[2]" mode="noannot"/>
37 <xsl:apply-templates select="*[3]" mode="noannot"/>
43 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con'] and (count(child::*) = 2)]" mode="pure">
44 <m:apply helm:xref="{@id}">
45 <m:not definitionURL="{CONST/@uri}" helm:xref="{MUTIND/@id}"/>
46 <xsl:apply-templates select="*[2]" mode="noannot"/>
52 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/Equivalence/iff.ind'] and (count(child::*) = 3)]" mode="pure">
53 <m:apply helm:xref="{@id}">
54 <m:iff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
55 <xsl:apply-templates select="*[2]" mode="noannot"/>
56 <xsl:apply-templates select="*[3]" mode="noannot"/>
63 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind' or attribute::uri='cic:/Coq/Init/Logic_Type/exT.ind'] and (count(child::*) = 3)]" mode="pure">
64 <m:apply helm:xref="{@id}">
65 <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
67 <xsl:when test="name(*[3]) = 'LAMBDA'">
69 <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>
71 <xsl:apply-templates select="LAMBDA/target" mode="noannot"/>
78 <m:csymbol>app</m:csymbol>
79 <xsl:apply-templates select="*[3]" mode="noannot"/>
87 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind' or attribute::uri='cic:/Coq/Init/Logic_Type/exT2.ind'] and (count(child::*) = 4)]" mode="pure">
88 <m:apply helm:xref="{@id}">
89 <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
91 <xsl:when test="name(*[3]) = 'LAMBDA'">
92 <xsl:variable name="bvarname" select="*[3]/target/@binder"/>
94 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="$bvarname"/></xsl:with-param></xsl:call-template></m:ci>
97 <xsl:apply-templates select="LAMBDA[1]/target" mode="noannot"/>
100 <xsl:when test="(name(*[4]) = 'LAMBDA') and
101 ($bvarname = *[4]/target/@binder)">
102 <xsl:apply-templates select="LAMBDA[2]/target" mode="noannot"/>
106 <m:csymbol>app</m:csymbol>
107 <xsl:apply-templates select="*[4]" mode="noannot"/>
108 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="$bvarname"/></xsl:with-param></xsl:call-template></m:ci>
115 <xsl:when test="name(*[4]) = 'LAMBDA'">
116 <xsl:variable name="bvarname" select="*[4]/target/@binder"/>
118 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="$bvarname"/></xsl:with-param></xsl:call-template></m:ci>
122 <m:csymbol>app</m:csymbol>
123 <xsl:apply-templates select="*[3]" mode="noannot"/>
124 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="$bvarname"/></xsl:with-param></xsl:call-template></m:ci>
127 <xsl:apply-templates select="*[4]/target" mode="noannot"/>
135 <m:csymbol>app</m:csymbol>
136 <xsl:apply-templates select="*[3]" mode="noannot"/>
141 <m:csymbol>app</m:csymbol>
142 <xsl:apply-templates select="*[4]" mode="noannot"/>
154 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Equality/eq.ind'] and (count(child::*) = 4)]" mode="pure">
155 <m:apply helm:xref="{@id}">
156 <m:eq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
157 <xsl:apply-templates select="*[3]" mode="noannot"/>
158 <xsl:apply-templates select="*[4]" mode="noannot"/>
163 <!-- TYPE EQUALITY -->
165 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_Type/eqT.ind'] and (count(child::*) = 4)]" mode="pure">
166 <m:apply helm:xref="{@id}">
167 <m:eq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
168 <xsl:apply-templates select="*[3]" mode="noannot"/>
169 <xsl:apply-templates select="*[4]" mode="noannot"/>
174 <!-- NOT and EQ have no parameters -->
175 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
176 and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Equality/eq.ind']]]" mode="pure">
178 <xsl:when test="count(APPLY/child::*) = 4">
179 <m:apply helm:xref="{@id}">
181 <xsl:apply-templates select="*[2]/*[3]" mode="noannot"/>
182 <xsl:apply-templates select="*[2]/*[4]" mode="set"/>
192 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
193 and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_Type/eqT.ind']]]" mode="pure">
195 <xsl:when test="count(APPLY/child::*) = 4">
196 <m:apply helm:xref="{@id}">
198 <xsl:apply-templates select="*[2]/*[3]" mode="noannot"/>
199 <xsl:apply-templates select="*[2]/*[4]" mode="set"/>
208 <!-- ************************ DATATYPES ******************************* -->
210 <!-- no datatypes in MathML content -->
213 <!-- *************************** PEANO ********************************* -->
215 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Peano/le.ind'] and (count(child::*) = 3)]" mode="pure">
216 <m:apply helm:xref="{@id}">
217 <m:leq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
218 <xsl:apply-templates select="*[2]" mode="noannot"/>
219 <xsl:apply-templates select="*[3]" mode="noannot"/>
223 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/lt.con'] and (count(child::*) = 3)]" mode="pure">
224 <m:apply helm:xref="{@id}">
225 <m:lt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
226 <xsl:apply-templates select="*[2]" mode="noannot"/>
227 <xsl:apply-templates select="*[3]" mode="noannot"/>
231 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/ge.con'] and (count(child::*) = 3)]" mode="pure">
232 <m:apply helm:xref="{@id}">
233 <m:geq definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
234 <xsl:apply-templates select="*[2]" mode="noannot"/>
235 <xsl:apply-templates select="*[3]" mode="noannot"/>
239 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/gt.con'] and (count(child::*) = 3)]" mode="pure">
240 <m:apply helm:xref="{@id}">
241 <m:gt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
242 <xsl:apply-templates select="*[2]" mode="noannot"/>
243 <xsl:apply-templates select="*[3]" mode="noannot"/>