source: Papers/itp-2013/bcprules.sty @ 2631

Last change on this file since 2631 was 2610, checked in by sacerdot, 7 years ago

...

File size: 8.8 KB
Line 
1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2%%%                                                                   %%%
3%%%        BCP's latex tricks for typesetting inference rules         %%%
4%%%                                                                   %%%
5%%%                         Version 1.4                               %%%
6%%%                                                                   %%%
7%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8
9%%%
10%%% This package supports two styles of rules: named and unnamed. 
11%%% Unnamed rules are centered on the page.  Named rules are set so
12%%% that a series of them will have the rules centered in a vertical
13%%% column taking most of the page and the labels right-justified.
14%%% When a label would overlap its rule, the label is moved down. 
15%%%
16%%% The width of the column of labels can be varied using a command of the
17%%% form
18%%%
19%%%   \typicallabel{T-Arrow-I}
20%%%
21%%% The default setting is:
22%%%
23%%%   \typicallabel{}
24%%%
25%%% In other words, the column of rules takes up the whole width of
26%%% the page: rules are centered on the centerline of the text, and no
27%%% extra space is left for the labels.
28%%%
29%%% The minimum distance between a rule and its label can be altered by a
30%%% command of the form
31%%%
32%%%   \setlength{\labelminsep}{0.5em}
33%%%
34%%% (This is the default value.)
35%%%
36%%% Examples:
37%%%
38%%% An axiom with a label in the right-hand column:
39%%%
40%%%   \infax[The name]{x - x = 0}
41%%%
42%%% An inference rule with a name:
43%%%
44%%%   \infrule[Another name]
45%%%     {\mbox{false}}
46%%%     {x - x = 1}
47%%%
48%%% A rule with multiple premises on the same line:
49%%%
50%%%   \infrule[Wide premises]
51%%%     {x > 0  \andalso y > 0  \andalso z > 0}
52%%%     {x + y + z > 0}
53%%%   
54%%% A rule with several lines of premises:
55%%%
56%%%   \infrule[Long premises]
57%%%     {x > 0  \\ y > 0  \\ z > 0}
58%%%     {x + y + z > 0}
59%%%   
60%%% A rule without a name, but centered on the same vertical line as rules
61%%% and axioms with names:
62%%%
63%%%   \infrule[]
64%%%     {x - y = 5}
65%%%     {y - x = -5}
66%%%
67%%% A rule without a name, centered on the page:
68%%%
69%%%   \infrule
70%%%     {x = 5}
71%%%     {x - 1 > 0}
72%%%
73%%%
74%%% Setting the flag \indexrulestrue causes an index entry to be
75%%% generated for each named rule.
76%%%
77%%% Setting the flag \suppressrulenamestrue causes the names of all rules
78%%% to be left blank
79%%%
80%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81
82%%% A switch controlling the sizes of rule names
83\newif\ifsmallrulenames  \smallrulenamesfalse
84\newcommand{\smallrulenames}{\smallrulenamestrue}
85\newcommand{\choosernsize}[2]{\ifsmallrulenames#1\else#2\fi}
86
87%%% The font for setting inference rule names
88\newcommand{\rn}[1]{%
89  \ifmmode 
90    \mathchoice
91      {\mbox{\choosernsize{\small}{}\sc #1}}
92      {\mbox{\choosernsize{\small}{}\sc #1}}
93      {\mbox{\choosernsize{\tiny}{\small}\sc #1}}
94      {\mbox{\choosernsize{\tiny}{\tiny}\uppercase{#1}}}%
95  \else
96    \hbox{\choosernsize{\small}{}\sc #1}%
97  \fi}
98
99\newif\ifsuppressrulenames 
100\suppressrulenamesfalse
101
102\newif\ifbcprulessavespace
103\bcprulessavespacefalse
104
105\newif\ifbcprulestwocol
106\bcprulestwocolfalse
107
108%%% How to display a rule's name to the right of the rule
109\newcommand{\inflabel}[1]{%
110  \ifsuppressrulenames\else
111    \def\lab{#1}%
112    \ifx\lab\empty
113      \relax
114    \else
115      (\rn{\lab})%
116  \fi\fi
117}
118
119%%% Amount of extra space to add before and after a rule
120\newlength{\afterruleskip}
121\setlength{\afterruleskip}{\bigskipamount}
122
123%%% Minimum distance between a rule and its label
124\newlength{\labelminsep}
125\setlength{\labelminsep}{0.2em}
126
127%%% The ``typical'' width of the column of labels: labels are allowed
128%%% to project further to the left if necessary; the rules will be
129%%% centered in a column of width \linewidth - \labelcolwidth
130\newdimen\labelcolwidth
131
132%%% Set the label column width by providing a ``typical'' label --
133%%% i.e. a label of average length
134\newcommand{\typicallabel}[1]{
135  \setbox \@tempboxa \hbox{\inflabel{#1}}
136  \labelcolwidth \wd\@tempboxa
137  }
138\typicallabel{}
139
140%%% A flag controlling generation of index entries
141\newif  \ifindexrules   \indexrulesfalse
142
143%%% Allocate some temporary registers
144\newbox\@labelbox
145\newbox\rulebox
146\newdimen\ruledim
147\newdimen\labeldim
148
149%%% Put a rule and its label on the same line if this can be done
150%%% without overlapping them; otherwise, put the label on the next
151%%% line.  Put a small amount of vertical space above and below.
152\newcommand{\layoutruleverbose}[2]%
153  {\unvbox\voidb@x  % to make sure we're in vmode
154   \addvspace{\afterruleskip}%
155
156   \setbox \rulebox \hbox{$\displaystyle #2$}
157
158   \setbox \@labelbox \hbox{#1}
159   \ruledim \wd \rulebox
160   \labeldim \wd \@labelbox
161
162   %%% Will it all fit comfortably on one line?
163   \@tempdima \linewidth
164   \advance \@tempdima -\labelcolwidth
165   \ifdim \@tempdima < \ruledim
166     \@tempdima \ruledim
167   \else
168     \advance \@tempdima by \ruledim
169     \divide \@tempdima by 2
170   \fi
171   \advance \@tempdima by \labelminsep
172   \advance \@tempdima by \labeldim
173   \ifdim \@tempdima < \linewidth
174     % Yes, everything fits on a line
175     \@tempdima \linewidth
176     \advance \@tempdima -\labelcolwidth
177     \hbox to \linewidth{%
178       \hbox to \@tempdima{%
179         \hfil
180         \box\rulebox
181         \hfil}%
182       \hfill
183       \hbox to 0pt{\hss\box\@labelbox}%
184     }%
185   \else
186   %
187   % Will it all fit _UN_comfortably on one line?
188   \@tempdima 0pt
189   \advance \@tempdima by \ruledim
190   \advance \@tempdima by \labelminsep
191   \advance \@tempdima by \labeldim
192   \ifdim \@tempdima < \linewidth
193     % Yes, everything fits, but not centered
194     \hbox to \linewidth{%
195         \hfil
196         \box\rulebox
197         \hskip \labelminsep
198         \box\@labelbox}%
199   \else
200   %
201   % Better put the label on the next line
202     \@tempdima \linewidth
203     \advance \@tempdima -\labelcolwidth
204     \hbox to \linewidth{%
205       \hbox to \@tempdima{%
206          \hfil
207          \box\rulebox
208          \hfil}
209       \hfil}%
210     \penalty10000
211     \hbox to \linewidth{%
212         \hfil
213         \box\@labelbox}%
214   \fi\fi
215
216   \addvspace{\afterruleskip}%
217   \@doendpe  % use LaTeX's trick of inhibiting paragraph indent for
218              % text immediately following a rule
219   \ignorespaces
220   }
221
222% Simplified form for when there is no label
223\newcommand{\layoutrulenolabel}[1]%
224  {\unvbox\voidb@x  % to make sure we're in vmode
225   \addvspace{\afterruleskip}%
226
227   \setbox \rulebox \hbox{$\displaystyle #1$}
228
229   \@tempdima \linewidth
230   \advance \@tempdima -\labelcolwidth
231   \hbox to \@tempdima{%
232      \hfil 
233      \box\rulebox
234      \hfil}%
235
236   \addvspace{\afterruleskip}%
237   \@doendpe  % use LaTeX's trick of inhibiting paragraph indent for
238              % text immediately following a rule
239   \ignorespaces
240   }
241
242% Alternate form, for when we need to save space
243%\newcommand{\layoutruleterse}[2]%
244%  {\noindent
245%   \parbox[b]{0.5\linewidth}{\layoutruleverbose{#1}{#2}}}
246
247\newcommand{\layoutruleterse}[2]%
248  {\setbox \rulebox \hbox{$\displaystyle #2$}
249   \noindent
250   \parbox[b]{0.5\linewidth}
251    {\vspace*{0.4em} \hfill\box\rulebox\hfill~}
252   }
253
254%%% Select low-level layout driver based on \bcprulessavespace flag
255\newcommand{\layoutrule}[2]{%
256      \ifbcprulessavespace 
257        \layoutruleterse{#1}{#2}
258      \else
259        \layoutruleverbose{#1}{#2}
260      \fi
261}
262
263%%% Highlighting for new versions of rules
264\newif\ifnewrule   \newrulefalse
265\newcommand{\setrulebody}[1]{%
266  \ifnewrule
267     \@ifundefined{HIGHLIGHT}{%
268        \fbox{\ensuremath{#1}}%
269     }{%
270        \HIGHLIGHT{#1}}%
271  \else
272     #1
273  \fi
274}
275
276%%% Commands for setting axioms and rules
277\newcommand{\typesetax}[1]{%
278   \setrulebody{%
279     \begin{array}{@{}c@{}}#1\end{array}}}
280\newcommand{\typesetrule}[2]{%
281   \setrulebody{%
282      \frac{\begin{array}{@{}c@{}}#1\end{array}}%
283           {\begin{array}{@{}c@{}}#2\end{array}}}}
284
285%%% Indexing
286\newcommand{\ruleindexprefix}[1]{%
287  \gdef\ruleindexprefixstring{#1}}
288\ruleindexprefix{}
289\newcommand{\maybeindex}[1]{%
290  \ifindexrules
291    \index{\ruleindexprefixstring#1@\rn{#1}}%
292  \fi}
293
294%%% Setting axioms, with or without names
295\def\infax{\@ifnextchar[{\@infaxy}{\@infaxx}}
296\def\@infaxx#1{%
297  \ifbcprulessavespace $\typesetax{#1}$%
298  \else \layoutrulenolabel{\typesetax{#1}}%
299  \fi\newrulefalse\ignorespaces}
300\def\@infaxy[#1]{\maybeindex{#1}\@infax{\inflabel{#1}}}
301\def\@infax#1#2{\layoutrule{#1}{\typesetax{#2}}\ignorespaces}
302
303%%% Setting rules, with or without names
304\def\infrule{\@ifnextchar[{\@infruley}{\@infrulex}}
305\def\@infrulex#1#2{%
306  \ifbcprulessavespace $\typesetrule{#1}{#2}$%
307  \else \layoutrulenolabel{\typesetrule{#1}{#2}}%
308  \fi\newrulefalse\ignorespaces}
309\def\@infruley[#1]{\maybeindex{#1}\@infrule{\inflabel{#1}}}
310\def\@infrule#1#2#3{\layoutrule{#1}{\typesetrule{#2}{#3}}\ignorespaces}
311
312%%% Miscellaneous helpful definitions
313\newcommand{\andalso}{\quad\quad}
314
315% Abbreviations
316\newcommand{\infabbrev}[2]{\infax{#1 \quad\eqdef\quad #2}}
317
Note: See TracBrowser for help on using the repository browser.