% \iffalse meta-comment
%
% Copyright (C) 2008 by Ulrich M. Schwarz
%
% This file may be distributed and/or modified under the conditions of
% the LaTeX Project Public License, version 1.3a.
% The license can be obtained from
% http://www.latex-project.org/lppl/lppl-1-3a.txt
%
% \fi
%
%\iffalse (hide this from DocInput)
%<*restate>
%\fi
%
%\DescribeEnv{restatable}
%Only one environment is provided: \verb|restatable|, which takes one
%optional and two mandatory arguments. The first mandatory argument is the
%type of the theorem, i.e. if you want |\begin{lemma}| to be called on
%the inside, give |lemma|. The second argument is the name of the macro
%that the text should be stored in, for example \verb|mylemma|. Be careful
%not to specify existing command names! The optional argument will become the
%optional argument to your theorem command. Consider the following example:
%\begin{verbatim}
%  \documentclass{article}
%  \usepackage{amsmath, amsthm, thm-restate}
%  \newtheorem{lemma}{Lemma}
%  \begin{document}
%    \begin{restatable}[Zorn]{lemma}{zornlemma}\label{thm:zorn}
%      If every chain in $X$ is upper-bounded, 
%      $X$ has a maximal element.
%
%      It's true, you know!
%    \end{restatable}
%    \begin{lemma}
%      This is some other lemma of no import.
%    \end{lemma}
%    And now, here's Mr. Zorn again: \zornlemma*
%  \end{document}
%\end{verbatim}
%which yields
%    \begin{restatable}[Zorn]{lemma}{zornlemma}\label{thm:zorn}
%      If every chain in $X$ is upper-bounded, $X$ has a maximal element.
%
%      It's true, you know!
%    \end{restatable}
%    \begin{lemma}
%      This is some other lemma of no import.
%    \end{lemma}
%    Actually, we have set a label in the environment, so we know that
%    it's Lemma~\ref{thm:zorn} on page~\ref{thm:zorn}.
%    And now, here's Mr. Zorn again: \zornlemma*
%    Since we prevent the label from being set again, we find that
%    it's still Lemma~\ref{thm:zorn} on page~\ref{thm:zorn}, even though
%    it occurs later also. 
%
% \DescribeEnv{restatable*}
% As you can see, we use the starred form |\mylemma*|. As in many cases in
% \LaTeX, the star means ``don't give a number'', since we want to retain
% the original number. There is also a starred variant of the |restatable|
% environment, where the first call doesn't determine the number, but a
% later call to |\mylemma| without star would. Since the number is carried
% around using \LaTeX' |\label| machanism, you'll need a rerun for things to
% settle.
%
% \subsection{Restrictions}
% The only counter that is saved is the one for the theorem number. So,
% putting floats inside a restatable is not advised: they will appear in the
% LoF several times with new numbers. 
% Equations should work, but the code handling them might turn out to be
% brittle, in particular when you add/remove hyperref.
% %In the same vein, numbered equations
% %within the statement appear again and are numbered again, with new
% %numbers. (This is vaguely non-trivial to do correctly if equations are not
% %numbered consecutively, but per-chapter, or there are multiple numbered
% %equations.) 
% Note that you cannot successfully reference the equations
% since all labels are disabled in the starred appearance. (The reference
% will point at the unstarred occurence.)
%
% You cannot nest
% restatables either. You \emph{can} use the |\restatable|\dots|\endrestatable|
% version, but everything up to the next matching |\end{...}| is scooped up.
% I've also probably missed many border cases.
%
%
%\StopEventually{}
%    \begin{macrocode}
\RequirePackage{thmtools}
\let\@xa\expandafter
\let\@nx\noexpand
\@ifundefined{c@thmt@dummyctr}{%
  \newcounter{thmt@dummyctr}%
  }{}
