latex-packages-build/wip/mkessler-refproof.sty

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Copyright © 2022 Maximilian Keßler
% 
% Permission is hereby granted, free of charge, to any person obtaining a copy
% of this software and associated documentation files (the “Software”), to deal
% in the Software without restriction, including without limitation the rights
% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
% copies of the Software, and to permit persons to whom the Software is
% furnished to do so, subject to the following conditions:
% The above copyright notice and this permission notice shall be included in all
% copies or substantial portions of the Software.
% 
% THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
% SOFTWARE.
% 
% This package has been generated by PyTeX, available at
%    https://github.com/kesslermaximilian/PyTeX
% and built from source file 'refproof.pysty3'.
% It is STRONGLY DISCOURAGED to edit this source file directly, since local
% changes will not be versioned by Git and overwritten by the next build. Always
% edit the source file and build the package again.
% 
% Build details:
%   PyTeX version: v1.2.0-26-g6048812 (commit 6048812)
%   Source code version: v2.5.2 (commit fbc4fd5)
% 
% This LaTeX package is free software and distributed under the MIT License. You
% may use it freely for your purposes. The latest version of the package can be
% obtained via GitHub under
%    https://github.com/kesslermaximilian/LatexPackages
% For further information see the url above.
% Reportings of bugs, suggestions and improvements are welcome, see the README
% at the Git repository for further information.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\ProvidesExplPackage{mkessler-refproof}{2022/01/15}{2.5.2}{Automatic references to theorems in proofs. Claim counters within proofs}



\ExplSyntaxOn

\RequirePackage{amssymb}
\RequirePackage{amsthm}
\RequirePackage{xparse}
\RequirePackage{refcount}
\RequirePackage{translator}
\RequirePackage{mkessler-subproof} % TODO: let PyTeX format the mkessler- prefix


%%%% Hook management

\cs_new:Npn\__mkessler_refproof_autoref:n
  {
    \ref
  }

\AddToHook{package/hyperref/after}
  {
    \cs_set:Npn\__mkessler_refproof_autoref:n
    {
      \autoref
    }
  }

%%% Saving old definitions

\cs_new_eq:NN \__mkessler_refproof_saved_proof:w        \proof
\cs_new_eq:NN \__mkessler_refproof_saved_endproof:      \endproof
\cs_new_eq:NN \__mkessler_refproof_saved_subproof:n     \rawsubproof
\cs_new_eq:NN \__mkessler_refproof_saved_endsubproof:   \rawendsubproof

%%% Internal variables

\int_new:N \__mkessler_refproof_proofdepth_int
\seq_new:N \__mkessler_refproof_nested_claim_counter_values_seq
\prop_new:N \__mkessler_refproof_refproof_claim_counters_prop

\cs_generate_variant:Nn \seq_push:Nn { N x }

%%% Language translations

\usedictionary{translator-proof-dictionary}

