%Luca Vercelli 2009
%Intuitionistic (double-sided) proof nets
\ProvidesPackage{proofnet-int}

%KNOWN BUGS:
%you must load hyperref *before* this package
% \ncput* doesn't work. why???
%
% ==============================================================================
%
%DOCUMENTATION OF COMMANDS
%
%We use PSTricks, pst-node, psmatrix. Please refer their documentation.
%Each node has a /name/ to identify it;
%all arrows and boxes are drawn later over the nodes.
%Letters to identify nodes are not supported, but you can simulate it with \uput.
%
%ENVIRONMENTS FOR DRAWING PROOFNETS:
% \proofnet[psmatrix-parameters]{content}
% \proofnetcenter[psmatrix-param]{content}
% \proofnetpage[psmatrix-param]{width}{content}
% \proofnetscaled[psmatrix-param]{scale}{content}
% \proofnetpagescaled[psmatrix-param]{scale}{width}{content}
%All these environments set the following psmatrix parameters:
%all arrows have {->} as default style; nodesep=0; mathematical mode; \scriptstyle.
%Probably you want to set colsep and rowsep.
%In development time, probably psmatrix is better than proofnet
%
%NODES:
% \nVoid{name}  %equivalent to \Rnode{name}{}
% \simplenet{name}{caption}
% \simplebox{name}{caption}
% \nIn{name}
% \nOut{name}
% \nWea[caption]{name}
% \nDaem[caption]{name}
% \nCon[caption]{name}		Probably you want to set offsetA for the outgoing edges
% \nId[caption]{name}
% \nAx[caption]{name}  %equivalent to \nId
% \nCut{name}
% \nRlin{name}
% \nLlin{name}
% \nRtens{name}
% \nLtens{name}
% \nRfor{name}
% \nLfor{name}
% \nRP[caption]{name}
% \nLP[caption]{name}
%
%EDGES:
%The style is {->} and should not be modified.
% \ncup[par]{nodeA}{nodeB}                                if the line is straight, prefer \ncline to \ncup
% \ncupl[par]{nodeA}{nodeB}                               useful with \nRtens
% \ncupr[par]{nodeA}{nodeB}                               useful with \nRtens
% \ncdown[par]{nodeA}{nodeB}
% \ncldownup[armA=xxx,armB=xxx,par]{nodeA}{nodeB}         useful with \nRlin.
%
%From PSTricks:                                   Useful parameters
%                                                 nodesep,nodesepA,nodesepB,offset,offsetA,offsetB
% \ncline*[par]{arrows(*)}{nodeA}{nodeB}
% \ncarc*[par]{arrows(*)}{nodeA}{nodeB}           arcangle
% \ncdiag*[par]{arrows(*)}{nodeA}{nodeB}          angle,arm,armA,armB
% \ncdiagg*[par]{arrows(*)}{nodeA}{nodeB}         "
% \ncbar*[par]{arrows(*)}{nodeA}{nodeB}           "
% \ncangle*[par]{arrows(*)}{nodeA}{nodeB}         "
% \ncangles*[par]{arrows(*)}{nodeA}{nodeB}        "
% \ncloop*[par]{arrows(*)}{nodeA}{nodeB}          loopsize
% \nccurve*[par]{arrows(*)}{nodeA}{nodeB}         ncurve
% \nccircle*[par]{arrows(*)}{node}{radius}
%
%
% The (*) parameters can be omitted.
%
%EDGE LABELS. Exactly the ones of PSTricks:
%                                             Useful parameters
% \ncput*[par]{stuff}                         ref,nrot,labelsep,offset
% \naput*[par]{stuff}
% \nbput*[par]{stuff}
% \tvput*[par]{stuff}
% \tlput*[par]{stuff}  or  <[par]{stuff}
% \trput*[par]{stuff}  or  >[par]{stuff}
% \thput*[par]{stuff}
% \taput*[par]{stuff}  or  ^[par]{stuff}
% \tbput*[par]{stuff}  or  _[par]{stuff}
%WHY THE * VARIANTS DON'T WORK????????
%To place labels manually, use polar coordinates from /node/:
% \uput{distance}[angle]{text-rotation(*)}(node){stuff}
%(Notice \SpecialCoor is enabled)
%
%BOXES
% \abox[param...]{num-of-lower-nodes}{upper-node}{low-node-1}...{low-node-n}
%For closed boxes, consider setting the parameters:
% \abox[armA=xxx,armB=xxx,loopsize=xxx,par]{0}{upper-node}

