Conversion rules are now correctly handled also for atoms.

The only residual problem is that some proofs + side-proofs
where the proof is an atom with different inner-types are
rendered as a proof with two sub-proofs which is innatural.

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 1d619260a2dbe6bd22fa5c64d5e14f57b4666081..f61cbe6d90d1ea9fece3bf22847b6a25ab8a357f 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -39,10 +39,39 @@
 <!-- Proof objects -->
 
 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
+<xsl:key name="typeid" use="@of" match="TYPE"/>
 
 <!-- ALL this elements does not have inner type -->
-<xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
-<xsl:apply-templates select="." mode="pure"/>
+<xsl:template match="PROD|SORT|MUTIND" mode="noannot">
+ <xsl:apply-templates select="." mode="pure"/>
+</xsl:template>
+
+<!-- Atomic elements that have an inner type iff the expected type -->
+<!-- is different from the synthesized type.                       -->
+<xsl:template match="REL|VAR|META|CONST|MUTCONSTRUCT" mode="noannot">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+  <xsl:for-each select="$InnerTypes">
+   <xsl:if test="key('typeid',$id)/*">
+    <xsl:text>yes</xsl:text>
+   </xsl:if>
+  </xsl:for-each>
+ </xsl:variable>
+ <xsl:choose>
+  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
+   <m:apply helm:xref="{@id}">
+    <m:csymbol>proof</m:csymbol>
+    <xsl:apply-templates mode="proof_transform" select="."/>
+    <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
+    <xsl:for-each select="$InnerTypes">
+     <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
+    </xsl:for-each>
+   </m:apply>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-templates select="." mode="pure"/>
+  </xsl:otherwise>
+ </xsl:choose>
 </xsl:template>
 
 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
@@ -50,12 +79,21 @@
 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
 <xsl:template match="LAMBDA" mode="noannot">
  <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+  <xsl:for-each select="$InnerTypes">
+   <xsl:if test="key('typeid',$id)/*">
+    <xsl:text>yes</xsl:text>
+   </xsl:if>
+  </xsl:for-each>
+ </xsl:variable>
  <xsl:choose>
-  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and name(../..) != 'LAMBDA'">
+  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
    <m:apply helm:xref="{@id}">
     <m:csymbol>proof</m:csymbol>
     <xsl:apply-templates mode="proof_transform" select="."/>
-    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+    <xsl:for-each select="$InnerTypes">
+     <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
+    </xsl:for-each>
    </m:apply>
   </xsl:when>
   <xsl:otherwise>
@@ -65,7 +103,7 @@
 </xsl:template>
 
 <!-- ALL these elements have inner type -->
-<xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="LETIN|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  <xsl:variable name="id" select="@id"/>
  <xsl:choose>
   <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
@@ -73,7 +111,9 @@
     <m:csymbol>proof</m:csymbol>
     <xsl:apply-templates mode="proof_transform" select="."/>
     <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
-    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+    <xsl:for-each select="$InnerTypes">
+     <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
+    </xsl:for-each>
    </m:apply>
   </xsl:when>
   <xsl:otherwise>
@@ -93,7 +133,7 @@
 </xsl:template>
 
 <!-- si presuppone che il tipo induttivo non sia mutuamente 
-     induttivo. Bisognerebbe andare a vedere l'utlimo parametro
+     induttivo. Bisognerebbe andare a vedere l'ultimo parametro
      del presunto "principio di induzione", tirare fuori il tipo induttivo
      e vedere se il suo nome coincide con il prefisso di _ind. 
      Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
@@ -596,8 +636,9 @@
         <m:apply helm:xref="{@id}">
          <m:csymbol>full_or_ind</m:csymbol>
          <xsl:apply-templates mode="noannot" select="*[7]"/>
-         <xsl:apply-templates mode="pure" 
-              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
+         <xsl:for-each select="$InnerTypes">
+          <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+         </xsl:for-each>
          <m:apply>
           <m:csymbol>left_case</m:csymbol>
           <m:bvar>
@@ -628,8 +669,9 @@
         <m:apply helm:xref="{@id}">
          <m:csymbol>or_ind</m:csymbol>
          <xsl:apply-templates mode="noannot" select="*[7]"/>
