Initial revision

[helm.git] / helm / style / proof31-10-00.xsl

diff --git a/helm/style/proof31-10-00.xsl b/helm/style/proof31-10-00.xsl
new file mode 100644 (file)
index 0000000..3c42343
--- /dev/null
+++ b/helm/style/proof31-10-00.xsl
@@ -0,0 +1,210 @@
+<?xml version="1.0"?>
+
+<!--******************************************************************--> 
+<!-- Basic Logic                                                      -->
+<!-- First draft: April 3 2000                                        -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm">
+
+<!--******************************************************************-->
+<!-- Variable containing the absolute path of the CIC file            -->
+<!--******************************************************************-->
+
+<xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>
+
+<!-- ************************* LOGIC *********************************-->
+
+<!-- Proof objects -->
+
+<!-- <xsl:key name="typeid" use="@id" match="TYPE"/> -->
+
+<xsl:template match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
+  <xsl:choose> 
+   <xsl:when test="@id">
+    <xsl:variable name="id" select="@id"/>
+    <xsl:choose>
+     <!-- <xsl:when test="//ALLTYPES and key('typeid',@id)"> -->
+     <xsl:when test="//ALLTYPES/TYPE[@id=$id]">
+     <xsl:choose>
+      <xsl:when test="name()= 'APPLY' and CONST[
+ attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
+       <m:apply helm:xref="{@id}">
+        <m:csymbol>rewrite</m:csymbol>
+        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+        <m:apply>
+         <m:csymbol>rw_step</m:csymbol>
+         <xsl:apply-templates mode="pure" select="*[3]"/>
+         <xsl:apply-templates mode="pure" select="*[6]"/>
+         <xsl:apply-templates mode="pure" select="*[7]"/>
+        </m:apply>
+        <xsl:apply-templates mode="rewrite" select="*[5]"/>
+       </m:apply>
+      </xsl:when>
+      <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
+      <xsl:when test="name()= 'APPLY' and CONST[
+ attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con'] 
+ and count(child::*) = 6">
+       <m:apply helm:xref="{@id}">
+        <m:csymbol>and_ind</m:csymbol>
+        <xsl:apply-templates mode="noannot" select="*[6]"/>
+        <m:ci><xsl:value-of select="*[5]/target/@binder"/></m:ci>
+        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
+        <m:ci><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></m:ci>
+        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
+        <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
+       </m:apply>
+      </xsl:when>
+      <xsl:when test="name()= 'APPLY' and CONST[
+ attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con'] 
+ and count(child::*) = 7">
+       <m:apply helm:xref="{@id}">
+        <m:csymbol>or_ind</m:csymbol>
+        <xsl:apply-templates mode="noannot" select="*[7]"/>
+        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+        <xsl:apply-templates mode="pure" select="*[5]"/>
+        <xsl:apply-templates mode="pure" select="*[6]"/>
+       </m:apply>
+      </xsl:when>
+      <xsl:otherwise>
+       <m:apply helm:xref="{@id}">
+        <m:csymbol>proof</m:csymbol>
+        <xsl:apply-templates select="." mode="pure"/>
+        <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
+        <xsl:apply-templates select="//ALLTYPES/TYPE[@id=$id]" mode="pure"/>
+       </m:apply>
+      </xsl:otherwise>
+     </xsl:choose>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-templates select="." mode="pure"/>
+     </xsl:otherwise>
+    </xsl:choose>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:apply-templates select="." mode="pure"/>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+<xsl:template match="*" mode="rewrite">
+  <xsl:choose>
+   <xsl:when test="name()= 'APPLY' and CONST[
+ attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
+    <xsl:variable name="id" select="@id"/>
+     <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+     <m:apply>
+      <m:csymbol>rw_step</m:csymbol>
+      <xsl:apply-templates mode="pure" select="*[3]"/>
+      <xsl:apply-templates mode="pure" select="*[6]"/>
+      <xsl:apply-templates mode="pure" select="*[7]"/>
+     </m:apply>
+     <xsl:apply-templates mode="rewrite" select="*[5]"/>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:apply-templates mode="noannot" select="."/>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+
+<!-- Basic proof operators -->
+
+<!-- non del tutto soddisfacente, ma .... -->
+<xsl:template match="APPLY[CONST[
+ attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
+    <xsl:choose>
+     <xsl:when test="count(child::*) > 7">
+      <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(//ALLTYPES/TYPE[@id=$ideqp])"/>
+      <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
+      <m:apply helm:xref="{@id}">
+       <m:csymbol>rewrite_and_apply</m:csymbol>
+       <m:apply>
+        <m:csymbol>rw_step</m:csymbol>
+        <xsl:apply-templates mode="pure" select="*[3]"/>
+        <xsl:apply-templates mode="pure" select="*[6]"/>
+        <xsl:choose>
+         <xsl:when test="$leteqp">
+          <xsl:choose>
+           <xsl:when test="$letsubp">
+            <m:ci>
+             <xsl:value-of select="'h2'"/>
+            </m:ci>
+           </xsl:when>
+           <xsl:otherwise>
+            <m:ci>
+             <xsl:value-of select="'h1'"/>
+            </m:ci>
+           </xsl:otherwise>
+          </xsl:choose>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:apply-templates mode="pure" select="*[7]"/>
+         </xsl:otherwise>
+        </xsl:choose>
+       </m:apply>
+      <xsl:choose>
+       <xsl:when test="$letsubp">
+        <m:ci>
+         <xsl:value-of select="'h1'"/>
+        </m:ci>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:apply-templates mode="pure" select="*[5]"/>
+       </xsl:otherwise>
+      </xsl:choose>
+      <xsl:apply-templates mode="flat" select="*[8]">
+       <xsl:with-param name="n">
+        <xsl:value-of select="1+$letsubp+$leteqp"/>
+       </xsl:with-param>
+      </xsl:apply-templates>
+     </m:apply>
+    </xsl:when>
+    <xsl:otherwise>
+     <m:apply helm:xref="{@id}">
+      <m:csymbol>app</m:csymbol>
+      <xsl:apply-templates mode="flat" select="*[1]"/>
+     </m:apply>
+    </xsl:otherwise>
+   </xsl:choose>
+</xsl:template> 
+
+<xsl:template match="APPLY[CONST[
+ attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
+    <xsl:choose>
+     <xsl:when test="count(child::*) > 4">
+      <m:apply helm:xref="{@id}">
+       <m:csymbol>app</m:csymbol>
+       <xsl:apply-templates mode="pure" select="*[1]"/>
+       <m:ci>*</m:ci>
+       <m:ci>*</m:ci>
+       <m:ci>*</m:ci>
+       <xsl:apply-templates mode="flat" select="*[5]"/>
+      </m:apply>
+     </xsl:when>
+     <xsl:otherwise>
+      <m:apply helm:xref="{@id}">
+       <m:csymbol>app</m:csymbol>
+       <xsl:apply-templates mode="flat" select="*[1]"/>
+      </m:apply>
+     </xsl:otherwise>
+    </xsl:choose>
+</xsl:template> 
+
+
+</xsl:stylesheet>
+
+
+
+
+
+