%% logictools.sty
  %% Copyright 2025 Miles Min Yin Cheang
  %
  % 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
  %   http://www.latex-project.org/lppl.txt
  % and version 1.3 or later is part of all distributions of LaTeX
  % version 2005/12/01 or later.
  %
  % This work has the LPPL maintenance status “maintained”.
  % 
  % The Current Maintainer of this work is Miles Min Yin Cheang
  %
  % This work consists of the file logictools.sty



\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{logictools}[2025/05/20, v0.1.1. logictools]
\RequirePackage[only,llparenthesis,rrparenthesis]{stmaryrd}
\RequirePackage{amsmath}
\RequirePackage{xfrac}
\RequirePackage{bussproofs}
\RequirePackage{adjustbox}
\RequirePackage{trimspaces}
\DeclareOption{oxford}{\let\formal@oxford\@empty}
\DeclareOption*{\PackageWarning{logictools}{Unknown ‘\CurrentOption’}}
\ProcessOptions\relax



% Loaded when package option oxford used:
\@ifundefined{formal@oxford}{}{%
\RequirePackage{bussproofs}
% Provides semantic value function
% Gives automatic mathcal letters for the structure
% Optionally gives a variable assignment, where if a single Latin letter is input then it will return the associated Greek symbol.
\NewDocumentCommand{\semval}{m m o}
{%
\IfNoValueTF{#3}
    {\ensuremath{|#1|_{\mathcal{#2}}}}
    {\ensuremath{|#1|_{\mathcal{#2}}^{\latinletterstogreek{#3}}}}%
}%

% Provides "y differs from x in at most v" sign
\newcommand{\difmost}[1]{%
\overset{#1}{\sim}%
}

% Provides logical comma symbol

\newcommand{\lcma}{%
\adjustbox{trim={.45\width} 0pt 0pt 0pt ,clip}{$\circ$}%
}

% Provides an easy way to notate an unspecified proof from a set of premisses
% Optionally, can include discharged assumptions

\NewDocumentCommand{\prooffrom}{m t^ t_ o d<> m}
{%
\def\@prffrmalign{m}%
\IfBooleanT{#2}%
{%
\IfBooleanT{#3}{\PackageWarning{logictools}{You shouldn't use both ^ and _ in one prooffrom. You got lucky, if you had done this the other way around (_^) everything would break.}}%
\def\@prffrmalign{t}%
}%
\IfBooleanT{#3}{\def\@prffrmalign{b}}%
\IfNoValueTF{#4}%
    {\IfNoValueTF{#5}%
        {\alwaysNoLine%
        \AxiomC{\fbox{#1}}%
        \UnaryInfC{\raisebox{0.675ex}[3.25ex]{\smash{$\vdots$}}}%
        \UnaryInfC{#6}%
        \alwaysSingleLine}
        {\alwaysNoLine%
        \AxiomC{\adjustbox{fbox,valign=\@prffrmalign}{#1}\adjustbox{valign=\@prffrmalign, rlap}{\hspace{0.1em}\scriptsize#5}}%
        \UnaryInfC{\raisebox{0.675ex}[3.25ex]{\smash{$\vdots$}}}%
        \UnaryInfC{#6}%
        \alwaysSingleLine}%
    }%
    {\IfNoValueF{#5}{\PackageWarning{logictools}{You shouldn't use both [...] and <...> in one prooffrom. You got lucky, if you had done this the other way around (<...>[...]) you would have gotten strange results.}}%
    \alwaysNoLine%
    \AxiomC{\adjustbox{fbox,valign=\@prffrmalign}{#1}\adjustbox{valign=\@prffrmalign, rlap}{\hspace{0.1em}\scriptsize$\left[\text{#4}\right]$}}%
    \UnaryInfC{\raisebox{0.675ex}[3.25ex]{\smash{$\vdots$}}}%
    \UnaryInfC{#6}%
    \alwaysSingleLine}%
}%
}
%---------------------------------------------------------------------

% Thanks to everyone at TeX-exchange for teaching me how to use expl3!
\ExplSyntaxOn
\exp_args:Nc \mathchardef { __formal_original_): }=\char_value_mathcode:n {`)}
\exp_args:Nc \mathchardef { __formal_original_(: }=\char_value_mathcode:n {`(}
\exp_args:Nc \mathchardef { __formal_original_|: }=\char_value_mathcode:n {`|}
\exp_args:Nc \mathchardef { __formal_original_;: }=\char_value_mathcode:n {`;}
\exp_args:Nc \mathchardef { __formal_original_.: }=\char_value_mathcode:n {`.}
\exp_args:Nc \mathchardef { __formal_original_[: }=\char_value_mathcode:n {`[}

% Error messages:
\msg_new:nnnn { logictools } { quantnoglobaldeferror }{}{} % msg if global def for a quantifier went missing
\msg_new:nnnn { logictools } { quantneverdeferror }{}{} % msg if quant is never defined at all

\tl_new:N \l__formal_rparchar_tl % the right parenthesis used in formallogic
\tl_new:N \l__formal_lparchar_tl % the left parenthesis used in formallogic
\keys_define:nn {formal/options}
 {
  parstackkern        .muskip_set:N = \l__formal_parstackkern_muskip, 
  parinnerpad         .muskip_set:N = \l__formal_parinnerpad_muskip, 
  italiccorrection    .muskip_set:N = \l__formal_italiccorrection_muskip,
  parvoffset          .dim_set:N = \l__formal_parvoffset_dim,
  quantskip           .muskip_set:N = \l__formal_quantskip_muskip,
  lastquantskip       .muskip_set:N = \l__formal_lastquantskip_muskip,
  scriptspace         .dim_set:N = \l__formal_scriptspace_dim,

  parstackkern        .default:n = -0.9mu,
  parinnerpad         .default:n = 0.9mu,
  italiccorrection    .default:n = 1.12mu,
  parvoffset          .default:n = 0.2ex,
  quantskip           .default:n = 4.32mu,
  lastquantskip       .default:n = 4.32mu,
  scriptspace         .default:n = -0.025em,
  
  partype .choice:,
  
  partype / double .code:n = 
  \tl_set:Nn \l__formal_rparchar_tl {\rrparenthesis}
  \tl_set:Nn \l__formal_lparchar_tl {\llparenthesis},
  
  partype / single .code:n = 
  \tl_set:Nn \l__formal_rparchar_tl {\use:c{__formal_original_):}}
  \tl_set:Nn \l__formal_lparchar_tl {\use:c{__formal_original_(:}},
  partype / unknown .code:n =
    \msg_error:nneee { formal/options } { unknown_bracket_type }
        { partype } % Name of choice key
        { double , single } % Valid choices
        { \exp_not:n {#1} }, % Invalid choice given
        
  partype           .default:n = single,
 }
% Initialise all the keys
\keys_set:nn {formal/options}
     {
      parstackkern,
      parinnerpad,
      italiccorrection,
      parvoffset,
      quantskip,
      lastquantskip,
      partype,
      scriptspace,
     }


\bool_new:N \l__formal_rparpadreq_bool % this boolean will be true when we need padding on an rpar
\bool_set_true:N \l__formal_rparpadreq_bool
\bool_new:N \l__formal_escaped_bool % this boolean will be true if content is surrounded by ""
\bool_set_false:N \l__formal_escaped_bool

\box_new:N \l__formal_lpar_box % the box for parentheses
\box_new:N \l__formal_rpar_box

\cs_new_protected:Nn \__formal_llpar_char:
{
    \bool_if:NTF \l__formal_escaped_bool 
    {\use:c {__formal_original_(:}}
    {
        \box_use:N \l__formal_lpar_box \peek_charcode:NF ( {\mskip \l__formal_parinnerpad_muskip}
    }
}

\cs_new_protected:Nn \__formal_rrpar_char:
{
    \bool_if:NTF \l__formal_escaped_bool
    {\use:c {__formal_original_):}}
    {
        \bool_if:NTF \l__formal_rparpadreq_bool 
        {\mskip \l__formal_parinnerpad_muskip \mkern \l__formal_italiccorrection_muskip} 
        {}
        
        \box_use:N \l__formal_rpar_box
        \peek_charcode:NTF ) {\bool_set_false:N \l__formal_rparpadreq_bool} {\bool_set_true:N \l__formal_rparpadreq_bool}
    }
}

\cs_new_protected:Nn \__formal_escapetoggle:
{
    \bool_set_inverse:N \l__formal_escaped_bool
}



\cs_new_protected:Nn \__formal_quantstackenter:
{
    \bool_if:NTF \l__formal_escaped_bool 
        {\use:c {__formal_original_|:}}
        {
            \begingroup
            \char_set_active_eq:nN { `| } \__formal_quantstackesc:
            \char_set_active_eq:nN { `; } \__formal_quantdivider:
            \char_set_mathcode:nn { `; } { "8000 }
            \__formal_headquant:w
        }
}

\cs_new_protected:Npn \__formal_headquant:w #1,
{
    \tl_trim_spaces_apply:nN {#1} \__formal_headbox:n
}

\cs_new_protected:Npn \__formal_headbox:n #1
{
\box_if_exist:cTF {l__formal_#1head_box}
    {
        \box_if_empty:cTF {l__formal_#1head_box} 
            {
                \box_if_exist:cTF {g__formal_#1head_box}
                {\box_use:c{g__formal_#1head_box}}
                {
                    \msg_set:nnnn { logictools } { quantnoglobaldeferror }{Quantifier~’#1’~not~defined~\msg_line_context:.}{You~are~attempting~to~use~a~locally~declared~quantifier~outside~of~its~group.~Either~define~it~globally~with~DeclareQuantifier,~or~define~it~locally~here~too.\\ \msg_see_documentation_text:n {logictools}}
                    \msg_error:nn {logictools} {quantnoglobaldeferror}
                }
            } 
            {
                \box_use:c{l__formal_#1head_box}
            }
    }
    {
        \msg_set:nnnn { logictools } { quantneverdeferror }
        {Quantifier~’#1’~used~but~never~defined.}{You~must~declare~quantifiers~with~the~command(s)~(L)DeclareQuantifier~before~using~them.\\ \msg_see_documentation_text:n {logictools}}
        \msg_error:nn {logictools} {quantneverdeferror}
    }
}


\cs_new_protected:Npn \__formal_quantdivider:
{
    \bool_if:NTF \l__formal_escaped_bool 
        {\use:c {__formal_original_;:}}
        {\__formal_bodyquant:w}
}

\cs_new_protected:Npn \__formal_bodyquant:w #1,
{
    \mskip \use:c{l__formal_quantskip_muskip} \tl_trim_spaces_apply:nN {#1} \__formal_bodybox:n
}

\cs_new_protected:Npn \__formal_bodybox:n #1
{
\box_if_exist:cTF {l__formal_#1body_box}
    {
        \box_if_empty:cTF {l__formal_#1body_box} 
            {
                \box_if_exist:cTF {g__formal_#1body_box}
                {\box_use:c{g__formal_#1body_box}}
                {
                    \msg_set:nnnn { logictools } { quantnoglobaldeferror }{Quantifier~’#1’~not~defined~\msg_line_context:.}{You~are~attempting~to~use~a~locally~declared~quantifier~outside~of~its~group.~Either~define~it~globally~with~DeclareQuantifier,~or~define~it~locally~here~too.\\ \msg_see_documentation_text:n {logictools}}
                    \msg_error:nn {logictools} {quantnoglobaldeferror}
                }
            } 
            {
                \box_use:c{l__formal_#1body_box}
            }
    }
    {
        \msg_set:nnnn { logictools } { quantneverdeferror }
        {Quantifier~’#1’~used~but~never~defined.}{You~must~declare~quantifiers~with~the~command(s)~(L)DeclareQuantifier~before~using~them.\\ \msg_see_documentation_text:n {logictools}}
        \msg_error:nn {logictools} {quantneverdeferror}
    }
}

\cs_new_protected:Nn \__formal_quantstackesc:
{
    \endgroup \mskip \use:c{l__formal_lastquantskip_muskip}
}

\cs_new_protected:Nn \__formal_dot:
{
    \bool_if:NTF \l__formal_escaped_bool 
        {\use:c {__formal_original_.:}}
        {\peek_charcode_remove:NTF =
            {\doteq}
            {\use:c {__formal_original_.:}}}
}

\cs_new_protected:Nn \__formal_lbrack:
{
    \bool_if:NTF \l__formal_escaped_bool 
        {\use:c {__formal_original_[:}}
        {\__formal_varsub:w}
}

\cs_new_protected:Npn \__formal_varsub:w #1/#2]
{
    \left["\sfrac{"#1"}{"#2"}"\right]
}


\NewDocumentEnvironment{formallogic}{O{}}
{
    \setlength{\parindent}{0pt}
    \cs_set:Npn \par {$\newline$}
    \keys_set:nn {formal/options} % Load any settings given in the optional argument.
        {
            #1,
        }
    \setlength\scriptspace{\l__formal_scriptspace_dim}

    \hbox_set:Nn \l__formal_lpar_box 
        {
            \raisebox{\l__formal_parvoffset_dim}{$\l__formal_lparchar_tl \mkern \l__formal_parstackkern_muskip$}
        }

    \hbox_set:Nn \l__formal_rpar_box 
        {
            \raisebox{\l__formal_parvoffset_dim}{$\mkern \l__formal_parstackkern_muskip \l__formal_rparchar_tl$}
        }

    \char_set_active_eq:nN { `( } \__formal_llpar_char:
    \char_set_mathcode:nn { `( } { "8000 }
    \char_set_active_eq:nN { `) } \__formal_rrpar_char:
    \char_set_mathcode:nn { `) } { "8000 }
    \char_set_active_eq:nN { `" } \__formal_escapetoggle:
    \char_set_mathcode:nn { `" } { "8000 }
    \char_set_active_eq:nN { `| } \__formal_quantstackenter:
    \char_set_mathcode:nn { `| } { "8000 }
    \char_set_active_eq:nN { `. } \__formal_dot:
    \char_set_mathcode:nn { `. } { "8000 }
    \char_set_active_eq:nN { `[ } \__formal_lbrack:
    \char_set_mathcode:nn { `[ } { "8000 }
    
    \(
    \peek_charcode:NTF ) {\bool_set_false:N \l__formal_rparpadreq_bool} {\bool_set_true:N \l__formal_rparpadreq_bool}
}
{\)}

% make quants
\NewDocumentCommand{\DeclareQuantifier}{m m O{0mu} O{0mu}}
{
    \box_if_exist:cF {g__formal_#1head_box} 
        {
            \box_new:c {g__formal_#1head_box}
            \box_new:c {g__formal_#1body_box}
        }
    \box_if_exist:cF {l__formal_#1head_box} 
        {
            \box_new:c {l__formal_#1head_box}
            \box_new:c {l__formal_#1body_box}
        }
    \hbox_gset:cn {g__formal_#1head_box} 
        {
            $#2 \mkern#4$
        }
    \hbox_gset:cn {g__formal_#1body_box} 
        {
            $\mskip#3 #2 \mkern#4$
        }
}
\NewDocumentCommand{\LDeclareQuantifier}{m m O{0mu} O{0mu}}
{
    \box_if_exist:cF {l__formal_#1head_box} 
        {
            \box_new:c {l__formal_#1head_box}
            \box_new:c {l__formal_#1body_box}
        }
    \hbox_set:cn {l__formal_#1head_box} 
        {
            $#2 \mkern#4$
        }
    \hbox_set:cn {l__formal_#1body_box} 
        {
            $\mskip#3 #2 \mkern#4$
        }
}

% Use this command to declare settings that will stay for the rest of the document!
\NewDocumentCommand \logictoolsoptions { m }
{
\keys_set:nn {formal/options} 
    {
    #1 
    }
}

% Command that puts things inside the formallogic environment, can be used inline.
\NewDocumentCommand \fmllgc {o m}
{
\text{\begin{formallogic}[#1]#2
\end{formallogic}}
}


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

% A command for turning latin characters into greek ones
\NewDocumentCommand{\latinletterstogreek}{m}
{
    \str_case_e:nnF { #1 }
    {
        {a}{\alpha}
        {b}{\beta}
        {c}{\varsigma}
        {d}{\delta}
        {e}{\varepsilon}
        {f}{\varphi}
        {g}{\gamma}
        {h}{\eta}
        {i}{\iota}
        {j}{\vartheta}
        {k}{\kappa}
        {l}{\lambda}
        {m}{\mu}
        {n}{\nu}
        {o}{o}
        {p}{\pi}
        {q}{\chi}
        {r}{\rho}
        {s}{\sigma}
        {t}{\tau}
        {u}{\upsilon}
        {v}{\nu}
        {w}{\omega}
        {x}{\xi}
        {y}{\psi}
        {z}{\zeta}
        {A}{\mathrm{A}}
        {B}{\mathrm{B}}
        {C}{\Sigma}
        {D}{\Delta}
        {E}{\mathrm{E}}
        {F}{\Phi}
        {G}{\Gamma}
        {H}{\mathrm{H}}
        {I}{\mathrm{I}}
        {J}{\Theta}
        {K}{\mathrm{K}}
        {L}{\Lambda}
        {M}{\mathrm{M}}
        {N}{\mathrm{N}}
        {O}{\mathrm{O}}
        {P}{\Pi}
        {Q}{\mathrm{X}}
        {R}{\mathrm{P}}
        {S}{\Sigma}
        {T}{\mathrm{T}}
        {U}{\Upsilon}
        {V}{\mathrm{V}}
        {W}{\Omega}
        {X}{\Xi}
        {Y}{\Psi}
        {Z}{\mathrm{Z}}
    }
    {#1}
}

\ExplSyntaxOff


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

% Shorter equals sign
\newcommand{\@ltoolsshorteq}{%
  \settowidth{\@tempdima}{$x$}% Width of x in mathfont
  \resizebox{\@tempdima}{\height}{=}%
}

\ExplSyntaxOn
% Provides the symbols for l-one, l-two, l-equals and nice looking superscript
\NewDocumentCommand{\lsym}{m o}%
{
\IfNoValueTF{#2}
    {% No superscript:
        \str_case:nnF {#1}
        {
            {1}{\text{$\mathcal{L}\sb{1}$}}
            {2}{\text{$\mathcal{L}\sb{2}$}}
            {=}{\text{$\mathcal{L}\sb{\text{\hspace{0.01em}\@ltoolsshorteq}}$}}
        }
        {\text{$\mathcal{L}\sb{\text{#1}}$}}
    }
    {% Superscript:
        \str_case:nnF {#1}
        {
            {1}{\text{$\mathcal{L}\sb{1}^{\text{#2}}$}}
            {2}{\text{$\mathcal{L}\sb{2}^{\text{#2}}$}}
            {=}{\text{$\mathcal{L}\sb{\text{\hspace{0.01em}\@ltoolsshorteq}}^{\text{#2}}$}}
        }
        {\text{$\mathcal{L}\sb{\text{#1}}^{\text{#2}}$}}
    }
}

\ExplSyntaxOff

\DeclareQuantifier{exists}{\exists}
\DeclareQuantifier{forall}{\forall}

% Fix for amsmath messing with math-active codes.
\edef\originalbmathcode{%
    \noexpand\mathchardef\noexpand\@tempa\the\mathcode`\(\relax}
\def\resetMathstrut@{%
  \setbox\z@\hbox{%
    \originalbmathcode
    \def\@tempb##1"##2##3{\the\textfont"##3\char"}%
    \expandafter\@tempb\meaning\@tempa \relax
  }%
  \ht\Mathstrutbox@\ht\z@ \dp\Mathstrutbox@\dp\z@
}