\gdef\theHthmt@dummyctr{dummy.\arabic{thmt@dummyctr}}%
\gdef\thethmt@dummyctr{}%
\long\def\thmt@collect@body#1#2\end#3{%
  \@xa\thmt@toks\@xa{\the\thmt@toks #2}%
  \def\thmttmpa{#3}%\def\thmttmpb{restatable}%
  \ifx\thmttmpa\@currenvir%thmttmpb
    \@xa\@firstoftwo% this is the end of the environment.
  \else
    \@xa\@secondoftwo% go on collecting
  \fi{% this is the end, my friend, drop the \end.
  % and call #1 with the collected body.
    \@xa#1\@xa{\the\thmt@toks}%
  }{% go on collecting
    \@xa\thmt@toks\@xa{\the\thmt@toks\end{#3}}%
    \thmt@collect@body{#1}%
  }%
}
%    \end{macrocode}
% A totally ignorant version of |\ref|, defaulting to \#2 if label not
% known yet. Otherwise, return the formatted number.
%    \begin{macrocode}
\def\thmt@trivialref#1#2{%
  \ifcsname r@#1\endcsname
    \@xa\@xa\@xa\thmt@trivi@lr@f\csname r@#1\endcsname\relax\@nil
  \else #2\fi
}
\def\thmt@trivi@lr@f#1#2\@nil{#1}
%    \end{macrocode}
%
% Counter safeties: some counters' values should be stored, such as
% equation, so we don't get a new number. (We cannot reference it anyway.) 
% We cannot store everything, though, think page counter or section number!
% There is one problem here: we have to remove all references to other
% counters from |\theequation|, otherwise your equation could get a number
% like (3.1) in one place and (4.1) in another section.
%
% The best solution I can come up with is to override the usual macros
% that counter display goes through, to check if their argument is one
% that should be fully-expanded away or retained.
%
% The following should only be called from within a group, and the sanitized
% |\thectr| must not be called from within that group, since it needs the
% original |\@arabic| et al.
%
%    \begin{macrocode}
\def\thmt@innercounters{%
  equation}
\def\thmt@counterformatters{%
  @alph,@Alph,@arabic,@roman,@Roman,@fnsymbol}

\@for\thmt@displ:=\thmt@counterformatters\do{%
  \@xa\let\csname thmt@\thmt@displ\@xa\endcsname\csname \thmt@displ\endcsname
}%
\def\thmt@sanitizethe#1{%
  \@for\thmt@displ:=\thmt@counterformatters\do{%
    \@xa\protected@edef\csname\thmt@displ\endcsname##1{%
      \@nx\ifx\@xa\@nx\csname c@#1\endcsname ##1%
        \@xa\protect\csname \thmt@displ\endcsname{##1}%
      \@nx\else
        \@nx\csname thmt@\thmt@displ\endcsname{##1}%
      \@nx\fi
    }%
  }%
  \expandafter\protected@edef\csname the#1\endcsname{\csname the#1\endcsname}%
  \ifcsname theH#1\endcsname
    \expandafter\protected@edef\csname theH#1\endcsname{\csname theH#1\endcsname}%
  \fi
}

\def\thmt@rst@storecounters#1{%
  \bgroup
        % ugly hack: save chapter,..subsection numbers
        % for equation numbers.
  %\refstepcounter{thmt@dummyctr}% why is this here?
  %% temporarily disabled, broke autorefname.
  \def\@currentlabel{}%
  \@for\thmt@ctr:=\thmt@innercounters\do{%
    \thmt@sanitizethe{\thmt@ctr}%
    \protected@edef\@currentlabel{%
      \@currentlabel
      \protect\def\@xa\protect\csname the\thmt@ctr\endcsname{%
        \csname the\thmt@ctr\endcsname}%
      \ifcsname theH\thmt@ctr\endcsname
        \protect\def\@xa\protect\csname theH\thmt@ctr\endcsname{%
          (restate \protect\theHthmt@dummyctr)\csname theH\thmt@ctr\endcsname}%
      \fi
      \protect\setcounter{\thmt@ctr}{\number\csname c@\thmt@ctr\endcsname}%
    }%
  }%
  \label{thmt@@#1@data}%
  \egroup
}%
%    \end{macrocode}
%
% Now, the main business.
%
%    \begin{macrocode}
\newif\ifthmt@thisistheone
\newenvironment{thmt@restatable}[3][]{%
  \thmt@toks{}% will hold body
%
  \stepcounter{thmt@dummyctr}% used for data storage label.
%
  \long\def\thmrst@store##1{%
    \@xa\gdef\csname #3\endcsname{%
      \@ifstar{%
        \thmt@thisistheonefalse\csname thmt@stored@#3\endcsname
      }{%
        \thmt@thisistheonetrue\csname thmt@stored@#3\endcsname
      }%
    }%
    \@xa\long\@xa\gdef\csname thmt@stored@#3\@xa\endcsname\@xa{%
      \begingroup
      \ifthmt@thisistheone
        % these are the valid numbers, store them for the other
        % occasions.
        \thmt@rst@storecounters{#3}%
      \else
        % this one should use other numbers...
        % first, fake the theorem number.
        \@xa\protected@edef\csname the#2\endcsname{%
          \thmt@trivialref{thmt@@#3}{??}}%
        % if the number wasn't there, have a "re-run to get labels right"
        % warning.
        \ifcsname r@thmt@@#3\endcsname\else
          \G@refundefinedtrue
        \fi
        % prevent stepcountering the theorem number,
        % but still, have some number for hyperref, just in case.
        \@xa\let\csname c@#2\endcsname=\c@thmt@dummyctr
        \@xa\let\csname theH#2\endcsname=\theHthmt@dummyctr
        % disable labeling.
        \let\label=\@gobble
        \let\ltx@label=\@gobble% amsmath needs this
        % We shall need to restore the counters at the end
        % of the environment, so we get
        % (4.2) [(3.1 from restate)] (4.3)
        \def\thmt@restorecounters{}%
        \@for\thmt@ctr:=\thmt@innercounters\do{%
          \protected@edef\thmt@restorecounters{%
            \thmt@restorecounters
            \protect\setcounter{\thmt@ctr}{\arabic{\thmt@ctr}}%
          }%
        }%
        % pull the new semi-static definition of \theequation et al.
        % from the aux file.
        \thmt@trivialref{thmt@@#3@data}{}%
      \fi
      % call the proper begin-env code, possibly with optional argument      
      % (omit if stored via key-val)
      \ifthmt@restatethis
        \thmt@restatethisfalse
      \else
        \csname #2\@xa\endcsname\ifx\@nx#1\@nx\else[{#1}]\fi
      \fi
      \ifthmt@thisistheone
        % store a label so we can pick up the number later.
        \label{thmt@@#3}%
      \fi
      % this will be the collected body.
      ##1
      \csname end#2\endcsname
      % if we faked the counter values, restore originals now.
      \ifthmt@thisistheone\else\thmt@restorecounters\fi
      \endgroup
    }% thmt@stored@#3
    % in either case, now call the just-created macro,
    \csname #3\@xa\endcsname\ifthmt@thisistheone\else*\fi
    % and artificially close the current environment.
    \@xa\end\@xa{\@currenvir}
  }% thm@rst@store
  \thmt@collect@body\thmrst@store
}{%
  %% now empty, just used as a marker.
}

\newenvironment{restatable}{%
  \thmt@thisistheonetrue\thmt@restatable
}{%
  \endthmt@restatable
}
\newenvironment{restatable*}{%
  \thmt@thisistheonefalse\thmt@restatable
}{%
  \endthmt@restatable
}

%%% support for keyval-style: restate=foobar
\protected@edef\thmt@thmuse@families{%
 \thmt@thmuse@families%
 ,restate phase 1%
 ,restate phase 2%
}

\newif\ifthmt@restatethis
\define@key{restate phase 1}{restate}{%
  \thmt@debug{we will restate as #1}%
  \@namedef{thmt@unusedkey@restate}{}%
  % spurious "unused key" fixes itself once we are after tracknames...
  \thmt@restatethistrue
  \def\thmt@storedoptargs{}%
  \def\thmt@storename{#1}%
  \protected@edef\tmp@a{%
    \@nx\thmt@thisistheonetrue
    \@nx\@xa\@nx\thmt@restatable\@nx\@xa[\@nx\thmt@storedoptargs]%
      {\thmt@envname}{\thmt@storename}%
  }%
  \@xa\g@addto@macro\@xa\thmt@local@postheadhook\@xa{%
    \tmp@a
  }%
}
\thmt@mkignoringkeyhandler{restate phase 1}

\define@key{restate phase 2}{restate}{%
  % do not store restate as a key for repetition:
  % infinite loop.
}
\kv@set@family@handler{restate phase 2}{%
  \ifthmt@restatethis
  \@xa\@xa\@xa\g@addto@macro\@xa\@xa\@xa\thmt@storedoptargs\@xa\@xa\@xa{%
    \@xa\kv@key\@xa=\kv@value,}%
  \fi
}

%    \end{macrocode}
%\iffalse
%</restate>
%\fi