summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/mathpartir
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/mathpartir
Initial commit
Diffstat (limited to 'macros/latex/contrib/mathpartir')
-rw-r--r--macros/latex/contrib/mathpartir/COPYING340
-rw-r--r--macros/latex/contrib/mathpartir/README35
-rw-r--r--macros/latex/contrib/mathpartir/mathpartir.dtx1273
-rw-r--r--macros/latex/contrib/mathpartir/mathpartir.ins65
-rw-r--r--macros/latex/contrib/mathpartir/mathpartir.pdfbin0 -> 265615 bytes
5 files changed, 1713 insertions, 0 deletions
diff --git a/macros/latex/contrib/mathpartir/COPYING b/macros/latex/contrib/mathpartir/COPYING
new file mode 100644
index 0000000000..d60c31a97a
--- /dev/null
+++ b/macros/latex/contrib/mathpartir/COPYING
@@ -0,0 +1,340 @@
+ GNU GENERAL PUBLIC LICENSE
+ Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.
+ 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+ Preamble
+
+ The licenses for most software are designed to take away your
+freedom to share and change it. By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users. This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it. (Some other Free Software Foundation software is covered by
+the GNU Library General Public License instead.) You can apply it to
+your programs, too.
+
+ When we speak of free software, we are referring to freedom, not
+price. Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+ To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+ For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have. You must make sure that they, too, receive or can get the
+source code. And you must show them these terms so they know their
+rights.
+
+ We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+ Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software. If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+ Finally, any free program is threatened constantly by software
+patents. We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary. To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+ The precise terms and conditions for copying, distribution and
+modification follow.
+
+ GNU GENERAL PUBLIC LICENSE
+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+ 0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License. The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language. (Hereinafter, translation is included without limitation in
+the term "modification".) Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope. The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+ 1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+ 2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+ a) You must cause the modified files to carry prominent notices
+ stating that you changed the files and the date of any change.
+
+ b) You must cause any work that you distribute or publish, that in
+ whole or in part contains or is derived from the Program or any
+ part thereof, to be licensed as a whole at no charge to all third
+ parties under the terms of this License.
+
+ c) If the modified program normally reads commands interactively
+ when run, you must cause it, when started running for such
+ interactive use in the most ordinary way, to print or display an
+ announcement including an appropriate copyright notice and a
+ notice that there is no warranty (or else, saying that you provide
+ a warranty) and that users may redistribute the program under
+ these conditions, and telling the user how to view a copy of this
+ License. (Exception: if the Program itself is interactive but
+ does not normally print such an announcement, your work based on
+ the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole. If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works. But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+ 3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+ a) Accompany it with the complete corresponding machine-readable
+ source code, which must be distributed under the terms of Sections
+ 1 and 2 above on a medium customarily used for software interchange; or,
+
+ b) Accompany it with a written offer, valid for at least three
+ years, to give any third party, for a charge no more than your
+ cost of physically performing source distribution, a complete
+ machine-readable copy of the corresponding source code, to be
+ distributed under the terms of Sections 1 and 2 above on a medium
+ customarily used for software interchange; or,
+
+ c) Accompany it with the information you received as to the offer
+ to distribute corresponding source code. (This alternative is
+ allowed only for noncommercial distribution and only if you
+ received the program in object code or executable form with such
+ an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it. For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable. However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+ 4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License. Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+ 5. You are not required to accept this License, since you have not
+signed it. However, nothing else grants you permission to modify or
+distribute the Program or its derivative works. These actions are
+prohibited by law if you do not accept this License. Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+ 6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions. You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+ 7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License. If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all. For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices. Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+ 8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded. In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+ 9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time. Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation. If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+ 10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission. For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this. Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+ NO WARRANTY
+
+ 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+ 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+ END OF TERMS AND CONDITIONS
+
+ How to Apply These Terms to Your New Programs
+
+ If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+ To do so, attach the following notices to the program. It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+ <one line to give the program's name and a brief idea of what it does.>
+ Copyright (C) <year> <name of author>
+
+ This program is free software; you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation; either version 2 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program; if not, write to the Free Software
+ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+ Gnomovision version 69, Copyright (C) year name of author
+ Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+ This is free software, and you are welcome to redistribute it
+ under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License. Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary. Here is a sample; alter the names:
+
+ Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+ `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+ <signature of Ty Coon>, 1 April 1989
+ Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs. If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library. If this is what you want to do, use the GNU Library General
+Public License instead of this License.
diff --git a/macros/latex/contrib/mathpartir/README b/macros/latex/contrib/mathpartir/README
new file mode 100644
index 0000000000..533d6ea55f
--- /dev/null
+++ b/macros/latex/contrib/mathpartir/README
@@ -0,0 +1,35 @@
+ +------------------------------------------------+
+ | mathpartir: |
+ | Math Paragraph for Typesetting Inference Rules |
+ +------------------------------------------------+
+
+Author : Didier Rémy
+Version : 1.3.2
+Bug Reports : to author
+Web Site : http://pauillac.inria.fr/~remy/latex/
+License : GPL - GNU General Public License 2 or later
+
+The package mathpartir provides:
+
+An environment mathpar for typesetting a sequence of math formulas in
+mixed horizontal and vertical mode. The environment selects the best
+arrangement according to the line width, exactly as paragraph mode
+does for words.
+
+A macro inferrule for typesetting type inference rules. See the
+package documentation and website for more information.
+
+This package is partially supported by HEVEA.
+
+Files in distribution:
+
+ README This file.
+ mathpartir.ins Package installation file.
+ mathpartir.dtx Package source file.
+ COPYING GPL license file.
+
+ mathpartir.sty Package style file. It was produced by
+ executing "latex mathpartir.ins".
+
+ mathpartir.pdf Package documentation. It was produced by
+ executing "pdflatex mathpartir.dtx" twice.
diff --git a/macros/latex/contrib/mathpartir/mathpartir.dtx b/macros/latex/contrib/mathpartir/mathpartir.dtx
new file mode 100644
index 0000000000..df27d11d91
--- /dev/null
+++ b/macros/latex/contrib/mathpartir/mathpartir.dtx
@@ -0,0 +1,1273 @@
+% \iffalse meta-comment
+%
+% Copyright (C) 2015 by Didier Remy <didier.remy(at)inria(dot)fr>
+%
+% The file is part of mathpartir
+%
+% mathpartir is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 2 of the License, or
+% (at your option) any later version.
+%
+% mathpartir is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+%
+% You should have received a copy of the GNU General Public License
+% along with mathpartir. If not, see <http://www.gnu.org/licenses/>.
+%
+% \fi
+%
+% \iffalse
+%<*driver>
+\ProvidesFile{mathpartir.dtx}
+%</driver>
+%<package>\NeedsTeXFormat{LaTeX2e}
+%<package>\ProvidesPackage{mathpartir}
+%<*package>
+ [2016/02/24 version 1.3.2 Math Paragraph for Typesetting Inference Rules]
+%</package>
+%
+%<hevea>\documentclass {article}
+%<*driver>
+\documentclass{ltxdoc}
+%</driver>
+%<*(driver|hevea)>
+\usepackage {mathpartir}
+\usepackage {listings}
+\usepackage {array}
+\usepackage {url}
+%<hevea>\usepackage {hevea}
+
+\lstset {basicstyle=\tt}
+\let \lst \verb
+
+\title {
+%<hevea>\begin{tabular}{>{\huge}c}
+\textbf{MATH} formulas in \\
+\textbf{PAR}ragraph mode\\[-1ex]
+%<*!hevea>
+\hskip 0em\hbox to 12em {\hrulefill}\\
+%</!hevea>
+%<hevea>\hline
+\textbf Typesetting \textbf Inference \textbf Rules \\
+%<hevea>\end{tabular}
+}
+\author {Didier R{\'{e}}my}
+\date {(Version 1.3.2, last modified 24/02/2016)}
+
+\begin{document}
+
+\maketitle
+
+%<*!hevea>
+\DeleteShortVerb{\|}
+\section{Introduction}
+%</!hevea>
+%<hevea>\begin{abstract}
+The package mathpartir provides macros for
+displaying formulas and lists of formulas that are typeset in mixed
+horizontal and vertical modes.
+
+The environment \verb"mathpar" generalizes the math display mode to allow
+several formulas on the same line, and several lines in the same
+display. The arrangement of the sequence of formulas into lines is automatic
+depending on the line width and on a minimum inter-formula space alike words
+are displayed in a paragraphs (in centerline mode). A typical application
+is displaying a set of type inference rules.
+
+The macro \verb"inferrule" typesets inference rules. Both premises and
+conclusions are presented as lists of formulas and are typeset in paragraph
+mode and wrapped into multiple lines whenever necessary.
+%<hevea> \end{abstract}
+
+%<hevea>\section {License}
+%<hevea>
+%<hevea>Mathpartir is Copyright (C) 2001-2005, 2015, 2016 INRIA. Mathpartir
+%<hevea>has been developed by Didier R{\'{e}}my. Mathpartir is free software; you
+%<hevea>can redistribute it and/or modify it under the terms of the GNU General
+%<hevea>Public License as published by the Free Software Foundation; either version
+%<hevea>2, or (at your option) any later version. See the GNU General Public
+%<hevea>License for more details (\url{http://pauillac.inria.fr/~remy/license/GPL}).
+%<hevea>Mathpartir is distributed in the hope that it will be useful, but without
+%<hevea>any warranty.
+
+\section {The mathpar environment}
+
+The mathpar environment is a ``paragraph mode for formulas''.
+It allows to typeset long list of formulas putting as
+many as possible on the same line:
+$$
+\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
+\begin{lstlisting}{Ocaml}
+\begin{mathpar}
+A-Formula \and
+Longer-Formula \and
+And \and The-Last-One
+\end{mathpar}
+\end{lstlisting}
+&
+\begin{mathpar}
+A-Formula
+\and
+Longer-Formula
+\and
+And
+\and
+The-Last-One
+\end{mathpar}
+\end{tabular}
+$$
+Formulas are separated by \verb"\and" (or equivalently by a blank line).
+To enforce a vertical break it suffices to replace \verb"\and" by
+\verb"\\".
+
+The implementation of \verb"mathpar" entirely relies on the paragraph mode
+for text. It starts a new paragraph, and a math formula within a paragraph,
+after adjusting the spacing and penalties for breaks. Then, it simply binds
+\verb"\and" to something like \verb"\goodbreak".
+
+\section {The inferrule macro}
+
+The inferrule macro is designed to typeset inference rules. It should
+only\footnote {Even though the basic version may work in text mode,
+we discourage its use in text mode; the star-version cannot be used in
+text-mode} be used in math mode (or display math mode).
+
+The basic use of the rule is
+\begin{verbatim}
+\inferrule
+ {one \\ two \\ three \\ or \\ more \\ premisses}
+ {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
+\end{verbatim}
+This is the rendering on a large page
+\def \one {\inferrule
+ {one \\ two \\ three \\ or \\ more \\ premises}
+ {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
+}
+$$
+%<hevea>\one
+%<*!hevea>
+\fbox {\vbox {\advance \hsize by -2\fboxsep \advance \hsize by -2\fboxrule
+ \linewidth\hsize
+ $$\one$$}}
+%</!hevea>
+$$
+However, the same formula on a narrower page will automatically be typeset
+like that:
+$$
+%<hevea>\one
+%<*!hevea>
+\fbox {\hsize 0.33 \hsize \vbox {$$\one$$}}
+%</!hevea>
+$$
+An inference rule is mainly composed of a premise and a conclusion.
+The premise and the conclusions are both list of formulas where the
+elements are separated by \verb"\\".
+
+Note the asymmetry between typesetting of the premises and of
+conclusions where lines closer to the center are fit first.
+
+A newline can be forced by adding an empty line \verb"\\\\"
+
+\begin{tabular}{m{0.44\hsize}m{0.44\hsize}}
+\begin{lstlisting}{Ocaml}
+\inferrule
+ {aa \\\\ bb}
+ {dd \\ ee \\ ff}
+\end{lstlisting}
+&
+$\inferrule {aa \\\\bb}{dd \\ ee \\ ff}$
+\\
+\end{tabular}
+
+\subsection {Single rules}
+
+Single rules are the default mode.
+Rules are aligned on their fraction bar, as illustrated below:
+$$
+\inferrule {aa \\ bb}{ee} \hspace {4em} \inferrule {aa \\\\ bb \\ ee}{ee}
+$$
+If the premise or the conclusion is empty, then the fraction bar is not
+typeset and the premise or the conclusion is centered:
+$$
+\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
+\begin{lstlisting}{Ocaml}
+\inferrule {}{aa} +
+\inferrule {aa \\\\ aa}{}
+\end{lstlisting}
+&
+$
+\inferrule {}{aa} +
+\inferrule {aa \\\\ aa}{}
+$
+\\
+\end{tabular}
+$$
+Use use \verb"{ }" instead of \verb"{}" to get an axiom for instance:
+$$
+\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
+\begin{lstlisting}{Ocaml}
+\inferrule { }{aa} +
+\inferrule {aa}{ }
+\end{lstlisting}
+&
+\mbox {$
+\inferrule { }{aa} +
+\inferrule {aa}{ }
+$}
+\\
+\end{tabular}
+$$
+
+The macro \lst"\inferrule" accepts a label as optional argument, which will
+be typeset on the top left corner of the rule:
+\par
+\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
+\begin{lstlisting}{Ocaml}
+\inferrule [yop]
+ {aa \\ bb}
+ {cc}
+\end{lstlisting}
+&
+$\inferrule [Yop]{aa \\ bb}{cc}$
+\\
+\end{tabular}
+\par\noindent
+See section~\ref {options} for changing typesetting of labels.
+A label can also be placed next to the rule directly, since the rule is
+centered:
+\par
+\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
+\begin{lstlisting}{Ocaml}
+\inferrule
+ {aa \\ bb}
+ {cc}
+\quad (\textsc {Yop})
+\end{lstlisting}
+&
+$\inferrule{aa \\ bb}{cc} \quad (\textsc {Yop})$
+\\
+\end{tabular}
+
+\subsection {Customizing presentation}
+
+By default, lines are centered in inference rules.
+However, this can be changed by either \lst"\mprset{flushleft}"
+or \lst"\mprset{center}". For instance,
+
+\begin{tabular}{m{0.44\hsize}m{0.44\hsize}}
+\begin{lstlisting}{Ocaml}
+$$\mprset{flushleft}
+ \inferrule
+ {a \\ bbb \\\\ ccc \\ dd}
+ {dd \\ ee \\ ff}$$
+\end{lstlisting}
+&
+$$\mprset{flushleft}
+\hsize 0.45\hsize
+\inferrule {a \\ bb \\ ccc \\ dddd}{e \\ ff \\ gg}$$
+\\
+\end{tabular}
+
+\noindent
+Note that lines are aligned independently in the premise and the
+conclusion, which are both themselves centered. In particular,
+left alignment will not affect a single-line premise or conclusion.
+
+\subsection {Customizing rules}
+
+One may wish to change use rules for rewriting rule or implications, etc.
+There is a generic way of definition new rules by providing three parts:
+a tail, a body, and a head. The rule will then be built by joining
+all three components in this order and filling the body with leaders to
+extend as much as necessary. Here are examples
+
+\begin{tabular}{m{0.54\hsize}m{0.44\hsize}}
+\begin{lstlisting}{Ocaml}
+$$\mprset{fraction={===}}
+ \inferrule {a \\ bbb} {cc}$$
+\end{lstlisting}
+&
+$$\mprset{fraction={===}}
+ \inferrule {a \\ bbb} {cc}$$
+
+\\
+\begin{lstlisting}{Ocaml}
+$$\mprset
+ {fraction={\models=\Rightarrow}}
+ \inferrule {a \\ bbb} {cc}$$
+\end{lstlisting}
+&
+$$\mprset
+ {fraction={\models=\Rightarrow}}
+ \inferrule {a \\ bbb} {cc}$$
+\\
+\end{tabular}
+The height and depth of the \emph{body} are used to adjust vertical space.
+One, may ``smash'' the body to reduce the vertical space
+
+\begin{tabular}{m{0.54\hsize}m{0.44\hsize}}
+\begin{lstlisting}{Ocaml}
+$$\mprset
+ {fraction={%
+ {\scriptstyle\vdash}%
+ {\smash-}%
+ {\rightarrow\!\!}%
+ }}
+ \inferrule {a \\ bbb} {cc}\,\,$$
+\end{lstlisting}
+&
+$$\mprset
+ {fraction={{\scriptstyle\vdash}{\smash-}{\rightarrow\!\!}}}
+ \inferrule {a \\ bbb} {cc}$$
+\\
+\begin{lstlisting}{Ocaml}
+$$\mprset {fraction={\cdot\cdots\cdot}}
+ \inferrule {a \\ bbb} {cc}$$
+\end{lstlisting}
+&
+$$\mprset {fraction={{}{\,\smash\cdot\,}{}}}
+ \inferrule {a \\ bbb} {cc}$$
+\\
+\end{tabular}
+Since vertical skip does not take header and footer into account, which is
+usually better but sometimes odd, this can be adjusted explicitly:
+
+\begin{tabular}{m{0.54\hsize}m{0.44\hsize}}
+\begin{lstlisting}{Ocaml}
+$$\mprset
+ {fraction={|=/},
+ fractionaboveskip=0.6ex,
+ fractionbelowskip=0.4ex}
+ \inferrule
+ {a \\ bbb_{\downarrow}}
+ {cc^{\T\uparrow}}$$
+\end{lstlisting}
+&
+$$\mprset
+ {fraction={|=/},
+ fractionaboveskip=0.6ex,
+ fractionbelowskip=0.4ex}
+ \inferrule
+ {a \\ bbb_{\downarrow}}
+ {cc^{\uparrow}}$$
+\\
+\end{tabular}
+Finally, it is also possible to provide its own definition
+of fraction by
+
+\begin{tabular}{m{0.54\hsize}m{0.44\hsize}}
+\begin{lstlisting}{Ocaml}
+\def \Over #1#2{\hbox{$#1 \over #2$}}
+$$\mprset{myfraction=\Over}
+ \inferrule {a \\ bbb} {cc}$$
+\end{lstlisting}
+&
+\def \Over #1#2{\hbox{$#1 \over #2$}}
+$$\mprset{myfraction=\Over}
+ \inferrule {a \\ bbb} {cc}$$
+\\
+\end{tabular}
+
+\paragraph{Customizing the horizontal skip between premises}
+(default value is 2em).
+\begin{quote}
+\begin{lstlisting}{Ocaml}
+$$\mprset {sep=6em}
+ \inferrule {a \\ bbb} {cc}$$
+\end{lstlisting}
+$$\mprset {sep=6em}
+ \inferrule {a \\ bbb} {cc}$$
+\end{quote}
+
+\paragraph{Customizing the vertical space between premises}
+(default value is empty). Notice that leaving it empty and setting vskip to
+0em is not quite equivalent as show below between the third and fourth rules
+(because the typesetting cannot use the primitive typesetting of
+fractions).
+\begin{quote}
+\begin{lstlisting}{Ocaml}
+$$\def\R{\inferrule {aa\\aa\\\\bbb\\bbb} {cc}
+ \hspace{3em}}
+ \R \mprset{vskip=0ex}\R \mprset{vskip=1ex}\R$$
+\end{lstlisting}
+$$\def \R{\inferrule {aa \\ aa \\\\ bbb \\ bbb} {cc}\hspace{3em}}
+ \R \mprset{vskip={}}
+ \R \mprset{vskip=0ex}\R \mprset{vskip=1ex}\R$$
+\end{quote}
+
+
+
+\subsection {Tabulars in inference rules}
+
+Although you probably do not want to do that, you may still use tabular
+or minipages inside inference rules, but between braces, as follows:
+$$
+\begin{tabular}{m{0.50\hsize}m{0.50\hsize}}
+\begin{lstlisting}{Ocaml}
+\infer [Tabular-Rule]
+{some \\ math \\ and \\
+ {\begin{tabular}[b]{|l|r|}
+ \hline Ugly & and
+ \\[1ex]\hline
+ table & text
+ \\\hline
+ \end{tabular}} \\
+ {\begin{minipage}[b]{6em}
+ Do you really wish
+ to do that?
+ \end{minipage}} \\
+}
+{some \\ conclusions}
+\end{lstlisting}
+&
+\infer [Tabular-Rule]
+{some \\ math \\ and \\
+ {\begin{tabular}[b]{|l|r|}
+ \hline Ugly & and
+ \\[1ex]\hline
+ table & text
+ \\\hline
+ \end{tabular}} \\
+ {\begin{minipage}[b]{6em}
+ Do you really wish
+ to do that?
+ \end{minipage}} \\
+}
+{some \\ conclusions}
+\\
+\end{tabular}
+$$
+
+
+\subsection {Derivation trees}
+
+To help writing cascades of rules forming a derivation tree, inference rules
+can also be aligned on their bottom line. For this, we use the star-version:
+$$
+\begin{tabular}{m{0.65\hsize}m{0.45\hsize}}
+\begin{lstlisting}{Ocaml}
+\inferrule*
+ {\inferrule* {aa \\ bb}{cc}
+ \\ dd}
+ {ee}
+\end{lstlisting}
+&
+$
+\inferrule*
+ {\inferrule* {aa \\ bb}{cc}
+ \\ dd}
+ {ee}
+$
+\\
+\end{tabular}
+$$
+The star version can also take an optional argument,
+but with a different semantics. The optional argument is parsed by the
+\verb"keyval" package, so as to offer a set of record-like options:
+$$
+\def \arraystretch {1.4}
+\begin{tabular}{|>{\tt}c|>{$}c<{$}|p{0.6\hsize}|}
+\hline
+\bf key & \bf arg & \bf Effect
+\\\hline
+before & tex & Execute $tex$ before typesetting the rule.
+ Useful for instance to change the maximal width of the rule.
+\\\hline
+width & d & Set the width of the rule to $d$
+\\\hline
+narrower & d & Set the width of the rule to $d$ times \verb"\hsize".
+\\\hline
+lab & \ell & Put label $\ell$ on the top of the rule as with the
+non-start version.
+\\\hline
+Lab & \ell & same as lab
+\\\hline
+left & \ell & Put label $\ell$ on the left of the rule
+\\\hline
+Left & \ell & Idem, but as if label $\ell$ had zero width.
+\\\hline
+Right & \ell & As \verb"Left", but on the right of the rule.
+\\\hline
+right & \ell & As \verb"left", but on the right of the rule.
+\\\hline
+leftskip & d & Cheat by (skip negative space) $d$ on the left side.
+\\\hline
+rightskip & d & Cheat by $d$ on the right side of the rule.
+\\\hline
+vdots & d & Raise the rule by $d$ and insert vertical dots.
+\\\hline
+\end{tabular}
+$$
+
+We remind at the end the global options that we've seen above that can
+also be set locally in derivation trees:
+\begin{mathpar}
+\def \arraystretch {1.4}
+\begin{tabular}{|>{\tt}c|>{$}c<{$}|p{0.6\hsize}|}
+\hline
+\\\hline\hline
+sep & d & Set the separation between premises and conclusions to $s$.
+\\\hline
+flushleft & - & flush premises to the left hand side
+\\\hline
+center & - & center premises on each line.
+\\\hline
+rewrite & d &
+\\\hline
+myfraction & tex & set fraction to $tex$ command
+\\\hline
+fraction & lmr & set fraction pattern to $lm...mr$ with leaders.
+\\\hline
+vskip & d & Set the vertical skip between premises and conclusions to $h$.
+\\\hline
+vcenter && Make the rule centered around the fraction line as the non-star
+version
+\\\hline
+\end{tabular}
+\end{mathpar}
+
+Here is an example of a complex derivation:
+$$
+\inferrule* [left=Total,rightstyle=\em,right={(when $n > 0$)}]
+ {\inferrule* [Left=Foo]
+ {\inferrule* [rightstyle={\bf},Right=Bar,vskip=1ex,
+ leftskip=2em,rightskip=2em,vdots=1.5em]
+ {a \\ a \\\\ bb \\ cc \\ dd}
+ {ee}
+ \\ ff \\ gg}
+ {hh}
+ \\
+ \inferrule* [lab=XX,sep=4em]{uu \\ vv}{ww}}
+ {(1)}
+$$
+and its code
+\begin{lstlisting}{Ocaml}
+\inferrule* [left=Total]
+ {\inferrule* [Left=Foo]
+ {\inferrule* [Right=Bar,rightstyle=\bf,
+ leftskip=2em,rightskip=2em,vdots=1.5em]
+ {a \\ a \\\\ bb \\ cc \\ dd}
+ {ee}
+ \\ ff \\ gg}
+ {hh}
+ \\
+ \inferrule* [lab=XX]{uu \\ vv}{ww}}
+ {(1)}
+\end{lstlisting}
+
+\def \L#1{\lower 0.4ex \hbox {#1}}
+\def \R#1{\raise 0.4ex \hbox {#1}}
+\def \hevea {H\L{E}\R{V}\L{E}A}
+\def \hevea {$\mbox {H}\!_{\mbox {E}}\!\mbox {V}\!_{\mbox {E}}\!\mbox {A}$}
+
+\subsection {Label styles}
+
+\label {options}
+
+The package uses
+\verb"\DefTirNameStyle",
+\verb"\LabTirNameStyle",
+\verb"\LeftTirNameStyle",
+and \verb"\RightTirNameStyle"
+to typeset labels introduced with the default option,
+\verb"Lab-",
+\verb"Left-", or
+\verb"Right-", respectively (or their uncapitablized variants).
+This can safely be redefined by the user.
+\verb"\DefTirName" is normally used for defining
+occurrences ({\em i.e.} in rule \lst"\inferrule") while the three other forms
+are used for referencing names ({\em i.e.} in the star-version). The styles
+can also be redefined using labeled-arguments of the star-version of
+{\tt\string\inferrule} as described in table below.
+
+Instead of just changing the style, the whole
+typesetting of labels may be changed by redefining
+\verb"\DefTirName",
+\verb"\LabTirName",
+\verb"\LeftTirName",
+and \verb"\RightTirName", each of which receives the label to be typeset as
+argument.
+
+Finally, the vertical skip
+
+\begin{mathpar}
+\def \arraystretch {1.4}
+\begin{tabular}{|>{\tt}c|>{$}c<{$}|p{0.6\hsize}|}
+\hline
+\bf key & \bf arg & \bf Effect
+\\\hline\hline
+style & tex & set the default style for labels to $tex$
+\\\hline
+leftstyle & tex & idem for labels
+\\\hline
+rightstyle & tex& idem for right labels
+\\\hline
+\end{tabular}
+\end{mathpar}
+
+\subsection {Star \emph{v.s.} non-star version}
+
+The package also defines \verb"\infer" as a shortcut for \verb"\inferrule"
+but only if it is not previously defined.
+
+There are two differences between the plain and star versions of
+\verb"\inferrule".
+The plain version centers the rule on the fraction line, while the
+star one centers the rule on the last conclusion, so as to be used in
+derivation trees.
+
+Another difference is that the optional argument of the plain version is a
+label to always be placed on top of the rule, while the $\ast$-version takes
+a record of arguments. Hence, it can be parameterized in many more ways.
+
+One may recover the plain version from the start version by passing the
+extra argument \texttt{vcenter} as illustrated below (the base line is
+aligned with the dotted line):
+\begin{mathpar}
+\cdots\cdots
+\cdots\cdots
+\inferrule*
+ {aa aa \\\\ aa \\ bb}{cc \\ cc \\\\ dd}
+\cdots\cdots
+\cdots\cdots
+\inferrule* [vcenter]
+ {aa aa \\\\ aa \\ bb}{cc \\ cc \\\\ dd}
+\cdots\cdots
+\cdots\cdots
+\end{mathpar}
+This is convenient, for instance to typeset rules with side conditions
+and keep them attached to the rule:
+\begin{mathpar}
+\def \RightTirName #1{\rm\hbox {\hskip 1ex (#1)}}
+\inferrule*[lab=Pos,right={if $n>0$}]
+ {aa \\ aa}
+ {cc}
+
+\inferrule*[lab=Neg,right={if $n<0$}]
+ {aa \\ aa}
+ {cc}
+\end{mathpar}
+Or differently,
+\begin{mathpar}
+\def \LabTirName #1{\hbox {(#1)}}
+\def \LeftTirName #1{\textsc{#1}}
+\inferrule*[Left=Pos,lab={if $n>0$}]
+ {aaa \\ aaa}
+ {cc}
+
+\inferrule*[Left=Neg,lab={if $n<0$}]
+ {aaa \\ aaa}
+ {cc}
+\end{mathpar}
+
+
+\subsection {Implementation}
+
+The main macro in the implementation of inference rules is the one that
+either premises and conclusions. The macros uses two box-registers one
+\verb"hbox" for typesetting each line and one \verb"vbox" for collecting
+lines. The premise appears as a list with
+\verb"\\" as separator. Each element is considered in turn typeset in a
+\verb"hbox" in display math mode. Its width is compare to the space left on
+the current line. If the box would not fit, the current horizontal line is
+transferred to the vertical box and emptied. Then, the current formula can
+safely be added to the horizontal line (if it does not fit, nothing can be
+done). When moved to the vertical list, lines are aligned on their center
+(as if their left-part was a left overlapped). At the end the vbox is
+readjusted on the right.
+
+This description works for conclusions. For premises, the elements must be
+processes in reverse order and the vertical list is simply built upside
+down.
+
+\section {Other Options for the {\tt mathpar} environment}
+
+The vertical space in \verb"mathpar" is adjusted by
+\verb"\MathparLineskip". To restore the normal paragraph parameters in mathpar
+mode (for instance for some inner paragraph), use the command
+\verb"\MathparNormalpar".
+The environment uses \verb"\MathparBindings" to
+rebind \verb"\\", \verb"and", and \verb"\par". You can redefine thus command
+to change the default bindings or add your own.
+
+
+\section {Examples}
+
+See the source of this documentation ---the file \lst"mathpartir.tex"---
+for full examples.
+
+\section {{\hevea} compatibility}
+
+The package also redefines \verb"\hva" to do nothing in \lst"mathpar"
+environment and in inference rules.
+
+In HeVeA, \verb"\and" will always produce a vertical break in mathpar
+environment; to obtain a horizontal break, use \verb"\hva \and" instead.
+Conversely, \verb"\\" will always produce a horizontal break in type
+inference rules; to obtain a vertical break, use \verb"\hva \\" instead.
+
+For instance, by default the following code,
+\begin{lstlisting}{Ocaml}
+\begin{mathpar}
+\inferrule* [Left=Foo]
+ {\inferrule* [Right=Bar,width=8em,
+ leftskip=2em,rightskip=2em,vdots=1.5em]
+ {a \\ a \\ bb \\ cc \\ dd}
+ {ee}
+ \\ ff \\ gg}
+ {hh}
+\and
+\inferrule* [lab=XX]{uu \\ vv}{ww}
+\end{mathpar}
+\end{lstlisting}
+which typesets in {\TeX} as follows,
+\begin{mathpar}
+\inferrule* [Left=Foo]
+ {\inferrule* [Right=Bar,width=8em,
+ leftskip=2em,rightskip=2em,vdots=1.5em]
+ {a \\ a \\ bb \\ cc \\ dd}
+ {ee}
+ \\ ff \\ gg}
+ {hh}
+\and
+\inferrule* [lab=XX]{uu \\ vv}{ww}
+\end{mathpar}
+would appear as follows with the compatible {\hevea} mode:
+\begin{mathpar}
+\inferrule* [left=Foo]
+ {\inferrule* [right=Bar]
+ {a \\ a \\ bb \\ cc \\ dd}
+ {ee}
+ \\ ff \\ gg}
+ {hh}
+\\
+\inferrule* [lab=XX]{uu \\ vv}{ww}
+\end{mathpar}
+To obtain (almost) the same rendering as in {\TeX}, it could be typed as
+\begin{lstlisting}[escapechar=\%]{Ocaml}
+ \begin{mathpar}
+ \inferrule* [Left=Foo]
+ {\inferrule* [Right=Bar,width=8em,
+ leftskip=2em,rightskip=2em,vdots=1.5em]
+ {a \\ a \hva \\ bb \\ cc \\ dd}
+ {ee}
+ \\ ff \\ gg}
+ {hh}
+ \hva \and
+ \inferrule* [lab=XX]{uu \\ vv}{ww}
+ \end{mathpar}
+ \end{lstlisting}
+ Actually, it would be typeset and follows with the compatible {\hevea} mode:
+ \begin{mathpar}
+ \inferrule* [left=Foo]
+ {\inferrule* [right=Bar]
+ {a \\ a \\\\ bb \\ cc \\ dd}
+ {ee}
+ \\ ff \\ gg}
+ {hh}
+ \and
+ \inferrule* [lab=XX]{uu \\ vv}{ww}
+\end{mathpar}
+
+%<*!hevea>
+ \DocInput{mathpartir.dtx}
+%</!hevea>
+
+\end{document}
+%</(driver|hevea)>
+% \fi
+%
+% \CheckSum{0}
+%
+% \CharacterTable
+% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+% Digits \0\1\2\3\4\5\6\7\8\9
+% Exclamation \! Double quote \" Hash (number) \#
+% Dollar \$ Percent \% Ampersand \&
+% Acute accent \' Left paren \( Right paren \)
+% Asterisk \* Plus \+ Comma \,
+% Minus \- Point \. Solidus \/
+% Colon \: Semicolon \; Less than \<
+% Equals \= Greater than \> Question mark \?
+% Commercial at \@ Left bracket \[ Backslash \\
+% Right bracket \] Circumflex \^ Underscore \_
+% Grave accent \` Left brace \{ Vertical bar \|
+% Right brace \} Tilde \~}
+%
+%
+% \changes{v1.3.1}{2015/11/06}{First version on CTAN}
+%
+% \GetFileInfo{mathpartir.dtx}
+%
+% \DoNotIndex{\newcommand,\newenvironment}
+%
+% \StopEventually{}
+%
+% \section{Implementation}
+%
+% \begin{macrocode}
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+%% \newdimen \mpr@tmpdim
+%% Dimens are a precious ressource. Uses seems to be local.
+\let \mpr@tmpdim \@tempdima
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+ \edef \MathparNormalpar
+ {\noexpand \lineskiplimit \the\lineskiplimit
+ \noexpand \lineskip \the\lineskip}%
+ }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+ {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+%\def \mpr@cr {\penalty -10000\vadjust{\vbox{}}\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+ \let \and \mpr@andcr
+ \let \par \mpr@andcr
+ \let \\\mpr@cr
+ \let \eqno \mpr@eqno
+ \let \hva \mpr@hva
+ }
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+ {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+ \noindent $\displaystyle\fi
+ \MathparBindings}
+ {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+\newenvironment{mathparpagebreakable}[1][]
+ {\begingroup
+ \par
+ \mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \mpr@prebindings \mpr@paroptions #1%
+ \vskip \abovedisplayskip \vskip -\lineskip%
+ \ifmmode \else $\displaystyle\fi
+ \MathparBindings
+ }
+ {\unskip
+ \ifmmode $\fi \par\endgroup
+ \vskip \belowdisplayskip
+ \noindent
+ \ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
+ \vbox \bgroup \tabskip 0em \let \\ \cr
+ \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+ \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+ \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+ \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+ \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
+ \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+ \mpr@flatten \mpr@all \mpr@to \mpr@one
+ \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+ \mpr@all \mpr@stripend
+ \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+ \ifx 1\mpr@isempty
+ \repeat
+}
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+ \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+%% Part III -- Type inference rules
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@vskip {}
+\def \mpr@htovlist {%
+ \setbox \mpr@hlist
+ \hbox {\strut
+ \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+ \unhbox \mpr@hlist}%
+ \setbox \mpr@vlist
+ \vbox {\if@premisse
+ \box \mpr@hlist
+ \ifx \mpr@vskip \empty \else
+ \hrule height 0em depth \mpr@vskip width 0em
+ \fi
+ \unvbox \mpr@vlist
+ \else
+ \unvbox \mpr@vlist
+ \ifx \mpr@vskip \empty \else
+ \hrule height 0em depth \mpr@vskip width 0em
+ \fi
+ \box \mpr@hlist
+ \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+% \setbox \mpr@hlist
+% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+% \setbox \mpr@vlist
+% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+% \else \unvbox \mpr@vlist \box \mpr@hlist
+% \fi}%
+% }
+
+\def \mpr@item #1{$\displaystyle #1$}
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+ \bgroup
+ \ifx #1T\@premissetrue
+ \else \ifx #1B\@premissefalse
+ \else
+ \PackageError{mathpartir}
+ {Premisse orientation should either be T or B}
+ {Fatal error in Package}%
+ \fi \fi
+ \def \@test {#2}\ifx \@test \mpr@blank\else
+ \setbox \mpr@hlist \hbox {}%
+ \setbox \mpr@vlist \vbox {}%
+ \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+ \let \@hvlist \empty \let \@rev \empty
+ \mpr@tmpdim 0em
+ \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+ \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+ \def \\##1{%
+ \def \@test {##1}\ifx \@test \empty
+ \mpr@htovlist
+ \mpr@tmpdim 0em %%% last bug fix not extensively checked
+ \else
+ \setbox0 \hbox{\mpr@item {##1}}\relax
+ \advance \mpr@tmpdim by \wd0
+ %\mpr@tmpdim 1.02\mpr@tmpdim
+ \ifnum \mpr@tmpdim < \hsize
+ \ifnum \wd\mpr@hlist > 0
+ \if@premisse
+ \setbox \mpr@hlist
+ \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+ \else
+ \setbox \mpr@hlist
+ \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
+ \fi
+ \else
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \else
+ \ifnum \wd \mpr@hlist > 0
+ \mpr@htovlist
+ \mpr@tmpdim \wd0
+ \fi
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \advance \mpr@tmpdim by \mpr@sep
+ \fi
+ }%
+ \@rev
+ \mpr@htovlist
+ \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+ \fi
+ \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+ \let\@@over\over % fallback if amsmath is not loaded
+ \let\@@overwithdelims\overwithdelims
+ \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+ \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+ }{}
+
+%% The default
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\mpr@over #2}$}}
+\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\@@atop #2}$}}
+
+\let \mpr@fraction \mpr@@fraction
+
+%% A generic solution to arrow
+
+\def \mpr@@fractionaboveskip {0ex}
+\def \mpr@@fractionbelowskip {0.22ex}
+
+\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
+ \def \mpr@tail{#1}%
+ \def \mpr@body{#2}%
+ \def \mpr@head{#3}%
+ \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
+ \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
+ \dimen0\ht3\advance\dimen0 by \dp3\relax
+ \dimen0 0.5\dimen0\relax
+ \advance \dimen0 by \mpr@@fractionaboveskip
+ \setbox1=\hbox {\raise \dimen0 \box1}\relax
+ \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
+ \advance \dimen0 by \mpr@@fractionbelowskip
+ \setbox2=\hbox {\lower \dimen0 \box2}\relax
+ \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
+ \dimen0=\wd0\box0
+ \box0 \hskip -\dimen0\relax
+ \hbox to \dimen0 {$%\color{blue}
+ \mathrel{\mpr@tail}\joinrel
+ \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
+ $}}}
+
+%% Old stuff should be removed in next version
+\def \mpr@@nothing #1#2
+ {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
+\def \mpr@@reduce #1#2{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+ {\bgroup
+ \ifnum \linewidth<\hsize \hsize \linewidth\fi
+ \mpr@rulelineskip
+ \let \and \qquad
+ \let \hva \mpr@hva
+ \let \@rulename \mpr@empty
+ \let \@rule@options \mpr@empty
+ \let \mpr@over \@@over
+ \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+ {\everymath={\displaystyle}%
+ \def \@test {#2}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+ \else
+ \def \@test {#3}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+ \else
+ \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+ \fi \fi
+ \def \@test {#1}\ifx \@test\empty \box0
+ \else \vbox
+%%% Suggestion de Francois pour les etiquettes longues
+%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+ {\hbox {\DefTirName {#1}}\box0}\fi
+ \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \\
+% Each \\ produces a break, attempting horizontal breaks if possible,
+% and vertical breaks if needed.
+%
+% An empty element obtained by \\\\ produces a vertical break in all cases.
+%
+% The former rule is aligned on the fraction bar.
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+%
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%
+% width set the width of the rule to val
+% narrower set the width of the rule to val\hsize
+% before execute val at the beginning/left
+% lab put a label [Val] on top of the rule
+% lskip add negative skip on the right
+% left put a left label [Val]
+% Left put a left label [Val], ignoring its width
+% right put a right label [Val]
+% Right put a right label [Val], ignoring its width
+% leftskip skip negative space on the left-hand side
+% rightskip skip negative space on the right-hand side
+% vdots lift the rule by val and fill vertical space with dots
+% after execute val at the end/right
+%
+% Note that most options must come in this order to avoid strange
+% typesetting (in particular leftskip must preceed left and Left and
+% rightskip must follow Right or right; vdots must come last
+% or be only followed by rightskip.
+%
+
+%% Keys that make sence in all kinds of rules
+\def \mprset #1{\setkeys{mprset}{#1}}
+\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
+\define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
+\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+% To be documented.
+\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction}
+\define@key {mprset}{sep}{\def\mpr@sep{#1}}
+\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
+\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
+\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def}
+\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
+\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
+\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
+\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def}
+\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
+\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
+\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+ \advance \hsize by -\wd0\box0}
+
+\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}}
+\define@key {mpr}{right}
+ {\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+ {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+\define@key {mpr}{vcenter}[]{\mpr@vcentertrue}
+
+\newif \ifmpr@vcenter \mpr@vcenterfalse
+\newcommand \mpr@inferstar@ [3][]{\begingroup
+ \setbox0 \hbox
+ {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+ \setbox \mpr@right \hbox{}%
+ \setkeys{mpr}{#1}%
+ $\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+ \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+ \box \mpr@right \mpr@vdots$
+ \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi}
+ \ifmpr@vcenter
+ \box0
+ \else
+ \setbox1 \hbox {\strut}
+ \@tempdima \dp0 \advance \@tempdima by -\dp1
+ \raise \@tempdima \box0
+ \fi
+ \endgroup}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode
+ \let \@do \mpr@inferstar@
+ \else
+ \let \@do \mpr@err@skipargs
+ \PackageError {mathpartir}
+ {\string\inferrule* can only be used in math mode}{}%
+ \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \TirNameStyle #1{\small \textsc{#1}}
+\def \LeftTirNameStyle #1{\TirNameStyle {#1}}
+\def \RightTirNameStyle #1{\TirNameStyle {#1}}
+
+\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}}
+\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}}
+\let \TirName \lefttir@name
+\let \LeftTirName \lefttir@name
+\let \DefTirName \lefttir@name
+\let \LabTirName \lefttir@name
+\let \RightTirName \righttir@name
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+% \end{macrocode}
+%
+% \Finale
+\endinput
diff --git a/macros/latex/contrib/mathpartir/mathpartir.ins b/macros/latex/contrib/mathpartir/mathpartir.ins
new file mode 100644
index 0000000000..cf0c3569db
--- /dev/null
+++ b/macros/latex/contrib/mathpartir/mathpartir.ins
@@ -0,0 +1,65 @@
+%%
+%% Copyright (C) 2015 by Didier Remy <didier.remy(at)inria(dot)fr>
+%%
+%% This file is part of mathpartir.
+%%
+%% mathpartir is free software: you can redistribute it and/or modify
+%% it under the terms of the GNU General Public License as published by
+%% the Free Software Foundation, either version 2 of the License, or
+%% (at your option) any later version.
+%%
+%% mathpartir is distributed in the hope that it will be useful,
+%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+%% GNU General Public License for more details.
+%%
+%% You should have received a copy of the GNU General Public License
+%% along with mathpartir. If not, see <http://www.gnu.org/licenses/>.
+%%
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/mathpartir}
+
+\preamble
+
+This is a generated file.
+
+Copyright (C) 2015 by Didier Remy <didier.remy(at)inria(dot)fr>
+
+This file is part of mathpartir.
+
+mathpartir is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 2 of the License, or
+(at your option) any later version.
+
+mathpartir is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with mathpartir. If not, see <http://www.gnu.org/licenses/>.
+
+\endpreamble
+
+\generate{\file{mathpartir.sty}{\from{mathpartir.dtx}{package}}}
+
+\obeyspaces
+\Msg{*************************************************************}
+\Msg{* *}
+\Msg{* To finish the installation you have to move the following *}
+\Msg{* file into a directory searched by TeX: *}
+\Msg{* *}
+\Msg{* mathpartir.sty *}
+\Msg{* *}
+\Msg{* To produce the documentation run the file mathpartir.dtx *}
+\Msg{* through PDFLaTeX. *}
+\Msg{* *}
+\Msg{* Happy TeXing! *}
+\Msg{* *}
+\Msg{*************************************************************}
+
+\endbatchfile
diff --git a/macros/latex/contrib/mathpartir/mathpartir.pdf b/macros/latex/contrib/mathpartir/mathpartir.pdf
new file mode 100644
index 0000000000..cc8f85581c
--- /dev/null
+++ b/macros/latex/contrib/mathpartir/mathpartir.pdf
Binary files differ