--- /dev/null
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!--***********************************************************************-->
+<!-- From MathML content to HTML -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
+<!--***********************************************************************-->
+
+
+<xsl:include href="html_init.xsl"/>
+<xsl:include href="html_set.xsl"/>
+<xsl:include href="html_reals.xsl"/>
+
+
+<!-- <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>-->
+<xsl:variable name="header" select="document('http://localhost:8081/conf')/html_link"/>
+
+<xsl:variable name="showcast" select="0"/>
+
+
+<!--***********************************************************************-->
+<!-- HTML Head and Body -->
+<!--***********************************************************************-->
+
+<xsl:output method="html"/>
+
+<xsl:variable name="framewidth" select="36"/>
+
+<xsl:template match="/">
+ <xsl:param name="current_indent" select="0"/>
+ <html>
+ <head></head>
+ <body>
+ <xsl:apply-templates>
+ <xsl:with-param name="current_indent" select="0"/>
+ </xsl:apply-templates>
+ </body>
+ </html>
+</xsl:template>
+
+<!--***********************************************************************-->
+<!-- Indentation -->
+<!--***********************************************************************-->
+
+<xsl:template name="make_indent">
+ <xsl:param name="current_indent" select="0"/>
+ <xsl:if test="$current_indent > 0">
+ <xsl:text> </xsl:text>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent - 1"/>
+ </xsl:call-template>
+ </xsl:if>
+</xsl:template>
+
+<!-- Syntactic Sugar -->
+
+<xsl:template match="m:type">
+<xsl:param name="current_indent" select="0"/>
+<xsl:apply-templates>
+ <xsl:with-param name="current_indent"
+ select="$current_indent"/>
+</xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="m:condition">
+<xsl:param name="current_indent" select="0"/>
+<xsl:apply-templates>
+ <xsl:with-param name="current_indent"
+ select="$current_indent"/>
+</xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="m:math">
+<xsl:param name="current_indent" select="0"/>
+<xsl:apply-templates>
+ <xsl:with-param name="current_indent"
+ select="$current_indent"/>
+</xsl:apply-templates>
+</xsl:template>
+
+<!-- CSYMBOL -->
+
+<xsl:template match="m:apply[m:csymbol]">
+ <xsl:param name="current_indent" select="0"/>
+ <xsl:param name="width" select="$framewidth"/>
+ <xsl:variable name="name">
+ <xsl:value-of select="m:csymbol"/>
+ </xsl:variable>
+ <xsl:variable name="charlength">
+ <xsl:apply-templates select="m:csymbol" mode="charcount"/>
+ </xsl:variable>
+ <!-- <xsl:value-of select="$current_indent"/> -->
+ <!-- <xsl:value-of select="$charlength"/> -->
+ <xsl:choose>
+ <xsl:when test="$name='prod'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <!-- Π -->
+ <FONT FACE="symbol" SIZE="+2" color="blue">P</FONT>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:bvar/m:type">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+ </xsl:apply-templates><BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <!-- Π -->
+ <FONT FACE="symbol" SIZE="+2" color="blue">P</FONT>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:bvar/m:type"/>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates select="*[position()=3]"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="$name='arrow'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <!-- -> -->
+ <FONT FACE="symbol" SIZE="+2" color="blue">®</FONT>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]"/>
+ <!-- -> -->
+ <FONT FACE="symbol" SIZE="+2" color="blue">®</FONT>
+ <xsl:apply-templates select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="$name='app'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ <xsl:for-each select="*[position()>2]">
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:apply-templates select=".">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ </xsl:for-each>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]"/>
+ <xsl:for-each select="*[position()>2]">
+ <xsl:text> </xsl:text>
+ <xsl:apply-templates select="."/>
+ </xsl:for-each>
+ <xsl:text>)</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="$name='cast'">
+ <xsl:choose>
+ <xsl:when test="$showcast = 1">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates><BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
+ <xsl:text>:></xsl:text>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 3"/>
+ </xsl:apply-templates>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]"/>
+ <xsl:text>:></xsl:text>
+ <xsl:apply-templates select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="$name='Prop'">
+ <xsl:text>Prop</xsl:text>
+ </xsl:when>
+ <xsl:when test="$name='Set'">
+ <xsl:text>Set</xsl:text>
+ </xsl:when>
+ <xsl:when test="$name='Type'">
+ <xsl:text>Type</xsl:text>
+ </xsl:when>
+ <xsl:when test="$name='mutcase'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text><</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ <xsl:text>> </xsl:text>
+ <xsl:text>CASE </xsl:text>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+ </xsl:apply-templates>
+ <xsl:text> OF </xsl:text>
+ <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:choose>
+ <xsl:when test="position() = 1">
+ <xsl:text>  </xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>| </xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="."/>
+ <FONT FACE="symbol" SIZE="+2" color="green">Þ</FONT>
+ <xsl:apply-templates select="following-sibling::*[position()= 1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
+ </xsl:apply-templates>
+ </xsl:for-each>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text><</xsl:text>
+ <xsl:apply-templates select="*[position()=2]"/>
+ <xsl:text>> </xsl:text>
+ <xsl:text>CASE </xsl:text>
+ <xsl:apply-templates select="*[position()=3]"/>
+ <xsl:text> OF </xsl:text>
+ <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+ <xsl:choose>
+ <xsl:when test="not(position() = 1)">
+ <xsl:text> | </xsl:text>
+ </xsl:when>
+ </xsl:choose>
+ <xsl:apply-templates select="."/>
+ <FONT FACE="symbol" SIZE="+2" color="green">Þ</FONT>
+ <xsl:apply-templates select="following-sibling::*[position()= 1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2 + string-length()"/>
+ </xsl:apply-templates>
+ </xsl:for-each>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="$name='fix'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>FIX</xsl:text>
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>{</xsl:text>
+ <xsl:for-each select="m:bvar">
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:type">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 5 + string-length(m:ci)"/>
+ </xsl:apply-templates>
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:text>:=</xsl:text>
+ <xsl:apply-templates select="following-sibling::*[position() = 1]">
+ <xsl:with-param name="current_indent" select="$current_indent +2"/>
+ </xsl:apply-templates>
+ </xsl:for-each>
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:text>}</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>FIX</xsl:text>
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>{</xsl:text>
+ <xsl:for-each select="m:bvar">
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:type"/>
+ <xsl:text>:=</xsl:text>
+ <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+ <xsl:choose>
+ <xsl:when test="position()=last()">
+ <xsl:text>}</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>;</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:for-each>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="$name='cofix'">
+ <xsl:choose>
+ <xsl:when test="($charlength + 10) > $framewidth">
+ <xsl:text>COFIX</xsl:text>
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>{</xsl:text>
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:for-each select="m:bvar">
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:type">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 5 + string-length(m:ci)"/>
+ </xsl:apply-templates>
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:text>:=</xsl:text>
+ <xsl:apply-templates select="following-sibling::*[position() = 1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 3"/>
+ </xsl:apply-templates>
+
+ </xsl:for-each>
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:text>}</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>COFIX</xsl:text>
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>{</xsl:text>
+ <xsl:for-each select="m:bvar">
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:type"/>
+ <xsl:text>:=</xsl:text>
+ <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+ <xsl:choose>
+ <xsl:when test="position()=last()">
+ <xsl:text>}</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>;</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:for-each>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ </xsl:choose>
+ <!-- </m:mrow> -->
+</xsl:template>
+
+<!-- LAMBDA -->
+
+<xsl:template match="m:lambda">
+<xsl:param name="current_indent" select="0"/>
+ <xsl:variable name="charlength">
+ <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
+ <!-- <xsl:apply-templates select="." mode="charcount"/> -->
+ </xsl:variable>
+ <!-- <xsl:value-of select="$charlength"/> -->
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <!-- λ -->
+ <FONT FACE="symbol" SIZE="+2" color="red">l</FONT>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:bvar/m:type">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+ </xsl:apply-templates><BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <!-- λ -->
+ <FONT FACE="symbol" SIZE="+2" color="red">l</FONT>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:bvar/m:type"/>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates select="*[position()=2]"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- href -->
+<xsl:template match="m:ci">
+ <xsl:choose>
+ <xsl:when test="boolean(@definitionURL)">
+<!-- CSC: non bisogna piu' utilizzare la url, bensi' la uri -->
+<!-- <xsl:variable name="url">
+ <xsl:value-of select="concat(string($absPath),
+ @definitionURL)"/>
+ </xsl:variable>-->
+ <a>
+ <xsl:attribute name="href">
+ <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
+ </xsl:attribute>
+ <xsl:apply-templates/>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- COUNTING -->
+
+<xsl:template match="m:ci|m:csymbol" mode="charcount">
+<xsl:param name="incurrent_length" select="0"/>
+ <xsl:choose>
+ <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
+ <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
+ <xsl:choose>
+ <xsl:when test="string($siblength) = """>
+ <xsl:value-of select="$incurrent_length + string-length()"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="number($siblength)"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$incurrent_length + string-length()"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="*" mode="charcount">
+ <xsl:param name="incurrent_length" select="0"/>
+ <xsl:choose>
+ <xsl:when test="count(child::*) = 0">
+ <xsl:value-of select="$incurrent_length"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
+ <xsl:choose>
+ <xsl:when test="$framewidth >= number($childlength)">
+ <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$childlength"/></xsl:apply-templates></xsl:variable>
+ <xsl:choose>
+ <xsl:when test="string($siblength) = """>
+ <xsl:value-of select="number($childlength)"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="number($siblength)"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="number($childlength)"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
+<!--***********************************************************************-->
+<!-- OBJECTS -->
+<!--***********************************************************************-->
+
+<!-- DEFINITION -->
+
+<xsl:template match="Definition">
+<xsl:param name="current_indent" select="0"/>
+<p>
+DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
+TYPE =<BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="type/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:apply-templates><BR/>
+BODY =<BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="body/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!-- AXIOM -->
+
+<xsl:template match="Axiom">
+<xsl:param name="current_indent" select="0"/>
+<p>
+AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
+TYPE = <xsl:apply-templates select="type/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!-- UNFINISHED PROOF -->
+
+<xsl:template match="CurrentProof">
+<xsl:param name="current_indent" select="0"/>
+<p>
+UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
+THESIS: <xsl:apply-templates select="type/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+ </xsl:apply-templates><BR/>
+CONJECTURES:
+ <xsl:for-each select="Conjecture">
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+ </xsl:call-template>
+ <xsl:value-of select="./@no"/> :
+ <xsl:apply-templates select="./*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 11"/>
+ </xsl:apply-templates>
+ </xsl:for-each>
+ <BR/>
+PROOF:
+ <xsl:apply-templates select="body/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+ </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!-- MUTUAL INDUCTIVE DEFINITION -->
+
+<xsl:template match="InductiveDefinition">
+<xsl:param name="current_indent" select="0"/>
+<p>
+ <xsl:for-each select="InductiveType">
+ <xsl:choose>
+ <xsl:when test="position() = 1">
+ <xsl:choose>
+ <xsl:when test="string(./@inductive) = "true"">
+ INDUCTIVE DEFINITION
+ </xsl:when>
+ <xsl:otherwise>
+ COINDUCTIVE DEFINITION
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ AND
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != """><xsl:value-of select="../Params"/></xsl:if>)
+ [
+ <xsl:if test="string(../Param) != """>
+ <xsl:for-each select="../Param">
+ <xsl:value-of select="./@name"/>
+ :
+ <xsl:apply-templates select="*"/>
+ </xsl:for-each>
+ </xsl:if>
+ ] <BR/>
+ OF ARITY
+ <xsl:apply-templates select="./arity/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 9"/>
+ </xsl:apply-templates> <BR/>
+ BUILT FROM:
+ <xsl:for-each select="./Constructor">
+ <BR/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 3"/>
+ </xsl:call-template>
+ <xsl:choose>
+ <xsl:when test="position() = 1">
+ <xsl:text>  </xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>| </xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:value-of select="./@name"/>
+ <xsl:text>: </xsl:text>
+ <xsl:apply-templates select="./*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
+ </xsl:apply-templates>
+ </xsl:for-each>
+ </xsl:for-each>
+</p>
+</xsl:template>
+
+<!-- VARIABLE -->
+
+<xsl:template match="Variable">
+<xsl:param name="current_indent" select="0"/>
+<p>
+VARIABLE <xsl:value-of select="@name"/><BR/>
+TYPE = <xsl:apply-templates select="type/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!--***********************************************************************-->
+<!-- SECTIONS -->
+<!--***********************************************************************-->
+
+<!-- SECTION -->
+
+<xsl:template match="SECTION">
+<xsl:param name="current_indent" select="0"/>
+ <h1>BEGIN OF SECTION</h1>
+ <xsl:apply-templates/>
+ <h1>END OF SECTION</h1>
+</xsl:template>
+
+</xsl:stylesheet>