path: root/macros/latex/contrib/ebproof/ebproof.dtx

% \iffalse meta-comment
%
% Copyright (C) 2015-2020 by Emmanuel Beffara
%
% This file may be distributed and/or modified under the conditions of the
% LaTeX Project Public License, either version 1.3 of this license or (at
% your option) any later version. The latest version of this license is in:
%
%   http://www.latex-project.org/lppl.txt
%
% and version 1.3 or later is part of all distributions of LaTeX version
% 2005/12/01 or later.
%
%<*driver>
\documentclass[full]{l3doc}
\usepackage{ebproof}
\usepackage{multicol}
\usepackage{tikz}
\usetikzlibrary{decorations.pathmorphing}
\EnableCrossrefs
\newenvironment{example}{%
  \VerbatimEnvironment
  \begin{VerbatimOut}{example.tex}}{%
  \end{VerbatimOut}
  \begin{center}
  \begin{minipage}{.4\textwidth}
    \input{example.tex}
  \end{minipage}%
  \begin{minipage}{.6\textwidth}
    \small\VerbatimInput[gobble=0]{example.tex}
  \end{minipage}%
  \end{center}
}
\begin{document}
  \DocInput{\jobname.dtx}
\end{document}
%</driver>
% \fi
%
% \title{^^A
%   The \pkg{ebproof} package \\
%   Formal proofs in the style of sequent calculus^^A
% }
%
% \author{^^A
%   Emmanuel Beffara\thanks
%     {^^A
%       E-mail:  \href{mailto:manu@beffara.org}{manu@beffara.org}^^A
%     }^^A
% }
%
% \date{Version 2.1 -- Released 2020-08-19}
%
% \maketitle
%
% \setcounter{tocdepth}{2}
% \begin{multicols}{2}
% \tableofcontents
% \end{multicols}
%
% \begin{documentation}
%
% \section{Introduction}
%
% The \pkg{ebproof} package provides commands to typeset proof trees, in the
% style of sequent calculus and related systems:
%
% \begin{example}
%   \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/}{\pkg{bussproofs}}
% package, in particular for the postfix notation.
% I actually wrote \pkg{ebproof} because there were some limitations in
% \pkg{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).
%
% Any feedback is welcome, in the form of bug reports, feature requests or
% suggestions, through the web page of the project at \url{https://framagit.org/manu/ebproof}.
%
% \section{Environments}
%
% \begin{function}{prooftree,prooftree*}
%   \begin{syntax}
%     \verb|\begin{prooftree}|\oarg{options}
%     ~ \meta{statements}
%     \verb|\end{prooftree}|
%   \end{syntax}
%   The package provides the \env{prooftree} environment, in standard and
%   starred variants.
%   This typesets the proof tree described by the \meta{statements}, as
%   described in section~\ref{sec:statements}.
%   The \meta{options} provide default formatting options for the proof tree,
%   available options are described in section~\ref{sec:options}.
%
%   Following the conventions of \pkg{amsmath} for alignment environments, the
%   non-starred version produces a proof tree at the current position in the
%   text flow (it can be used in math mode or text mode) while the starred
%   version typesets the proof on a line of its own, like a displayed formula.
% \end{function}
%
% \begin{example}
%   \[
%     \begin{prooftree}
%       \infer0{ \vdash A }
%       \hypo{ \vdash B } \infer1{ \vdash B, C }
%       \infer2{ \vdash A\wedge B, C }
%     \end{prooftree}
%     \quad \rightsquigarrow \quad
%     \begin{prooftree}
%       \infer0{ \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 describe 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 \env{prooftree} environment, the stack is empty.
% At the end, it must contain exactly one tree, which is the one that will be
% printed.
%
% Note that the commands defined in this section only exist right inside
% \env{prooftree} environments.
% If you have a macro with the same name as one of the statements, for instance
% \cs{hypo}, then this macro will keep its meaning outside \env{prooftree}
% environments as well as inside the arguments of a statement.
% If you really need to access the statements in another context, you can can
% always call them by prefixing their names with \texttt{ebproof}, for instance as
% \cs{ebproofhypo}.
%
% \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{function}{\hypo}
%   \begin{syntax}
%     \cs{hypo}\oarg{options}\marg{text}
%   \end{syntax}
%   The statement \cs{hypo} pushes 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{function}
%
% \begin{function}{\infer}
%   \begin{syntax}
%     \cs{infer}\oarg{options}\meta{arity}\oarg{label}\marg{text}
%   \end{syntax}
%   The statement \cs{infer} builds 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 \cmd{right label} option.
% \end{function}
%
% \medskip
%
% 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 \cmd{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}
%   \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}
%
% \begin{function}{\ellipsis}
%   \begin{syntax}
%     \cs{ellipsis}\marg{label}\marg{text}
%   \end{syntax}
%   The statement \cs{ellipsis} typesets vertical dots, with a label on the right,
%   and a new conclusion. No inference lines are inserted.
% \end{function}
%
% \begin{example}
%   \begin{prooftree}
%     \hypo{ \Gamma &\vdash A }
%     \ellipsis{foo}{ \Gamma &\vdash A, B }
%   \end{prooftree}
% \end{example}
%
%
% \subsection{Modifying proof trees}
%
% The following additional statements may be used to affect the format of the
% last proof tree on the stack.
%
% \begin{function}{\rewrite}
%   \begin{syntax}
%     \cs{rewrite}\marg{code}
%   \end{syntax}
%   The statement \cs{rewrite} is used to modify the proof of the stack while
%   preserving its size and alignment.
%   The \meta{code} is typeset in horizontal mode, with the following control
%   sequences defined:
%   \begin{itemize}
%   \item \cs{treebox} is a box register that contains the original material,
%   \item \cs{treemark}\marg{name} expands as the position of a given mark with
%     respect to the left of the box.
%   \end{itemize}
% \end{function}
%
% A simple use of this statement is to change the color of a proof tree:
% \begin{example}
%   \begin{prooftree}
%     \hypo{ \Gamma, A &\vdash B }
%     \infer1[abs]{ \Gamma &\vdash A\to B }
%     \rewrite{\color{red}\box\treebox}
%     \hypo{ \Gamma \vdash A }
%     \infer2[app]{ \Gamma \vdash B }
%   \end{prooftree}
% \end{example}
% Note the absence of spaces inside the call to \cs{rewrite}, because spaces
% would affect the position of the tree box.
% Note also that explicit use of \cs{treebox} is required to actually draw the
% subtree.
% Not using it will effectively not render the subtree, while still reserving
% its space in the enclosing tree:
% \begin{example}
%   \begin{prooftree}
%     \hypo{ \Gamma, A &\vdash B }
%     \infer1[abs]{ \Gamma &\vdash A\to B }
%     \rewrite{}
%     \hypo{ \Gamma \vdash A }
%     \infer2[app]{ \Gamma \vdash B }
%   \end{prooftree}
% \end{example}
% This kind of manipulation is useful for instance in conjunction with the
% \pkg{beamer} package to allow revealing subtrees of a proof tree
% progressively in successive slides of a given frame.
%
% \begin{function}{\delims}
%   \begin{syntax}
%     \cs{delims}\marg{left}\marg{right}
%   \end{syntax}
%   The statement \cs{delims} puts 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.
% \end{function}
%
% \begin{example}
%   \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}
%
% \begin{function}{\overlay}
%   \begin{syntax}
%     \cs{overlay}
%   \end{syntax}
%   The statement \cs{overlay} combines the last two proofs on the stack into
%   a single one, so that their conclusions are placed at the same point.
% \end{function}
%
% \begin{example}
%   \begin{prooftree}
%     \hypo{Z}
%     \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D}
%       \rewrite{\color{blue}\box\treebox}
%     \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I}
%       \rewrite{\color{red}\box\treebox}
%     \overlay \hypo{J} \infer3{K}
%   \end{prooftree}
% \end{example}
%
% The primary use of this feature is for building animated presentations where
% a subtree in a proof has to be modified without affecting the general
% alignment of the surrounding proof. For instance, the example above could be
% used in Beamer to build successive slides in a given frame with two
% different subtrees:
%
% \begin{verbatim}
%   \begin{prooftree}
%     \hypo{Z}
%     \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D}
%       \only<2>{\rewrite{}} % erases this version on slide 2
%     \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I}
%       \only<1>{\rewrite{}} % erases this version on slide 1
%     \overlay \hypo{J} \infer3{K}
%   \end{prooftree}
% \end{verbatim}
%
% \section{Options}
% \label{sec:options}
%
% The formatting of trees, conclusion texts and inference rules is affected by
% options, specified using the \LaTeX3 key-value system.
% All options are in the \texttt{ebproof} module in the key tree.
% They can be set locally for a proof tree or for a single statement using
% optional arguments in the associated commands.
%
% \begin{function}{\ebproofset,\set}
%   \begin{syntax}
%     \cs{ebproofset}\marg{options}
%   \end{syntax}
%   The statement \cs{ebproofset} is used to set some options. When used
%   inside a \env{prooftree} environment, it can written \cs{set}.
%   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{function}
%
% \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 \env{proof} environment has undefined
% behaviour.
%
% \begin{variable}{proof style}
%   The option \cmd{proof style} sets the general shape for representing proofs.
%   The following styles are provided:
%   \begin{description}
%   \item[upwards] 
%     This is the default style.
%     Proof trees grow upwards, with conclusions below and premisses above.
%   \item[downwards]
%     Proof trees grow downwards, with conclusions above and premisses below.
%     \fvset{gobble=6}
%     \begin{example}
%       \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{description}
% \end{variable}
%
% In the optional argument of \env{prooftree} environments, proof styles can
% be specified directly, without prefixing the name by ``\texttt{proof style=}''.
% For instance, the first line of the example above could be written
% \verb|\begin{prooftree}| equivalently.
%
% \begin{variable}{center}
%   The option \cmd{center} toggles vertical centering of typeset proofs.
%   If set to \texttt{true}, the tree produced by the \env{prooftree}
%   environment will be vertically centered around the text line.
%   If set to \texttt{false}, the base line of the tree will be the base line
%   of the conclusion.
%   The default value is \texttt{true}.
% \end{variable}
%
% \begin{example}
%   \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}
%
% \subsection{Spacing}
%
% \begin{variable}{separation}
%   Horizontal separation between sub-proofs in an inference is defined by the
%   option \cmd{separation}.
%   The default value is \texttt{1.5em}.
% \end{variable}
%
% \begin{example}
%   \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}
%
% \begin{variable}{rule margin}
%   The spacing above and below inference lines is defined by the option
%   \cmd{rule margin}.
%   The default value is \texttt{0.7ex}.
% \end{variable}
%
% \begin{example}
%   \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}
%
% \subsection{Shape of inference lines}
%
% \begin{variable}{rule style}
%   The shape of inference lines is set by the option \cmd{rule style}.
%   The following values are provided:
%   \begin{center}
%     \begin{tabular}{@{}l@{\qquad}l@{}}
%       \toprule
%       \cmd{simple}  & a simple line (this is the default style) \\
%       \cmd{no rule} & no rule, only a single space of length \texttt{rule margin} \\
%       \cmd{double}  & a double line \\
%       \cmd{dashed}  & a single dashed line \\
%       \bottomrule
%     \end{tabular}
%   \end{center}
% \end{variable}
%
% The precise rendering is influenced by parameters specified below.
% Arbitrary new shapes can defined using the \cs{ebproofnewrulestyle} command
% described in section~\ref{sec:styles}, using \texttt{rule code} option
% described below.
%
% In the optional argument of the \cs{infer} statement, rule styles can be
% specified directly, without prefixing the style name by ``\texttt{rule style=}''.
% For instance, \verb|\infer[dashed]| is equivalent to
% \verb|\infer[rule style=dashed]|.
%
% \begin{example}
%   \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{variable}{rule thickness,rule separation}
%   The thickness of inference lines is defined by option \cmd{rule
%   thickness}, it is \texttt{0.4pt} by default.
%   The distance between the two lines in the \texttt{double} rule style is
%   defined by the \cmd{rule separation} option.
%   It is \texttt{2pt} by default.
% \end{variable}
% \begin{variable}{rule dash length,rule dash space}
%   For dashed rules, the length of dashes is defined by the option
%   \cmd{rule dash length} and the space between dashes is defined by the
%   option \cmd{rule dash space}.
%   The default values are \texttt{0.2em} and \texttt{0.3em} respectively.
% \end{variable}
%
% \begin{variable}{rule code}
%   Arbitrary rule shapes can be optained using the \cmd{rule code} option.
%   The argument is 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 \texttt{rule margin} to \texttt{0pt}).
% \end{variable}
%
% \begin{example}
%   \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 \pkg{tikz} package, with the
% \pkg{decorations.pathmorphing} library for the \texttt{snake} decoration.
%
% \subsection{Format of conclusions and labels}
%
% \begin{variable}{template,left template,right template}
%   The format of text in inferences is defined by templates.
%   The option \cmd{template} is used for text with no alignment mark, the
%   options \cmd{left template} and \cmd{right template} are used for the left
%   and right side of the alignment mark when it is present.
%   The value of these options is arbitrary \TeX\ code, composed in horizontal mode.
%   The macro \cs{inserttext} is used to insert the actual text passed to the
%   \cs{hypo} and \cs{infer} statements.
%   The default value for \cmd{template} is simply \verb|$\inserttext$|, so
%   that conclusions are set in math mode.
%   The default values for \cmd{left template} and \cmd{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.
% \end{variable}
%
% \begin{example}
%   \begin{prooftree}[template=(\textbf\inserttext)]
%     \hypo{ foo }
%     \hypo{ bar }
%     \infer1{ baz }
%     \infer2{ quux }
%   \end{prooftree}
% \end{example}
%
% \begin{variable}{left label,right label}
%   The text to use as the labels of the rules, on the left and on the right
%   of the inference line, is defined by the options \cmd{left label} and
%   \cmd{right label}.
%   Using the second optional argument in \cs{infer} is equivalent to setting
%   the \env{right label} option with the value of that argument.
% \end{variable}
%
% \begin{example}
%   \begin{prooftree}
%     \hypo{ \Gamma, A &\vdash B }
%     \infer[left label=$\lambda$]1[abs]
%       { \Gamma &\vdash A\to B }
%     \hypo{ \Gamma \vdash A }
%     \infer[left label=@]2[app]{ \Gamma \vdash B }
%   \end{prooftree}
% \end{example}
%
% \begin{variable}{left label template,right label template}
%   Similarly to conclusions, labels are formatted according to templates.
%   The code is arbitrary \TeX\ code, composed in horizontal mode, where the
%   macro \cs{inserttext} can be used to insert the actual label text.
%   The default values are simply \cs{inserttext} so that labels are set in
%   plain text mode.
% \end{variable}
% \begin{variable}{label separation}
%   The spacing between an inference line and its labels is defined by the
%   option \cmd{label separation}, the default value is \texttt{0.5em}.
%   The height of the horizontal axis used for aligning the labels with the
%   rules is defined by the option \cmd{label axis}, the default value is
%   \texttt{0.5ex}.
% \end{variable}
%
%
% \subsection{Style macros}
% \label{sec:styles}
%
% The following commands allow for the definition of custom styles using the
% basic style options, in a way similar to PGF's ``styles'' and \LaTeX3's
% ``meta-keys''.
% This allows setting a bunch of options with the same values in many proofs
% using a single definition.
%
% \begin{function}{\ebproofnewstyle}
%   \begin{syntax}
%     \cs{ebproofnewstyle}\marg{name}\marg{options}
%   \end{syntax}
%   The statement \cs{ebproofnewstyle} defines a new style option with some
%   \meta{name} that sets a given set of \meta{options}.
% \end{function}
% For instance, the following code defines a new option \cmd{small} that sets
% various parameters so that proofs are rendered smaller.
% \begin{example}
%   \ebproofnewstyle{small}{
%     separation = 1em, rule margin = .5ex,
%     template = \footnotesize$\inserttext$ }
%   \begin{prooftree}[small]
%     \hypo{ \Gamma, A \vdash B }
%     \infer1{ \Gamma \vdash A\to B }
%     \hypo{ \Gamma \vdash A } \infer2{ \Gamma \vdash B }
%   \end{prooftree}
% \end{example}
%
% \begin{function}{\ebproofnewrulestyle}
%   \begin{syntax}
%     \cs{ebproofnewrulestyle}\marg{name}\marg{options}
%   \end{syntax}
%   The statement \cs{ebproofnewrulestyle} does the same for rule styles.
%   The \meta{options} part includes options used to set how to draw rules in
%   the new style.
% \end{function}
%
% The option \cmd{rule code} is useful in this command as it allows to
% define arbitrary rule styles.
% For instance, the squiggly rule example above could be turned into a new
% rule style \texttt{zigzag} with the following code:
% \begin{example}
%   \ebproofnewrulestyle{zigzag}{
%     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}
%
%
% \section{License}
%
% This work may be distributed and/or modified under the
% conditions of the \LaTeX\ Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
% \begin{center}
%   \url{http://www.latex-project.org/lppl.txt}
% \end{center}
% and version 1.3 or later is part of all distributions of \LaTeX\
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status `maintained'.
%
% The Current Maintainer of this work is Emmanuel Beffara.
%
% This work consists of the files \texttt{ebproof.sty} and \texttt{ebproof.tex}.
%
% \section{History}
%
% This section lists the principal evolutions of the package, in reverse
% chronological order.
% \begin{description}
% \item[Version 2.1 (2020-08-19)]
%   Mostly a bugfix release.
%   \begin{itemize}
%   \item Makes the \env{prooftree} environment robust to use in tabular
%     contexts.
%   \item Adds the \cs{overlay} statement.
%   \item Fixes a compatibility issue with \LaTeX\ release 2020-10-01.
%   \end{itemize}
% \item[Version 2.0 (2017-05-17)]
%   A complete rewrite of the code using the \LaTeX3 programming environment. 
%   The incompatible changes from the user's point of view are the following:
%   \begin{itemize}
%   \item Proof statements are now writtten in lowercase ({i.e.} \cs{Infer} is
%     now written \cs{infer} etc.) but the syntax is otherwise unchanged.
%     The old uppercase commands still work but produce a deprecation warning,
%     they will be removed in a future version.
%   \item New styles are now defined using \cs{ebproofnewstyle} and
%     \cs{ebproofnewrulestyle}. The previous method using PGF styles does not
%     work anymore (because PGF is not used anymore).
%   \end{itemize}
%   The new commands and options are the following:
%   \begin{itemize}
%   \item The statement \cs{rewrite} generalizes \cs{Alter},
%   \item The option \cmd{label axis} controls vertical alignment of labels.
%   \end{itemize}
% \item[Version 1.1 (2015-03-13)]
%   A bugfix release.
%   In \cmd{template} options, one now uses \cs{inserttext} instead of \verb|#1|
%   for the text arguments, which improves robustness.
% \item[Version 1.0 (2015-02-04)]
%   The first public release.
% \end{description}
%
% \end{documentation}
%
% \clearpage \appendix
%
% \begin{implementation}
%
% \section{Implementation}
%
%    \begin{macrocode}
%<*package>
\NeedsTeXFormat{LaTeX2e}
\RequirePackage{expl3}
\RequirePackage{xparse}
\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees}
%<@@=ebproof>
%    \end{macrocode}
%
% \subsection{Parameters}
%
% We first declare all options. For the meaning of options, see
% section~\ref{sec:options}.
%
%    \begin{macrocode}
\keys_define:nn { ebproof } {
center .bool_set:N = \l_@@_center_bool,
proof~style .choice: ,
proof~style / upwards .code:n = \bool_set_false:N \l_@@_updown_bool,
proof~style / downwards .code:n = \bool_set_true:N \l_@@_updown_bool,
separation .dim_set:N = \l_@@_separation_dim,
rule~margin .dim_set:N = \l_@@_rule_margin_dim,
rule~thickness .dim_set:N = \l_@@_rule_thickness_dim,
rule~separation .dim_set:N = \l_@@_rule_separation_dim,
rule~dash~length .dim_set:N = \l_@@_rule_dash_length_dim,
rule~dash~space .dim_set:N = \l_@@_rule_dash_space_dim,
rule~code .tl_set:N = \l_@@_rule_code_tl,
rule~style .choice:,
template .tl_set:N = \l_@@_template_tl,
left~template .tl_set:N = \l_@@_left_template_tl,
right~template .tl_set:N = \l_@@_right_template_tl,
left~label .tl_set:N = \l_@@_left_label_tl,
right~label .tl_set:N = \l_@@_right_label_tl,
left~label~template .tl_set:N = \l_@@_left_label_template_tl,
right~label~template .tl_set:N = \l_@@_right_label_template_tl,
label~separation .dim_set:N = \l_@@_label_separation_dim,
label~axis .dim_set:N = \l_@@_label_axis_dim,
}
%    \end{macrocode}
%
% \begin{macro}{\ebproofnewrulestyle}
%   We then define the document-level macro \cs{ebproofnewrulestyle} and use
%   it to define the default styles. This simply consists in defining a
%   meta-key.
%    \begin{macrocode}
\NewDocumentCommand \ebproofnewrulestyle { mm } {
  \keys_define:nn { ebproof } {
    rule~style / #1 .meta:nn = { ebproof } { #2 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% The styles |simple|, |no rule| and |double| are defined in a straightforward
% way.
%
%    \begin{macrocode}
\ebproofnewrulestyle { simple } {
  rule~code = { \tex_hrule:D height \l_@@_rule_thickness_dim }
}
\ebproofnewrulestyle { no~rule } {
  rule~code =
}
\ebproofnewrulestyle { double } {
  rule~code = {
    \tex_hrule:D height \l_@@_rule_thickness_dim
    \skip_vertical:N \l_@@_rule_separation_dim
    \tex_hrule:D height \l_@@_rule_thickness_dim
  }
}
%    \end{macrocode}
%
% The |dashed| style uses leaders and filling for repeating a single dash. We
% use \TeX\ primitives that have no \LaTeX3 counterpart for this.
%
%    \begin{macrocode}
\ebproofnewrulestyle { dashed } {
  rule~code = {
    \hbox_to_wd:nn { \tex_hsize:D } {
      \dim_set:Nn \l_tmpa_dim { \l_@@_rule_dash_space_dim / 2 }
      \skip_horizontal:n { -\l_tmpa_dim }
      \tex_cleaders:D \hbox:n {
        \skip_horizontal:N \l_tmpa_dim
        \tex_vrule:D
          height \l_@@_rule_thickness_dim
          width \l_@@_rule_dash_length_dim
        \skip_horizontal:N \l_tmpa_dim
      } \tex_hfill:D
      \skip_horizontal:n { -\l_tmpa_dim }
    }
  }
}
%    \end{macrocode}
%
% Now we can define the default values, including the default rule style.
%
%    \begin{macrocode}
\keys_set:nn { ebproof } {
  center = true,
  proof~style = upwards,
  separation = 1.5em,
  rule~margin = .7ex,
  rule~thickness = .4pt,
  rule~separation = 2pt,
  rule~dash~length = .2em,
  rule~dash~space = .3em,
  rule~style = simple,
  template = $\inserttext$,
  left~template = $\inserttext\mathrel{}$,
  right~template = $\mathrel{}\inserttext$,
  left~label = ,
  right~label = ,
  left~label~template = \inserttext,
  right~label~template = \inserttext,
  label~separation = 0.5em,
  label~axis = 0.5ex
}
%    \end{macrocode}
%
% \begin{macro}{\ebproofnewstyle}
%   Defining a style simply means defining a meta-key.
%    \begin{macrocode}
\NewDocumentCommand \ebproofnewstyle { mm } {
  \keys_define:nn { ebproof } { #1 .meta:n = { #2 } }
}
%    \end{macrocode}
% \end{macro}
%
%
% \subsection{Proof boxes}
%
% \TeX\ does not actually provide data structures, so we have to encode things.
% We provide an allocator for ``registers'' holding boxes with attributes. Such
% a register consists in a box register and a property list for marks, which
% maps mark names to values as explicit dimensions with units.
%
% \begin{macro}{\@@_new:N}
%   Using only public interfaces forces a convoluted approach to allocation:
%   we use a global counter \cs{g_ebproof_register_int} to number registers,
%   then each allocation creates registers named \cs{g_ebproof_K_N} where K is
%   the kind of component (box or marks) and N is the identifier of the
%   register. The proof box register itself only contains the identifier used
%   for indirection.
%    \begin{macrocode}
\int_new:N \g_@@_register_int
\cs_new:Nn \@@_box:N { g__ebproof_box_ \tl_use:N #1 }
\cs_new:Nn \@@_marks:N { g__ebproof_marks_ \tl_use:N #1 }
\cs_new:Nn \@@_new:N {
  \tl_new:N #1
  \int_gincr:N \g_@@_register_int
  \tl_gset:Nx #1 { \int_to_arabic:n { \g_@@_register_int } }
  \box_new:c { \@@_box:N #1 }
  \prop_new:c { \@@_marks:N #1 }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_clear:N}
%   The box is cleared by setting it to an empty hbox.
%   Using \cs{box_clear:N} instead would not work because trying to push this
%   box on the stack would not actually append any box.
%    \begin{macrocode}
\cs_new:Nn \@@_clear:N {
  \hbox_set:cn { \@@_box:N #1 } {}
  \prop_clear:c { \@@_marks:N #1 }
  \@@_set_mark:Nnn #1 { left } { 0pt }
  \@@_set_mark:Nnn #1 { right } { 0pt }
  \@@_set_mark:Nnn #1 { axis } { 0pt }
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Mark operations}
%
% \begin{macro}{\@@_set_mark:Nnn}
%   Setting the value of a mark uses a temporary register to evaluate the
%   dimension expression because values are stored textually in a property
%   list.
%    \begin{macrocode}
\dim_new:N \l_@@_transit_dim
\cs_new:Nn \@@_set_mark:Nnn {
  \dim_set:Nn \l_@@_transit_dim { #3 }
  \prop_put:cnV { \@@_marks:N #1 } { #2 }
    \l_@@_transit_dim
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_mark:Nn}
%   Getting the value of a mark simply consists in getting an item in a
%   property list.
%    \begin{macrocode}
\cs_new:Nn \@@_mark:Nn {
  \prop_item:cn { \@@_marks:N #1 } { #2 }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_shift_x:Nn}
%   This function shifts the marks by a specified amount, without modifying
%   the box.
%    \begin{macrocode}
\cs_new:Nn \@@_shift_x:Nn {
  \prop_map_inline:cn { \@@_marks:N #1 } {
    \@@_set_mark:Nnn #1 { ##1 } { ##2 + #2 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_enlarge_conclusion:NN}
%   This function moves the left and right marks of the first tree so that
%   they are at least as far from the axis as they are in the second tree. 
%   For instance we get the following:
%   \begin{center}
%     \begin{tikzpicture}[y=-3ex]
%       \node (L1) at (1,0) {L}; \node (A1) at (2,0) {A}; \node (R1) at (4,0) {R};
%       \node (L2) at (0,1) {L}; \node (A2) at (2,1) {A}; \node (R2) at (3,1) {R};
%       \node (L3) at (0,2) {L}; \node (A3) at (2,2) {A}; \node (R3) at (4,2) {R};
%       \draw (L1) -- (A1) -- (R1);
%       \draw (L2) -- (A2) -- (R2);
%       \draw (L3) -- (A3) -- (R3);
%       \node[anchor=west] at (5,0) {box 1 before};
%       \node[anchor=west] at (5,1) {box 2 before};
%       \node[anchor=west] at (5,2) {box 1 after};
%     \end{tikzpicture}
%   \end{center}
%   The contents of the trees are unchanged.
%    \begin{macrocode}
\cs_new:Nn \@@_enlarge_conclusion:NN {
  \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis}
    + \@@_mark:Nn #2 {left} - \@@_mark:Nn #2 {axis} }
  \dim_compare:nNnT { \l_tmpa_dim } < { \@@_mark:Nn #1 {left} } {
    \@@_set_mark:Nnn #1 {left} { \l_tmpa_dim } }
  \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis}
    + \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {axis} }
  \dim_compare:nNnT { \l_tmpa_dim } > { \@@_mark:Nn #1 {right} } {
    \@@_set_mark:Nnn #1 {right} { \l_tmpa_dim } }
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Building blocks}
%
% \begin{macro}{\@@_make_simple:Nn}
%   Make a tree with explicit material in horizontal mode. Set the left and
%   right marks to extremal positions and set the axis in the middle.
%    \begin{macrocode}
\cs_new:Nn \@@_make_simple:Nn {
  \hbox_set:cn { \@@_box:N #1 } { #2 }
  \@@_set_mark:Nnn #1 { left } { 0pt }
  \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } / 2 }
  \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_make_split:Nnn}
%   Make a tree with explicit material in horizontal mode, split in two parts.
%   Set the left and right marks to extremal positions and set the axis
%   between the two parts.
%    \begin{macrocode}
\cs_new:Nn \@@_make_split:Nnn {
  \@@_set_mark:Nnn #1 { left } { 0pt }
  \hbox_set:cn { \@@_box:N #1 } { #2 }
  \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } }
  \hbox_set:cn { \@@_box:N #1 } { \hbox_unpack:c { \@@_box:N #1 } #3 }
  \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_make_vertical:Nnnn}
%   Make a tree with explicit material in vertical mode, using an explicit
%   width and axis.
%    \begin{macrocode}
\cs_new:Nn \@@_make_vertical:Nnnn {
  \@@_set_mark:Nnn #1 { left } { 0pt }
  \@@_set_mark:Nnn #1 { axis } { #2 }
  \@@_set_mark:Nnn #1 { right } { #3 }
  \vbox_set:cn { \@@_box:N #1 } {
    \dim_set:Nn \tex_hsize:D { \@@_mark:Nn #1 {right} }
    #4
  }
  \box_set_wd:cn { \@@_box:N #1 } { \@@_mark:Nn #1 {right} }
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Assembling boxes}
%
% \begin{macro}{\@@_extend:Nnnnn}
%   Extend a tree box. The marks are shifted so that alignment is preserved.
%   The arguments are dimensions for the left, top, right and bottom sides
%   respectively.
%    \begin{macrocode}
\cs_new:Nn \@@_extend:Nnnnn {
  \dim_compare:nNnF { #2 } = { 0pt } {
    \hbox_set:cn { \@@_box:N #1 } {
      \skip_horizontal:n { #2 }
      \box_use:c { \@@_box:N #1 }
    }
    \@@_shift_x:Nn #1 { #2 }
  }
  \box_set_ht:Nn #1 { \box_ht:c { \@@_box:N #1 } + #3 }
  \box_set_wd:Nn #1 { \box_wd:c { \@@_box:N #1 } + #4 }
  \box_set_dp:Nn #1 { \box_dp:c { \@@_box:N #1 } + #5 }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_append_right:NnN}
%   Append the contents of the second tree to the first one on the right, with
%   matching baselines. The marks of both trees are preserved. The middle
%   argument specifies the space to insert between boxes.
%    \begin{macrocode}
\cs_new:Nn \@@_append_right:NnN {
  \hbox_set:cn { \@@_box:N #1 } {
    \box_use:c { \@@_box:N #1 }
    \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
    \box_use:c { \@@_box:N #3 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_append_left:NnN}
%   Append the contents of the second tree to the first one on the left, with
%   matching baselines. The marks of the first tree are shifted accordingly.
%   The middle argument specifies the space to insert between boxes.
%    \begin{macrocode}
\cs_new:Nn \@@_append_left:NnN {
  \@@_shift_x:Nn #1 { \box_wd:c { \@@_box:N #3 } + #2 }
  \hbox_set:cn { \@@_box:N #1 } {
    \box_use:c { \@@_box:N #3 }
    \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
    \box_use:c { \@@_box:N #1 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_align:NN}
%   Shift one of two trees to the right so that their axes match. The marks of
%   the one that is shifted are updated accordingly.
%    \begin{macrocode}
\cs_new:Nn \@@_align:NN {
  \dim_set:Nn \l_tmpa_dim
    { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #1 {axis} }
  \dim_compare:nNnTF \l_tmpa_dim < { 0pt } {
    \@@_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt }
  } {
    \@@_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_append_above:NN}
%   Append the contents of the second tree above the first one, with matching
%   axes. The marks of the first tree are preserved.
%    \begin{macrocode}
\cs_new:Nn \@@_append_above:NN {
  \@@_align:NN #1 #2
  \vbox_set:cn  { \@@_box:N #1 } {
    \box_use:c { \@@_box:N #2 }
    \tex_prevdepth:D -1000pt
    \box_use:c { \@@_box:N #1 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_append_below:NN}
%   Append the contents of the second tree below the first one, with matching
%   axes. The marks of the first tree are preserved.
%    \begin{macrocode}
\cs_new:Nn \@@_append_below:NN {
  \@@_align:NN #1 #2
  \vbox_set_top:Nn #1 {
    \box_use:c { \@@_box:N #1 }
    \tex_prevdepth:D -1000pt
    \box_use:c { \@@_box:N #2 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_overlay:NN}
%   Append the second tree as an overlay over the first one, so that the
%   baselines and axes match. The bounding box of the result adjusts to
%   contain both trees.
%    \begin{macrocode}
\cs_new:Nn \@@_overlay:NN {
  \@@_align:NN #1 #2
  \hbox_set:cn { \@@_box:N #1 } {
    \hbox_overlap_right:n { \box_use:c { \@@_box:N #1 } }
    \box_use:c { \@@_box:N #2 }
    \dim_compare:nNnT
      { \box_wd:c { \@@_box:N #2 } } < { \box_wd:c { \@@_box:N #1 } }
      { \skip_horizontal:n
        { \box_wd:c { \@@_box:N #1 } - \box_wd:c { \@@_box:N #2 } } }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_vcenter:N}
%   Shift the material in a tree vertically so that the height and depth are
%   equal (like \TeX's \cs{vcenter} but around the baseline).
%    \begin{macrocode}
\cs_new:Nn \@@_vcenter:N {
  \dim_set:Nn \l_tmpa_dim
    { ( \box_ht:c { \@@_box:N #1 } - \box_dp:c { \@@_box:N #1 } ) / 2 }
  \box_set_eq:Nc \l_tmpa_box { \@@_box:N #1 }
  \hbox_set:cn { \@@_box:N #1 }
    { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } }
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Making inferences}
%
% The following commands use the parameters defined at the beginning of the
% package for actually building proof trees using the commands defined above.
%
% \begin{macro}{\@@_append_vertical:NN}
%   Append the contents of the second tree above or below the first one,
%   depending on current settings. Axes are aligned and the marks of the first
%   tree are preserved.
%    \begin{macrocode}
\cs_new:Nn \@@_append_vertical:NN {
  \bool_if:NTF \l_@@_updown_bool
    { \@@_append_below:NN #1 #2 }
    { \@@_append_above:NN #1 #2 }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_make_rule_for:NNN}
%   Make a box containing an inference rule with labels, using the current
%   settings. The width and axis position are taken as those of the conclusion
%   of another tree box. The third argument is used as a temporary register
%   for building labels.
%    \begin{macrocode}
\cs_new:Nn \@@_make_rule_for:NNN {
%    \end{macrocode}
%   Build the rule.
%    \begin{macrocode}
  \@@_make_vertical:Nnnn #1
    { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #2 {left} }
    { \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {left} }
    {
      \skip_vertical:N \l_@@_rule_margin_dim
      \tl_if_empty:NF { \l_@@_rule_code_tl } {
        \tl_use:N \l_@@_rule_code_tl
        \skip_vertical:N \l_@@_rule_margin_dim
      }
    }
  \@@_vcenter:N #1
%    \end{macrocode}
%   Append the left label.
%    \begin{macrocode}
  \tl_if_blank:VF \l_@@_left_label_tl {
    \@@_make_simple:Nn #3 {
      \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n {
        \cs_set_eq:NN \inserttext \l_@@_left_label_tl
        \tl_use:N \l_@@_left_label_template_tl
      } }
    }
    \box_set_ht:cn { \@@_box:N #3 } { 0pt }
    \box_set_dp:cn { \@@_box:N #3 } { 0pt }
    \@@_append_left:NnN
      \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box
  }
%    \end{macrocode}
%   Append the right label.
%    \begin{macrocode}
  \tl_if_blank:VF \l_@@_right_label_tl {
    \@@_make_simple:Nn #3 {
      \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n {
        \cs_set_eq:NN \inserttext \l_@@_right_label_tl
        \tl_use:N \l_@@_right_label_template_tl
      } }
    }
    \box_set_ht:cn { \@@_box:N #3 } { 0pt }
    \box_set_dp:cn { \@@_box:N #3 } { 0pt }
    \@@_append_right:NnN
      \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box
  }
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Stack-based interface}
%
% \subsubsection{The stack}
%
% Logically, box structures are stored on a stack. However, \TeX\ does not
% provide data structures for that and the grouping mechanism is not flexible
% enough, so we encode them using what we actually have. A stack for boxes is
% implemented using a global hbox \cs{g_@@_stack_box} that contains all the
% boxes successively. A sequence \cs{g_@@_stack_seq} is used to store the
% dimensions property lists textually. We maintain a counter
% \cs{g_@@_level_int} with the number of elements on the stack, for
% consistency checks.
%    \begin{macrocode}
\int_new:N \g_@@_level_int
\box_new:N \g_@@_stack_box
\seq_new:N \g_@@_stack_seq
%    \end{macrocode}
%
% \begin{macro}{\@@_clear_stack:}
%   Clear the stack.
%    \begin{macrocode}
\cs_new:Nn \@@_clear_stack: {
  \int_gset:Nn \g_@@_level_int { 0 }
  \hbox_gset:Nn \g_@@_stack_box { }
  \seq_gclear:N \g_@@_stack_seq
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_push:N}
%   Push the contents of a register on the stack.
%    \begin{macrocode}
\cs_new:Nn \@@_push:N {
  \int_gincr:N \g_@@_level_int
  \hbox_gset:Nn \g_@@_stack_box
    { \hbox_unpack:N \g_@@_stack_box \box_use:c { \@@_box:N #1 } }
  \seq_gput_left:Nv \g_@@_stack_seq
    { \@@_marks:N #1 }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_pop:N}
%   Pop the value from the top of the stack into a register.
%    \begin{macrocode}
\cs_new:Nn \@@_pop:N {
  \int_compare:nNnTF { \g_@@_level_int } > { 0 } {
    \int_gdecr:N \g_@@_level_int
    \hbox_gset:Nn \g_@@_stack_box {
      \hbox_unpack:N \g_@@_stack_box
      \box_gset_to_last:N \g_tmpa_box
    }
    \box_set_eq_clear:cN { \@@_box:N #1 } \g_tmpa_box
    \seq_gpop_left:NN \g_@@_stack_seq \l_tmpa_tl
    \tl_set_eq:cN { \@@_marks:N #1 } \l_tmpa_tl
  } {
    \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{}
    \@@_clear:N #1
  }
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Assembling trees}
%
%    \begin{macrocode}
\@@_new:N \l_@@_a_box
\@@_new:N \l_@@_b_box
\@@_new:N \l_@@_c_box
\@@_new:N \l_@@_d_box
%    \end{macrocode}
%
% \begin{macro}{\@@_join_horizontal:n}
%   Join horizontally a number of elements at the top of the stack. If several
%   trees are joined, use the left mark of the left tree, the right mark of
%   the right tree and set the axis in the middle of these marks.
%    \begin{macrocode}
\cs_new:Nn \@@_join_horizontal:n {
  \int_case:nnF { #1 } {
  { 0 } {
    \group_begin:
    \@@_clear:N \l_@@_a_box
    \@@_push:N \l_@@_a_box
    \group_end:
  }
  { 1 } { }
  } {
    \group_begin:
    \@@_pop:N \l_@@_a_box
    \prg_replicate:nn { #1 - 1 } {
      \@@_pop:N \l_@@_b_box
      \@@_append_left:NnN
        \l_@@_a_box \l_@@_separation_dim \l_@@_b_box
    }
    \@@_set_mark:Nnn \l_@@_a_box { left }
      { \@@_mark:Nn \l_@@_b_box { left } }
    \@@_set_mark:Nnn \l_@@_a_box { axis }
      { ( \@@_mark:Nn \l_@@_a_box { left }
        + \@@_mark:Nn \l_@@_a_box { right } ) / 2 }
    \@@_push:N \l_@@_a_box
    \group_end:
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_join_vertical:}
%   Join vertically the two elements at the top of the stack, with a
%   horizontal rule of the appropriate size.
%    \begin{macrocode}
\cs_new:Nn \@@_join_vertical: {
  \group_begin:
  \@@_pop:N \l_@@_a_box
  \@@_pop:N \l_@@_b_box
  \@@_enlarge_conclusion:NN \l_@@_b_box \l_@@_a_box
  \@@_make_rule_for:NNN \l_@@_c_box \l_@@_b_box
    \l_@@_d_box
  \@@_append_vertical:NN \l_@@_a_box \l_@@_c_box
  \@@_append_vertical:NN \l_@@_a_box \l_@@_b_box
  \@@_push:N \l_@@_a_box
  \group_end:
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{High-level commands}
%
% \begin{macro}{\@@_statement_parse:w}
%   An auxiliary function for parsing the argument in
%   \cs{@@_push_statement:n}.
%    \begin{macrocode}
\cs_new:Npn \@@_statement_parse:w #1 & #2 & #3 \q_stop {
  \tl_if_empty:nTF { #3 } {
    \@@_make_simple:Nn \l_@@_a_box
      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_template_tl }
  } {
    \@@_make_split:Nnn \l_@@_a_box
      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_left_template_tl }
      { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_@@_right_template_tl }
  }
  \@@_push:N \l_@@_a_box
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_push_statement:n}
%   Push a box with default formatting, using explicit alignment if the code
%   contains a |&| character
%    \begin{macrocode}
\cs_new:Nn \@@_push_statement:n {
  \@@_statement_parse:w #1 & & \q_stop
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Document interface}
%
% \subsubsection{Functions to define statements}
%
% The \cs{g_@@_statements_seq} variable contains the list of all defined
% statements. For each statement |X|, there is a document command \cs{ebproofX}
% and the alias \cs{X} is defined when entering a |prooftree| environment.
%    \begin{macrocode}
\seq_new:N \g_@@_statements_seq
%    \end{macrocode}
%
% \begin{macro}{\@@_setup_statements:}
%   Install the aliases for statements, saving the original value of the control
%   sequences.
%    \begin{macrocode}
\cs_new:Nn \@@_setup_statements: {
  \seq_map_inline:Nn \g_@@_statements_seq {
    \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 }
    \cs_set_eq:cc { ##1 } { ebproof ##1 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_restore_statements:}
%   Restore the saved meanings of the control sequences. This is useful when
%   interpreting user-provided code in statement arguments. The meanings are
%   automatically restored when leaving a |prooftree| environment because of
%   grouping.
%    \begin{macrocode}
\cs_new:Nn \@@_restore_statements: {
  \seq_map_inline:Nn \g_@@_statements_seq {
    \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_new_statement:nnn}
%   Define a new statement. The first argument is the name, the second one is
%   an argument specifier as used by |xparse| and the third one is the body of
%   the command.
%    \begin{macrocode}
\cs_new:Nn \@@_new_statement:nnn {
  \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 }
  \seq_put_right:Nn \g_@@_statements_seq { #1 }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@@_new_deprecated_statement:nnnn}
%   Define a deprecated statement. The syntax is the same as above except that
%   an extra argument in third position indicates what should be used instead.
%   The effect is the same except that a warning message is issued the first
%   time the statement is used.
%    \begin{macrocode}
\cs_new:Nn \@@_new_deprecated_statement:nnnn {
  \cs_new:cpn { ebproof_#1_warning: } {
    \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 }
    \cs_gset:cn { ebproof_#1_warning: } { }
  }
  \@@_new_statement:nnn { #1 } { #2 }
    { \use:c { ebproof_#1_warning: } #4 }
}
%    \end{macrocode}
% \end{macro}
%
%
% \subsubsection{Basic commands}
%
% \begin{macro}{\ebproofset,\set}
%   This is a simple wrapper around \cs{keys_set:nn}.
%    \begin{macrocode}
\@@_new_statement:nnn { set } { m } {
  \keys_set:nn { ebproof } { #1 }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\hypo}
%   This is mostly a wrapper around \cs{ebproof_push_statement:n}, with
%   material to handle options and the statements macros.
%    \begin{macrocode}
\@@_new_statement:nnn { hypo } { O{} m } {
  \group_begin:
  \@@_restore_statements:
  \keys_set:nn { ebproof } { #1 }
  \@@_push_statement:n { #2 }
  \group_end:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\infer}
%   This is a bit more involved than \cs{hypo} because we have to handle rule
%   style options and joining.
%    \begin{macrocode}
\@@_new_statement:nnn { infer } { O{} m O{} m } {
  \group_begin:
  \@@_restore_statements:
  \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl
  \keys_set:nV { ebproof } \l_tmpa_tl
  \tl_set:Nn \l_@@_right_label_tl { #3 }
  \@@_join_horizontal:n { #2 }
  \@@_push_statement:n { #4 }
  \@@_join_vertical:
  \group_end:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\ellipsis}
%   An ellipsis is made by hand using vertical leaders to render the dots
%   after rendering the label.
%    \begin{macrocode}
\@@_new_statement:nnn { ellipsis } { m m } {
  \group_begin:
  \@@_restore_statements:
  \tl_clear:N \l_@@_rule_code_tl
  \@@_make_split:Nnn \l_@@_a_box { } {
    \vbox_set:Nn \l_tmpa_box {
      \skip_vertical:n { 1.2ex }
      \hbox:n { \tex_ignorespaces:D #1 }
      \skip_vertical:n { 1.2ex }
    }
    \vbox_to_ht:nn { \box_ht:N \l_tmpa_box } {
      \tex_xleaders:D \vbox_to_ht:nn { .8ex }
        { \tex_vss:D \hbox:n { . } \tex_vss:D }
      \tex_vfill:D
    }
    \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box }
  }
  \@@_push:N \l_@@_a_box
  \@@_join_vertical:
  \@@_push_statement:n {#2}
  \@@_join_vertical:
  \group_end:
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Modifying trees}
%
% \begin{macro}{\rewrite}
%   Rewrite the box at the top of the stack while preserving its dimensions an
%   marks. The code is typeset in horizontal mode, with control sequences to
%   access the original box and its marks.
%    \begin{macrocode}
\@@_new_statement:nnn { rewrite } { m } {
  \group_begin:
  \@@_restore_statements:
  \@@_pop:N \l_@@_a_box
  \box_set_eq:Nc \l_tmpa_box { \@@_box:N \l_@@_a_box }
  \hbox_set:Nn \l_tmpb_box {
    \cs_set_eq:NN \treebox \l_tmpa_box
    \cs_set:Npn \treemark { \@@_mark:Nn \l_@@_a_box }
    { #1 }
  }
  \box_set_wd:Nn \l_tmpb_box { \box_wd:c { \@@_box:N \l_@@_a_box } }
  \box_set_ht:Nn \l_tmpb_box { \box_ht:c { \@@_box:N \l_@@_a_box } }
  \box_set_dp:Nn \l_tmpb_box { \box_dp:c { \@@_box:N \l_@@_a_box } }
  \box_set_eq:cN { \@@_box:N \l_@@_a_box } \l_tmpb_box
  \@@_push:N \l_@@_a_box
  \group_end:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\delims}
%   Insert \cs{left} and \cs{right} delimiters without changing the alignment.
%    \begin{macrocode}
\@@_new_statement:nnn { delims } { m m } {
  \group_begin:
  \@@_restore_statements:
  \@@_pop:N \l_@@_a_box
  \hbox_set:Nn \l_tmpa_box
    { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ }
  \dim_set:Nn \l_tmpa_dim
    { \box_ht:N \l_tmpa_box - \box_ht:c { \@@_box:N \l_@@_a_box } }
  \hbox_set:cn { \@@_box:N \l_@@_a_box } {
    $ #1 \tex_vrule:D
      height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt
    \tex_right:D . $
  }
  \@@_shift_x:Nn \l_@@_a_box
    { \box_wd:c { \@@_box:N \l_@@_a_box } }
  \hbox_set:cn { \@@_box:N \l_@@_a_box } {
    \hbox_unpack:c { \@@_box:N \l_@@_a_box }
    $ \tex_left:D . \box_use:N \l_tmpa_box #2 $
  }
  \hbox_set:cn { \@@_box:N \l_@@_a_box }
    { \box_move_down:nn { \l_tmpa_dim }
        { \box_use:c { \@@_box:N \l_@@_a_box } } }
  \@@_push:N \l_@@_a_box
  \group_end:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\overlay}
%   Pop two trees and append the second tree as an overlay over the first one,
%   so that the baselines and axes match. The bounding box of the result
%   adjusts to contain both trees.
%    \begin{macrocode}
\@@_new_statement:nnn { overlay } { } {
  \group_begin:
  \@@_pop:N \l_@@_a_box
  \@@_pop:N \l_@@_b_box
  \@@_overlay:NN \l_@@_a_box \l_@@_b_box
  \@@_push:N \l_@@_a_box
  \group_end:
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Deprecated statements}
%
% These statements were defined in versions 1.x of the package, they are
% preserved for temporary upwards compatibility and will be removed in a
% future version.
%    \begin{macrocode}
\@@_new_deprecated_statement:nnnn { Alter } { m }
  { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } }
\@@_new_deprecated_statement:nnnn { Delims } { }
  { use~\token_to_str:c{delims}~instead } { \ebproofdelims }
\@@_new_deprecated_statement:nnnn { Ellipsis } { }
  { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis }
\@@_new_deprecated_statement:nnnn { Hypo } { }
  { use~\token_to_str:c{hypo}~instead } { \ebproofhypo }
\@@_new_deprecated_statement:nnnn { Infer } { }
  { use~\token_to_str:c{infer}~instead } { \ebproofinfer }
%    \end{macrocode}
%
%
% \subsubsection{Environment interface}
%
% The stack is initialised globally. The \env{prooftree} environment does not
% clear the stack, instead it saves the initial level in order to check that
% statements are properly balanced. This allows for nested uses of the
% environment, if it ever happens to be useful.
%
%    \begin{macrocode}
\@@_clear_stack:
\tl_new:N \l_@@_start_level_tl
%    \end{macrocode}
%
% \begin{macro}{prooftree,prooftree*}
%   The \env{prooftree} environment.
%    \begin{macrocode}
\NewDocumentEnvironment { prooftree } { s O{} } {
  \group_align_safe_begin:
  \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl
  \keys_set:nV { ebproof } \l_tmpa_tl
  \tl_set:Nx \l_@@_start_level_tl { \int_use:N \g_@@_level_int }
  \vbox_set:Nw \l_tmpa_box
  \@@_setup_statements:
} {
  \vbox_set_end:
  \@@_pop:N \l_@@_a_box
  \int_compare:nNnF { \g_@@_level_int } = { \tl_use:N \l_@@_start_level_tl } {
    \PackageError{ebproof}{Malformed~proof~tree}{
      Some~hypotheses~were~declared~but~not~used~in~this~tree.}
  }
  \IfBooleanTF { #1 } {
    \[ \box_use:c { \@@_box:N \l_@@_a_box } \]
    \ignorespacesafterend
  } {
    \hbox_unpack:N \c_empty_box
    \bool_if:NTF \l_@@_center_bool {
      \hbox:n { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ }
    } {
      \box_use:c { \@@_box:N \l_@@_a_box }
    }
  }
  \group_align_safe_end:
}
%    \end{macrocode}
% A trick for the starred version:
%    \begin{macrocode}
\cs_new:cpn { prooftree* } { \prooftree* }
\cs_new:cpn { endprooftree* } { \endprooftree }
%    \end{macrocode}
% \end{macro}
%
%    \begin{macrocode}
%</package>
%    \end{macrocode}
%
% \end{implementation}