--- /dev/null
+<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=""">
+ <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=""">
+ <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>
projects / helm.git / blobdiff