From: Matteo Selmi <matteo.selmi@mail.polimi.it>
Date: Wed, 30 Oct 2002 15:02:54 +0000 (+0000)
Subject: Correct errors due to a different form of LAMBDA
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94ec937790dc8852a895f3b0cec4183d4e5eeb42;p=helm.git

Correct errors due to a different form of LAMBDA
---

diff --git a/helm/style/set.xsl b/helm/style/set.xsl
index f1f7b7e50..b574bc593 100644
--- a/helm/style/set.xsl
+++ b/helm/style/set.xsl
@@ -38,21 +38,20 @@
 <!-- ************************* LOGIC *********************************-->
 
 
-
 <xsl:template match="*" mode="set">
     <xsl:choose>
      <xsl:when test="name() = 'LAMBDA'">
       <m:set>
        <m:bvar>
         <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
+         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[1]/@binder"/></xsl:with-param></xsl:call-template>
         </m:ci>
         <m:type>
-         <xsl:apply-templates select="source" mode="noannot"/>
+         <xsl:apply-templates select="*[1]" mode="noannot"/>
         </m:type>
        </m:bvar>
        <m:condition>
-        <xsl:apply-templates select="target" mode="noannot"/>
+        <xsl:apply-templates select="*[2]" mode="lambda"/>
        </m:condition>
       </m:set>
      </xsl:when>
@@ -62,10 +61,9 @@
     </xsl:choose>
 </xsl:template>
 
-
 <!-- IN -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/In.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -91,7 +89,7 @@
 <!-- NOT-IN -->
 <!-- NOT ha no parameters -->
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
-and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]]" mode="pure">
+and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/In.con']]]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -115,7 +113,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- EMPTY SET -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Empty_set.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -129,7 +127,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 2">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
        </m:set>
@@ -143,7 +141,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- SINGLETON -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Singleton.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -158,7 +156,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 3">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}">
         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
@@ -173,7 +171,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- COUPLE -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Couple.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -189,7 +187,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 4">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}">
         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
@@ -205,7 +203,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- TRIPLE -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -222,7 +220,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 5">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
        <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}">
         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
@@ -239,7 +237,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- INTERSECTION -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Intersection.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -274,7 +272,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- UNION -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Union.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Union.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -308,9 +306,8 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- INCLUDED -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Included.con']]" mode="pure">
-    <xsl:variable name="no_params">
-     <xsl:call-template name="get_no_params">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Included.con']]" mode="pure">
+    <xsl:variable name="no_params">     <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="CONST/@uri"/>
      </xsl:call-template>
@@ -331,7 +328,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- STRICTLY INCLUDED -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Strict_Included.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -354,7 +351,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- SET-DIFF -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Setminus.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -388,7 +385,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- ADD-ELEM -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Add.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Add.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -426,7 +423,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- SUBTRACT-ELEM -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Subtract.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -464,7 +461,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- CARD -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/cardinal.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -490,7 +487,8 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 
 <!-- *******************  SIGMA TYPES  **************************** -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/Subsets/sig.ind']]" mode="pure">
+
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/sig.ind']]" mode="pure">
  <xsl:choose>
   <xsl:when test="count(child::*) = 3">
    <xsl:choose>
@@ -498,14 +496,14 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
      <m:set>
        <m:bvar>
         <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/target/@binder"/></xsl:with-param></xsl:call-template>
+         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/*[1]/@binder"/></xsl:with-param></xsl:call-template>
         </m:ci>
         <m:type>
-         <xsl:apply-templates select="*[3]/source/*[1]" mode="noannot"/>
+         <xsl:apply-templates select="*[3]/*[1]/*[1]" mode="noannot"/>
         </m:type>
        </m:bvar>
        <m:condition>
-        <xsl:apply-templates select="*[3]/target/*[1]" mode="noannot"/>
+        <xsl:apply-templates select="*[3]/*[2]" mode="lambda"/>
        </m:condition>
      </m:set>
     </xsl:when>
@@ -535,4 +533,5 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 </xsl:template>
 
 
+
 </xsl:stylesheet>