% \iffalse meta-comment 
% An Infrastructure for Structural Markup for Proofs
% Copyright (c) 2019 Michael Kohlhase, all rights reserved
%                this file is released under the
%                LaTeX Project Public License (LPPL)
% 
% The original of this file is in the public repository at 
% http://github.com/sLaTeX/sTeX/
%
% TODO update copyright  
%
%<*driver>
\def\libfolder#1{../../lib/#1}
\input{../../doc/stex-docheader}

\begin{document}
  \DocInput{\jobname.dtx}
\end{document}
%</driver>
% \fi
%
% \GetFileInfo{sproof.sty}
% 
% \title{\sTeX-Proofs: Structural Markup for Proofs\thanks{Version {\fileversion} (last revised {\filedate})}
% }
%
% \author{Michael Kohlhase, Dennis Müller\\
% 	FAU Erlangen-Nürnberg\\
% 	\url{http://kwarc.info/}
%c }
%
% \maketitle
%
%\ifinfulldoc\else
% \begin{abstract}
%   This is the documentation for the \pkg{stex-proofs} package.
%
% The |sproof| package is part of the {\stex} collection, a version of {\TeX/\LaTeX} that
% allows to markup {\TeX/\LaTeX} documents semantically without leaving the document
% format, essentially turning {\TeX/\LaTeX} into a document format for mathematical
% knowledge management (MKM).
%
% The \pkg{stex-proofs} package supplies macros and environment that allow to annotate the
% structure of mathematical proofs in {\stex} files. This structure can be used by MKM
% systems for added-value services, either directly from the \sTeX sources, or after
% translation.
%
% For a more high-level introduction, see \href{\basedocurl/manual.pdf}{the \sTeX Manual}
% or the \href{\basedocurl/stex.pdf}{full \sTeX documentation}.
% \end{abstract}
% 
% \tableofcontents
%
% \input{../../doc/packages/stex-proofs}
% \fi
%
% \begin{documentation}
% \changes{v0.9}{2022/02/14}{Moved over from the \pkg{sproofs} package}
% 
%
%
% \end{documentation}
%
% \begin{implementation}
%
% \section{The Implementation} 
% 
%    \begin{macrocode}
%<*package>
%<@@=stex_sproof>

%%%%%%%%%%%%%   sproof.dtx   %%%%%%%%%%%%%

%    \end{macrocode}
%
%
% \subsection{Proofs}\label{sec:impl:proofs}
% 
% We first define some keys for the |proof| environment.
%    \begin{macrocode}
\keys_define:nn { stex / spf } {
  id          .str_set_x:N  = \spfid,
  for         .clist_set:N  = \l_@@_spf_for_clist ,
  from        .tl_set:N     = \l_@@_spf_from_tl ,
  proofend    .tl_set:N     = \l_@@_spf_proofend_tl,
  type        .str_set_x:N  = \spftype,
  title       .tl_set:N     = \spftitle,
  continues   .tl_set:N     = \l_@@_spf_continues_tl,
  functions   .tl_set:N     = \l_@@_spf_functions_tl,
  term        .tl_set:N     = \l_@@_spf_term_tl,
  method      .tl_set:N     = \l_@@_spf_method_tl,
  hide        .bool_set:N   = \l_@@_spf_hide_bool  
}
\cs_new_protected:Nn \_@@_spf_args:n {
	\str_clear:N \spfid
	\tl_clear:N \l_@@_spf_for_tl
	\tl_clear:N \l_@@_spf_from_tl
	\tl_set:Nn \l_@@_spf_proofend_tl {\sproof@box}
	\str_clear:N \spftype
	\tl_clear:N \spftitle
	\tl_clear:N \l_@@_spf_continues_tl
	\tl_clear:N \l_@@_spf_term_tl
	\tl_clear:N \l_@@_spf_functions_tl
	\tl_clear:N \l_@@_spf_method_tl
  \bool_set_false:N \l_@@_spf_hide_bool
	\keys_set:nn { stex / spf }{ #1 }
}
\bool_set_true:N \l_@@_inc_counter_bool
%    \end{macrocode}
%
% \begin{macro}{\c_@@_flow_str}
% We define this macro, so that we can test whether the |display| key has the value |flow|
%    \begin{macrocode}
\str_set:Nn\c_@@_flow_str{inline}
%    \end{macrocode}
% \end{macro}
%
% For proofs, we will have to have deeply nested structures of enumerated list-like
% environments. However, {\LaTeX} only allows |enumerate| environments up to nesting depth
% 4 and general list environments up to listing depth 6. This is not enough for us.
% Therefore we have decided to go along the route proposed by Leslie Lamport to use a
% single top-level list with dotted sequences of numbers to identify the position in the
% proof tree. Unfortunately, we could not use his |pf.sty| package directly, since it does
% not do automatic numbering, and we have to add keyword arguments all over the place, to
% accomodate semantic information.
%
%    \begin{macrocode}
\intarray_new:Nn\l_@@_counter_intarray{50}
\cs_new_protected:Npn \sproofnumber {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int .
    \int_incr:N \l_tmpa_int
  }
}
\cs_new_protected:Npn \_@@_inc_counter: {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \int_incr:N \l_tmpa_int
  }
  \int_compare:nNnF \l_tmpa_int = 1 {
    \int_decr:N \l_tmpa_int
  }
  \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int {
    \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int + 1
  }
}

