From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Dec 2000 18:37:08 +0000 (+0000)
Subject: Performance improvements using the sort attribute
X-Git-Tag: nogzip~92
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6e68f7835f9b0fedb5c8b6bdda3f1abfe776428;p=helm.git

Performance improvements using the sort attribute
---

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index d36e0152a..e71ba3fe1 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -116,7 +116,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
       <m:csymbol>letin</m:csymbol>
       <!-- <xsl:for-each select="*[boolean(key('typeid',@id))]"> -->
       <!-- first process all subproofs (let-in) -->
-      <xsl:for-each select="*[@id = (//InnerTypes/TYPE/@of)]">
+      <xsl:for-each select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]">
        <m:apply>
         <m:csymbol>let</m:csymbol>
         <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position())"/></xsl:with-param></xsl:call-template></m:ci>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index ba45ee0dc..426e16129 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -98,7 +98,8 @@
       <xsl:apply-templates mode="pure" select="*[6]"/>
      </m:apply>
     </xsl:when>
-    <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
+    <!-- <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1"> -->
+    <xsl:when test="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 1">
      <m:apply helm:xref="{@id}">
       <m:csymbol>thread</m:csymbol>
       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
@@ -106,7 +107,7 @@
        <m:csymbol>app</m:csymbol>
        <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
       </m:apply>
-      <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
+      <xsl:apply-templates mode="thread" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
      </m:apply>
     </xsl:when>
     <xsl:otherwise>
@@ -122,7 +123,8 @@
 
 <xsl:template match="*" mode="copy-of-no-prop">
  <xsl:choose>
-  <xsl:when test="@id = //InnerTypes/TYPE/@of">
+  <!-- <xsl:when test="@id = //InnerTypes/TYPE/@of"> -->
+  <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
    <m:ci>previous</m:ci>
   </xsl:when>
   <xsl:otherwise>
@@ -166,7 +168,8 @@
          <m:csymbol>app</m:csymbol>
          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
         </m:apply>
-        <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
+        <!-- <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/> -->
+        <xsl:apply-templates mode="thread" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
        </m:apply>
    </xsl:when>
    <xsl:otherwise>
@@ -187,8 +190,12 @@
       <xsl:variable name="id" select="@id"/>
       <xsl:variable name="ideqp" select="*[7]/@id"/>
       <xsl:variable name="idsubp" select="*[5]/@id"/>
+<!--
       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
+-->
+      <xsl:variable name="leteqp" select="boolean(*[7][@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
+      <xsl:variable name="letsubp" select="boolean(*[5][@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
       <m:apply helm:xref="{@id}">
        <m:csymbol>rewrite_and_apply</m:csymbol>
        <m:apply>