| OLD | NEW |
|---|
| (Empty) | |
| 1 % proof.sty (Proof Figure Macros) |
| 2 % |
| 3 % version 3.1 (for both LaTeX 2.09 and LaTeX 2e) |
| 4 % Nov 24, 2005 |
| 5 % Copyright (C) 1990 -- 2005, Makoto Tatsuta (tatsuta@nii.ac.jp) |
| 6 % |
| 7 % This program is free software; you can redistribute it or modify |
| 8 % it under the terms of the GNU General Public License as published by |
| 9 % the Free Software Foundation; either versions 1, or (at your option) |
| 10 % any later version. |
| 11 % |
| 12 % This program is distributed in the hope that it will be useful |
| 13 % but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 14 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| 15 % GNU General Public License for more details. |
| 16 % |
| 17 % Usage: |
| 18 % In \documentstyle, specify an optional style `proof', say, |
| 19 % \documentstyle[proof]{article}. |
| 20 % |
| 21 % The following macros are available: |
| 22 % |
| 23 % In all the following macros, all the arguments such as |
| 24 % <Lowers> and <Uppers> are processed in math mode. |
| 25 % |
| 26 % \infer<Lower><Uppers> |
| 27 % draws an inference. |
| 28 % |
| 29 % Use & in <Uppers> to delimit upper formulae. |
| 30 % <Uppers> consists more than 0 formulae. |
| 31 % |
| 32 % \infer returns \hbox{ ... } or \vbox{ ... } and |
| 33 % sets \@LeftOffset and \@RightOffset globally. |
| 34 % |
| 35 % \infer[<Label>]<Lower><Uppers> |
| 36 % draws an inference labeled with <Label>. |
| 37 % |
| 38 % \infer*<Lower><Uppers> |
| 39 % draws a many step deduction. |
| 40 % |
| 41 % \infer*[<Label>]<Lower><Uppers> |
| 42 % draws a many step deduction labeled with <Label>. |
| 43 % |
| 44 % \infer=<Lower><Uppers> |
| 45 % draws a double-ruled deduction. |
| 46 % |
| 47 % \infer=[<Label>]<Lower><Uppers> |
| 48 % draws a double-ruled deduction labeled with <Label>. |
| 49 % |
| 50 % \deduce<Lower><Uppers> |
| 51 % draws an inference without a rule. |
| 52 % |
| 53 % \deduce[<Proof>]<Lower><Uppers> |
| 54 % draws a many step deduction with a proof name. |
| 55 % |
| 56 % Example: |
| 57 % If you want to write |
| 58 % B C |
| 59 % ----- |
| 60 % A D |
| 61 % ---------- |
| 62 % E |
| 63 % use |
| 64 % \infer{E}{ |
| 65 % A |
| 66 % & |
| 67 % \infer{D}{B & C} |
| 68 % } |
| 69 % |
| 70 |
| 71 % Style Parameters |
| 72 |
| 73 \newdimen\inferLineSkip \inferLineSkip=2pt |
| 74 \newdimen\inferLabelSkip \inferLabelSkip=5pt |
| 75 \def\inferTabSkip{\quad} |
| 76 |
| 77 % Variables |
| 78 |
| 79 \newdimen\@LeftOffset % global |
| 80 \newdimen\@RightOffset % global |
| 81 \newdimen\@SavedLeftOffset % safe from users |
| 82 |
| 83 \newdimen\UpperWidth |
| 84 \newdimen\LowerWidth |
| 85 \newdimen\LowerHeight |
| 86 \newdimen\UpperLeftOffset |
| 87 \newdimen\UpperRightOffset |
| 88 \newdimen\UpperCenter |
| 89 \newdimen\LowerCenter |
| 90 \newdimen\UpperAdjust |
| 91 \newdimen\RuleAdjust |
| 92 \newdimen\LowerAdjust |
| 93 \newdimen\RuleWidth |
| 94 \newdimen\HLabelAdjust |
| 95 \newdimen\VLabelAdjust |
| 96 \newdimen\WidthAdjust |
| 97 |
| 98 \newbox\@UpperPart |
| 99 \newbox\@LowerPart |
| 100 \newbox\@LabelPart |
| 101 \newbox\ResultBox |
| 102 |
| 103 % Flags |
| 104 |
| 105 \newif\if@inferRule % whether \@infer draws a rule. |
| 106 \newif\if@DoubleRule % whether \@infer draws doulbe rules. |
| 107 \newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset. |
| 108 |
| 109 % Special Fonts |
| 110 |
| 111 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@ |
| 112 \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}} |
| 113 |
| 114 % Macros |
| 115 |
| 116 % Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch. |
| 117 |
| 118 \def\@IFnextchar#1#2#3{% |
| 119 \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet |
| 120 \reserved@c\@IFnch} |
| 121 \def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch |
| 122 \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else |
| 123 \let\reserved@d\reserved@b\fi |
| 124 \fi \reserved@d} |
| 125 |
| 126 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax |
| 127 \ifx \@tempa \@tempb #2\else #3\fi } |
| 128 |
| 129 \def\infer{\@IFnextchar *{\@inferSteps}{\relax |
| 130 \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}} |
| 131 |
| 132 \def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse |
| 133 \@IFnextchar [{\@infer}{\@infer[\@empty]}} |
| 134 |
| 135 \def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue |
| 136 \@IFnextchar [{\@infer}{\@infer[\@empty]}} |
| 137 |
| 138 \def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}} |
| 139 |
| 140 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]} |
| 141 |
| 142 \def\deduce{\@IFnextchar [{\@deduce{\@empty}} |
| 143 {\@inferRulefalse \@infer[\@empty]}} |
| 144 |
| 145 % \@deduce<Proof Label>[<Proof>]<Lower><Uppers> |
| 146 |
| 147 \def\@deduce#1[#2]#3#4{\@inferRulefalse |
| 148 \@infer[\@empty]{#3}{\@infer[{#1}]{#2}{#4}}} |
| 149 |
| 150 % \@infer[<Label>]<Lower><Uppers> |
| 151 % If \@inferRuletrue, it draws a rule and <Label> is right to |
| 152 % a rule. In this case, if \@DoubleRuletrue, it draws |
| 153 % double rules. |
| 154 % |
| 155 % Otherwise, draws no rule and <Label> is right to <Lower>. |
| 156 |
| 157 \def\@infer[#1]#2#3{\relax |
| 158 % Get parameters |
| 159 \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi |
| 160 \setbox\@LabelPart=\hbox{$#1$}\relax |
| 161 \setbox\@LowerPart=\hbox{$#2$}\relax |
| 162 % |
| 163 \global\@LeftOffset=0pt |
| 164 \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax |
| 165 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&& |
| 166 \inferTabSkip |
| 167 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr |
| 168 #3\cr}}\relax |
| 169 \UpperLeftOffset=\@LeftOffset |
| 170 \UpperRightOffset=\@RightOffset |
| 171 % Calculate Adjustments |
| 172 \LowerWidth=\wd\@LowerPart |
| 173 \LowerHeight=\ht\@LowerPart |
| 174 \LowerCenter=0.5\LowerWidth |
| 175 % |
| 176 \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset |
| 177 \advance\UpperWidth by -\UpperRightOffset |
| 178 \UpperCenter=\UpperLeftOffset |
| 179 \advance\UpperCenter by 0.5\UpperWidth |
| 180 % |
| 181 \ifdim \UpperWidth > \LowerWidth |
| 182 % \UpperCenter > \LowerCenter |
| 183 \UpperAdjust=0pt |
| 184 \RuleAdjust=\UpperLeftOffset |
| 185 \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter |
| 186 \RuleWidth=\UpperWidth |
| 187 \global\@LeftOffset=\LowerAdjust |
| 188 % |
| 189 \else % \UpperWidth <= \LowerWidth |
| 190 \ifdim \UpperCenter > \LowerCenter |
| 191 % |
| 192 \UpperAdjust=0pt |
| 193 \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter |
| 194 \LowerAdjust=\RuleAdjust |
| 195 \RuleWidth=\LowerWidth |
| 196 \global\@LeftOffset=\LowerAdjust |
| 197 % |
| 198 \else % \UpperWidth <= \LowerWidth |
| 199 % \UpperCenter <= \LowerCenter |
| 200 % |
| 201 \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter |
| 202 \RuleAdjust=0pt |
| 203 \LowerAdjust=0pt |
| 204 \RuleWidth=\LowerWidth |
| 205 \global\@LeftOffset=0pt |
| 206 % |
| 207 \fi\fi |
| 208 % Make a box |
| 209 \if@inferRule |
| 210 % |
| 211 \setbox\ResultBox=\vbox{ |
| 212 \moveright \UpperAdjust \box\@UpperPart |
| 213 \nointerlineskip \kern\inferLineSkip |
| 214 \if@DoubleRule |
| 215 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth |
| 216 \kern 1pt\hrule width\RuleWidth}\relax |
| 217 \else |
| 218 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax |
| 219 \fi |
| 220 \nointerlineskip \kern\inferLineSkip |
| 221 \moveright \LowerAdjust \box\@LowerPart }\relax |
| 222 % |
| 223 \@ifEmpty{#1}{}{\relax |
| 224 % |
| 225 \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust |
| 226 \advance\HLabelAdjust by -\RuleWidth |
| 227 \WidthAdjust=\HLabelAdjust |
| 228 \advance\WidthAdjust by -\inferLabelSkip |
| 229 \advance\WidthAdjust by -\wd\@LabelPart |
| 230 \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi |
| 231 % |
| 232 \VLabelAdjust=\dp\@LabelPart |
| 233 \advance\VLabelAdjust by -\ht\@LabelPart |
| 234 \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight |
| 235 \advance\VLabelAdjust by \inferLineSkip |
| 236 % |
| 237 \setbox\ResultBox=\hbox{\box\ResultBox |
| 238 \kern -\HLabelAdjust \kern\inferLabelSkip |
| 239 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax |
| 240 % |
| 241 }\relax % end @ifEmpty |
| 242 % |
| 243 \else % \@inferRulefalse |
| 244 % |
| 245 \setbox\ResultBox=\vbox{ |
| 246 \moveright \UpperAdjust \box\@UpperPart |
| 247 \nointerlineskip \kern\inferLineSkip |
| 248 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart |
| 249 \@ifEmpty{#1}{}{\relax |
| 250 \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax |
| 251 \fi |
| 252 % |
| 253 \global\@RightOffset=\wd\ResultBox |
| 254 \global\advance\@RightOffset by -\@LeftOffset |
| 255 \global\advance\@RightOffset by -\LowerWidth |
| 256 \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi |
| 257 % |
| 258 \box\ResultBox |
| 259 } |
| OLD | NEW |
|---|
Chromium Code Reviews
Issue 1205173003:
Syntax and subtyping for strong dart (Closed)
Base URL: git@github.com:dart-lang/dev_compiler.git@master