"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}