]> matita.cs.unibo.it Git - helm.git/blob - style/basic.xsl
made executable again
[helm.git] / style / basic.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 <!-- Basic Logic                                                      -->
29 <!-- First draft: April 3 2000                                        -->
30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi          -->
31 <!--******************************************************************-->
32
33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
34                               xmlns:m="http://www.w3.org/1998/Math/MathML"
35                               xmlns:helm="http://www.cs.unibo.it/helm">
36
37
38 <!-- ************************* LOGIC *********************************-->
39
40 <!-- AND -->
41
42 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Conjunction/and.ind'] and (count(child::*) = 3)]" mode="pure">
43     <m:apply helm:xref="{@id}">
44     <m:and definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
45      <xsl:apply-templates select="*[2]" mode="noannot"/>
46      <xsl:apply-templates select="*[3]" mode="noannot"/>
47     </m:apply>
48 </xsl:template>
49
50 <!-- OR -->
51
52 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Disjunction/or.ind'] and (count(child::*) = 3)]" mode="pure">
53     <m:apply helm:xref="{@id}">
54     <m:or definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
55      <xsl:apply-templates select="*[2]" mode="noannot"/>
56      <xsl:apply-templates select="*[3]" mode="noannot"/>
57     </m:apply>
58 </xsl:template>
59
60 <!-- NOT -->
61
62 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con'] and (count(child::*) = 2)]" mode="pure">
63     <m:apply helm:xref="{@id}">
64     <m:not definitionURL="{CONST/@uri}" helm:xref="{MUTIND/@id}"/>
65      <xsl:apply-templates select="*[2]" mode="noannot"/>
66     </m:apply>
67 </xsl:template>
68
69 <!-- IFF -->
70 <!-- 
71 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/Equivalence/iff.ind'] and (count(child::*) = 3)]" mode="pure">
72     <m:apply helm:xref="{@id}">
73     <m:iff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
74      <xsl:apply-templates select="*[2]" mode="noannot"/>
75      <xsl:apply-templates select="*[3]" mode="noannot"/>
76     </m:apply>
77 </xsl:template>
78 -->
79
80 <!-- EXISTS -->
81
82 <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">
83     <m:apply helm:xref="{@id}">
84      <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
85      <xsl:choose>
86       <xsl:when test="name(*[3]) = 'LAMBDA'">
87        <m:bvar>
88         <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
89        </m:bvar>
90        <m:condition>
91         <xsl:apply-templates select="*[2]" mode="pure"/>
92        </m:condition>
93        <xsl:apply-templates select="LAMBDA/target" mode="noannot"/>
94       </xsl:when>
95       <xsl:otherwise>
96        <m:bvar>
97         <m:ci>$x</m:ci>
98        </m:bvar>
99        <m:condition>
100         <xsl:apply-templates select="*[2]" mode="pure"/>
101        </m:condition>
102        <m:apply>
103         <m:csymbol>app</m:csymbol>
104         <xsl:apply-templates select="*[3]" mode="noannot"/>
105         <m:ci>$x</m:ci>
106        </m:apply>
107       </xsl:otherwise>
108      </xsl:choose>
109     </m:apply>
110 </xsl:template>
111
112 <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">
113     <m:apply helm:xref="{@id}">
114     <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
115      <xsl:choose>
116       <xsl:when test="name(*[3]) = 'LAMBDA'">
117        <xsl:variable name="bvarname" select="*[3]/target/@binder"/>
118        <m:bvar>
119         <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>
120        </m:bvar>
121        <m:condition>
122         <xsl:apply-templates select="LAMBDA[1]/target" mode="noannot"/>
123        </m:condition>
124        <xsl:choose>
125         <xsl:when test="(name(*[4]) = 'LAMBDA') and 
126            ($bvarname = *[4]/target/@binder)">
127          <xsl:apply-templates select="LAMBDA[2]/target" mode="noannot"/>
128         </xsl:when>
129         <xsl:otherwise>
130          <m:apply>
131           <m:csymbol>app</m:csymbol>
132           <xsl:apply-templates select="*[4]" mode="noannot"/>
133           <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>
134          </m:apply>
135         </xsl:otherwise>
136        </xsl:choose>
137       </xsl:when>
138       <xsl:otherwise>
139        <xsl:choose>
140         <xsl:when test="name(*[4]) = 'LAMBDA'">
141          <xsl:variable name="bvarname" select="*[4]/target/@binder"/>
142          <m:bvar>
143           <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>
144          </m:bvar>
145          <m:condition>
146           <m:apply>
147            <m:csymbol>app</m:csymbol>
148            <xsl:apply-templates select="*[3]" mode="noannot"/>
149            <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>
150           </m:apply>
151          </m:condition>
152          <xsl:apply-templates select="*[4]/target" mode="noannot"/>
153         </xsl:when>
154         <xsl:otherwise>
155          <m:bvar>
156           <m:ci>x</m:ci>
157          </m:bvar>
158          <m:condition>
159           <m:apply>
160            <m:csymbol>app</m:csymbol>
161            <xsl:apply-templates select="*[3]" mode="noannot"/>
162            <m:ci>x</m:ci>
163           </m:apply>
164          </m:condition>
165          <m:apply>
166           <m:csymbol>app</m:csymbol>
167           <xsl:apply-templates select="*[4]" mode="noannot"/>
168           <m:ci>x</m:ci>
169          </m:apply>
170         </xsl:otherwise>
171        </xsl:choose>
172       </xsl:otherwise>
173      </xsl:choose>
174     </m:apply>
175 </xsl:template>
176
177 <!-- EQUALITY and TYPE EQUALITY -->
178
179 <xsl:template match="APPLY[MUTIND/@uri='cic:/Coq/Init/Logic/Equality/eq.ind']" mode="pure">
180    <xsl:call-template name="mk-mml-op-noannot">
181       <xsl:with-param name="hide" select="1"/>
182       <xsl:with-param name="c-tag" select="MUTIND"/>
183       <xsl:with-param name="m-tag" select="'eq'"/>
184    </xsl:call-template>
185 </xsl:template>
186
187 <xsl:template match="APPLY[MUTIND/@uri='cic:/Coq/Init/Logic_Type/eqT.ind']" mode="pure">
188    <xsl:call-template name="mk-mml-op-noannot">
189       <xsl:with-param name="hide" select="1"/>
190       <xsl:with-param name="c-tag" select="MUTIND"/>
191       <xsl:with-param name="m-tag" select="'eq'"/>
192    </xsl:call-template>
193 </xsl:template>
194
195 <!-- NOT-EQ -->
196 <!-- NOT and EQ have no parameters -->
197 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
198 and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Equality/eq.ind']]]" mode="pure">
199     <xsl:choose>
200      <xsl:when test="count(APPLY/child::*) = 4">
201       <m:apply helm:xref="{@id}">
202        <m:neq/>
203        <xsl:apply-templates select="*[2]/*[3]" mode="noannot"/>
204        <xsl:apply-templates select="*[2]/*[4]" mode="set"/>  
205       </m:apply>
206      </xsl:when>
207      <xsl:otherwise>
208       <xsl:apply-imports/>
209      </xsl:otherwise>
210     </xsl:choose>
211 </xsl:template>
212
213 <!-- NOT-EQT -->
214 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
215 and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_Type/eqT.ind']]]" mode="pure">
216     <xsl:choose>
217      <xsl:when test="count(APPLY/child::*) = 4">
218       <m:apply helm:xref="{@id}">
219        <m:neq/>
220        <xsl:apply-templates select="*[2]/*[3]" mode="noannot"/>
221        <xsl:apply-templates select="*[2]/*[4]" mode="set"/>  
222       </m:apply>
223      </xsl:when>
224      <xsl:otherwise>
225       <xsl:apply-imports/>
226      </xsl:otherwise>
227     </xsl:choose>
228 </xsl:template>
229
230 <!-- ************************ DATATYPES ******************************* -->
231
232 <!-- no datatypes in MathML content -->
233
234 <!-- ************************** PEANO ********************************* -->
235
236 <!-- see arith.xsl --> <!-- FG -->
237
238 </xsl:stylesheet>