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