%%
%% This is file `NaturalDeduction.sty'.
%%
%% Copyright (C) 2015-2020
%% by Nicolas Fillion <nfillion@sfu.ca>
%%
%% A flexible set of macros for Fitch-style natural deduction that supports overlay in Beamer and other TikZ-related options. 
%% Author: Nicolas Fillion, Simon Fraser University
%% Created: July 20, 2015
%% Modified: May 13, 2020
%% Version: 1.3
%% Documentation: NaturalDeductionSTY-Documentation.tex
%% URL: http://www.nfillion.com
%%
%% LICENSE:
%% This program is free software that can be distributed and/or modified under the conditions
%% of the LaTeX Project Public License, either version 1.3c or the latest version, as the case
%% may be. The latest version of this license is available at http://www.latex-project.org/lppl.txt
%% and version 1.3c or later is part of all distributions of LaTeX version 2005/12/01 or later.
%% 
%% This work is "maintained" (as per the LPPL maintenance status) by Nicolas Fillion. Please report any bug or requests for
%% additional functionality by email.
%%
%% USAGE EXAMPLE WITHOUT OVERLAY:
%% 
%% The following is a simple example illustrating the usage of this %% package.  For detailed
%% instructions and additional functionality, see the user guide, which can be found in the file
%% NaturalDeductionSTY-Documentation.tex.
%% \begin{fitch}
%% \prem{1}{\forall x Px}{Prem}
%% \prem{2}{\exists x\neg Px}{Prem}
%% \open
%% \getline{3}{\forall z (Pz\vee Qz)}{Supp/CP}
%% \open
%% \getline{4}{\neg R}{Supp/RA}
%% \getline{5}{\neg Pi}{$\exists$E 2}
%% \getline{6}{Pi}{$\forall$E 1}
%% \getline{7}{\bot}{$\bot$I 5,6}
%% \close
%% \getline{8}{R}{RA 4--7}
%% \close
%% \getline[number=changed number]{9}{\forall z (Pz\vee Qz)\to R}{CP 2--8}
%% \end{fitch}
%%
%% Package options with default values
%% use as \usepackage[option1,option2,etc]{NaturalDeduction} or as \begin{fitch}[option1,option2,etc.] 
%% JustPos=3.5
%% JustSpace=.25 
%% LineSpacing=0.7
%% IndentWidth=0.7
%% NumberSpacing=0 
%% FontSize=normalsize
%% Scale=1
%% PremLine=true
%% SuppLine=true
%% MainScopeLine=true
%% ScopeLines=true
%% NoStructure=true
%% MathModeFormula=false
%%
%% Options for the commands \prem and \getline
%% number=x % to display a different string as line number
%% nonumber=false
%%
%% add beamer options on, of, oj for the uncover number of each node of a line
%%
%% Package Identification
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{NaturalDeduction}[2018/01/09 v1.3 Natural Deduction Package based on TikZ and supporting Beamer overlay]
%
%
%% Package Requirements
\RequirePackage{tikz}
\RequirePackage{kvoptions}
\RequirePackage{fmtcount}
%
%
%% Set key values family and prefix
\SetupKeyvalOptions{
	family=ND,
	prefix=ND@}		
%Declare options
% 1. Package loading options
\DeclareStringOption[3.5]{JustPos} %optional setup option for justification position
\DeclareStringOption[.25]{JustSpace} %optional setup option for space between supposition lines and justification
\DeclareStringOption[.7]{LineSpacing} %optional setup option for space between lines
\DeclareStringOption[.7]{IndentWidth} %optional setup for the width of indentation of subproofs
\DeclareStringOption[0]{NumberSpacing} %optional setup for the space between line numbers and main scope line
\DeclareStringOption[normalsize]{FontSize}
\DeclareStringOption[1]{Scale}
\DeclareStringOption[5cm]{CommentWidth}
%
\DeclareBoolOption[true]{PremLine}
\DeclareBoolOption[true]{SuppLine}
\DeclareBoolOption[true]{MainScopeLine}
\DeclareBoolOption[true]{ScopeLines}
\DeclareBoolOption[false]{NoStructure}
\DeclareBoolOption[false]{ArthurStyle}
\DeclareBoolOption[false]{BergmannStyle}
\DeclareBoolOption[false]{Overlay}
\DeclareBoolOption[false]{MathModeFormula}
% 2. Command options
\DeclareStringOption[0]{number} %optional line number parameter
\DeclareBoolOption[false]{nonumber}
\DeclareStringOption[1]{on}
\DeclareStringOption[1]{of}
\DeclareStringOption[1]{oj}
\DeclareStringOption[1]{oa}
\DeclareStringOption[1]{oc}
% Process Options
%\setkeys{ND}{option}%that would set defaults.	
\ProcessKeyvalOptions{ND}


% Setup the consequences of the omnibus option NoStructure
\ifND@NoStructure
	\setkeys{ND}{PremLine=false,SuppLine=false,MainScopeLine=false,ScopeLines=false,IndentWidth=0}
\fi

% Setup the consequences of the omnibus option NoStructure
\ifND@ArthurStyle
	\setkeys{ND}{PremLine=false,SuppLine=false,MainScopeLine=false,ScopeLines=true}
\fi

\ifND@BergmannStyle
	\setkeys{ND}{PremLine=true,SuppLine=true,MainScopeLine=true,ScopeLines=true}
\fi


% Define counters
\newcounter{leftindent} % a counter used throughout keeping track of the subproof number
\newcounter{numberoflines} %count how many lines (\line and \prem) are in the proof
\newcounter{numberofprems} % count how many premises are in the proof

% Define new environment
\newenvironment{fitch}[1][]
	%At the beginning of the environment
	{ 
	\setkeys{ND}{#1}
	\begin{tikzpicture}[font=\csname \ND@FontSize\endcsname,scale=\ND@Scale]
	}
	%At the end of the environment %%%%%%%%%%%%%%%%%%%%%%
	{
	%If no line, add a token empty line to avoid error messages
	\ifnum\thenumberoflines<1
		\draw (0,0) node (emptynode) {};
		\def\topline_2{emptynode}
		\def\bottomline_2{emptynode}
	\fi
	%Store coordinate of top of diagram
	\newdimen\topcoord
	\pgfextracty{\topcoord}{\pgfpointanchor{\topline_2}{north}}
	\newdimen\bottomcoord
	\pgfextracty{\bottomcoord}{\pgfpointanchor{\bottomline_2}{south}}
	%Add a main scope line
	\ifnum\thenumberoflines>0
		\ifND@MainScopeLine
			\draw (0,\topcoord) edge (0,\bottomcoord);
		\fi
	\fi
	%Add a hypothesis line
	\ifnum\thenumberofprems>0
	\ifND@PremLine
		\ifcsdef{lastprem}{\draw ([yshift=-.5\baselineskip]\lastprem_2.west) edge ([xshift=-\ND@JustSpace cm,yshift=-.5\baselineskip]\lastprem_3.west);}
	\fi
	\else
	% \draw (0,0) node {there are no premises in this diagram!};
	\fi
	%Closing commands
	\end{tikzpicture}
	% Reset counters when the environment closes so latex doesn't remember it next time a fitch environment is opened
	\setcounter{leftindent}{0} 
	\setcounter{numberoflines}{0}
	\setcounter{numberofprems}{0}
	}


% Define the commands \open and \close managing subproofs
\newcommand{\open}{%
	\addtocounter{leftindent}{1}
	}
\newcommand{\close}[1][]{%
	%Put code for the scope line here, with a conditional on the style Boolean
	\def\topnodenum{\csname firstline\roman{leftindent}\endcsname}
	\def\bottomnodenum{\csname lastline\roman{leftindent}\endcsname}	
	\ifND@ScopeLines
		\ifND@Overlay
			\def\temp{#1}\ifx\temp\empty % make sure the argument of \close isn't empty to avoid error
			\draw (\topnodenum_2.north west) edge (\bottomnodenum_2.south west);
			\else			
			\uncover<#1->{\draw (\topnodenum_2.north west) edge (\bottomnodenum_2.south west);}
			\fi
		\else
		\draw (\topnodenum_2.north west) edge (\bottomnodenum_2.south west);
		\fi	
	\fi
	%Adjust counter
	\expandafter\let\csname firstline\roman{leftindent}\endcsname\undefined
	\expandafter\let\csname lastline\roman{leftindent}\endcsname\undefined
	\let\topnodenum\undefined
	\let\bottomnodenum\undefined
	\addtocounter{leftindent}{-1}	
	}
	

%Dynamic macro definition for the \firstline and \lastline set of commands (one for each subpoof).
\newcommand\updatescopeinfo[2]{%                                                         
	%Family of \firstlines
	\ifcsdef{firstline#1}{
			%command is defined
			\ifnum#2<\csname firstline#1\endcsname
				\expandafter\renewcommand\csname firstline#1\endcsname{#2}
			\fi
			}{
			%command is undefined
			\expandafter\newcommand\csname firstline#1\endcsname{#2}
			}
	%Family of \lastlines
	\ifcsdef{lastline#1}{
			%command is defined
			\ifnum#2>\csname lastline#1\endcsname
				\expandafter\renewcommand\csname lastline#1\endcsname{#2}
			\fi
			}{
			%command is undefined
			\expandafter\newcommand\csname lastline#1\endcsname{#2}
			}
}


%Keep track of the line number of the first and last line to draw main scope line
\newcommand\storetopbottomcoord[1]{%
	\ifcsdef{topline}{
		\ifnum\topline>#1
			\def\topline{#1}
		\fi
		}{
		\def\topline{#1}
		}
	\ifcsdef{bottomline}{
		\ifnum\bottomline<#1
			\def\bottomline{#1}
		\fi
		}{
		\def\bottomline{#1}
		}
	}	


%The main line command
\DeclareRobustCommand{\getline}[4][]{%
	%Set the keys
	\setkeys{ND}{#1}
	%Process batch overlay information
	%Update scope line information
	\updatescopeinfo{\roman{leftindent}}{#2}
	%Update counters
	\addtocounter{numberoflines}{1}
	%Conditionally define the line number tag
	\if\ND@number0
	\def\numbertag{#2}
	\else
	\def\numbertag{\ND@number}
	\fi
	% Ensure that on, of, oj are defined. First, with keyval, else oa, else 1.
	\ifx\ND@on\relax
		\ifx\ND@oa\relax
		\def\ND@on{1}
		\else
		\def\ND@on{\ND@oa}
		\fi
	\else
	\fi
	%
	\ifx\ND@of\relax
		\ifx\ND@oa\relax
		\def\ND@of{1}
		\else
		\def\ND@of{\ND@oa}
		\fi
	\else
	\fi
	%
	\ifx\ND@oj\relax
		\ifx\ND@oa\relax
		\def\ND@oj{1}
		\else
		\def\ND@oj{\ND@oa}
		\fi
	\else
	\fi
	%Actually draw the line
	%Number node
	\ifND@Overlay
		\uncover<\ND@on->{\draw (-\ND@NumberSpacing,-#2*\ND@LineSpacing) node[anchor=east] (#2_1) {\ifND@nonumber \else (\numbertag)\fi };}
	\else
	\draw (-\ND@NumberSpacing,-#2*\ND@LineSpacing) node[anchor=east] (#2_1) {\ifND@nonumber \else (\numbertag)\fi };
	\fi
	%Formula node
	\ifND@Overlay
		\uncover<\ND@of->{ \draw (\value{leftindent}*\ND@IndentWidth,-#2*\ND@LineSpacing) node[anchor=west] (#2_2) {
			\ifND@MathModeFormula\ensuremath{#3}\else#3\fi
			};}
	\else
	\draw (\value{leftindent} * \ND@IndentWidth, - #2 * \ND@LineSpacing) node[anchor=west] (#2_2) {
		\ifND@MathModeFormula\ensuremath{#3}\else #3\fi
		};
	\fi
	%Justification node
	\ifND@Overlay
		\uncover<\ND@oj->{	\draw (\ND@JustPos,-#2*\ND@LineSpacing) node[anchor=west] (#2_3) {#4}; }
	\else
	\draw (\ND@JustPos,-#2*\ND@LineSpacing) node[anchor=west] (#2_3) {#4}; 
	\fi
	%Store y coordinate of top and bottom of diagram
	\storetopbottomcoord{#2}
	%Decide whether to add a hypothesis horizontal line
	\ifND@SuppLine
	\if\theleftindent0
	\else
		\ifnum\numexpr\csname firstline\roman{leftindent}\endcsname =#2
			\ifND@Overlay
			\uncover<\ND@of->{\draw ([yshift=-.5\baselineskip]#2_2.west) edge ([xshift=-\ND@JustSpace cm,yshift=-.5\baselineskip]#2_3.west);}
			\else
			\draw ([yshift=-.5\baselineskip]#2_2.west) edge ([xshift=-\ND@JustSpace cm,yshift=-.5\baselineskip]#2_3.west);
			\fi
		\fi
	\fi
	\fi
	%Keys to reset
	 \def\ND@number{0}
	 \let\ND@oa\relax
	 \let\ND@on\relax
	 \let\ND@of\relax
	 \let\ND@oj\relax
	\ND@nonumberfalse
}
	

%The prem command
\DeclareRobustCommand{\prem}[4][]{%
	%Set the keys
	\let\ND@on\relax
	\let\ND@of\relax
	\let\ND@oj\relax
	\setkeys{ND}{#1}
	%Update scope line information
	\updatescopeinfo{\roman{leftindent}}{#2}
	% Update counters
	\addtocounter{numberoflines}{1}
	\addtocounter{numberofprems}{1}
	%Conditionally define the line number tag
	\if\ND@number0
 	\def\numbertag{#2}
	\else
	\def\numbertag{\ND@number}
	\fi
	% Ensure that on, of, oj are defined. First, with keyval, else oa, else 1.
	\ifx\ND@on\relax
		\ifx\ND@oa\relax
		\def\ND@on{1}
		\else
		\def\ND@on{\ND@oa}
		\fi
	\else
	\fi
	%
	\ifx\ND@of\relax
		\ifx\ND@oa\relax
		\def\ND@of{1}
		\else
		\def\ND@of{\ND@oa}
		\fi
	\else
	\fi
	%
	\ifx\ND@oj\relax
		\ifx\ND@oa\relax
		\def\ND@oj{1}
		\else
		\def\ND@oj{\ND@oa}
		\fi
	\else
	\fi
	%Actually draw the line
	%Number node	 
	\ifND@Overlay
		\uncover<\ND@on->{\draw (-\ND@NumberSpacing,-#2*\ND@LineSpacing) node[anchor=east] (#2_1) {\ifND@nonumber \else (\numbertag)\fi };}
	\else
	\draw (-\ND@NumberSpacing,-#2*\ND@LineSpacing) node[anchor=east] (#2_1) {\ifND@nonumber \else (\numbertag)\fi };
	\fi	
	%Formula node
	\ifND@Overlay
		\uncover<\ND@of->{	\draw (\value{leftindent}*\ND@IndentWidth,-#2*\ND@LineSpacing) node[anchor=west] (#2_2) {
			\ifND@MathModeFormula\ensuremath{#3}\else#3\fi
			};}		
	\else
	\draw (\value{leftindent} * \ND@IndentWidth, - #2 * \ND@LineSpacing) node[anchor=west] (#2_2) {
		\ifND@MathModeFormula\ensuremath{#3}\else #3\fi
		};
	\fi		
	%Justification node
	\ifND@Overlay
		\uncover<\ND@oj->{	\draw (\ND@JustPos,-#2*\ND@LineSpacing) node[anchor=west] (#2_3) {#4}; }		
	\else
	\draw (\ND@JustPos,-#2*\ND@LineSpacing) node[anchor=west] (#2_3) {#4}; 
	\fi
	%Store y coordinate of top and bottom of diagram
	\storetopbottomcoord{#2}
	%Keep track of last premise for the premise line
	\ifcsdef{lastprem}{
		\ifnum\lastprem<#2
			\def\lastprem{#2}
		\fi
		}{
		\def\lastprem{#2}
		}
	%Keys to reset
	 \def\ND@number{0}
	 \let\ND@oa\relax
	 \let\ND@on\relax
	 \let\ND@of\relax
	 \let\ND@oj\relax
	 \ND@nonumberfalse
}


%The comment command
\DeclareRobustCommand{\comment}[3][]{%
	%Set the keys
	\let\ND@oc\relax
	\setkeys{ND}{#1}
	%Actually draw the comment
	\ifND@Overlay
		\@ifundefined{ND@oc}{
		\uncover<\ND@oa>{		\node[right of=#2_3,xshift=3mm,anchor=west,text width=\ND@CommentWidth] {#3}; }
	}{
	\uncover<\ND@oc>{		\node[right of=#2_3,xshift=3mm,anchor=west,text width=\ND@CommentWidth] {#3}; }		
		}
	\else
	\node[right of=#2_3,xshift=3mm,anchor=west,text width=\ND@CommentWidth] {#3};
	\fi
}

		
\endinput
%%
%% End of file `NaturalDeduction.sty'