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