"Fossies" - the Fresh Open Source Software Archive

Member "hevea-2.35/examples/fancy-test.tex" (16 Jan 2021, 9152 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 
    2 \documentclass {article}
    3 \input{fancysection.hva}
    4 %\colorsections{20}
    5 %\definecolor{title}{named}{Blue}
    6 \usepackage {mathpartir}
    7 \usepackage {listings}
    8 \usepackage {array}
    9 \usepackage {url}
   10 \newif \ifhevea 
   11 %HEVEA \heveatrue
   12 \ifhevea 
   13 \usepackage {hevea}
   14 \fi
   15 
   16 \lstset {basicstyle=\tt}
   17 \let \lst \verb
   18 
   19 \title {Didier's Mathpartir}
   20 \author{Didier Remy}
   21 
   22 %\loadcssfile{x.css}
   23 %\setLATEXstyle{title}{background:green;color:black;font:helvetica}
   24 %\setHTMLstyle{H1.part}{background:green;color:white;font:helvetica}
   25 %\setLATEXstyle{section}{background:blue;color:white}
   26 %\setLATEXstyle{subsection}{background:blue;color:white}
   27 %\setHTMLstyle{H5}{background:cyan;color:black}
   28 %\setLATEXstyle{subparagraph}{background:magenta;color:white}
   29 %\setHTMLstyle{H3}{background:blue;color:white;font:sans-serif}
   30 %\setstyles{background:blue;color:white;font:sans-serif}
   31 %\setstyles{backgound:green}
   32 
   33 \begin{document}
   34 
   35 \maketitle
   36 
   37 \part{Only One Part}
   38 
   39 \section {The inferrule macro}
   40 The inferrule macro is designed to typeset inference rules.  It should
   41 only\footnote {Even though the basic version may work in text mode,
   42 we discourage its use in text mode; the star-version cannot be used in
   43 text-mode} be used in math mode (or display math mode). 
   44 
   45 The basic use of the rule is 
   46 \begin{verbatim}
   47 \inferrule
   48   {one \\ two \\ three \\ or \\ more \\ premisses}
   49   {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
   50 \end{verbatim}
   51 This is the rendering on a large page
   52 \def \one {\inferrule
   53   {one \\ two \\ three \\ or \\ more \\ premisses}
   54   {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
   55 }
   56 $$
   57 \ifhevea \one
   58 \else
   59 \fbox {\vbox {\advance \hsize by -2\fboxsep \advance \hsize by -2\fboxrule
   60        \linewidth\hsize
   61         $$\one$$}}
   62 \fi
   63 $$
   64 
   65 However, the same formula on a narrower page will automatically be typsetted
   66 like that:
   67 \def \two {\inferrule
   68   {one \\\\ two \\ three \\ or \\\\ more \\ premisses}
   69   {and \\ any \\ number \\\\ of \\ conclusions \\\\ as \\ well}
   70 }
   71 $$
   72 \ifhevea \two
   73 \else
   74 \fbox {\hsize 0.33 \hsize \vbox {$$\two$$}}
   75 \fi
   76 $$
   77 An inference rule is mainly composed of a premisse and a conclusion. 
   78 The premisse and the conclusions are both list of formulas where the
   79 elements are separated by \verb"\\". 
   80 
   81 Note the dissymetry between typesetting of the premisses and of
   82 conclusions where lines closer to the center are fit first. 
   83 
   84 A newline can be forced by adding an empty line \verb"\\\\"
   85 
   86 \begin{tabular}{m{0.44\hsize}m{0.1\hsize}m{0.44\hsize}}
   87 \begin{lstlisting}{Ocaml}
   88 \inferrule 
   89    {aa \\\\ bb}
   90    {dd \\ ee \\ ff}
   91 \end{lstlisting}
   92 &
   93 ~~~
   94 &
   95 $\inferrule {aa \\\\bb}{dd \\ ee \\ ff}$
   96 \\
   97 \end{tabular}
   98 
   99 \subsection {Single rules}
  100 
  101 Single rules are the default mode. 
  102 Rules are aligned on their fraction bar, as illustrated below:
  103 $$
  104 \inferrule {aa \\ bb}{ee} \hspace {4em} \inferrule {aa \\\\ bb \\ ee}{ee}
  105 $$
  106 If the premise or the conclusion is empty, then the fraction bar is not
  107 typeset and the premise or the conclusion is centered:
  108 $$
  109 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  110 \begin{lstlisting}{Ocaml}
  111 \inferrule {}{aa} + 
  112 \inferrule {aa \\\\ aa}{}
  113 \end{lstlisting}
  114 &
  115 ~~~~~~~~
  116 &
  117 $
  118 \inferrule {}{aa} + 
  119 \inferrule {aa \\\\ aa}{}
  120 $
  121 \\
  122 \end{tabular}
  123 $$
  124 \paragraph{OOOOOH}
  125 Use use \verb"{ }" instead of \verb"{}" to get an axiom for instance:
  126 $$
  127 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  128 \begin{lstlisting}{Ocaml}
  129 \inferrule { }{aa} + 
  130 \inferrule {aa}{ }
  131 \end{lstlisting}
  132 &
  133 ~~~~~~
  134 &
  135 \mbox {$
  136 \inferrule { }{aa} + 
  137 \inferrule {aa}{ }
  138 $}
  139 \\
  140 \end{tabular}
  141 $$
  142 \subparagraph{OOOOHOOOH}
  143 The macro \lst"\inferrule" acceps a label as optional argument, which will
  144 be typeset on the top left corner of the rule: 
  145 \par
  146 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  147 \begin{lstlisting}{Ocaml}
  148 \inferrule [yop]
  149    {aa \\ bb}
  150    {cc}
  151 \end{lstlisting}
  152 &
  153 $\inferrule [Yop]{aa \\ bb}{cc}$
  154 \\
  155 \end{tabular}
  156 \par\noindent
  157 See section~\ref{options} for changing typesetting of labels. 
  158 A label can also be placed next to the rule directly, since the rule is
  159 centered: 
  160 \par
  161 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  162 \begin{lstlisting}{Ocaml}
  163 \inferrule 
  164    {aa \\ bb}
  165    {cc}
  166 \quad (\textsc {Yop})
  167 \end{lstlisting}
  168 &
  169 ~~~~~~
  170 &
  171 $\inferrule{aa \\ bb}{cc} \quad (\textsc {Yop})$
  172 \\
  173 \end{tabular}
  174 
  175 \subsection {Customizing}
  176 
  177 By default, lines are centerred in inference rules. 
  178 However, this can be changed by either \lst"\mprset{flushleft}"
  179 or \lst"\mprset{center}". For instance, 
  180 
  181 \begin{tabular}{m{0.44\hsize}m{0.12\hsize}m{0.44\hsize}}
  182 \begin{lstlisting}{Ocaml}
  183 $$\mprset{flushleft}
  184   \inferrule 
  185     {a \\ bbb \\\\ ccc \\ dddd}
  186     {e \\ ff \\ gg}$$ 
  187 \end{lstlisting}
  188 &
  189 ~~~~~
  190 &
  191 $$\mprset{flushleft} 
  192 \inferrule {a \\ bbb  \\\\ ccc \\ dddd}{e \\ ff \\ gg}$$
  193 \\
  194 \end{tabular}
  195 
  196 \noindent
  197 Note that lines are aligned independently in the premise and the
  198 conclusion, which are both themselves centered. In particular, 
  199 left alignment will not affect a single-line premisse or conclusion. 
  200 
  201 
  202 \subsection {Derivation trees}
  203 
  204 To help writing cascades of rules forming a derivation tree, inference rules
  205 can also be aligned on their bottom line. For this, we use the star-version:
  206 $$
  207 \begin{tabular}{m{0.45\hsize}m{0.1\hsize}m{0.45\hsize}}
  208 \begin{lstlisting}{Ocaml}
  209 \inferrule*
  210    {\inferrule* {aa \\ bb}{cc}
  211     \\ dd}
  212    {ee}
  213 \end{lstlisting}
  214 &
  215 ~~~~~~
  216 &
  217 $
  218 \inferrule*
  219    {\inferrule* {aa \\ bb}{cc}
  220     \\ dd}
  221    {ee}
  222 $
  223 \\
  224 \end{tabular}
  225 $$
  226 The star version can also take an optional argument, 
  227 but with a different semantics. The optional argument is parsed by the 
  228 \verb"keyval" package, so as to offer a set of record-like options: 
  229 $$
  230 \def \val {{\em v}}
  231 \def \arraystretch {1.4}
  232 \begin{tabular}{|>{\tt}c|p{0.7\hsize}|}
  233 \hline
  234 \bf key & \bf Effect for value {\val}
  235 \\\hline\hline
  236 before & Execute {\val} before typesetting the rule.
  237          Useful for instance to change the maximal width of the rule.
  238 \\\hline
  239 width &  Set the width of the rule to {\val}
  240 \\\hline
  241 narrower & Set the width of the rule to {\val} times \verb"\hsize".
  242 \\\hline
  243 left & Put a label {\val} on the left of the rule
  244 \\\hline
  245 Left & Idem, but as if the label had zero width. 
  246 \\\hline
  247 Right & As \verb"Left", but on  the right of the rule.
  248 \\\hline
  249 right & As \verb"left",  but on the right of the rule.
  250 \\\hline
  251 leftskip & Cheat by (skip negative space) {\val} on the left side.
  252 \\\hline
  253 rightskip & Cheat by {\val} on the right side of the rule.
  254 \\\hline
  255 vdots & Raise the rule by {\val} and insert vertical dots. 
  256 \\\hline
  257 \end{tabular}
  258 $$
  259 Here is an example of a complex derivation:
  260 $$
  261 \inferrule* [left=Total]
  262   {\inferrule* [Left=Foo]
  263      {\inferrule* [Right=Bar,
  264                        leftskip=2em,rightskip=2em,vdots=1.5em]
  265          {a \\ a \\\\ bb \\ cc \\ dd}
  266          {ee}
  267        \\ ff \\ gg}
  268      {hh}
  269   \\
  270   \inferrule* [lab=XX]{uu \\ vv}{ww}}
  271   {(1)}
  272 $$
  273 and its code
  274 \begin{lstlisting}{Ocaml}
  275 \inferrule* [left=Total]
  276   {\inferrule* [Left=Foo]
  277      {\inferrule* [Right=Bar,
  278                        leftskip=2em,rightskip=2em,vdots=1.5em]
  279          {a \\ a \\\\ bb \\ cc \\ dd}
  280          {ee}
  281        \\ ff \\ gg}
  282      {hh}
  283   \\
  284   \inferrule* [lab=XX]{uu \\ vv}{ww}}
  285   {(1)}
  286 \end{lstlisting}
  287 
  288 \def \L#1{\lower 0.4ex \hbox {#1}}
  289 \def \R#1{\raise 0.4ex \hbox {#1}}
  290 \def \hevea {H\L{E}\R{V}\L{E}A}
  291 \def \hevea {$\mbox {H}\!_{\mbox {E}}\!\mbox {V}\!_{\mbox {E}}\!\mbox {A}$}
  292 
  293 
  294 \subsection {Implementation}
  295 
  296 The main macro in the implementation of inference rules is the one that
  297 either premises and conclusions.  The macros uses two box-registers one
  298 \verb"hbox" for typesetting each line and one \verb"vbox" for collecting
  299 lines. The premise appears as a list with
  300 \verb"\\" as separator. Each element is considered in turn typeset in a
  301 \verb"hbox" in display math mode. Its width is compare to the space left on
  302 the current line. If the box would not fit, the current horizontal line is
  303 transferred to the vertical box and emptied. Then, the current formula can
  304 safely be added to the horizontal line (if it does not fit, nothing can be
  305 done). When moved to the vertical list, lines are aligned on their center
  306 (as if their left-part was a left overlapped). At the end the vbox is
  307 readjusted on the right. 
  308 
  309 This description works for conclusions. For premises, the elements must be
  310 processes in reverse order and the vertical list is simply built upside
  311 down. 
  312 
  313 
  314 \section {Other Options}
  315 
  316 \label {options}
  317 
  318 The package also defines \verb"\infer" as a shortcut for \verb"\inferrule"
  319 but only if it is not previously defined. 
  320 
  321 The package uses \verb"\TirName" and \verb"\RefTirName" to typeset labels,
  322 which can safely be redefined by the user. The former is used for defining
  323 occurrences ({\em ie.} in rule \lst"\inferrule") while the latter is used
  324 for referencing ({\em ie.} in the star-version). 
  325 
  326 The vertical space in \verb"mathpar" is adjusted by
  327 \verb"\MathparLineskip". To restore the normal paragraph parameters in mathpar
  328 mode (for instance for some inner paragraph), use the command
  329 \verb"\MathparNormalpar".  
  330 The environment uses \verb"\MathparBindings" to
  331 rebind \verb"\\", \verb"and", and \verb"\par". You can redefine thus command
  332 to change the default bindings or add your own. 
  333 
  334 
  335 \end{document}