1. Fixati alcuni problemi di indentazione con le rewrite.

[helm.git] / helm / style / proofs.xsl

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 9fd99d5d1f428bae49b03611cab694aee57154b9..51a0f0d52a5abc6b91eff213af41aeaf01049061 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -169,7 +169,10 @@
        <xsl:apply-templates mode="noannot" select="*[5]"/>
        <xsl:apply-templates mode="pure" select="*[3]"/>
        <xsl:apply-templates mode="pure" select="*[6]"/>
-       <xsl:apply-templates mode="proof_transform" select="*[7]"/>
+       <xsl:call-template name="generate_side_proof">
+        <xsl:with-param name="proof" select="*[7]"/>
+       </xsl:call-template>
+       <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
       </m:apply>
     </xsl:when>
     <!-- EQUALITY with extra-parameters -->
@@ -189,7 +192,10 @@
           <xsl:apply-templates mode="noannot" select="*[5]"/>
           <xsl:apply-templates mode="pure" select="*[3]"/>
           <xsl:apply-templates mode="pure" select="*[6]"/>
-          <xsl:apply-templates mode="pure" select="*[7]"/>
+          <xsl:call-template name="generate_side_proof">
+           <xsl:with-param name="proof" select="*[7]"/>
+           </xsl:call-template>
+          <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
          </m:apply>
          <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
         </m:apply>
@@ -223,7 +229,10 @@
              </m:ci>
              <xsl:apply-templates mode="pure" select="*[3]"/>
              <xsl:apply-templates mode="pure" select="*[6]"/>
-             <xsl:apply-templates mode="pure" select="*[7]"/>
+             <xsl:call-template name="generate_side_proof">
+              <xsl:with-param name="proof" select="*[7]"/>
+             </xsl:call-template>
+             <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
             </m:apply>
             <xsl:apply-templates mode="flat" select="*[8]">
              <xsl:with-param name="n">
@@ -246,8 +255,11 @@
              <m:csymbol>rw_step</m:csymbol>
              <xsl:apply-templates mode="pure" select="*[5]"/>
              <xsl:apply-templates mode="pure" select="*[3]"/>
-             <xsl:apply-templates mode="pure" select="*[6]"/>
-             <xsl:apply-templates mode="pure" select="*[7]"/>
+             <xsl:apply-templates mode="pure" select="*[6]"/>             
+             <xsl:call-template name="generate_side_proof">
+              <xsl:with-param name="proof" select="*[7]"/>
+             </xsl:call-template>
+             <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
             </m:apply>
             <xsl:apply-templates mode="flat" select="*[8]">
              <xsl:with-param name="n">
@@ -397,7 +409,10 @@
        <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
        <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
        <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
-       <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/>
+       <xsl:call-template name="generate_side_proof">
+        <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
+       </xsl:call-template>
+       <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
       </m:apply>
      </xsl:when>
      <xsl:otherwise>
@@ -411,6 +426,38 @@
  </xsl:choose>
 </xsl:template>
 
+<xsl:template name="is_simple">
+ <xsl:param name="proof" select="/.."/>
+ <xsl:value-of select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
+</xsl:template>
+
+<xsl:template name="generate_side_proof">
+ <xsl:param name="proof" select="/.."/>
+<!-- 
+ <xsl:variable name="is_simple">
+  <xsl:call-template name="is_simple">
+   <xsl:with-param name="proof" select="$proof"/>
+  </xsl:call-template>
+ </xsl:variable> -->
+<xsl:variable name="is_simple" select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
+ <xsl:choose>
+  <xsl:when test="$is_simple">
+   <xsl:choose>
+    <xsl:when test="name($proof)='APPLY'">
+     <xsl:apply-templates select="$proof" mode="letin"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:apply-templates select="$proof" mode="pure"/>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-templates select="$proof" mode="noannot"/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 
 <xsl:template match="APPLY" mode="letin">
    <xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>