"Fossies" - the Fresh Open Source Software Archive

Member "hevea-2.35/examples/mathpartir-test.tex" (16 Jan 2021, 13835 Bytes) of package /linux/www/hevea-2.35.tar.gz:


As a special service "Fossies" has tried to format the requested source page into HTML format using (guessed) TeX and LaTeX source code syntax highlighting (style: standard) with prefixed line numbers. Alternatively you can here view or download the uninterpreted source code file.

    1 %  Mathpartir --- Math Paragraph for Typesetting Inference Rules
    2 %
    3 %  Copyright (C) 2001, 2002, 2003 Didier Rémy
    4 %
    5 %  Author         : Didier Remy 
    6 %  Version        : 1.1.1
    7 %  Bug Reports    : to author
    8 %  Web Site       : http://pauillac.inria.fr/~remy/latex/
    9 % 
   10 %  WhizzyTeX is free software; you can redistribute it and/or modify
   11 %  it under the terms of the GNU General Public License as published by
   12 %  the Free Software Foundation; either version 2, or (at your option)
   13 %  any later version.
   14 %  
   15 %  Mathpartir is distributed in the hope that it will be useful,
   16 %  but WITHOUT ANY WARRANTY; without even the implied warranty of
   17 %  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   18 %  GNU General Public License for more details 
   19 %  (http://pauillac.inria.fr/~remy/license/GPL).
   20 %
   21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   22 %  File mathpartir.tex (Documentation)
   23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   24 
   25 \documentclass {article}
   26 
   27 \usepackage {mathpartir}
   28 \usepackage {listings}
   29 \usepackage {array}
   30 \usepackage {url}
   31 \newif \ifhevea 
   32 %HEVEA \heveatrue
   33 \ifhevea 
   34 \usepackage {hevea}
   35 \fi
   36 
   37 \lstset {basicstyle=\tt}
   38 \let \lst \verb
   39 
   40 \title {Remy's Mathpartir}
   41 
   42 \begin{document}
   43 
   44 \begin{abstract}
   45 This package provides macros for displaying lists of formulas that are
   46 typeset in mixed horizontal and vertical modes. The package is two-folded.
   47 
   48 The first part is an environment \verb"mathpar" that generalizes the math
   49 display mode to allow several formulas on the same line, and several lines
   50 in the same display. The arrangement of the sequence of formulas into lines
   51 is automatic depending on the line width and on a minimum inter-formula
   52 space and line width alike words in a paragraphs (in centerline mode).  A
   53 typical application is  displaying a set of type inference rules.
   54 
   55 The second par is a macro \lst"inferrule" to typeset inference rules
   56 themselves.  Here again, both premises and conclusions are presented as list
   57 of formulas that should be displayed in almost the same way, except that the
   58 width is not fixed in advance; and the inference rule should use no more
   59 width than necessary so that other inference rules are given a chance to
   60 appear on the same line.
   61 
   62 Although \verb"mathpar" and \verb"inferrule" look similar in their
   63 specification, and are often used in combination, they are in fact
   64 completely different in their implementations.
   65 \end{abstract}
   66 
   67 \section {The mathpar environment}
   68 
   69 The mathpar environment is a ``paragraph mode for formulas''. 
   70 It  allows to typeset long list of formulas putting as
   71 many as possible on the same line: 
   72 $$
   73 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
   74 \begin{lstlisting}{Ocaml}
   75 \begin{mathpar}
   76 A-Formula \and 
   77 Longer-Formula \and 
   78 And \and The-Last-One
   79 \end{mathpar}
   80 \end{lstlisting}
   81 &
   82 ~~~
   83 &
   84 \begin{mathpar}
   85 A-Formula 
   86 \and
   87 Longer-Formula
   88 \and
   89 And 
   90 \and
   91 The-Last-One
   92 \end{mathpar}
   93 \end{tabular}
   94 $$
   95 Formulas are separated by \verb"\and" (or equivalently by a blank line). 
   96 To enforce a vertical break it sufficies to replace \verb"\and" by
   97 \verb"\\". 
   98 
   99 The implementation of \verb"mathpar" entirely relies on the paragraph mode
  100 for text. It starts  a new paragraph, and a math formula within a paragraph,
  101 after adjusting the spacing and penalties for breaks. Then, it simply binds
  102 \verb"\and" to something like \verb"\goodbreak". 
  103 \section {The inferrule macro}
  104 
  105 The inferrule macro is designed to typeset inference rules.  It should
  106 only\footnote {Even though the basic version may work in text mode,
  107 we discourage its use in text mode; the star-version cannot be used in
  108 text-mode} be used in math mode (or display math mode). 
  109 
  110 The basic use of the rule is 
  111 \begin{verbatim}
  112 \inferrule
  113   {one \\ two \\ three \\ or \\ more \\ premisses}
  114   {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
  115 \end{verbatim}
  116 This is the rendering on a large page
  117 \def \one {\inferrule
  118   {one \\ two \\ three \\ or \\ more \\ premisses}
  119   {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
  120 }
  121 $$
  122 \ifhevea \one
  123 \else
  124 \fbox {\vbox {\advance \hsize by -2\fboxsep \advance \hsize by -2\fboxrule
  125        \linewidth\hsize
  126         $$\one$$}}
  127 \fi
  128 $$
  129 
  130 However, the same formula on a narrower page will automatically be typsetted
  131 like that:
  132 \def \two {\inferrule
  133   {one \\\\ two \\ three \\ or \\\\ more \\ premisses}
  134   {and \\ any \\ number \\\\ of \\ conclusions \\\\ as \\ well}
  135 }
  136 $$
  137 \ifhevea \two
  138 \else
  139 \fbox {\hsize 0.33 \hsize \vbox {$$\two$$}}
  140 \fi
  141 $$
  142 An inference rule is mainly composed of a premisse and a conclusion. 
  143 The premisse and the conclusions are both list of formulas where the
  144 elements are separated by \verb"\\". 
  145 
  146 Note the dissymetry between typesetting of the premisses and of
  147 conclusions where lines closer to the center are fit first. 
  148 
  149 A newline can be forced by adding an empty line \verb"\\\\"
  150 
  151 \begin{tabular}{m{0.44\hsize}m{0.1\hsize}m{0.44\hsize}}
  152 \begin{lstlisting}{Ocaml}
  153 \inferrule 
  154    {aa \\\\ bb}
  155    {dd \\ ee \\ ff}
  156 \end{lstlisting}
  157 &
  158 ~~~
  159 &
  160 $\inferrule {aa \\\\bb}{dd \\ ee \\ ff}$
  161 \\
  162 \end{tabular}
  163 
  164 \subsection {Single rules}
  165 
  166 Single rules are the default mode. 
  167 Rules are aligned on their fraction bar, as illustrated below:
  168 $$
  169 \inferrule {aa \\ bb}{ee} \hspace {4em} \inferrule {aa \\\\ bb \\ ee}{ee}
  170 $$
  171 If the premise or the conclusion is empty, then the fraction bar is not
  172 typeset and the premise or the conclusion is centered:
  173 $$
  174 \begin{tabular}{m{0.3\hsize}m{0.05\hsize}m{0.3\hsize}m{0.05\hsize}m{0.3\hsize}}
  175 \begin{lstlisting}{Ocaml}
  176 \inferrule {}{aa} + 
  177 \inferrule {aa \\\\ aa}{}
  178 \end{lstlisting}
  179 &
  180 ~~~~~~~~
  181 &
  182 $\inferrule {}{aa}$
  183 &
  184 $+$
  185 &
  186 $\inferrule {aa \\\\ aa}{}$
  187 \\
  188 \end{tabular}
  189 $$
  190 Use use \verb"{ }" instead of \verb"{}" to get an axiom for instance:
  191 $$
  192 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  193 \begin{lstlisting}{Ocaml}
  194 \inferrule { }{aa} + 
  195 \inferrule {aa}{ }
  196 \end{lstlisting}
  197 &
  198 ~~~~~~
  199 &
  200 $
  201 \inferrule { }{aa} + 
  202 \inferrule {aa}{ }
  203 $
  204 \\
  205 \end{tabular}
  206 $$
  207 
  208 The macro \lst"\inferrule" acceps a label as optional argument, which will
  209 be typeset on the top left corner of the rule: 
  210 \par
  211 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  212 \begin{lstlisting}{Ocaml}
  213 \inferrule [yop]
  214    {aa \\ bb}
  215    {cc}
  216 \end{lstlisting}
  217 &
  218 $\inferrule [Yop]{aa \\ bb}{cc}$
  219 \\
  220 \end{tabular}
  221 \par\noindent
  222 See section~\ref {options} for changing typesetting of labels. 
  223 A label can also be placed next to the rule directly, since the rule is
  224 centered: 
  225 \par
  226 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  227 \begin{lstlisting}{Ocaml}
  228 \inferrule 
  229    {aa \\ bb}
  230    {cc}
  231 \quad (\textsc {Yop})
  232 \end{lstlisting}
  233 &
  234 ~~~~~~
  235 &
  236 $\inferrule{aa \\ bb}{cc} \quad (\textsc {Yop})$
  237 \\
  238 \end{tabular}
  239 
  240 \subsection {Customizing}
  241 
  242 By default, lines are centerred in inference rules. 
  243 However, this can be changed by either \lst"\mprset{flushleft}"
  244 or \lst"\mprset{center}". For instance, 
  245 
  246 \begin{tabular}{m{0.44\hsize}m{0.12\hsize}m{0.44\hsize}}
  247 \begin{lstlisting}{Ocaml}
  248 $$\mprset{flushleft}
  249   \inferrule 
  250     {a \\ bbb \\\\ ccc \\ dddd}
  251     {e \\ ff \\ gg}$$ 
  252 \end{lstlisting}
  253 &
  254 ~~~~~
  255 &
  256 $$\mprset{flushleft} 
  257 \inferrule {a \\ bbb  \\\\ ccc \\ dddd}{e \\ ff \\ gg}$$
  258 \\
  259 \end{tabular}
  260 
  261 \noindent
  262 Note that lines are aligned independently in the premise and the
  263 conclusion, which are both themselves centered. In particular, 
  264 left alignment will not affect a single-line premisse or conclusion. 
  265 
  266 
  267 \subsection {Derivation trees}
  268 
  269 To help writing cascades of rules forming a derivation tree, inference rules
  270 can also be aligned on their bottom line. For this, we use the star-version:
  271 $$
  272 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  273 \begin{lstlisting}{Ocaml}
  274 \inferrule*
  275    {\inferrule* {aa \\ bb}{cc}
  276     \\ dd}
  277    {ee}
  278 \end{lstlisting}
  279 &
  280 ~~~~~~
  281 &
  282 $
  283 \inferrule*
  284    {\inferrule* {aa \\ bb}{cc}
  285     \\ dd}
  286    {ee}
  287 $
  288 \\
  289 \end{tabular}
  290 $$
  291 The star version can also take an optional argument, 
  292 but with a different semantics. The optional argument is parsed by the 
  293 \verb"keyval" package, so as to offer a set of record-like options: 
  294 $$
  295 \def \val {{\em v}}
  296 \def \arraystretch {1.4}
  297 \begin{tabular}{|>{\tt}c|p{0.7\hsize}|}
  298 \hline
  299 \bf key & \bf Effect for value {\val}
  300 \\\hline\hline
  301 before & Execute {\val} before typesetting the rule.
  302          Useful for instance to change the maximal width of the rule.
  303 \\\hline
  304 width &  Set the width of the rule to {\val}
  305 \\\hline
  306 narrower & Set the width of the rule to {\val} times \verb"\hsize".
  307 \\\hline
  308 left & Put a label {\val} on the left of the rule
  309 \\\hline
  310 Left & Idem, but as if the label had zero width. 
  311 \\\hline
  312 Right & As \verb"Left", but on  the right of the rule.
  313 \\\hline
  314 right & As \verb"left",  but on the right of the rule.
  315 \\\hline
  316 leftskip & Cheat by (skip negative space) {\val} on the left side.
  317 \\\hline
  318 rightskip & Cheat by {\val} on the right side of the rule.
  319 \\\hline
  320 vdots & Raise the rule by {\val} and insert vertical dots. 
  321 \\\hline
  322 \end{tabular}
  323 $$
  324 Here is an example of a complex derivation:
  325 $$
  326 \inferrule* [left=Total]
  327   {\inferrule* [Left=Foo]
  328      {\inferrule* [Right=Bar,
  329                        leftskip=2em,rightskip=2em,vdots=1.5em]
  330          {a \\ a \\\\ bb \\ cc \\ dd}
  331          {ee}
  332        \\ ff \\ gg}
  333      {hh}
  334    \\\\
  335    \inferrule* [lab=XX]{uu \\ vv}{ww}
  336   }
  337   {(1)}
  338 $$
  339 and its code
  340 \begin{lstlisting}{Ocaml}
  341 \inferrule* [left=Total]
  342   {\inferrule* [Left=Foo]
  343      {\inferrule* [Right=Bar,
  344                        leftskip=2em,rightskip=2em,vdots=1.5em]
  345          {a \\ a \\\\ bb \\ cc \\ dd}
  346          {ee}
  347        \\ ff \\ gg}
  348      {hh}
  349   \\
  350   \inferrule* [lab=XX]{uu \\ vv}{ww}}
  351   {(1)}
  352 \end{lstlisting}
  353 
  354 \def \L#1{\lower 0.4ex \hbox {#1}}
  355 \def \R#1{\raise 0.4ex \hbox {#1}}
  356 \def \hevea {H\L{E}\R{V}\L{E}A}
  357 \def \hevea {$\mbox {H}\!_{\mbox {E}}\!\mbox {V}\!_{\mbox {E}}\!\mbox {A}$}
  358 
  359 
  360 \subsection {Implementation}
  361 
  362 The main macro in the implementation of inference rules is the one that
  363 either premises and conclusions.  The macros uses two box-registers one
  364 \verb"hbox" for typesetting each line and one \verb"vbox" for collecting
  365 lines. The premise appears as a list with
  366 \verb"\\" as separator. Each element is considered in turn typeset in a
  367 \verb"hbox" in display math mode. Its width is compare to the space left on
  368 the current line. If the box would not fit, the current horizontal line is
  369 transferred to the vertical box and emptied. Then, the current formula can
  370 safely be added to the horizontal line (if it does not fit, nothing can be
  371 done). When moved to the vertical list, lines are aligned on their center
  372 (as if their left-part was a left overlapped). At the end the vbox is
  373 readjusted on the right. 
  374 
  375 This description works for conclusions. For premises, the elements must be
  376 processes in reverse order and the vertical list is simply built upside
  377 down. 
  378 
  379 
  380 \section {Other Options}
  381 
  382 \label {options}
  383 
  384 The package also defines \verb"\infer" as a shortcut for \verb"\inferrule"
  385 but only if it is not previously defined. 
  386 
  387 The package uses \verb"\TirName" and \verb"\RefTirName" to typeset labels,
  388 which can safely be redefined by the user. The former is used for defining
  389 occurrences ({\em ie.} in rule \lst"\inferrule") while the latter is used
  390 for referencing ({\em ie.} in the star-version). 
  391 
  392 The vertical space in \verb"mathpar" is adjusted by
  393 \verb"\MathparLineskip". To restore the normal paragraph parameters in mathpar
  394 mode (for instance for some inner paragraph), use the command
  395 \verb"\MathparNormalpar".  
  396 The environment uses \verb"\MathparBindings" to
  397 rebind \verb"\\", \verb"and", and \verb"\par". You can redefine thus command
  398 to change the default bindings or add your own. 
  399 
  400 \section {Examples}
  401 
  402 See the source of this documentation ---the file \lst"mathpartir.tex"---
  403 for full examples. 
  404 
  405 \section {{\hevea} compatibility}
  406 
  407 The package also redefines \verb"\hva" to do nothing in \lst"mathpar"
  408 environment and nor in inference rules. 
  409 
  410 In HeVeA, \verb"\and" will always produce a vertical break in mathpar
  411 environment; to obtain a horizontal break, use \verb"\hva \and" instead.
  412 Conversely, \verb"\\" will always produce a horizontal break in type
  413 inference rules; to obtain a vertical break, use \verb"\hva \\" instead.
  414 
  415 For instance, by default the following code,
  416 \begin{lstlisting}{Ocaml}
  417 \begin{mathpar}
  418 \inferrule* [Left=Foo]
  419    {\inferrule* [Right=Bar,width=8em,
  420                  leftskip=2em,rightskip=2em,vdots=1.5em]
  421       {a \\ a \\ bb \\ cc \\ dd}
  422       {ee}
  423     \\ ff \\ gg}
  424    {hh}
  425 \and
  426 \inferrule* [lab=XX]{uu \\ vv}{ww}
  427 \end{mathpar}
  428 \end{lstlisting}
  429 which typesets in {\TeX} as follows,
  430 \begin{mathpar}
  431 \inferrule* [Left=Foo]
  432    {\inferrule* [Right=Bar,width=8em,
  433                  leftskip=2em,rightskip=2em,vdots=1.5em]
  434       {a \\ a \\ bb \\ cc \\ dd}
  435       {ee}
  436     \\ ff \\ gg}
  437    {hh}
  438 \and
  439 \inferrule* [lab=XX]{uu \\ vv}{ww}
  440 \end{mathpar}
  441 would appear as follows with the compatible {\hevea} mode:
  442 \begin{mathpar}
  443 \inferrule* [left=Foo]
  444    {\inferrule* [right=Bar]
  445       {a \\ a \\ bb \\ cc \\ dd}
  446       {ee}
  447     \\ ff \\ gg}
  448    {hh}
  449 \\
  450 \inferrule* [lab=XX]{uu \\ vv}{ww}
  451 \end{mathpar}
  452 To obtain (almost) the same rendering as in {\TeX}, it could be typed as 
  453 \begin{lstlisting}[escapechar=\%]{Ocaml}
  454 \begin{mathpar}
  455 \inferrule* [Left=Foo]
  456    {\inferrule* [Right=Bar,width=8em,
  457                  leftskip=2em,rightskip=2em,vdots=1.5em]
  458       {a \\ a \hva \\ bb \\ cc \\ dd}
  459       {ee}
  460     \\ ff \\ gg}
  461    {hh}
  462 \hva \and
  463 \inferrule* [lab=XX]{uu \\ vv}{ww}
  464 \end{mathpar}
  465 \end{lstlisting}
  466 Actually, it would be typeset and follows with the compatible {\hevea} mode:
  467 \begin{mathpar}
  468 \inferrule* [left=Foo]
  469    {\inferrule* [right=Bar]
  470       {a \\ a \\\\ bb \\ cc \\ dd}
  471       {ee}
  472     \\ ff \\ gg}
  473    {hh}
  474 \and
  475 \inferrule* [lab=XX]{uu \\ vv}{ww}
  476 \end{mathpar}
  477 
  478 
  479 \end{document}
  480 
  481 \end{document}
  482 
  483 % LocalWords:  mathpar aa Yop bb dd ee ff cc Ocaml Foo leftskip rightskip vdots
  484 % LocalWords:  gg hh uu vv ww HeVeA escapechar
  485