From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 6 Dec 2002 16:04:07 +0000 (+0000)
Subject: instantiate for induction principles covered.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6dbd09d74f55aab28ddcb9ba59d77996641d1eda;p=helm.git

instantiate for induction principles covered.
---

diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 21f16d7a4..1d6dc4dd7 100644
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -50,54 +50,59 @@
 
 <xsl:template mode="try_inductive" match="APPLY">
  <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="uri">
   <xsl:choose>
-   <xsl:when test="CONST[1]">
-    <xsl:variable name="uri" select="CONST[1]/@uri"/>
-    <xsl:choose>
-     <xsl:when test="contains($uri,'_ind.con')">
-      <xsl:variable name="ind_uri" 
-        select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
-      <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
-      <xsl:variable name="inductive_def" 
-     select="document($InductiveTypeUrl)/InductiveDefinition"/>
-      <xsl:choose>
-       <xsl:when test="$inductive_def">
-        <xsl:variable name="ind_name">
-         <xsl:call-template name="get_name">
-          <xsl:with-param name="uri" select="$uri"/>
-         </xsl:call-template>
-        </xsl:variable>
-        <xsl:apply-templates mode="inductive" select=".">
-         <xsl:with-param name="inductive_def_uri" 
-          select="$ind_uri"/>
-         <xsl:with-param name="inductive_def" select="$inductive_def"/>
-         <xsl:with-param name="inductive_def_index" select="1"/>
-         <xsl:with-param name="inductive_def_name" select="$ind_name"/>
-        </xsl:apply-templates>
-       </xsl:when>
-       <xsl:otherwise>
-        <xsl:apply-templates select="." mode="letin"/>
-       </xsl:otherwise>
-      </xsl:choose>
-     </xsl:when>
-     <xsl:otherwise>
-      <xsl:apply-templates select="." mode="letin"/>
-     </xsl:otherwise>
-    </xsl:choose>
+   <xsl:when test="name(*[1])='CONST'">
+    <xsl:value-of select="*[1]/@uri"/>
    </xsl:when>
    <xsl:otherwise>
-    <xsl:apply-templates select="." mode="letin"/>
+    <!-- instantiate -->
+    <xsl:value-of select="*[1]/CONST[1]/@uri"/>
    </xsl:otherwise>
   </xsl:choose>
+ </xsl:variable>
+ <xsl:choose>
+  <xsl:when test="contains($uri,'_ind.con')">
+   <xsl:variable name="ind_uri" 
+        select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
+   <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
+   <xsl:variable name="inductive_def" 
+        select="document($InductiveTypeUrl)/InductiveDefinition"/>
+   <xsl:choose>
+    <xsl:when test="$inductive_def">
+     <xsl:variable name="ind_name">
+      <xsl:call-template name="get_name">
+       <xsl:with-param name="uri" select="$uri"/>
+      </xsl:call-template>
+     </xsl:variable>
+     <xsl:apply-templates mode="inductive" select=".">
+      <xsl:with-param name="uri" select="$uri"/>
+      <xsl:with-param name="inductive_def_uri" 
+       select="$ind_uri"/>
+      <xsl:with-param name="inductive_def" select="$inductive_def"/>
+      <xsl:with-param name="inductive_def_index" select="1"/>
+      <xsl:with-param name="inductive_def_name" select="$ind_name"/>
+     </xsl:apply-templates>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:apply-templates select="." mode="letin"/>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-templates select="." mode="letin"/>
+  </xsl:otherwise>
+ </xsl:choose>
 </xsl:template>
 
 
 <xsl:template mode="inductive" match="APPLY">
+ <xsl:param name="uri" select="''"/> 
  <xsl:param name="inductive_def_uri" select="''"/>
  <xsl:param name="inductive_def" select="/.."/>
  <xsl:param name="inductive_def_index" select="1"/>
  <xsl:param name="inductive_def_name" select="''"/>
- <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$uri"/></xsl:call-template></xsl:variable>
  <!-- expected_args_type contains the types of the arguments expected by
       the induction principle -->
  <xsl:variable name="expected_args_types"