helm/style/inductive.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 inductive objects to MathML content:     -->
  29 <!-- First draft: March 2001, Andrea asperti                          -->
  30 <!--******************************************************************-->
  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 <xsl:template mode="inductive" match="APPLY">
  39  <xsl:param name="inductive_def_uri" select="''"/>
  40  <xsl:param name="inductive_def" select="/.."/>
  41  <xsl:param name="inductive_def_index" select="1"/>
  42  <xsl:param name="inductive_def_name" select="''"/>
  43  <xsl:param name="section_params" select="0"/>
  44  <!-- expected_args_type contains the types of the arguments expected by
  45       the induction principle -->
  46  <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
  47  <xsl:variable name="expected_args_types"
  48         select="document($InductiveTypeUrl)/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
  49  <xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
  50  <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
  51  <!-- First check that the induction principle is applied to the
  52       expected number of arguments -->
  53  <xsl:choose>
  54   <xsl:when test="$no_expected_args = count($actual_arguments)">
  55    <!-- Now check that each actual argument starts with the
  56         expected number of lambda abstractions -->
  57    <xsl:variable name="argsOK">
  58     <xsl:call-template name="check_args">
  59      <xsl:with-param name="arg_types" select="$expected_args_types"/>
  60      <xsl:with-param name="actual_args" select="$actual_arguments"/>
  61     </xsl:call-template>
  62    </xsl:variable>
  63    <xsl:choose>
  64     <!-- il semplice test $argsOK non funziona -->
  65     <xsl:when test="string($argsOK) = 'true'">
  66      <!-- arguments are in the expected form: we create a
  67           "by_induction" content element -->
  68      <!-- no_params is the number of paramters in square brackets -->
  69      <xsl:variable name="no_params"
  70       select="$inductive_def/@noParams"/>
  71      <!-- the inductive property is the first argument following
  72           the parameters  -->
  73      <xsl:variable name="inductive_property"
  74                select="$actual_arguments[1 + $no_params]"/>
  75      <xsl:variable name="tail_args"
  76       select="$actual_arguments[position()> (1 + $no_params)]"/>
  77      <!-- inductive_type contains the right inductive type in the
  78           mutual inductive definition -->
  79      <xsl:variable name="inductive_type"
  80       select="$inductive_def/InductiveType[position()=$inductive_def_index]"/>
  81      <xsl:variable name="no_constructors"
  82       select="count($inductive_type/Constructor)"/>
  83      <!-- each case has a single argument -->
  84      <xsl:variable name="args_for_cases"
  85       select="$tail_args[($no_constructors + 1) > position()]"/>
  86      <!-- extra_args contains the remaining arguments; the LAST one
  87           of them is the argument we are inductively arguing on -->
  88      <xsl:variable name="extra_args"
  89       select="$tail_args[position()> $no_constructors]"/>
  90      <m:apply>
  91       <m:csymbol>by_induction</m:csymbol>
  92       <!-- the first (i.e. second) argument of by_induction
  93            is the uri of the inductive definition -->
  94       <m:ci><xsl:value-of select="$inductive_def_uri"/></m:ci>
  95       <!-- next, we have the inductive property, currently not
  96            used for rendering (it could be omitted??) -->
  97       <xsl:apply-templates mode="pure" select="$inductive_property"/>
  98       <!-- each case has its own "inductive_case" element -->
  99       <!-- the inductive case element is composed by:
 100            * "case_lhs" element, containing the constructor name applied
 101               to its arguments. The arguments are abstraction variables
 102               (with types) got form the initial lambdas of the argument
 103               for the case.
 104            * "induction_hypothesis" element, containg the induction
 105               hypothesis. Again, these are abstraction variables
 106               (with types) got form the initial lambdas of the argument
 107               for the case.
 108            * body of the case, without specific markup.
 109        -->
 110       <xsl:for-each select="$inductive_type/Constructor">
 111        <xsl:variable name="pos" select="position()"/>
 112        <xsl:variable name="current_arg"
 113                      select="$args_for_cases[position()=$pos]"/>
 114        <m:apply>
 115         <m:csymbol>inductive_case</m:csymbol>
 116         <m:apply>
 117          <m:csymbol>case_lhs</m:csymbol>
 118          <m:ci definitionURL="{$inductive_def_uri}">
 119           <xsl:value-of select="@name"/>
 120          </m:ci>
 121          <xsl:call-template name="get_constructor_args">
 122           <xsl:with-param name="no_params"
 123                select="$no_params"/>
 124           <xsl:with-param name="constructor_arity"
 125                select="*[1]"/>
 126           <xsl:with-param name="actual_arg"
 127                select="$current_arg"/>
 128           <xsl:with-param name="inductive_def_name"
 129                select="$inductive_def_name"/>
 130           </xsl:call-template>
 131         </m:apply>
 132         <m:apply>
 133          <m:csymbol>induction_hypothesis</m:csymbol>
 134          <xsl:call-template name="get_induction_hypothesis">
 135           <xsl:with-param name="no_params"
 136                select="$no_params"/>
 137           <xsl:with-param name="constructor_arity"
 138                select="*[1]"/>
 139           <xsl:with-param name="actual_arg"
 140                select="$current_arg"/>
 141           <xsl:with-param name="inductive_def_name"
 142                select="$inductive_def_name"/>
 143          </xsl:call-template>
 144         </m:apply>
 145         <xsl:call-template name="get_body">
 146          <xsl:with-param name="no_params"
 147                select="$no_params"/>
 148          <xsl:with-param name="constructor_arity"
 149                select="*[1]"/>
 150          <xsl:with-param name="actual_arg" select="$current_arg"/>
 151          <xsl:with-param name="inductive_def_name"
 152                select="$inductive_def_name"/>
 153         </xsl:call-template>
 154        </m:apply>
 155       </xsl:for-each>
 156       <!-- the inductive argument is the last argument of extra-args -->
 157       <m:apply>
 158        <m:csymbol>extra_args</m:csymbol>
 159        <xsl:apply-templates mode="pure" select="$extra_args"/>
 160       </m:apply>
 161      </m:apply>
 162     </xsl:when>
 163     <xsl:otherwise>
 164      <xsl:apply-templates mode="letin" select="."/>
 165     </xsl:otherwise>
 166    </xsl:choose>
 167   </xsl:when>
 168   <xsl:otherwise>
 169    <xsl:apply-templates mode="letin" select="."/>
 170   </xsl:otherwise>
 171  </xsl:choose>
 172 </xsl:template>
 173
 174 <!-- check_args checks that the number of lambda abstractions
 175      of each actual parameter is GREATER OR EQUAL to the number
 176      or products of the corresponding formal parameter of the
 177      induction principles. That is, that each argument is
 178      sufficiently eta-expanded.
 179      If this is not the case, not good rendering looks possible.
 180      Check_args returns a boolean.
 181    -->
 182 <xsl:template name="check_args">
 183  <xsl:param name="arg_types" select="/.."/>
 184  <xsl:param name="actual_args" select="/.."/>
 185  <xsl:param name="bool_var" select="true()"/>
 186  <xsl:choose>
 187   <xsl:when test="count($arg_types) = 0">
 188     <xsl:value-of select="$bool_var"/>
 189   </xsl:when>
 190   <xsl:otherwise>
 191    <xsl:variable name="no_expected_arg_of_arg">
 192     <xsl:apply-templates mode="count_arity" select="$arg_types[1]">
 193      <xsl:with-param name="what" select="'PROD'"/>
 194     </xsl:apply-templates>
 195    </xsl:variable>
 196    <xsl:variable name="no_actual_abst_of_arg">
 197     <xsl:apply-templates mode="count_arity" select="$actual_args[1]">
 198      <xsl:with-param name="what" select="'LAMBDA'"/>
 199     </xsl:apply-templates>
 200    </xsl:variable>
 201    <!-- REPLACE WITH EQUALITY ???? -->
 202    <xsl:variable name="test_arg"
 203     select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/>
 204    <xsl:call-template name="check_args">
 205     <xsl:with-param name="arg_types" select="$arg_types[position()>1]"/>
 206     <xsl:with-param name="actual_args" select="$actual_args[position()>1]"/>
 207     <xsl:with-param name="bool_var" select="($bool_var and $test_arg)"/>
 208    </xsl:call-template>
 209   </xsl:otherwise>
 210  </xsl:choose>
 211 </xsl:template>
 212
 213 <!-- count_arity counts the number of head lambda (or prod) -->
 214 <xsl:template mode="count_arity" match="*">
 215  <xsl:param name="what" select="'LAMBDA'"/>
 216  <xsl:param name="num" select="0"/>
 217  <!-- MANCANO I CAST ??? -->
 218  <xsl:choose>
 219   <xsl:when test="name(.) = $what">
 220    <xsl:apply-templates mode="count_arity" select="target/*[1]">
 221     <xsl:with-param name="what" select="$what"/>
 222     <xsl:with-param name="num" select="$num+1"/>
 223    </xsl:apply-templates>
 224   </xsl:when>
 225   <xsl:otherwise>
 226    <xsl:value-of select="$num"/>
 227   </xsl:otherwise>
 228  </xsl:choose>
 229 </xsl:template>
 230
 231 <!-- The following three functions are essentially identical
 232      in their recursive structure.
 233      The problem is that of decomposing an actual argument for
 234      a case in three parts:
 235      * constructor variables
 236      * induction hypothesis
 237      * body
 238      To this aim we must proceed in parallel with the type of
 239      the constructor: if the type contains a prod, then the
 240      the corresponding lambda of the argument provides the
 241      constructor variable. Moreover, if the source type of the
 242      prod contains a reference to the inductive type, it is a
 243      recursive argument and the NEXT lambda of the argument
 244      provides an induction hypothesis.
 245      Unfortunately the three functions cannot be merged into a
 246      single one without a conversion from document tree fragments
 247      to node-sets.
 248 -->
 249 <xsl:template name="get_constructor_args">
 250  <xsl:param name="no_params" select="0"/>
 251  <xsl:param name="constructor_arity" select="/.."/>
 252  <xsl:param name="actual_arg" select="/.."/>
 253  <xsl:param name="inductive_def_name" select="''"/>
 254  <xsl:choose>
 255  <xsl:when test="$no_params = 0">
 256  <xsl:if test="name($constructor_arity)='PROD'">
 257   <m:bvar>
 258    <m:ci><xsl:value-of select="$actual_arg/target/@binder"/></m:ci>
 259    <m:type>
 260     <xsl:apply-templates mode="pure" select="$actual_arg/source/*[1]"/>
 261    </m:type>
 262   </m:bvar>
 263   <xsl:choose>
 264    <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
 265     <xsl:call-template name="get_constructor_args">
 266     <xsl:with-param name="constructor_arity"
 267         select="$constructor_arity/target/*[1]"/>
 268     <xsl:with-param name="actual_arg"
 269         select="$actual_arg/target/LAMBDA/target/*[1]"/>
 270     <xsl:with-param name="inductive_def_name"
 271                select="$inductive_def_name"/>
 272     </xsl:call-template>
 273    </xsl:when>
 274    <xsl:otherwise>
 275     <xsl:call-template name="get_constructor_args">
 276     <xsl:with-param name="constructor_arity"
 277         select="$constructor_arity/target/*[1]"/>
 278     <xsl:with-param name="actual_arg"
 279         select="$actual_arg/target/*[1]"/>
 280     <xsl:with-param name="inductive_def_name"
 281                select="$inductive_def_name"/>
 282     </xsl:call-template>
 283    </xsl:otherwise>
 284   </xsl:choose>
 285  </xsl:if>
 286  </xsl:when>
 287  <xsl:otherwise>
 288   <xsl:call-template name="get_constructor_args">
 289     <xsl:with-param name="no_params" select="$no_params - 1"/>
 290     <xsl:with-param name="constructor_arity"
 291         select="$constructor_arity/target/*[1]"/>
 292     <xsl:with-param name="actual_arg"
 293         select="$actual_arg"/>
 294     <xsl:with-param name="inductive_def_name"
 295                select="$inductive_def_name"/>
 296     </xsl:call-template>
 297  </xsl:otherwise>
 298  </xsl:choose>
 299 </xsl:template>
 300
 301 <xsl:template name="get_induction_hypothesis">
 302  <xsl:param name="no_params" select="0"/>
 303  <xsl:param name="constructor_arity" select="/.."/>
 304  <xsl:param name="actual_arg" select="/.."/>
 305  <xsl:param name="inductive_def_name" select="''"/>
 306  <xsl:choose>
 307  <xsl:when test="$no_params = 0">
 308  <xsl:if test="name($constructor_arity)='PROD'">
 309   <xsl:choose>
 310    <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
 311     <m:bvar>
 312      <m:ci>
 313       <xsl:value-of select="$actual_arg/target/LAMBDA/target/@binder"/>
 314      </m:ci>
 315      <m:type>
 316       <xsl:apply-templates mode="pure"
 317            select="$actual_arg/target/LAMBDA/source"/>
 318      </m:type>
 319     </m:bvar>
 320     <xsl:call-template name="get_induction_hypothesis">
 321     <xsl:with-param name="constructor_arity"
 322         select="$constructor_arity/target/*[1]"/>
 323     <xsl:with-param name="actual_arg"
 324         select="$actual_arg/target/LAMBDA/target/*[1]"/>
 325     <xsl:with-param name="inductive_def_name"
 326                select="$inductive_def_name"/>
 327     </xsl:call-template>
 328    </xsl:when>
 329    <xsl:otherwise>
 330     <xsl:call-template name="get_induction_hypothesis">
 331     <xsl:with-param name="constructor_arity"
 332         select="$constructor_arity/target/*[1]"/>
 333     <xsl:with-param name="actual_arg"
 334         select="$actual_arg/target/*[1]"/>
 335     <xsl:with-param name="inductive_def_name"
 336                select="$inductive_def_name"/>
 337     </xsl:call-template>
 338    </xsl:otherwise>
 339   </xsl:choose>
 340  </xsl:if>
 341  </xsl:when>
 342  <xsl:otherwise>
 343   <xsl:call-template name="get_induction_hypothesis">
 344     <xsl:with-param name="no_params" select="$no_params - 1"/>
 345     <xsl:with-param name="constructor_arity"
 346         select="$constructor_arity/target/*[1]"/>
 347     <xsl:with-param name="actual_arg"
 348         select="$actual_arg"/>
 349     <xsl:with-param name="inductive_def_name"
 350                select="$inductive_def_name"/>
 351     </xsl:call-template>
 352  </xsl:otherwise>
 353  </xsl:choose>
 354 </xsl:template>
 355
 356 <xsl:template name="get_body">
 357  <xsl:param name="no_params" select="0"/>
 358  <xsl:param name="constructor_arity" select="/.."/>
 359  <xsl:param name="actual_arg" select="/.."/>
 360  <xsl:param name="inductive_def_name" select="''"/>
 361  <xsl:choose>
 362  <xsl:when test="$no_params = 0">
 363  <xsl:choose>
 364  <xsl:when test="name($constructor_arity)='PROD'">
 365   <xsl:choose>
 366    <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
 367     <xsl:call-template name="get_body">
 368     <xsl:with-param name="constructor_arity"
 369         select="$constructor_arity/target/*[1]"/>
 370     <xsl:with-param name="actual_arg"
 371         select="$actual_arg/target/LAMBDA/target/*[1]"/>
 372     <xsl:with-param name="inductive_def_name"
 373                select="$inductive_def_name"/>
 374     </xsl:call-template>
 375    </xsl:when>
 376    <xsl:otherwise>
 377     <xsl:call-template name="get_body">
 378     <xsl:with-param name="constructor_arity"
 379         select="$constructor_arity/target/*[1]"/>
 380     <xsl:with-param name="actual_arg"
 381         select="$actual_arg/target/*[1]"/>
 382     <xsl:with-param name="inductive_def_name"
 383                select="$inductive_def_name"/>
 384     </xsl:call-template>
 385    </xsl:otherwise>
 386   </xsl:choose>
 387  </xsl:when>
 388  <xsl:otherwise>
 389   <xsl:apply-templates mode="noannot" select="$actual_arg"/>
 390  </xsl:otherwise>
 391  </xsl:choose>
 392  </xsl:when>
 393  <xsl:otherwise>
 394   <xsl:call-template name="get_body">
 395     <xsl:with-param name="no_params" select="$no_params - 1"/>
 396     <xsl:with-param name="constructor_arity"
 397         select="$constructor_arity/target/*[1]"/>
 398     <xsl:with-param name="actual_arg"
 399         select="$actual_arg"/>
 400     <xsl:with-param name="inductive_def_name"
 401                select="$inductive_def_name"/>
 402     </xsl:call-template>
 403  </xsl:otherwise>
 404  </xsl:choose>
 405 </xsl:template>
 406
 407 </xsl:stylesheet>