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 <!--******************************************************************-->
28 <!-- XSLT version 0.1 of CIC inductive objects to MathML content: -->
29 <!-- First draft: March 2001, Andrea asperti -->
30 <!--******************************************************************-->
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">
38 <xsl:template mode="inductive" match="APPLY">
39 <xsl:param name="inductive_def_uri" select="/.."/>
40 <xsl:param name="inductive_def_index" select="1"/>
41 <xsl:param name="inductive_def_name" select="''"/>
42 <xsl:param name="section_params" select="0"/>
43 <!-- expected_args_type contains the types of the arguments expected by
44 the induction principle -->
45 <xsl:variable name="expected_args_types"
46 select="document(concat(string($absPath),*[1]/@uri))/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
47 <xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
48 <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
49 <!-- First check that the induction principle is applied to the
50 expected number of arguments -->
52 <xsl:when test="$no_expected_args = count($actual_arguments)">
53 <!-- Now check that each actual argument starts with the
54 expected number of lambda abstractions -->
55 <xsl:variable name="argsOK">
56 <xsl:call-template name="check_args">
57 <xsl:with-param name="arg_types" select="$expected_args_types"/>
58 <xsl:with-param name="actual_args" select="$actual_arguments"/>
62 <!-- il semplice test $argsOK non funziona -->
63 <xsl:when test="string($argsOK) = 'true'">
64 <!-- arguments are in the expected form: we create a
65 "by_induction" content element -->
66 <!-- inductive_def contains the inductive definition -->
67 <xsl:variable name="inductive_def"
68 select="document(concat(string($absPath),$inductive_def_uri))/InductiveDefinition"/>
69 <!-- no_params is the number of paramters in square brackets -->
70 <xsl:variable name="no_params"
71 select="$inductive_def/@noParams"/>
72 <!-- the inductive property is the first argument following
74 <xsl:variable name="inductive_property"
75 select="$actual_arguments[1 + $no_params]"/>
76 <xsl:variable name="tail_args"
77 select="$actual_arguments[position()> (1 + $no_params)]"/>
78 <!-- inductive_type contains the right inductive type in the
79 mutual inductive definition -->
80 <xsl:variable name="inductive_type"
81 select="$inductive_def/InductiveType[position()=$inductive_def_index]"/>
82 <xsl:variable name="no_constructors"
83 select="count($inductive_type/Constructor)"/>
84 <!-- each case has a single argument -->
85 <xsl:variable name="args_for_cases"
86 select="$tail_args[($no_constructors + 1) > position()]"/>
87 <!-- extra_args contains the remaining arguments; the LAST one
88 of them is the argument we are inductively arguing on -->
89 <xsl:variable name="extra_args"
90 select="$tail_args[position()> $no_constructors]"/>
92 <m:csymbol>by_induction</m:csymbol>
93 <!-- the first (i.e. second) argument of by_induction
94 is the uri of the inductive definition -->
95 <m:ci><xsl:value-of select="$inductive_def_uri"/></m:ci>
96 <!-- next, we have the inductive property, currently not
97 used for rendering (it could be omitted??) -->
98 <xsl:apply-templates mode="pure" select="$inductive_property"/>
99 <!-- each case has its own "inductive_case" element -->
100 <!-- the inductive case element is composed by:
101 * "case_lhs" element, containing the constructor name applied
102 to its arguments. The arguments are abstraction variables
103 (with types) got form the initial lambdas of the argument
105 * "induction_hypothesis" element, containg the induction
106 hypothesis. Again, these are abstraction variables
107 (with types) got form the initial lambdas of the argument
109 * body of the case, without specific markup.
111 <xsl:for-each select="$inductive_type/Constructor">
112 <xsl:variable name="pos" select="position()"/>
113 <xsl:variable name="current_arg"
114 select="$args_for_cases[position()=$pos]"/>
116 <m:csymbol>inductive_case</m:csymbol>
118 <m:csymbol>case_lhs</m:csymbol>
119 <m:ci definitionURL="{$inductive_def_uri}">
120 <xsl:value-of select="@name"/>
122 <xsl:call-template name="get_constructor_args">
123 <xsl:with-param name="no_params"
124 select="$no_params"/>
125 <xsl:with-param name="constructor_arity"
127 <xsl:with-param name="actual_arg"
128 select="$current_arg"/>
129 <xsl:with-param name="inductive_def_name"
130 select="$inductive_def_name"/>
134 <m:csymbol>induction_hypothesis</m:csymbol>
135 <xsl:call-template name="get_induction_hypothesis">
136 <xsl:with-param name="no_params"
137 select="$no_params"/>
138 <xsl:with-param name="constructor_arity"
140 <xsl:with-param name="actual_arg"
141 select="$current_arg"/>
142 <xsl:with-param name="inductive_def_name"
143 select="$inductive_def_name"/>
146 <xsl:call-template name="get_body">
147 <xsl:with-param name="no_params"
148 select="$no_params"/>
149 <xsl:with-param name="constructor_arity"
151 <xsl:with-param name="actual_arg" select="$current_arg"/>
152 <xsl:with-param name="inductive_def_name"
153 select="$inductive_def_name"/>
157 <!-- the inductive argument is the last argument of extra-args -->
159 <m:csymbol>extra_args</m:csymbol>
160 <xsl:apply-templates mode="pure" select="$extra_args"/>
165 <xsl:apply-templates mode="letin" select="."/>
170 <xsl:apply-templates mode="letin" select="."/>
175 <!-- check_args checks that the number of lambda abstractions
176 of each actual parameter is GREATER OR EQUAL to the number
177 or products of the corresponding formal parameter of the
178 induction principles. That is, that each argument is
179 sufficiently eta-expanded.
180 If this is not the case, not good rendering looks possible.
181 Check_args returns a boolean.
183 <xsl:template name="check_args">
184 <xsl:param name="arg_types" select="/.."/>
185 <xsl:param name="actual_args" select="/.."/>
186 <xsl:param name="bool_var" select="true()"/>
188 <xsl:when test="count($arg_types) = 0">
189 <xsl:value-of select="$bool_var"/>
192 <xsl:variable name="no_expected_arg_of_arg">
193 <xsl:apply-templates mode="count_arity" select="$arg_types[1]">
194 <xsl:with-param name="what" select="'PROD'"/>
195 </xsl:apply-templates>
197 <xsl:variable name="no_actual_abst_of_arg">
198 <xsl:apply-templates mode="count_arity" select="$actual_args[1]">
199 <xsl:with-param name="what" select="'LAMBDA'"/>
200 </xsl:apply-templates>
202 <!-- REPLACE WITH EQUALITY ???? -->
203 <xsl:variable name="test_arg"
204 select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/>
205 <xsl:call-template name="check_args">
206 <xsl:with-param name="arg_types" select="$arg_types[position()>1]"/>
207 <xsl:with-param name="actual_args" select="$actual_args[position()>1]"/>
208 <xsl:with-param name="bool_var" select="($bool_var and $test_arg)"/>
214 <!-- count_arity counts the number of head lambda (or prod) -->
215 <xsl:template mode="count_arity" match="*">
216 <xsl:param name="what" select="'LAMBDA'"/>
217 <xsl:param name="num" select="0"/>
218 <!-- MANCANO I CAST ??? -->
220 <xsl:when test="name(.) = $what">
221 <xsl:apply-templates mode="count_arity" select="target/*[1]">
222 <xsl:with-param name="what" select="$what"/>
223 <xsl:with-param name="num" select="$num+1"/>
224 </xsl:apply-templates>
227 <xsl:value-of select="$num"/>
232 <!-- The following three functions are essentially identical
233 in their recursive structure.
234 The problem is that of decomposing an actual argument for
235 a case in three parts:
236 * constructor variables
237 * induction hypothesis
239 To this aim we must proceed in parallel with the type of
240 the constructor: if the type contains a prod, then the
241 the corresponding lambda of the argument provides the
242 constructor variable. Moreover, if the source type of the
243 prod contains a reference to the inductive type, it is a
244 recursive argument and the NEXT lambda of the argument
245 provides an induction hypothesis.
246 Unfortunately the three functions cannot be merged into a
247 single one without a conversion from document tree fragments
250 <xsl:template name="get_constructor_args">
251 <xsl:param name="no_params" select="0"/>
252 <xsl:param name="constructor_arity" select="/.."/>
253 <xsl:param name="actual_arg" select="/.."/>
254 <xsl:param name="inductive_def_name" select="''"/>
256 <xsl:when test="$no_params = 0">
257 <xsl:if test="name($constructor_arity)='PROD'">
259 <m:ci><xsl:value-of select="$actual_arg/target/@binder"/></m:ci>
261 <xsl:apply-templates mode="pure" select="$actual_arg/source/*[1]"/>
265 <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
266 <xsl:call-template name="get_constructor_args">
267 <xsl:with-param name="constructor_arity"
268 select="$constructor_arity/target/*[1]"/>
269 <xsl:with-param name="actual_arg"
270 select="$actual_arg/target/LAMBDA/target/*[1]"/>
271 <xsl:with-param name="inductive_def_name"
272 select="$inductive_def_name"/>
276 <xsl:call-template name="get_constructor_args">
277 <xsl:with-param name="constructor_arity"
278 select="$constructor_arity/target/*[1]"/>
279 <xsl:with-param name="actual_arg"
280 select="$actual_arg/target/*[1]"/>
281 <xsl:with-param name="inductive_def_name"
282 select="$inductive_def_name"/>
289 <xsl:call-template name="get_constructor_args">
290 <xsl:with-param name="no_params" select="$no_params - 1"/>
291 <xsl:with-param name="constructor_arity"
292 select="$constructor_arity/target/*[1]"/>
293 <xsl:with-param name="actual_arg"
294 select="$actual_arg"/>
295 <xsl:with-param name="inductive_def_name"
296 select="$inductive_def_name"/>
302 <xsl:template name="get_induction_hypothesis">
303 <xsl:param name="no_params" select="0"/>
304 <xsl:param name="constructor_arity" select="/.."/>
305 <xsl:param name="actual_arg" select="/.."/>
306 <xsl:param name="inductive_def_name" select="''"/>
308 <xsl:when test="$no_params = 0">
309 <xsl:if test="name($constructor_arity)='PROD'">
311 <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
314 <xsl:value-of select="$actual_arg/target/LAMBDA/target/@binder"/>
317 <xsl:apply-templates mode="pure"
318 select="$actual_arg/target/LAMBDA/source"/>
321 <xsl:call-template name="get_induction_hypothesis">
322 <xsl:with-param name="constructor_arity"
323 select="$constructor_arity/target/*[1]"/>
324 <xsl:with-param name="actual_arg"
325 select="$actual_arg/target/LAMBDA/target/*[1]"/>
326 <xsl:with-param name="inductive_def_name"
327 select="$inductive_def_name"/>
331 <xsl:call-template name="get_induction_hypothesis">
332 <xsl:with-param name="constructor_arity"
333 select="$constructor_arity/target/*[1]"/>
334 <xsl:with-param name="actual_arg"
335 select="$actual_arg/target/*[1]"/>
336 <xsl:with-param name="inductive_def_name"
337 select="$inductive_def_name"/>
344 <xsl:call-template name="get_induction_hypothesis">
345 <xsl:with-param name="no_params" select="$no_params - 1"/>
346 <xsl:with-param name="constructor_arity"
347 select="$constructor_arity/target/*[1]"/>
348 <xsl:with-param name="actual_arg"
349 select="$actual_arg"/>
350 <xsl:with-param name="inductive_def_name"
351 select="$inductive_def_name"/>
357 <xsl:template name="get_body">
358 <xsl:param name="no_params" select="0"/>
359 <xsl:param name="constructor_arity" select="/.."/>
360 <xsl:param name="actual_arg" select="/.."/>
361 <xsl:param name="inductive_def_name" select="''"/>
363 <xsl:when test="$no_params = 0">
365 <xsl:when test="name($constructor_arity)='PROD'">
367 <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
368 <xsl:call-template name="get_body">
369 <xsl:with-param name="constructor_arity"
370 select="$constructor_arity/target/*[1]"/>
371 <xsl:with-param name="actual_arg"
372 select="$actual_arg/target/LAMBDA/target/*[1]"/>
373 <xsl:with-param name="inductive_def_name"
374 select="$inductive_def_name"/>
378 <xsl:call-template name="get_body">
379 <xsl:with-param name="constructor_arity"
380 select="$constructor_arity/target/*[1]"/>
381 <xsl:with-param name="actual_arg"
382 select="$actual_arg/target/*[1]"/>
383 <xsl:with-param name="inductive_def_name"
384 select="$inductive_def_name"/>
390 <xsl:apply-templates mode="noannot" select="$actual_arg"/>
395 <xsl:call-template name="get_body">
396 <xsl:with-param name="no_params" select="$no_params - 1"/>
397 <xsl:with-param name="constructor_arity"
398 select="$constructor_arity/target/*[1]"/>
399 <xsl:with-param name="actual_arg"
400 select="$actual_arg"/>
401 <xsl:with-param name="inductive_def_name"
402 select="$inductive_def_name"/>