%%%Now, we internally got a proof and a subproof environment
%%%Make them available as 'old' variants, with their defautl behaviour
\NewDocumentEnvironment{oldproof}{ o }
{
  \IfValueTF { #1 }
    {
      \__mkessler_refproof_saved_proof:w { #1 }
    }
    {
      \__mkessler_refproof_saved_proof:w
    }
}
{
    \__mkessler_refproof_saved_endproof:
}

\NewDocumentEnvironment{oldsubproof}{ o }
{
  \IfValueTF { #1 }
    {
      \__mkessler_refproof_saved_subproof:n { #1 }
    }
    {
      \__mkessler_refproof_saved_subproof:n { \translate { Subproof } }
    }
}
{
  \__mkessler_refproof_saved_endsubproof:
}

%%% Main implementation

%Introduce claim environment
\newtheorem{claim}{\translate{Claim}}
\newtheorem*{claim*}{\translate{Claim}}
\AtBeginDocument{\def\claimautorefname{\translate{Claim}}}


\cs_new:Nn \__mkessler_refproof_enter_proof:
  {
    \int_gincr:N \__mkessler_refproof_proofdepth_int
    \seq_gpush:Nx \__mkessler_refproof_nested_claim_counter_values_seq
    {
      \arabic { claim }
    }
    \group_begin:
  }

\cs_new:Nn \__mkessler_refproof_leave_proof:
  {
    \group_end:
    \seq_gpop:NN \__mkessler_refproof_nested_claim_counter_values_seq \l_tmpa_tl
    \setcounter { claim } { \tl_use:N \l_tmpa_tl }
    \int_gdecr:N \__mkessler_refproof_proofdepth_int
  }


% Usage:
% #1 = \BooleanTrue or \BooleanFalse indicating presence of star
% #2 = star version of translation
% #3 = nonstar version of translation
\cs_new:Nn \__mkessler_refproof_set_proof_prefix:nnn
  {
    \IfBooleanTF { #1 }
      {
        \cs_set:Nn \__mkessler_refproof_proof_prefix:
          {
            \translate { #2 }
          }
      }
      {
        \cs_set:Nn \__mkessler_refproof_proof_prefix:
          {
            \translate { #3 }
          }
      }
  }

\cs_new:Nn \__mkessler_refproof_proof_comment:n 
{
  \IfValueT { #1 }
    {
      \c_space_tl ( #1 )
    }
}


\NewDocumentEnvironment{refproof}{s m !o}
  {
    \__mkessler_refproof_enter_proof:

    \prop_get:NnN
      \__mkessler_refproof_refproof_claim_counters_prop
      { #2 }
      \l_tmpa_tl

    \quark_if_no_value:NTF \l_tmpa_tl
      {
        \setcounter { claim } { 0 }
        \__mkessler_refproof_set_proof_prefix:nnn { #1 }
          { Proof* ~ of }
          { Proof  ~ of }
      }
      {
        \setcounter { claim } { \tl_use:N \l_tmpa_tl }
        \__mkessler_refproof_set_proof_prefix:nnn { #1 }
          { Continuation ~ of ~ proof* ~ of }
          { Continuation ~ of ~ proof  ~ of }
      }
    % Set up counter number printing as subindexed by numbering of the reference
    \renewcommand \theclaim
      {
        \getrefnumber { #2 } . \arabic { claim }
      }
    \__mkessler_refproof_saved_proof:w
      [
        \__mkessler_refproof_proof_prefix:
        \c_space_tl
        \__mkessler_refproof_autoref:n { #2 }
        \__mkessler_refproof_proof_comment:n { #3 }
      ]
  }
{
    \__mkessler_refproof_saved_endproof:
    \prop_gput:Nnx \__mkessler_refproof_refproof_claim_counters_prop
      { #2 }
      {
        \value{claim}
      }
      \__mkessler_refproof_leave_proof:
}

%%% A 'smart' proof environment
\AtBeginDocument{
    \RenewDocumentEnvironment{proof}{!s !o}
    {
        \__mkessler_refproof_enter_proof:

        \setcounter{claim}{0}

        \renewcommand \theclaim
          {
            \arabic { claim }
          }
        \int_compare:nNnTF \__mkessler_refproof_proofdepth_int > 1
        {
          \__mkessler_refproof_set_proof_prefix:nnn { #1 }
            { Subproof* }
            { Subproof  }
          \__mkessler_refproof_saved_subproof:n
            {
              \__mkessler_refproof_proof_prefix:
              \__mkessler_refproof_proof_comment:n { #2 }
            }
        }
        {
          \__mkessler_refproof_set_proof_prefix:nnn { #1 }
            { Proof* }
            { Proof  }
            \__mkessler_refproof_saved_proof:w
            [
              \__mkessler_refproof_proof_prefix:
              \__mkessler_refproof_proof_comment:n { #2 }
            ]
        }
    }
    {
        \__mkessler_refproof_saved_endproof:
        \__mkessler_refproof_leave_proof:
    }
}

\RenewDocumentEnvironment{subproof}{!s !o}
{
    \__mkessler_refproof_enter_proof:

    \setcounter { claim } { 0 }
    \renewcommand \theclaim
      {
        \arabic { claim }
      }

    \__mkessler_refproof_set_proof_prefix:nnn { #1 }
      { Subproof* }
      { Subproof  }
    \__mkessler_refproof_saved_subproof:n
      {
        \__mkessler_refproof_proof_prefix:
        \__mkessler_refproof_proof_comment:n { #2 }
      }
}
{
    \__mkessler_refproof_saved_endsubproof:
    \__mkessler_refproof_leave_proof:
}

\DeclareDocumentCommand { \proofdepth } { }
  {
    \int_to_arabic:n \__mkessler_refproof_proofdepth_int
  }