-         <xsl:apply-templates mode="pure" 
-              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
+         <xsl:for-each select="$InnerTypes">
+          <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+         </xsl:for-each>
          <xsl:apply-templates mode="pure" select="*[5]"/>
          <xsl:apply-templates mode="pure" select="*[6]"/>
         </m:apply>
@@ -749,23 +791,53 @@
      </xsl:otherwise>
     </xsl:choose>
     <xsl:apply-templates mode="proof_transform" select="$proof"/>
-    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$proof/@id]/*"/>
+    <xsl:for-each select="$InnerTypes">
+     <xsl:apply-templates mode="pure" select="key('typeid',$proof/@id)/*"/>
+    </xsl:for-each>
    </m:apply>
    <!-- <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')])"/>
+   <xsl:variable name="no_subproofs">
+    <xsl:variable name="stars">
+     <xsl:for-each select="*[@sort='Prop']">
+      <xsl:variable name="id" select="@id"/>
+      <xsl:variable name="innertype_available">
+       <xsl:for-each select="$InnerTypes">
+        <xsl:if test="key('typeid',$id)/*">
+         <xsl:text>yes</xsl:text>
+        </xsl:if>
+       </xsl:for-each>
+      </xsl:variable>
+      <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
+       <!-- We generate one star for each subproof -->
+       <xsl:text>*</xsl:text>
+      </xsl:if>
+     </xsl:for-each>
+    </xsl:variable>
+    <xsl:value-of select="string-length($stars)"/>
+   </xsl:variable>
    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
    <xsl:choose>
     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
      <m:apply helm:xref="{@id}">
       <m:csymbol>letin1</m:csymbol>
-      <xsl:apply-templates mode="noannot" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
+      <xsl:for-each select="*[@sort='Prop']">
+       <xsl:variable name="id" select="@id"/>
+       <xsl:variable name="innertype_available">
+        <xsl:for-each select="$InnerTypes">
+         <xsl:if test="key('typeid',$id)/*">
+          <xsl:text>yes</xsl:text>
+         </xsl:if>
+        </xsl:for-each>
+       </xsl:variable>
+       <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
+        <xsl:apply-templates mode="noannot" select="."/>
+       </xsl:if>
+      </xsl:for-each>
       <!-- now re-process the application -->
       <m:apply helm:xref="{@id}">
        <m:csymbol>app</m:csymbol>
@@ -807,12 +879,22 @@
 <xsl:template name="gen_let">
  <xsl:param name="init_pos" select="0"/>
  <xsl:param name="from" select="0"/>
-      <xsl:for-each select="*[position()>$from and @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()+$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
-        <xsl:apply-templates mode="noannot" select="."/>
-       </m:apply>
+      <xsl:for-each select="*[position()>$from and @sort='Prop']">
+       <xsl:variable name="id" select="@id"/>
+       <xsl:variable name="innertype_available">
+        <xsl:for-each select="$InnerTypes">
+         <xsl:if test="key('typeid',$id)/*">
+          <xsl:text>yes</xsl:text>
+         </xsl:if>
+        </xsl:for-each>
+       </xsl:variable>
+       <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
+        <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()+$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
+         <xsl:apply-templates mode="noannot" select="."/>
+        </m:apply>
+       </xsl:if>
       </xsl:for-each>
 </xsl:template>
 
@@ -829,8 +911,16 @@
 </xsl:template>
 
 <xsl:template match="*" mode="previous">
+ <xsl:variable name="innertype_available">
+  <xsl:variable name="id" select="@id"/>
+  <xsl:for-each select="$InnerTypes">
+   <xsl:if test="key('typeid',$id)/*">
+    <xsl:text>yes</xsl:text>
+   </xsl:if>
+  </xsl:for-each>
+ </xsl:variable>
  <xsl:choose>
-  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
+  <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
    <m:ci>previous</m:ci>
   </xsl:when>
   <xsl:otherwise>
@@ -852,8 +942,15 @@
 <xsl:template match="*" mode="flat">
  <xsl:param name="n" select="1"/>
  <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+  <xsl:for-each select="$InnerTypes">
+   <xsl:if test="key('typeid',$id)/*">
+    <xsl:text>yes</xsl:text>
+   </xsl:if>
+  </xsl:for-each>
+ </xsl:variable>
  <xsl:choose>
-  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
+  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
    <m:ci>
     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
    </m:ci>