\cs_new_protected:Npn \_@@_add_counter: {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \int_incr:N \l_tmpa_int
  }
  \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int { 1 }
}

\cs_new_protected:Npn \_@@_remove_counter: {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \int_incr:N \l_tmpa_int
  }
  \int_decr:N \l_tmpa_int
  \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int { 0 }
}
%    \end{macrocode}
%
%\begin{macro}{\sproofend}
%    This macro places a little box at the end of the line if there is space, or at the
%    end of the next line if there isn't
%    \begin{macrocode}
\def\sproof@box{
  \hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}
}
\def\sproofend{
  \tl_if_empty:NF \l_@@_spf_proofend_tl {
    \hfil\null\nobreak\hfill\l_@@_spf_proofend_tl\par\smallskip
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{spf@*@kw}
%    \begin{macrocode}
\def\spf@proofsketch@kw{Proof~Sketch}
\def\spf@proof@kw{Proof}
\def\spf@step@kw{Step}
%    \end{macrocode}
% \end{macro}
%
% For the other languages, we set up triggers
%    \begin{macrocode}
\AddToHook{begindocument}{
  \ltx@ifpackageloaded{babel}{
    \makeatletter
    \clist_set:Nx \l_tmpa_clist {\bbl@loaded}
    \clist_if_in:NnT \l_tmpa_clist {ngerman}{
      \input{sproof-ngerman.ldf}
    }
    \clist_if_in:NnT \l_tmpa_clist {finnish}{
      \input{sproof-finnish.ldf}
    }
    \clist_if_in:NnT \l_tmpa_clist {french}{
      \input{sproof-french.ldf}
    }
    \clist_if_in:NnT \l_tmpa_clist {russian}{
      \input{sproof-russian.ldf}
    }
    \makeatother
  }{}
}
%    \end{macrocode}
%
% \begin{macro}{spfsketch}
%    \begin{macrocode}
\newcommand\spfsketch[2][]{
  \begingroup
  \let \premise \stex_proof_premise:
  \_@@_spf_args:n{#1}
  \stex_if_smsmode:TF {
    \str_if_empty:NF \spfid {
      \stex_ref_new_doc_target:n \spfid
    }
  }{
    \seq_clear:N \l_tmpa_seq
    \clist_map_inline:Nn \l_@@_spf_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \exp_args:Nnx
    \stex_annotate:nnn{proofsketch}{\seq_use:Nn \l_tmpa_seq {,}}{
      \str_if_empty:NF \spftype {
        \stex_annotate_invisible:nnn{type}{\spftype}{}
      }
      \clist_set:No \l_tmpa_clist \spftype
      \tl_set:Nn \l_tmpa_tl {
        \titleemph{
          \tl_if_empty:NTF \spftitle {
            \spf@proofsketch@kw
          }{
            \spftitle
          }
        }:~
      }
      \clist_map_inline:Nn \l_tmpa_clist {
        \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
          \tl_clear:N \l_tmpa_tl
        }
      }
      \str_if_empty:NF \spfid {
        \stex_ref_new_doc_target:n \spfid
      }
      \l_tmpa_tl #2 \sproofend
    }
  }
  \endgroup
  \stex_smsmode_do:
}

%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\_@@_maybe_comment:,\_@@_maybe_comment_end:,\_@@_start_comment:}
%    \begin{macrocode}
\bool_set_false:N \l_@@_in_spfblock_bool

\cs_new_protected:Nn \_@@_maybe_comment: {
  \bool_if:NF \l_@@_in_spfblock_bool {
    \par \setbox \l_tmpa_box \vbox \bgroup \everypar{\_@@_start_comment:}
  }
}
\cs_new_protected:Nn \_@@_maybe_comment_end: {
  \bool_if:NF \l_@@_in_spfblock_bool { \egroup }
}
\cs_new_protected:Nn \_@@_start_comment: {
  \csname @ @ par\endcsname\egroup\item[]\bgroup\stexcommentfont
}

%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stexcommentfont}
%    \begin{macrocode}
\cs_new_protected:Npn \stexcommentfont {
  \small\itshape
}
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{sproof}
%    In this environment, we initialize the proof depth counter |\count10| to 10, and set
%    up the description environment that will take the proof steps. At the end of the
%    proof, we position the proof end into the last line.
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_start_env:nnn {
  \seq_clear:N \l_tmpa_seq
  \clist_map_inline:Nn \l_@@_spf_for_clist {
    \tl_if_empty:nF{ ##1 }{
      \stex_get_symbol:n { ##1 }
      \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
        \l_stex_get_symbol_uri_str
      }
    }
  }
  \exp_args:Nnnx
  \begin{stex_annotate_env}{#1}{\seq_use:Nn \l_tmpa_seq {,}}
  \str_if_empty:NF \spftype {
    \stex_annotate_invisible:nnn{type}{\spftype}{}
  }
  #3 {~\stex_annotate:nnn{spftitle}{}{#2}}
  \str_if_empty:NF \spfid {
    \stex_ref_new_doc_target:n \spfid
  }
  \begin{stex_annotate_env}{spfbody}{\bool_if:NTF \l_@@_spf_hide_bool {false}{true}}
  \bool_if:NT \l_@@_spf_hide_bool{
    \stex_html_backend:F{\setbox\l_tmpa_box\vbox\bgroup}
  }
  \begin{list}{}{
    \setlength\topsep{0pt}
    \setlength\parsep{0pt}
    \setlength\rightmargin{0pt}
    
  }\_@@_maybe_comment:
}
\cs_new_protected:Nn \_@@_end_env:n {
  \stex_if_smsmode:F{
    \_@@_maybe_comment_end:
    \end{list}  
    \bool_if:NT \l_@@_spf_hide_bool{
      \stex_html_backend:F{\egroup}
    }
    \clist_set:No \l_tmpa_clist \spftype
    #1
    \end{stex_annotate_env}
    \end{stex_annotate_env}
  }
}
\NewDocumentEnvironment{sproof}{s O{} m}{
  \intarray_gzero:N \l_@@_counter_intarray
  \intarray_gset:Nnn \l_@@_counter_intarray 1 1
  \stex_reactivate_macro:N \yield
  \stex_reactivate_macro:N \eqstep
  \stex_reactivate_macro:N \assumption
  \stex_reactivate_macro:N \conclude
  \stex_reactivate_macro:N \spfstep
  \_@@_spf_args:n{#2}
  \stex_if_smsmode:TF {
    \str_if_empty:NF \spfid {
      \stex_ref_new_doc_target:n \spfid
    }
  }{
    \_@@_start_env:nnn{sproof}{#3}{
      \clist_set:No \l_tmpa_clist \spftype
      \tl_clear:N \l_tmpa_tl
      \clist_map_inline:Nn \l_tmpa_clist {
        \tl_if_exist:cT {_@@_sproof_##1_start:}{
          \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sproof_##1_start:}}
        }
        \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
          \tl_set:Nn \l_tmpa_tl {\use:n{}}
        }
      }
      \tl_if_empty:NTF \l_tmpa_tl {
        \_@@_sproof_start:
      }{
        \l_tmpa_tl
      }
    }
  }
  \stex_smsmode_do:
}{\_@@_end_env:n{
  \tl_clear:N \l_tmpa_tl
  \clist_map_inline:Nn \l_tmpa_clist {
    \tl_if_exist:cT {_@@_sproof_##1_end:}{
      \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sproof_##1_end:}}
    }
  }
  \tl_if_empty:NTF \l_tmpa_tl {
    \_@@_sproof_end:
  }{
    \l_tmpa_tl
  }
}}
\NewDocumentEnvironment{subproof}{s O{} m}{
  \_@@_spf_args:n{#2}
  \stex_if_smsmode:TF {
    \str_if_empty:NF \spfid {
      \stex_ref_new_doc_target:n \spfid
    }
  }{
    \_@@_start_env:nnn{subproof}{\item[\sproofnumber]\ignorespacesandpars #3}{}
  }
  \_@@_add_counter:
  \stex_smsmode_do:
}{\_@@_remove_counter:\_@@_end_env:n{}  
  \bool_if:NT \l_@@_inc_counter_bool {
    \_@@_inc_counter:
  }
  \aftergroup\_@@_maybe_comment:
}
\AddToHook{env/subproof/before}{\_@@_maybe_comment_end:}

\cs_new_protected:Nn \_@@_sproof_start: {
  \par\noindent\titleemph{
    \tl_if_empty:NTF \spftype {
      \spf@proof@kw
    }{
      \spftype
    }
  }:
}
\cs_new_protected:Nn \_@@_sproof_end: {\sproofend}

\newcommand\stexpatchproof[3][] {
  \str_set:Nx \l_tmpa_str{ #1 }
  \str_if_empty:NTF \l_tmpa_str {
    \tl_set:Nn \_@@_sproof_start: { #2 }
    \tl_set:Nn \_@@_sproof_end: { #3 }
  }{
    \exp_after:wN \tl_set:Nn \csname _@@_sproof_#1_start:\endcsname{ #2 }
    \exp_after:wN \tl_set:Nn \csname _@@_sproof_#1_end:\endcsname{ #3 }
  }
}
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\pstep,\conclude,\assumption,\have,\eqstep}
%    \begin{macrocode}

\keys_define:nn { stex / spfsteps } {
  id          .str_set_x:N  = \spfstepid,
  for         .clist_set:N  = \l_@@_spf_for_clist ,
  type        .str_set_x:N  = \spftype,
  title       .tl_set:N     = \spftitle,
  method      .tl_set:N     = \l_@@_spf_method_tl,
  term        .tl_set:N     = \l_@@_spf_term_tl
}
\cs_new_protected:Nn \_@@_spfstep_args:n {
	\str_clear:N \spfstepid
	\clist_clear:N \l_@@_spf_for_clist
	\str_clear:N \spftype
	\tl_clear:N \l_@@_spf_method_tl
	\tl_clear:N \l_@@_spf_term_tl
  %\bool_set_false:N \l_@@_inc_counter_bool
	\keys_set:nn { stex / spfsteps }{ #1 }
}

\cs_new_protected:Nn \_@@_make_step_macro:Nnnnn {
  \NewDocumentCommand #1 {s O{} +m} {
    \_@@_maybe_comment_end:

    \_@@_spfstep_args:n{##2}
    \stex_annotate:nnn{spfstep}{#2}{ 
      \tl_if_empty:NF \l_@@_spf_term_tl {
        \stex_annotate_invisible:nnn{spfyield}{}{$\l_@@_spf_term_tl$}
      }
      \bool_if:NTF \l_@@_in_spfblock_bool {
        #4
      }{
        \item[\IfBooleanTF ##1 {}{#3}]
      }
      \ignorespacesandpars ##3
    }
    \bool_if:NF \l_@@_in_spfblock_bool { \IfBooleanTF ##1 {}{ #5 } }
    \_@@_maybe_comment:
  }
  \stex_deactivate_macro:Nn #1 {sproof~environments}
}

\_@@_make_step_macro:Nnnnn \assumption {assumption} \sproofnumber {} \_@@_inc_counter:
\_@@_make_step_macro:Nnnnn \conclude {conclusion} {$\Rightarrow$} {} {}
\_@@_make_step_macro:Nnnnn \spfstep {} \sproofnumber {} \_@@_inc_counter:

\NewDocumentCommand \eqstep {s m}{
  \_@@_maybe_comment_end:
  \bool_if:NTF \l_@@_in_spfblock_bool {
    $=$
  }{
    \item[$=$]
  }
  $\stex_annotate:nnn{spfstep}{eq}{ #2 }$
  \_@@_maybe_comment:
}
\stex_deactivate_macro:Nn \eqstep {sproof~environments}

\NewDocumentCommand \yield {+m}{
  \stex_annotate:nnn{spfyield}{}{ #1 }
}
\stex_deactivate_macro:Nn \yield {sproof~environments}

\NewDocumentEnvironment{spfblock}{}{
  \item[]
  \bool_set_true:N \l_@@_in_spfblock_bool
}{
  \aftergroup\_@@_maybe_comment:
}
\AddToHook{env/spfblock/before}{\_@@_maybe_comment_end:}

%    \end{macrocode}
% \end{macro}
%
% 
% \begin{macro}{\spfidea}
%    \begin{macrocode}
\NewDocumentCommand\spfidea{O{} +m}{
  \_@@_spf_args:n{#1}
  \titleemph{
    \tl_if_empty:NTF \spftype {Proof~Idea}{
      \spftype
    }:
  }~#2
  \sproofend
}
%    \end{macrocode}
% \end{macro}
%
%    \begin{macrocode}
\newcommand\spfjust[1]{
  #1
}
%</package>
%    \end{macrocode}
% \end{implementation}
% \Finale
% \ifinfulldoc\else\printbibliography\fi
\endinput

%%% Local Variables: 
%%% mode: doctex
%%% TeX-master: t
%%% End: 
