helm/style/content_to_html.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  28                               xmlns:m="http://www.w3.org/1998/Math/MathML">
  29
  30 <!--***********************************************************************-->
  31 <!-- From MathML content to HTML                                           -->
  32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
  33 <!--***********************************************************************-->
  34
  35 <xsl:include href="html_init.xsl"/>
  36 <xsl:include href="html_set.xsl"/>
  37 <xsl:include href="html_reals.xsl"/>
  38
  39 <xsl:variable name="showcast" select="0"/>
  40
  41 <!--***********************************************************************-->
  42 <!-- HTML Head and Body                                                    -->
  43 <!--***********************************************************************-->
  44
  45 <!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
  46
  47 <!-- document needs method="xml" and searches locally for the dtd if        -->
  48 <!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
  49 <!-- For having output html must be media-type="html" and for having the    -->
  50 <!-- correct <br /> you must specify at least the remote dtd by means of    -->
  51 <!-- doctype-public                                                         -->
  52 <xsl:output
  53         method="xml"
  54         encoding="iso-8859-1"
  55         media-type="text/html"
  56         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
  57
  58 <xsl:variable name="framewidth" select="36"/>
  59
  60 <xsl:template match="/">
  61  <xsl:param name="current_indent" select="0"/>
  62                <html>
  63                 <head>
  64                  <style>
  65                  A { text-decoration: none }
  66                  </style>
  67                 </head>
  68                 <body bgcolor="white">
  69                 <xsl:apply-templates>
  70                  <xsl:with-param name="current_indent" select="0"/>
  71                 </xsl:apply-templates>
  72                 </body>
  73                </html>
  74 </xsl:template>
  75
  76 <!--***********************************************************************-->
  77 <!-- Indentation                                                           -->
  78 <!--***********************************************************************-->
  79
  80 <xsl:template name="make_indent">
  81  <xsl:param name="current_indent" select="0"/>
  82   <xsl:if test="$current_indent > 0">
  83    <xsl:text>&#x00a0;</xsl:text>
  84    <xsl:call-template name="make_indent">
  85     <xsl:with-param name="current_indent" select="$current_indent - 1"/>
  86    </xsl:call-template>
  87   </xsl:if>
  88 </xsl:template>
  89
  90 <!-- Syntactic Sugar -->
  91 <xsl:template match="m:type">
  92 <xsl:param name="current_indent" select="0"/>
  93 <xsl:apply-templates>
  94  <xsl:with-param name="current_indent"
  95            select="$current_indent"/>
  96 </xsl:apply-templates>
  97 </xsl:template>
  98
  99 <xsl:template match="m:condition">
 100 <xsl:param name="current_indent" select="0"/>
 101 <xsl:apply-templates>
 102  <xsl:with-param name="current_indent"
 103            select="$current_indent"/>
 104 </xsl:apply-templates>
 105 </xsl:template>
 106
 107 <xsl:template match="m:math">
 108 <xsl:param name="current_indent" select="0"/>
 109 <xsl:apply-templates>
 110  <xsl:with-param name="current_indent"
 111            select="$current_indent"/>
 112 </xsl:apply-templates>
 113 </xsl:template>
 114
 115 <!--*********************************************************************-->
 116 <!--                         INLINE MODE                                 -->
 117 <!--*********************************************************************-->
 118
 119 <!-- href -->
 120 <xsl:template mode="inline" match="m:ci">
 121  <xsl:choose>
 122   <xsl:when test="boolean(@definitionURL)">
 123    <a href="{@definitionURL}">
 124    <xsl:apply-templates/>
 125    </a>
 126   </xsl:when>
 127   <xsl:otherwise>
 128    <xsl:value-of select="."/>
 129   </xsl:otherwise>
 130  </xsl:choose>
 131 </xsl:template>
 132
 133 <!-- CSYMBOL -->
 134
 135 <xsl:template match="m:apply[m:csymbol]" mode="inline">
 136    <xsl:variable name="name">
 137     <xsl:value-of select="m:csymbol"/>
 138    </xsl:variable>
 139    <xsl:choose>
 140     <!-- FORALL -->
 141     <xsl:when test="$name='forall'">
 142      <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
 143      <xsl:apply-templates select="m:bvar/m:ci"/>
 144      <xsl:text>:</xsl:text>
 145      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 146      <xsl:text>.</xsl:text>
 147      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 148     </xsl:when>
 149     <xsl:when test="$name='prod'">
 150      <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
 151      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
 152      <xsl:text>:</xsl:text>
 153      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 154      <xsl:text>.</xsl:text>
 155      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 156     </xsl:when>
 157     <!-- ARROW -->
 158     <xsl:when test="$name='arrow'">
 159      <xsl:text>(</xsl:text>
 160      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 161      <FONT color="blue" FACE="symbol">
 162       <xsl:text>&#x00ae;</xsl:text>
 163      </FONT>
 164      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 165      <xsl:text>)</xsl:text>
 166     </xsl:when>
 167     <!-- APP -->
 168     <xsl:when test="$name='app'">
 169      <xsl:text>(</xsl:text>
 170      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 171      <xsl:for-each select="*[position()>2]">
 172       <xsl:text>&#x00A0;</xsl:text>
 173       <xsl:apply-templates mode="inline" select="."/>
 174      </xsl:for-each>
 175      <xsl:text>)</xsl:text>
 176     </xsl:when>
 177     <!-- CAST -->
 178     <xsl:when test="$name='cast'">
 179      <xsl:text>(</xsl:text>
 180      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 181      <xsl:text>:></xsl:text>
 182      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 183      <xsl:text>)</xsl:text>
 184     </xsl:when>
 185     <xsl:when test="$name='Prop'">
 186      <FONT color="violet">Prop</FONT>
 187     </xsl:when>
 188     <xsl:when test="$name='Set'">
 189      <FONT color="violet">Set</FONT>
 190     </xsl:when>
 191     <xsl:when test="$name='Type'">
 192      <FONT color="violet">Type</FONT>
 193     </xsl:when>
 194     <!-- MUTCASE -->
 195     <xsl:when test="$name='mutcase'">
 196      <xsl:text>&lt;</xsl:text>
 197      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 198      <xsl:text>&gt; </xsl:text>
 199      <FONT color="red">CASE </FONT>
 200      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 201      <FONT color="red"> OF </FONT>
 202      <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 203       <xsl:choose>
 204        <xsl:when test="not(position() = 1)">
 205         <xsl:text> | </xsl:text>
 206        </xsl:when>
 207       </xsl:choose>
 208       <xsl:apply-templates mode="inline" select="."/>
 209       <FONT FACE="Symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
 210       <xsl:apply-templates mode="inline"
 211            select="following-sibling::*[position()= 1]"/>
 212      </xsl:for-each>
 213     </xsl:when>
 214     <!-- FIX -->
 215     <xsl:when test="$name='fix'">
 216      <FONT color="red">FIX</FONT>
 217      <xsl:value-of select="m:ci"/>
 218      <xsl:text>{</xsl:text>
 219      <xsl:for-each select="m:bvar">
 220       <xsl:value-of select="m:ci"/>
 221       <xsl:text>:</xsl:text>
 222       <xsl:apply-templates mode="inline" select="m:type"/>
 223       <xsl:text>:=</xsl:text>
 224       <xsl:apply-templates mode="inline"
 225              select="following-sibling::*[position() = 1]"/>
 226       <xsl:choose>
 227        <xsl:when test="position()=last()">
 228         <xsl:text>}</xsl:text>
 229        </xsl:when>
 230        <xsl:otherwise>
 231         <xsl:text>;</xsl:text>
 232        </xsl:otherwise>
 233       </xsl:choose>
 234      </xsl:for-each>
 235     </xsl:when>
 236     <!-- COFIX -->
 237     <xsl:when test="$name='cofix'">
 238      <xsl:text>COFIX</xsl:text>
 239      <xsl:value-of select="m:ci"/>
 240      <xsl:text>{</xsl:text>
 241      <xsl:for-each select="m:bvar">
 242       <xsl:value-of select="m:ci"/>
 243       <xsl:text>:</xsl:text>
 244       <xsl:apply-templates mode="inline" select="m:type"/>
 245       <xsl:text>:=</xsl:text>
 246       <xsl:apply-templates mode="inline"
 247           select="following-sibling::*[position() = 1]"/>
 248       <xsl:choose>
 249        <xsl:when test="position()=last()">
 250         <xsl:text>}</xsl:text>
 251        </xsl:when>
 252        <xsl:otherwise>
 253         <xsl:text>;</xsl:text>
 254        </xsl:otherwise>
 255       </xsl:choose>
 256      </xsl:for-each>
 257     </xsl:when>
 258     <!-- proof -->
 259     <xsl:when test="$name='proof'">
 260        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 261        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
 262        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 263     </xsl:when>
 264     <!-- and_ind -->
 265     <xsl:when test="$name='and_ind'">
 266      <FONT color="red">From&#x00a0;</FONT>
 267      <xsl:apply-templates select="*[2]"/>
 268      <FONT color="red">&#x00a0;we get</FONT>
 269      (
 270      <xsl:apply-templates select="*[3]"/>
 271      )&#x00a0;
 272      <xsl:apply-templates mode="inline" select="*[4]"/>
 273      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
 274      (
 275      <xsl:apply-templates select="*[5]"/>
 276      )&#x00a0;
 277      <xsl:apply-templates mode="inline" select="*[6]"/>
 278      ;
 279      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
 280      <xsl:apply-templates mode="inline" select="*[7]"/>
 281     </xsl:when>
 282    </xsl:choose>
 283 </xsl:template>
 284
 285 <xsl:template mode="inline" match="m:lambda">
 286       <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
 287       <xsl:apply-templates select="m:bvar/m:ci"/>
 288       <xsl:text>:</xsl:text>
 289       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 290       <xsl:text>.</xsl:text>
 291       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 292 </xsl:template>
 293
 294 <!--*********************************************************************-->
 295 <!--                       COUNTING MODE                                 -->
 296 <!--*********************************************************************-->
 297
 298 <xsl:template match="m:apply[m:csymbol]">
 299   <xsl:param name="current_indent" select="0"/>
 300   <xsl:param name="width" select="$framewidth"/>
 301   <xsl:variable name="name">
 302    <xsl:value-of select="m:csymbol"/>
 303   </xsl:variable>
 304   <xsl:variable name="charlength">
 305    <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 306   </xsl:variable>
 307      <!-- <xsl:value-of select="$current_indent"/> -->
 308      <!-- <xsl:value-of select="$charlength"/> -->
 309      <xsl:choose>
 310      <!-- FORALL -->
 311       <xsl:when test="$name='forall'">
 312        <xsl:choose>
 313        <xsl:when test="$charlength > $framewidth">
 314          <!-- &#x03a0; -->
 315          <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
 316          <xsl:apply-templates select="m:bvar/m:ci"/>
 317          <xsl:text>:</xsl:text>
 318          <xsl:apply-templates select="m:bvar/m:type">
 319           <xsl:with-param name="current_indent"
 320            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 321          </xsl:apply-templates>
 322          <br/>
 323          <xsl:call-template name="make_indent">
 324           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 325          </xsl:call-template>
 326          <xsl:text>.</xsl:text>
 327          <xsl:apply-templates select="*[position()=3]">
 328           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 329          </xsl:apply-templates>
 330        </xsl:when>
 331        <xsl:otherwise>
 332         <xsl:apply-templates mode="inline" select="."/>
 333        </xsl:otherwise>
 334        </xsl:choose>
 335       </xsl:when>
 336       <!-- PROD -->
 337       <xsl:when test="$name='prod'">
 338        <xsl:choose>
 339        <xsl:when test="$charlength > $framewidth">
 340          <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
 341          <xsl:apply-templates select="m:bvar/m:ci"/>
 342          <xsl:text>:</xsl:text>
 343          <xsl:apply-templates select="m:bvar/m:type">
 344           <xsl:with-param name="current_indent"
 345            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 346          </xsl:apply-templates><br/>
 347          <xsl:call-template name="make_indent">
 348           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 349          </xsl:call-template>
 350          <xsl:text>.</xsl:text>
 351          <xsl:apply-templates select="*[position()=3]">
 352           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 353          </xsl:apply-templates>
 354        </xsl:when>
 355        <xsl:otherwise>
 356         <xsl:apply-templates mode="inline" select="."/>
 357        </xsl:otherwise>
 358        </xsl:choose>
 359       </xsl:when>
 360       <!-- ARROW -->
 361       <xsl:when test="$name='arrow'">
 362        <xsl:choose>
 363        <xsl:when test="$charlength > $framewidth">
 364        <xsl:text>(</xsl:text>
 365        <xsl:apply-templates select="*[position()=2]">
 366         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 367        </xsl:apply-templates>
 368        <br/>
 369        <xsl:call-template name="make_indent">
 370         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 371        </xsl:call-template>
 372        <!-- -> -->
 373        <FONT color="blue" FACE="symbol">
 374         <xsl:text>&#x00ae;</xsl:text>
 375        </FONT>
 376        <xsl:apply-templates select="*[position()=3]">
 377         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 378        </xsl:apply-templates>
 379        <xsl:text>)</xsl:text>
 380        </xsl:when>
 381        <xsl:otherwise>
 382         <xsl:apply-templates mode="inline" select="."/>
 383        </xsl:otherwise>
 384        </xsl:choose>
 385       </xsl:when>
 386       <!-- APP -->
 387       <xsl:when test="$name='app'">
 388        <xsl:choose>
 389        <xsl:when test="$charlength  > $framewidth">
 390         <xsl:text>(</xsl:text>
 391         <xsl:apply-templates select="*[position()=2]">
 392          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 393         </xsl:apply-templates>
 394          <xsl:for-each select="*[position()>2]">
 395           <br/>
 396            <xsl:call-template name="make_indent">
 397             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 398            </xsl:call-template>
 399             <xsl:apply-templates select=".">
 400              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 401             </xsl:apply-templates>
 402          </xsl:for-each>
 403          <xsl:text>)</xsl:text>
 404        </xsl:when>
 405        <xsl:otherwise>
 406         <xsl:apply-templates mode="inline" select="."/>
 407        </xsl:otherwise>
 408        </xsl:choose>
 409       </xsl:when>
 410       <xsl:when test="$name='cast'">
 411        <xsl:choose>
 412         <xsl:when test="$showcast = 1">
 413          <xsl:choose>
 414           <xsl:when test="$charlength > $framewidth">
 415            <xsl:text>(</xsl:text>
 416            <xsl:apply-templates select="*[position()=2]">
 417             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 418            </xsl:apply-templates><br/>
 419            <xsl:call-template name="make_indent">
 420             <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
 421            <xsl:text>:></xsl:text>
 422            <xsl:apply-templates select="*[position()=3]">
 423             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 424            </xsl:apply-templates>
 425            <xsl:text>)</xsl:text>
 426           </xsl:when>
 427           <xsl:otherwise>
 428            <xsl:apply-templates mode="inline" select="."/>
 429           </xsl:otherwise>
 430          </xsl:choose>
 431         </xsl:when>
 432         <xsl:otherwise>
 433          <xsl:apply-templates select="*[position()=2]">
 434           <xsl:with-param name="current_indent" select="$current_indent"/>
 435          </xsl:apply-templates>
 436         </xsl:otherwise>
 437        </xsl:choose>
 438       </xsl:when>
 439       <xsl:when test="$name='Prop'">
 440        <xsl:text>Prop</xsl:text>
 441       </xsl:when>
 442       <xsl:when test="$name='Set'">
 443        <xsl:text>Set</xsl:text>
 444       </xsl:when>
 445       <xsl:when test="$name='Type'">
 446        <xsl:text>Type</xsl:text>
 447       </xsl:when>
 448       <xsl:when test="$name='mutcase'">
 449        <xsl:choose>
 450        <xsl:when test="$charlength > $framewidth">
 451          <xsl:text>&lt;</xsl:text>
 452          <xsl:apply-templates select="*[position()=2]">
 453           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 454          </xsl:apply-templates>
 455          <xsl:text>&gt; </xsl:text>
 456          <xsl:text>CASE </xsl:text>
 457          <xsl:apply-templates select="*[position()=3]">
 458           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 459          </xsl:apply-templates>
 460          <xsl:text> OF </xsl:text>
 461          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 462          <br/>
 463          <xsl:call-template name="make_indent">
 464             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 465          </xsl:call-template>
 466             <xsl:choose>
 467             <xsl:when test="position() = 1">
 468              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 469             </xsl:when>
 470             <xsl:otherwise>
 471              <xsl:text>| </xsl:text>
 472             </xsl:otherwise>
 473             </xsl:choose>
 474             <xsl:apply-templates select="."/>
 475             <FONT FACE="Symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
 476             <xsl:apply-templates select="following-sibling::*[position()= 1]">
 477              <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
 478             </xsl:apply-templates>
 479          </xsl:for-each>
 480        </xsl:when>
 481        <xsl:otherwise>
 482         <xsl:apply-templates mode="inline" select="."/>
 483        </xsl:otherwise>
 484        </xsl:choose>
 485       </xsl:when>
 486       <!-- FIX -->
 487       <xsl:when test="$name='fix'">
 488        <xsl:choose>
 489        <xsl:when test="$charlength  > $framewidth">
 490             <xsl:text>FIX</xsl:text>
 491             <xsl:value-of select="m:ci"/>
 492             <xsl:text>{</xsl:text>
 493             <xsl:for-each select="m:bvar">
 494               <br/>
 495               <xsl:call-template name="make_indent">
 496                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 497               </xsl:call-template>
 498               <xsl:value-of select="m:ci"/>
 499               <xsl:text>:</xsl:text>
 500               <xsl:apply-templates select="m:type">
 501                <xsl:with-param name="current_indent"
 502                     select="$current_indent + 5 + string-length(m:ci)"/>
 503                </xsl:apply-templates>
 504               <br/>
 505               <xsl:call-template name="make_indent">
 506                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 507               </xsl:call-template>
 508               <xsl:text>:=</xsl:text>
 509               <xsl:apply-templates select="following-sibling::*[position() = 1]">
 510                <xsl:with-param name="current_indent" select="$current_indent +2"/>
 511               </xsl:apply-templates>
 512             </xsl:for-each>
 513              <br/>
 514               <xsl:call-template name="make_indent">
 515                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 516               </xsl:call-template>
 517            <xsl:text>}</xsl:text>
 518        </xsl:when>
 519        <xsl:otherwise>
 520         <xsl:apply-templates mode="inline" select="."/>
 521        </xsl:otherwise>
 522        </xsl:choose>
 523       </xsl:when>
 524       <!-- COFIX -->
 525       <xsl:when test="$name='cofix'">
 526        <xsl:choose>
 527        <xsl:when test="($charlength + 10) > $framewidth">
 528             <xsl:text>COFIX</xsl:text>
 529             <xsl:value-of select="m:ci"/>
 530             <xsl:text>{</xsl:text>
 531             <br/>
 532             <xsl:call-template name="make_indent">
 533              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 534             </xsl:call-template>
 535             <xsl:for-each select="m:bvar">
 536                 <xsl:value-of select="m:ci"/>
 537                 <xsl:text>:</xsl:text>
 538                 <xsl:apply-templates select="m:type">
 539                  <xsl:with-param name="current_indent"
 540                     select="$current_indent + 5 + string-length(m:ci)"/>
 541                 </xsl:apply-templates>
 542                 <br/>
 543                 <xsl:call-template name="make_indent">
 544                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 545                 </xsl:call-template>
 546                 <xsl:text>:=</xsl:text>
 547                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
 548                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 549                 </xsl:apply-templates>
 550
 551             </xsl:for-each>
 552             <br/>
 553               <xsl:call-template name="make_indent">
 554                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 555               </xsl:call-template>
 556             <xsl:text>}</xsl:text>
 557        </xsl:when>
 558        <xsl:otherwise>
 559         <xsl:apply-templates mode="inline" select="m:type"/>
 560        </xsl:otherwise>
 561        </xsl:choose>
 562       </xsl:when>
 563       <!-- ***************************************** -->
 564       <!-- *********** PROOF ELEMENTS ************** -->
 565       <!-- ***************************************** -->
 566       <!-- PROOF -->
 567       <xsl:when test="$name='proof'">
 568        <xsl:apply-templates select="*[position()=2]">
 569         <xsl:with-param name="current_indent" select="$current_indent"/>
 570        </xsl:apply-templates>
 571        <br/>
 572        <!-- <xsl:element name="br"/> -->
 573        <xsl:call-template name="make_indent">
 574         <xsl:with-param name="current_indent" select="$current_indent"/>
 575        </xsl:call-template>
 576        <FONT color="red">we proved&#x00a0;</FONT>
 577        <xsl:apply-templates select="*[position()=3]">
 578         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
 579        </xsl:apply-templates>
 580       </xsl:when>
 581       <!-- letin1 -->
 582       <xsl:when test="$name='letin1'">
 583        <xsl:apply-templates select="*[position()=2]">
 584         <xsl:with-param name="current_indent" select="$current_indent"/>
 585        </xsl:apply-templates>
 586        <br/>
 587        <xsl:call-template name="make_indent">
 588         <xsl:with-param name="current_indent" select="$current_indent"/>
 589        </xsl:call-template>
 590        <xsl:apply-templates select="*[position()=3]">
 591         <xsl:with-param name="current_indent" select="$current_indent"/>
 592        </xsl:apply-templates>
 593       </xsl:when>
 594       <!-- letin -->
 595       <xsl:when test="$name='letin'">
 596        <xsl:for-each select="*[position()>1 and last()>position()]">
 597         <xsl:apply-templates select=".">
 598          <xsl:with-param name="current_indent" select="$current_indent"/>
 599         </xsl:apply-templates>
 600         <br/>
 601         <xsl:call-template name="make_indent">
 602          <xsl:with-param name="current_indent" select="$current_indent"/>
 603         </xsl:call-template>
 604        </xsl:for-each>
 605        <xsl:apply-templates select="*[position()=last()]">
 606         <xsl:with-param name="current_indent" select="$current_indent"/>
 607        </xsl:apply-templates>
 608       </xsl:when>
 609       <!-- Let -->
 610       <xsl:when test="$name='let'">
 611        (
 612        <xsl:apply-templates select="m:ci"/>
 613        )
 614        <xsl:apply-templates select="*[3]">
 615         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 616        </xsl:apply-templates>
 617       </xsl:when>
 618       <!-- rw_step -->
 619       <xsl:when test="$name='rw_step'">
 620        <xsl:choose>
 621         <xsl:when test="name(*[2])='m:apply'">
 622          <xsl:apply-templates select="*[2]">
 623           <xsl:with-param name="current_indent" select="$current_indent"/>
 624          </xsl:apply-templates>
 625         </xsl:when>
 626         <xsl:otherwise>
 627          <FONT color="red">Consider&#x00a0;</FONT>
 628          <xsl:apply-templates select="*[2]"/>
 629         </xsl:otherwise>
 630        </xsl:choose>
 631        <br/>
 632        <xsl:call-template name="make_indent">
 633         <xsl:with-param name="current_indent" select="$current_indent"/>
 634        </xsl:call-template>
 635        <FONT color="red">Rewrite&#x00a0;</FONT>
 636        <xsl:apply-templates select="*[3]"/>
 637        <FONT color="red">&#x00a0;with&#x00a0;</FONT>
 638        <xsl:apply-templates select="*[4]"/>
 639        <FONT color="red">&#x00a0;by&#x00a0;</FONT>
 640        <xsl:apply-templates select="*[5]"/>
 641       </xsl:when>
 642       <!-- rewrite and apply -->
 643       <xsl:when test="$name='rewrite_and_apply'">
 644        <xsl:apply-templates select="*[2]">
 645         <xsl:with-param name="current_indent" select="$current_indent"/>
 646        </xsl:apply-templates>
 647        <br/>
 648        <xsl:call-template name="make_indent">
 649         <xsl:with-param name="current_indent" select="$current_indent"/>
 650        </xsl:call-template>
 651        <FONT color="red">Then apply it to&#x00a0;</FONT>
 652        <xsl:apply-templates select="*[position()>2]"/>
 653       </xsl:when>
 654       <!-- and_ind -->
 655       <xsl:when test="$name='and_ind'">
 656        <xsl:choose>
 657         <xsl:when test="name(*[2])='m:apply'">
 658          <xsl:apply-templates select="*[2]">
 659           <xsl:with-param name="current_indent" select="$current_indent"/>
 660          </xsl:apply-templates>
 661         </xsl:when>
 662         <xsl:otherwise>
 663          <FONT color="red">Consider&#x00a0;</FONT>
 664          <xsl:apply-templates select="*[2]"/>
 665         </xsl:otherwise>
 666        </xsl:choose>
 667        <br/>
 668        <xsl:call-template name="make_indent">
 669         <xsl:with-param name="current_indent" select="$current_indent"/>
 670        </xsl:call-template>
 671        <FONT color="red">In particular, we have</FONT>
 672        <br/>
 673        <xsl:call-template name="make_indent">
 674         <xsl:with-param name="current_indent" select="$current_indent"/>
 675        </xsl:call-template>
 676        (
 677        <xsl:apply-templates select="*[3]"/>
 678        )&#x00a0;
 679        <xsl:apply-templates select="*[4]">
 680         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 681        </xsl:apply-templates>
 682        <br/>
 683        <xsl:call-template name="make_indent">
 684         <xsl:with-param name="current_indent" select="$current_indent"/>
 685        </xsl:call-template>
 686        (
 687        <xsl:apply-templates select="*[5]"/>
 688        )&#x00a0;
 689        <xsl:apply-templates select="*[6]">
 690         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 691        </xsl:apply-templates>
 692        <br/>
 693        <xsl:call-template name="make_indent">
 694         <xsl:with-param name="current_indent" select="$current_indent"/>
 695        </xsl:call-template>
 696        <xsl:apply-templates select="*[7]">
 697         <xsl:with-param name="current_indent" select="$current_indent"/>
 698        </xsl:apply-templates>
 699       </xsl:when>
 700       <!-- or_ind -->
 701       <xsl:when test="$name='or_ind'">
 702        <xsl:choose>
 703         <xsl:when test="name(*[2])='m:apply'">
 704          <xsl:apply-templates select="*[2]">
 705           <xsl:with-param name="current_indent" select="$current_indent"/>
 706          </xsl:apply-templates>
 707         </xsl:when>
 708         <xsl:otherwise>
 709          <FONT color="red">Consider&#x00a0;</FONT>
 710          <xsl:apply-templates select="*[2]"/>
 711         </xsl:otherwise>
 712        </xsl:choose>
 713        <br/>
 714        <xsl:call-template name="make_indent">
 715         <xsl:with-param name="current_indent" select="$current_indent"/>
 716        </xsl:call-template>
 717        <FONT color="red">We prove&#x00a0;</FONT>
 718        <xsl:apply-templates select="*[3]"/>
 719        <FONT color="red">&#x00a0;by cases:</FONT>
 720        <br/>
 721        <xsl:call-template name="make_indent">
 722         <xsl:with-param name="current_indent" select="$current_indent"/>
 723        </xsl:call-template>
 724        *
 725        <xsl:apply-templates select="*[4]">
 726         <xsl:with-param name="current_indent" select="$current_indent"/>
 727        </xsl:apply-templates>
 728        <br/>
 729        <xsl:call-template name="make_indent">
 730         <xsl:with-param name="current_indent" select="$current_indent"/>
 731        </xsl:call-template>
 732        *
 733        <xsl:apply-templates select="*[5]">
 734         <xsl:with-param name="current_indent" select="$current_indent"/>
 735        </xsl:apply-templates>
 736       </xsl:when>
 737       <!-- Ex_ind -->
 738       <xsl:when test="$name='ex_ind'">
 739        <xsl:choose>
 740         <xsl:when test="name(*[2])='m:apply'">
 741          <xsl:apply-templates select="*[2]">
 742           <xsl:with-param name="current_indent" select="$current_indent"/>
 743          </xsl:apply-templates>
 744         </xsl:when>
 745         <xsl:otherwise>
 746          <FONT color="red">Consider&#x00a0;</FONT>
 747          <xsl:apply-templates select="*[2]">
 748           <xsl:with-param name="current_indent" select="$current_indent"/>
 749          </xsl:apply-templates>
 750         </xsl:otherwise>
 751        </xsl:choose>
 752        <br/>
 753        <xsl:call-template name="make_indent">
 754         <xsl:with-param name="current_indent" select="$current_indent"/>
 755        </xsl:call-template>
 756        <FONT color="red">Let&#x00a0;</FONT>
 757        <xsl:apply-templates mode="inline" select="*[3]"/>
 758        :
 759        <xsl:apply-templates mode="inline" select="*[4]"/>
 760        <FONT color="red">&#x00a0;such that</FONT>
 761        <br/>
 762        <xsl:call-template name="make_indent">
 763         <xsl:with-param name="current_indent" select="$current_indent"/>
 764        </xsl:call-template>
 765        (
 766        <xsl:apply-templates mode="inline" select="*[5]"/>
 767        )
 768        <xsl:apply-templates select="*[6]">
 769         <xsl:with-param name="current_indent" select="$current_indent +7"/>
 770        </xsl:apply-templates>
 771        <br/>
 772        <xsl:call-template name="make_indent">
 773         <xsl:with-param name="current_indent" select="$current_indent"/>
 774        </xsl:call-template>
 775        <xsl:apply-templates select="*[7]">
 776         <xsl:with-param name="current_indent" select="$current_indent"/>
 777        </xsl:apply-templates>
 778       </xsl:when>
 779      </xsl:choose>
 780 </xsl:template>
 781
 782 <!-- LAMBDA -->
 783
 784 <xsl:template match="m:lambda">
 785 <xsl:param name="current_indent" select="0"/>
 786     <xsl:variable name="charlength">
 787      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
 788      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
 789     </xsl:variable>
 790     <!-- <xsl:value-of select="$charlength"/> -->
 791     <!-- <xsl:value-of select="$current_indent"/> -->
 792      <xsl:choose>
 793      <xsl:when test="$charlength > $framewidth">
 794        <!-- &#x03bb; -->
 795        <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
 796        <xsl:apply-templates select="m:bvar/m:ci"/>
 797        <xsl:text>:</xsl:text>
 798        <xsl:apply-templates select="m:bvar/m:type">
 799         <xsl:with-param name="current_indent"
 800            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
 801        </xsl:apply-templates><br/>
 802        <xsl:call-template name="make_indent">
 803         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 804        </xsl:call-template>
 805        <xsl:text>.</xsl:text>
 806        <xsl:apply-templates select="*[position()=2]">
 807         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 808        </xsl:apply-templates>
 809      </xsl:when>
 810      <xsl:otherwise>
 811       <xsl:apply-templates mode="inline" select="."/>
 812      </xsl:otherwise>
 813      </xsl:choose>
 814 </xsl:template>
 815
 816 <!-- href -->
 817 <xsl:template match="m:ci">
 818  <xsl:choose>
 819   <xsl:when test="boolean(@definitionURL)">
 820    <a href="{@definitionURL}">
 821    <xsl:apply-templates/>
 822    </a>
 823   </xsl:when>
 824   <xsl:otherwise>
 825    <xsl:value-of select="."/>
 826   </xsl:otherwise>
 827  </xsl:choose>
 828 </xsl:template>
 829
 830 <!-- COUNTING -->
 831
 832 <xsl:template match="m:ci|m:csymbol" mode="charcount">
 833 <xsl:param name="incurrent_length" select="0"/>
 834     <xsl:choose>
 835     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 836      <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>
 837      <xsl:choose>
 838      <xsl:when test="string($siblength) = &quot;&quot;">
 839       <xsl:value-of select="$incurrent_length + string-length()"/>
 840      </xsl:when>
 841      <xsl:otherwise>
 842       <xsl:value-of select="number($siblength)"/>
 843      </xsl:otherwise>
 844      </xsl:choose>
 845     </xsl:when>
 846     <xsl:otherwise>
 847      <xsl:value-of select="$incurrent_length + string-length()"/>
 848     </xsl:otherwise>
 849     </xsl:choose>
 850 </xsl:template>
 851
 852 <xsl:template match="*" mode="charcount">
 853  <xsl:param name="incurrent_length" select="0"/>
 854  <xsl:choose>
 855   <xsl:when test="count(child::*) = 0">
 856    <xsl:value-of select="$incurrent_length"/>
 857   </xsl:when>
 858   <xsl:otherwise>
 859     <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>
 860     <xsl:choose>
 861      <xsl:when test="$framewidth >= number($childlength)">
 862       <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>
 863       <xsl:choose>
 864        <xsl:when test="string($siblength) = &quot;&quot;">
 865         <xsl:value-of select="number($childlength)"/>
 866        </xsl:when>
 867        <xsl:otherwise>
 868         <xsl:value-of select="number($siblength)"/>
 869        </xsl:otherwise>
 870       </xsl:choose>
 871      </xsl:when>
 872      <xsl:otherwise>
 873       <xsl:value-of select="number($childlength)"/>
 874      </xsl:otherwise>
 875     </xsl:choose>
 876   </xsl:otherwise>
 877  </xsl:choose>
 878 </xsl:template>
 879
 880
 881 <!--***********************************************************************-->
 882 <!-- OBJECTS                                                               -->
 883 <!--***********************************************************************-->
 884
 885 <!-- DEFINITION -->
 886
 887 <xsl:template match="Definition">
 888 <xsl:param name="current_indent" select="0"/>
 889 <p>
 890 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
 891 TYPE =<br/>
 892       <xsl:call-template name="make_indent">
 893        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 894       </xsl:call-template>
 895        <xsl:apply-templates select="type/*[1]">
 896         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 897        </xsl:apply-templates><br/>
 898 BODY =<br/>
 899       <xsl:call-template name="make_indent">
 900        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 901       </xsl:call-template>
 902        <xsl:apply-templates select="body/*[1]">
 903         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 904        </xsl:apply-templates>
 905 </p>
 906 </xsl:template>
 907
 908 <!-- AXIOM -->
 909
 910 <xsl:template match="Axiom">
 911 <xsl:param name="current_indent" select="0"/>
 912 <p>
 913 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
 914 TYPE =<br/>
 915       <xsl:call-template name="make_indent">
 916        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 917       </xsl:call-template>
 918 <xsl:apply-templates select="type/*[1]">
 919           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 920        </xsl:apply-templates>
 921 </p>
 922 </xsl:template>
 923
 924 <!-- UNFINISHED PROOF -->
 925
 926 <xsl:template match="CurrentProof">
 927 <xsl:param name="current_indent" select="0"/>
 928 <p>
 929 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
 930 THESIS:  <xsl:apply-templates select="type/*[1]">
 931           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 932          </xsl:apply-templates><br/>
 933 CONJECTURES:
 934       <xsl:for-each select="Conjecture">
 935       <br/>
 936       <xsl:call-template name="make_indent">
 937        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 938       </xsl:call-template>
 939       <xsl:value-of select="./@no"/> :
 940       <xsl:apply-templates select="./*[1]">
 941        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
 942       </xsl:apply-templates>
 943       </xsl:for-each>
 944       <br/>
 945 PROOF:
 946       <xsl:apply-templates select="body/*[1]">
 947         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 948       </xsl:apply-templates>
 949 </p>
 950 </xsl:template>
 951
 952 <!-- MUTUAL INDUCTIVE DEFINITION -->
 953
 954 <xsl:template match="InductiveDefinition">
 955 <xsl:param name="current_indent" select="0"/>
 956 <p>
 957      <xsl:for-each select="InductiveType">
 958          <xsl:choose>
 959          <xsl:when test="position() = 1">
 960           <xsl:choose>
 961           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 962           INDUCTIVE DEFINITION
 963           </xsl:when>
 964           <xsl:otherwise>
 965           COINDUCTIVE DEFINITION
 966           </xsl:otherwise>
 967           </xsl:choose>
 968          </xsl:when>
 969          <xsl:otherwise>
 970           AND
 971          </xsl:otherwise>
 972          </xsl:choose>
 973          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
 974          [
 975           <xsl:if test="string(../Param) != &quot;&quot;">
 976            <xsl:for-each select="../Param">
 977             <xsl:value-of select="./@name"/>
 978             :
 979             <xsl:apply-templates select="*"/>
 980            </xsl:for-each>
 981           </xsl:if>
 982          ] <br/>
 983          OF ARITY
 984          <xsl:apply-templates select="./arity/*[1]">
 985           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 986          </xsl:apply-templates> <br/>
 987          BUILT FROM:
 988       <xsl:for-each select="./Constructor">
 989       <br/>
 990       <xsl:call-template name="make_indent">
 991        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 992       </xsl:call-template>
 993          <xsl:choose>
 994          <xsl:when test="position() = 1">
 995          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 996          </xsl:when>
 997          <xsl:otherwise>
 998          <xsl:text>| </xsl:text>
 999          </xsl:otherwise>
1000          </xsl:choose>
1001          <xsl:value-of select="./@name"/>
1002          <xsl:text>: </xsl:text>
1003          <xsl:apply-templates select="./*[1]">
1004           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
1005          </xsl:apply-templates>
1006       </xsl:for-each>
1007      </xsl:for-each>
1008 </p>
1009 </xsl:template>
1010
1011 <!-- VARIABLE -->
1012
1013 <xsl:template match="Variable">
1014 <xsl:param name="current_indent" select="0"/>
1015 <p>
1016 VARIABLE <xsl:value-of select="@name"/><br/>
1017 TYPE = <xsl:apply-templates select="type/*[1]">
1018           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1019        </xsl:apply-templates>
1020 </p>
1021 </xsl:template>
1022
1023 <!--***********************************************************************-->
1024 <!-- SECTIONS                                                              -->
1025 <!--***********************************************************************-->
1026
1027 <!-- SECTION -->
1028
1029 <xsl:template match="SECTION">
1030 <xsl:param name="current_indent" select="0"/>
1031  <h1>BEGIN OF SECTION</h1>
1032   <xsl:apply-templates/>
1033  <h1>END OF SECTION</h1>
1034 </xsl:template>
1035
1036 </xsl:stylesheet>