From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 3 Apr 2001 08:18:56 +0000 (+0000)
Subject: *** empty log message ***
X-Git-Tag: v0_1_2~43
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0a3a47d4b47605d55010bc2ef1175e8562bbdec2;p=helm.git

*** empty log message ***
---

diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
new file mode 100644
index 000000000..5211c000c
--- /dev/null
+++ b/helm/style/inductive.xsl
@@ -0,0 +1,410 @@
+<?xml version="1.0"?>
+
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
+<!--******************************************************************--> 
+<!-- XSLT version 0.1 of CIC inductive objects to MathML content:     -->
+<!-- First draft: March 2001, Andrea asperti                          -->
+<!--******************************************************************-->
+
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm">
+
+
+<xsl:template mode="inductive" match="APPLY">
+ <xsl:param name="inductive_def_uri" select="/.."/>
+ <xsl:param name="inductive_def_index" select="1"/>
+ <xsl:param name="inductive_def_name" select="''"/>
+ <xsl:param name="section_params" select="0"/>
+ <!-- expected_args_type contains the types of the arguments expected by
+      the induction principle -->
+ <xsl:variable name="expected_args_types" 
+	select="document(concat(string($absPath),*[1]/@uri))/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
+ <xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
+ <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
+ <!-- First check that the induction principle is applied to the
+      expected number of arguments -->
+ <xsl:choose>
+  <xsl:when test="$no_expected_args = count($actual_arguments)">
+   <!-- Now check that each actual argument starts with the
+        expected number of lambda abstractions -->
+   <xsl:variable name="argsOK"> 
+    <xsl:call-template name="check_args">
+     <xsl:with-param name="arg_types" select="$expected_args_types"/>
+     <xsl:with-param name="actual_args" select="$actual_arguments"/>
+    </xsl:call-template>
+   </xsl:variable>
+   <xsl:choose>
+    <!-- il semplice test $argsOK non funziona -->
+    <xsl:when test="string($argsOK) = 'true'">
+     <!-- arguments are in the expected form: we create a
+          "by_induction" content element -->
+     <!-- inductive_def contains the inductive definition -->
+     <xsl:variable name="inductive_def" 
+      select="document(concat(string($absPath),$inductive_def_uri))/InductiveDefinition"/>
+     <!-- no_params is the number of paramters in square brackets -->
+     <xsl:variable name="no_params" 
+      select="$inductive_def/@noParams"/>
+     <!-- the inductive property is the first argument following
+          the parameters  -->
+     <xsl:variable name="inductive_property" 
+               select="$actual_arguments[1 + $no_params]"/>
+     <xsl:variable name="tail_args" 
+      select="$actual_arguments[position()> (1 + $no_params)]"/>
+     <!-- inductive_type contains the right inductive type in the
+          mutual inductive definition -->
+     <xsl:variable name="inductive_type" 
+      select="$inductive_def/InductiveType[position()=$inductive_def_index]"/>
+     <xsl:variable name="no_constructors" 
+      select="count($inductive_type/Constructor)"/>
+     <!-- each case has a single argument -->
+     <xsl:variable name="args_for_cases" 
+      select="$tail_args[($no_constructors + 1) > position()]"/>
+     <!-- extra_args contains the remaining arguments; the LAST one
+          of them is the argument we are inductively arguing on -->
+     <xsl:variable name="extra_args" 
+      select="$tail_args[position()> $no_constructors]"/>
+     <m:apply>
+      <m:csymbol>by_induction</m:csymbol>
+      <!-- the first (i.e. second) argument of by_induction
+           is the uri of the inductive definition -->
+      <m:ci><xsl:value-of select="$inductive_def_uri"/></m:ci>
+      <!-- next, we have the inductive property, currently not
+           used for rendering (it could be omitted??) -->
+      <xsl:apply-templates mode="pure" select="$inductive_property"/>
+      <!-- each case has its own "inductive_case" element -->
+      <!-- the inductive case element is composed by:
+           * "case_lhs" element, containing the constructor name applied
+              to its arguments. The arguments are abstraction variables
+              (with types) got form the initial lambdas of the argument
+              for the case.
+           * "induction_hypothesis" element, containg the induction 
+              hypothesis. Again, these are abstraction variables
+              (with types) got form the initial lambdas of the argument
+              for the case.
+           * body of the case, without specific markup.
+       -->
+      <xsl:for-each select="$inductive_type/Constructor">
+       <xsl:variable name="pos" select="position()"/>
+       <xsl:variable name="current_arg" 
+                     select="$args_for_cases[position()=$pos]"/>
+       <m:apply>
+        <m:csymbol>inductive_case</m:csymbol>
+        <m:apply>
+         <m:csymbol>case_lhs</m:csymbol>
+         <m:ci definitionURL="{$inductive_def_uri}">
+          <xsl:value-of select="@name"/>
+         </m:ci>     
+         <xsl:call-template name="get_constructor_args">
+          <xsl:with-param name="no_params" 
+               select="$no_params"/>
+          <xsl:with-param name="constructor_arity" 
+               select="*[1]"/>
+          <xsl:with-param name="actual_arg" 
+               select="$current_arg"/>
+          <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+          </xsl:call-template>
+        </m:apply>
+        <m:apply>
+         <m:csymbol>induction_hypothesis</m:csymbol>
+         <xsl:call-template name="get_induction_hypothesis">
+          <xsl:with-param name="no_params" 
+               select="$no_params"/>
+          <xsl:with-param name="constructor_arity" 
+               select="*[1]"/>
+          <xsl:with-param name="actual_arg" 
+               select="$current_arg"/>
+          <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+         </xsl:call-template>
+        </m:apply>
+        <xsl:call-template name="get_body">
+         <xsl:with-param name="no_params" 
+               select="$no_params"/>
+         <xsl:with-param name="constructor_arity" 
+               select="*[1]"/>
+         <xsl:with-param name="actual_arg" select="$current_arg"/>
+         <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+        </xsl:call-template>
+       </m:apply>
+      </xsl:for-each>
+      <!-- the inductive argument is the last argument of extra-args -->
+      <m:apply>
+       <m:csymbol>extra_args</m:csymbol>
+       <xsl:apply-templates mode="pure" select="$extra_args"/>
+      </m:apply>
+     </m:apply>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:apply-templates mode="letin" select="."/>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-templates mode="letin" select="."/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- check_args checks that the number of lambda abstractions
+     of each actual parameter is GREATER OR EQUAL to the number
+     or products of the corresponding formal parameter of the
+     induction principles. That is, that each argument is 
+     sufficiently eta-expanded.
+     If this is not the case, not good rendering looks possible.
+     Check_args returns a boolean. 
+   -->
+<xsl:template name="check_args">
+ <xsl:param name="arg_types" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="bool_var" select="true()"/>
+ <xsl:choose>
+  <xsl:when test="count($arg_types) = 0">
+    <xsl:value-of select="$bool_var"/>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:variable name="no_expected_arg_of_arg">
+    <xsl:apply-templates mode="count_arity" select="$arg_types[1]">
+     <xsl:with-param name="what" select="'PROD'"/>
+    </xsl:apply-templates>
+   </xsl:variable>
+   <xsl:variable name="no_actual_abst_of_arg"> 
+    <xsl:apply-templates mode="count_arity" select="$actual_args[1]">
+     <xsl:with-param name="what" select="'LAMBDA'"/>
+    </xsl:apply-templates>
+   </xsl:variable>
+   <!-- REPLACE WITH EQUALITY ???? -->
+   <xsl:variable name="test_arg" 
+    select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/> 
+   <xsl:call-template name="check_args">
+    <xsl:with-param name="arg_types" select="$arg_types[position()>1]"/>
+    <xsl:with-param name="actual_args" select="$actual_args[position()>1]"/>
+    <xsl:with-param name="bool_var" select="($bool_var and $test_arg)"/>
+   </xsl:call-template> 
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- count_arity counts the number of head lambda (or prod) -->
+<xsl:template mode="count_arity" match="*">
+ <xsl:param name="what" select="'LAMBDA'"/>
+ <xsl:param name="num" select="0"/>
+ <!-- MANCANO I CAST ??? -->
+ <xsl:choose>
+  <xsl:when test="name(.) = $what">
+   <xsl:apply-templates mode="count_arity" select="target/*[1]">
+    <xsl:with-param name="what" select="$what"/>
+    <xsl:with-param name="num" select="$num+1"/>
+   </xsl:apply-templates>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:value-of select="$num"/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- The following three functions are essentially identical
+     in their recursive structure.
+     The problem is that of decomposing an actual argument for
+     a case in three parts: 
+     * constructor variables
+     * induction hypothesis
+     * body
+     To this aim we must proceed in parallel with the type of
+     the constructor: if the type contains a prod, then the 
+     the corresponding lambda of the argument provides the 
+     constructor variable. Moreover, if the source type of the
+     prod contains a reference to the inductive type, it is a
+     recursive argument and the NEXT lambda of the argument 
+     provides an induction hypothesis.
+     Unfortunately the three functions cannot be merged into a
+     single one without a conversion from document tree fragments
+     to node-sets. 
+-->
+<xsl:template name="get_constructor_args">
+ <xsl:param name="no_params" select="0"/>
+ <xsl:param name="constructor_arity" select="/.."/>
+ <xsl:param name="actual_arg" select="/.."/>
+ <xsl:param name="inductive_def_name" select="''"/>
+ <xsl:choose>
+ <xsl:when test="$no_params = 0">
+ <xsl:if test="name($constructor_arity)='PROD'">
+  <m:bvar>
+   <m:ci><xsl:value-of select="$actual_arg/target/@binder"/></m:ci>
+   <m:type>
+    <xsl:apply-templates mode="pure" select="$actual_arg/source/*[1]"/>
+   </m:type> 
+  </m:bvar>
+  <xsl:choose>
+   <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+    <xsl:call-template name="get_constructor_args">
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg/target/LAMBDA/target/*[1]"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:call-template name="get_constructor_args">
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg/target/*[1]"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:if>
+ </xsl:when>
+ <xsl:otherwise>
+  <xsl:call-template name="get_constructor_args">
+    <xsl:with-param name="no_params" select="$no_params - 1"/>
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="get_induction_hypothesis">
+ <xsl:param name="no_params" select="0"/>
+ <xsl:param name="constructor_arity" select="/.."/>
+ <xsl:param name="actual_arg" select="/.."/>
+ <xsl:param name="inductive_def_name" select="''"/>
+ <xsl:choose>
+ <xsl:when test="$no_params = 0">
+ <xsl:if test="name($constructor_arity)='PROD'">
+  <xsl:choose>
+   <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+    <m:bvar>
+     <m:ci>
+      <xsl:value-of select="$actual_arg/target/LAMBDA/target/@binder"/>
+     </m:ci>
+     <m:type>
+      <xsl:apply-templates mode="pure" 
+           select="$actual_arg/target/LAMBDA/source"/>
+     </m:type>
+    </m:bvar>
+    <xsl:call-template name="get_induction_hypothesis">
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg/target/LAMBDA/target/*[1]"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:call-template name="get_induction_hypothesis">
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg/target/*[1]"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:if>
+ </xsl:when>
+ <xsl:otherwise>
+  <xsl:call-template name="get_induction_hypothesis">
+    <xsl:with-param name="no_params" select="$no_params - 1"/>
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="get_body">
+ <xsl:param name="no_params" select="0"/>
+ <xsl:param name="constructor_arity" select="/.."/>
+ <xsl:param name="actual_arg" select="/.."/>
+ <xsl:param name="inductive_def_name" select="''"/>
+ <xsl:choose>
+ <xsl:when test="$no_params = 0">
+ <xsl:choose>
+ <xsl:when test="name($constructor_arity)='PROD'">
+  <xsl:choose>
+   <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+    <xsl:call-template name="get_body">
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg/target/LAMBDA/target/*[1]"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:call-template name="get_body">
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg/target/*[1]"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+  <xsl:apply-templates mode="noannot" select="$actual_arg"/>
+ </xsl:otherwise> 
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+  <xsl:call-template name="get_body">
+    <xsl:with-param name="no_params" select="$no_params - 1"/>
+    <xsl:with-param name="constructor_arity" 
+        select="$constructor_arity/target/*[1]"/>
+    <xsl:with-param name="actual_arg" 
+        select="$actual_arg"/>
+    <xsl:with-param name="inductive_def_name" 
+               select="$inductive_def_name"/>
+    </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
+</xsl:stylesheet>
+