]> matita.cs.unibo.it Git - helm.git/blob - helm/style/content.xsl
added LICENSE
[helm.git] / helm / style / content.xsl
1 <?xml version="1.0"?>
2
3 <!-- Copyright (C) 2000, HELM Team                                     -->
4 <!--                                                                   -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
6 <!-- Library of Mathematics, developed at the Computer Science         -->
7 <!-- Department, University of Bologna, Italy.                         -->
8 <!--                                                                   -->
9 <!-- HELM is free software; you can redistribute it and/or             -->
10 <!-- modify it under the terms of the GNU General Public License       -->
11 <!-- as published by the Free Software Foundation; either version 2    -->
12 <!-- of the License, or (at your option) any later version.            -->
13 <!--                                                                   -->
14 <!-- HELM is distributed in the hope that it will be useful,           -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
17 <!-- GNU General Public License for more details.                      -->
18 <!--                                                                   -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software               -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
22 <!-- MA  02111-1307, USA.                                              -->
23 <!--                                                                   -->
24 <!-- For details, see the HELM World-Wide-Web page,                    -->
25 <!-- http://cs.unibo.it/helm/.                                         -->
26
27 <!--******************************************************************--> 
28 <!-- XSLT version 0.1 of CIC objects to MathML content:               -->
29 <!-- First draft: February 14 2000, Andrea Asperti, Irene Schena      -->
30 <!-- Revised: March 3 2000, Irene Schena                              -->
31 <!-- Revised: March 10 2000, Irene Schena                             -->
32 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena     -->
33 <!--******************************************************************-->
34
35 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
36                               xmlns:m="http://www.w3.org/1998/Math/MathML"
37                               xmlns:helm="http://www.cs.unibo.it/helm">
38
39 <xsl:include href="params.xsl"/>
40
41 <!--<xsl:output
42            method="xml" 
43            version="1.0" 
44            encoding="ISO-8859-1" 
45            omit-xml-declaration="no"
46            standalone="no" 
47            doctype-public="http://www.w3.org/TR/REC-MathML" 
48            indent="yes"
49            media-type="text/mathml" /> -->
50
51 <!-- DA FARE: 
52 1)risolvere nella fase di pre-processing le uri relative delle var, settando 
53 l'attributo
54 definitionURL dell'oggetto corrispondente (alcuni punteranno a nulla! -quelli 
55 che non hanno il file di definizione corrispondente-); [le uri assolute hanno
56 la forma cic:/.../ in definitionURL e questo schema di uri verra' risolto da
57 Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
58 -->
59
60 <!--******************************************************************-->
61 <!-- Variable containing the absolute path of the CIC file            -->
62 <!--******************************************************************-->
63
64 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
65
66 <!-- CIC TERMS -->
67
68 <xsl:template match="LAMBDA" mode="pure">
69     <m:lambda helm:xref="{@id}">
70      <m:bvar>
71       <m:ci>
72        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
73       </m:ci>
74       <m:type>
75        <xsl:apply-templates select="source/*[1]" mode="noannot"/>
76       </m:type>
77      </m:bvar>
78      <xsl:apply-templates select="target/*[1]" mode="noannot"/>
79     </m:lambda>
80 </xsl:template>
81
82 <xsl:template match="PROD" mode="pure">
83     <m:apply helm:xref="{@id}">
84      <xsl:choose>
85      <xsl:when test="string(target/@binder)= &quot;&quot;">
86       <m:csymbol>arrow</m:csymbol>
87       <xsl:apply-templates select="source/*[1]" mode="noannot"/>
88      </xsl:when>
89      <xsl:otherwise>
90       <xsl:choose>
91        <xsl:when test="@type = 'Prop'">
92         <m:csymbol>forall</m:csymbol>
93        </xsl:when>
94        <xsl:otherwise>
95         <m:csymbol>prod</m:csymbol>
96        </xsl:otherwise>
97       </xsl:choose>
98        <m:bvar>
99         <m:ci>
100          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
101         </m:ci>
102         <m:type>
103          <xsl:apply-templates select="source/*[1]" mode="noannot"/>
104         </m:type>
105        </m:bvar>
106      </xsl:otherwise>
107      </xsl:choose>
108      <xsl:apply-templates select="target/*[1]" mode="noannot"/>
109     </m:apply>
110 </xsl:template>
111
112 <xsl:template match="CAST" mode="pure">
113     <m:apply helm:xref="{@id}">
114      <m:csymbol>cast</m:csymbol>
115      <xsl:apply-templates mode="noannot" select="*/*"/>
116     </m:apply>
117 </xsl:template>
118
119 <xsl:template match="REL" mode="pure">
120     <m:ci helm:xref="{@id}">
121      <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
122     </m:ci>
123 </xsl:template>
124
125 <xsl:template match="SORT" mode="pure">
126     <m:apply helm:xref="{@id}">
127      <m:csymbol>
128       <xsl:value-of select="@value"/>
129      </m:csymbol>
130     </m:apply>
131 </xsl:template>
132
133 <xsl:template match="APPLY" mode="pure">
134    <xsl:choose>
135     <!-- <xsl:when test="//InnerTypes and boolean(key('typeid',*/@id))"> -->
136     <!-- start looking for subproofs -->
137     <!-- <xsl:when test="((*/@id) = (//InnerTypes/TYPE/@of))"> -->
138     <xsl:when test="//InnerTypes and count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) > 0">
139      <m:apply helm:xref="{@id}">
140       <m:csymbol>letin</m:csymbol>
141       <!-- <xsl:for-each select="*[boolean(key('typeid',@id))]"> -->
142       <!-- first process all subproofs (let-in) -->
143       <xsl:for-each select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]">
144        <m:apply>
145         <m:csymbol>let</m:csymbol>
146         <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position())"/></xsl:with-param></xsl:call-template></m:ci>
147         <xsl:apply-templates mode="noannot" select="."/>
148        </m:apply>
149       </xsl:for-each>
150       <!-- now re-process the application in mode appflat -->
151       <xsl:apply-templates mode="appflat" select="."/> 
152      </m:apply>
153     </xsl:when>
154     <xsl:otherwise>
155      <xsl:apply-templates mode="appflat" select="."/>
156     </xsl:otherwise>
157    </xsl:choose>
158 </xsl:template>
159
160 <xsl:template match="APPLY" mode="appflat">
161       <m:apply helm:xref="{@id}">
162        <m:csymbol>app</m:csymbol>
163        <!-- mode flat looks for siblings: call with the first child -->
164        <xsl:apply-templates mode="flat" select="*[1]"/>
165       </m:apply>
166 </xsl:template>
167
168 <xsl:template match="*" mode="flat">
169  <xsl:param name="n" select="1"/>
170  <xsl:variable name="id" select="@id"/>
171  <xsl:choose>
172   <!-- <xsl:when test="key('typeid',@id)"> -->
173   <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
174   <xsl:when test="//InnerTypes and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
175    <m:ci>
176     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
177    </m:ci>
178    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
179     <xsl:with-param name="n" select="$n+1"/>
180    </xsl:apply-templates>
181   </xsl:when>
182   <xsl:otherwise>
183    <xsl:apply-templates mode="pure" select="."/>
184    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
185     <xsl:with-param name="n" select="$n"/>
186    </xsl:apply-templates>
187   </xsl:otherwise>
188  </xsl:choose>
189 </xsl:template>
190
191 <xsl:template match="VAR" mode="pure">
192     <m:ci helm:xref="{@id}">
193      <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="substring-after(@relUri,&quot;,&quot;)"/></xsl:with-param></xsl:call-template>
194     </m:ci>
195 </xsl:template>
196
197 <xsl:template match="META" mode="pure">
198     <m:ci helm:xref="{@id}">
199      <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@no"/></xsl:with-param></xsl:call-template>
200     </m:ci>
201 </xsl:template>
202
203 <xsl:template match="CONST" mode="pure">
204     <m:ci definitionURL="{@uri}" helm:xref="{@id}">
205      <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri">
206       <xsl:with-param name="uri" select="@uri"/>
207      </xsl:call-template></xsl:with-param></xsl:call-template>
208      <!-- <xsl:value-of select="document(concat(string($absPath),@uri))/*/@name"/> -->
209     </m:ci>
210 </xsl:template>
211
212 <xsl:template match="MUTIND" mode="pure">
213     <m:ci definitionURL="{@uri}" helm:xref="{@id}">
214      <xsl:variable name="index"><xsl:value-of select="@noType"/></xsl:variable>
215      <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),@uri))/InductiveDefinition/InductiveType[position()=number($index)+1]/@name"/></xsl:with-param></xsl:call-template>
216     </m:ci>
217 </xsl:template>
218
219 <xsl:template match="MUTCONSTRUCT" mode="pure">
220     <m:ci definitionURL="{@uri}" helm:xref="{@id}">
221      <xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
222      <xsl:variable name="Cindex"><xsl:value-of select="@noConstr"/></xsl:variable>
223      <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),@uri))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($Cindex)]/@name"/></xsl:with-param></xsl:call-template>
224     </m:ci>
225 </xsl:template>
226
227 <xsl:template match="MUTCASE" mode="pure">
228     <xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
229     <xsl:variable name="Turi"><xsl:value-of select="@uriType"/></xsl:variable>
230     <m:apply helm:xref="{@id}">
231      <m:csymbol>mutcase</m:csymbol>
232      <xsl:apply-templates select="patternsType/*[1]" mode="noannot"/>
233      <xsl:apply-templates select="inductiveTerm/*[1]" mode="noannot"/>
234      <xsl:variable name="nop"><xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/@noParams"/></xsl:variable>
235      <xsl:for-each select="pattern">
236       <xsl:variable name="pos" select="position()"/>
237       <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>
238       <xsl:choose>
239       <xsl:when test="$nopar = 0">
240        <m:ci>
241         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/></xsl:with-param></xsl:call-template>
242        </m:ci>
243       </xsl:when>
244       <xsl:otherwise>
245        <m:apply>
246         <m:csymbol>app</m:csymbol>
247         <m:ci>
248          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/></xsl:with-param></xsl:call-template>
249         </m:ci>
250         <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>
251         </m:apply>
252        </xsl:otherwise>
253        </xsl:choose>
254       <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>
255      </xsl:for-each> 
256     </m:apply>
257 </xsl:template>
258
259 <xsl:template match="FIX" mode="pure">
260     <m:apply helm:xref="{@id}">
261      <xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
262      <m:csymbol>fix</m:csymbol>
263      <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="FixFunction[position()=number($findex)+1]/@name"/></xsl:with-param></xsl:call-template></m:ci>
264      <xsl:apply-templates mode="pure" select="*"/>
265     </m:apply>
266 </xsl:template>
267
268 <xsl:template match="COFIX" mode="pure">
269    <m:apply helm:xref="{@id}">
270      <xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
271      <m:csymbol>cofix</m:csymbol>
272      <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="CofixFunction[position()=number($findex)+1]/@name"/></xsl:with-param></xsl:call-template></m:ci>
273      <xsl:apply-templates mode="pure" select="*"/>
274     </m:apply>
275 </xsl:template>
276
277 <!-- ELEMENTS OF CIC TERMS -->
278
279 <xsl:template match="FixFunction" mode="pure">
280     <m:bvar>
281      <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@name"/></xsl:with-param></xsl:call-template></m:ci>
282      <m:type><xsl:apply-templates select="type/*[1]" mode="noannot"/></m:type>
283     </m:bvar> 
284     <xsl:apply-templates select="body/*[1]" mode="noannot"/>
285 </xsl:template>
286
287 <xsl:template match="CofixFunction" mode="pure">
288     <m:bvar>
289      <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@name"/></xsl:with-param></xsl:call-template></m:ci>
290      <m:type><xsl:apply-templates select="type/*[1]" mode="noannot"/></m:type>
291     </m:bvar> 
292     <xsl:apply-templates select="body/*[1]" mode="noannot"/>
293 </xsl:template>
294
295 </xsl:stylesheet>
296
297
298
299
300