1 % Mathpartir --- Math Paragraph for Typesetting Inference Rules |
|
2 % |
|
3 % Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy |
|
4 % |
|
5 % Author : Didier Remy |
|
6 % Version : 1.2.0 |
|
7 % Bug Reports : to author |
|
8 % Web Site : http://pauillac.inria.fr/~remy/latex/ |
|
9 % |
|
10 % Mathpartir 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.sty (LaTeX macros) |
|
23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
24 |
|
25 \NeedsTeXFormat{LaTeX2e} |
|
26 \ProvidesPackage{mathpartir} |
|
27 [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules] |
|
28 |
|
29 %% |
|
30 |
|
31 %% Identification |
|
32 %% Preliminary declarations |
|
33 |
|
34 \RequirePackage {keyval} |
|
35 |
|
36 %% Options |
|
37 %% More declarations |
|
38 |
|
39 %% PART I: Typesetting maths in paragraphe mode |
|
40 |
|
41 \newdimen \mpr@tmpdim |
|
42 |
|
43 % To ensure hevea \hva compatibility, \hva should expands to nothing |
|
44 % in mathpar or in inferrule |
|
45 \let \mpr@hva \empty |
|
46 |
|
47 %% normal paragraph parametters, should rather be taken dynamically |
|
48 \def \mpr@savepar {% |
|
49 \edef \MathparNormalpar |
|
50 {\noexpand \lineskiplimit \the\lineskiplimit |
|
51 \noexpand \lineskip \the\lineskip}% |
|
52 } |
|
53 |
|
54 \def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em} |
|
55 \def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em} |
|
56 \def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} |
|
57 \let \MathparLineskip \mpr@lineskip |
|
58 \def \mpr@paroptions {\MathparLineskip} |
|
59 \let \mpr@prebindings \relax |
|
60 |
|
61 \newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em |
|
62 |
|
63 \def \mpr@goodbreakand |
|
64 {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip} |
|
65 \def \mpr@and {\hskip \mpr@andskip} |
|
66 \def \mpr@andcr {\penalty 50\mpr@and} |
|
67 \def \mpr@cr {\penalty -10000\mpr@and} |
|
68 \def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10} |
|
69 |
|
70 \def \mpr@bindings {% |
|
71 \let \and \mpr@andcr |
|
72 \let \par \mpr@andcr |
|
73 \let \\\mpr@cr |
|
74 \let \eqno \mpr@eqno |
|
75 \let \hva \mpr@hva |
|
76 } |
|
77 \let \MathparBindings \mpr@bindings |
|
78 |
|
79 % \@ifundefined {ignorespacesafterend} |
|
80 % {\def \ignorespacesafterend {\aftergroup \ignorespaces} |
|
81 |
|
82 \newenvironment{mathpar}[1][] |
|
83 {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering |
|
84 \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else |
|
85 \noindent $\displaystyle\fi |
|
86 \MathparBindings} |
|
87 {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend} |
|
88 |
|
89 % \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum |
|
90 % \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi} |
|
91 |
|
92 %%% HOV BOXES |
|
93 |
|
94 \def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip |
|
95 \vbox \bgroup \tabskip 0em \let \\ \cr |
|
96 \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup |
|
97 \egroup} |
|
98 |
|
99 \def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize |
|
100 \box0\else \mathvbox {#1}\fi} |
|
101 |
|
102 |
|
103 %% Part II -- operations on lists |
|
104 |
|
105 \newtoks \mpr@lista |
|
106 \newtoks \mpr@listb |
|
107 |
|
108 \long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter |
|
109 {#2}\edef #2{\the \mpr@lista \the \mpr@listb}} |
|
110 |
|
111 \long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter |
|
112 {#2}\edef #2{\the \mpr@listb\the\mpr@lista}} |
|
113 |
|
114 \long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb |
|
115 \expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}} |
|
116 |
|
117 \def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2} |
|
118 \long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}} |
|
119 |
|
120 \def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2} |
|
121 \long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}} |
|
122 |
|
123 \def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}% |
|
124 \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the |
|
125 \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty |
|
126 \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop |
|
127 \mpr@flatten \mpr@all \mpr@to \mpr@one |
|
128 \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof |
|
129 \mpr@all \mpr@stripend |
|
130 \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi |
|
131 \ifx 1\mpr@isempty |
|
132 \repeat |
|
133 } |
|
134 |
|
135 \def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty |
|
136 \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp} |
|
137 |
|
138 %% Part III -- Type inference rules |
|
139 |
|
140 \newif \if@premisse |
|
141 \newbox \mpr@hlist |
|
142 \newbox \mpr@vlist |
|
143 \newif \ifmpr@center \mpr@centertrue |
|
144 \def \mpr@htovlist {% |
|
145 \setbox \mpr@hlist |
|
146 \hbox {\strut |
|
147 \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi |
|
148 \unhbox \mpr@hlist}% |
|
149 \setbox \mpr@vlist |
|
150 \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist |
|
151 \else \unvbox \mpr@vlist \box \mpr@hlist |
|
152 \fi}% |
|
153 } |
|
154 % OLD version |
|
155 % \def \mpr@htovlist {% |
|
156 % \setbox \mpr@hlist |
|
157 % \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}% |
|
158 % \setbox \mpr@vlist |
|
159 % \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist |
|
160 % \else \unvbox \mpr@vlist \box \mpr@hlist |
|
161 % \fi}% |
|
162 % } |
|
163 |
|
164 \def \mpr@item #1{$\displaystyle #1$} |
|
165 \def \mpr@sep{2em} |
|
166 \def \mpr@blank { } |
|
167 \def \mpr@hovbox #1#2{\hbox |
|
168 \bgroup |
|
169 \ifx #1T\@premissetrue |
|
170 \else \ifx #1B\@premissefalse |
|
171 \else |
|
172 \PackageError{mathpartir} |
|
173 {Premisse orientation should either be T or B} |
|
174 {Fatal error in Package}% |
|
175 \fi \fi |
|
176 \def \@test {#2}\ifx \@test \mpr@blank\else |
|
177 \setbox \mpr@hlist \hbox {}% |
|
178 \setbox \mpr@vlist \vbox {}% |
|
179 \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi |
|
180 \let \@hvlist \empty \let \@rev \empty |
|
181 \mpr@tmpdim 0em |
|
182 \expandafter \mpr@makelist #2\mpr@to \mpr@flat |
|
183 \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi |
|
184 \def \\##1{% |
|
185 \def \@test {##1}\ifx \@test \empty |
|
186 \mpr@htovlist |
|
187 \mpr@tmpdim 0em %%% last bug fix not extensively checked |
|
188 \else |
|
189 \setbox0 \hbox{\mpr@item {##1}}\relax |
|
190 \advance \mpr@tmpdim by \wd0 |
|
191 %\mpr@tmpdim 1.02\mpr@tmpdim |
|
192 \ifnum \mpr@tmpdim < \hsize |
|
193 \ifnum \wd\mpr@hlist > 0 |
|
194 \if@premisse |
|
195 \setbox \mpr@hlist |
|
196 \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}% |
|
197 \else |
|
198 \setbox \mpr@hlist |
|
199 \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}% |
|
200 \fi |
|
201 \else |
|
202 \setbox \mpr@hlist \hbox {\unhbox0}% |
|
203 \fi |
|
204 \else |
|
205 \ifnum \wd \mpr@hlist > 0 |
|
206 \mpr@htovlist |
|
207 \mpr@tmpdim \wd0 |
|
208 \fi |
|
209 \setbox \mpr@hlist \hbox {\unhbox0}% |
|
210 \fi |
|
211 \advance \mpr@tmpdim by \mpr@sep |
|
212 \fi |
|
213 }% |
|
214 \@rev |
|
215 \mpr@htovlist |
|
216 \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist |
|
217 \fi |
|
218 \egroup |
|
219 } |
|
220 |
|
221 %%% INFERENCE RULES |
|
222 |
|
223 \@ifundefined{@@over}{% |
|
224 \let\@@over\over % fallback if amsmath is not loaded |
|
225 \let\@@overwithdelims\overwithdelims |
|
226 \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims |
|
227 \let\@@above\above \let\@@abovewithdelims\abovewithdelims |
|
228 }{} |
|
229 |
|
230 %% The default |
|
231 |
|
232 \def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em |
|
233 $\displaystyle {#1\mpr@over #2}$}} |
|
234 \let \mpr@fraction \mpr@@fraction |
|
235 |
|
236 %% A generic solution to arrow |
|
237 |
|
238 \def \mpr@make@fraction #1#2#3#4#5{\hbox {% |
|
239 \def \mpr@tail{#1}% |
|
240 \def \mpr@body{#2}% |
|
241 \def \mpr@head{#3}% |
|
242 \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}% |
|
243 \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}% |
|
244 \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}% |
|
245 \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax |
|
246 \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax |
|
247 \setbox0=\hbox {$\box1 \@@atop \box2$}% |
|
248 \dimen0=\wd0\box0 |
|
249 \box0 \hskip -\dimen0\relax |
|
250 \hbox to \dimen0 {$% |
|
251 \mathrel{\mpr@tail}\joinrel |
|
252 \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}% |
|
253 $}}} |
|
254 |
|
255 %% Old stuff should be removed in next version |
|
256 \def \mpr@@reduce #1#2{\hbox |
|
257 {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}} |
|
258 \def \mpr@@rewrite #1#2#3{\hbox |
|
259 {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}} |
|
260 \def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}} |
|
261 |
|
262 \def \mpr@empty {} |
|
263 \def \mpr@inferrule |
|
264 {\bgroup |
|
265 \ifnum \linewidth<\hsize \hsize \linewidth\fi |
|
266 \mpr@rulelineskip |
|
267 \let \and \qquad |
|
268 \let \hva \mpr@hva |
|
269 \let \@rulename \mpr@empty |
|
270 \let \@rule@options \mpr@empty |
|
271 \let \mpr@over \@@over |
|
272 \mpr@inferrule@} |
|
273 \newcommand {\mpr@inferrule@}[3][] |
|
274 {\everymath={\displaystyle}% |
|
275 \def \@test {#2}\ifx \empty \@test |
|
276 \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}% |
|
277 \else |
|
278 \def \@test {#3}\ifx \empty \@test |
|
279 \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}% |
|
280 \else |
|
281 \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}% |
|
282 \fi \fi |
|
283 \def \@test {#1}\ifx \@test\empty \box0 |
|
284 \else \vbox |
|
285 %%% Suggestion de Francois pour les etiquettes longues |
|
286 %%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi |
|
287 {\hbox {\RefTirName {#1}}\box0}\fi |
|
288 \egroup} |
|
289 |
|
290 \def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} |
|
291 |
|
292 % They are two forms |
|
293 % \inferrule [label]{[premisses}{conclusions} |
|
294 % or |
|
295 % \inferrule* [options]{[premisses}{conclusions} |
|
296 % |
|
297 % Premisses and conclusions are lists of elements separated by \\ |
|
298 % Each \\ produces a break, attempting horizontal breaks if possible, |
|
299 % and vertical breaks if needed. |
|
300 % |
|
301 % An empty element obtained by \\\\ produces a vertical break in all cases. |
|
302 % |
|
303 % The former rule is aligned on the fraction bar. |
|
304 % The optional label appears on top of the rule |
|
305 % The second form to be used in a derivation tree is aligned on the last |
|
306 % line of its conclusion |
|
307 % |
|
308 % The second form can be parameterized, using the key=val interface. The |
|
309 % folloiwng keys are recognized: |
|
310 % |
|
311 % width set the width of the rule to val |
|
312 % narrower set the width of the rule to val\hsize |
|
313 % before execute val at the beginning/left |
|
314 % lab put a label [Val] on top of the rule |
|
315 % lskip add negative skip on the right |
|
316 % left put a left label [Val] |
|
317 % Left put a left label [Val], ignoring its width |
|
318 % right put a right label [Val] |
|
319 % Right put a right label [Val], ignoring its width |
|
320 % leftskip skip negative space on the left-hand side |
|
321 % rightskip skip negative space on the right-hand side |
|
322 % vdots lift the rule by val and fill vertical space with dots |
|
323 % after execute val at the end/right |
|
324 % |
|
325 % Note that most options must come in this order to avoid strange |
|
326 % typesetting (in particular leftskip must preceed left and Left and |
|
327 % rightskip must follow Right or right; vdots must come last |
|
328 % or be only followed by rightskip. |
|
329 % |
|
330 |
|
331 %% Keys that make sence in all kinds of rules |
|
332 \def \mprset #1{\setkeys{mprset}{#1}} |
|
333 \define@key {mprset}{flushleft}[]{\mpr@centerfalse} |
|
334 \define@key {mprset}{center}[]{\mpr@centertrue} |
|
335 \define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} |
|
336 \define@key {mprset}{myfraction}[]{\let \mpr@fraction #1} |
|
337 \define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} |
|
338 |
|
339 \newbox \mpr@right |
|
340 \define@key {mpr}{flushleft}[]{\mpr@centerfalse} |
|
341 \define@key {mpr}{center}[]{\mpr@centertrue} |
|
342 \define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} |
|
343 \define@key {mpr}{myfraction}[]{\let \mpr@fraction #1} |
|
344 \define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} |
|
345 \define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax |
|
346 \advance \hsize by -\wd0\box0} |
|
347 \define@key {mpr}{width}{\hsize #1} |
|
348 \define@key {mpr}{sep}{\def\mpr@sep{#1}} |
|
349 \define@key {mpr}{before}{#1} |
|
350 \define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}} |
|
351 \define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}} |
|
352 \define@key {mpr}{narrower}{\hsize #1\hsize} |
|
353 \define@key {mpr}{leftskip}{\hskip -#1} |
|
354 \define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce} |
|
355 \define@key {mpr}{rightskip} |
|
356 {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}} |
|
357 \define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax |
|
358 \advance \hsize by -\wd0\box0} |
|
359 \define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax |
|
360 \advance \hsize by -\wd0\box0} |
|
361 \define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}} |
|
362 \define@key {mpr}{right} |
|
363 {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0 |
|
364 \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} |
|
365 \define@key {mpr}{RIGHT} |
|
366 {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0 |
|
367 \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} |
|
368 \define@key {mpr}{Right} |
|
369 {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}} |
|
370 \define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} |
|
371 \define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} |
|
372 |
|
373 \newdimen \rule@dimen |
|
374 \newcommand \mpr@inferstar@ [3][]{\setbox0 |
|
375 \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax |
|
376 \setbox \mpr@right \hbox{}% |
|
377 $\setkeys{mpr}{#1}% |
|
378 \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else |
|
379 \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi |
|
380 \box \mpr@right \mpr@vdots$} |
|
381 \setbox1 \hbox {\strut} |
|
382 \rule@dimen \dp0 \advance \rule@dimen by -\dp1 |
|
383 \raise \rule@dimen \box0} |
|
384 |
|
385 \def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}} |
|
386 \newcommand \mpr@err@skipargs[3][]{} |
|
387 \def \mpr@inferstar*{\ifmmode |
|
388 \let \@do \mpr@inferstar@ |
|
389 \else |
|
390 \let \@do \mpr@err@skipargs |
|
391 \PackageError {mathpartir} |
|
392 {\string\inferrule* can only be used in math mode}{}% |
|
393 \fi \@do} |
|
394 |
|
395 |
|
396 %%% Exports |
|
397 |
|
398 % Envirnonment mathpar |
|
399 |
|
400 \let \inferrule \mpr@infer |
|
401 |
|
402 % make a short name \infer is not already defined |
|
403 \@ifundefined {infer}{\let \infer \mpr@infer}{} |
|
404 |
|
405 \def \TirNameStyle #1{\small \textsc{#1}} |
|
406 \def \tir@name #1{\hbox {\small \TirNameStyle{#1}}} |
|
407 \let \TirName \tir@name |
|
408 \let \DefTirName \TirName |
|
409 \let \RefTirName \TirName |
|
410 |
|
411 %%% Other Exports |
|
412 |
|
413 % \let \listcons \mpr@cons |
|
414 % \let \listsnoc \mpr@snoc |
|
415 % \let \listhead \mpr@head |
|
416 % \let \listmake \mpr@makelist |
|
417 |
|
418 |
|
419 |
|
420 |
|
421 \endinput |
|