latex-packages/src/environments/refproof/refproof.pysty3

__HEADER__(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__PACKAGE_MACRO__(autoref:n)
  {
    \ref
  }

\AddToHook{package/hyperref/after}
  {
    \cs_set:Npn__PACKAGE_MACRO__(autoref:n)
    {
      \autoref
    }
  }

%%% Saving old definitions

\cs_new_eq:NN __PACKAGE_MACRO__(saved_proof:w)        \proof
\cs_new_eq:NN __PACKAGE_MACRO__(saved_endproof:)      \endproof
\cs_new_eq:NN __PACKAGE_MACRO__(saved_subproof:n)     \rawsubproof
\cs_new_eq:NN __PACKAGE_MACRO__(saved_endsubproof:)   \rawendsubproof

%%% Internal variables

\int_new:N __PACKAGE_MACRO__(proofdepth_int)
\seq_new:N __PACKAGE_MACRO__(nested_claim_counter_values_seq)
\prop_new:N __PACKAGE_MACRO__(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 }
    {
      __PACKAGE_MACRO__(saved_proof:w) { #1 }
    }
    {
      __PACKAGE_MACRO__(saved_proof:w)
    }
}
{
    __PACKAGE_MACRO__(saved_endproof:)
}

\NewDocumentEnvironment{oldsubproof}{ o }
{
  \IfValueTF { #1 }
    {
      __PACKAGE_MACRO__(saved_subproof:n) { #1 }
    }
    {
      __PACKAGE_MACRO__(saved_subproof:n) { \translate { Subproof } }
    }
}
{
  __PACKAGE_MACRO__(saved_endsubproof:)
}

%%% Main implementation

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


\cs_new:Nn __PACKAGE_MACRO__(enter_proof:)
  {
    \int_gincr:N __PACKAGE_MACRO__(proofdepth_int)
    \seq_gpush:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq)
    {
      \arabic { claim }
    }
    \group_begin:
  }

\cs_new:Nn __PACKAGE_MACRO__(leave_proof:)
  {
    \group_end:
    \seq_gpop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) \l_tmpa_tl
    \setcounter { claim } { \tl_use:N \l_tmpa_tl }
    \int_gdecr:N __PACKAGE_MACRO__(proofdepth_int)
  }


% Usage:
% #1 = \BooleanTrue or \BooleanFalse indicating presence of star
% #2 = star version of translation
% #3 = nonstar version of translation
\cs_new:Nn __PACKAGE_MACRO__(set_proof_prefix:nnn)
  {
    \IfBooleanTF { #1 }
      {
        \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
          {
            \translate { #2 }
          }
      }
      {
        \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
          {
            \translate { #3 }
          }
      }
  }

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


\NewDocumentEnvironment{refproof}{s m !o}
  {
    __PACKAGE_MACRO__(enter_proof:)

    \prop_get:NnN
      __PACKAGE_MACRO__(refproof_claim_counters_prop)
      { #2 }
      \l_tmpa_tl

    \quark_if_no_value:NTF \l_tmpa_tl
      {
        \setcounter { claim } { 0 }
        __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
          { Proof* ~ of }
          { Proof  ~ of }
      }
      {
        \setcounter { claim } { \tl_use:N \l_tmpa_tl }
        __PACKAGE_MACRO__(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 }
      }
    __PACKAGE_MACRO__(saved_proof:w)
      [
        __PACKAGE_MACRO__(proof_prefix:)
        \c_space_tl
        __PACKAGE_MACRO__(autoref:n) { #2 }
        __PACKAGE_MACRO__(proof_comment:n) { #3 }
      ]
  }
{
    __PACKAGE_MACRO__(saved_endproof:)
    \prop_gput:Nnx __PACKAGE_MACRO__(refproof_claim_counters_prop)
      { #2 }
      {
        \value{claim}
      }
      __PACKAGE_MACRO__(leave_proof:)
}

%%% A 'smart' proof environment
\AtBeginDocument{
    \RenewDocumentEnvironment{proof}{!s !o}
    {
        __PACKAGE_MACRO__(enter_proof:)

        \setcounter{claim}{0}

        \renewcommand \theclaim
          {
            \arabic { claim }
          }
        \int_compare:nNnTF __PACKAGE_MACRO__(proofdepth_int) > 1
        {
          __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
            { Subproof* }
            { Subproof  }
          __PACKAGE_MACRO__(saved_subproof:n)
            {
              __PACKAGE_MACRO__(proof_prefix:)
              __PACKAGE_MACRO__(proof_comment:n) { #2 }
            }
        }
        {
          __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
            { Proof* }
            { Proof  }
            __PACKAGE_MACRO__(saved_proof:w)
            [
              __PACKAGE_MACRO__(proof_prefix:)
              __PACKAGE_MACRO__(proof_comment:n) { #2 }
            ]
        }
    }
    {
        __PACKAGE_MACRO__(saved_endproof:)
        __PACKAGE_MACRO__(leave_proof:)
    }
}

\RenewDocumentEnvironment{subproof}{!s !o}
{
    __PACKAGE_MACRO__(enter_proof:)

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

    __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
      { Subproof* }
      { Subproof  }
    __PACKAGE_MACRO__(saved_subproof:n)
      {
        __PACKAGE_MACRO__(proof_prefix:)
        __PACKAGE_MACRO__(proof_comment:n) { #2 }
      }
}
{
    __PACKAGE_MACRO__(saved_endsubproof:)
    __PACKAGE_MACRO__(leave_proof:)
}

\DeclareDocumentCommand { \proofdepth } { }
  {
    \int_to_arabic:n __PACKAGE_MACRO__(proofdepth_int)
  }