helm/style/mmlextension_andrea.xsl

   1 <?xml version="1.0"?>
   2
   3 <!--***********************************************************************-->
   4 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
   5 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
   6 <!-- Revised: March 3 2000, Irene Schena                                   -->
   7 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena          -->
   8 <!-- Revised: March 21 2000, Irene Schena                                  -->
   9 <!--***********************************************************************-->
  10
  11 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  12                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  13                               xmlns:helm="http://www.cs.unibo.it/helm">
  14
  15 <xsl:import href="mml2mmlv1_0.xsl"/>
  16
  17 <!--***********************************************************************-->
  18 <!-- Parameter affecting line-breaking                                     -->
  19 <!--***********************************************************************-->
  20
  21 <xsl:variable name="framewidth" select="15"/>
  22
  23 <!--***********************************************************************-->
  24 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
  25 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
  26 <!-- sono i termini: la presentation per un termine e' generata come primo -->
  27 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
  28 <!-- nel secondo figlio di semantics, annotation-xml                       -->
  29 <!--***********************************************************************-->
  30
  31 <!--**********************-->
  32 <!--        OBJECTS       -->
  33 <!--**********************-->
  34
  35 <xsl:template match="/">
  36  <xsl:processing-instruction name="cocoon-format">type="text/xhtml"</xsl:processing-instruction>
  37  <xsl:apply-templates select="*"/>
  38 </xsl:template>
  39
  40 <!-- DEFINITION -->
  41
  42 <xsl:template match="Definition">
  43     <m:math>
  44      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  45       <m:mtr>
  46        <m:mtd>
  47         <m:mrow>
  48          <m:mtext>DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
  49         </m:mrow>
  50        </m:mtd>
  51       </m:mtr>
  52       <m:mtr>
  53        <m:mtd>
  54         <m:mrow>
  55          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  56          <xsl:apply-templates select="type/*[1]"/>
  57         </m:mrow>
  58        </m:mtd>
  59       </m:mtr>
  60       <m:mtr>
  61        <m:mtd>
  62         <m:mrow>
  63          <m:mtext>AS</m:mtext>
  64         </m:mrow>
  65        </m:mtd>
  66       </m:mtr>
  67       <m:mtr>
  68        <m:mtd>
  69         <m:mrow>
  70          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  71          <xsl:apply-templates select="body/*[1]"/>
  72         </m:mrow>
  73        </m:mtd>
  74       </m:mtr>
  75      </m:mtable>
  76     </m:math>
  77 </xsl:template>
  78
  79 <!-- AXIOM -->
  80
  81 <xsl:template match="Axiom">
  82     <m:math>
  83      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  84       <m:mtr>
  85        <m:mtd>
  86         <m:mrow>
  87          <m:mtext>AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
  88         </m:mrow>
  89        </m:mtd>
  90       </m:mtr>
  91       <m:mtr>
  92        <m:mtd>
  93         <m:mrow>
  94          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  95          <xsl:apply-templates select="type/*[1]"/>
  96         </m:mrow>
  97        </m:mtd>
  98       </m:mtr>
  99      </m:mtable>
 100     </m:math>
 101 </xsl:template>
 102
 103 <!-- UNFINISHED PROOF -->
 104
 105 <xsl:template match="CurrentProof">
 106     <m:math>
 107      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 108       <m:mtr>
 109        <m:mtd>
 110         <m:mrow>
 111          <m:mtext>UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)</m:mtext>
 112         </m:mrow>
 113        </m:mtd>
 114       </m:mtr>
 115       <m:mtr>
 116        <m:mtd>
 117         <m:mrow>
 118          <m:mtext>THESIS:</m:mtext>
 119         </m:mrow>
 120        </m:mtd>
 121       </m:mtr>
 122       <m:mtr>
 123        <m:mtd>
 124         <m:mrow>
 125          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 126          <xsl:apply-templates select="type/*[1]"/>
 127         </m:mrow>
 128        </m:mtd>
 129       </m:mtr>
 130       <m:mtr>
 131        <m:mtd>
 132         <m:mrow>
 133          <m:mtext>CONJECTURES:</m:mtext>
 134         </m:mrow>
 135        </m:mtd>
 136       </m:mtr>
 137       <xsl:for-each select="Conjecture">
 138       <m:mtr>
 139        <m:mtd>
 140         <m:mrow>
 141          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 142          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
 143          <xsl:apply-templates select="./*[1]"/>
 144         </m:mrow>
 145        </m:mtd>
 146       </m:mtr>
 147       </xsl:for-each>
 148       <m:mtr>
 149        <m:mtd>
 150         <m:mrow>
 151          <m:mtext>CORRESPONDING PROOF:</m:mtext>
 152         </m:mrow>
 153        </m:mtd>
 154       </m:mtr>
 155       <m:mtr>
 156        <m:mtd>
 157         <m:mrow>
 158          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 159          <xsl:apply-templates select="body/*[1]"/>
 160         </m:mrow>
 161        </m:mtd>
 162       </m:mtr>
 163      </m:mtable>
 164     </m:math>
 165 </xsl:template>
 166
 167 <!-- MUTUAL INDUCTIVE DEFINITION -->
 168
 169 <xsl:template match="InductiveDefinition">
 170     <m:math>
 171      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 172      <xsl:for-each select="InductiveType">
 173       <m:mtr>
 174        <m:mtd>
 175         <m:mrow>
 176          <xsl:choose>
 177          <xsl:when test="position() = 1">
 178           <xsl:choose>
 179           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 180            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 181           </xsl:when>
 182           <xsl:otherwise>
 183            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 184           </xsl:otherwise>
 185           </xsl:choose>
 186          </xsl:when>
 187          <xsl:otherwise>
 188           <m:mtext>AND</m:mtext>
 189          </xsl:otherwise>
 190          </xsl:choose>
 191          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 192          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 193         </m:mrow>
 194        </m:mtd>
 195       </m:mtr>
 196       <m:mtr>
 197        <m:mtd>
 198         <m:mrow>
 199          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 200          <m:mtext>[</m:mtext>
 201          <xsl:choose>
 202          <xsl:when test="string(../Param) != &quot;&quot;">
 203           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 204            <xsl:for-each select="../Param">
 205             <m:mtr>
 206              <m:mtd>
 207               <m:mrow>
 208                <m:mi><xsl:value-of select="./@name"/></m:mi>
 209                <m:mo>:</m:mo>
 210                <xsl:apply-templates select="*"/>
 211               </m:mrow>
 212              </m:mtd>
 213             </m:mtr>
 214            </xsl:for-each>
 215             <m:mtr>
 216              <m:mtd>
 217               <m:mrow>
 218                <m:mtext>]</m:mtext>
 219               </m:mrow>
 220              </m:mtd>
 221             </m:mtr>
 222           </m:mtable>
 223          </xsl:when>
 224          <xsl:otherwise>
 225           <m:mtext>]</m:mtext>
 226          </xsl:otherwise>
 227          </xsl:choose>
 228         </m:mrow>
 229        </m:mtd>
 230       </m:mtr>
 231       <m:mtr>
 232        <m:mtd>
 233         <m:mrow>
 234          <m:mtext>OF ARITY</m:mtext>
 235         </m:mrow>
 236        </m:mtd>
 237       </m:mtr>
 238       <m:mtr>
 239        <m:mtd>
 240         <m:mrow>
 241          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 242          <xsl:apply-templates select="./arity/*[1]"/>
 243         </m:mrow>
 244        </m:mtd>
 245       </m:mtr>
 246       <m:mtr>
 247        <m:mtd>
 248         <m:mrow>
 249          <m:mtext>BUILT FROM</m:mtext>
 250         </m:mrow>
 251        </m:mtd>
 252       </m:mtr>
 253       <xsl:for-each select="./Constructor">
 254       <m:mtr>
 255        <m:mtd>
 256         <m:mrow>
 257          <xsl:choose>
 258          <xsl:when test="position() = 1">
 259           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 260          </xsl:when>
 261          <xsl:otherwise>
 262           <m:mtext>|</m:mtext>
 263           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 264          </xsl:otherwise>
 265          </xsl:choose>
 266          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 267          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 268          <xsl:apply-templates select="./*[1]"/>
 269         </m:mrow>
 270        </m:mtd>
 271       </m:mtr>
 272       </xsl:for-each>
 273      </xsl:for-each>
 274      </m:mtable>
 275     </m:math>
 276 </xsl:template>
 277
 278 <!-- VARIABLE -->
 279
 280 <xsl:template match="Variable">
 281     <m:math>
 282      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 283       <m:mtr>
 284        <m:mtd>
 285         <m:mrow>
 286          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 287         </m:mrow>
 288        </m:mtd>
 289       </m:mtr>
 290       <m:mtr>
 291        <m:mtd>
 292         <m:mrow>
 293          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 294          <xsl:apply-templates select="type/*[1]"/>
 295         </m:mrow>
 296        </m:mtd>
 297       </m:mtr>
 298      </m:mtable>
 299     </m:math>
 300 </xsl:template>
 301
 302 <!--**********************-->
 303 <!--        TERMS         -->
 304 <!--**********************-->
 305
 306 <xsl:template match="m:bvar">
 307  <xsl:choose>
 308   <xsl:when test="m:type">
 309    <xsl:variable name="charlength">
 310     <xsl:apply-templates select="m:ci" mode="charcount"/>
 311    </xsl:variable>
 312    <xsl:choose>
 313     <xsl:when test="$charlength >= $framewidth">
 314      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 315       <m:mtr>
 316        <m:mtd>
 317         <xsl:apply-templates select="m:ci"/>
 318         <m:mo>:</m:mo>
 319        </m:mtd>
 320       </m:mtr>
 321       <m:mtr>
 322        <m:mtd>
 323          <xsl:apply-templates select="m:type"/>
 324        </m:mtd>
 325       </m:mtr>
 326      </m:mtable>
 327     </xsl:when>
 328     <xsl:otherwise>
 329      <xsl:apply-templates select="m:ci"/>
 330      <m:mo>:</m:mo>
 331      <xsl:apply-templates select="m:type"/>
 332     </xsl:otherwise>
 333    </xsl:choose>
 334   </xsl:when>
 335   <xsl:otherwise>
 336    <xsl:apply-templates select="m:ci"/>
 337   </xsl:otherwise>
 338  </xsl:choose>
 339 </xsl:template>
 340
 341
 342 <!-- CSYMBOL -->
 343
 344 <xsl:template match="m:apply[m:csymbol]">
 345     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 346     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 347     <m:mrow>
 348      <xsl:if test="@helm:xref">
 349       <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
 350      </xsl:if>
 351      <xsl:choose>
 352       <xsl:when test="$name='prod'">
 353        <xsl:choose>
 354        <xsl:when test="$charlength >= $framewidth">
 355         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 356          <m:mtr>
 357           <m:mtd>
 358             <m:mo color="Blue">&#x03a0;</m:mo>
 359             <xsl:apply-templates select="m:bvar"/>
 360           </m:mtd>
 361          </m:mtr>
 362          <m:mtr>
 363           <m:mtd>
 364            <m:mrow>
 365             <m:mo>.</m:mo>
 366             <xsl:apply-templates select="*[position()=3]"/>
 367            </m:mrow>
 368           </m:mtd>
 369          </m:mtr>
 370         </m:mtable>
 371        </xsl:when>
 372        <xsl:otherwise>
 373         <m:mo color="Blue">&#x03a0;</m:mo>
 374         <xsl:apply-templates select="m:bvar/m:ci"/>
 375         <m:mo>:</m:mo>
 376         <xsl:apply-templates select="m:bvar/m:type"/>
 377         <m:mo>.</m:mo>
 378         <xsl:apply-templates select="*[position()=3]"/>
 379        </xsl:otherwise>
 380        </xsl:choose>
 381       </xsl:when>
 382       <xsl:when test="$name='arrow'">
 383        <xsl:choose>
 384        <xsl:when test="$charlength >= $framewidth">
 385         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 386          <m:mtr>
 387           <m:mtd>
 388            <m:mrow>
 389             <m:mo stretchy="false">(</m:mo>
 390             <xsl:apply-templates select="*[position()=2]"/>
 391            </m:mrow>
 392           </m:mtd>
 393          </m:mtr>
 394          <m:mtr>
 395           <m:mtd>
 396            <m:mrow>
 397             <m:mo color="Blue">&#x2192;</m:mo>
 398             <xsl:apply-templates select="*[position()=3]"/>
 399            </m:mrow>
 400           </m:mtd>
 401          </m:mtr>
 402          <m:mtr>
 403           <m:mtd>
 404            <m:mrow>
 405             <m:mo stretchy="false">)</m:mo>
 406            </m:mrow>
 407           </m:mtd>
 408          </m:mtr>
 409         </m:mtable>
 410        </xsl:when>
 411        <xsl:otherwise>
 412         <m:mo stretchy="false">(</m:mo>
 413         <xsl:apply-templates select="*[position()=2]"/>
 414         <m:mo color="Blue">&#x2192;</m:mo>
 415         <xsl:apply-templates select="*[position()=3]"/>
 416         <m:mo stretchy="false">)</m:mo>
 417        </xsl:otherwise>
 418        </xsl:choose>
 419       </xsl:when>
 420       <xsl:when test="$name='app'">
 421        <xsl:choose>
 422        <xsl:when test="$charlength >= $framewidth">
 423         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 424          <m:mtr>
 425           <m:mtd>
 426            <m:mrow>
 427             <m:mo stretchy="false">(</m:mo>
 428             <xsl:apply-templates select="*[position()=2]"/>
 429            </m:mrow>
 430           </m:mtd>
 431          </m:mtr>
 432          <xsl:for-each select="*[position()>2]">
 433          <m:mtr>
 434           <m:mtd>
 435            <m:mrow>
 436             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 437             <xsl:apply-templates select="."/>
 438            </m:mrow>
 439           </m:mtd>
 440          </m:mtr>
 441          </xsl:for-each>
 442          <m:mtr>
 443           <m:mtd>
 444            <m:mrow>
 445             <m:mo stretchy="false">)</m:mo>
 446            </m:mrow>
 447           </m:mtd>
 448          </m:mtr>
 449         </m:mtable>
 450        </xsl:when>
 451        <xsl:otherwise>
 452         <m:mo stretchy="false">(</m:mo>
 453         <xsl:apply-templates select="*[position()=2]"/>
 454         <xsl:for-each select="*[position()>2]">
 455          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 456          <xsl:apply-templates select="."/>
 457         </xsl:for-each>
 458         <m:mo stretchy="false">)</m:mo>
 459        </xsl:otherwise>
 460        </xsl:choose>
 461       </xsl:when>
 462       <xsl:when test="$name='cast'">
 463        <xsl:choose>
 464        <xsl:when test="$charlength >= $framewidth">
 465         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 466          <m:mtr>
 467           <m:mtd>
 468            <m:mrow>
 469             <m:mo stretchy="false">(</m:mo>
 470             <xsl:apply-templates select="*[position()=2]"/>
 471            </m:mrow>
 472           </m:mtd>
 473          </m:mtr>
 474          <m:mtr>
 475           <m:mtd>
 476            <m:mrow>
 477             <m:mo color="#b03060">:></m:mo>
 478             <xsl:apply-templates select="*[position()=3]"/>
 479            </m:mrow>
 480           </m:mtd>
 481          </m:mtr>
 482          <m:mtr>
 483           <m:mtd>
 484            <m:mrow>
 485             <m:mo stretchy="false">)</m:mo>
 486            </m:mrow>
 487           </m:mtd>
 488          </m:mtr>
 489         </m:mtable>
 490        </xsl:when>
 491        <xsl:otherwise>
 492         <m:mo stretchy="false">(</m:mo>
 493         <xsl:apply-templates select="*[position()=2]"/>
 494         <m:mo color="#b03060">:></m:mo>
 495         <xsl:apply-templates select="*[position()=3]"/>
 496         <m:mo stretchy="false">)</m:mo>
 497        </xsl:otherwise>
 498        </xsl:choose>
 499       </xsl:when>
 500       <xsl:when test="$name='Prop'">
 501        <m:mo>Prop</m:mo>
 502       </xsl:when>
 503       <xsl:when test="$name='Set'">
 504        <m:mo>Set</m:mo>
 505       </xsl:when>
 506       <xsl:when test="$name='Type'">
 507        <m:mo>Type</m:mo>
 508       </xsl:when>
 509       <xsl:when test="$name='mutcase'">
 510        <xsl:choose>
 511        <xsl:when test="$charlength >= $framewidth">
 512         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 513         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 514          <m:mtr>
 515           <m:mtd>
 516            <m:mrow>
 517             <m:mo>&lt;</m:mo>
 518             <xsl:apply-templates select="*[position()=2]"/>
 519             <xsl:if test="$framewidth > $charlength">
 520              <m:mo>&gt;</m:mo>
 521              <m:mo>CASES</m:mo>
 522              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 523              <xsl:apply-templates select="*[position()=3]"/>
 524             </xsl:if>
 525            </m:mrow>
 526           </m:mtd>
 527          </m:mtr>
 528          <xsl:if test="$charlength >= $framewidth">
 529          <m:mtr>
 530           <m:mtd>
 531            <m:mrow>
 532             <m:mo>&gt;</m:mo>
 533             <m:mo>CASES</m:mo>
 534             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 535             <xsl:apply-templates select="*[position()=3]"/>
 536            </m:mrow>
 537           </m:mtd>
 538          </m:mtr>
 539          </xsl:if>
 540          <m:mtr>
 541           <m:mtd>
 542            <m:mrow>
 543             <m:mo>OF</m:mo>
 544            </m:mrow>
 545           </m:mtd>
 546          </m:mtr>
 547          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 548          <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 549          <m:mtr>
 550           <m:mtd>
 551            <m:mrow>
 552             <xsl:choose>
 553             <xsl:when test="position() = 1">
 554               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 555             </xsl:when>
 556             <xsl:otherwise>
 557              <m:mo stretchy="false">|</m:mo>
 558             </xsl:otherwise>
 559             </xsl:choose>
 560             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 561             <xsl:apply-templates select="."/>
 562             <xsl:if test="$framewidth > $charlength">
 563              <m:mo color="Green">&#x21d2;</m:mo>
 564              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 565             </xsl:if>
 566            </m:mrow>
 567           </m:mtd>
 568          </m:mtr>
 569          <xsl:if test="$charlength >= $framewidth">
 570          <m:mtr>
 571           <m:mtd>
 572            <m:mrow>
 573             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 574             <m:mo color="Green">&#x21d2;</m:mo>
 575             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 576            </m:mrow>
 577           </m:mtd>
 578          </m:mtr>
 579          </xsl:if>
 580         </xsl:for-each>
 581          <m:mtr>
 582           <m:mtd>
 583            <m:mrow>
 584             <m:mo>END</m:mo>
 585            </m:mrow>
 586           </m:mtd>
 587          </m:mtr>
 588         </m:mtable>
 589        </xsl:when>
 590        <xsl:otherwise>
 591         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 592         <m:mo>CASES</m:mo>
 593         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 594         <xsl:apply-templates select="*[position()=3]"/>
 595         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 596         <m:mo>OF</m:mo>
 597         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 598          <xsl:choose>
 599          <xsl:when test="position() != 1">
 600           <m:mo stretchy="false">|</m:mo>
 601          </xsl:when>
 602          </xsl:choose>
 603          <xsl:apply-templates select="."/>
 604          <m:mo color="Green">&#x21d2;</m:mo>
 605          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 606         </xsl:for-each>
 607         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 608         <m:mo>END</m:mo>
 609        </xsl:otherwise>
 610        </xsl:choose>
 611       </xsl:when>
 612       <xsl:when test="$name='fix'">
 613        <xsl:choose>
 614        <xsl:when test="$charlength >= $framewidth">
 615         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 616          <m:mtr>
 617           <m:mtd>
 618            <m:mrow>
 619             <m:mo>FIX</m:mo>
 620             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 621             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 622             <m:mo stretchy="false">{</m:mo>
 623            </m:mrow>
 624           </m:mtd>
 625          </m:mtr>
 626          <m:mtr>
 627           <m:mtd>
 628            <m:mrow>
 629             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 630             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 631             <xsl:for-each select="m:bvar">
 632              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 633              <m:mtr>
 634               <m:mtd>
 635                <m:mrow>
 636                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 637                 <m:mo>:</m:mo>
 638                 <xsl:if test="$framewidth > $charlength">
 639                  <xsl:apply-templates select="m:type"/>
 640                 </xsl:if>
 641                </m:mrow>
 642               </m:mtd>
 643              </m:mtr>
 644              <xsl:if test="$charlength >= $framewidth">
 645              <m:mtr>
 646               <m:mtd>
 647                <m:mrow>
 648                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 649                 <xsl:apply-templates select="m:type"/>
 650                </m:mrow>
 651               </m:mtd>
 652              </m:mtr>
 653              </xsl:if>
 654              <m:mtr>
 655               <m:mtd>
 656                <m:mrow>
 657                 <m:mo>:=</m:mo>
 658                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 659                </m:mrow>
 660               </m:mtd>
 661              </m:mtr>
 662             </xsl:for-each>
 663             </m:mtable>
 664            </m:mrow>
 665           </m:mtd>
 666          </m:mtr>
 667          <m:mtr>
 668           <m:mtd>
 669            <m:mrow>
 670             <m:mo stretchy="false">}</m:mo>
 671            </m:mrow>
 672           </m:mtd>
 673          </m:mtr>
 674         </m:mtable>
 675        </xsl:when>
 676        <xsl:otherwise>
 677         <m:mo>FIX</m:mo>
 678         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 679         <m:mo stretchy="false">{</m:mo>
 680         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 681         <xsl:for-each select="m:bvar">
 682          <m:mtr>
 683           <m:mtd>
 684            <m:mrow>
 685             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 686             <m:mo>:</m:mo>
 687             <xsl:apply-templates select="m:type"/>
 688             <m:mo>:=</m:mo>
 689             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 690             <xsl:if test="position()=last()">
 691              <m:mo stretchy="false">}</m:mo>
 692             </xsl:if>
 693            </m:mrow>
 694           </m:mtd>
 695          </m:mtr>
 696          </xsl:for-each>
 697         </m:mtable>
 698        </xsl:otherwise>
 699        </xsl:choose>
 700       </xsl:when>
 701       <xsl:when test="$name='cofix'">
 702        <xsl:choose>
 703        <xsl:when test="$charlength >= $framewidth">
 704         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 705          <m:mtr>
 706           <m:mtd>
 707            <m:mrow>
 708             <m:mo>COFIX</m:mo>
 709             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 710             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 711             <m:mo stretchy="false">{</m:mo>
 712            </m:mrow>
 713           </m:mtd>
 714          </m:mtr>
 715          <m:mtr>
 716           <m:mtd>
 717            <m:mrow>
 718             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 719             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 720             <xsl:for-each select="m:bvar">
 721              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 722              <m:mtr>
 723               <m:mtd>
 724                <m:mrow>
 725                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 726                 <m:mo>:</m:mo>
 727                 <xsl:if test="$framewidth > $charlength">
 728                  <xsl:apply-templates select="m:type"/>
 729                 </xsl:if>
 730                </m:mrow>
 731               </m:mtd>
 732              </m:mtr>
 733              <xsl:if test="$charlength >= $framewidth">
 734              <m:mtr>
 735               <m:mtd>
 736                <m:mrow>
 737                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 738                 <xsl:apply-templates select="m:type"/>
 739                </m:mrow>
 740               </m:mtd>
 741              </m:mtr>
 742              </xsl:if>
 743              <m:mtr>
 744               <m:mtd>
 745                <m:mrow>
 746                 <m:mo>:=</m:mo>
 747                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 748                </m:mrow>
 749               </m:mtd>
 750              </m:mtr>
 751             </xsl:for-each>
 752             </m:mtable>
 753            </m:mrow>
 754           </m:mtd>
 755          </m:mtr>
 756          <m:mtr>
 757           <m:mtd>
 758            <m:mrow>
 759             <m:mo stretchy="false">}</m:mo>
 760            </m:mrow>
 761           </m:mtd>
 762          </m:mtr>
 763         </m:mtable>
 764        </xsl:when>
 765        <xsl:otherwise>
 766         <m:mo>COFIX</m:mo>
 767         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 768         <m:mo stretchy="false">{</m:mo>
 769         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 770         <xsl:for-each select="m:bvar">
 771          <m:mtr>
 772           <m:mtd>
 773            <m:mrow>
 774             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 775             <m:mo>:</m:mo>
 776             <xsl:apply-templates select="m:type"/>
 777             <m:mo>:=</m:mo>
 778             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 779             <xsl:if test="position()=last()">
 780              <m:mo stretchy="false">}</m:mo>
 781             </xsl:if>
 782            </m:mrow>
 783           </m:mtd>
 784          </m:mtr>
 785          </xsl:for-each>
 786         </m:mtable>
 787        </xsl:otherwise>
 788        </xsl:choose>
 789       </xsl:when>
 790       </xsl:choose>
 791      </m:mrow>
 792 </xsl:template>
 793
 794 <!-- LAMBDA -->
 795
 796 <xsl:template match="m:lambda">
 797     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
 798     <m:mrow helm:xref="{@helm:xref}">
 799      <xsl:choose>
 800      <xsl:when test="$charlength >= $framewidth">
 801       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 802         <m:mtr>
 803           <m:mtd>
 804             <m:mo color="Blue">&#x03bb;</m:mo>
 805             <xsl:apply-templates select="m:bvar"/>
 806           </m:mtd>
 807          </m:mtr>
 808        <m:mtr>
 809         <m:mtd>
 810          <m:mrow>
 811           <m:mo>.</m:mo>
 812           <xsl:apply-templates select="*[position()=2]"/>
 813          </m:mrow>
 814         </m:mtd>
 815        </m:mtr>
 816       </m:mtable>
 817      </xsl:when>
 818      <xsl:otherwise>
 819       <m:mo color="Red">&#x03bb;</m:mo>
 820       <xsl:apply-templates select="m:bvar/m:ci"/>
 821       <m:mo>:</m:mo>
 822       <xsl:apply-templates select="m:bvar/m:type"/>
 823       <m:mo>.</m:mo>
 824       <xsl:apply-templates select="*[position()=2]"/>
 825      </xsl:otherwise>
 826      </xsl:choose>
 827     </m:mrow>
 828 </xsl:template>
 829
 830 <!-- *********************************** -->
 831 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
 832 <!-- *********************************** -->
 833
 834 <!-- Logic -->
 835
 836 <xsl:template match = "m:apply[m:and[1]|m:or[1]
 837           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]|m:eq[1]
 838           |m:intesect[1]|m:union[1]|m:subset[1]|m:prsubset]">
 839  <xsl:variable name="symbol">
 840   <xsl:choose>
 841    <xsl:when test="m:and[1]">
 842     <xsl:value-of select="'wedge'"/>
 843    </xsl:when>
 844    <xsl:when test="m:or[1]">
 845     <xsl:value-of select="'vee'"/>
 846    </xsl:when>
 847    <xsl:when test="m:geq[1]">
 848     <xsl:value-of select="'geq'"/>
 849    </xsl:when>
 850    <xsl:when test="m:leq[1]">
 851     <xsl:value-of select="'leq'"/>
 852    </xsl:when>
 853    <xsl:when test="m:gt[1]">
 854     <xsl:value-of select="'gt'"/>
 855    </xsl:when>
 856    <xsl:when test="m:lt[1]">
 857     <xsl:value-of select="'lt'"/>
 858    </xsl:when>
 859    <xsl:when test="m:eq[1]">
 860     <xsl:value-of select="'eq'"/>
 861    </xsl:when>
 862    <xsl:when test="m:subset[1]">
 863     <xsl:value-of select="'SubsetEqual'"/>
 864    </xsl:when>
 865    <xsl:when test="m:prsubset[1]">
 866     <xsl:value-of select="'subset'"/>
 867    </xsl:when>
 868    <xsl:when test="m:intersect[1]">
 869     <xsl:value-of select="'Intersection'"/>
 870    </xsl:when>
 871    <xsl:when test="m:union[1]">
 872     <xsl:value-of select="'Union'"/>
 873    </xsl:when>
 874   </xsl:choose>
 875  </xsl:variable>
 876  <xsl:variable name="charlength">
 877   <xsl:apply-templates select="*[1]" mode="charcount"/>
 878  </xsl:variable>
 879  <xsl:choose>
 880   <xsl:when test="$charlength >= $framewidth">
 881    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 882     <m:mtr>
 883      <m:mtd>
 884       <m:mo stretchy="false">(</m:mo>
 885       <xsl:apply-templates select="*[position()=2]"/>
 886      </m:mtd>
 887     </m:mtr>
 888     <xsl:for-each select = "*[position()>2]">
 889      <m:mtr>
 890       <m:mtd>
 891        <m:mrow>
 892         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 893         <m:mo>
 894          <m:mchar name="{$symbol}"/>
 895         </m:mo>
 896         <xsl:apply-templates select="."/>
 897        </m:mrow>
 898       </m:mtd>
 899      </m:mtr>
 900     </xsl:for-each>
 901     <m:mtr>
 902      <m:mtd>
 903       <m:mo stretchy="false">)</m:mo>
 904      </m:mtd>
 905     </m:mtr>
 906    </m:mtable>
 907   </xsl:when>
 908   <xsl:otherwise>
 909    <xsl:apply-imports/>
 910   </xsl:otherwise>
 911  </xsl:choose>
 912 </xsl:template>
 913
 914 <xsl:template match = "m:set">
 915  <xsl:variable name="charlength">
 916   <xsl:apply-templates select="." mode="charcount"/>
 917  </xsl:variable>
 918  <xsl:choose>
 919   <xsl:when test="$charlength >= $framewidth">
 920    <xsl:choose>
 921     <xsl:when test="name(*[1]) = 'm:bvar'">
 922      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 923       <m:mtr>
 924        <m:mtd>
 925         <m:mo stretchy="false">{</m:mo>
 926         <xsl:apply-templates select="m:bvar"/>
 927        </m:mtd>
 928       </m:mtr>
 929       <m:mtr>
 930        <m:mtd>
 931         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 932         <m:mo>|</m:mo>
 933         <xsl:apply-templates select="m:condition"/>
 934        </m:mtd>
 935       </m:mtr>
 936       <m:mtr>
 937        <m:mtd>
 938         <m:mo stretchy="false">}</m:mo>
 939        </m:mtd>
 940       </m:mtr>
 941      </m:mtable>
 942     </xsl:when>
 943     <xsl:otherwise>
 944      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 945       <m:mtr>
 946        <m:mtd>
 947         <m:mo stretchy="false">{</m:mo>
 948         <xsl:apply-templates select="*[1]"/>
 949         <xsl:if test="count(child::*) != 1">
 950          <m:mo>,</m:mo>
 951         </xsl:if>
 952        </m:mtd>
 953       </m:mtr>
 954       <xsl:for-each select = "*[position()>1]">
 955        <m:mtr>
 956         <m:mtd>
 957          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 958          <xsl:apply-templates select="."/>
 959          <xsl:if test="position() != last()">
 960           <m:mo>,</m:mo>
 961          </xsl:if>
 962         </m:mtd>
 963        </m:mtr>
 964       </xsl:for-each>
 965       <m:mtr>
 966        <m:mtd>
 967         <m:mo stretchy="false">}</m:mo>
 968        </m:mtd>
 969       </m:mtr>
 970      </m:mtable>
 971     </xsl:otherwise>
 972    </xsl:choose>
 973   </xsl:when>
 974   <xsl:otherwise>
 975    <xsl:apply-imports/>
 976   </xsl:otherwise>
 977  </xsl:choose>
 978 </xsl:template>
 979
 980 <!--**********************-->
 981 <!--       COUNTING       -->
 982 <!--**********************-->
 983
 984 <xsl:template match="m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
 985  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff" mode="charcount">
 986 <xsl:param name="incurrent_length" select="0"/>
 987     <xsl:choose>
 988     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
 989      <xsl:variable name="siblength">
 990       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
 991        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
 992       </xsl:apply-templates>
 993      </xsl:variable>
 994      <xsl:choose>
 995      <xsl:when test="string($siblength) = &quot;&quot;">
 996       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
 997      </xsl:when>
 998      <xsl:otherwise>
 999       <xsl:value-of select="number($siblength)"/>
