3 <!-- Copyright (C) 2000, HELM Team -->
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. -->
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. -->
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. -->
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. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <!--******************************************************************-->
29 <!-- (completely) Revisited: february 2001, Andrea Asperti -->
30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
31 <!--******************************************************************-->
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">
37 <!-- ************************* LOGIC *********************************-->
39 <!-- Proof objects -->
41 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
43 <!-- ALL this elements does not have inner type -->
44 <xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
45 <xsl:apply-templates select="." mode="pure"/>
48 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
50 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
51 <xsl:template match="LAMBDA" mode="noannot">
52 <xsl:variable name="id" select="@id"/>
54 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and name(../..) != 'LAMBDA'">
55 <m:apply helm:xref="{@id}">
56 <m:csymbol>proof</m:csymbol>
57 <xsl:apply-templates mode="proof_transform" select="."/>
58 <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
62 <xsl:apply-templates select="." mode="pure"/>
67 <!-- ALL these elements have inner type -->
68 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
69 <xsl:variable name="id" select="@id"/>
71 <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
72 <m:apply helm:xref="{@id}">
73 <m:csymbol>proof</m:csymbol>
74 <xsl:apply-templates mode="proof_transform" select="."/>
75 <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
80 <xsl:when test="name()='APPLY'">
81 <xsl:apply-templates select="." mode="letin"/>
84 <xsl:apply-templates select="." mode="pure"/>
91 <xsl:template mode="proof_transform" match="*">
92 <xsl:variable name="id" select="@id"/>
94 <!-- NATIND 3 parametri -->
95 <xsl:when test="name()='APPLY' and CONST[
96 attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 4">
98 <m:csymbol>nat_ind</m:csymbol>
99 <xsl:apply-templates mode="noannot" select="*[3]"/>
100 <xsl:apply-templates mode="noannot" select="*[4]"/>
103 <!-- NATIND 4 parametri -->
104 <xsl:when test="name()='APPLY' and CONST[
105 attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 5">
107 <m:csymbol>nat_ind</m:csymbol>
108 <xsl:apply-templates mode="noannot" select="*[3]"/>
109 <xsl:apply-templates mode="noannot" select="*[4]"/>
113 <xsl:when test="name()= 'APPLY' and CONST[
114 attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
115 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
116 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
118 <m:csymbol>rw_step</m:csymbol>
119 <xsl:apply-templates mode="noannot" select="*[5]"/>
120 <xsl:apply-templates mode="pure" select="*[3]"/>
121 <xsl:apply-templates mode="pure" select="*[6]"/>
122 <xsl:apply-templates mode="pure" select="*[7]"/>
125 <!-- EQUALITY with extra-parameters -->
126 <xsl:when test="name()= 'APPLY' and CONST[
127 attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
128 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
129 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
130 <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
132 <xsl:when test="$no_extraproofs=0">
134 <m:csymbol>rewrite_and_apply</m:csymbol>
136 <m:csymbol>rw_step</m:csymbol>
137 <xsl:apply-templates mode="noannot" select="*[5]"/>
138 <xsl:apply-templates mode="pure" select="*[3]"/>
139 <xsl:apply-templates mode="pure" select="*[6]"/>
140 <xsl:apply-templates mode="pure" select="*[7]"/>
142 <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
147 <xsl:when test="*[5]/@sort='Prop'">
148 <m:apply helm:xref="{@id}">
149 <m:csymbol>letin</m:csymbol>
151 <m:csymbol>let</m:csymbol>
153 <xsl:call-template name="insert_subscript">
154 <xsl:with-param name="node_value" select="'h1'"/>
157 <xsl:apply-templates mode="noannot" select="*[5]"/>
159 <xsl:call-template name="gen_let">
160 <xsl:with-param name="init_pos" select="1"/>
161 <xsl:with-param name="from" select="7"/>
164 <m:csymbol>rewrite_and_apply</m:csymbol>
166 <m:csymbol>rw_step</m:csymbol>
168 <xsl:call-template name="insert_subscript">
169 <xsl:with-param name="node_value" select="'h1'"/>
172 <xsl:apply-templates mode="pure" select="*[3]"/>
173 <xsl:apply-templates mode="pure" select="*[6]"/>
174 <xsl:apply-templates mode="pure" select="*[7]"/>
176 <xsl:apply-templates mode="flat" select="*[8]">
177 <xsl:with-param name="n">
178 <xsl:value-of select="2"/>
180 </xsl:apply-templates>
185 <m:apply helm:xref="{@id}">
186 <m:csymbol>letin</m:csymbol>
187 <xsl:call-template name="gen_let">
188 <xsl:with-param name="init_pos" select="0"/>
189 <xsl:with-param name="form" select="7"/>
192 <m:csymbol>rewrite_and_apply</m:csymbol>
194 <m:csymbol>rw_step</m:csymbol>
195 <xsl:apply-templates mode="pure" select="*[5]"/>
196 <xsl:apply-templates mode="pure" select="*[3]"/>
197 <xsl:apply-templates mode="pure" select="*[6]"/>
198 <xsl:apply-templates mode="pure" select="*[7]"/>
200 <xsl:apply-templates mode="flat" select="*[8]">
201 <xsl:with-param name="n">
202 <xsl:value-of select="1"/>
204 </xsl:apply-templates>
212 <!-- gestire meglio il caso di and_ind quando la prova
213 non e' della forma \x.\y.M -->
214 <xsl:when test="name()= 'APPLY' and CONST[
215 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
216 and count(child::*) = 6
217 and name(*[5])='LAMBDA'
218 and name(*[5]/target/*[1])='LAMBDA'">
219 <m:apply helm:xref="{@id}">
220 <m:csymbol>and_ind</m:csymbol>
221 <xsl:apply-templates mode="noannot" select="*[6]"/>
222 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
223 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
224 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
225 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
226 <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
229 <xsl:when test="name()= 'APPLY' and CONST[
230 attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
231 and count(child::*) = 7">
232 <m:apply helm:xref="{@id}">
233 <m:csymbol>or_ind</m:csymbol>
234 <xsl:apply-templates mode="noannot" select="*[7]"/>
235 <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
236 <xsl:apply-templates mode="pure" select="*[5]"/>
237 <xsl:apply-templates mode="pure" select="*[6]"/>
240 <!-- ex_ind, exT_ind -->
241 <xsl:when test="name()= 'APPLY'
242 and (CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
243 CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
244 and count(child::*) = 6
245 and name(*[5])='LAMBDA'
246 and name(*[5]/target/*[1])='LAMBDA'">
247 <m:apply helm:xref="{@id}">
248 <m:csymbol>ex_ind</m:csymbol>
249 <xsl:apply-templates mode="noannot" select="*[6]"/>
250 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
251 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
252 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
253 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
254 <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
259 <xsl:when test="name()='APPLY'">
260 <xsl:apply-templates select="." mode="letin"/>
263 <xsl:apply-templates select="." mode="pure"/>
271 <xsl:template match="APPLY" mode="letin">
272 <xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
273 <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
275 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
276 <m:apply helm:xref="{@id}">
277 <m:csymbol>letin1</m:csymbol>
278 <xsl:apply-templates mode="noannot" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
279 <!-- now re-process the application -->
280 <m:apply helm:xref="{@id}">
281 <m:csymbol>app</m:csymbol>
282 <!-- mode previous looks for siblings:
283 call with the first child -->
284 <xsl:apply-templates mode="previous" select="*[1]"/>
288 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
289 <m:apply helm:xref="{@id}">
290 <m:csymbol>letin</m:csymbol>
291 <!-- first process all subproofs (let-in) -->
292 <xsl:call-template name="gen_let"/>
293 <!-- now re-process the application -->
294 <m:apply helm:xref="{@id}">
295 <m:csymbol>app</m:csymbol>
296 <!-- mode flat looks for siblings: call with the first child -->
297 <xsl:apply-templates mode="flat" select="*[1]"/>
302 <xsl:apply-templates mode="pure" select="."/>
307 <xsl:template name="gen_let">
308 <xsl:param name="init_pos" select="0"/>
309 <xsl:param name="from" select="0"/>
310 <xsl:for-each select="*[position()>$from and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]">
312 <m:csymbol>let</m:csymbol>
313 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position()+$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
314 <xsl:apply-templates mode="noannot" select="."/>
319 <xsl:template match="*" mode="previous">
321 <xsl:when test="$naturalLanguage='yes' and(@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX'))">
322 <m:ci>previous</m:ci>
325 <xsl:apply-templates select="." mode="pure"/>
328 <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
331 <xsl:template match="*" mode="flat">
332 <xsl:param name="n" select="1"/>
333 <xsl:variable name="id" select="@id"/>
335 <!-- <xsl:when test="key('typeid',@id)"> -->
336 <!-- <xsl:when test="$InnerTypes/InnerTypes/TYPE[@of=$id]"> -->
337 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
339 <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>
341 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
342 <xsl:with-param name="n" select="$n+1"/>
343 </xsl:apply-templates>
346 <xsl:apply-templates mode="pure" select="."/>
347 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
348 <xsl:with-param name="n" select="$n"/>
349 </xsl:apply-templates>
355 <!-- <xsl:template match="APPLY[CONST[
356 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
358 <xsl:when test="count(child::*) > 4">
359 <m:apply helm:xref="{@id}">
360 <m:csymbol>app</m:csymbol>
361 <xsl:apply-templates mode="pure" select="*[1]"/>
365 <xsl:apply-templates mode="flat" select="*[5]"/>
369 <m:apply helm:xref="{@id}">
370 <m:csymbol>app</m:csymbol>
371 <xsl:apply-templates mode="flat" select="*[1]"/>