% =================================================================================

\RequirePackage{pstricks,pst-node}
\RequirePackage{xifthen}
\RequirePackage{graphics} %maybe this is wrong.. you can use graphicx

%\simplenet[width]{name}{caption}
%\simplebox[width]{name}{caption}
\newcommand{\simplenet}[3][1cm]{\Rnode{#2}{\psframebox[shadowsize=2,linestyle=dashed]{
	\begin{minipage}{#1}
	\centering
	$ #3 $
	\end{minipage}
	}}}
\newcommand{\simplebox}[3][8mm]{\Rnode{#2}{\psframebox[linewidth=2pt]{
	\begin{minipage}{#1}
	\centering
	$ #3 $
	\end{minipage}
	}}}

\newcommand{\nVoid}[2][]{\Rnode[#1]{#2}{}}  %an empty node
\newcommand{\nIn}[2][]{\circlenode[#1]{#2}{\textnormal{\textbf i}}}  % Input node
\newcommand{\nOut}[2][]{\circlenode[#1]{#2}{\textnormal{\textbf o}}}  % Output node
\newcommand{\nWeak}[3][]{\cnode*[#1]{2pt}{#2}\rput[bl](2pt,0){\textnormal{\textbf W}#3}}  % Weakening
\newcommand{\nDaem}[3][]{\cnode*[#1]{2pt}{#2}\rput[bl](3pt,-2pt){\textnormal{\textbf h}#3}}  % Daemon (h) link
%\newcommand{\nCon}[2][]{\trinode[trimode=D]{#2}{\ \ }\rput(-10pt,-2pt){\textnormal{\textbf Y}#1}}  % Contraction
\newcommand{\nCont}[2][]{\ifthenelse{\isempty{#1}}
	{\trinode[trimode=D,linearc=0]{#2}{}}
	{\trinode[trimode=D,linearc=0,#1]{#2}{}}
	}  % Contraction
\newcommand{\nId}[2][]{\Rnode{#2}{\psframebox[#1]{\textnormal{\textbf I}}}}  % Identity
\newcommand{\nAx}[2][]{\nId[#1]{#2}}  %equivalent to \nId
\newcommand{\nCut}[2][]{\rnode{#2}{\psframebox[#1]{\textnormal{\textbf{Cut}}}}}  % Cut
\newcommand{\nRlin}[2][]{\ovalnode[#1]{#2}{\multimap_{\mathcal R}}}  % Right linear
\newcommand{\nLlin}[2][]{\ovalnode[#1]{#2}{\multimap_{\mathcal L}}}  % Left linear
\newcommand{\nRtens}[2][]{\ovalnode[#1]{#2}{\otimes_{\mathcal R}}}  % Right linear
\newcommand{\nLtens}[2][]{\ovalnode[#1]{#2}{\otimes_{\mathcal L}}}  % Left linear
\newcommand{\nRfor}[2][]{\ovalnode[#1]{#2}{\forall_{\mathcal R}}}  % Right forall
\newcommand{\nLfor}[2][]{\ovalnode[#1]{#2}{\forall_{\mathcal L}}}  % Left forall
% \newcommand{\nRP}[2][]{\ovalnode{#2}{\textnormal{\textbf Po}#1}}  % Right of course
% \newcommand{\nLP}[2][]{\ovalnode{#2}{\textnormal{\textbf Pi}#1}}  % Left of course
\newcommand{\nOC}[2][]{\ovalnode[#1]{#2}{!}}  % Right of course
\newcommand{\nOC}[2][]{\ovalnode[#1]{#2}{!}}  % Left of course

%ARROWS
\newcommand{\ncup}[3][]{
	\ifthenelse{\isempty{#1}}
		{\ncangle[angleA=90,angleB=-90]{->}{#2}{#3}}
		{\ncangle[angleA=90,angleB=-90,#1]{->}{#2}{#3}}
	}
\newcommand{\ncupl}[3][]{
	\ifthenelse{\isempty{#1}}
		{\ncangle[angleA=90,angleB=-135]{->}{#2}{#3}}
		{\ncangle[angleA=90,angleB=-135,#1]{->}{#2}{#3}}
	}
\newcommand{\ncupr}[3][]{
	\ifthenelse{\isempty{#1}}
		{\ncangle[angleA=90,angleB=-45]{->}{#2}{#3}}
		{\ncangle[angleA=90,angleB=-45,#1]{->}{#2}{#3}}
	}
\newcommand{\ncdown}[3][]{
	\ifthenelse{\isempty{#1}}
		{\ncangle[angleA=-90,angleB=90]{->}{#2}{#3}}
		{\ncangle[angleA=-90,angleB=90,#1]{->}{#2}{#3}}
	}
\newcommand{\ncldownup}[3][]{ %probably you want to set armA and armB
	\ifthenelse{\isempty{#1}}
		{\ncangles[angleA=180,angleB=-90]{->}{#2}{#3}	}
		{\ncangles[angleA=180,angleB=-90,#1]{->}{#2}{#3}	}
	}

%BOXES--------------------------------------------------------------------

\newcounter{aboxcounter}

\newcommand{\abox}[3][] { %\abox[param]{lower-boxes-counter}{upper}
	\setcounter{aboxcounter}{#2}
	\ifthenelse{\value{aboxcounter}<0}
		{\PackageError{proofnet}
				{Illegal number of premise nodes for \protect\abox}
				{\protect\abox first argument must be nonnegative}
			\stop
		}
		{\ifthenelse{\value{aboxcounter}=0} %closed box
			{\ifthenelse{\isempty{#1}}
				{\ncloop[angleA=180,linewidth=2pt]{-}{#3}{#3} }
				{\ncloop[angleA=180,linewidth=2pt,#1]{-}{#3}{#3} }
			}
			{\aboxmorearguments[#1]{#3}}
		}
}

\newcommand{\aboxmorearguments}[3][]{ %\aboxmorearguments[param]{upper}{first}
	\ifthenelse{\isempty{#1}}
		{\ncangle[angleA=180,angleB=180,linewidth=2pt]{-}{#2}{#3}}
		{\ncangle[angleA=180,angleB=180,linewidth=2pt,#1]{-}{#2}{#3}}
	\ifthenelse{\value{aboxcounter}=1}
		{\aboxlastline[#1]{#2}{#3}}
		{\aboxlowerline[#1]{#2}{#3}}
	}

\newcommand{\aboxlowerline}[4][]{ %\aboxlowerline[param]{upper}{first}{second}
	\ifthenelse{\isempty{#1}}
		{\ncline[angleA=0,angleB=180,linewidth=2pt]{-}{#3}{#4}}
		{\ncline[angleA=0,angleB=180,linewidth=2pt,#1]{-}{#3}{#4}}
	\ifthenelse{\value{aboxcounter}=2}
		{\aboxlastline[#1]{#2}{#4}}
		{
			\addtocounter{aboxcounter}{-1}
			\aboxlowerline[#1]{#2}{#4}
		}
	}

\newcommand{\aboxlastline}[3][]{ %\aboxlastline[param]{upper}{lower}
	\ifthenelse{\isempty{#1}}
		{\ncangle[angleA=0,angleB=0,linewidth=2pt]{-}{#2}{#3}}
		{\ncangle[angleA=0,angleB=0,linewidth=2pt,#1]{-}{#2}{#3}}
	}

%-----------------------------------------------------------------------------

%default separation values. Can be changed before every \proofnet, or
%can be setted as optional argument in \proofnet
\psset{colsep=10pt}
\psset{rowsep=10pt}
\psset{labelsep=1pt}
\psset{linearc=2pt}

% PROOF NET ENVIRONMENTS
\newcommand{\proofnet}[2][]{
  $\psset{nodesep=0pt}
  \everypsbox{\scriptstyle}
  \psset{arrows=->}
  \ifthenelse{\isempty{#1}}
    {
    \begin{psmatrix}
    #2
    \end{psmatrix}
    }
    {
    \begin{psmatrix}[#1]
    #2
    \end{psmatrix}
    }
  $
  }

\newcommand{\proofnetcenter}[2][]{
	\begin{center}
	\proofnet[#1]{#2}
	\end{center}
	}

\newcommand{\proofnetpage}[3][]{
	\begin{minipage}{#2}
	\begin{center}
	\proofnet[#1]{#3}
	\end{center}
	\end{minipage}
	}

\newcommand{\proofnetscaled}[3][]{
	\begin{center}
	\scalebox{#2}{\proofnet[#1]{#3}}
	\end{center}
	}

\newcommand{\proofnetpagescaled}[4][]{
	\begin{minipage}{#3}
	\begin{center}
	\scalebox{#2}{\proofnet[#1]{#4}}
	\end{center}
	\end{minipage}
	}


\SpecialCoor  %enables special coordinates