From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Mon, 2 Sep 2019 13:46:59 +0900 Subject: Initial commit --- macros/latex/contrib/mathpartir/COPYING | 340 +++++++ macros/latex/contrib/mathpartir/README | 35 + macros/latex/contrib/mathpartir/mathpartir.dtx | 1273 ++++++++++++++++++++++++ macros/latex/contrib/mathpartir/mathpartir.ins | 65 ++ macros/latex/contrib/mathpartir/mathpartir.pdf | Bin 0 -> 265615 bytes 5 files changed, 1713 insertions(+) create mode 100644 macros/latex/contrib/mathpartir/COPYING create mode 100644 macros/latex/contrib/mathpartir/README create mode 100644 macros/latex/contrib/mathpartir/mathpartir.dtx create mode 100644 macros/latex/contrib/mathpartir/mathpartir.ins create mode 100644 macros/latex/contrib/mathpartir/mathpartir.pdf (limited to 'macros/latex/contrib/mathpartir') 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. + + + Copyright (C) + + 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. + + , 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 +% +% 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 . +% +% \fi +% +% \iffalse +%<*driver> +\ProvidesFile{mathpartir.dtx} +% +%\NeedsTeXFormat{LaTeX2e} +%\ProvidesPackage{mathpartir} +%<*package> + [2016/02/24 version 1.3.2 Math Paragraph for Typesetting Inference Rules] +% +% +%\documentclass {article} +%<*driver> +\documentclass{ltxdoc} +% +%<*(driver|hevea)> +\usepackage {mathpartir} +\usepackage {listings} +\usepackage {array} +\usepackage {url} +%\usepackage {hevea} + +\lstset {basicstyle=\tt} +\let \lst \verb + +\title { +%\begin{tabular}{>{\huge}c} +\textbf{MATH} formulas in \\ +\textbf{PAR}ragraph mode\\[-1ex] +%<*!hevea> +\hskip 0em\hbox to 12em {\hrulefill}\\ +% +%\hline +\textbf Typesetting \textbf Inference \textbf Rules \\ +%\end{tabular} +} +\author {Didier R{\'{e}}my} +\date {(Version 1.3.2, last modified 24/02/2016)} + +\begin{document} + +\maketitle + +%<*!hevea> +\DeleteShortVerb{\|} +\section{Introduction} +% +%\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. +% \end{abstract} + +%\section {License} +% +%Mathpartir is Copyright (C) 2001-2005, 2015, 2016 INRIA. Mathpartir +%has been developed by Didier R{\'{e}}my. 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, or (at your option) any later version. See the GNU General Public +%License for more details (\url{http://pauillac.inria.fr/~remy/license/GPL}). +%Mathpartir is distributed in the hope that it will be useful, but without +%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} +} +$$ +%\one +%<*!hevea> +\fbox {\vbox {\advance \hsize by -2\fboxsep \advance \hsize by -2\fboxrule + \linewidth\hsize + $$\one$$}} +% +$$ +However, the same formula on a narrower page will automatically be typeset +like that: +$$ +%\one +%<*!hevea> +\fbox {\hsize 0.33 \hsize \vbox {$$\one$$}} +% +$$ +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} +% + +\end{document} +% +% \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 +%% +%% 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 . +%% + +\input docstrip.tex +\keepsilent + +\usedir{tex/latex/mathpartir} + +\preamble + +This is a generated file. + +Copyright (C) 2015 by Didier Remy + +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 . + +\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 Binary files /dev/null and b/macros/latex/contrib/mathpartir/mathpartir.pdf differ -- cgit v1.2.3