1000      </xsl:otherwise>
1001      </xsl:choose>
1002     </xsl:when>
1003     <xsl:otherwise>
1004      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1005     </xsl:otherwise>
1006     </xsl:choose>
1007 </xsl:template>
1008
1009 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1010 <xsl:param name="incurrent_length" select="0"/>
1011 <xsl:param name="nosibling" select="0"/>
1012     <xsl:choose>
1013     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1014      <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>
1015      <xsl:choose>
1016      <xsl:when test="string($siblength) = &quot;&quot;">
1017       <xsl:value-of select="$incurrent_length + string-length()"/>
1018      </xsl:when>
1019      <xsl:otherwise>
1020       <xsl:value-of select="number($siblength)"/>
1021      </xsl:otherwise>
1022      </xsl:choose>
1023     </xsl:when>
1024     <xsl:otherwise>
1025      <xsl:value-of select="$incurrent_length + string-length()"/>
1026     </xsl:otherwise>
1027     </xsl:choose>
1028 </xsl:template>
1029
1030 <xsl:template match="*" mode="charcount">
1031 <xsl:param name="incurrent_length" select="0"/>
1032 <xsl:param name="nosibling" select="0"/>
1033     <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/><xsl:with-param name="nosibling" select="0"/></xsl:apply-templates></xsl:variable>
1034     <xsl:choose>
1035     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1036      <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>
1037      <xsl:choose>
1038      <xsl:when test="string($siblength) = &quot;&quot;">
1039       <xsl:value-of select="number($childlength)"/>
1040      </xsl:when>
1041      <xsl:otherwise>
1042       <xsl:value-of select="number($siblength)"/>
1043      </xsl:otherwise>
1044      </xsl:choose>>
1045     </xsl:when>
1046     <xsl:otherwise>
1047      <xsl:value-of select="number($childlength)"/>
1048     </xsl:otherwise>
1049     </xsl:choose>
1050 </xsl:template>
1051
1052 </xsl:stylesheet>