From 5186e33c6d218e9003f3da20bedfa840c1765d27 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Tue, 3 Feb 2015 23:39:18 +0000 Subject: ebproof (3feb15) git-svn-id: svn://tug.org/texlive/trunk@36202 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/doc/latex/ebproof/README | 16 + Master/texmf-dist/doc/latex/ebproof/ebproof.pdf | Bin 0 -> 196387 bytes Master/texmf-dist/doc/latex/ebproof/ebproof.tex | 493 ++++++++++++++++++++++ Master/texmf-dist/tex/latex/ebproof/ebproof.sty | 537 ++++++++++++++++++++++++ Master/tlpkg/bin/tlpkg-ctan-check | 2 +- Master/tlpkg/bin/tlpkginfo | 2 +- Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc | 1 + Master/tlpkg/tlpsrc/ebproof.tlpsrc | 0 8 files changed, 1049 insertions(+), 2 deletions(-) create mode 100644 Master/texmf-dist/doc/latex/ebproof/README create mode 100644 Master/texmf-dist/doc/latex/ebproof/ebproof.pdf create mode 100644 Master/texmf-dist/doc/latex/ebproof/ebproof.tex create mode 100644 Master/texmf-dist/tex/latex/ebproof/ebproof.sty create mode 100644 Master/tlpkg/tlpsrc/ebproof.tlpsrc (limited to 'Master') diff --git a/Master/texmf-dist/doc/latex/ebproof/README b/Master/texmf-dist/doc/latex/ebproof/README new file mode 100644 index 00000000000..a64bac6f41f --- /dev/null +++ b/Master/texmf-dist/doc/latex/ebproof/README @@ -0,0 +1,16 @@ +The ebproofs package provides commands to typeset proof trees, in the style of +sequent calculus and related systems. The commands allow for writing +inferences with any number of premisses and alignment of successive formulas +on an arbitrary point. Various options allow complete control over spacing, +styles of inference rules, placement of labels, etc. + +The distribution includes the following files: + + - ebproof.sty : the package + - ebproof.pdf : the documentation + - ebproof.tex : the LaTeX source for the documentation + +The package requires pgfkeys (from TikZ/PGF) for the option system. + +This package is written by Emmanuel Beffara +It is subject to the LaTeX Project Public License. diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf new file mode 100644 index 00000000000..e58d9616168 Binary files /dev/null and b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf differ diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.tex b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex new file mode 100644 index 00000000000..acb05d56759 --- /dev/null +++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex @@ -0,0 +1,493 @@ +\documentclass{article} + +\DeclareRobustCommand\package[1]{\texttt{#1}} + +\title{The \package{ebproof} package} +\author{Emmanuel Beffara \\ \url{manu@beffara.org}} +\date{Version 1.0 \\ February 3, 2015} + +\usepackage{amssymb} +\usepackage{color} +\usepackage{fancyvrb} +\usepackage[a4paper]{geometry} +\usepackage[colorlinks=true,urlcolor=blue]{hyperref} +\usepackage{multicol} + +\usepackage{tikz} +\usetikzlibrary{decorations.pathmorphing} + +\usepackage{ebproof} + +\newcommand\lit[1]{\texttt{#1}} +\newcommand\cs[1]{\lit{\char`\\#1}} +\newcommand\env[1]{\lit{#1}} +\newcommand\opt[1]{\lit{#1}} +\newcommand\meta[1]{$\langle$\textit{#1}$\rangle$} +\newcommand\oarg[1]{\lit{[}\meta{#1}\lit{]}} +\newcommand\marg[1]{\lit{\{}\meta{#1}\lit{\}}} + +\newenvironment{csdoc}[1]{% + \smallbreak\noindent{#1}% + \begin{list}{}{% + \topsep=1ex% + }% + \item +}{% + \end{list}% +} + +\newenvironment{example}[1]{% + \def\exampleoptions{#1}% + \VerbatimOut{example.tex}}{% + \endVerbatimOut + \begin{center} + \begin{minipage}{.4\textwidth} + \input{example.tex} + \end{minipage}% + \begin{minipage}{.6\textwidth} + \small + \expandafter\VerbatimInput\expandafter[\exampleoptions]{example.tex} + \end{minipage}% + \end{center} +} + +\setcounter{tocdepth}{2} + +\begin{document} +\maketitle + +\begin{multicols}{2} + \tableofcontents +\end{multicols} + +\section{Introduction} + +The \env{ebproof} package provides commands to typeset proof trees, in the +style of sequent calculus and related systems: + +\begin{example}{gobble=2} + \begin{prooftree} + \Hypo{ \Gamma, A &\vdash B } + \Infer1[abs]{ \Gamma &\vdash A\to B } + \Hypo{ \Gamma \vdash A } + \Infer2[app]{ \Gamma \vdash B } + \end{prooftree} +\end{example} + +The structure is very much inspired by the +\href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\package{bussproofs}} +package, in particular for the postfix notation. +I actually wrote \package{ebproof} because there were some limitations in +\package{bussproofs} that I did not know how to lift, and also because I did +not like some choices in that package (and also because it was fun to write). + +\section{Environments} + +The package provides the \env{prooftree} environment, in a standard and +starred variants. + +\begin{csdoc}{ + \cs{begin}\lit{\{prooftree\}}\oarg{options} + \meta{statements} + \cs{end}\lit{\{prooftree\}}} + Typeset the proof tree desribed by the \meta{statements}, as described in + section~\ref{sec:statements}. + The \meta{options} provide default formatting options for the proof tree. + This environment can be used either in math mode or in text mode. + It produces a proof tree at the current position in the text flow. +\end{csdoc} + +\begin{csdoc}{ + \cs{begin}\lit{\{prooftree*\}}\oarg{options} + \meta{statements} + \cs{end}\lit{\{prooftree*\}}} + Typeset the proof centered on a line of its own; it is essentially + equivalent to wrapping the \env{prooftree} environment inside a \env{center} + environment. +\end{csdoc} + +\noindent +The starred version is used in situations when a single proof will be +displayed. +The non-starred version is useful in order to integrate the proof into some +larger structure, like two parts of a formula: + +\begin{example}{gobble=2} + \[ + \begin{prooftree} + \Hypo{ \vdash A } + \Hypo{ \vdash B } \Infer1{ \vdash B, C } + \Infer2{ \vdash A\wedge B, C } + \end{prooftree} + \quad \rightsquigarrow \quad + \begin{prooftree} + \Hypo{ \vdash A } \Hypo{ \vdash B } + \Infer2{ \vdash A\wedge B } + \Infer1{ \vdash A\wedge B, C } + \end{prooftree} + \] +\end{example} + +\section{Statements} +\label{sec:statements} + +Statements describes proofs in postfix notation: when typesetting a proof tree +whose last rule has, say, two premisses, you will first write statements for +the subtree of the first premiss, then statements for the subtree of the +second premiss, then a statement like \cs{Infer2}\{\meta{conclusion}\} to +build an inference with these two subtrees as premisses and the given text as +conclusion. + +Hence statements operate on a stack of proof trees. +At the beginning of a \lit{prooftree} environment, the stack is empty. +At the end, it must contain exactly one tree, which is the one that will be +printed. + +\subsection{Basic statements} + +The basic statements for building proofs are the following, where +\meta{options} stands for arbitrary options as described in +section~\ref{sec:options}. +\begin{csdoc}{\cs{Hypo}\oarg{options}\marg{text}} + Push a new proof tree consisting only in one conclusion line, with no + premiss and no line above, in other words a tree with only a leaf + (\cs{Hypo} stands for \emph{hypothesis}). +\end{csdoc} +\begin{csdoc}{\cs{Infer}\oarg{options}\marg{arity}\oarg{label}\marg{text}} + Build an inference step by taking some proof trees from the top of the + stack, assembling them with a rule joining their conclusions and putting a + new conclusion below. + The \meta{arity} is the number of sub-proofs, it may be any number + including 0 (in this case there will be a line above the conclusion but no + sub-proof). + If \meta{label} is present, it is used as the label on the right of the + inference line; it is equivalent to using the \opt{right label} option. +\end{csdoc} + +The \meta{text} in these statements is the contents of the conclusion at the +root of the tree that the statements create. +It is typeset in math mode by default but any kind of formatting can be used +instead, using the \opt{template} option. +The \meta{label} text is formatted in horizontal text mode by default. + +Each proof tree has a vertical axis, used for alignment of successive steps. +The position of the axis is deduced from the text of the conclusion at the +root of the tree: if \meta{text} contains the alignment character \verb|&| +then the axis is set at that position, otherwise the axis is set at the center +of the conclusion text. +The \cs{Infer} statement makes sure that the axis of the premiss is at the +same position as the axis of the conclusion. +If there are several premisses, it places the axis at the center between the +left of the leftmost conclusion and the right of the rightmost conclusion: + +\begin{example}{gobble=2} + \begin{prooftree} + \Hypo{ &\vdash A, B, C } + \Infer1{ A &\vdash B, C } + \Infer1{ A, B &\vdash C } + \Hypo{ D &\vdash E } + \Infer2{ A, B, D &\vdash C, E } + \Infer1{ A, B &\vdash C, D, E } + \Infer1{ A &\vdash B, C, D, E } + \end{prooftree} +\end{example} + +\subsection{Additional statements} + +The following additional statements may be used to affect the format of the +last proof tree on the stack: + +\begin{csdoc}{\cs{Ellipsis}\marg{label}\marg{text}} + Typeset vertical dots, with a label on the right, and a new conclusion. + No inference lines are inserted. + \begin{example}{gobble=4} + \begin{prooftree} + \Hypo{ \Gamma &\vdash A } + \Ellipsis{foo}{ \Gamma &\vdash A, B } + \end{prooftree} + \end{example} +\end{csdoc} + +\begin{csdoc}{\cs{Alter}\marg{code}} + Modify the proof with arbitrary commands, assuming that these commands do + not affect the size. + The \meta{code} is executed in an \cs{hbox} and is followed by the insertion + of the actual box with the current sub-proof. + It is mostly useful with \cs{color} commands: + \begin{example}{gobble=4} + \begin{prooftree} + \Hypo{ \Gamma, A &\vdash B } + \Infer1[abs]{ \Gamma &\vdash A\to B } + \Alter{\color{red}} + \Hypo{ \Gamma \vdash A } + \Infer2[app]{ \Gamma \vdash B } + \end{prooftree} + \end{example} +\end{csdoc} + +\begin{csdoc}{\cs{Delims}\marg{left}\marg{right}} + Put left and right delimiters around the whole sub-proof, without changing + the alignment (the spacing is affected by the delimiters, however). + The \meta{left} text must contain an opening occurrence of \cs{left} and the + \meta{right} text must contain a matching occurrence of \cs{right}. + For instance, \verb|\Delims{\left(}{\right)}| will put the + sub-proof between parentheses. + \begin{example}{gobble=4} + \begin{prooftree} + \Hypo{ A_1 \vee \cdots \vee A_n } + \Hypo{ [A_i] } + \Ellipsis{}{ B } + \Delims{ \left( }{ \right)_{1\leq i\leq n} } + \Infer2{ B } + \end{prooftree} + \end{example} +\end{csdoc} + +\section{Options} +\label{sec:options} + +The formatting of trees, conclusion texts and inference rules is affected by +options, specfied using the key-value system of PGF/TikZ, provided by the +\package{pgfkeys} package. +All options are in the \lit{/ebproof/} path in the key tree of +\package{pgfkeys}. +They can be set locally for a proof tree or for a single statement using +optional arguments in the associated commands. + +\begin{csdoc}{\cs{ebproofset}\marg{options}} + Set some options. + The options will apply in the current scope; using this in preamble will + effectively set options globally. + Specific options may also be specified for each proof tree and for each + statement in a proof tree, using optional arguments. +\end{csdoc} + +\subsection{General shape} + +The options in this section only make sense at the global level and at the +proof level. +Changing the proof style inside a \lit{proof} environment has undefined +behaviour. + +\begin{csdoc}{\opt{proof style=}\meta{name}} + Set the general shape for representing proofs. + The following styles are provided: + \begin{csdoc}{\lit{upwards}} + This is the default style. + Proof trees grow upwards, with conclusions below and premisses above. + \end{csdoc} + \begin{csdoc}{\lit{downwards}} + Proof trees grow downwards, with conclusions above and premisses below. + \begin{example}{gobble=4} + \begin{prooftree}[proof style=downwards] + \Hypo{ \Gamma, A &\vdash B } + \Infer1[abs]{ \Gamma &\vdash A\to B } + \Hypo{ \Gamma \vdash A } + \Infer2[app]{ \Gamma \vdash B } + \end{prooftree} + \end{example} + \end{csdoc} +\end{csdoc} + +In the optional argument of \lit{prooftree} environments, proof styles can +be specified directly, without prefixing the name by ``\lit{proof style=}''. +For instance, the first line of the example above could be written +\cs{begin}\lit{\{prooftree\}[downwards]} equivalently. + +\begin{csdoc}{\opt{center=}\meta{boolean}} + If set to \lit{true}, the tree produced by the \env{prooftree} environment + will be vertically centered around the text line. + If set to \lit{false}, the base line of the tree will be the base line of + the conclusion. + The default value is \lit{true}. + \begin{example}{gobble=4} + \begin{prooftree}[center=false] + \Infer0{ A \vdash A } + \end{prooftree} + \qquad + \begin{prooftree}[center=false] + \Hypo{ \Gamma, A \vdash B } + \Infer1{ \Gamma \vdash A \to B } + \end{prooftree} + \end{example} +\end{csdoc} + +\subsection{Spacing} + +\begin{csdoc}{\opt{separation=}\meta{dimension}} + The horizontal separation between sub-proofs in an inference. + The default value is \lit{1.5em}. + \begin{example}{gobble=4} + \begin{prooftree}[separation=0.5em] + \Hypo{ A } \Hypo{ B } \Infer2{ C } + \Hypo{ D } \Hypo{ E } \Hypo{ F } \Infer3{ G } + \Hypo{ H } \Infer[separation=3em]3{ K } + \end{prooftree} + \end{example} +\end{csdoc} + +\begin{csdoc}{\opt{rule margin=}\meta{dimension}} + The spacing above and below inference lines. + The default value is \lit{0.7ex}. + \begin{example}{gobble=4} + \begin{prooftree}[rule margin=2ex] + \Hypo{ \Gamma, A &\vdash B } + \Infer1[abs]{ \Gamma &\vdash A\to B } + \Hypo{ \Gamma \vdash A } + \Infer2[app]{ \Gamma \vdash B } + \end{prooftree} + \end{example} +\end{csdoc} + +\subsection{Shape of inference lines} + +\begin{csdoc}{\opt{rule style=}\meta{name}} + Set the shape of inference lines. + The following values are provided: + \begin{csdoc}{\opt{simple}} + A simple horizontal rule is drawn. + This is the default style. + \end{csdoc} + \begin{csdoc}{\opt{no rule}} + No inference line is drawn. + A single space of the length of \lit{rule margin} is inserted. + \end{csdoc} + \begin{csdoc}{\opt{double}} + A double line is drawn. + \end{csdoc} + \begin{csdoc}{\opt{dashed}} + A single dashed line is drawn. + \end{csdoc} + The precise rendering is influenced by parameters specified below. + Arbitrary new shapes can defined using the \lit{rule code} option described + afterwards. +\end{csdoc} + +In the optional argument of the \cs{Infer} statement, rule styles can be +specified directly, without prefixing the style name by ``\lit{rule style=}''. +For instance, \cs{Infer}\lit{[dashed]} is equivalent to +\cs{Infer}\lit{[rule style=dashed]}. + +\begin{example}{gobble=2} + \begin{prooftree} + \Hypo{ \Gamma &\vdash A \to B } + \Infer[no rule]1{ \Gamma &\vdash {!A} \multimap B } + \Hypo{ \Delta &\vdash A } + \Infer[rule thickness=2pt]1{ \Delta &\vdash {!A} } + \Infer0{ B \vdash B } + \Infer[dashed]2{ \Delta, {!A}\multimap B \vdash B } + \Infer2{ \Gamma, \Delta &\vdash B } + \Infer[double]1{ \Gamma \cup \Delta &\vdash B } + \end{prooftree} +\end{example} + +\begin{csdoc}{\opt{rule thickness=}\meta{dimension}} + The thickness of inference lines. + It is \lit{0.4pt} by default. +\end{csdoc} +\begin{csdoc}{\opt{rule separation=}\meta{dimension}} + The distance between the two lines in the \lit{double} rule style. + It is \lit{2pt} by default. +\end{csdoc} +\begin{csdoc}{\opt{rule dash length=}\meta{dimension}} + The length of dashes in the \lit{dashed} rule style. + It is \lit{0.2em} by default. +\end{csdoc} +\begin{csdoc}{\opt{rule dash space=}\meta{dimension}} + The space between dashes in the \lit{dashed} rule style. + It is \lit{0.3em} by default. +\end{csdoc} + +\begin{csdoc}{\opt{rule code=}\meta{code}} + This option is used to define an arbitrary shape for rules. + The \meta{code} is used to render the rule, it is executed in vertical mode + in a \cs{vbox} whose \cs{hsize} is set to the width of the rule. + Margins above and below are inserted automatically (they can be removed by + setting \lit{rule margin} to \lit{0pt}). + + \begin{example}{gobble=4} + \begin{prooftree}[rule code={\hbox{\tikz + \draw[decorate,decoration={snake,amplitude=.3ex}] + (0,0) -- (\hsize,0);}}] + \Hypo{ \Gamma &\vdash A } + \Infer1{ \Gamma &\vdash A, \ldots, A } + \Hypo{ \Delta, A, \ldots, A \vdash \Theta } + \Infer2{ \Gamma, \Delta \vdash \Theta } + \end{prooftree} + \end{example} + Note that this example requires the \package{tikz} package, with the + \package{decorations.pathmorphing} library for the \lit{snake} decoration. +\end{csdoc} + +The option \opt{rule code} is particularly useful in a ``styles'' in the sense of +\package{pgfkeys} as it allows to define new rule styles. +The allowed values for \opt{rule style} are actually defined this way. +The above example could be turned into a new rule style \lit{zigzag} with the +following command: +\begin{example}{gobble=2} + \ebproofset{ + rule style/zigzag/.style={rule code={\hbox{\tikz + \draw[decorate,decoration={snake,amplitude=.3ex}] + (0,0) -- (\hsize,0);}}}} + \begin{prooftree} + \Hypo{ \Gamma &\vdash A } + \Infer1{ \Gamma &\vdash A, \ldots, A } + \Hypo{ \Delta, A, \ldots, A \vdash \Theta } + \Infer[zigzag]2{ \Gamma, \Delta \vdash \Theta } + \end{prooftree} +\end{example} + +\subsection{Format of conclusions} + +\begin{csdoc}{% + \opt{template=}\meta{macro} \\ + \opt{left template=}\meta{macro} \\ + \opt{right template=}\meta{macro}} + Defines how conclusions are formatted. + The macros are arbitrary \TeX\ code, composed in horizontal mode, with the + macro argument \verb|#1| standing for the actual text passed to the + \cs{Hypo} and \cs{Infer} statements. + The \opt{template} value is used for conclusions with no alignment mark. + The \opt{left template} and \opt{right template} values are used on the left + and right side of the alignment mark when it is present. + The default value for \opt{template} is simply \verb|$#1$|, so that + conclusions are set in math mode. + The default values for \opt{left template} and \opt{right template} are + similar, with spacing assuming that a relation symbol is put near the + alignment mark, so that \verb|\Infer1{A &\vdash B}| is spaced correctly. + + \begin{example}{gobble=4} + \begin{prooftree}[template=(\textbf{#1})] + \Hypo{ foo } + \Hypo{ bar } + \Infer1{ baz } + \Infer2{ quux } + \end{prooftree} + \end{example} +\end{csdoc} + +\subsection{Format of labels} + +\begin{csdoc}{% + \opt{left label=}\meta{text} \\ + \opt{right label=}\meta{text}} + The text to use as the labels of the rules, on the left and on the right + of the inference line. + Using the second optional argument in \cs{Infer} is equivalent to setting + the \env{right label} option with the value of that argument. +\end{csdoc} +\begin{csdoc}{% + \opt{left label template=}\meta{macro} \\ + \opt{right label template=}\meta{macro}} + These macros are used to typeset the text of labels on the left and right of + inference lines. + The default values are \verb|#1| so that labels are set in plain text mode. +\end{csdoc} + +\begin{csdoc}{\opt{label separation=}\meta{dimension}} + The spacing between an inference lines and its labels. + The default value is \lit{0.5em}. +\end{csdoc} + + +\end{document} diff --git a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty new file mode 100644 index 00000000000..e8018884a29 --- /dev/null +++ b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty @@ -0,0 +1,537 @@ +% This package contains macros for typesetting proof trees. + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{ebproof}[2015/02/03 v1.0 EB's proof trees] + +% The |pgfkeys| package is used for the parameters in proof construction. +% The |ifthen| package is used for some tests. + +\RequirePackage{pgfkeys} +\RequirePackage{ifthen} + +%%% Registers and internal parameters + +\newbox\ebproof@leftbox +\newbox\ebproof@rightbox +\newif\ifebproof@updown \ebproof@updownfalse +\newif\ifebproof@center \ebproof@centertrue + +\def\ebproof@template#1{$#1$} +\def\ebproof@lefttemplate#1{$#1\mathrel{}$} +\def\ebproof@righttemplate#1{$\mathrel{}#1$} +\def\ebproof@leftlabeltemplate#1{#1} +\def\ebproof@rightlabeltemplate#1{#1} +\def\ebproof@setleftlabel{\setbox\ebproof@leftbox=\box\voidb@x} +\def\ebproof@setrightlabel{\setbox\ebproof@rightbox=\box\voidb@x} + +%%% Parameters + +\def\ebproofset#1{\pgfqkeys{/ebproof}{#1}} + +\ebproofset{ +% +% general shape +% +center/.is if=ebproof@center, +proof style/.is choice, +proof style/upwards/.code={\ebproof@updownfalse}, +proof style/downwards/.code={\ebproof@updowntrue}, +% +% spacing +% +separation/.initial=1.5em, +rule margin/.initial=.7ex, +% +% shape of inference lines +% +rule thickness/.initial=.4pt, +rule separation/.initial=2pt, +rule dash length/.initial=.2em, +rule dash space/.initial=.3em, +rule code/.initial=, +% +% templates +% +template/.code={\def\ebproof@template##1{#1}}, +left template/.code={\def\ebproof@lefttemplate##1{#1}}, +right template/.code={\def\ebproof@righttemplate##1{#1}}, +% +% labels +% +left label/.code={% + \def\ebproof@setleftlabel{% + \setbox\ebproof@leftbox=\hbox{\ebproof@leftlabeltemplate{#1}}}}, +right label/.code={% + \def\ebproof@setrightlabel{% + \setbox\ebproof@rightbox=\hbox{\ebproof@rightlabeltemplate{#1}}}}, +left label template/.code={\def\ebproof@leftlabeltemplate##1{#1}}, +right label template/.code={\def\ebproof@rightlabeltemplate##1{#1}}, +label separation/.initial=0.5em, +} + +% Rule styles + +\pgfqkeys{/ebproof/rule style}{ +.is choice, +.search also=/ebproof, +simple/.style={/ebproof/rule code={% + \hrule height \pgfkeysvalueof{/ebproof/rule thickness}\relax + }}, +% +no rule/.style={/ebproof/rule code=}, +% +double/.style={/ebproof/rule code={% + \hrule height \pgfkeysvalueof{/ebproof/rule thickness} + \kern\pgfkeysvalueof{/ebproof/rule separation}% + \hrule height \pgfkeysvalueof{/ebproof/rule thickness} + }}, +% +dashed/.style={/ebproof/rule code={% + \hbox to \hsize{% + \@tempdima=\pgfkeysvalueof{/ebproof/rule dash space}% + \divide\@tempdima2% + \kern-\@tempdima% + \cleaders\hbox{% + \kern\@tempdima% + \vrule + height \pgfkeysvalueof{/ebproof/rule thickness} + width \pgfkeysvalueof{/ebproof/rule dash length}% + \kern\@tempdima + }\hfill + \kern-\@tempdima + }% + }}, +% +simple % use the 'simple' rule style by default +} + +%%% Storage + +% Proof trees are represented as a data structure that consists of the +% following data: +% +% - box : the tree itself, as a box, with the base line on that of +% the conclusion +% - left : the distance from the left of the box to the left of the +% conclusion +% - right : the distance from the right of the box to the right of the +% conclusion +% - axis : the distance from the left of the box to the vertical axis +% of the conclusion +% +% TeX does not actually provide data structures, so we have to encode things. +% First we provide local allocators, for temporary allocation of registers in +% a group. Dimensions are initialized to 0pt. + +\def\ebproof@localdimen#1{% + \advance\count11\@ne% \count11 is the number of the last allocated \dimen + \expandafter\dimendef\csname#1\endcsname=\count11% + \csname#1\endcsname=0pt\relax} + +% For boxes, the allocator must be used as +% +% \ebproof@localbox{NAME}=\hbox{...} +% +% in order to set the value of the box. + +\def\ebproof@localbox#1{% + \advance\count14\@ne% \count14 is the number of the last allocated \box + \expandafter\chardef\csname#1\endcsname\count14% + \setbox\csname#1\endcsname} + +% From this we deduce an allocator for data structures. This allocator +% receives a base name |A| and defines the registers |\A@box|, |\A@left|, +% |\A@right| and |\A@axis|. The macro is used like |\ebproof@localbox|, by +% providing a value for the box. + +\def\ebproof@alloc#1{% + \ebproof@localdimen{#1@left}% + \ebproof@localdimen{#1@right}% + \ebproof@localdimen{#1@axis}% + \ebproof@localbox{#1@box}} + +% Logically, such structures are stored on a stack. However, TeX does not +% provide data structures, so we encode them using what we actually have. A +% stack for boxes is implemented using a global hbox |\ebproof@box@stack| that +% contains all the boxes successively, and the |\lastbox| primitive allows us +% to pop elements from there. A macro |\ebproof@stack| is used to store the +% dimensions textually: the empty stack is an empty macro, and a non-empty +% stack is represented as |{left}{right}{axis}{tail}|. We maintain a counter +% |\ebproof@level| with the number of elements on the stack, for consistency +% checks. + +\newcount\ebproof@level +\newbox\ebproof@box@stack +\newbox\ebproof@box@temp + +% Clear the stack. + +\def\ebproof@clear{% + \global\ebproof@level=0% + \global\setbox\ebproof@box@stack=\box\voidb@x% + \gdef\ebproof@stack{}} + +% Push an allocated structure (by name) on the stack. + +\def\ebproof@push#1{% + \global\advance\ebproof@level1\relax + \global\setbox\ebproof@box@stack=\hbox{% + \unhbox\ebproof@box@stack\copy\csname#1@box\endcsname}% + \xdef\ebproof@stack{% + {\the\csname#1@left\endcsname}% + {\the\csname#1@right\endcsname}% + {\the\csname#1@axis\endcsname}% + {\ebproof@stack}}} + +% Allocate a structure and pop its value from the top of the stack. + +\def\ebproof@pop#1{% + \ifnum\ebproof@level>0\relax + \global\advance\ebproof@level-1\relax + \global\setbox\ebproof@box@stack=\hbox{% + \unhbox\ebproof@box@stack + \global\setbox\ebproof@box@temp=\lastbox}% + \ebproof@alloc{#1}=\box\ebproof@box@temp% + \begingroup\def\pop##1##2##3##4{\endgroup% + \csname#1@left\endcsname=##1\relax + \csname#1@right\endcsname=##2\relax + \csname#1@axis\endcsname=##3\relax + \gdef\ebproof@stack{##4}}% + \expandafter\pop\ebproof@stack + \else + \PackageError{ebproof}{% + Missing premiss in a proof tree}{}% + \ebproof@alloc{#1}=\box\voidb@x% + \fi} + + +%%% Making boxes + +% Push a box with the axis in the middle. + +\def\ebproof@pushsimple#1{% + \begingroup + \ebproof@alloc{A}=\hbox{#1}% + \A@axis=.5\wd\A@box + \ebproof@push{A}% + \endgroup} + +% Push a box made of two halves, with the axis between the halves. + +\def\ebproof@pushsplit#1#2{% + \begingroup + \ebproof@alloc{A}=\hbox{#1}% + \A@axis=\wd\A@box + \setbox\A@box=\hbox{\unhbox\A@box#2}% + \ebproof@push{A}% + \endgroup} + +% Join horizontally the two elements at the top of the stack. + +\def\ebproof@joinh{% + \begingroup + \ebproof@pop{A}% + \ebproof@pop{B}% + \ebproof@alloc{C}=\hbox{% + \box\B@box + \kern\pgfkeysvalueof{/ebproof/separation}% + \box\A@box}% + \C@left=\B@left + \C@right=\A@right + \C@axis=\wd\C@box + \advance\C@axis\B@left + \advance\C@axis-\A@right + \divide\C@axis2\relax + \ebproof@push{C}% + \endgroup} + +% An $n$-ary version of the horizontal join. + +\def\ebproof@joinh@multi#1{% + \begingroup + \countdef\c=1 + \c=#1\relax% + \ifnum\c=0 + \ebproof@alloc{X}=\hbox{}% + \ebproof@push{X}% + \else + \ebproof@joinh@loop + \fi + \endgroup} +\def\ebproof@joinh@loop{% + \ifnum\c>1 + \ebproof@joinh + \advance\c-1 + \expandafter\ebproof@joinh@loop + \fi} + +% Append the last element to the right of the previous one, without changing +% its alignment. + +\def\ebproof@joinright{% + \begingroup + \ebproof@pop{A}% + \ebproof@pop{B}% + \ebproof@alloc{C}=\hbox{% + \box\B@box + \kern\pgfkeysvalueof{/ebproof/separation}% + \copy\A@box}% + \C@left=\B@left + \C@right=\B@right + \advance\C@right\wd\A@box + \advance\C@right\pgfkeysvalueof{/ebproof/separation}% + \ebproof@push{C}% + \endgroup} + +% Join vertically the two elements at the top of the stack, with a horizontal +% rule of the appropriate size. + +\def\ebproof@joinv{% + \begingroup + \ebproof@setleftlabel + \ebproof@setrightlabel + \ebproof@pop{A}% + \ebproof@pop{B}% + % + \ebproof@alloc{C}=\box\voidb@x% + \ebproof@localdimen{A@shift}% + \ebproof@localdimen{B@shift}% + \ebproof@localdimen{R@shift}% + \ebproof@localdimen{R@raise}% + \ebproof@localdimen{R@width}% + \ebproof@localdimen{C@width}% + \ebproof@localdimen{tmp}% + % + % The placement of the boxes and the axis of the result + \ifdim\A@axis>\B@axis + \A@shift=0pt% + \B@shift=\A@axis + \advance\B@shift-\B@axis + \C@axis=\A@axis + \else + \A@shift=\B@axis + \advance\A@shift-\A@axis + \B@shift=0pt% + \C@axis=\B@axis + \fi + % The paddings of the result + \C@left=\A@left + \advance\C@left\A@shift + \C@right=\A@right + \tmp=\wd\B@box + \advance\tmp\B@shift + \advance\tmp-\wd\A@box + \advance\tmp-\A@shift + \ifdim\tmp>0pt% + \C@width=\wd\B@box + \advance\C@width\B@shift + \advance\C@right\tmp + \else + \C@width=\wd\A@box + \advance\C@width\A@shift + \fi + % The position of the rule + \R@shift=\A@left + \advance\R@shift\A@shift + \tmp=\B@left + \advance\tmp\B@shift + \ifdim\R@shift>\tmp + \R@shift=\tmp + \fi + % The width of the rule + \R@width=\wd\A@box + \advance\R@width\A@shift + \advance\R@width-\A@right + \tmp=\wd\B@box + \advance\tmp\B@shift + \advance\tmp-\B@right + \ifdim\tmp>\R@width + \R@width=\tmp + \fi + \advance\R@width-\R@shift + % Make the rule box + \ebproof@localbox{R@box}=\vbox{% + \hsize=\R@width + \hrule width \R@width height 0pt\relax + \kern\pgfkeysvalueof{/ebproof/rule margin}% + \pgfkeysgetvalue{/ebproof/rule code}{\@rulecode}% + \ifx\@rulecode\@empty\else + \@rulecode + \unskip% so that only one margin is inserted if no rule is drawn + \kern\pgfkeysvalueof{/ebproof/rule margin}% + \fi + }% + % Shift things if the left box is wider than |\R@shift| + \ifvoid\ebproof@leftbox\else + \tmp=\wd\ebproof@leftbox + \advance\tmp\pgfkeysvalueof{/ebproof/label separation} + \ifdim\tmp>\R@shift + \advance\tmp-\R@shift + \advance\A@shift\tmp + \advance\B@shift\tmp + \advance\C@left\tmp + \advance\C@axis\tmp + \advance\C@width\tmp + \R@shift=0pt\relax + \else + \advance\R@shift-\tmp + \fi + \fi + % Compute how the rule box must be shifted so that labels are aligned + \ebproof@localbox{RC@box}=\hbox{$\vcenter{\copy\R@box}$}% + \R@raise=\ht\R@box + \advance\R@raise-\ht\RC@box + % Make the complete rule box + \setbox\RC@box=\hbox{% + \ifvoid\ebproof@leftbox\else + \copy\ebproof@leftbox + \kern\pgfkeysvalueof{/ebproof/label separation} + \fi + \box\RC@box + \ifvoid\ebproof@rightbox\else + \kern\pgfkeysvalueof{/ebproof/label separation} + \copy\ebproof@rightbox + \fi} + % Adapt the dimensions on the right if the total rule width is too large + \tmp=\wd\RC@box + \advance\tmp\R@shift + \ifdim\tmp>\C@width + \advance\tmp-\C@width + \advance\C@right\tmp + \fi + % Cancel the labels' height and depth + \setbox\RC@box=\hbox{\raise\R@raise\box\RC@box} + \ht\RC@box=\ht\R@box + \dp\RC@box=\dp\R@box + % Make the box + \ifebproof@updown + \setbox\C@box=\vtop{% + \moveright\A@shift\box\A@box + \hrule height 0pt + \moveright\R@shift\box\RC@box% + \hrule height 0pt + \moveright\B@shift\box\B@box}% + \else + \setbox\C@box=\vbox{% + \moveright\B@shift\box\B@box + \hrule height 0pt + \moveright\R@shift\box\RC@box% + \hrule height 0pt + \moveright\A@shift\box\A@box}% + \fi + \ebproof@push{C}% + \endgroup} + +%%% Modifying boxes + +% Alter a proof with a command that does not affect the size. Typically useful +% with |\color| commands. + +\def\ebproof@alter#1{% + \begingroup + \ebproof@pop{A}% + \setbox\A@box=\hbox{{#1\box\A@box}}% + \ebproof@push{A}% + \endgroup} + +% Insert |\left| and |\right| delimiters without changing the alignment + +\def\ebproof@delims#1#2{% + \begingroup + \ebproof@pop{TREE}% + \ebproof@localbox{@SHIFTED}=% + \hbox{$\vcenter{\copy\TREE@box}$}% + \ebproof@localbox{@LEFT}=% + \hbox{$#1\vrule height \ht\@SHIFTED depth \dp\@SHIFTED width 0pt\right.$}% + \ebproof@localbox{@RIGHT}=% + \hbox{$\left.\vrule height \ht\@SHIFTED depth \dp\@SHIFTED width 0pt#2$}% + \ebproof@localdimen{dy} + \dy=\dp\@SHIFTED + \advance\dy-\dp\TREE@box + \ebproof@alloc{A}=% + \hbox{\raise\dy\hbox{\copy\@LEFT\box\@SHIFTED\copy\@RIGHT}}% + \A@left=\wd\@LEFT \advance\A@left\TREE@left + \A@right=\wd\@RIGHT \advance\A@right\TREE@right + \A@axis=\wd\@LEFT \advance\A@axis\TREE@axis + \ebproof@push{A}% + \endgroup} + +%%% High-level commands + +% Push a box with default formatting, using explicit alignment if the code +% contains a |&| character + +\def\ebproof@hypo@parse#1\ebproof@hypo@stop{ + \ifthenelse{\equal{#3}{}}% + {\ebproof@pushsimple{\ebproof@template{#1}}}% + {\ebproof@pushsplit + {\ebproof@lefttemplate{#1}}% + {\ebproof@righttemplate{#2}}}} + +\newcommand\ebproof@hypo[2][]{% + {\ebproofset{#1}\ebproof@hypo@parse#2&&\ebproof@hypo@stop}} + +% Build a n-ary rule + +\def\ebproof@infer{% + \@ifnextchar[{\ebproof@infer@}{\ebproof@infer@[]}} +\def\ebproof@infer@[#1]#2{% + \@ifnextchar[{\ebproof@infer@@{#1}{#2}}{\ebproof@infer@@{#1}{#2}[]}} +\def\ebproof@infer@@#1#2[#3]#4{{% + \pgfqkeys{/ebproof/rule style}{.search also=/ebproof,#1}% + \ebproof@joinh@multi{#2}% + \ebproof@hypo{#4}% + \ifthenelse{\equal{#3}{}}{}{\ebproofset{right label={#3}}}% + \ebproof@joinv}} + +% Ellipsis with vertical dots + +\def\ebproof@ellipsis#1#2{{% + \ebproofset{rule code=}% + \ebproof@pushsplit{}{% + \setbox0=\vbox{\kern1.2ex\hbox{\ignorespaces#1}\hrule height 0pt\kern1.2ex}% + \vbox to\ht0{\xleaders\vbox to .8ex{\vss\hbox{.}\vss}\vfill}% + \rlap{ \box0}}% + \ebproof@joinv + \ebproof@hypo{#2}% + \ebproof@joinv}} + +%%% Environment interface + +\ebproof@clear + +\def\ebproof@begin{% + \edef\ebproof@start@level{\the\ebproof@level}% + \setbox1=\vbox\bgroup + \let\Hypo=\ebproof@hypo + \let\Infer=\ebproof@infer + \let\Ellipsis=\ebproof@ellipsis + \let\Alter=\ebproof@alter + \let\Delims=\ebproof@delims} +\def\ebproof@end{% + \egroup + \ebproof@pop{X}% + \ifnum\ebproof@level=\ebproof@start@level\else + \PackageError{ebproof}{Malformed proof tree}{% + Some hypotheses were declared but not used in this tree.}% + \fi + \ifebproof@center + \hbox{$\vcenter{\hbox{\box\X@box}}$}% + \else + \box\X@box + \fi + \global\setbox\ebproof@box@temp=\box1} + +\newenvironment{prooftree}[1][]{% + \pgfqkeys{/ebproof/proof style}{.search also=/ebproof,#1}% + \leavevmode\ebproof@begin +}{% + \ebproof@end} + +\newenvironment{prooftree*}[1][]{% + \center + \pgfqkeys{/ebproof/proof style}{.search also=/ebproof,#1}% + \leavevmode\ebproof@begin +}{% + \ebproof@end + \endcenter} diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check index 648f02b01e5..2ed3e71da42 100755 --- a/Master/tlpkg/bin/tlpkg-ctan-check +++ b/Master/tlpkg/bin/tlpkg-ctan-check @@ -178,7 +178,7 @@ my @TLP_working = qw( dvdcoll dvgloss dviasm dviincl dvipdfmx-def dvipsconfig dynblocks dyntree ean ean13isbn easy easy-todo easyfig easylist - ebezier ebgaramond ebgaramond-maths ebong ebook ebsthesis + ebezier ebgaramond ebgaramond-maths ebong ebook ebproof ebsthesis ec ecc ecclesiastic ecltree eco economic ecv ed edfnotes edmac edmargin ednotes eemeir eepic efbox egameps egplot eiad eiad-ltx eijkhout einfuehrung ejpecp ekaia diff --git a/Master/tlpkg/bin/tlpkginfo b/Master/tlpkg/bin/tlpkginfo index 6e764c71d0a..2bde3b9d208 100755 --- a/Master/tlpkg/bin/tlpkginfo +++ b/Master/tlpkg/bin/tlpkginfo @@ -17,7 +17,7 @@ sub main { # erroneous or problematic tds files (when new, tell RobinF and author) $erroneous_tds = join ("|", - qw(countriesofeurope dad engpron gost hacm he-she hobby imtekda + qw(countriesofeurope dad ebproof engpron gost hacm he-she hobby imtekda mathdesign spanish sttools), ); diff --git a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc index ac29fcbef45..730d8b34f7f 100644 --- a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc +++ b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc @@ -18,6 +18,7 @@ depend commath depend concmath depend concrete depend conteq +depend ebproof depend eqnarray depend extarrows depend extpfeil diff --git a/Master/tlpkg/tlpsrc/ebproof.tlpsrc b/Master/tlpkg/tlpsrc/ebproof.tlpsrc new file mode 100644 index 00000000000..e69de29bb2d -- cgit v1.2.3