summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/generic/tex-ewd
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2008-11-12 00:43:36 +0000
committerKarl Berry <karl@freefriends.org>2008-11-12 00:43:36 +0000
commit6d06dddb5a2041f7c07b6502a3bfa973f0d86635 (patch)
tree62f472d0a2ad901fc2c4f0faa319b6f34780f939 /Master/texmf-dist/tex/generic/tex-ewd
parente9b1b6d6533ffee4803e30a3267261699e9ae3f9 (diff)
new generic package tex-ewd (11nov08)
git-svn-id: svn://tug.org/texlive/trunk@11261 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/generic/tex-ewd')
-rw-r--r--Master/texmf-dist/tex/generic/tex-ewd/dotnot.tex182
1 files changed, 182 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/generic/tex-ewd/dotnot.tex b/Master/texmf-dist/tex/generic/tex-ewd/dotnot.tex
new file mode 100644
index 00000000000..24031e2a42a
--- /dev/null
+++ b/Master/texmf-dist/tex/generic/tex-ewd/dotnot.tex
@@ -0,0 +1,182 @@
+% These macros are based on plain TeX. Use them to typeset
+% calculational proofs and programs written in what Dijkstra called ``dot
+% notation''. Dijkstra described the proof format in EWD 1300 and
+% the programming language in ``A Discipline of Programming''.
+% Don't hesitate to contact me:
+% Wolfgang Helbig helbig@lehre.ba-stuttgart.de
+% Stauferstr. 22 http://wwwlehre.ba-stuttgart.de/~helbig
+% 71334 Waiblingen November 2008
+
+% Sets and quantified operators
+% The first two parameters are delimited by `: ', they provide the
+% the quantifier and the range. The last parameter defines the term.
+% It is delimited by `\>'. If the range is empty, the two colons will not
+% be separated by space. The quantifier may be empty to give you a set.
+
+\def\<#1: #2: #3\>{\langle #1\;:\if#2\empty\else\;#2\;\fi:\;#3\rangle}
+\let\mx\uparrow % maximum
+\let\mn\downarrow % minimum
+\let\fa\forall % universal quantifier
+\let\ex\exists % existential quantifier
+\let\su\Sigma % sum
+\def\nbr{\#} % number of
+
+% Space surrounding binary operators.
+% The lower the precedence of a operator the more space should surround it.
+% Plain TeX provides \qquad = 36u; \quad = 18u; \; = 5u; \> = 4u; \, = 3u;
+% \!=-3u where one u is em/18.
+
+% logical operators (use mxx for operator xx surrounded by space)
+\let\eq\equiv
+\def\meq{\qquad\eq\qquad} % equivalence surrounded by 36u
+\let\ff\Leftarrow % "follows from"
+\def\mff{\quad\ff\quad} % "follows from" surrounded by 18u
+\let\impl\Rightarrow
+\def\mimpl{\quad\impl\quad} % "implies" surrounded by 18u
+\let\and\land
+\def\mand{\;\,\and\;\,} % "and" surrounded by 9u
+%\let\or\lor
+\def\mor{\;\,\lor\;\,} % "or" surrounded by by 9u
+
+% For most arithmetic operators, we use what plain TeX provides, namely
+% mathrel is surrounded by 5u space (see p. 170 in The TeXbook)
+% mathbin is surrounded by 4u space
+% mathpunct is followed by 3u space
+
+% Plain TeXs classification needs some correction however.
+% ``\mathcode "cfpp'' encodes class, font family and position in the font.
+% Plain TeX treats '*' as a bin operator, we need it as an ordinary symbol.
+\mathcode`\*="0203 % class was 2 (binary)
+
+% Plain TeX treats ':' as a rel operator, we need it as an ordinary symbol.
+\mathcode`\:="003A % class was 3 (relation)
+
+% \div and \mod should be surrounded by very little space, since
+% they have a high precedence
+\def\halfthinneg{\mskip-.5\thinmuskip}
+\def\div{\mathbin{\halfthinneg\hbox{\bf div}\halfthinneg}}
+\def\mod{\mathbin{\halfthinneg\hbox{\bf mod}\halfthinneg}}
+\def\gcd{\hbox{\bf gcd}}
+
+% Indented formulas and proofs
+% A proof is a succession of formula lines and hint lines.
+
+% A formula line has one parameter which is deliminated by \\
+% Use as `\f formula \\'
+\def\f#1\\{\tabalign&&$#1$\cr} % like `\f E=mc^2\\'
+
+% A hint line has two parameters, a relational operator and a hint.
+% Use as `\h\eq {hint why the relation holds}'
+\def\h#1#2{\tabalign&$#1$&&$\{\,$#2$\,\}$\cr} % hint line
+\def\heq#1{\h\eq {#1}} % Abbreviation for `\h\eq {easily seen}'
+
+% A named formula has two parameters: The name, deliminated by
+% `:' and the formula, deliminated by `\\'.
+% Use as `\nf R1: formula \\'
+\def\nf #1:#2\\{\tabalign$#1:$&&$#2$\cr} % like `\nf Einstein: E=mc^2\\'
+
+% A numbered formula is similar, it typesets a parenthesized number at
+% the left side, e.g., `\nrf 1 E=mc^2\\'
+% Use as `\nrf 1 formula \\'
+\def\nrf #1#2\\{\tabalign(#1)&&$#2$\cr} % numbered formula
+
+% To typeset formulas, named formulas, and hints in double columns, use
+% the `d'-versions that take twice as much parameters.
+\def\dnf #1:#2\\#3:#4\\{\tabalign$#1:$&&$#2$&&$#3:$&&$#4$\cr} % named formula
+\def\df#1\\#2\\{\tabalign&&$#1$&&&&$#2$\cr} % double formula
+% Use `\dh \relax \relax = {hint}' for empty left columns
+\def\dh#1#2#3#4{\tabalign&$#1$&&\condhint{#2}&&$#3$&&$\{\,$#4$\,\}$\cr}
+\def\condhint#1{\ifx#1\relax\else$\{\,$#1$\,\}$\fi} % left column empty
+
+% Here are the alignments of (double column) formulas and hint lines.
+\def\+{\tabalign} % we don't want \outer\def
+\def\setcols{\settabs\+\qquad&\quad&\qquad&\hskip .5\hsize\hskip-5em&
+ \qquad&\quad&\qquad&\cr}
+
+% Macros for programs
+% comments are specified as `\co {some text}'
+\def\co#1{\;\{\,#1\,\}} % comment
+\def\cofl#1{\{\,#1\,\}} % comment flush left
+
+% Indententation of a program line is controlled by \& and \decind.
+% \& sets the indentation of the following lines to its current position.
+% \decind decrements the indentation level of the following lines
+\newcount\nskips % holds number of tabstops
+\def\skipn{\ifcase\nskips\def\j{&}\or\def\j{&&}\or\def\j{&&&}
+ \or\def\j{&&&&}\or\def\j{&&&&&}\or\def\j{&&&&&&}\or\def\j{&&&&&&&}
+ \else\def\j{}\fi\j} % skip nskips tabstops
+\def\skipnmone{\global\advance\nskips by -1 \skipn\global\advance\nskips by 1}
+
+% Set a tabstop, succeeding lines will be left aligned to the new tabstop.
+\def\&{$\cleartabs&\global\advance\nskips by 1$}%
+
+% Decrement indentation, succeeding lines will be left aligned to the tabstop
+% preceding the current one.
+\def\decind{$\global\advance\nskips by -1$}
+
+% The active character ^^M (end of line) both formats a program line and
+% deliminates it.
+\def\eatfirst#1{}
+\catcode`\^^M=\active %
+\def\programline#1{\ifx;#1\def\next##1^^M{\+\skipnmone\hfill$;\;$&$##1$\cr^^M}%
+ \else\ifx\eblock#1\def\next{\eblock}%
+ \else\ifx\cofl#1\def\next##1^^M{\+\skipn$\cofl{##1}$\cr^^M}%
+ \else\ifx\od#1\def\next##1^^M{\+\skipnmone\hfill$\rawod$&$##1$\decind\cr^^M}%
+ \else\ifx\FI#1\def\next##1^^M{\+\skipnmone\hfill$\rawfi$&$##1$\decind\cr^^M}%
+ \else\ifx\|#1\def\next##1^^M{\+\skipnmone\hfill$\rawbar\;\;$&$##1$\cr^^M}%
+ \else\ifx\]#1\def\next##1^^M{\+\skipnmone\hfill$]\;$&$##1$&\decind\cr^^M}%
+ \else\def\next##1^^M{\+\skipn$#1##1$\cr^^M}\fi\fi\fi\fi\fi\fi\fi\next}%
+%
+% Enclose a block of program lines between \bblock and \eblock.
+\def\bblock{\doparskip\nskips=0\catcode`\^^M=\active \let^^M=\programline }%
+\def\eblock{\catcode`\^^M=5 \setcols }%
+\catcode`\^^M=5 %
+
+% Identation is controlled automatically be some tokens as follows:
+
+% `\[', `\do', and `\IF' set a tabstop right of them and increment
+% the indent level. The corresponding closing tokens decrement the
+% indent level. The `;', the `|', the \od and the \]| tokens at the
+% beginning of a new line are typeset slightly left of the current
+% identation level.
+
+% Tokens in our programming language
+% block
+\def\[{[\;\&}
+\def\nomenclature#1{\mathbin{\hbox{\bf#1}}\>}
+\def\glocon{\nomenclature{glocon}}
+\def\glovar{\nomenclature{glovar}}
+\def\vircon{\nomenclature{vircon}}
+\def\virvar{\nomenclature{virvar}}
+\def\pricon{\nomenclature{pricon}}
+\def\privar{\nomenclature{privar}}
+\def\]{\;]\decind}
+% primitive initializing statement
+\def\vir{${\bf\ vir }$}
+\def\array{${\bf\ array}$}
+% assignment
+\def\:#1{\mathord{\>\,:\!=\>\,}} % use as `\:='
+% guarded command list
+\def\-#1{\;\;\mathord{\rightarrow}\;\;} % use as '\->'
+\def\|{\;\rawbar\;}
+% if statement
+\def\IF{\rawif\&}
+\def\FI{\;\;\rawfi\decind}
+% do statement
+\def\do{\rawdo\&}
+\def\od{\;\;\rawod\decind}
+
+% internal use
+\def\rawbar{|\hskip -1.4pt]}
+\def\rawdo{\hbox{\bf do}\;\;}
+\def\rawod{\hbox{\bf od}\;\;}
+\def\rawfi{\hbox{\bf fi}\;\;}
+\def\rawif{\hbox{\bf if}\;\;}
+
+% format definitions
+\parindent=0pt
+\parskip=6pt plus 2pt minus 2pt
+\def\unparskip{\vskip-\parskip}
+\def\doparskip{\vskip \parskip}
+\def\bi{\hfil\break\hbox{\qquad}}
+\setcols