%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Copyright © 2022 Maximilian Keßler
% 
% This work may be distributed and/or modified
% 
% 1. under the LaTeX Project Public License and/or
% 2. under the GNU General Public License
% 
% Distribution under conditions of the LaTeX Project Public License,
% requires 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 Maximilian Keßler.
% 
% 
% Distribution under the GNU General Public License requires either
% version 3 or (at your opinion) any later version.
% 
% 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-31-gc9bb0e8 (commit c9bb0e8)
%   Source code version: v2.9-16-gd96c0bd (commit d96c0bd)
% 
% This LaTeX package is free software and is dual-licensed
% under the LPPLv1.3c and the GPLv3 licenses.
% You may use it freely for your purposes.
% The latest version of the package sources can be obtained
% via GitLab under
%    https://gitlab.com/latexci/packages/LatexPackages
% The latest version of the built packages can be obtained via GitLab under
%    https://gitlab.com/latexci/packages/LatexPackagesBuild
% For further information see the urls above.
% Reportings of bugs, suggestions and improvements are welcome, see the README
% at the Git repository for further information.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\ProvidesExplPackage{mkessler-refproof}{2022/06/27}{2.9-16-gd96c0bd}{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} { }
  {
        \__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
  }