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 <!-- Completely revisited: November 2002, Andrea asperti -->
30 <!-- First draft: March 2001, Andrea asperti -->
31 <!--******************************************************************-->
34 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
35 xmlns:m="http://www.w3.org/1998/Math/MathML"
36 xmlns:helm="http://www.cs.unibo.it/helm">
38 <!-- try_inductive essentially checks if the head constant is an
39 invocation of an induction principle.
40 Si presuppone che il tipo induttivo non sia mutuamente
41 induttivo. Bisognerebbe andare a vedere l'utlimo parametro
42 del presunto "principio di induzione", tirare fuori il tipo induttivo
43 e vedere se il suo nome coincide con il prefisso di _ind.
44 Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
45 parametro di nat_double_ind e' di tipo nat, e nat e' diverso
46 da nat_double. Per ora, verifico solo l'esistenza di nat_double,
47 ma questo, benche' non porti ad errore, non copre tutti i
48 casi per quelli mutuamente induttivi -->
51 <xsl:template mode="try_inductive" match="APPLY">
52 <xsl:variable name="id" select="@id"/>
53 <xsl:variable name="uri">
55 <xsl:when test="name(*[1])='CONST'">
56 <xsl:value-of select="*[1]/@uri"/>
60 <xsl:value-of select="*[1]/CONST[1]/@uri"/>
65 <xsl:when test="contains($uri,'_ind.con')">
66 <xsl:variable name="ind_uri"
67 select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
68 <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
69 <xsl:variable name="inductive_def"
70 select="document($InductiveTypeUrl)/InductiveDefinition"/>
72 <xsl:when test="$inductive_def">
73 <xsl:variable name="ind_name">
74 <xsl:call-template name="get_name">
75 <xsl:with-param name="uri" select="$uri"/>
78 <xsl:apply-templates mode="inductive" select=".">
79 <xsl:with-param name="uri" select="$uri"/>
80 <xsl:with-param name="inductive_def_uri"
82 <xsl:with-param name="inductive_def" select="$inductive_def"/>
83 <xsl:with-param name="inductive_def_index" select="1"/>
84 <xsl:with-param name="inductive_def_name" select="$ind_name"/>
85 </xsl:apply-templates>
88 <xsl:apply-templates select="." mode="letin"/>
93 <xsl:apply-templates select="." mode="letin"/>
99 <xsl:template mode="inductive" match="APPLY">
100 <xsl:param name="uri" select="''"/>
101 <xsl:param name="inductive_def_uri" select="''"/>
102 <xsl:param name="inductive_def" select="/.."/>
103 <xsl:param name="inductive_def_index" select="1"/>
104 <xsl:param name="inductive_def_name" select="''"/>
105 <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$uri"/></xsl:call-template></xsl:variable>
106 <!-- expected_args_type contains the types of the arguments expected by
107 the induction principle -->
108 <xsl:variable name="expected_args_types"
109 select="document($InductiveTypeUrl)/ConstantType/PROD/decl/*[1]"/>
110 <xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
111 <xsl:variable name="actual_arguments" select="*[position()>1]"/>
112 <!-- First check that the induction principle is applied to the
113 expected number of arguments -->
115 <xsl:when test="$no_expected_args = count($actual_arguments)">
116 <!-- Now check that each actual argument starts with the
117 expected number of lambda abstractions -->
118 <xsl:variable name="argsOK">
119 <xsl:call-template name="check_args">
120 <xsl:with-param name="arg_types" select="$expected_args_types"/>
121 <xsl:with-param name="actual_args" select="$actual_arguments"/>
125 <!-- il semplice test $argsOK non funziona -->
126 <xsl:when test="string($argsOK) = 'true'">
127 <!-- arguments are in the expected form: we create a
128 "by_induction" content element -->
129 <!-- no_params is the number of parameters in square brackets -->
130 <xsl:variable name="no_params"
131 select="$inductive_def/@noParams"/>
132 <!-- the inductive property is the first argument following
134 <xsl:variable name="inductive_property"
135 select="$actual_arguments[1 + $no_params]"/>
136 <xsl:variable name="tail_args"
137 select="$actual_arguments[position()> (1 + $no_params)]"/>
138 <!-- inductive_type contains the right inductive type in the
139 mutual inductive definition -->
140 <xsl:variable name="inductive_type"
141 select="$inductive_def/InductiveType[position()=$inductive_def_index]"/>
142 <xsl:variable name="no_constructors"
143 select="count($inductive_type/Constructor)"/>
144 <!-- each case has a single argument -->
145 <xsl:variable name="args_for_cases"
146 select="$tail_args[($no_constructors + 1) > position()]"/>
147 <!-- extra_args contains the remaining arguments; the LAST one
148 of them is the argument we are inductively arguing on -->
149 <xsl:variable name="extra_args"
150 select="$tail_args[position()> $no_constructors]"/>
152 <m:csymbol>by_induction</m:csymbol>
153 <!-- the first (i.e. second) argument of by_induction
154 is the uri of the inductive definition -->
155 <m:ci><xsl:value-of select="$inductive_def_uri"/></m:ci>
156 <!-- next, we have the inductive property, currently not
157 used for rendering (it could be omitted ??) -->
158 <xsl:apply-templates mode="pure" select="$inductive_property"/>
159 <!-- each case has its own "inductive_case" element -->
160 <!-- the inductive case element is composed by:
161 * "case_lhs" element, containing the constructor name applied
162 to its arguments. The arguments are abstraction variables
163 (with types) got form the initial lambdas of the argument
165 * "induction_hypothesis" element, containg the induction
166 hypothesis. Again, these are abstraction variables
167 (with types) got form the initial lambdas of the argument
169 * body of the case, without specific markup.
171 <xsl:for-each select="$inductive_type/Constructor">
172 <xsl:variable name="pos" select="position()"/>
173 <xsl:variable name="current_arg"
174 select="$args_for_cases[position()=$pos]"/>
176 <m:csymbol>inductive_case</m:csymbol>
178 <m:csymbol>case_lhs</m:csymbol>
179 <m:ci definitionURL="{$inductive_def_uri}">
180 <xsl:value-of select="@name"/>
182 <xsl:call-template name="get_constructor_args">
183 <xsl:with-param name="constructor_args"
184 select="PROD/decl[position()> $no_params]"/>
185 <xsl:with-param name="actual_args"
186 select="$current_arg/decl"/>
187 <xsl:with-param name="inductive_def_uri"
188 select="$inductive_def_uri"/>
192 <m:csymbol>induction_hypothesis</m:csymbol>
193 <xsl:call-template name="get_induction_hypothesis">
194 <xsl:with-param name="constructor_args"
195 select="PROD/decl[position()> $no_params]"/>
196 <xsl:with-param name="actual_args"
197 select="$current_arg/decl"/>
198 <xsl:with-param name="inductive_def_uri"
199 select="$inductive_def_uri"/>
203 <xsl:when test="count(PROD/decl) > $no_params">
204 <!-- in this case the actual_arg must be a LAMBDA -->
205 <xsl:call-template name="get_body">
206 <xsl:with-param name="constructor_args"
207 select="PROD/decl[position()>$no_params]"/>
208 <xsl:with-param name="actual_args" select="$current_arg/decl"/>
209 <xsl:with-param name="inductive_def_uri"
210 select="$inductive_def_uri"/>
211 <xsl:with-param name="target"
212 select="$current_arg/target/*[1]"/>
216 <xsl:apply-templates mode="noannot" select="$current_arg"/>
221 <!-- the inductive argument is the last argument of extra-args -->
223 <m:csymbol>extra_args</m:csymbol>
224 <xsl:apply-templates mode="pure" select="$extra_args"/>
229 <xsl:apply-templates mode="letin" select="."/>
234 <xsl:apply-templates mode="letin" select="."/>
239 <!-- check_args checks that the number of lambda abstractions
240 of each actual parameter is GREATER OR EQUAL to the number
241 or products of the corresponding formal parameter of the
242 induction principles. That is, that each argument is
243 sufficiently eta-expanded.
244 If this is not the case, not good rendering looks possible.
245 Check_args returns a boolean.
249 <xsl:template name="check_args">
250 <xsl:param name="arg_types" select="/.."/>
251 <xsl:param name="actual_args" select="/.."/>
252 <xsl:param name="bool_var" select="true()"/>
253 <!-- <xsl:value-of select="false()"/> -->
255 <xsl:when test="count($arg_types) = 0">
256 <xsl:value-of select="$bool_var"/>
259 <xsl:variable name="no_expected_arg_of_arg"
260 select="count($arg_types[1]/decl)"/>
261 <xsl:variable name="no_actual_abst_of_arg"
262 select="count($actual_args[1]/decl)"/>
263 <xsl:variable name="test_arg"
264 select="($no_actual_abst_of_arg >= $no_expected_arg_of_arg)"/>
265 <xsl:call-template name="check_args">
266 <xsl:with-param name="arg_types" select="$arg_types[position()>1]"/>
267 <xsl:with-param name="actual_args" select="$actual_args[position()>1]"/>
268 <xsl:with-param name="bool_var" select="($bool_var and $test_arg)"/>
275 <!-- The following three functions are essentially identical
276 in their recursive structure.
277 The problem is that of decomposing an actual argument for
278 a case in three parts:
279 * constructor variables
280 * induction hypothesis
282 To this aim we must proceed in parallel with the type of
283 the constructor: if the type contains a prod, then the
284 the corresponding lambda of the argument provides the
285 constructor variable. Moreover, if the source type of the
286 prod contains a reference to the inductive type, it is a
287 recursive argument and the NEXT lambda of the argument
288 provides an induction hypothesis.
289 Unfortunately the three functions cannot be merged into a
290 single one without a conversion from document tree fragments
294 <xsl:template name="get_constructor_args">
295 <xsl:param name="constructor_args" select="/.."/>
296 <xsl:param name="actual_args" select="/.."/>
297 <xsl:param name="inductive_def_uri" select="''"/>
298 <xsl:if test="$constructor_args">
300 <m:ci><xsl:value-of select="$actual_args[1]/@binder"/></m:ci>
302 <xsl:apply-templates mode="pure" select="$actual_args[1]/*"/>
306 <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
307 <xsl:call-template name="get_constructor_args">
308 <xsl:with-param name="constructor_arity"
309 select="$constructor_args[position()>1]"/>
310 <xsl:with-param name="actual_args"
311 select="$actual_args[position()>2]"/>
312 <xsl:with-param name="inductive_def_uri"
313 select="$inductive_def_uri"/>
317 <xsl:call-template name="get_constructor_args">
318 <xsl:with-param name="constructor_args"
319 select="$constructor_args[position()>1]"/>
320 <xsl:with-param name="actual_args"
321 select="$actual_args[position()>1]"/>
322 <xsl:with-param name="inductive_def_uri"
323 select="$inductive_def_uri"/>
330 <xsl:template name="get_induction_hypothesis">
331 <xsl:param name="constructor_args" select="/.."/>
332 <xsl:param name="actual_args" select="/.."/>
333 <xsl:param name="inductive_def_uri" select="''"/>
334 <xsl:if test="$constructor_args">
336 <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
339 <xsl:value-of select="$actual_args[2]/@binder"/>
342 <xsl:apply-templates mode="pure"
343 select="$actual_args[2]/*"/>
346 <xsl:call-template name="get_induction_hypothesis">
347 <xsl:with-param name="constructor_args"
348 select="$constructor_args[position()>1]"/>
349 <xsl:with-param name="actual_args"
350 select="$actual_args[position()>2]"/>
351 <xsl:with-param name="inductive_def_uri"
352 select="$inductive_def_uri"/>
356 <xsl:call-template name="get_induction_hypothesis">
357 <xsl:with-param name="constructor_args"
358 select="$constructor_args[position()>1]"/>
359 <xsl:with-param name="actual_args"
360 select="$actual_args[position()>1]"/>
361 <xsl:with-param name="inductive_def_uri"
362 select="$inductive_def_uri"/>
369 <xsl:template name="get_body">
370 <xsl:param name="constructor_args" select="/.."/>
371 <xsl:param name="actual_args" select="/.."/>
372 <xsl:param name="inductive_def_uri" select="''"/>
373 <xsl:param name="target" select="/.."/>
375 <xsl:when test="$constructor_args">
377 <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
378 <xsl:call-template name="get_body">
379 <xsl:with-param name="constructor_args"
380 select="$constructor_args[position()> 1]"/>
381 <xsl:with-param name="actual_args"
382 select="$actual_args[position()> 2]"/>
383 <xsl:with-param name="inductive_def_uri"
384 select="$inductive_def_uri"/>
385 <xsl:with-param name="target"
390 <xsl:call-template name="get_body">
391 <xsl:with-param name="constructor_args"
392 select="$constructor_args[position()> 1]"/>
393 <xsl:with-param name="actual_args"
394 select="$actual_args[position()> 1]"/>
395 <xsl:with-param name="inductive_def_uri"
396 select="$inductive_def_uri"/>
397 <xsl:with-param name="target"
405 <xsl:when test="$actual_args">
406 <xsl:apply-templates select="$actual_args[1]" mode="lambda_prop"/>
409 <xsl:apply-templates mode="noannot" select="$target"/>