\NeedsTeXFormat{LaTeX2e}[1995/12/01]
\ProvidesPackage{inference}[2009/01/08 v1.0 (F.Guidi)]

\RequirePackage{txfonts}

% logical constants backend
\newcommand*\lvalue[1]{\mathord{#1}}
\newcommand*\linfix[4]{{\def\trd{#3}\trd\ifx\trd\empty\mathord\else#1\fi{#2}{#4}}}
\newcommand*\lrel[3]{\linfix{\mathrel}{#1}{#2}{#3}}
\newcommand*\lbin[3]{\linfix{\mathbin}{#1}{#2}{#3}}

% logical constants frontend
\newcommand*\ltop{\lvalue{\top}}
\newcommand*\lzero{\lvalue{0}}
\newcommand*\lone{\lvalue{1}}
\newcommand*\lbot{\lvalue{\bot}}
\newcommand*\lamp[2]{\lrel{\&}{#1}{#2}}
\newcommand*\lplus[2]{\lrel{\oplus}{#1}{#2}}
\renewcommand*\ltimes[2]{\lrel{\otimes}{#1}{#2}}
\newcommand*\lpar[2]{\lrel{\invamp}{#1}{#2}}
\newcommand*\limp[2]{\lrel{\rightarrow}{#1}{#2}}
\newcommand*\lexcl[2]{\lrel{\leftarrow}{#1}{#2}}
\newcommand*\llin[2]{\lrel{\multimap}{#1}{#2}}
\newcommand*\lsup[2]{\lrel{\supset}{#1}{#2}}
\newcommand*\lent[2]{\lrel{@}{#1}{#2}}

% meta-logical constants 
\newcommand*\ment[2]{{\def\fst{#1}\def\snd{#2}\fst
 \ifx\fst\empty\ifx\snd\empty\mathord\else\mathrel\fi\else\mathrel\fi
 \vdash\snd}}

% inference rules backend
\newcommand*\ilabel[1]{\rlap{\,\scriptsize{#1}}}
\newcommand*\imain[1]{\begin{tabular}{c}$#1$\end{tabular}}
\newcommand*\itree[1]{\begin{tabular}[b]{c}$#1$\end{tabular}}
\newcommand*\iassume[2]{{\def\snd{#2}\ifx\snd\empty{#1}\else[#1]^{#2}\fi}}
\newcommand*\istep[1]{$\\\noalign{\vskip-5\doublerulesep}\hrulefill\ilabel{#1}\\\noalign{\vskip-2\doublerulesep}$}
\newcommand*\idischarge[2]{\istep{{#1}\ {#2}}}
\newcommand*\iline[1]{$\\\vline\ilabel{#1}\\$}

% inference rules frontend
\newcommand*\irule[3]{\itree{#1\istep{#2}#3}}
\newcommand*\idrule[4]{\itree{#1\idischarge{#2}{#3}#4}}
\newcommand*\itrack[3]{\itree{#1\iline{#2}#3}}
\newcommand*\iatrack[4]{\itree{\iassume{#1}{#2}\iline{#3}#4}}

\newcommand*\imrule[3]{\imain{#1\istep{#2}#3}}
\newcommand*\idmrule[4]{\imain{#1\idischarge{#2}{#3}#4}}
\newcommand*\imtrack[3]{\imain{#1\iline{#2}#3}}
\newcommand*\iamtrack[4]{\imain{\iassume{#1}{#2}\iline{#3}#4}}

% inference rules labels
\newcommand*\iid{id}
\newcommand*\irefl{refl}
\newcommand*\icut[1]{cut{#1}}
\newcommand*\itop[1]{$\ltop${#1}}
\newcommand*\izero[1]{$\lzero${#1}}
\newcommand*\ione[1]{$\lone${#1}}
\newcommand*\ibot[1]{$\lbot${#1}}
\newcommand*\iimp[1]{$\limp{}{#1}$}
\newcommand*\isup[1]{$\lsup{}{#1}$}
\newcommand*\iexcl[1]{$\lexcl{}{#1}$}
\newcommand*\iany[1]{$#1$}

\endinput