%% fitch.sty
%% Macros for Fitch-style natural deduction
%% Copyright 2002-2023 Peter Selinger
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
%   https://www.latex-project.org/lppl.txt
% and version 1.3c or later is part of all distributions of LaTeX
% version 2008 or later.
%
% This work has the LPPL maintenance status `maintained'.
% 
% The Current Maintainer of this work is Richard Zach <rzach@ucalgary.ca>
%
% This work consists of the files fitch.sty and fitchdoc.tex.

% Original Author: Peter Selinger, Dalhousie University
% Created: Jan 14, 2002
% Modified: December 17, 2023
% Version: 1.0
% Copyright: (C) 2002-2005 Peter Selinger, Richard Zach
% Filename: fitch.sty
% Documentation: fitchdoc.tex
% https://github.com/OpenLogicProject/fitch/

% USAGE EXAMPLE:
% 
% 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 fitchdoc.tex.
% 
% \[
% \begin{nd}
%   \hypo{1}  {P\vee Q}   
%   \hypo{2}  {\neg Q}                         
%   \open                              
%   \hypo{3a} {P}
%   \have{3b} {P}        \r{3a}
%   \close                   
%   \open
%   \hypo{4a} {Q}
%   \have{4b} {\neg Q}   \r{2}
%   \have{4c} {\bot}     \ne{4a,4b}
%   \have{4d} {P}        \be{4c}
%   \close                             
%   \have{5}  {P}        \oe{1,3a-3b,4a-4d}                 
% \end{nd}
% \]

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{fitch}[2023-12-17 v1.0 Macros for Fitch-style natural deduction]

% Define keyval options

\RequirePackage{kvoptions}

\SetupKeyvalOptions{
family = fitch,
prefix = nd@ % prefix with nd@ for compatibility with old code
}

\DeclareStringOption[ndrules]{rules}
\DeclareStringOption[array]{arrayenv}
\DeclareStringOption[ndjustformat]{justformat}
\DeclareStringOption[ndrefformat]{refformat}

\DeclareStringOption[4.5ex]{height}[4.5ex]
\DeclareStringOption[3.5ex]{topheight}[3.5ex]
\DeclareStringOption[1.5ex]{depth}[1.5ex]
\DeclareStringOption[1em]{labelsep}[1em]
\DeclareStringOption[1.6em]{indent}[1.6em]
\DeclareStringOption[1.5ex]{hsep}[1.5ex]
\DeclareStringOption[2.5em]{justsep}[2.5em]
\DeclareStringOption[.2mm]{linethickness}[.2mm]
\DeclareStringOption[1em]{cindent}[1em]
\DeclareBoolOption[true]{outerline}

% user command to redefine dimensions
\def\nddim#1#2#3#4#5#6#7#8{
  \setkeys{fitch}{
    height=#1,
    topheight=#2,
    depth=#3,
    labelsep=#4,
    indent=#5,
    hsep=#6,
    justsep=#7,
    linethickness=#8
  }
}

\DeclareLocalOptions{
  rules,
  arrayenv,
  justformat,
  refformat,
  height,
  topheight,
  depth,
  labelsep,
  indent,
  hsep,
  justsep,
  linethickness,
  cindent,
  outerline
}

\ProcessLocalKeyvalOptions{fitch}

% Actual fitch.sty code

\newlength{\nd@dim}

% References

\newcount\nd@ctr
\def\nd@render{\expandafter\ifx\expandafter\nd@x\nd@base\nd@x\the\nd@ctr\else\nd@base\ifnum\nd@ctr<0\the\nd@ctr\else\ifnum\nd@ctr>0+\the\nd@ctr\fi\fi\fi}
\expandafter\def\csname nd@-\endcsname{}

\def\nd@num#1{\nd@numo{\nd@render}{#1}\global\advance\nd@ctr1}
\def\nd@numopt#1#2{\nd@numo{$#1$}{#2}}
\def\nd@numo#1#2{\edef\x{#1}\mbox{$\x$}\expandafter\global\expandafter\let\csname nd@-#2\endcsname\x}
\def\nd@ref#1{\expandafter\let\expandafter\x\csname nd@-#1\endcsname\ifx\x\relax%
  \PackageWarning{fitch}{Undefined line reference: #1}\mbox{\textbf{??}}\else\csname\nd@refformat\endcsname{\mbox{$\x$}}\fi}
\def\nd@noop{}
\def\nd@set#1#2{\ifx\relax#1\nd@noop\else\global\def\nd@base{#1}\fi\ifx\relax#2\relax\else\global\nd@ctr=#2\fi}
\def\nd@reset{\nd@set{}{1}}
\def\nd@refa#1{\nd@ref{#1}}
\def\nd@aux#1#2{\ifx#2-\nd@refa{#1}--\def\nd@c{\nd@aux{}}%
  \else\ifx#2,\nd@refa{#1}, \def\nd@c{\nd@aux{}}%
  \else\ifx#2;\nd@refa{#1}; \def\nd@c{\nd@aux{}}%
  \else\ifx#2.\nd@refa{#1}. \def\nd@c{\nd@aux{}}%
  \else\ifx#2)\nd@refa{#1})\def\nd@c{\nd@aux{}}%
  \else\ifx#2(\nd@refa{#1}(\def\nd@c{\nd@aux{}}%
  \else\ifx#2\nd@end\nd@refa{#1}\def\nd@c{}%
  \else\def\nd@c{\nd@aux{#1#2}}%
  \fi\fi\fi\fi\fi\fi\fi\nd@c}
\def\ndref#1{\nd@aux{}#1\nd@end}

% Layer A

% set initial dimensions
%\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}

\def\nd@v{\rule[-\nd@depth]{\nd@linethickness}{\nd@height}}
\def\nd@h{\rule[-\nd@depth]{0mm}{\nd@height}} % strut
\def\nd@t{\rule[-\nd@depth]{\nd@linethickness}{\nd@topheight}}
\def\nd@i{\hspace{\nd@indent}} 
\def\nd@s{\hspace{\nd@hsep}}
\def\nd@g#1{\nd@f{\makebox[\nd@indent][c]{$#1$}}}
\def\nd@f#1{\raisebox{0pt}[0pt][0pt]{$#1$}}
\def\nd@u#1{\makebox[0pt][l]{\settowidth{\nd@dim}{\nd@f{#1}}%
  \addtolength{\nd@dim}{\nd@hsep}\addtolength{\nd@dim}{\nd@hsep}%
  \hspace{-\nd@hsep}\rule[-\nd@depth]{\nd@dim}{\nd@linethickness}}\nd@f{#1}}

% Lists

\def\nd@push#1#2{\expandafter\gdef\expandafter#1\expandafter%
  {\expandafter\nd@cons\expandafter{#1}{#2}}}
\def\nd@pop#1{{\def\nd@nil{\gdef#1{\nd@nil}}\def\nd@cons##1##2%
    {\gdef#1{##1}}#1}}
\def\nd@iter#1#2{{\def\nd@nil{}\def\nd@cons##1##2{##1#2{##2}}#1}}
\def\nd@modify#1#2#3{{\def\nd@nil{\gdef#1{\nd@nil}}\def\nd@cons##1##2%
    {\advance#2-1 ##1\advance#2 1 \ifnum#2=1\nd@push#1{#3}\else%
      \nd@push#1{##2}\fi}#1}}

\def\nd@cont#1{{\def\nd@t{\nd@v}\def\nd@v{\nd@v}\def\nd@g##1{\nd@i}%
    \def\nd@i{\nd@i}\def\nd@nil{\gdef#1{\nd@nil}}\def\nd@cons##1##2%
    {##1\expandafter\nd@push\expandafter#1\expandafter{##2}}#1}}

% Layer B

\newcount\nd@n
\def\nd@beginb{%
  \begingroup
  \nd@reset
  \gdef\nd@stack{\nd@nil}%
  \nd@push\nd@stack{\nd@h}%
  \ifnd@outerline
    \nd@push\nd@stack{\nd@t}\fi
  \begin{\nd@arrayenv}{l@{\hspace{\nd@labelsep}}l@{\hspace{\nd@justsep}}l}}
\def\nd@resumeb{%
  \begingroup
  \begin{\nd@arrayenv}{l@{\hspace{\nd@labelsep}}l@{\hspace{\nd@justsep}}l}}
\def\nd@endb{\end{\nd@arrayenv}\endgroup}
\def\nd@hypob#1#2{\nd@f{\nd@num{#1}}&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@u{#2}&}
\def\nd@haveb#1#2{\nd@f{\nd@num{#1}}&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@f{#2}&}
\def\nd@havecontb#1#2{&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@f{\hspace{\nd@cindent}#2}&}
\def\nd@hypocontb#1#2{&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@u{\hspace{\nd@cindent}#2}&}

\def\nd@openb{\nd@push\nd@stack{\nd@i}\nd@push\nd@stack{\nd@t}}
\def\nd@closeb{\nd@pop\nd@stack\nd@pop\nd@stack}
\def\nd@guardb#1#2{\nd@n=#1\multiply\nd@n by 2 \nd@modify\nd@stack\nd@n{\nd@g{#2}}}

% Layer C

\def\nd@clr{\gdef\nd@cmd{}\gdef\nd@typ{\relax}}
\def\nd@sto#1#2#3{\gdef\nd@typ{#1}\gdef\nd@byt{}%
  \gdef\nd@cmd{\nd@typ{#2}{#3}\nd@byt\\}}
\def\nd@chtyp{\expandafter\ifx\nd@typ\nd@hypocontb\def\nd@typ{\nd@havecontb}\else\def\nd@typ{\nd@haveb}\fi}
\def\nd@hypoc#1#2{\nd@chtyp\nd@cmd\nd@sto{\nd@hypob}{#1}{#2}}
\def\nd@havec#1#2{\nd@cmd\nd@sto{\nd@haveb}{#1}{#2}}
\def\nd@hypocontc#1{\nd@chtyp\nd@cmd\nd@sto{\nd@hypocontb}{}{#1}}
\def\nd@havecontc#1{\nd@cmd\nd@sto{\nd@havecontb}{}{#1}}
\def\nd@by#1#2{\ifx\nd@x#2\nd@x\gdef\nd@byt{\mbox{#1}}\else\ifx\nd@x#1\nd@x\gdef\nd@byt{\mbox{\ndref{#2}}}\else\gdef\nd@byt{\mbox{\csname\nd@justformat\endcsname{#1}{\ndref{#2}}}}\fi\fi\ignorespaces}

% multi-line macros
\def\nd@mhypoc#1#2{\nd@mhypocA{#1}#2\\\nd@stop\\}
\def\nd@mhypocA#1#2\\{\nd@hypoc{#1}{#2}\nd@mhypocB}
\def\nd@mhypocB#1\\{\ifx\nd@stop#1\else\nd@hypocontc{#1}\expandafter\nd@mhypocB\fi}
\def\nd@mhavec#1#2{\nd@mhavecA{#1}#2\\\nd@stop\\}
\def\nd@mhavecA#1#2\\{\nd@havec{#1}{#2}\nd@mhavecB}
\def\nd@mhavecB#1\\{\ifx\nd@stop#1\else\nd@havecontc{#1}\expandafter\nd@mhavecB\fi}
\def\nd@mhypocontc#1{\nd@mhypocB#1\\\nd@stop\\}
\def\nd@mhavecontc#1{\nd@mhavecB#1\\\nd@stop\\}

\def\nd@beginc{\nd@beginb\nd@clr}
\def\nd@resumec{\nd@resumeb\nd@clr}
\def\nd@endc{\nd@cmd\nd@endb}
\def\nd@openc{\nd@cmd\nd@clr\nd@openb}
\def\nd@closec{\nd@cmd\nd@clr\nd@closeb}
\let\nd@guardc\nd@guardb

% Layer D

% macros with optional arguments spelled-out
\def\nd@hypod[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd@guardb{1}{#4}\fi\nd@mhypoc{#3}{#5}\nd@set{#1}{#2}\ignorespaces}
\def\nd@haved[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd@guardb{1}{#4}\fi\nd@mhavec{#3}{#5}\nd@set{#1}{#2}\ignorespaces}
\def\nd@havecont#1{\nd@mhavecontc{#1}}
\def\nd@hypocont#1{\nd@mhypocontc{#1}}
\def\nd@base{undefined}
\def\nd@opend[#1]#2{\nd@cmd\nd@clr\nd@openb\nd@guard{#1}#2}
\def\nd@close{\nd@cmd\nd@clr\nd@closeb}
\def\nd@guardd[#1]#2{\nd@guardb{#1}{#2}}

% Handling of optional arguments.

\def\nd@optarg#1#2#3{\ifx[#3\def\nd@c{#2#3}\else\def\nd@c{#2[#1]{#3}}\fi\nd@c}
\def\nd@optargg#1#2#3{\ifx[#3\def\nd@c{#1#3}\else\def\nd@c{#2{#3}}\fi\nd@c}

\def\nd@five#1{\nd@optargg{\nd@four{#1}}{\nd@two{#1}}}
\def\nd@four#1[#2]{\nd@optarg{0}{\nd@three{#1}[#2]}}
\def\nd@three#1[#2][#3]#4{\nd@optarg{}{#1[#2][#3]{#4}}}
\def\nd@two#1{\nd@three{#1}[\relax][]}

\def\nd@have{\nd@five{\nd@haved}}
\def\nd@hypo{\nd@five{\nd@hypod}}
\def\nd@open{\nd@optarg{}{\nd@opend}}
\def\nd@guard{\nd@optarg{1}{\nd@guardd}}

\def\nd@init{%
  \let\open\nd@open%
  \let\close\nd@close%
  \let\hypo\nd@hypo%
  \let\have\nd@have%
  \let\hypocont\nd@hypocont%
  \let\havecont\nd@havecont%
  \let\by\nd@by%
  \let\guard\nd@guard%
  \csname\nd@rules\endcsname
}

% Define default rule names

\def\ndrules{%
  \def\ii{\by{$\Rightarrow$I}}%
  \def\ie{\by{$\Rightarrow$E}}%
  \def\Ai{\by{$\forall$I}}%
  \def\Ae{\by{$\forall$E}}%
  \def\Ei{\by{$\exists$I}}%
  \def\Ee{\by{$\exists$E}}%
  \def\ai{\by{$\wedge$I}}%
  \def\ae{\by{$\wedge$E}}%
  \def\ai{\by{$\wedge$I}}%
  \def\ae{\by{$\wedge$E}}%
  \def\oi{\by{$\vee$I}}%
  \def\oe{\by{$\vee$E}}%
  \def\ni{\by{$\neg$I}}%
  \def\ne{\by{$\neg$E}}%
  \def\be{\by{$\bot$E}}%
  \def\nne{\by{$\neg\neg$E}}%
  \def\r{\by{R}}}

% default justification format

\newcommand{\ndjustformat}[2]{#1, #2}

% default line number format

\newcommand{\ndrefformat}[1]{#1}

% User-level commands for proofs

\newenvironment{nd}[1][]
  {\begingroup
  \setkeys{fitch}{#1}%
  \nd@init\nd@beginc\ignorespaces}
  {\nd@endc\endgroup}
\newenvironment{ndresume}[1][]
  {\begingroup
  \setkeys{fitch}{#1}%
  \nd@init\nd@resumec\ignorespaces}
  {\nd@endc\endgroup}
\newenvironment{fitchproof}[1][]
  {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{nd}[#1]}
  {\end{nd}\end{list}}
\newenvironment{fitchproof*}[1][]
  {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{ndresume}[#1]}
  {\end{ndresume}\end{list}}

% End of file fitch.sty