]> matita.cs.unibo.it Git - helm.git/blob - helm/style/content.xsl.csc
5f7c1e13137a5c31c43b060bdca2db33a4a12204
[helm.git] / helm / style / content.xsl.csc
1 <?xml version="1.0"?>
2
3 <!--******************************************************************--> 
4 <!-- XSLT version 0.1 of CIC objects to MathML content:               -->
5 <!-- First draft: February 14 2000, Andrea Asperti, Irene Schena      -->
6 <!-- Revised: March 3 2000, Irene Schena                              -->
7 <!-- Revised: March 10 2000, Irene Schena                             -->
8 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena     -->
9 <!--******************************************************************-->
10
11 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
12                               xmlns:m="http://www.w3.org/1998/Math/MathML">
13
14 <xsl:include href="params.xsl"/>
15
16 <!--<xsl:output
17            method="xml" 
18            version="1.0" 
19            encoding="ISO-8859-1" 
20            omit-xml-declaration="no"
21            standalone="no" 
22            doctype-public="http://www.w3.org/TR/REC-MathML" 
23            indent="yes"
24            media-type="text/mathml" /> -->
25
26 <!-- DA FARE: 
27 1)risolvere nella fase di pre-processing le uri relative, settando l'attributo
28 definitionURL dell'oggetto corrispondente (alcuni punteranno a nulla! -quelli 
29 che non hanno il file di definizione corrispondente-); [le uri assolute hanno
30 la forma cic:/.../ in definitionURL e questo schema di uri verra' risolto da
31 Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
32 2)aggiungere nei file xml gli ID, affinche' nello stylesheet si setti
33 l'attributo xref di ogni oggetto per puntare (tramite ID) al suo corrispondente
34 della rappresentazione interna. 
35 -->
36
37 <!--******************************************************************-->
38 <!-- Variable containing the absolute path of the CIC file            -->
39 <!--******************************************************************-->
40
41 <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>
42
43 <!-- CIC TERMS -->
44
45 <xsl:template match="LAMBDA" mode="noannot">
46   <xsl:param name="backpointer" select="''"/>
47     <m:lambda>
48      <m:bvar>
49       <m:ci>
50        [[<xsl:value-of select="$backpointer"/>]]
51        <xsl:value-of select="target/@binder"/>
52       </m:ci>
53       <m:type>
54        <xsl:apply-templates select="source/*[1]" mode="noannot">
55         <xsl:with-param name="backpointer" select="concat($backpointer,'/*[1]/*[1]')"/>
56        </xsl:apply-templates>
57       </m:type>
58      </m:bvar>
59      <xsl:apply-templates select="target/*[1]" mode="noannot">
60       <xsl:with-param name="backpointer" select="concat($backpointer,'/*[2]/*[1]')"/>
61      </xsl:apply-templates>
62     </m:lambda>
63 </xsl:template>
64
65 <xsl:template match="PROD" mode="noannot">
66   <xsl:param name="backpointer" select="''"/>
67     <m:apply>
68      <xsl:choose>
69      <xsl:when test="string(target/@binder)= &quot;&quot;">
70       <m:csymbol>arrow</m:csymbol>
71       <xsl:apply-templates select="source/*[1]" mode="noannot">
72        <xsl:with-param name="backpointer" select="concat($backpointer,'/*[1]/*[1]')"/>
73       </xsl:apply-templates>
74      </xsl:when>
75      <xsl:otherwise>
76       <m:csymbol>prod</m:csymbol>
77        <m:bvar>
78         <m:ci>
79          [[<xsl:value-of select="$backpointer"/>]]
80          <xsl:value-of select="target/@binder"/>
81         </m:ci>
82         <m:type>
83          <xsl:apply-templates select="source/*[1]" mode="noannot">
84           <xsl:with-param name="backpointer" select="concat($backpointer,'/*[1]/*[1]')"/>
85          </xsl:apply-templates>
86         </m:type>
87        </m:bvar>
88      </xsl:otherwise>
89      </xsl:choose>
90      <xsl:apply-templates select="target/*[1]" mode="noannot">
91       <xsl:with-param name="backpointer" select="concat($backpointer,'/*[2]/*[1]')"/>
92      </xsl:apply-templates>
93     </m:apply>
94 </xsl:template>
95
96 <xsl:template match="CAST" mode="noannot">
97   <xsl:param name="backpointer" select="''"/>
98     <m:apply>
99      <m:csymbol>cast</m:csymbol>
100      <xsl:apply-templates mode="noannot" select="*[1]/*[1]">
101       <xsl:with-param name="backpointer" select="concat($backpointer,'/*[1]/*[1]')"/>
102      </xsl:apply-templates>
103      <xsl:apply-templates mode="noannot" select="*[2]/*[1]">
104       <xsl:with-param name="backpointer" select="concat($backpointer,'/*[2]/*[1]')"/>
105      </xsl:apply-templates>
106     </m:apply>
107 </xsl:template>
108
109 <xsl:template match="REL" mode="noannot">
110   <xsl:param name="backpointer" select="''"/>
111     <m:ci>
112      [[<xsl:value-of select="$backpointer"/>]]
113      <xsl:value-of select="@binder"/>
114     </m:ci>
115 </xsl:template>
116
117 <xsl:template match="SORT" mode="noannot">
118   <xsl:param name="backpointer" select="''"/>
119     <m:apply>
120      <m:csymbol>
121       <xsl:value-of select="@value"/>
122      </m:csymbol>
123     </m:apply>
124 </xsl:template>
125
126 <xsl:template match="APPLY" mode="noannot">
127   <xsl:param name="backpointer" select="''"/>
128     <m:apply>
129     <m:csymbol>app</m:csymbol>
130      <xsl:for-each select="*">
131       <xsl:apply-templates mode="noannot" select=".">
132        <xsl:with-param name="backpointer" select="concat($backpointer,'/*[',position(),']')"/>
133       </xsl:apply-templates>
134      </xsl:for-each>
135     </m:apply>
136 </xsl:template>
137
138 <xsl:template match="VAR" mode="noannot">
139   <xsl:param name="backpointer" select="''"/>
140     <m:ci>
141      [[<xsl:value-of select="$backpointer"/>]]
142      <xsl:value-of select="substring-after(@relUri,&quot;,&quot;)"/>
143     </m:ci>
144 </xsl:template>
145
146 <xsl:template match="META" mode="noannot">
147   <xsl:param name="backpointer" select="''"/>
148     <m:ci>
149      [[<xsl:value-of select="$backpointer"/>]]
150      <xsl:value-of select="@no"/>
151     </m:ci>
152 </xsl:template>
153
154 <xsl:template match="CONST" mode="noannot">
155   <xsl:param name="backpointer" select="''"/>
156     <m:ci definitionURL="{@uri}">
157      [[<xsl:value-of select="$backpointer"/>]]
158      <xsl:call-template name="name_of_uri">
159       <xsl:with-param name="uri" select="@uri"/>
160      </xsl:call-template>
161      <!-- <xsl:value-of select="document(concat(string($absPath),@uri))/*/@name"/> -->
162     </m:ci>
163 </xsl:template>
164
165 <xsl:template match="MUTIND" mode="noannot">
166   <xsl:param name="backpointer" select="''"/>
167     <m:ci definitionURL="{@uri}">
168      <xsl:variable name="index"><xsl:value-of select="@noType"/></xsl:variable>
169      [[<xsl:value-of select="$backpointer"/>]]
170      <xsl:value-of select="document(concat(string($absPath),@uri))/InductiveDefinition/InductiveType[position()=number($index)+1]/@name"/>
171     </m:ci>
172 </xsl:template>
173
174 <xsl:template match="MUTCONSTRUCT" mode="noannot">
175   <xsl:param name="backpointer" select="''"/>
176     <m:ci definitionURL="{@uri}">
177      <xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
178      <xsl:variable name="Cindex"><xsl:value-of select="@noConstr"/></xsl:variable>
179      [[<xsl:value-of select="$backpointer"/>]]
180      <xsl:value-of select="document(concat(string($absPath),@uri))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($Cindex)]/@name"/>
181     </m:ci>
182 </xsl:template>
183
184 <xsl:template match="MUTCASE" mode="noannot">
185   <xsl:param name="backpointer" select="''"/>
186     <xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
187     <xsl:variable name="Turi"><xsl:value-of select="@uriType"/></xsl:variable>
188     <m:apply>
189      <m:csymbol>mutcase</m:csymbol>
190      <xsl:apply-templates select="patternsType/*[1]" mode="noannot">
191        <xsl:with-param name="backpointer" select="concat($backpointer,'/*[1]/*[1]')"/>
192      </xsl:apply-templates>
193      <xsl:apply-templates select="inductiveTerm/*[1]" mode="noannot">
194        <xsl:with-param name="backpointer" select="concat($backpointer,'/*[2]/*[1]')"/>
195      </xsl:apply-templates>
196      <xsl:variable name="nop"><xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/@noParams"/></xsl:variable>
197      <xsl:for-each select="pattern">
198       <xsl:variable name="pos" select="position()"/>
199       <xsl:variable name="nopar"><xsl:apply-templates select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/*[1]" mode="counting"><xsl:with-param name="noparams" select="$nop"/></xsl:apply-templates></xsl:variable>
200       <xsl:choose>
201       <xsl:when test="$nopar = 0">
202        <m:ci>
203         <xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/>
204        </m:ci>
205       </xsl:when>
206       <xsl:otherwise>
207        <m:apply>
208         <m:csymbol>app</m:csymbol>
209         <m:ci>
210          <xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/>
211         </m:ci>
212         <xsl:apply-templates select="./*[1]" mode="abstparams"><xsl:with-param name="noparams" select="$nopar"/><xsl:with-param name="binder">LAMBDA</xsl:with-param></xsl:apply-templates>
213         </m:apply>
214        </xsl:otherwise>
215        </xsl:choose>
216       <xsl:apply-templates select="./*[1]" mode="abstparams"><xsl:with-param name="noparams" select="$nopar"/><xsl:with-param name="target" select="1"/><xsl:with-param name="binder">LAMBDA</xsl:with-param></xsl:apply-templates>
217      </xsl:for-each> 
218     </m:apply>
219 </xsl:template>
220
221 <xsl:template match="FIX" mode="noannot">
222   <xsl:param name="backpointer" select="''"/>
223     <m:apply>
224      <xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
225      <m:csymbol>fix</m:csymbol>
226      <m:ci><xsl:value-of select="FixFunction[position()=number($findex)+1]/@name"/></m:ci>
227      <xsl:apply-templates mode="noannot" select="*"/>
228     </m:apply>
229 </xsl:template>
230
231 <xsl:template match="COFIX" mode="noannot">
232    <m:apply>
233      <xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
234      <m:csymbol>cofix</m:csymbol>
235      <m:ci><xsl:value-of select="CofixFunction[position()=number($findex)+1]/@name"/></m:ci>
236      <xsl:apply-templates mode="noannot" select="*"/>
237     </m:apply>
238 </xsl:template>
239
240 <!-- ELEMENTS OF CIC TERMS -->
241
242 <xsl:template match="FixFunction" mode="noannot">
243     <m:bvar>
244      <m:ci><xsl:value-of select="@name"/></m:ci>
245      <m:type><xsl:apply-templates select="type/*[1]" mode="noannot"/></m:type>
246     </m:bvar> 
247     <xsl:apply-templates select="body/*[1]" mode="noannot"/>
248 </xsl:template>
249
250 <xsl:template match="CofixFunction" mode="noannot">
251     <m:bvar>
252      <m:ci><xsl:value-of select="@name"/></m:ci>
253      <m:type><xsl:apply-templates select="type/*[1]" mode="noannot"/></m:type>
254     </m:bvar> 
255     <xsl:apply-templates select="body/*[1]" mode="noannot"/>
256 </xsl:template>
257
258 </xsl:stylesheet>