Algebra notation.

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

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 0651f65ec6cdb2224b864010bd8a5025953cbee2..4c207e4820e6d30f0e52a540aab890478536bc31 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -79,7 +79,10 @@
   <xsl:otherwise>
    <xsl:choose>
     <xsl:when test="name()='APPLY'">
-     <xsl:apply-templates select="." mode="letin"/>
+     <!-- This is the case of an applicative expression wich is not
+          a proof but could contains proofs...
+          MODE LETIN OR MODE PURE ??? Big question -->
+     <xsl:apply-templates select="." mode="pure"/>
     </xsl:when>
     <xsl:otherwise>
      <xsl:apply-templates select="." mode="pure"/>
@@ -152,12 +155,55 @@
    </xsl:choose>
 </xsl:template>
 
+<xsl:template mode="eq_transitive" match="*">
+ <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
+ <xsl:choose>
+  <xsl:when test="name()='APPLY'">
+   <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
+   <xsl:variable name="id" select="@id"/>
+   <xsl:choose>
+    <!-- ricordarsi di trattare il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+     <!-- <m:ci>eccomi-3</m:ci> -->
+     <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
+     <xsl:apply-templates mode="noannot" select="*[4]"/>
+     <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:call-template name="generate_side_proof">
+      <xsl:with-param name="proof" select="."/>
+      <xsl:with-param name="show_statement" select="0"/>
+     </xsl:call-template> 
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:call-template name="generate_side_proof">
+    <xsl:with-param name="proof" select="."/>
+    <xsl:with-param name="show_statement" select="0"/>
+   </xsl:call-template>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
 
 <xsl:template mode="proof_transform" match="*">
  <xsl:choose>
   <xsl:when test="name()='APPLY'">
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
+    <!-- Algebra equality (eq_transitive_unfolded) -->
+    <!-- It requires a special mode "eq_transitive"-->
+    <!-- togliere il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>eq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when>
     <!-- EQUALITY -->
     <xsl:when test="CONST[
  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
@@ -434,6 +480,7 @@
 
 <xsl:template name="generate_side_proof">
  <xsl:param name="proof" select="/.."/>
+ <xsl:param name="show_statement" select="1"/>
 <!-- 
  <xsl:variable name="is_simple">
   <xsl:call-template name="is_simple">
@@ -453,7 +500,20 @@
    </xsl:choose>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:apply-templates select="$proof" mode="noannot"/>
+   <xsl:variable name="id" select="@id"/>
+   <m:apply helm:xref="{@id}">
+    <xsl:choose>
+     <xsl:when test="$show_statement = 1">
+      <m:csymbol>proof</m:csymbol>
+     </xsl:when>
+     <xsl:otherwise>
+      <m:csymbol>side_proof</m:csymbol>
+     </xsl:otherwise>
+    </xsl:choose>
+    <xsl:apply-templates mode="proof_transform" select="."/>
+    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+   </m:apply>
+   <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
   </xsl:otherwise>
  </xsl:choose>
 </xsl:template>