+++ /dev/null
-<?xml version="1.0"?>
-
-<!-- Copyright (C) 2000, HELM Team -->
-<!-- -->
-<!-- This file is part of HELM, an Hypertextual, Electronic -->
-<!-- Library of Mathematics, developed at the Computer Science -->
-<!-- Department, University of Bologna, Italy. -->
-<!-- -->
-<!-- HELM is free software; you can redistribute it and/or -->
-<!-- modify it under the terms of the GNU General Public License -->
-<!-- as published by the Free Software Foundation; either version 2 -->
-<!-- of the License, or (at your option) any later version. -->
-<!-- -->
-<!-- HELM is distributed in the hope that it will be useful, -->
-<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
-<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
-<!-- GNU General Public License for more details. -->
-<!-- -->
-<!-- You should have received a copy of the GNU General Public License -->
-<!-- along with HELM; if not, write to the Free Software -->
-<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
-<!-- MA 02111-1307, USA. -->
-<!-- -->
-<!-- For details, see the HELM World-Wide-Web page, -->
-<!-- http://cs.unibo.it/helm/. -->
-
-<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, Guidi -->
-<!--***********************************************************************-->
-
-<xsl:param name="CICURI" select="''"/>
-<xsl:param name="type" select="'standalone'"/>
-<xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
-<xsl:param name="explode_tactics" select="false()"/>
-
-<xsl:include href="nuprl_html_arith.xsl"/>
-<xsl:include href="nuprl_html_basic.xsl"/>
-
-<xsl:variable name="showcast" select="0"/>
-
-<!--***********************************************************************-->
-<!-- HTML Head and Body -->
-<!--***********************************************************************-->
-
-<!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
-
-<!-- document needs method="xml" and searches locally for the dtd if -->
-<!-- doctype-system is specified (the dtd must exist locally for parsing). -->
-<!-- For having output html must be media-type="html" and for having the -->
-<!-- correct <br /> you must specify at least the remote dtd by means of -->
-<!-- doctype-public -->
-
-<!-- Commentd out by Zack, a try-fix for NuPRL stylesheets with OCaml UWOBO -->
-<!--
-<xsl:output
- method="xml"
- encoding="iso-8859-1"
- media-type="text/html"
- doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
--->
-<xsl:output
- method="html"
- encoding="iso-8859-1"
- media-type="text/html"
- doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
-
-<xsl:variable name="framewidth" select="55"/>
-
-<!--forall-->
- <xsl:variable name="forall">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">"</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∀</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--lambda-->
- <xsl:variable name="lambda">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">l</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">λ</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--prod-->
- <xsl:variable name="prod">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Õ</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Π</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--arrow-->
- <xsl:variable name="arrow">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">®</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">→</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--RightArrow-->
- <xsl:variable name="RightArrow">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Þ</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">⇒</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--product-->
- <xsl:variable name="product">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">S</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Σ</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--member-->
- <xsl:variable name="member">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Î</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∈</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--member-->
- <xsl:variable name="intersection">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Ç</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∩</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--integers-->
- <xsl:variable name="integers">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">I</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Ι</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--naturalnumbers-->
- <xsl:variable name="naturalnumbers">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">N</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Ν</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--implies-->
- <xsl:variable name="implies">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">î</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">⇒</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-<!--exists-->
- <xsl:variable name="NUPRLexists">
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">$</xsl:when>
- <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∃</xsl:when>
- <xsl:otherwise>???</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
-
-
-
-<xsl:template name="mksymbol">
- <xsl:param name="symbol" select="'???'"/>
- <xsl:param name="color" select="'blue'"/>
- <xsl:param name="size" select="''"/>
-
- <xsl:choose>
- <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
- <FONT FACE="symbol" SIZE="{$size}" COLOR="{$color}">
- <xsl:value-of select="$symbol"/>
- </FONT>
- </xsl:when>
- <xsl:otherwise>
- <FONT COLOR="{$color}">
- <xsl:value-of select="$symbol"/>
- </FONT>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template match="/">
- <xsl:param name="current_indent" select="0"/>
- <xsl:choose>
- <xsl:when test="$type = 'standalone'">
- <html>
- <head>
- <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
- <style> A { text-decoration: none } </style>
- <script>
- <xsl:text disable-output-escaping="yes">
- <![CDATA[
- function Hide(which){
- if (!document.getElementById)
- return
- which.style.display="none"
- }
-
- function Show(which){
- if (!document.getElementById)
- return
- which.style.display=""
- }
-
- document.to_be_deleted = new Array();
- ]]>
- </xsl:text>
- </script>
- </head>
- <body bgcolor="white">
- <xsl:attribute name="onLoad">
- if(document.getElementById)
- for(var i=0;i<document.to_be_deleted.length;i++)
- Hide(document.getElementById(document.to_be_deleted[i]));
- </xsl:attribute>
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="0"/>
- </xsl:apply-templates>
- </body>
- </html>
- </xsl:when>
- <xsl:otherwise>
- <to_be_embedded>
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="0"/>
- </xsl:apply-templates>
- </to_be_embedded>
- </xsl:otherwise>
- </xsl:choose>
-</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>
-
-
-
-<!--*********************************************************************-->
-<!-- INLINE MODE -->
-<!--*********************************************************************-->
-
-<!-- href -->
-<xsl:template mode="inline" match="m:ci">
- <xsl:choose>
- <xsl:when test="boolean(@definitionURL)">
- <a href="{@definitionURL}">
- <xsl:apply-templates/>
- </a>
- </xsl:when>
- <xsl:otherwise>
- <xsl:value-of select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- CSYMBOL -->
-
-<xsl:template match="m:apply[m:csymbol]" mode="inline">
- <xsl:param name="current_indent" select="0"/>
- <xsl:variable name="name">
- <xsl:value-of select="m:csymbol"/>
- </xsl:variable>
- <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
- <xsl:choose>
-
- <!-- FUNCTION-DIP (PROD) -->
- <xsl:when test="$name='prod'">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$prod"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:if test="m:bvar/m:ci=""">
- <xsl:text>""</xsl:text>
- </xsl:if>
- <xsl:text>:</xsl:text>
- <!--<xsl:if test="m:bvar/m:type/*[*]">
- <xsl:text>( </xsl:text>
- </xsl:if>-->
- <xsl:apply-templates select="m:bvar/m:type"/>
- <!--<xsl:if test="m:bvar/m:type/*[*]">
- <xsl:text>) </xsl:text>
- </xsl:if>-->
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[position()=3]"/>
- </xsl:when>
-
- <!-- ARROW --> <!-- FUNCTION (IND) -->
- <xsl:when test="$name='arrow'">
- <xsl:text>(</xsl:text>
- <xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$arrow"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[position()=3]"/>
- <xsl:text>)</xsl:text>
- </xsl:when>
-
-
- <!-- FORALL -->
- <xsl:when test="$name='forall'">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$forall"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:text>:</xsl:text>
- <!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
- <xsl:text>(</xsl:text>
- </xsl:if>-->
- <xsl:apply-templates select="m:bvar/m:type"/>
- <!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
- <xsl:text>)</xsl:text>
- </xsl:if>-->
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[position()=3]"/>
- </xsl:when>
-
-
- <!-- PRODUCT -->
- <xsl:when test="$name='product'">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$product"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[position()=3]"/>
- </xsl:when>
-
- <!-- PROD_IND -->
- <xsl:when test="$name='product_ind'">
- <FONT color="blue">
- <xsl:text>( </xsl:text>
- </FONT>
- <xsl:apply-templates mode="inline" select="m:type"/>
- <FONT color="blue" size="+2">
- <xsl:text>x</xsl:text>
- </FONT>
- <xsl:apply-templates mode="inline" select="*[position()=3]"/>
- <FONT color="blue">
- <xsl:text> )</xsl:text>
- </FONT>
-
- </xsl:when>
-
- <!-- PAIR -->
- <xsl:when test="$name='pair'">
- <FONT color="blue" size="+1">
- <xsl:text><</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[2]"/>
- <xsl:text>, </xsl:text>
- <xsl:apply-templates select="*[3]"/>
- <FONT color="blue" size="+1">
- <xsl:text>></xsl:text>
- </FONT>
- </xsl:when>
-
- <!-- UNION -->
- <xsl:when test="$name='union'">
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue" size="+2">
- <xsl:text>+</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]"/>
- </xsl:when>
-
- <!-- INL -->
- <xsl:when test="$name='inl'">
- <FONT color="blue">
- <xsl:text>inl (</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue">
- <xsl:text> )</xsl:text>
- </FONT>
- </xsl:when>
-
- <!-- INR -->
- <xsl:when test="$name='inr'">
- <FONT color="blue" size="+1">
- <xsl:text>inr (</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue" size="+1">
- <xsl:text> )</xsl:text>
- </FONT>
- </xsl:when>
-
- <!-- EQUAL -->
- <xsl:when test="$name='equal'">
- <xsl:apply-templates select="*[position()=3]"/>
- <FONT color="blue" size="+1">
- <xsl:text> = </xsl:text>
- </FONT>
- <xsl:apply-templates select="*[position()=4]"/>
- <xsl:text> </xsl:text>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$member"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:text> </xsl:text>
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
-
- <!-- CONS -->
- <xsl:when test="$name='cons'">
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue">
- <xsl:text>::</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]"/>
- </xsl:when>
-
- <!-- REC -->
-
- <xsl:when test="$name='rec'">
- <FONT color="blue">
- <xsl:text>rectype</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue">
- <xsl:text>=</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]"/>
- </xsl:when>
-
-
- <!-- SET -->
-
- <xsl:when test="$name='t_set'">
- <FONT color="blue">
- <xsl:text>{</xsl:text>
- </FONT>
- <xsl:choose>
- <xsl:when test="m:bvar/m:ci">
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <FONT color="blue">
- <xsl:text>:</xsl:text>
- </FONT>
- <xsl:apply-templates select="m:bvar/m:type"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates select="m:bvar/m:type"/>
- </xsl:otherwise>
- </xsl:choose>
- <FONT color="blue">
- <xsl:text>|</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]"/>
- <FONT color="blue">
- <xsl:text>}</xsl:text>
- </FONT>
-
- </xsl:when>
-
- <!-- ISECT -->
-
- <xsl:when test="$name='isect'">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$intersection"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <FONT color="blue">
- <xsl:text>:</xsl:text>
- </FONT>
- <xsl:apply-templates select="m:bvar/m:type"/>
- <FONT color="blue">
- <xsl:text>.</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]"/>
- </xsl:when>
-
- <!-- QUOTIENT -->
-
- <xsl:when test="$name='quotient'">
- <xsl:apply-templates select="m:bvar[1]"/>
- <xsl:text>,</xsl:text>
- <xsl:apply-templates select="m:bvar[2]"/>
- <FONT color="blue">
- <xsl:text>:</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue">
- <xsl:text>//</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[5]"/>
- </xsl:when>
-
- <!-- SO_LAMBDA -->
- <xsl:when test="$name='so_lambda'">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$lambda"/>
- <xsl:with-param name="color" select="'red'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:apply[1]/*[2]"/>
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[3]"/>
- </xsl:when>
-
-
- <!-- SO_APPLY -->
-
- <xsl:when test="$name='so_apply'">
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[position()=2]"/>
- <xsl:for-each select="*[position()>2]">
- <xsl:text> </xsl:text>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:for-each>
- <xsl:text>)</xsl:text>
- </xsl:when>
- <!-- APP -->
- <xsl:when test="$name='app'">
- <!-- NuPRL rendering -->
- <xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <xsl:if test="count(*) > 2">
- <xsl:text>(</xsl:text>
- <xsl:for-each select="*[position() > 2]">
- <xsl:apply-templates select="." mode="inline"/>
- <xsl:if test="not(position() = last())">
- <xsl:text>,</xsl:text>
- </xsl:if>
- </xsl:for-each>
- <xsl:text>)</xsl:text>
- </xsl:if>
- <!-- CIC rendering
- <xsl:text>(</xsl:text>
- <xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <xsl:for-each select="*[position()>2]">
- <xsl:text> </xsl:text>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:for-each>
- <xsl:text>)</xsl:text>
- -->
- </xsl:when>
- <!-- CAST -->
- <xsl:when test="$name='cast'">
- <xsl:text>(</xsl:text>
- <xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <xsl:text>:></xsl:text>
- <xsl:apply-templates mode="inline" select="*[position()=3]"/>
- <xsl:text>)</xsl:text>
- </xsl:when>
- <xsl:when test="$name='Prop'">
- <FONT color="violet">Prop</FONT>
- </xsl:when>
- <xsl:when test="$name='Set'">
- <FONT color="violet">Set</FONT>
- </xsl:when>
- <xsl:when test="$name='Type'">
- <FONT color="violet">Type</FONT>
- </xsl:when>
-
- <!-- MUTCASE -->
- <xsl:when test="$name='mutcase'">
- <xsl:text><</xsl:text>
- <xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <xsl:text>> </xsl:text>
- <FONT color="red">CASE </FONT>
- <xsl:apply-templates mode="inline" select="*[position()=3]"/>
- <FONT color="red"> OF </FONT>
-<xsl:for-each select="m:piecewise/m:piece">
-<!--<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 mode="inline" select="./*[2]"/>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$RightArrow"/>
- <xsl:with-param name="color" select="'green'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:apply-templates mode="inline"
- select="./*[1]"/>
- </xsl:for-each>
- </xsl:when>
-
- <!-- FIX -->
- <xsl:when test="$name='fix'">
- <FONT color="red">FIX</FONT>
- <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 mode="inline" select="m:type"/>
- <xsl:text>:=</xsl:text>
- <xsl:apply-templates mode="inline"
- 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:when>
-
- <!-- COFIX -->
- <xsl:when test="$name='cofix'">
- <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 mode="inline" select="m:type"/>
- <xsl:text>:=</xsl:text>
- <xsl:apply-templates mode="inline"
- 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:when>
-
- <!-- proof -->
- <xsl:when test="$name='proof' or $name='side_proof'">
- <xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <FONT color="red"> proves </FONT>
- <xsl:apply-templates mode="inline" select="*[position()=3]"/>
- </xsl:when>
- <xsl:when test="$name='letin1'">
- <xsl:text>letin1 (inline error)</xsl:text>
- </xsl:when>
- <!-- false_ind -->
- <xsl:when test="$name='false_ind'">
- <xsl:apply-templates mode="inline" select="*[3]"/>
- <FONT color="red">Contradiction.</FONT>
- </xsl:when>
- <!-- and_ind -->
- <xsl:when test="$name='and_ind'">
- <FONT color="red">From </FONT>
- <xsl:apply-templates select="*[2]"/>
- <FONT color="red"> we get</FONT>
- (
- <xsl:apply-templates select="*[3]"/>
- ) 
- <xsl:apply-templates mode="inline" select="*[4]"/>
- <FONT color="red"> and </FONT>
- (
- <xsl:apply-templates select="*[5]"/>
- ) 
- <xsl:apply-templates mode="inline" select="*[6]"/>
- ;
- <FONT color="red"> hence </FONT>
- <xsl:apply-templates mode="inline" select="*[7]"/>
- </xsl:when>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:lambda">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$lambda"/>
- <xsl:with-param name="color" select="'red'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
-
- <!-- IN NuPrl non e' specificato il tipo -->
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:if test="m:bvar[m:mtype]">
- <xsl:text>:</xsl:text>
- <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
- </xsl:if>
- <xsl:text>.</xsl:text>
- <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-</xsl:template>
-
-<!--*********************************************************************-->
-<!-- NORMAL MODE -->
-<!--*********************************************************************-->
-
-<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:variable name="uri">
- <xsl:value-of select="*[1]/@definitionURL"/>
- </xsl:variable>
-
-
- <xsl:choose>
-
- <!-- FUNCTION-DIP (PROD) -->
- <xsl:when test="$name='prod'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$prod"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:if test="m:bvar/m:ci=""">
- <xsl:text>""</xsl:text>
- </xsl:if>
- <xsl:text>:</xsl:text>
- <!--<xsl:if test="m:bvar/m:type/*[*]">
- <xsl:text>( </xsl:text>
- </xsl:if>-->
- <xsl:apply-templates select="m:bvar/m:type">
- <xsl:with-param name="current_indent"
- select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
- </xsl:apply-templates>
- <!--<xsl:if test="m:bvar/m:type/*[*]">
- <xsl:text>) </xsl:text>
- </xsl:if>-->
- <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>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- ARROW --> <!-- FUNCTION IND -->
- <xsl:when test="$name='arrow'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:text>arrow</xsl:text>
- <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:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$arrow"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <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:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:when>
-
- <!-- TYPE_OF -->
- <xsl:when test="$name='type_of'">
- <xsl:value-of select="*[2]"/>
- <xsl:text>:</xsl:text>
- <xsl:if test="count(*[3]/*) > 1">
- <xsl:text>(</xsl:text>
- </xsl:if>
- <xsl:apply-templates select="*[3]"/>
- <xsl:if test="count(*[3]/*) > 1">
- <xsl:text>)</xsl:text>
- </xsl:if>
- </xsl:when>
-
- <!-- AXIOM -->
- <xsl:when test="$name='Ax'">
- <FONT color="blue">
- <xsl:text>Ax</xsl:text>
- </FONT>
- </xsl:when>
-
- <!-- VOID -->
- <xsl:when test="$name='void'">
- <FONT color="blue">
- <xsl:text>Void</xsl:text>
- </FONT>
- </xsl:when>
-
- <!-- ATOM -->
- <xsl:when test="$name='atom'">
- <FONT color="blue">
- <xsl:text>Atom</xsl:text>
- </FONT>
- </xsl:when>
-
-
-
- <!-- FORALL -->
- <xsl:when test="$name='forall'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <!-- Π -->
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$forall"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates select="m:bvar/m:type">
- <xsl:with-param name="current_indent"
- select="$current_indent + 5 + 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>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- PRODUCT -->
- <xsl:when test="$name='product'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$product"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates select="m:bvar/m:type">
- <xsl:with-param name="current_indent"
- select="$current_indent + 5 + 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>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- PROD_IND -->
- <xsl:when test="$name='product_ind'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <FONT color="blue">
- <xsl:text>( </xsl:text>
- </FONT>
- <xsl:apply-templates select="m:type">
- <xsl:with-param name="current_indent"
- select="$current_indent + 5 + 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>
- <FONT color="blue" size="+1">
- <xsl:text> x </xsl:text>
- </FONT>
- <xsl:apply-templates select="*[position()=3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- <FONT color="blue">
- <xsl:text> )</xsl:text>
- </FONT>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- PAIR -->
- <xsl:when test="$name='pair'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <FONT color="blue" size="+1">
- <xsl:text><</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- <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:apply-templates select="*[position()=3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- <FONT color="blue" size="+1">
- <xsl:text>></xsl:text>
- </FONT>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- UNION -->
- <xsl:when test="$name='union'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <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 color="blue" size="+1">
- <xsl:text>+</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[position()=3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- INL -->
- <xsl:when test="$name='inl'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <FONT color="blue">
- <xsl:text>inl (</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- <FONT color="blue">
- <xsl:text> )</xsl:text>
- </FONT>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- INR -->
- <xsl:when test="$name='inr'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <FONT color="blue" size="+1">
- <xsl:text>inr (</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- <FONT color="blue" size="+1">
- <xsl:text> )</xsl:text>
- </FONT>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- PROP -->
- <xsl:when test="$name='prop'">
- <FONT color="blue">
- <xsl:text>P</xsl:text>
- </FONT>
- <FONT color="blue" size="-2">
- <xsl:apply-templates select="m:cn">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- </FONT>
- </xsl:when>
-
- <!-- UNIVERSE -->
- <xsl:when test="$name='universe'">
- <FONT color="blue" size="+1">
- <xsl:text>U</xsl:text>
- </FONT>
- <FONT color="blue" size="2">
- <xsl:apply-templates select="m:cn"/>
- </FONT>
- </xsl:when>
-
- <!-- EQUAL -->
- <xsl:when test="$name='equal'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:apply-templates select="*[position()=3]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="blue" size="+1">
- <xsl:text>= </xsl:text>
- </FONT>
- <xsl:apply-templates select="*[position()=4]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <!-- member -->
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$member"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- TOKEN -->
-
- <xsl:when test="$name='token'">
- <FONT color="blue">
- <xsl:text>"</xsl:text>
- </FONT>
- <xsl:apply-templates select="m:ci"/>
- <FONT color="blue">
- <xsl:text>"</xsl:text>
- </FONT>
- </xsl:when>
-
- <!-- NIL -->
-
- <xsl:when test="$name='nil'">
- <FONT color="blue">
- <xsl:text>[]</xsl:text>
- </FONT>
- </xsl:when>
-
- <!-- CONS -->
- <xsl:when test="$name='cons'">
- <xsl:apply-templates select="*[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 color="blue">
- <xsl:text>::</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- </xsl:when>
-
-
- <!-- REC -->
-
- <xsl:when test="$name='rec'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <FONT color="blue">
- <xsl:text>rectype</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[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 color="blue">
- <xsl:text>=</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- SET -->
-
- <xsl:when test="$name='t_set'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <FONT color="blue">
- <xsl:text>{</xsl:text>
- </FONT>
- <xsl:choose>
- <xsl:when test="m:bvar/m:ci">
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <FONT color="blue">
- <xsl:text>:</xsl:text>
- </FONT>
- <xsl:apply-templates select="m:bvar/m:type">
- <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:when>
- <xsl:otherwise>
- <xsl:apply-templates select="m:bvar/m:type">
- <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:otherwise>
- </xsl:choose>
- <FONT color="blue">
- <xsl:text>|</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
-
- <FONT color="blue">
- <xsl:text>}</xsl:text>
- </FONT>
-
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- ISECT -->
-
- <xsl:when test="$name='isect'">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$intersection"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <FONT color="blue">
- <xsl:text>:</xsl:text>
- </FONT>
- <xsl:apply-templates select="m:bvar/m:type">
- <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 color="blue">
- <xsl:text>.</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
-
- </xsl:when>
-
- <!-- QUOTIENT -->
-
- <xsl:when test="$name='quotient'">
- <xsl:apply-templates select="m:bvar[1]"/>
- <xsl:text>,</xsl:text>
- <xsl:apply-templates select="m:bvar[2]"/>
- <FONT color="blue">
- <xsl:text>:</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[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 color="blue">
- <xsl:text>//</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[5]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
-
- </xsl:when>
-
- <!-- IF_THEN_ELSE -->
- <xsl:when test="$name='if_then_else'">
- <xsl:choose>
- <xsl:when test="m:where = 'atom_eq'">
- <FONT color="blue">
- <xsl:text>atom_eq (</xsl:text>
- </FONT>
- </xsl:when>
- <xsl:when test="m:where = 'int_eq'">
- <FONT color="blue">
- <xsl:text>int_eq (</xsl:text>
- </FONT>
- </xsl:when>
- <xsl:when test="m:where = 'less'">
- <FONT color="blue">
- <xsl:text>less (</xsl:text>
- </FONT>
- </xsl:when>
- </xsl:choose>
- <xsl:apply-templates select="*[3]"/>
- <xsl:text>; </xsl:text>
- <xsl:apply-templates select="*[4]"/>
- <xsl:text>; </xsl:text>
- <xsl:apply-templates select="*[5]"/>
- <xsl:text>; </xsl:text>
- <xsl:apply-templates select="*[6]"/>
- <FONT color="blue">
- <xsl:text>)</xsl:text>
- </FONT>
- </xsl:when>
-
-
- <!-- SO_LAMBDA -->
- <xsl:when test="$name='so_lambda'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$lambda"/>
- <xsl:with-param name="color" select="'red'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:apply[1]/*[2]"/>
- <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="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
-
- <!-- SO_APPLY -->
-
- <xsl:when test="$name='so_apply'">
- <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:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
-
- <!-- APP -->
- <xsl:when test="$name='app'">
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <!-- NuPRL rendering -->
- <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:if test="count(*) > 2">
- <xsl:text>(</xsl:text>
- <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="." mode="inline"/>
- <xsl:if test="not(position() = last())">
- <xsl:text>,</xsl:text>
- </xsl:if>
- </xsl:for-each>
- <xsl:text>)</xsl:text>
- </xsl:if>
- <!-- CIC rendering
- <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:apply-templates mode="inline" select="."/>
- </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:apply-templates mode="inline" select="."/>
- </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>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
- <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="m:piecewise/m:piece">
- <!-- <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="./*[2]"/>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$RightArrow"/>
- <xsl:with-param name="color" select="'green'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:variable name="body_size">
- <xsl:apply-templates
- select="./*[1]/*[1]" mode="charcount"/>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="$body_size > $framewidth">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent"
- select="$current_indent + 8"/>
- </xsl:call-template>
-<xsl:apply-templates
- select="./*[1]">
- <xsl:with-param name="current_indent"
- select="$current_indent + 8"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates select="./*[1]"
- mode="inline" />
- </xsl:otherwise>
- </xsl:choose>
- </xsl:for-each>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <!-- FIX -->
- <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:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <!-- COFIX -->
- <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:apply-templates mode="inline" select="m:type"/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:when test="$name='let_in'">
- <xsl:text>let </xsl:text>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:text> := </xsl:text>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent+14"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>in </xsl:text>
- <xsl:apply-templates select="*[4]">
- <xsl:with-param name="current_indent" select="$current_indent+5"/>
- </xsl:apply-templates>
- </xsl:when>
-
- <!-- ***************************************** -->
- <!-- *********** PROOF ELEMENTS ************** -->
- <!-- ***************************************** -->
- <!-- PROOF -->
- <xsl:when test="$name='proof'">
- <xsl:variable name="nonce" select="generate-id()"/>
- <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
- <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
- <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
- <span ID="{$freshid1}">
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
-  
- </span>
- <xsl:choose>
- <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
- (preceding-sibling::*[1]/text()='rw_step') or
- (name(..)='m:lambda')">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">we proved </FONT>
- </xsl:when>
- <xsl:otherwise>
- <script>
- if(document.getElementById) {
- document.write('\
- <span ID="{$freshid2}">\
- <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));return (0==1);">Proof of</a>\
- </span>\
- <span ID="{$freshid3}">\
- <br/>\
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>\
- <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we proved</a>\
- </span>\
- ');
- document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
- document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
- document.write(' ');
- } else {
- document.write('\
- <br/>\
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>\
- <FONT color="red">we proved </FONT>\
- ');
- }
- </script>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:apply-templates select="*[position()=3]">
- <xsl:with-param name="current_indent" select="$current_indent + 16"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- side_proof -->
- <xsl:when test="$name='side_proof'">
- <xsl:variable name="nonce" select="generate-id()"/>
- <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
- <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
- <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
- <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
- <span ID="{$freshid1}">
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
-  
- </span>
- <script>
- if(document.getElementById) {
- document.write('\
- <span ID="{$freshid2}">\
- <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));Show(document.getElementById(\'{$freshid4}\'));return (0==1);">Justification</a>\
- </span>\
- <span ID="{$freshid3}">\
- <br/>\
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>\
- <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));Hide(document.getElementById(\'{$freshid4}\'));return (0==1);">we proved</a>\
- </span>\
- ');
- document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
- document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
- document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
- document.write(' ');
- } else {
- document.write('\
- <br/>\
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>\
- <FONT color="red">we proved </FONT>\
- ');
- }
- </script>
- <span ID="{$freshid4}">
- <xsl:apply-templates select="*[position()=3]">
- <xsl:with-param name="current_indent" select="$current_indent + 16"/>
- </xsl:apply-templates>
- </span>
- </xsl:when>
- <!-- eq_chain -->
- <xsl:when test="$name='eq_chain'">
- <FONT color="red">We have the following equality chain:</FONT>
- <xsl:for-each select="*[position() mod 2 = 0]">
- <xsl:variable name="pos" select="position()"/>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 5"/>
- </xsl:call-template>
- <xsl:choose>
- <xsl:when test="$pos=1">
- <xsl:apply-templates select=".">
- <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=".">
- <xsl:with-param name="current_indent" select="$current_indent + 5"/>
- </xsl:apply-templates>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:if test="$pos != last()">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 15"/>
- </xsl:call-template>
- <xsl:apply-templates select="../*[position()=2*$pos +1]">
- <xsl:with-param name="current_indent" select="$current_indent + 15"/>
- </xsl:apply-templates>
- </xsl:if>
- </xsl:for-each>
- </xsl:when>
- <!-- diseq_chain -->
- <xsl:when test="$name='diseq_chain'">
- <FONT color="red">We have the following chain of disequalities:</FONT>
- <xsl:for-each select="*[position() mod 3 = 2]">
- <xsl:variable name="pos" select="position()"/>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 5"/>
- </xsl:call-template>
- <xsl:choose>
- <xsl:when test="$pos=1">
- <xsl:apply-templates select=".">
- <xsl:with-param name="current_indent" select="$current_indent + 5"/>
- </xsl:apply-templates>
- <xsl:text> </xsl:text>
- <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
- <xsl:text> </xsl:text>
- <xsl:apply-templates select=".">
- <xsl:with-param name="current_indent" select="$current_indent + 5"/>
- </xsl:apply-templates>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:if test="$pos != last()">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 15"/>
- </xsl:call-template>
- <xsl:apply-templates select="../*[position()=3*$pos +1]">
- <xsl:with-param name="current_indent" select="$current_indent + 15"/>
- </xsl:apply-templates>
- </xsl:if>
- </xsl:for-each>
- </xsl:when>
- <!-- letin1 -->
- <xsl:when test="$name='letin1'">
- <xsl:apply-templates select="*[position()=2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[position()=3]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- letin -->
- <xsl:when test="$name='letin'">
- <xsl:for-each select="*[position()>1 and last()>position()]">
- <xsl:apply-templates select=".">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- </xsl:for-each>
- <xsl:apply-templates select="*[position()=last()]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- Let -->
- <xsl:when test="$name='let'">
- (
- <xsl:apply-templates select="m:ci"/>
- )
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 7"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- rw_step -->
- <xsl:when test="$name='rw_step'">
- <xsl:choose>
- <xsl:when test="name(*[2])='m:apply'">
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <FONT color="red">Consider </FONT>
- <xsl:apply-templates select="*[2]"/>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:variable name="charlength_first">
- <xsl:apply-templates select="*[3]" mode="root_charcount"/>
- </xsl:variable>
- <xsl:variable name="charlength_second">
- <xsl:apply-templates select="*[4]" mode="root_charcount"/>
- </xsl:variable>
- <xsl:variable name="charlength_side_proof">
- <xsl:apply-templates select="*[5]" mode="root_charcount"/>
- </xsl:variable>
- <xsl:variable name="split1"
- select="($charlength_first + $charlength_second) > $framewidth"/>
- <xsl:variable name="split2"
- select="($charlength_second + $charlength_side_proof) > $framewidth"/>
- <!-- <xsl:value-of select="$current_indent"/> -->
- <!-- <xsl:value-of select="string($charlength_second)"/> -->
- <!-- <xsl:value-of select="$charlength_side_proof"/> -->
- <!-- <xsl:value-of select="$split2"/> -->
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">Rewrite </FONT>
- <xsl:apply-templates mode="inline" select="*[3]"/>
- <xsl:text> </xsl:text>
- <xsl:if test="$split1">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:call-template>
- </xsl:if>
- <FONT color="red">with </FONT>
- <xsl:apply-templates mode="inline" select="*[4]"/>
- <xsl:text> </xsl:text>
- <xsl:if test="$split2">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:call-template>
- </xsl:if>
- <FONT color="red">by </FONT>
- <xsl:apply-templates select="*[5]">
- <xsl:with-param name="current_indent" select="$current_indent+7"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- rewrite and apply -->
- <xsl:when test="$name='rewrite_and_apply'">
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">Then apply it to </FONT>
- <xsl:apply-templates select="*[position()>2]"/>
- </xsl:when>
- <!-- by_induction -->
- <xsl:when test="$name='by_induction'">
- <FONT color="red">We prove </FONT>
- <xsl:apply-templates select="../*[3]">
- <xsl:with-param name="current_indent" select="$current_indent+18"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">by induction on </FONT>
- <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
- <xsl:with-param name="current_indent" select="$current_indent+30"/>
- </xsl:apply-templates>
- <!--
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>The induction property is</xsl:text>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- -->
- <xsl:apply-templates
- select="*[position()>3 and not(position()=last())]">
- <xsl:with-param name="current_indent" select="$current_indent+4"/>
- </xsl:apply-templates>
- <!-- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>End induction</xsl:text> -->
- </xsl:when>
- <!-- inductive_case -->
- <xsl:when test="$name='inductive_case'">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">Case </FONT>
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent +10"/>
- </xsl:apply-templates>
- <xsl:if test="*[3]/*[position()>1]">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent+4"/>
- </xsl:call-template>
- <FONT color="red">By induction hypothesis, we have:</FONT>
- <xsl:for-each select="*[3]/*[position()>1]">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 4"/>
- </xsl:call-template>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="m:ci"/>
- <xsl:text>) </xsl:text>
- <xsl:apply-templates select="m:type">
- <xsl:with-param name="current_indent" select="$current_indent + 8"/>
- </xsl:apply-templates>
- </xsl:for-each>
- </xsl:if>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 4"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[4]">
- <xsl:with-param name="current_indent" select="$current_indent +4"/>
- </xsl:apply-templates>
- <!-- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>End Case</xsl:text> -->
- </xsl:when>
- <!-- case_lhs -->
- <xsl:when test="$name='case_lhs'">
- <xsl:choose>
- <xsl:when test="count(*)=2">
- <xsl:apply-templates mode="inline" select="*[2]"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates mode="inline" select="*[2]"/>
- <xsl:for-each select="m:bvar">
- <xsl:text> </xsl:text>
- <xsl:apply-templates mode="inline" select="*[1]"/>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
- </xsl:for-each>
- <xsl:text>)</xsl:text>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <!-- false_ind -->
- <xsl:when test="$name='false_ind'">
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">Contradiction.</FONT>
- </xsl:when>
- <!-- and_ind -->
- <xsl:when test="$name='and_ind'">
- <xsl:choose>
- <xsl:when test="name(*[2])='m:apply'">
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <FONT color="red">Consider </FONT>
- <xsl:apply-templates select="*[2]"/>
- </xsl:otherwise>
- </xsl:choose>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">In particular, we have</FONT>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- (
- <xsl:apply-templates select="*[3]"/>
- ) 
- <xsl:apply-templates select="*[4]">
- <xsl:with-param name="current_indent" select="$current_indent + 9"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- (
- <xsl:apply-templates select="*[5]"/>
- ) 
- <xsl:apply-templates select="*[6]">
- <xsl:with-param name="current_indent" select="$current_indent + 9"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[7]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- full_or_ind -->
- <xsl:when test="$name='full_or_ind'">
- <xsl:choose>
- <xsl:when test="name(*[2])='m:apply'">
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <FONT color="red">Consider </FONT>
- <xsl:apply-templates select="*[2]"/>
- </xsl:otherwise>
- </xsl:choose>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">We proceed by cases to prove </FONT>
- <xsl:apply-templates select="*[3]"/>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent+4"/>
- </xsl:call-template>
- <FONT color="red">Left: suppose </FONT>
- <xsl:text>(</xsl:text>
- <xsl:value-of select="*[4]/m:bvar/m:ci"/>
- <xsl:text>) </xsl:text>
- <xsl:apply-templates
- select="*[4]/m:bvar/m:type/*[1]"/>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent+15"/>
- </xsl:call-template>
- <xsl:apply-templates
- select="*[4]/*[3]">
- <xsl:with-param name="current_indent" select="$current_indent+15"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent+4"/>
- </xsl:call-template>
- <FONT color="red">Right: suppose </FONT>
- <xsl:text>(</xsl:text>
- <xsl:value-of select="*[5]/m:bvar/m:ci"/>
- <xsl:text>) </xsl:text>
- <xsl:apply-templates
- select="*[5]/m:bvar/m:type/*[1]"/>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent+16"/>
- </xsl:call-template>
- <xsl:apply-templates
- select="*[5]/*[3]">
- <xsl:with-param name="current_indent" select="$current_indent+16"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- or_ind -->
- <xsl:when test="$name='or_ind'">
- <xsl:choose>
- <xsl:when test="name(*[2])='m:apply'">
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <FONT color="red">Consider </FONT>
- <xsl:apply-templates select="*[2]"/>
- </xsl:otherwise>
- </xsl:choose>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">We prove </FONT>
- <xsl:apply-templates select="*[3]"/>
- <FONT color="red"> by cases:</FONT>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- Left: 
- <xsl:apply-templates select="*[4]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- Right: 
- <xsl:apply-templates select="*[5]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <!-- Ex_ind -->
- <xsl:when test="$name='ex_ind'">
- <xsl:choose>
- <xsl:when test="name(*[2])='m:apply'">
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <FONT color="red">Consider </FONT>
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:otherwise>
- </xsl:choose>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <FONT color="red">Let </FONT>
- <xsl:apply-templates mode="inline" select="*[3]"/>
- :
- <xsl:apply-templates mode="inline" select="*[4]"/>
- <FONT color="red"> such that</FONT>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- (
- <xsl:apply-templates mode="inline" select="*[5]"/>
- )
- <xsl:apply-templates select="*[6]">
- <xsl:with-param name="current_indent" select="$current_indent +7"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[7]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- </xsl:choose>
-</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:value-of select="$current_indent"/> -->
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <!-- λ -->
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$lambda"/>
- <xsl:with-param name="color" select="'red'"/>
- <xsl:with-param name="size" select="'+2'"/>
- </xsl:call-template>
- <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 + 4 + 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>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- href -->
-<xsl:template match="m:ci">
- <xsl:choose>
- <xsl:when test="boolean(@definitionURL)">
- <a href="{@definitionURL}">
- <xsl:apply-templates/>
- </a>
- </xsl:when>
- <xsl:otherwise>
- <xsl:value-of select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- CHAR COUNTING -->
-
-<!-- enter this counting mode selecting the root -->
-<xsl:template match="*" mode="root_charcount">
-<xsl:param name="incurrent_length" select="0"/>
- <xsl:choose>
- <xsl:when test="count(*)=0">
- <xsl:value-of select="0"/>
- </xsl:when>
- <xsl:when test="name()='m:ci'">
- <xsl:value-of select="string-length()"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates select="*[1]" mode="charcount">
- <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
- </xsl:apply-templates>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-
- <!-- CASI PARTICOLARI MODE=INLINE -->
-
-<xsl:template mode="inline" match="m:interval">
- <FONT color="blue">
- <xsl:text>[</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[1]"/>
- <xsl:text>, </xsl:text>
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue">
- <xsl:text>]</xsl:text>
- </FONT>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:apply[m:in]">
- <xsl:apply-templates select="*[2]"/>
- <xsl:text> </xsl:text>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$member"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:text> </xsl:text>
- <xsl:apply-templates select="*[3]"/>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:integers">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$integers"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:naturalnumbers">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$naturalnumbers"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:apply[m:implies]">
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[2]"/>
- <xsl:text> </xsl:text>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$implies"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:text> </xsl:text>
- <xsl:apply-templates select="*[3]"/>
- <xsl:text>)</xsl:text>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:apply[m:exists]">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$NUPRLexists"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates select="m:condition/*"/>
-<!-- CSC: old wrong code
- <xsl:if test="count(m:condition/m:apply/*[3]) > 1">
- <xsl:text>(</xsl:text>
- </xsl:if>
- <xsl:apply-templates select="m:condition/m:apply/*[3]"/>
- <xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
- <xsl:text>)</xsl:text>
- </xsl:if>
--->
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[position()=4]"/>
-
-
-</xsl:template>
-<!--
-<xsl:template mode="inline" match="m:apply/*[m:ci][position()=1]">
- <xsl:apply-templates select="*[1]"/>
- <xsl:text>(</xsl:text>
- <xsl:for-each select="*[position()>1 and position()!=last()]">
- <xsl:apply-templates/>
- <xsl:text>, </xsl:text>
- </xsl:for-each>
- <xsl:apply-templates select="*[position()=last()]"/>
- <xsl:text>)</xsl:text>
-</xsl:template>
--->
-<!-- CASI PARTICOLARI NON IN LINE -->
-
-<xsl:template match="m:interval">
- <FONT color="blue">
- <xsl:text>[</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[1]"/>
- <xsl:text>, </xsl:text>
- <xsl:apply-templates select="*[2]"/>
- <FONT color="blue">
- <xsl:text>]</xsl:text>
- </FONT>
-
-
- <!--<xsl:param name="current_indent" select="0"/>
- <xsl:variable name="charlength">
- <xsl:apply-templates select="." mode="charcount"/>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <FONT color="blue">
- <xsl:text>[</xsl:text>
- </FONT>
- <xsl:apply-templates select="*[1]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:text>, </xsl:text>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <FONT color="blue">
- <xsl:text>]</xsl:text>
- </FONT>
- </xsl:when>
- <xsl:otherwise>
- </xsl:otherwise>
- </xsl:choose>-->
-</xsl:template>
-
-<xsl:template match="m:apply[m:in]">
- <xsl:param name="current_indent" select="0"/>
- <xsl:variable name="charlength">
- <xsl:apply-templates select="m:in" mode="charcount"/>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$member"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:text> </xsl:text>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template match="m:integers">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$integers"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
-</xsl:template>
-
-<xsl:template match="m:naturalnumbers">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$naturalnumbers"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
-</xsl:template>
-
-<xsl:template match="m:apply[m:implies]">
- <xsl:param name="current_indent" select="0"/>
- <xsl:variable name="charlength">
- <xsl:apply-templates select="m:implies" mode="charcount"/>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:text>implies</xsl:text>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$implies"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:text> </xsl:text>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:text>)</xsl:text>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template match="m:apply[m:exists]">
- <xsl:param name="current_indent" select="0"/>
- <xsl:variable name="charlength">
- <xsl:apply-templates select="m:implies" mode="charcount"/>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="$charlength > $framewidth">
- <xsl:call-template name="mksymbol">
- <xsl:with-param name="symbol" select="$NUPRLexists"/>
- <xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+0'"/>
- </xsl:call-template>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:text>:</xsl:text>
- <!--<xsl:if test="count(m:condition/m:apply/*[3]) > 1">
- <xsl:text>(</xsl:text>
- </xsl:if>-->
- <xsl:apply-templates select="m:condition/m:apply/*[3]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <!--<xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
- <xsl:text>)</xsl:text>
- </xsl:if>-->
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[position()=4]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="inline" select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!--
-<xsl:template match="m:apply/m:ci">
- <xsl:apply-templates/>
- <xsl:text>(</xsl:text>
- <xsl:for-each select="*[position()>1 and position()!=last()]">
- <xsl:apply-templates/>
- <xsl:text>, </xsl:text>
- </xsl:for-each>
- <xsl:apply-templates select="*[position()=last()]"/>
- <xsl:text>)</xsl:text>
-</xsl:template>
--->
-<!-- enter this mode selecting the first child -->
-
-<xsl:template match="m:ci|m:csymbol|m:implies|m:exists|m:interval|m:in" 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 -->
-<!--***********************************************************************-->
-
-<!-- Rule -->
-
-<xsl:template match="Rule">
-<xsl:param name="current_indent" select="0"/>
-
- <xsl:variable name="char">
- <xsl:value-of select="m:apply"/>
- </xsl:variable>
- <xsl:variable name="length" select="string-length($char)"/>
-
-<p>
-<xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
-<FONT color="red">Rule: </FONT>
-<xsl:choose>
- <xsl:when test="m:ci">
- <FONT color="red">
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </FONT>
- </xsl:when>
- <xsl:otherwise>
- <xsl:choose>
- <xsl:when test="$length > $framewidth">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:variable name="char_rule">
- <xsl:value-of select="m:apply/*[1]"/>
- </xsl:variable>
- <xsl:variable name="length_rule" select="string-length($char_rule)"/>
- <FONT>
- <xsl:apply-templates select="m:apply/*[1]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:if test="count(m:apply/*)>2">
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/>
- </xsl:call-template>
- </xsl:if>
- <FONT color="red">
- <xsl:text> ( </xsl:text>
- </FONT>
- </FONT>
- <xsl:for-each select="m:apply/*[position()!=1]">
- <xsl:if test="position()!=1">
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/>
- </xsl:call-template>
- </xsl:if>
- <xsl:choose>
- <xsl:when test="*[1]='level-exp'">
- <xsl:text>level-exp(</xsl:text>
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:text>)</xsl:text>
- </xsl:when>
- <xsl:when test="m:apply">
- <xsl:apply-templates select=".">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:if test="position()!=last()">
- <xsl:text>, </xsl:text>
- <br/>
- </xsl:if>
- </xsl:for-each>
- <FONT color="red">
- <xsl:text> )</xsl:text>
- </FONT>
-
- </xsl:when>
- <xsl:otherwise>
- <FONT>
- <xsl:apply-templates select="m:apply/*[1]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
-
- <FONT color="red">
- <xsl:text> ( </xsl:text>
- </FONT>
- </FONT>
- <xsl:for-each select="m:apply/*[position()!=1]">
- <xsl:choose>
- <xsl:when test="*[1]='level-exp'">
- <xsl:text>level-exp(</xsl:text>
- <xsl:apply-templates select="*[2]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:text>)</xsl:text>
- </xsl:when>
- <xsl:when test="m:apply">
- <xsl:apply-templates select=".">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
-
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:if test="position()!=last()">
- <xsl:text>, </xsl:text>
- </xsl:if>
- </xsl:for-each>
- <FONT color="red">
- <xsl:text> )</xsl:text>
- </FONT>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:otherwise>
-</xsl:choose>
-</p>
-</xsl:template>
-
-<!-- Sequent -->
-
-<xsl:template match="Sequent">
-<xsl:param name="current_indent" select="0"/>
-<xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
-</xsl:call-template>
-<FONT color="red">Sequent <xsl:value-of select="@id"/></FONT>
-<br/>
-<br/>
-<xsl:for-each select="Decl">
- <xsl:variable name="num" select="position()"/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:value-of select="$num"/>
- <xsl:text>) </xsl:text>
- <xsl:if test="@name">
- <FONT color="green">
- <xsl:value-of select="@name"/>
- <xsl:text>:</xsl:text>
- </FONT>
- </xsl:if>
-
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="$current_indent + 10"/>
- </xsl:apply-templates>
- <!--<xsl:choose>
- <xsl:when test="m:apply">
- <xsl:apply-templates select=".">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:otherwise>
- </xsl:choose>-->
-<br/>
- </xsl:for-each>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
-
- <FONT color="red" size="+1">|- </FONT>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:apply-templates select="Goal/*">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
-</xsl:template>
-
-<!-- NODE -->
-
-<xsl:template match="Node">
- <xsl:param name="current_indent" select="0"/>
-
- <xsl:variable name="nonce" select="generate-id()"/>
- <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
- <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
- <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
- <xsl:variable name="freshid5" select="concat('e',$nonce)"/>
- <br/>
- <xsl:apply-templates select="Sequent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- <xsl:choose>
- <xsl:when test="Rule">
- <xsl:apply-templates select="Rule">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="TacticInstance">
- <br/>
- <br/>
- <span>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>By </xsl:text>
- <xsl:apply-templates select="TacticInstance/@name"/>
- <a style="text-decoration:underline ; color:green" href="{TacticInstance/@uri}">Tactic Details</a>
- <xsl:if test="$explode_tactics">
- <span ID="{$freshid4}">
- <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid4}'));Show(document.getElementById('{$freshid5}'));return (0==1);">Details</a>
- </span>
- </xsl:if>
- </span>
- <xsl:if test="$explode_tactics">
- <div ID="{$freshid5}">
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid4}'));Hide(document.getElementById('{$freshid5}'));return (0==1);">Hide details</a>
- <br/>
- <xsl:apply-templates select="TacticProof">
- <xsl:with-param name="current_indent" select="$current_indent + 5"/>
- </xsl:apply-templates>
- </div>
- </xsl:if>
- <br/><br/>
- </xsl:when>
- </xsl:choose>
- <xsl:if test="count(Node)!=0">
- <xsl:choose>
- <xsl:when test="count(Node)=1">
- <span ID="{$freshid2}">
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoal</a>
- <br/>
- </span>
- </xsl:when>
- <xsl:otherwise>
- <span ID="{$freshid2}">
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoals</a>
- <br/>
- </span>
- </xsl:otherwise>
- </xsl:choose>
- <div ID="{$freshid3}">
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid2}'));Hide(document.getElementById('{$freshid3}'));return (0==1);">Back</a>
- <br/>
- <xsl:apply-templates select="Node">
- <xsl:with-param name="current_indent" select="$current_indent + 5"/>
- </xsl:apply-templates>
- </div>
- <script>
- document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
- </script>
- </xsl:if>
-</xsl:template>
-
-<!-- NuPRLDefinition -->
-
-<xsl:template match="NuPrlDefinition">
- <xsl:apply-templates select="*[1]"/>
- <xsl:text> := </xsl:text>
- <xsl:apply-templates select="*[2]"/>
-</xsl:template>
-
-<!-- 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/Node">
- <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 =<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>
-</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:for-each select="Decl|Def|Hidden">
- <xsl:choose>
- <xsl:when test="name(.)='Decl'">
- <xsl:choose>
- <xsl:when test="@name">
- <xsl:value-of select="@name"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:text>_</xsl:text>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:text> : </xsl:text>
- <xsl:apply-templates select="./*[1]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="name(.)='Def'">
- <xsl:choose>
- <xsl:when test="@name">
- <xsl:value-of select="@name"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:text>_</xsl:text>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:text> := </xsl:text>
- <xsl:apply-templates select="./*[1]">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:text> _ :? _ </xsl:text>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:for-each>
- |- <xsl:value-of select="./@no"/> :
- <xsl:apply-templates select="./Goal/*[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 + 2*string-length(./@name) + 5"/>
- </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>
-<xsl:if test="body">
-<br/>
-BODY = <xsl:apply-templates select="body/*[1]">
- <xsl:with-param name="current_indent" select="$current_indent + 7"/>
- </xsl:apply-templates>
-</xsl:if>
-</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>