X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fnuprl_stylesheets%2Fnuprl_term.xsl;fp=helm%2Fnuprl_stylesheets%2Fnuprl_term.xsl;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=1bd02c93e598a868673dd13836616090755990a6;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git

diff --git a/helm/nuprl_stylesheets/nuprl_term.xsl b/helm/nuprl_stylesheets/nuprl_term.xsl
deleted file mode 100644
index 1bd02c93e..000000000
--- a/helm/nuprl_stylesheets/nuprl_term.xsl
+++ /dev/null
@@ -1,598 +0,0 @@
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
-                              xmlns:m="http://www.w3.org/1998/Math/MathML">
-
-<xsl:include href="nuprl_proof.xsl"/>
-<xsl:include href="nuprl_abstract.xsl"/>
-<xsl:include href="nuprl_rules.xsl"/>
-
-<!-- NuPrl Term -->
-<xsl:template match="var">
-  <m:ci>
-    <xsl:value-of select="@val"/>
-  </m:ci>
-</xsl:template>
-
-
-<xsl:template match="function">
-  <xsl:choose>
-  <xsl:when test="type_of">
-    <xsl:choose>
-    <xsl:when test="type_of/@var=&quot;&quot;">
-    <m:apply>
-      <m:csymbol>arrow</m:csymbol>
-      <xsl:apply-templates select="type_of/*"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:when>
-  <xsl:otherwise>
-    <m:apply>
-      <m:csymbol>prod</m:csymbol>
-      <m:bvar>
-        <m:ci>
-	  <xsl:value-of select="type_of/@var"/>
-	</m:ci>
-        <m:type>
-	  <xsl:apply-templates select="type_of/*"/>
-	</m:type>
-      </m:bvar>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:otherwise>
-  </xsl:choose>
-  </xsl:when>
-  <xsl:otherwise>
-    <m:apply>
-      <m:csymbol>arrow</m:csymbol>
-      <xsl:apply-templates select="*[1]"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:otherwise>
-  </xsl:choose>
-</xsl:template>
-
-
-<xsl:template match="lambda">
-  <m:lambda>
-    <m:bvar>
-      <m:ci>
-        <xsl:value-of select="@binder"/>
-      </m:ci>
-    </m:bvar>
-    <xsl:apply-templates/>
-  </m:lambda>
-</xsl:template>
-
-
-<xsl:template match="apply">
-  <m:apply>
-    <m:csymbol>app</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="product">
-  <m:apply>
-    <xsl:choose>
-      <xsl:when test="type_of">
-        <xsl:choose>
-        <xsl:when test="type_of/@var=&quot;&quot;">
-          <m:csymbol>product_ind</m:csymbol>
-          <m:type>
-            <xsl:apply-templates select="type_of/*"/>
-          </m:type>
-        </xsl:when>
-        <xsl:otherwise>
-          <m:csymbol>product</m:csymbol>
-          <m:bvar>
-            <m:ci>
-	      <xsl:value-of select="type_of/@var"/>
-	    </m:ci>
-          <m:type>
-	    <xsl:apply-templates select="type_of/*"/>
-	  </m:type>
-          </m:bvar>
-        </xsl:otherwise>
-        </xsl:choose>
-      </xsl:when>
-      <xsl:otherwise>
-        <m:csymbol>product_ind</m:csymbol>
-	<m:type>
-          <xsl:apply-templates select="*[1]"/>
-        </m:type>
-      </xsl:otherwise>
-    </xsl:choose>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="pair">
-  <m:apply>
-    <m:csymbol>pair</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="spread">
-  <m:apply>
-  <m:csymbol>mutcase</m:csymbol>
-  <m:csymbol>NONE</m:csymbol>
-  <xsl:apply-templates select="*[1]"/>
-  <m:piecewise>
-    <m:piece>
-      <xsl:apply-templates select="*[4]"/>
-      <m:apply>
-        <m:csymbol>pair</m:csymbol>
-        <xsl:apply-templates select="binder[1]"/>
-        <xsl:apply-templates select="binder[2]"/>
-      </m:apply>
-    </m:piece>
-  </m:piecewise>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="union">
-  <m:apply>
-    <m:csymbol>union</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="inl">
-  <m:apply>
-    <m:csymbol>inl</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="inr">
-  <m:apply>
-    <m:csymbol>inr</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="decide">
-  <m:apply>
-    <m:csymbol>mutcase</m:csymbol>
-    <m:csymbol>NONE</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <m:piecewise>
-    <m:piece>
-      <xsl:apply-templates select="*[3]"/>
-      <m:apply>
-        <m:csymbol>inl</m:csymbol>
-        <xsl:apply-templates select="binder[1]"/>
-      </m:apply>
-    </m:piece>
-    <m:piece>
-      <xsl:apply-templates select="*[5]"/>
-      <m:apply>
-        <m:csymbol>inr</m:csymbol>
-        <xsl:apply-templates select="binder[2]"/>
-      </m:apply>
-    </m:piece>
-    </m:piecewise>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="universe">
-  <m:apply>
-    <m:csymbol>universe</m:csymbol>
-    <m:cn>
-      <xsl:value-of select="@level"/>
-    </m:cn>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="equal">
-  <m:apply>
-    <m:csymbol>equal</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-    <xsl:apply-templates select="*[3]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="axiom">
-  <m:apply>
-    <m:csymbol>Ax</m:csymbol>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="void">
-  <m:apply>
-    <m:csymbol>void</m:csymbol>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="any">
-  <m:apply>
-    <m:csymbol>mutcase</m:csymbol>
-    <m:csymbol>NONE</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="atom">
-  <m:apply>
-    <m:csymbol>atom</m:csymbol>  
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="token">
-  <m:apply>
-    <m:csymbol>token</m:csymbol>
-    <m:ci>
-      <xsl:value-of select="@val"/>
-    </m:ci>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="atom_eq">
-  <m:apply>
-    <m:csymbol>if_then_else</m:csymbol>
-    <m:where>atom_eq</m:where>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-    <xsl:apply-templates select="*[3]"/>
-    <xsl:apply-templates select="*[4]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="int">
-  <m:integers/>
-</xsl:template>
-
-
-<xsl:template match="natural_number">
-  <m:cn>
-    <xsl:value-of select="@val"/>
-  </m:cn>
-</xsl:template>
-
-
-<xsl:template match="minus">
-  <m:apply>
-    <m:minus/>
-    <xsl:apply-templates select="*[1]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="add">
-  <m:apply>
-    <m:plus/>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="subtract">
-  <m:apply>
-    <m:minus/>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="multiply">
-  <m:apply>
-    <m:times/>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="divide">
-  <m:apply>
-    <m:divide/>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="remainder">
-  <m:apply>
-    <m:rem/>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="int_eq">
-  <m:apply>
-    <m:csymbol>if_then_else</m:csymbol>
-    <m:where>int_eq</m:where>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-    <xsl:apply-templates select="*[3]"/>
-    <xsl:apply-templates select="*[4]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="less">
-  <m:apply>
-    <m:csymbol>if_then_else</m:csymbol>
-    <m:where>less</m:where>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-    <xsl:apply-templates select="*[3]"/>
-    <xsl:apply-templates select="*[4]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="ind">
-  <m:apply>
-    <m:csymbol>by_induction</m:csymbol>
-    <m:ci>ind</m:ci>
-    <m:csymbol>NONE</m:csymbol>
-    <m:apply>   <!-- CASO BASE -->
-      <m:csymbol>inductive_case</m:csymbol>
-      <m:apply>
-        <m:csymbol>case_lhs</m:csymbol>
-	<m:ci>0</m:ci>
-      </m:apply>
-      <m:apply>
-        <m:csymbol>induction_hypothesis</m:csymbol>
-      </m:apply>
-      <xsl:apply-templates select="*[5]"/>
-    </m:apply>
-	
-    <m:apply> <!--CASO INDUTTIVO PER I NUMERI POSITIVI-->
-      <m:csymbol>inductive_case</m:csymbol>
-      <m:apply>
-        <m:csymbol>case_lhs</m:csymbol>
-	<m:ci>succ</m:ci>
-	<m:bvar>
-          <xsl:apply-templates select="*[6]"/> <!-- u -->
-	  <m:type>int</m:type>
-	</m:bvar>
-      </m:apply>
-      <m:apply>
-        <m:csymbol>induction_hypothesis</m:csymbol>
-        <xsl:apply-templates select="*[7]"/> <!-- v  -->
-      </m:apply>
-      <xsl:apply-templates select="*[8]"/> <!-- t -->
-    </m:apply>
-
-    <m:apply> <!--CASO INDUTTIVO PER I NUMERI NEGATIVI-->
-      <m:csymbol>inductive_case</m:csymbol>
-      <m:apply>
-        <m:csymbol>case_lhs</m:csymbol>
-	<m:ci>pred</m:ci>
-	<m:bvar>
-          <xsl:apply-templates select="*[2]"/> <!-- x -->
-	  <m:type>int</m:type>
-	</m:bvar>
-      </m:apply>
-      <m:apply>
-        <m:csymbol>induction_hypothesis</m:csymbol>
-	<xsl:apply-templates select="*[3]"/> <!-- y -->
-      </m:apply>
-      <xsl:apply-templates select="*[4]"/>
-    </m:apply>
-    <m:apply> 
-      <m:csymbol>extra_args</m:csymbol>
-      <xsl:apply-templates select="*[1]"/>  <!-- a -->
-    </m:apply> 
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="less_than">
-  <m:apply>
-    <m:lt/>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="list">
-  <m:ci>list</m:ci>
-</xsl:template>
-
-
-<xsl:template match="nil">
-  <m:apply>
-    <m:csymbol>nil</m:csymbol> 
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="cons">
-  <m:apply>
-    <m:csymbol>cons</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="list_ind">
-  <m:apply>
-    <m:csymbol>by_induction</m:csymbol>
-    <m:ci>list_ind</m:ci>
-    <m:csymbol>NONE</m:csymbol>
-    <m:apply>
-      <m:csymbol>inductive_case</m:csymbol>
-      <m:apply>
-        <m:csymbol>case_lhs</m:csymbol>
-	<m:ci>nil</m:ci>
-      </m:apply>
-      <m:apply>
-        <m:csymbol>induction_hypothesis</m:csymbol>
-      </m:apply>
-      <xsl:apply-templates select="*[2]"/> <!-- base -->
-    </m:apply>
-    <m:apply>
-      <m:csymbol>inductive_case</m:csymbol>
-      <m:apply>
-        <m:csymbol>case_lhs</m:csymbol>
-	<m:ci>cons</m:ci>
-	<m:bvar>
-	  <xsl:apply-templates select="*[3]"/> <!-- x -->
-	  <m:type>?</m:type>
-        </m:bvar>
-        <m:bvar>
-	<xsl:apply-templates select="*[4]"/> <!-- l -->
-          <m:type>?</m:type>
-	</m:bvar>
-      </m:apply>
-      <m:apply>
-        <m:csymbol>induction_hypothesis</m:csymbol>
-        <xsl:apply-templates select="*[5]"/> <!-- Fxl -->
-      </m:apply>
-      <xsl:apply-templates select="*[6]"/> <!-- t -->
-    </m:apply>
-    <m:apply>
-      <m:csymbol>extra_args</m:csymbol>
-      <xsl:apply-templates select="*[1]"/> <!-- s -->
-    </m:apply>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="rec">
-  <m:apply>
-    <m:csymbol>rec</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="rec_ind">
-  <m:apply>
-    <m:csymbol>app</m:csymbol>
-    <m:apply>
-      <m:csymbol>fix</m:csymbol>
-      <m:ci>
-        <xsl:apply-templates select="*[2]"/>
-      </m:ci>
-      <m:bvar>
-        <m:ci>
-          <xsl:apply-templates select="*[2]"/>
-        </m:ci>
-        <m:type>?</m:type>
-      </m:bvar>
-      <m:lambda>
-        <m:bvar>
-         <xsl:apply-templates select="*[3]"/>
-        </m:bvar>
-        <xsl:apply-templates select="*[4]"/>
-      </m:lambda>
-    </m:apply>
-    <xsl:apply-templates select="*[1]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="set">
-  <m:apply>
-    <m:csymbol>t_set</m:csymbol>
-    <m:bvar>
-      <xsl:choose>
-      <xsl:when test="type_of">
-        <m:ci>
-          <xsl:value-of select="type_of/@var"/>
-        </m:ci>
-        <m:type>
-          <xsl:apply-templates select="type_of/*"/>
-        </m:type>
-      </xsl:when>
-      <xsl:otherwise>
-        <m:type>
-          <xsl:apply-templates select="*[1]"/>
-        </m:type>
-      </xsl:otherwise>
-      </xsl:choose>
-    </m:bvar>
-    <xsl:apply-templates select="*[2]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="isect">
-  <m:apply>
-    <m:csymbol>isect</m:csymbol>
-    <m:bvar>
-      <m:ci>
-        <xsl:value-of select="type_of/@var"/>
-      </m:ci>	
-      <m:type>
-        <xsl:apply-templates select="type_of/*"/>
-      </m:type>
-    </m:bvar>
-    <xsl:apply-templates select="*[1]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="quotient">
-  <m:apply>
-    <m:csymbol>quotient</m:csymbol>
-    <xsl:apply-templates select="*[1]"/>
-    <m:bvar>
-      <xsl:value-of select="binder[1]/@var"/>
-    </m:bvar>
-    <m:bvar>
-      <xsl:value-of select="binder[2]/@var"/>
-    </m:bvar>
-    <xsl:apply-templates select="*[4]"/>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="type_of">
-  <m:apply>
-    <m:csymbol>type_of</m:csymbol>
-    <m:ci>
-      <xsl:value-of select="@var"/>
-    </m:ci>
-    <xsl:apply-templates select="*[1]"/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="prop">
-  <m:apply>
-    <m:csymbol>prop</m:csymbol>
-    <m:cn>
-      <xsl:value-of select="@level"/>
-    </m:cn>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="binder">
-  <m:ci>
-    <xsl:value-of select="@var"/>
-  </m:ci>
-</xsl:template>
-
-</xsl:stylesheet>