12 % This program is distributed in the hope that it will be useful |
15 % This program is distributed in the hope that it will be useful |
13 % but WITHOUT ANY WARRANTY; without even the implied warranty of |
16 % but WITHOUT ANY WARRANTY; without even the implied warranty of |
14 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
17 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
15 % GNU General Public License for more details. |
18 % GNU General Public License for more details. |
16 % |
19 % |
17 % Usage: |
20 % Usage: |
18 % In \documentstyle, specify an optional style `proof', say, |
21 % In \documentstyle, specify an optional style `proof', say, |
19 % \documentstyle[proof]{article}. |
22 % \documentstyle[proof]{article}. |
20 % |
23 % |
21 % The following macros are available: |
24 % The following macros are available: |
22 % |
25 % |
23 % In all the following macros, all the arguments such as |
26 % In all the following macros, all the arguments such as |
24 % <Lowers> and <Uppers> are processed in math mode. |
27 % <Lowers> and <Uppers> are processed in math mode. |
25 % |
28 % |
26 % \infer<Lower><Uppers> |
29 % \infer<Lower><Uppers> |
27 % draws an inference. |
30 % draws an inference. |
28 % |
31 % |
29 % Use & in <Uppers> to delimit upper formulae. |
32 % Use & in <Uppers> to delimit upper formulae. |
30 % <Uppers> consists more than 0 formulae. |
33 % <Uppers> consists more than 0 formulae. |
31 % |
34 % |
32 % \infer returns \hbox{ ... } or \vbox{ ... } and |
35 % \infer returns \hbox{ ... } or \vbox{ ... } and |
33 % sets \@LeftOffset and \@RightOffset globally. |
36 % sets \@LeftOffset and \@RightOffset globally. |
34 % |
37 % |
35 % \infer[<Label>]<Lower><Uppers> |
38 % \infer[<Label>]<Lower><Uppers> |
36 % draws an inference labeled with <Label>. |
39 % draws an inference labeled with <Label>. |
37 % |
40 % |
38 % \infer*<Lower><Uppers> |
41 % \infer*<Lower><Uppers> |
39 % draws a many step deduction. |
42 % draws a many step deduction. |
40 % |
43 % |
41 % \infer*[<Label>]<Lower><Uppers> |
44 % \infer*[<Label>]<Lower><Uppers> |
42 % draws a many step deduction labeled with <Label>. |
45 % draws a many step deduction labeled with <Label>. |
43 % |
46 % |
44 % \deduce<Lower><Uppers> |
47 % \infer=<Lower><Uppers> |
45 % draws an inference without a rule. |
48 % draws a double-ruled deduction. |
46 % |
49 % |
47 % \deduce[<Proof>]<Lower><Uppers> |
50 % \infer=[<Label>]<Lower><Uppers> |
48 % draws a many step deduction with a proof name. |
51 % draws a double-ruled deduction labeled with <Label>. |
49 % |
52 % |
50 % Example: |
53 % \deduce<Lower><Uppers> |
51 % If you want to write |
54 % draws an inference without a rule. |
52 % B C |
55 % |
53 % ----- |
56 % \deduce[<Proof>]<Lower><Uppers> |
54 % A D |
57 % draws a many step deduction with a proof name. |
55 % ---------- |
58 % |
56 % E |
59 % Example: |
57 % use |
60 % If you want to write |
58 % \infer{E}{ |
61 % B C |
59 % A |
62 % ----- |
60 % & |
63 % A D |
61 % \infer{D}{B & C} |
64 % ---------- |
62 % } |
65 % E |
63 % |
66 % use |
64 |
67 % \infer{E}{ |
65 % Style Parameters |
68 % A |
66 |
69 % & |
67 \newdimen\inferLineSkip \inferLineSkip=2pt |
70 % \infer{D}{B & C} |
68 \newdimen\inferLabelSkip \inferLabelSkip=5pt |
71 % } |
|
72 % |
|
73 |
|
74 % Style Parameters |
|
75 |
|
76 \newdimen\inferLineSkip \inferLineSkip=2pt |
|
77 \newdimen\inferLabelSkip \inferLabelSkip=5pt |
69 \def\inferTabSkip{\quad} |
78 \def\inferTabSkip{\quad} |
70 |
79 |
71 % Variables |
80 % Variables |
72 |
81 |
73 \newdimen\@LeftOffset % global |
82 \newdimen\@LeftOffset % global |
74 \newdimen\@RightOffset % global |
83 \newdimen\@RightOffset % global |
75 \newdimen\@SavedLeftOffset % safe from users |
84 \newdimen\@SavedLeftOffset % safe from users |
76 |
85 |
77 \newdimen\UpperWidth |
86 \newdimen\UpperWidth |
78 \newdimen\LowerWidth |
87 \newdimen\LowerWidth |
79 \newdimen\LowerHeight |
88 \newdimen\LowerHeight |
80 \newdimen\UpperLeftOffset |
89 \newdimen\UpperLeftOffset |
92 \newbox\@UpperPart |
101 \newbox\@UpperPart |
93 \newbox\@LowerPart |
102 \newbox\@LowerPart |
94 \newbox\@LabelPart |
103 \newbox\@LabelPart |
95 \newbox\ResultBox |
104 \newbox\ResultBox |
96 |
105 |
97 % Flags |
106 % Flags |
98 |
107 |
99 \newif\if@inferRule % whether \@infer draws a rule. |
108 \newif\if@inferRule % whether \@infer draws a rule. |
100 \newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset. |
109 \newif\if@DoubleRule % whether \@infer draws doulbe rules. |
101 \newif\if@MathSaved % whether inner math mode where \infer or |
110 \newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset. |
102 % \deduce appears. |
111 \newif\if@MathSaved % whether inner math mode where \infer or |
103 |
112 % \deduce appears. |
104 % Special Fonts |
113 |
|
114 % Special Fonts |
105 |
115 |
106 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@ |
116 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@ |
107 \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}} |
117 \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}} |
108 |
118 |
109 % Math Save Macros |
119 % Math Save Macros |
110 % |
120 % |
111 % \@SaveMath is called in the very begining of toplevel macros |
121 % \@SaveMath is called in the very begining of toplevel macros |
112 % which are \infer and \deduce. |
122 % which are \infer and \deduce. |
113 % \@RestoreMath is called in the very last before toplevel macros end. |
123 % \@RestoreMath is called in the very last before toplevel macros end. |
114 % Remark \infer and \deduce ends calling \@infer. |
124 % Remark \infer and \deduce ends calling \@infer. |
115 |
125 %TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty" |
116 \def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner |
126 |
117 \relax $\relax \@MathSavedtrue \fi\fi } |
127 \def\@SaveMath{} |
118 |
128 |
119 \def\@RestoreMath{\if@MathSaved \relax $\relax\fi } |
129 \def\@RestoreMath{} |
120 |
130 |
121 % Macros |
131 % Macros |
122 |
132 |
123 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax |
133 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax |
124 \ifx \@tempa \@tempb #2\else #3\fi } |
134 \ifx \@tempa \@tempb #2\else #3\fi } |
125 |
135 |
126 \def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}} |
136 \def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax |
127 |
137 \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}} |
128 \def\@inferOneStep{\@inferRuletrue |
138 |
129 \@ifnextchar [{\@infer}{\@infer[\@empty]}} |
139 \def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse |
|
140 \@ifnextchar [{\@infer}{\@infer[\@empty]}} |
|
141 |
|
142 \def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue |
|
143 \@ifnextchar [{\@infer}{\@infer[\@empty]}} |
130 |
144 |
131 \def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}} |
145 \def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}} |
132 |
146 |
133 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]} |
147 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]} |
134 |
148 |
135 \def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}} |
149 \def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}} |
136 {\@inferRulefalse \@infer[\@empty]}} |
150 {\@inferRulefalse \@infer[\@empty]}} |
137 |
151 |
138 % \@deduce<Proof Label>[<Proof>]<Lower><Uppers> |
152 % \@deduce<Proof Label>[<Proof>]<Lower><Uppers> |
139 |
153 |
140 \def\@deduce#1[#2]#3#4{\@inferRulefalse |
154 \def\@deduce#1[#2]#3#4{\@inferRulefalse |
141 \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}} |
155 \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}} |
142 |
156 |
143 % \@infer[<Label>]<Lower><Uppers> |
157 % \@infer[<Label>]<Lower><Uppers> |
144 % If \@inferRuletrue, draws a rule and <Label> is right to |
158 % If \@inferRuletrue, it draws a rule and <Label> is right to |
145 % a rule. |
159 % a rule. In this case, if \@DoubleRuletrue, it draws |
146 % Otherwise, draws no rule and <Label> is right to <Lower>. |
160 % double rules. |
|
161 % |
|
162 % Otherwise, draws no rule and <Label> is right to <Lower>. |
147 |
163 |
148 \def\@infer[#1]#2#3{\relax |
164 \def\@infer[#1]#2#3{\relax |
149 % Get parameters |
165 % Get parameters |
150 \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi |
166 \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi |
151 \setbox\@LabelPart=\hbox{$#1$}\relax |
167 \setbox\@LabelPart=\hbox{$#1$}\relax |
152 \setbox\@LowerPart=\hbox{$#2$}\relax |
168 \setbox\@LowerPart=\hbox{$#2$}\relax |
153 % |
169 % |
154 \global\@LeftOffset=0pt |
170 \global\@LeftOffset=0pt |
155 \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax |
171 \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax |
156 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&& |
172 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&& |
157 \inferTabSkip |
173 \inferTabSkip |
158 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr |
174 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr |
159 #3\cr}}\relax |
175 #3\cr}}\relax |
160 % Here is a little trick. |
176 % Here is a little trick. |
161 % \@ReturnLeftOffsettrue(false) influences on \infer or |
177 % \@ReturnLeftOffsettrue(false) influences on \infer or |
162 % \deduce placed in ## locally |
178 % \deduce placed in ## locally |
163 % because of \@SaveMath and \@RestoreMath. |
179 % because of \@SaveMath and \@RestoreMath. |
164 \UpperLeftOffset=\@LeftOffset |
180 \UpperLeftOffset=\@LeftOffset |
165 \UpperRightOffset=\@RightOffset |
181 \UpperRightOffset=\@RightOffset |
166 % Calculate Adjustments |
182 % Calculate Adjustments |
167 \LowerWidth=\wd\@LowerPart |
183 \LowerWidth=\wd\@LowerPart |
168 \LowerHeight=\ht\@LowerPart |
184 \LowerHeight=\ht\@LowerPart |
169 \LowerCenter=0.5\LowerWidth |
185 \LowerCenter=0.5\LowerWidth |
170 % |
186 % |
171 \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset |
187 \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset |
172 \advance\UpperWidth by -\UpperRightOffset |
188 \advance\UpperWidth by -\UpperRightOffset |
173 \UpperCenter=\UpperLeftOffset |
189 \UpperCenter=\UpperLeftOffset |
174 \advance\UpperCenter by 0.5\UpperWidth |
190 \advance\UpperCenter by 0.5\UpperWidth |
175 % |
191 % |
176 \ifdim \UpperWidth > \LowerWidth |
192 \ifdim \UpperWidth > \LowerWidth |
177 % \UpperCenter > \LowerCenter |
193 % \UpperCenter > \LowerCenter |
178 \UpperAdjust=0pt |
194 \UpperAdjust=0pt |
179 \RuleAdjust=\UpperLeftOffset |
195 \RuleAdjust=\UpperLeftOffset |
180 \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter |
196 \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter |
181 \RuleWidth=\UpperWidth |
197 \RuleWidth=\UpperWidth |
182 \global\@LeftOffset=\LowerAdjust |
198 \global\@LeftOffset=\LowerAdjust |
183 % |
199 % |
184 \else % \UpperWidth <= \LowerWidth |
200 \else % \UpperWidth <= \LowerWidth |
185 \ifdim \UpperCenter > \LowerCenter |
201 \ifdim \UpperCenter > \LowerCenter |
186 % |
202 % |
187 \UpperAdjust=0pt |
203 \UpperAdjust=0pt |
188 \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter |
204 \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter |
189 \LowerAdjust=\RuleAdjust |
205 \LowerAdjust=\RuleAdjust |
190 \RuleWidth=\LowerWidth |
206 \RuleWidth=\LowerWidth |
191 \global\@LeftOffset=\LowerAdjust |
207 \global\@LeftOffset=\LowerAdjust |
192 % |
208 % |
193 \else % \UpperWidth <= \LowerWidth |
209 \else % \UpperWidth <= \LowerWidth |
194 % \UpperCenter <= \LowerCenter |
210 % \UpperCenter <= \LowerCenter |
195 % |
211 % |
196 \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter |
212 \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter |
197 \RuleAdjust=0pt |
213 \RuleAdjust=0pt |
198 \LowerAdjust=0pt |
214 \LowerAdjust=0pt |
199 \RuleWidth=\LowerWidth |
215 \RuleWidth=\LowerWidth |
200 \global\@LeftOffset=0pt |
216 \global\@LeftOffset=0pt |
201 % |
217 % |
202 \fi\fi |
218 \fi\fi |
203 % Make a box |
219 % Make a box |
204 \if@inferRule |
220 \if@inferRule |
205 % |
221 % |
206 \setbox\ResultBox=\vbox{ |
222 \setbox\ResultBox=\vbox{ |
207 \moveright \UpperAdjust \box\@UpperPart |
223 \moveright \UpperAdjust \box\@UpperPart |
208 \nointerlineskip \kern\inferLineSkip |
224 \nointerlineskip \kern\inferLineSkip |
209 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax |
225 \if@DoubleRule |
210 \nointerlineskip \kern\inferLineSkip |
226 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth |
211 \moveright \LowerAdjust \box\@LowerPart }\relax |
227 \kern 1pt\hrule width\RuleWidth}\relax |
212 % |
228 \else |
213 \@ifEmpty{#1}{}{\relax |
229 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax |
214 % |
230 \fi |
215 \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust |
231 \nointerlineskip \kern\inferLineSkip |
216 \advance\HLabelAdjust by -\RuleWidth |
232 \moveright \LowerAdjust \box\@LowerPart }\relax |
217 \WidthAdjust=\HLabelAdjust |
233 % |
218 \advance\WidthAdjust by -\inferLabelSkip |
234 \@ifEmpty{#1}{}{\relax |
219 \advance\WidthAdjust by -\wd\@LabelPart |
235 % |
220 \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi |
236 \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust |
221 % |
237 \advance\HLabelAdjust by -\RuleWidth |
222 \VLabelAdjust=\dp\@LabelPart |
238 \WidthAdjust=\HLabelAdjust |
223 \advance\VLabelAdjust by -\ht\@LabelPart |
239 \advance\WidthAdjust by -\inferLabelSkip |
224 \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight |
240 \advance\WidthAdjust by -\wd\@LabelPart |
225 \advance\VLabelAdjust by \inferLineSkip |
241 \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi |
226 % |
242 % |
227 \setbox\ResultBox=\hbox{\box\ResultBox |
243 \VLabelAdjust=\dp\@LabelPart |
228 \kern -\HLabelAdjust \kern\inferLabelSkip |
244 \advance\VLabelAdjust by -\ht\@LabelPart |
229 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax |
245 \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight |
230 % |
246 \advance\VLabelAdjust by \inferLineSkip |
231 }\relax % end @ifEmpty |
247 % |
232 % |
248 \setbox\ResultBox=\hbox{\box\ResultBox |
233 \else % \@inferRulefalse |
249 \kern -\HLabelAdjust \kern\inferLabelSkip |
234 % |
250 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax |
235 \setbox\ResultBox=\vbox{ |
251 % |
236 \moveright \UpperAdjust \box\@UpperPart |
252 }\relax % end @ifEmpty |
237 \nointerlineskip \kern\inferLineSkip |
253 % |
238 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart |
254 \else % \@inferRulefalse |
239 \@ifEmpty{#1}{}{\relax |
255 % |
240 \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax |
256 \setbox\ResultBox=\vbox{ |
241 \fi |
257 \moveright \UpperAdjust \box\@UpperPart |
242 % |
258 \nointerlineskip \kern\inferLineSkip |
243 \global\@RightOffset=\wd\ResultBox |
259 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart |
244 \global\advance\@RightOffset by -\@LeftOffset |
260 \@ifEmpty{#1}{}{\relax |
245 \global\advance\@RightOffset by -\LowerWidth |
261 \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax |
246 \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi |
262 \fi |
247 % |
263 % |
248 \box\ResultBox |
264 \global\@RightOffset=\wd\ResultBox |
249 \@RestoreMath |
265 \global\advance\@RightOffset by -\@LeftOffset |
|
266 \global\advance\@RightOffset by -\LowerWidth |
|
267 \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi |
|
268 % |
|
269 \box\ResultBox |
|
270 \@RestoreMath |
250 } |
271 } |
|
272 \endinput |