%Luca Vercelli 2009
%classical (one-sided) proof nets
\ProvidesPackage{proofnet}

%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}
	}}}

%%% NODES
\newcommand{\nVoid}[2][]{\rnode[#1]{#2}{}}  % void node
\newcommand{\nLab}[3][]{\Rnode[#1]{#2}{#3}}  % label node
\newcommand{\nAx}[2][]{\ovalnode[#1]{#2}{\frown}}  % Axiom
\newcommand{\nId}[2][]{\nAx[#1][#2]}  % Axiom
\newcommand{\nCut}[2][]{\ovalnode[#1]{#2}{\stackrel{\smile}{}}}  % Cut
\newcommand{\nWeak}[2][]{\ovalnode[#1]{#2}{W}}  % Weakening
\newcommand{\nCont}[2][]{\ifthenelse{\isempty{#1}}
	{\trinode[trimode=D,linearc=0]{#2}{}}
	{\trinode[trimode=D,linearc=0,#1]{#2}{}}
	}  % Contraction
\newcommand{\nTens}[2][]{\ovalnode[#1]{#2}{\otimes}}  % Tensor
\newcommand{\nPar}[2][]{\ovalnode[#1]{#2}{\parr}}  % Co-tensor
\newcommand{\nFor}[2][]{\ovalnode[#1]{#2}{\forall}}  % Forall
\newcommand{\nEx}[2][]{\ovalnode[#1]{#2}{\exists}}  % Existential
\newcommand{\nOC}[2][]{\circlenode[#1]{#2}{!}}  % Of course
\newcommand{\nWN}[2][]{\circlenode[#1]{#2}{?}}  % Why not
\newcommand{\nParag}[2][]{\circlenode[#1]{#2}{\S}}  % Paragraph
\newcommand{\nPax}[2][]{\circlenode[#1]{#2}{\mbox{\tiny pax}}}
\newcommand{\nFlat}[2][]{\circlenode[#1]{#2}{\fls}}  % Flat
\newcommand{\nDer}[2][]{\ovalnode[#1]{#2}{Der}}  % Dereliction
\newcommand{\nDig}[2][]{\ovalnode[#1]{#2}{Dig}}  % Dereliction

%ARROWS
\newcommand{\ncup}[3][]{
	\ifthenelse{\isempty{#1}}
		{\nccurve[angleA=90,angleB=-90]{->}{#2}{#3}}
		{\nccurve[angleA=90,angleB=-90,#1]{->}{#2}{#3}}
	}
\newcommand{\ncupl}[3][]{
	\ifthenelse{\isempty{#1}}
		{\nccurve[angleA=90,angleB=-135]{->}{#2}{#3}}
		{\nccurve[angleA=90,angleB=-135,#1]{->}{#2}{#3}}
	}
\newcommand{\ncupr}[3][]{
	\ifthenelse{\isempty{#1}}
		{\nccurve[angleA=90,angleB=-45]{->}{#2}{#3}}
		{\nccurve[angleA=90,angleB=-45,#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 (for \uput)