X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Finductive.xsl;h=1d6dc4dd7b76a815876ad72a69cc90c8f92717ed;hb=000ee25879c192864cfaa0ebc27cc91a896378df;hp=4066d4be3e289a76395cbd556adb8d4bb76b853a;hpb=edeecdcf2cb51318a7d4c608652f4f988e80f66f;p=helm.git

diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 4066d4be3..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" 
@@ -245,17 +250,18 @@
  <xsl:param name="arg_types" select="/.."/>
  <xsl:param name="actual_args" select="/.."/>
  <xsl:param name="bool_var" select="true()"/>
+ <!-- <xsl:value-of select="false()"/> -->
  <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" 
-                 select="count($arg_types[1]/PROD/decl)"/>
+                 select="count($arg_types[1]/decl)"/>
    <xsl:variable name="no_actual_abst_of_arg" 
-                 select="count($actual_args[1]/LAMBDA/decl)"/> 
+                 select="count($actual_args[1]/decl)"/> 
    <xsl:variable name="test_arg" 
-    select="$no_actual_abst_of_arg >= $no_expected_arg_of_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]"/>