% \iffalse meta-comment
% An Infrastructure for Semantic Macros and Module Scoping
% 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
%
% \title{ \sTeX-Symbols
% 	\thanks{Version {\fileversion} (last revised {\filedate})} 
% }
%
% \author{Michael Kohlhase, Dennis Müller\\
% 	FAU Erlangen-Nürnberg\\
% 	\url{http://kwarc.info/}
% }
%
% \maketitle
%
%\ifinfulldoc\else
% This is the documentation for the \pkg{stex-symbols} package.
% For a more high-level introduction, 
%  see \href{\basedocurl/manual.pdf}{the \sTeX Manual} or the
%  \href{\basedocurl/stex.pdf}{full \sTeX documentation}.
%
%  \tableofcontents
%
% \input{../../doc/packages/stex-symbols}
% \fi
%
% \begin{documentation}\label{pkg:symbols:doc}
% \changes{3.1.0}{2022/03/03}{Introduced sequence variables}
% \changes{3.1.0}{2022/03/01}{Fixed bug with precedences in variables}
% \changes{3.1.0}{2022/03/01}{Introduced \detokenize{\varemph, \varemph@uri}}
%
% Code related to symbol declarations and notations
%
% \section{Macros and Environments}\label{pkg:symbols:doc:macros}
%
% \begin{function}{\symdecl}
%   \begin{syntax} \cs{symdecl}\Arg{macroname}|[|\meta{args}|]| \end{syntax}
%   Declares a new symbol with semantic macro \cs{macroname}. Optional
%   arguments are:
%   \begin{itemize}
%     \item |name|: An (\omdoc) name. By default equal to \meta{macroname}.
%     \item |type|: An (ideally semantic) term, representing a \emph{type}. Not used by \sTeX, but
%         passed on to \mmt for semantic services.
%     \item |def|: An (ideally semantic) term, representing a \emph{definiens}. Not used by \sTeX, but
%         passed on to \mmt for semantic services.
%     \item |args|: Specifies the ``signature'' of the semantic macro.
%       Can be either an integer $0 \leq n \leq 9$, or a (more precise)
%       sequence of the following characters:
%         \begin{itemize}
%           \item[|i|] a ``normal'' argument, e.g.
%             |\symdecl{plus}[args=ii]| allows for |\plus{2}{2}|.
%           \item[|a|] an \emph{associative} argument; i.e. a sequence of
%             arbitrarily many arguments provided as a comma-separated list,
%             e.g.
%             |\symdecl{plus}[args=a]| allows for |\plus{2,2,2}|.
%           \item[|b|] a \emph{variable} argument. Is treated by \sTeX
%             like an |i|-argument, but an application is turned into
%             an |OMBind| in \omdoc, binding the provided variable
%             in the subsequent arguments of the operator; e.g.
%             |\symdecl{forall}[args=bi]| allows for |\forall{x\in\Nat}{x\geq0}|.
%         \end{itemize}
%   \end{itemize}
% \end{function}
%
% \begin{function}{\stex_symdecl_do:n}
%   Implements the core functionality of \cs{symdecl}, and is
%   called by \cs{symdecl} and \cs{symdef}.
%
%   Ultimately stores the symbol \meta{URI} in the property
%   list |\l_stex_symdecl_|\meta{URI}|_prop| with fields:
%   \begin{itemize}
%     \item |name| (string),
%     \item |module| (string),
%     \item |notations| (sequence of strings; initially empty),
%     \item |type| (token list),
%     \item |args| (string of |i|s, |a|s and |b|s),
%     \item |arity| (integer string),
%     \item |assocs| (integer string; number of associative arguments),
%   \end{itemize}
% \end{function}
%
% \begin{function}{\stex_all_symbols:n}
%   Iterates over all currently available symbols.
%   Requires two |\seq_map_break:| to break fully.
% \end{function}
%
% \begin{function}{\stex_get_symbol:n}
%   Computes the full URI of a symbol from a macro argument, e.g.
%   the macro name, the macro itself, the full URI...
% \end{function}
%
% \begin{function}{\notation}
%   \begin{syntax} \cs{notation}|[|\meta{args}|]|\Arg{symbol}\Arg{notations$^+$} \end{syntax}
%   Introduces a new notation for \meta{symbol}, see \cs{stex_notation_do:nn}
% \end{function}
%
% \begin{function}{\stex_notation_do:nn}
%   \begin{syntax} \cs{stex_notation_do:nn}\Arg{URI}\Arg{notations$^+$}\end{syntax}
%
%   Implements the core functionality of \cs{notation}, and is
%   called by \cs{notation} and \cs{symdef}.
%
%   Ultimately stores the notation in the property
%   list\\ |\g_stex_notation_|\meta{URI}|#|\meta{variant}|#|^^A
%   \meta{lang}|_prop| with fields:
%   \begin{itemize}
%     \item |symbol| (URI string),
%     \item |language| (string),
%     \item |variant| (string),
%     \item |opprec| (integer string),
%     \item |argprecs| (sequence of integer strings)
%   \end{itemize}
% \end{function}
%
% \begin{function}{\symdef}
%   \begin{syntax} \cs{symdef}|[|\meta{args}|]|\Arg{symbol}\Arg{notations$^+$} \end{syntax}
%   Combines \cs{symdecl} and \cs{notation} by introducing a new
%   symbol and assigning a new notation for it.
% \end{function}
%
% \end{documentation}
%
% \begin{implementation}\label{pkg:symbols:impl}
%
% \section{\sTeX-Symbols Implementation}
%
%    \begin{macrocode}
%<*package>

%%%%%%%%%%%%%   symbols.dtx   %%%%%%%%%%%%%

%    \end{macrocode}
%
% Warnings and error messages
%
%    \begin{macrocode}
\msg_new:nnn{stex}{error/wrongargs}{
  args~value~in~symbol~declaration~for~#1~
  needs~to~be~i,~a,~b~or~B,~but~#2~given
}
\msg_new:nnn{stex}{error/unknownsymbol}{
  No~symbol~#1~found!
}
\msg_new:nnn{stex}{error/seqlength}{
  Expected~#1~arguments;~got~#2!
}
\msg_new:nnn{stex}{error/unknownnotation}{
  Unknown~notation~#1~for~#2!
}
%    \end{macrocode}
%
% \subsection{Symbol Declarations}
%    \begin{macrocode}
%<@@=stex_symdecl>
%    \end{macrocode}
%
% \begin{macro}{\stex_all_symbols:n}
%   Map over all available symbols
%    \begin{macrocode}
\cs_new_protected:Nn \stex_all_symbols:n {
  \def \_@@_all_symbols_cs ##1 {#1}
  \seq_map_inline:Nn \l_stex_all_modules_seq {
    \seq_map_inline:cn{c_stex_module_##1_constants}{
      \_@@_all_symbols_cs{##1?####1}
    }
  } 
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\STEXsymbol}
%    \begin{macrocode}
\NewDocumentCommand \STEXsymbol { m } {
  \stex_get_symbol:n { #1 }
  \exp_args:No
  \stex_invoke_symbol:n { \l_stex_get_symbol_uri_str }
}
%    \end{macrocode}
% \end{macro}
%
% |symdecl| arguments:
%
%    \begin{macrocode}
\keys_define:nn { stex / symdecl } {
  name        .str_set_x:N  = \l_stex_symdecl_name_str ,
  args        .str_set_x:N  = \l_stex_symdecl_args_str ,
  type        .tl_set:N     = \l_stex_symdecl_type_tl ,
  deprecate   .str_set_x:N  = \l_stex_symdecl_deprecate_str ,
  align       .str_set:N    = \l_stex_symdecl_align_str , % TODO(?)
  gfc         .str_set:N    = \l_stex_symdecl_gfc_str , % TODO(?)
  def         .tl_set:N     = \l_stex_symdecl_definiens_tl ,
  reorder     .str_set_x:N  = \l_stex_symdecl_reorder_str ,
  argnames    .clist_set:N  = \l_stex_symdecl_argnames_clist ,
  assoc       .choices:nn   = 
      {bin,binl,binr,pre,conj,pwconj}
      {\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}}
}

\bool_new:N \l_stex_symdecl_make_macro_bool

\cs_new_protected:Nn \_@@_args:n {
  \str_clear:N \l_stex_symdecl_name_str
  \str_clear:N \l_stex_symdecl_args_str
  \str_clear:N \l_stex_symdecl_deprecate_str
  \str_clear:N \l_stex_symdecl_reorder_str
  \str_clear:N \l_stex_symdecl_assoctype_str
  \bool_set_false:N \l_stex_symdecl_local_bool
  \tl_clear:N \l_stex_symdecl_type_tl
  \tl_clear:N \l_stex_symdecl_definiens_tl
  \clist_clear:N \l_stex_symdecl_argnames_clist
  
  \keys_set:nn { stex / symdecl } { #1 }
}
%    \end{macrocode}
%
% \begin{macro}{\symdecl}
%
% Parses the optional arguments and passes them on to
% \cs{stex_symdecl_do:} (so that \cs{symdef}
% can do the same)
%
%    \begin{macrocode}

\NewDocumentCommand \symdecl { s m O{}} {
  \_@@_args:n { #3 }
  \IfBooleanTF #1 {
    \bool_set_false:N \l_stex_symdecl_make_macro_bool
  } {
    \bool_set_true:N \l_stex_symdecl_make_macro_bool
  }
  \stex_symdecl_do:n { #2 }
  \stex_smsmode_do:
}

\cs_new_protected:Nn \stex_symdecl_do:nn {
  \_@@_args:n{#1}
  \bool_set_false:N \l_stex_symdecl_make_macro_bool
  \stex_symdecl_do:n{#2}
}

\stex_deactivate_macro:Nn \symdecl {module~environments}
%    \end{macrocode}
% \end{macro}
%
%
% \begin{macro}{\stex_symdecl_do:n}
%    \begin{macrocode}
\cs_new_protected:Nn \stex_symdecl_do:n {
  \stex_if_in_module:F {
    % TODO throw error? some default namespace?
  }
  
  \str_if_empty:NT \l_stex_symdecl_name_str {
    \str_set:Nx \l_stex_symdecl_name_str { #1 }
  }

  \prop_if_exist:cT { l_stex_symdecl_ 
      \l_stex_current_module_str ?
      \l_stex_symdecl_name_str
    _prop
  }{
    % TODO throw error (beware of circular dependencies)
  }

  \prop_clear:N \l_tmpa_prop
  \prop_put:Nnx \l_tmpa_prop { module } { \l_stex_current_module_str }
  \seq_clear:N \l_tmpa_seq
  \prop_put:Nno \l_tmpa_prop { name } \l_stex_symdecl_name_str
  \prop_put:Nno \l_tmpa_prop { type } \l_stex_symdecl_type_tl

  \str_if_empty:NT \l_stex_symdecl_deprecate_str {
    \str_if_empty:NF \l_stex_module_deprecate_str {
      \str_set_eq:NN \l_stex_symdecl_deprecate_str \l_stex_module_deprecate_str
    }
  }
  \prop_put:Nno \l_tmpa_prop { deprecate } \l_stex_symdecl_deprecate_str

  \exp_args:No \stex_add_constant_to_current_module:n {
    \l_stex_symdecl_name_str
  }

  % arity/args
  \int_zero:N \l_tmpb_int

  \bool_set_true:N \l_tmpa_bool
  \str_map_inline:Nn \l_stex_symdecl_args_str {
    \token_case_meaning:NnF ##1 {
      0 {} 1 {} 2 {} 3 {} 4 {} 5 {} 6 {} 7 {} 8 {} 9 {}
      {\tl_to_str:n i} { \bool_set_false:N \l_tmpa_bool }
      {\tl_to_str:n b} { \bool_set_false:N \l_tmpa_bool }
      {\tl_to_str:n a} { 
        \bool_set_false:N \l_tmpa_bool
        \int_incr:N \l_tmpb_int
      }
      {\tl_to_str:n B} { 
        \bool_set_false:N \l_tmpa_bool
        \int_incr:N \l_tmpb_int
      }
    }{
      \msg_error:nnxx{stex}{error/wrongargs}{
        \l_stex_current_module_str ?
        \l_stex_symdecl_name_str
      }{##1}
    }
  }

  \bool_if:NTF \l_tmpa_bool {
    % possibly numeric
    \str_if_empty:NTF \l_stex_symdecl_args_str {
      \prop_put:Nnn \l_tmpa_prop { args } {}
      \prop_put:Nnn \l_tmpa_prop { arity } { 0 }
    }{
      \int_set:Nn \l_tmpa_int { \l_stex_symdecl_args_str }
      \prop_put:Nnx \l_tmpa_prop { arity } { \int_use:N \l_tmpa_int }
      \str_clear:N \l_tmpa_str
      \int_step_inline:nn \l_tmpa_int {
        \str_put_right:Nn \l_tmpa_str i
      }
      \prop_put:Nnx \l_tmpa_prop { args } { \l_tmpa_str }
    }
  } {
    \prop_put:Nnx \l_tmpa_prop { args } { \l_stex_symdecl_args_str }
    \prop_put:Nnx \l_tmpa_prop { arity }
      { \str_count:N \l_stex_symdecl_args_str }
  }
  \prop_put:Nnx \l_tmpa_prop { assocs } { \int_use:N \l_tmpb_int }
  
  \tl_if_empty:NTF \l_stex_symdecl_definiens_tl {
    \prop_put:Nnx \l_tmpa_prop { defined }{ false }
  }{
    \prop_put:Nnx \l_tmpa_prop { defined }{ true }
  }

  % argnames

  \clist_clear:N \l_tmpa_clist
  \int_step_inline:nn {\prop_item:Nn \l_tmpa_prop {arity}} {
    \clist_if_empty:NTF \l_stex_symdecl_argnames_clist {
      \clist_put_right:Nn \l_tmpa_clist {##1}
    }{
      \clist_pop:NN \l_stex_symdecl_argnames_clist \l_tmpa_tl
      \exp_args:NNx \clist_put_right:Nn \l_tmpa_clist {\c_dollar_str\l_tmpa_tl}
    }
  }
  \prop_put:Nnx \l_tmpa_prop {argnames} {\clist_use:Nn \l_tmpa_clist ,}

  % semantic macro

  \bool_if:NT \l_stex_symdecl_make_macro_bool {
    \exp_args:Nx \stex_do_up_to_module:n {
      \tl_set:cn { #1 } { \stex_invoke_symbol:n {
        \l_stex_current_module_str ? \l_stex_symdecl_name_str
      }}
    }
  }

  \stex_debug:nn{symbols}{New~symbol:~
    \l_stex_current_module_str ? \l_stex_symdecl_name_str^^J
    Type:~\exp_not:o { \l_stex_symdecl_type_tl }^^J
    Args:~\prop_item:Nn \l_tmpa_prop { args }^^J
    Definiens:~\exp_not:o {\l_stex_symdecl_definiens_tl}
  }

  % circular dependencies require this:
  \stex_if_do_html:T {
    \stex_annotate_invisible:nnn {symdecl} {
      \l_stex_current_module_str ? \l_stex_symdecl_name_str
    } {
      \tl_if_empty:NF \l_stex_symdecl_type_tl {
        \stex_annotate_invisible:nnn{type}{}{$\l_stex_symdecl_type_tl$}
      }
      \stex_annotate_invisible:nnn{args}{\prop_item:Nn \l_tmpa_prop { args }}{}
      \stex_annotate_invisible:nnn{macroname}{#1}{}
      \tl_if_empty:NF \l_stex_symdecl_definiens_tl {
        \stex_annotate_invisible:nnn{definiens}{}
          {$\l_stex_symdecl_definiens_tl$}
      }
      \str_if_empty:NF \l_stex_symdecl_assoctype_str {
        \stex_annotate_invisible:nnn{assoctype}{\l_stex_symdecl_assoctype_str}{}
      }
      \str_if_empty:NF \l_stex_symdecl_reorder_str {
        \stex_annotate_invisible:nnn{reorderargs}{\l_stex_symdecl_reorder_str}{}
      }
    }
  }
  \prop_if_exist:cF {
    l_stex_symdecl_ 
    \l_stex_current_module_str ? \l_stex_symdecl_name_str
    _prop 
  } {
    \bool_if:NTF \l_stex_symdecl_local_bool \stex_do_up_to_module:x \stex_execute_in_module:x {
      \_@@_restore_symbol:nnnnnnnn
        {\l_stex_symdecl_name_str}
        { \prop_item:Nn \l_tmpa_prop {args} }
        { \prop_item:Nn \l_tmpa_prop {arity} }
        { \prop_item:Nn \l_tmpa_prop {assocs} }
        { \prop_item:Nn \l_tmpa_prop {defined} }
        {\bool_if:NT \l_stex_symdecl_make_macro_bool {#1} }
        {\l_stex_current_module_str}
        { \prop_item:Nn \l_tmpa_prop {argnames} }
    }
  }
}
\cs_new_protected:Nn \_@@_restore_symbol:nnnnnnnn {
  \prop_clear:N \l_tmpa_prop
  \prop_put:Nnn \l_tmpa_prop { module } { #7 }
  \prop_put:Nnn \l_tmpa_prop { name } { #1}
  \prop_put:Nnn \l_tmpa_prop { args } {#2}
  \prop_put:Nnn \l_tmpa_prop { arity } { #3 }
  \prop_put:Nnn \l_tmpa_prop { assocs } { #4 }
  \prop_put:Nnn \l_tmpa_prop { defined } { #5 }
  \prop_put:Nnn \l_tmpa_prop { argnames } { #8 }
  \tl_if_empty:nF{#6}{
    \tl_set:cx{#6}{\stex_invoke_symbol:n{\detokenize{#7 ? #1}}}
  }
  \prop_set_eq:cN{l_stex_symdecl_ \detokenize{#7 ? #1} _prop}\l_tmpa_prop
  \seq_clear:c{l_stex_symdecl_ \detokenize{#7 ? #1} _notations}
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\textsymdecl}
%    \begin{macrocode}

\keys_define:nn { stex / textsymdecl } {
  name    .str_set_x:N = \l_@@_name_str ,
  type    .tl_set:N    = \l_@@_type_tl
}

\cs_new_protected:Nn \_stex_textsymdecl_args:n {
  \str_clear:N \l_@@_name_str
  \tl_clear:N \l_@@_type_tl
  \clist_clear:N \l_stex_symdecl_argnames_clist
  \keys_set:nn { stex / textsymdecl } { #1 }
}

\NewDocumentCommand \textsymdecl {m O{} m} {
  \_stex_textsymdecl_args:n { #2 }
  \str_if_empty:NTF \l_@@_name_str {
    \_@@_args:n{name=#1,#2}
  }{
    \_@@_args:n{#2}
  }
  \bool_set_true:N \l_stex_symdecl_make_macro_bool
  \stex_symdecl_do:n{#1-sym}
  \stex_execute_in_module:n{
    \cs_set_nopar:cpn{#1name}{
      \ifvmode\hbox_unpack:N\c_empty_box\fi
      \ifmmode\hbox{#3}\else#3\fi\xspace
    }
    \cs_set_nopar:cpn{#1}{
      \ifmmode\csname#1-sym\expandafter\endcsname\else
      \ifvmode\hbox_unpack:N\c_empty_box\fi
      \symref{#1-sym}{#3}\expandafter\xspace
      \fi
    }
  }
  \stex_execute_in_module:x{
    \__stex_notation_restore_notation:nnnnn
    {\l_stex_current_module_str?\tl_if_empty:NTF\l_@@_name_str{#1}\l_@@_name_str}
    {}{0}
    {\exp_not:n{\STEXInternalTermMathOMSiiii{\STEXInternalCurrentSymbolStr}{}{\neginfprec}{
      \comp{\hbox{#3}}\STEXInternalSymbolAfterInvokationTL
    }}}
    {}
  }
  \stex_smsmode_do:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_get_symbol:n}
%
%    \begin{macrocode}
\str_new:N \l_stex_get_symbol_uri_str

\cs_new_protected:Nn \stex_get_symbol:n {
  \tl_if_head_eq_catcode:nNTF { #1 } \relax {
    \tl_set:Nn \l_tmpa_tl { #1 }
    \_@@_get_symbol_from_cs:
  }{
    % argument is a string
    % is it a command name?
    \cs_if_exist:cTF { #1 }{
      \cs_set_eq:Nc \l_tmpa_tl { #1 }
      \str_set:Nx \l_tmpa_str { \cs_argument_spec:N \l_tmpa_tl }
      \str_if_empty:NTF \l_tmpa_str {
        \exp_args:Nx \cs_if_eq:NNTF {
          \tl_head:N \l_tmpa_tl
        } \stex_invoke_symbol:n {
          \_@@_get_symbol_from_cs:
        }{
          \_@@_get_symbol_from_string:n { #1 }
        }
      } {
        \_@@_get_symbol_from_string:n { #1 }
      }
    }{
      % argument is not a command name
      \_@@_get_symbol_from_string:n { #1 }
      % \l_stex_all_symbols_seq
    }
  }
  \str_if_eq:eeF {
    \prop_item:cn {
      l_stex_symdecl_\l_stex_get_symbol_uri_str _prop
    }{ deprecate }
  }{}{
    \msg_warning:nnxx{stex}{warning/deprecated}{
      Symbol~\l_stex_get_symbol_uri_str
    }{
      \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop}{ deprecate }
    }
  }
}

\cs_new_protected:Nn \_@@_get_symbol_from_string:n {
  \tl_set:Nn \l_tmpa_tl {
    \msg_error:nnn{stex}{error/unknownsymbol}{#1}
  }
  \str_set:Nn \l_tmpa_str { #1 }

  %\int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str }

  \str_if_in:NnTF \l_tmpa_str ? {
    \exp_args:NNno \seq_set_split:Nnn \l_tmpa_seq ? \l_tmpa_str
    \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str
    \str_set:Nx \l_tmpb_str {\seq_use:Nn \l_tmpa_seq ?}
  }{
    \str_clear:N \l_tmpb_str
  }
  \str_if_empty:NTF \l_tmpb_str {
    \seq_map_inline:Nn \l_stex_all_modules_seq {
      \seq_map_inline:cn{c_stex_module_##1_constants}{
        \exp_args:Nno \str_if_eq:nnT{####1} \l_tmpa_str {
          \seq_map_break:n{\seq_map_break:n{
            \tl_set:Nn \l_tmpa_tl {
              \str_set:Nn \l_stex_get_symbol_uri_str { ##1 ? ####1 }
            }
          }}
        }
      }
    } 
  }{
    \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpb_str }
    \seq_map_inline:Nn \l_stex_all_modules_seq {
      \str_if_eq:eeT{ \l_tmpb_str }{ \str_range:nnn {##1}{-\l_tmpa_int}{-1}}{
        \seq_map_inline:cn{c_stex_module_##1_constants}{
          \exp_args:Nno \str_if_eq:nnT{####1} \l_tmpa_str {
            \seq_map_break:n{\seq_map_break:n{
              \tl_set:Nn \l_tmpa_tl {
                \str_set:Nn \l_stex_get_symbol_uri_str { ##1 ? ####1 }
              }
            }}
          }
        }
      }
    }
  }

  \l_tmpa_tl
}

\cs_new_protected:Nn \_@@_get_symbol_from_cs: {
  \exp_args:NNx \tl_set:Nn \l_tmpa_tl 
    { \tl_tail:N \l_tmpa_tl }
  \tl_if_single:NTF \l_tmpa_tl {
    \exp_args:No \tl_if_head_is_group:nTF \l_tmpa_tl {
      \exp_after:wN \str_set:Nn \exp_after:wN
        \l_stex_get_symbol_uri_str \l_tmpa_tl
    }{
      % TODO
      % tail is not a single group
    }
  }{
    % TODO
    % tail is not a single group
  }
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Notations}
%    \begin{macrocode}
%<@@=stex_notation>
%    \end{macrocode}
%
% |notation| arguments:
%
%    \begin{macrocode}
\keys_define:nn { stex / notation } {
%  lang    .tl_set_x:N  = \l_@@_lang_str ,
  variant .tl_set_x:N   = \l_@@_variant_str ,
  prec    .str_set_x:N  = \l_@@_prec_str ,
  op      .tl_set:N     = \l_@@_op_tl ,
  primary .bool_set:N   = \l_@@_primary_bool ,
  primary .default:n    = {true} ,
  hints    .str_set_x:N = \l_@@_hints_str,
  unknown .code:n       = \str_set:Nx 
      \l_@@_variant_str \l_keys_key_str
}

\cs_new_protected:Nn \_stex_notation_args:n {
%  \str_clear:N \l_@@_lang_str
  \str_clear:N \l_@@_variant_str
  \str_clear:N \l_@@_prec_str
  \str_clear:N \l_@@_hints_str
  \tl_clear:N \l_@@_op_tl
  \bool_set_false:N \l_@@_primary_bool
  
  \keys_set:nn { stex / notation } { #1 }
}
%    \end{macrocode}
%
%
%
% \begin{macro}{\notation}
%    \begin{macrocode}
\NewDocumentCommand \notation { s m O{}} {
  \_stex_notation_args:n { #3 }
  \tl_clear:N \l_stex_symdecl_definiens_tl
  \stex_get_symbol:n { #2 }
  \tl_set:Nn \l_stex_notation_after_do_tl {
    \_@@_final:
    \IfBooleanTF#1{
      \stex_setnotation:n {\l_stex_get_symbol_uri_str}
    }{}
    \stex_smsmode_do:\ignorespacesandpars
  }
  \stex_notation_do:nnnnn
    { \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { args } }
    { \prop_item:cn { l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { arity } }
    { \l_@@_variant_str }
    { \l_@@_prec_str}
}
\stex_deactivate_macro:Nn \notation {module~environments}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_notation_do:nnnnn}
%    \begin{macrocode}
\seq_new:N \l_@@_precedences_seq
\tl_new:N \l_@@_opprec_tl
\int_new:N \l_@@_currarg_int
\tl_new:N \STEXInternalSymbolAfterInvokationTL

\cs_new_protected:Nn \stex_notation_do:nnnnn {
  \let\STEXInternalCurrentSymbolStr\relax
  \seq_clear:N \l_@@_precedences_seq
  \tl_clear:N \l_@@_opprec_tl
  \str_set:Nx \l_@@_args_str { #1 }
  \str_set:Nx \l_@@_arity_str { #2 }
  \str_set:Nx \l_@@_suffix_str { #3 }
  \str_set:Nx \l_@@_prec_str { #4 }

  % precedences
  \str_if_empty:NTF \l_@@_prec_str {
    \int_compare:nNnTF \l_@@_arity_str = 0 {
      \tl_set:No \l_@@_opprec_tl { \neginfprec }
    }{
      \tl_set:Nn \l_@@_opprec_tl { 0 }
    }
  } {
    \str_if_eq:onTF \l_@@_prec_str {nobrackets}{
      \tl_set:No \l_@@_opprec_tl { \neginfprec }
      \int_step_inline:nn { \l_@@_arity_str } {
        \exp_args:NNo
        \seq_put_right:Nn \l_@@_precedences_seq { \infprec }
      }
    }{
      \seq_set_split:NnV \l_tmpa_seq ; \l_@@_prec_str
      \seq_pop_left:NNTF \l_tmpa_seq \l_tmpa_str {
        \tl_set:No \l_@@_opprec_tl { \l_tmpa_str }
        \seq_pop_left:NNT \l_tmpa_seq \l_tmpa_str {
          \exp_args:NNNo \exp_args:NNno \seq_set_split:Nnn 
            \l_tmpa_seq {\tl_to_str:n{x} } { \l_tmpa_str }
          \seq_map_inline:Nn \l_tmpa_seq {
            \seq_put_right:Nn \l_@@_precedences_seq { ##1 }
          }
        }
      }{
        \int_compare:nNnTF \l_@@_arity_str = 0 {
          \tl_set:No \l_@@_opprec_tl { \infprec }
        }{
          \tl_set:No \l_@@_opprec_tl { 0 }
        }
      }
    }
  }

  \seq_set_eq:NN \l_tmpa_seq \l_@@_precedences_seq
  \int_step_inline:nn { \l_@@_arity_str } {
    \seq_pop_left:NNF \l_tmpa_seq \l_tmpb_str {
      \exp_args:NNo
      \seq_put_right:No \l_@@_precedences_seq { 
        \l_@@_opprec_tl
      }
    }
  }
  \tl_clear:N \l_stex_notation_dummyargs_tl

  \int_compare:nNnTF \l_@@_arity_str = 0 {
    \exp_args:NNe
    \cs_set:Npn \l_stex_notation_macrocode_cs {
      \STEXInternalTermMathOMSiiii { \STEXInternalCurrentSymbolStr } 
        { \l_@@_suffix_str }
        { \l_@@_opprec_tl } 
        { \exp_not:n { #5 } }
    }
    \l_stex_notation_after_do_tl
  }{
    \str_if_in:NnTF \l_@@_args_str b {
      \exp_args:Nne \use:nn
      {
      \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs
      \cs_set:Npn \l_@@_arity_str } { {
        \STEXInternalTermMathOMBiiii { \STEXInternalCurrentSymbolStr } 
          { \l_@@_suffix_str }
          { \l_@@_opprec_tl } 
          { \exp_not:n { #5 } }
      }}
    }{
      \str_if_in:NnTF \l_@@_args_str B {
        \exp_args:Nne \use:nn
        {
        \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs
        \cs_set:Npn \l_@@_arity_str } { {
          \STEXInternalTermMathOMBiiii { \STEXInternalCurrentSymbolStr } 
            { \l_@@_suffix_str }
            { \l_@@_opprec_tl } 
            { \exp_not:n { #5 } }
        } }
      }{
        \exp_args:Nne \use:nn
        {
        \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs
        \cs_set:Npn \l_@@_arity_str } { {
          \STEXInternalTermMathOMAiiii { \STEXInternalCurrentSymbolStr } 
            { \l_@@_suffix_str }
            { \l_@@_opprec_tl } 
            { \exp_not:n { #5 } }
        } }
      }
    }

    \str_set_eq:NN \l_@@_remaining_args_str \l_@@_args_str
    \int_zero:N \l_@@_currarg_int
    \seq_set_eq:NN \l_@@_remaining_precs_seq \l_@@_precedences_seq
    \_@@_arguments:
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\_@@_arguments:}
%
% Takes care of annotating the arguments in a
% notation macro
%
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_arguments: {
  \int_incr:N \l_@@_currarg_int
  \str_if_empty:NTF \l_@@_remaining_args_str {
    \l_stex_notation_after_do_tl
  }{
    \str_set:Nx \l_tmpa_str { \str_head:N \l_@@_remaining_args_str }
    \str_set:Nx \l_@@_remaining_args_str { \str_tail:N \l_@@_remaining_args_str }
    \str_if_eq:VnTF \l_tmpa_str a {
      \_@@_argument_assoc:nn{a}
    }{
      \str_if_eq:VnTF \l_tmpa_str B {
        \_@@_argument_assoc:nn{B}
      }{
        \seq_pop_left:NN \l_@@_remaining_precs_seq \l_tmpb_str
        \tl_put_right:Nx \l_stex_notation_dummyargs_tl {
          { \STEXInternalTermMathArgiii
            { \l_tmpa_str\int_use:N \l_@@_currarg_int }
            { \l_tmpb_str }
            { ####\int_use:N \l_@@_currarg_int }
          }
        }
        \_@@_arguments:
      }
    }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\_@@_argument_assoc:nn}
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_argument_assoc:nn {

  \cs_generate_from_arg_count:NNnn \l_tmpa_cs \cs_set:Npn 
    {\l_@@_arity_str}{
    #2
  }
  \int_zero:N \l_tmpa_int
  \tl_clear:N \l_tmpa_tl
  \str_map_inline:Nn \l_@@_args_str {
    \int_incr:N \l_tmpa_int
    \tl_put_right:Nx \l_tmpa_tl {
      \str_if_eq:nnTF {##1}{a}{ {} }{
        \str_if_eq:nnTF {##1}{B}{ {} }{
          {\_stex_term_arg:nn{##1\int_use:N \l_tmpa_int}{################ \int_use:N \l_tmpa_int}}
        }
      }
    }
  }
  \exp_after:wN\exp_after:wN\exp_after:wN \def 
  \exp_after:wN\exp_after:wN\exp_after:wN \l_tmpa_cs 
  \exp_after:wN\exp_after:wN\exp_after:wN ## 
  \exp_after:wN\exp_after:wN\exp_after:wN 1 
  \exp_after:wN\exp_after:wN\exp_after:wN ## 
  \exp_after:wN\exp_after:wN\exp_after:wN 2 
  \exp_after:wN\exp_after:wN\exp_after:wN {
    \exp_after:wN \exp_after:wN \exp_after:wN 
    \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN {
      \exp_after:wN \l_tmpa_cs \l_tmpa_tl
    }
  }

  \seq_pop_left:NN \l_@@_remaining_precs_seq \l_tmpa_str
  \tl_put_right:Nx \l_stex_notation_dummyargs_tl { {
    \STEXInternalTermMathAssocArgiiiii
      { \int_use:N \l_@@_currarg_int }
      { \l_tmpa_str }
      { ####\int_use:N \l_@@_currarg_int }
      { \l_tmpa_cs {####1} {####2} }
      {#1}
  } }
  \_@@_arguments:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\_@@_final:}
%
% Called after processing all notation arguments
%
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_restore_notation:nnnnn {
  \cs_generate_from_arg_count:cNnn{stex_notation_\detokenize{#1} \c_hash_str \detokenize{#2}_cs}
  \cs_set_nopar:Npn {#3}{#4}
  \tl_if_empty:nF {#5}{
    \tl_set:cn{stex_op_notation_\detokenize{#1} \c_hash_str \detokenize{#2}_cs}{ \comp{ #5 } }
  }
  \seq_if_exist:cT { l_stex_symdecl_\detokenize{#1} _notations }{
    \seq_put_right:cx { l_stex_symdecl_\detokenize{#1} _notations } { \detokenize{#2} }
  }
}

\cs_new_protected:Nn \_@@_final: {

  \stex_execute_in_module:x {
    \_@@_restore_notation:nnnnn
      {\l_stex_get_symbol_uri_str}
      {\l_@@_suffix_str}
      {\l_@@_arity_str}
      {
        \exp_after:wN \exp_after:wN \exp_after:wN
        \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN 
        { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \STEXInternalSymbolAfterInvokationTL}
      }
      {\exp_args:No \exp_not:n \l_@@_op_tl }
  }

  \stex_debug:nn{symbols}{
    Notation~\l_@@_suffix_str
    ~for~\l_stex_get_symbol_uri_str^^J
    Operator~precedence:~\l_@@_opprec_tl^^J
    Argument~precedences:~
      \seq_use:Nn \l_@@_precedences_seq {,~}^^J
    Notation: \cs_meaning:c {
      stex_notation_ \l_stex_get_symbol_uri_str \c_hash_str 
      \l_@@_suffix_str
      _cs
    }
  }
    % HTML annotations
  \stex_if_do_html:T {
    \stex_annotate_invisible:nnn { notation }
    { \l_stex_get_symbol_uri_str } {
      \stex_annotate_invisible:nnn { notationfragment }
        { \l_@@_suffix_str }{}
      \stex_annotate_invisible:nnn { precedence }
        { \l_@@_prec_str }{}

      \int_zero:N \l_tmpa_int
      \str_set_eq:NN \l_@@_remaining_args_str \l_@@_args_str
      \tl_clear:N \l_tmpa_tl
      \int_step_inline:nn { \l_@@_arity_str }{
        \int_incr:N \l_tmpa_int
        \str_set:Nx \l_tmpb_str { \str_head:N \l_@@_remaining_args_str }
        \str_set:Nx \l_@@_remaining_args_str { \str_tail:N \l_@@_remaining_args_str }
        \str_if_eq:VnTF \l_tmpb_str a {
          \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { 
            \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} ,
            \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{}
          } }
        }{
          \str_if_eq:VnTF \l_tmpb_str B {
            \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { 
              \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} ,
              \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{}
            } }
          }{
            \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { 
              \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int}{}
            } }
          }
        }
      }
      \stex_annotate_invisible:nnn { notationcomp }{}{
        \str_set:Nx \STEXInternalCurrentSymbolStr {\l_stex_get_symbol_uri_str }
        $ \exp_args:Nno \use:nn { \use:c {
          stex_notation_ \STEXInternalCurrentSymbolStr
          \c_hash_str \l_@@_suffix_str _cs
        } } { \l_tmpa_tl } $
      }
      \tl_if_empty:NF \l_@@_op_tl {
        \stex_annotate_invisible:nnn { notationopcomp }{}{
          $\l_@@_op_tl$
        }
      }
    }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\setnotation}
%    \begin{macrocode}
\keys_define:nn { stex / setnotation } {
%  lang    .tl_set_x:N  = \l_@@_lang_str ,
  variant .tl_set_x:N  = \l_@@_variant_str ,
  unknown .code:n      = \str_set:Nx 
      \l_@@_variant_str \l_keys_key_str
}

\cs_new_protected:Nn \_stex_setnotation_args:n {
 % \str_clear:N \l_@@_lang_str
  \str_clear:N \l_@@_variant_str
  \keys_set:nn { stex / setnotation } { #1 }
}

\cs_new_protected:Nn \_@@_setnotation:nn {
  \seq_if_exist:cT{l_stex_symdecl_#1_notations}{
    \seq_remove_all:cn { l_stex_symdecl_#1 _notations }{ #2 }
    \seq_put_left:cn { l_stex_symdecl_#1 _notations }{ #2 }
  }
}

\cs_new_protected:Nn \stex_setnotation:n {
  \exp_args:Nnx \seq_if_in:cnTF { l_stex_symdecl_#1 _notations }
    { \l_@@_variant_str }{
      \stex_execute_in_module:x{ \_@@_setnotation:nn {#1}{\l_@@_variant_str} }
      \stex_debug:nn {notations}{
        Setting~default~notation~
        {\l_@@_variant_str }~for~
        #1 \\
        \expandafter\meaning\csname
        l_stex_symdecl_#1 _notations\endcsname
      }
    }{
      \msg_error:nnxx{stex}{unknownnotation}{\l_@@_variant_str}{#1}
    }
}

\NewDocumentCommand \setnotation {m m} {
  \stex_get_symbol:n { #1 }
  \_stex_setnotation_args:n { #2 }
  \stex_setnotation:n{\l_stex_get_symbol_uri_str}
  \stex_smsmode_do:\ignorespacesandpars
}

\cs_new_protected:Nn \stex_copy_notations:nn {
  \stex_debug:nn {notations}{
    Copying~notations~from~#2~to~#1\\
    \seq_use:cn{l_stex_symdecl_#2_notations}{,~}
  }
  \tl_clear:N \l_tmpa_tl
  \int_step_inline:nn { \prop_item:cn {l_stex_symdecl_#2_prop}{ arity } } {
    \tl_put_right:Nn \l_tmpa_tl { {######## ##1} }
  }
  \seq_map_inline:cn {l_stex_symdecl_#2_notations}{\begingroup
    \stex_debug:nn{Here}{Here:~##1}
    \cs_set_eq:Nc \l_tmpa_cs { stex_notation_ #2 \c_hash_str ##1 _cs }
    \edef \l_tmpa_tl {
      \exp_after:wN\exp_after:wN\exp_after:wN \exp_not:n 
      \exp_after:wN\exp_after:wN\exp_after:wN {
        \exp_after:wN \l_tmpa_cs \l_tmpa_tl
      }
    }

    \exp_after:wN \def \exp_after:wN \l_tmpa_tl 
    \exp_after:wN ####\exp_after:wN 1 \exp_after:wN ####\exp_after:wN 2
    \exp_after:wN  { \l_tmpa_tl }

    \edef \l_tmpa_tl {
      \exp_after:wN \exp_not:n \exp_after:wN {
        \l_tmpa_tl {######## 1}{######## 2}
      }
    }

    \stex_debug:nn{Here}{Here:~\expandafter\detokenize\expandafter{\l_tmpa_tl}}

    \stex_execute_in_module:x {
      \_@@_restore_notation:nnnnn 
        {#1}{##1}
        { \prop_item:cn {l_stex_symdecl_#2_prop}{ arity } }
        { \exp_after:wN\exp_not:n\exp_after:wN{\l_tmpa_tl} }
        {
          \cs_if_exist:cT{stex_op_notation_ #2\c_hash_str ##1 _cs}{
            \exp_args:NNo\exp_args:No\exp_not:n{\csname stex_op_notation_ #2\c_hash_str ##1 _cs\endcsname}
          }
        }
    }\endgroup
  }
}

\NewDocumentCommand \copynotation {m m} {
  \stex_get_symbol:n { #1 }
  \str_set_eq:NN \l_tmpa_str \l_stex_get_symbol_uri_str
  \stex_get_symbol:n { #2 }
  \exp_args:Noo
  \stex_copy_notations:nn \l_tmpa_str \l_stex_get_symbol_uri_str
  \stex_smsmode_do:\ignorespacesandpars
}

%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\symdef}
%    \begin{macrocode}
\keys_define:nn { stex / symdef } {
  name    .str_set_x:N = \l_stex_symdecl_name_str ,
  args    .str_set_x:N = \l_stex_symdecl_args_str ,
  type    .tl_set:N    = \l_stex_symdecl_type_tl ,
  def     .tl_set:N    = \l_stex_symdecl_definiens_tl ,
  reorder .str_set_x:N = \l_stex_symdecl_reorder_str ,
  op      .tl_set:N    = \l_@@_op_tl ,
 % lang    .str_set_x:N = \l_@@_lang_str ,
  variant .str_set_x:N = \l_@@_variant_str ,
  prec    .str_set_x:N = \l_@@_prec_str ,
  argnames    .clist_set:N  = \l_stex_symdecl_argnames_clist ,
  assoc   .choices:nn  = 
      {bin,binl,binr,pre,conj,pwconj}
      {\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}},
  unknown .code:n      = \str_set:Nx 
      \l_@@_variant_str \l_keys_key_str
}

\cs_new_protected:Nn \_@@_symdef_args:n {
  \str_clear:N \l_stex_symdecl_name_str
  \str_clear:N \l_stex_symdecl_args_str
  \str_clear:N \l_stex_symdecl_assoctype_str
  \str_clear:N \l_stex_symdecl_reorder_str
  \bool_set_false:N \l_stex_symdecl_local_bool
  \tl_clear:N \l_stex_symdecl_type_tl
  \tl_clear:N \l_stex_symdecl_definiens_tl
  \clist_clear:N \l_stex_symdecl_argnames_clist
 % \str_clear:N \l_@@_lang_str
  \str_clear:N \l_@@_variant_str
  \str_clear:N \l_@@_prec_str
  \tl_clear:N \l_@@_op_tl
  
  \keys_set:nn { stex / symdef } { #1 }
}

\NewDocumentCommand \symdef { m O{} } {
  \_@@_symdef_args:n { #2 }
  \bool_set_true:N \l_stex_symdecl_make_macro_bool
  \stex_symdecl_do:n { #1 }
  \tl_set:Nn \l_stex_notation_after_do_tl {
    \_@@_final:
    \stex_smsmode_do:\ignorespacesandpars
  }
  \str_set:Nx \l_stex_get_symbol_uri_str {
    \l_stex_current_module_str ? \l_stex_symdecl_name_str
  }
  \exp_args:Nx \stex_notation_do:nnnnn
    { \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { args } }
    { \prop_item:cn { l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { arity } }
    { \l_@@_variant_str }
    { \l_@@_prec_str}
}
\stex_deactivate_macro:Nn \symdef {module~environments}

\keys_define:nn { stex / mmtdef } {
  name    .str_set_x:N = \l_stex_symdecl_name_str ,
  args    .str_set_x:N = \l_stex_symdecl_args_str ,
  reorder .str_set_x:N = \l_stex_symdecl_reorder_str ,
  op      .tl_set:N    = \l_@@_op_tl ,
 % lang    .str_set_x:N = \l_@@_lang_str ,
  variant .str_set_x:N = \l_@@_variant_str ,
  prec    .str_set_x:N = \l_@@_prec_str ,
  argnames    .clist_set:N  = \l_stex_symdecl_argnames_clist ,
  assoc   .choices:nn  = 
      {bin,binl,binr,pre,conj,pwconj}
      {\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}},
  unknown .code:n      = \str_set:Nx 
      \l_@@_variant_str \l_keys_key_str
}
\cs_new_protected:Nn \_stex_mmtdef_args:n {
  \str_clear:N \l_stex_symdecl_name_str
  \str_clear:N \l_stex_symdecl_args_str
  \str_clear:N \l_stex_symdecl_assoctype_str
  \str_clear:N \l_stex_symdecl_reorder_str
  \bool_set_false:N \l_stex_symdecl_local_bool
  \clist_clear:N \l_stex_symdecl_argnames_clist
 % \str_clear:N \l_@@_lang_str
  \str_clear:N \l_@@_variant_str
  \str_clear:N \l_@@_prec_str
  \tl_clear:N \l_@@_op_tl
  
  \keys_set:nn { stex / mmtdef } { #1 }
}

\NewDocumentCommand \mmtdef {m O{} }{
  \_stex_mmtdef_args:n{ #2 }
  \bool_set_true:N \l_stex_symdecl_make_macro_bool
  \str_if_empty:NT \l_stex_symdecl_name_str {
    \str_set:Nx \l_stex_symdecl_name_str { #1 }
  }
  %\tl_set:Nx \l_stex_symdecl_definiens_tl {
  %  \stex_annotate:nnn{ OMID }{
  %    \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str 
  %  }{}
  %}
  \stex_symdecl_do:n { #1 }
  \MMTrule{rules.stex.mmt.kwarc.info?SubstitutionRule}{
    \stex_annotate:nnn{ OMID }{
      \l_stex_current_module_str ? \l_stex_symdecl_name_str
    }{},
    \stex_annotate:nnn{ OMID }{
      \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str 
    }{}
  }
  \tl_set:Nn \l_stex_notation_after_do_tl {
    \_@@_final:
    \stex_smsmode_do:\ignorespacesandpars
  }
  \str_set:Nx \l_stex_get_symbol_uri_str {
    \l_stex_current_module_str ? \l_stex_symdecl_name_str
  }
  \exp_args:Nx \stex_notation_do:nnnnn
    { \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { args } }
    { \prop_item:cn { l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { arity } }
    { \l_@@_variant_str }
    { \l_@@_prec_str}
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Variables}
%
%    \begin{macrocode}
%<@@=stex_variables>

\keys_define:nn { stex / vardef } {
  name    .str_set_x:N  = \l_@@_name_str ,
  args    .str_set_x:N  = \l_@@_args_str ,
  type    .tl_set:N     = \l_@@_type_tl ,
  def     .tl_set:N     = \l_@@_def_tl ,
  op      .tl_set:N     = \l_@@_op_tl ,
  prec    .str_set_x:N  = \l_@@_prec_str ,
  reorder .str_set_x:N  = \l_@@_reorder_str ,
  argnames    .clist_set:N  = \l_@@_argnames_clist ,
  assoc   .choices:nn   = 
      {bin,binl,binr,pre,conj,pwconj}
      {\str_set:Nx \l_@@_assoctype_str {\l_keys_choice_tl}},
  bind    .choices:nn   =
      {forall,exists}
      {\str_set:Nx \l_@@_bind_str {\l_keys_choice_tl}}
}

\cs_new_protected:Nn \_@@_args:n {
  \str_clear:N \l_@@_name_str
  \str_clear:N \l_@@_args_str
  \str_clear:N \l_@@_prec_str
  \str_clear:N \l_@@_assoctype_str
  \str_clear:N \l_@@_reorder_str
  \str_clear:N \l_@@_bind_str
  \tl_clear:N \l_@@_type_tl
  \tl_clear:N \l_@@_def_tl
  \tl_clear:N \l_@@_op_tl
  \clist_clear:N \l_@@_argnames_clist

  \keys_set:nn { stex / vardef } { #1 }
}

\NewDocumentCommand \_@@_do_simple:nnn { m O{}} {
  \_@@_args:n {#2}
  \str_if_empty:NT \l_@@_name_str {
    \str_set:Nx \l_@@_name_str { #1 }
  }
  \prop_clear:N \l_tmpa_prop
  \prop_put:Nno \l_tmpa_prop { name } \l_@@_name_str
  
  \int_zero:N \l_tmpb_int
  \bool_set_true:N \l_tmpa_bool
  \str_map_inline:Nn \l_@@_args_str {
    \token_case_meaning:NnF ##1 {
      0 {} 1 {} 2 {} 3 {} 4 {} 5 {} 6 {} 7 {} 8 {} 9 {}
      {\tl_to_str:n i} { \bool_set_false:N \l_tmpa_bool }
      {\tl_to_str:n b} { \bool_set_false:N \l_tmpa_bool }
      {\tl_to_str:n a} { 
        \bool_set_false:N \l_tmpa_bool
        \int_incr:N \l_tmpb_int
      }
      {\tl_to_str:n B} { 
        \bool_set_false:N \l_tmpa_bool
        \int_incr:N \l_tmpb_int
      }
    }{
      \msg_error:nnxx{stex}{error/wrongargs}{
        variable~\l_@@_name_str
      }{##1}
    }
  }
  \bool_if:NTF \l_tmpa_bool {
    % possibly numeric
    \str_if_empty:NTF \l_@@_args_str {
      \prop_put:Nnn \l_tmpa_prop { args } {}
      \prop_put:Nnn \l_tmpa_prop { arity } { 0 }
    }{
      \int_set:Nn \l_tmpa_int { \l_@@_args_str }
      \prop_put:Nnx \l_tmpa_prop { arity } { \int_use:N \l_tmpa_int }
      \str_clear:N \l_tmpa_str
      \int_step_inline:nn \l_tmpa_int {
        \str_put_right:Nn \l_tmpa_str i
      }
      \str_set_eq:NN \l_@@_args_str \l_tmpa_str
      \prop_put:Nnx \l_tmpa_prop { args } { \l_@@_args_str }
    }
  } {
    \prop_put:Nnx \l_tmpa_prop { args } { \l_@@_args_str }
    \prop_put:Nnx \l_tmpa_prop { arity }
      { \str_count:N \l_@@_args_str }
  }
  \prop_put:Nnx \l_tmpa_prop { assocs } { \int_use:N \l_tmpb_int }
  \tl_set:cx { #1 }{ \stex_invoke_variable:n { \l_@@_name_str } }

  % argnames

  \clist_clear:N \l_tmpa_clist
  \int_step_inline:nn {\prop_item:Nn \l_tmpa_prop {arity}} {
    \clist_if_empty:NTF \l_@@_argnames_clist {
      \clist_put_right:Nn \l_tmpa_clist {##1}
    }{
      \clist_pop:NN \l_@@_argnames_clist \l_tmpa_tl
      \exp_args:NNx \clist_put_right:Nn \l_tmpa_clist {\c_dollar_str\l_tmpa_tl}
    }
  }
  \prop_put:Nnx \l_tmpa_prop {argnames} {\clist_use:Nn \l_tmpa_clist ,}


  \prop_set_eq:cN { l_stex_symdecl_var://\l_@@_name_str _prop} \l_tmpa_prop

  \tl_if_empty:NF \l_@@_op_tl {
    \cs_set:cpx {
      stex_var_op_notation_ \l_@@_name_str _cs
    } { \exp_not:N\comp{ \exp_args:No \exp_not:n { \l_@@_op_tl } } }
  }

  \tl_set:Nn \l_stex_notation_after_do_tl {
    \exp_args:Nne \use:nn {
      \cs_generate_from_arg_count:cNnn { stex_var_notation_\l_@@_name_str _cs }
        \cs_set:Npn { \prop_item:Nn \l_tmpa_prop { arity } }
    } {{
      \exp_after:wN \exp_after:wN \exp_after:wN
      \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN 
      { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \STEXInternalSymbolAfterInvokationTL}
    }}
    \stex_if_do_html:T {
      \stex_annotate_invisible:nnn {vardecl}{\l_@@_name_str}{
        \stex_annotate_invisible:nnn { precedence }
          { \l_@@_prec_str }{}
        \tl_if_empty:NF \l_@@_type_tl {\stex_annotate_invisible:nnn{type}{}{$\l_@@_type_tl$}}
        \stex_annotate_invisible:nnn{args}{ \l_@@_args_str }{}
        \stex_annotate_invisible:nnn{macroname}{#1}{}
        \tl_if_empty:NF \l_@@_def_tl {
          \stex_annotate_invisible:nnn{definiens}{}
            {$\l_@@_def_tl$}
        }
        \str_if_empty:NF \l_@@_assoctype_str {
          \stex_annotate_invisible:nnn{assoctype}{\l_@@_assoctype_str}{}
        }
        \str_if_empty:NF \l_@@_reorder_str {
          \stex_annotate_invisible:nnn{reorderargs}{\l_@@_reorder_str}{}
        }
        \int_zero:N \l_tmpa_int
        \str_set_eq:NN \l_@@_remaining_args_str \l_@@_args_str
        \tl_clear:N \l_tmpa_tl
        \int_step_inline:nn { \prop_item:Nn \l_tmpa_prop { arity } }{
          \int_incr:N \l_tmpa_int
          \str_set:Nx \l_tmpb_str { \str_head:N \l_@@_remaining_args_str }
          \str_set:Nx \l_@@_remaining_args_str { \str_tail:N \l_@@_remaining_args_str }
          \str_if_eq:VnTF \l_tmpb_str a {
            \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { 
              \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} ,
              \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{}
            } }
          }{
            \str_if_eq:VnTF \l_tmpb_str B {
              \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { 
                \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} ,
                \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{}
              } }
            }{
              \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { 
                \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int}{}
              } }
            }
          }
        }
        \stex_annotate_invisible:nnn { notationcomp }{}{
          \str_set:Nx \STEXInternalCurrentSymbolStr {var://\l_@@_name_str }
          $ \exp_args:Nno \use:nn { \use:c {
            stex_var_notation_\l_@@_name_str _cs
          } } { \l_tmpa_tl } $
        }
        \tl_if_empty:NF \l_@@_op_tl {
          \stex_annotate_invisible:nnn { notationopcomp }{}{
            $\l_@@_op_tl$
          }
        }
      }
      \str_if_empty:NF \l_@@_bind_str {
        \stex_annotate_invisible:nnn {bindtype}{\l_@@_bind_str,\l_@@_name_str}{}
      }
    }\ignorespacesandpars
  }

  \stex_notation_do:nnnnn { \l_@@_args_str } { \prop_item:Nn \l_tmpa_prop { arity } } {}{ \l_@@_prec_str}
}

\cs_new:Nn \_stex_reset:N {
  \tl_if_exist:NTF #1 {
    \def \exp_not:N #1 { \exp_args:No \exp_not:n #1 }
  }{
    \let \exp_not:N #1 \exp_not:N \undefined
  }
}

\NewDocumentCommand \_@@_do_complex:nn { m m }{
  \clist_set:Nx \l_@@_names { \tl_to_str:n {#1} }
  \exp_args:Nnx \use:nn {
    % TODO
    \stex_annotate_invisible:nnn {vardecl}{\clist_use:Nn\l_@@_names,}{
      #2
    }
  }{
    \_stex_reset:N \varnot
    \_stex_reset:N \vartype
    \_stex_reset:N \vardefi
  }
}

\NewDocumentCommand \vardef { s } {
  \IfBooleanTF#1 {
    \_@@_do_complex:nn
  }{
    \_@@_do_simple:nnn
  }
}

\NewDocumentCommand \svar { O{} m }{
  \tl_if_empty:nTF {#1}{
    \str_set:Nn \l_tmpa_str { #2 }
  }{
    \str_set:Nn \l_tmpa_str { #1 }
  }
  \_stex_term_omv:nn {
    var://\l_tmpa_str
  }{ 
    \exp_args:Nnx \use:nn {
      \def\comp{\_varcomp}
      \str_set:Nx \STEXInternalCurrentSymbolStr { var://\l_tmpa_str }
      \comp{ #2 }
    }{
      \_stex_reset:N \comp
      \_stex_reset:N \STEXInternalCurrentSymbolStr
    }
  }
}



\keys_define:nn { stex / varseq } {
  name    .str_set_x:N  = \l_@@_name_str ,
  args    .int_set:N    = \l_@@_args_int ,
  type    .tl_set:N     = \l_@@_type_tl  ,
  mid     .tl_set:N     = \l_@@_mid_tl   ,
  bind    .choices:nn   =
      {forall,exists}
      {\str_set:Nx \l_@@_bind_str {\l_keys_choice_tl}}
}

\cs_new_protected:Nn \_@@_seq_args:n {
  \str_clear:N \l_@@_name_str
  \int_set:Nn \l_@@_args_int 1
  \tl_clear:N \l_@@_type_tl
  \str_clear:N \l_@@_bind_str

  \keys_set:nn { stex / varseq } { #1 }
}

\NewDocumentCommand \varseq {m O{} m m m}{
  \_@@_seq_args:n { #2 }
  \str_if_empty:NT \l_@@_name_str {
    \str_set:Nx \l_@@_name_str { #1 }
  }
  \prop_clear:N \l_tmpa_prop
  \prop_put:Nnx \l_tmpa_prop { arity }{\int_use:N \l_@@_args_int}

  \seq_set_from_clist:Nn \l_tmpa_seq {#3}
  \int_compare:nNnF {\seq_count:N \l_tmpa_seq} = \l_@@_args_int {
    \msg_error:nnxx{stex}{error/seqlength}
      {\int_use:N \l_@@_args_int}
      {\seq_count:N \l_tmpa_seq}
  }
  \seq_set_from_clist:Nn \l_tmpb_seq {#4}
  \int_compare:nNnF {\seq_count:N \l_tmpb_seq} = \l_@@_args_int {
    \msg_error:nnxx{stex}{error/seqlength}
      {\int_use:N \l_@@_args_int}
      {\seq_count:N \l_tmpb_seq}
  }
  \prop_put:Nnn \l_tmpa_prop {starts} {#3}
  \prop_put:Nnn \l_tmpa_prop {ends} {#4}

  \cs_generate_from_arg_count:cNnn {stex_varseq_\l_@@_name_str _cs}
    \cs_set:Npn  {\int_use:N \l_@@_args_int} { #5 }

  % argnames

  \clist_clear:N \l_tmpa_clist
  \int_step_inline:nn {\l_@@_args_int} {
      \clist_put_right:Nn \l_tmpa_clist {##1}
  }
  \prop_put:Nnx \l_tmpa_prop {argnames} {\clist_use:Nn \l_tmpa_clist ,}



  
  \exp_args:NNo \tl_set:No \l_tmpa_tl {\use:c{stex_varseq_\l_@@_name_str _cs}}
  \int_step_inline:nn \l_@@_args_int {
    \tl_put_right:Nx \l_tmpa_tl { {\seq_item:Nn \l_tmpa_seq {##1}} }
  }
  \tl_set:Nx \l_tmpa_tl {\exp_args:NNo \exp_args:No \exp_not:n{\l_tmpa_tl}}
  \tl_put_right:Nn \l_tmpa_tl {,\ellipses,}
  \tl_if_empty:NF \l_@@_mid_tl {
    \tl_put_right:No \l_tmpa_tl \l_@@_mid_tl
    \tl_put_right:Nn \l_tmpa_tl {,\ellipses,}
  }
  \exp_args:NNo \tl_set:No \l_tmpb_tl {\use:c{stex_varseq_\l_@@_name_str _cs}}
  \int_step_inline:nn \l_@@_args_int {
    \tl_put_right:Nx \l_tmpb_tl { {\seq_item:Nn \l_tmpb_seq {##1}} }
  }
  \tl_set:Nx \l_tmpb_tl {\exp_args:NNo \exp_args:No \exp_not:n{\l_tmpb_tl}}
  \tl_put_right:No \l_tmpa_tl \l_tmpb_tl
  

  \prop_put:Nno \l_tmpa_prop { notation }\l_tmpa_tl

  \tl_set:cx {#1} {\stex_invoke_sequence:n {\l_@@_name_str}}

  \exp_args:NNo \tl_set:No \l_tmpa_tl {\use:c{stex_varseq_\l_@@_name_str _cs}}

  \int_step_inline:nn \l_@@_args_int {
    \tl_set:Nx \l_tmpa_tl {\exp_args:No \exp_not:n \l_tmpa_tl {
      \STEXInternalTermMathArgiii{i##1}{0}{\exp_not:n{####}##1}
    }}
  }

  \tl_set:Nx \l_tmpa_tl {
    \STEXInternalTermMathOMAiiii { varseq://\l_@@_name_str}{}{0}{
      \exp_args:NNo \exp_args:No \exp_not:n {\l_tmpa_tl}
    }
  }

  \tl_set:No \l_tmpa_tl { \exp_after:wN { \l_tmpa_tl \STEXInternalSymbolAfterInvokationTL} }
  
  \exp_args:Nno \use:nn {
  \cs_generate_from_arg_count:cNnn {stex_varseq_\l_@@_name_str _cs}
    \cs_set:Npn {\int_use:N \l_@@_args_int}}{\l_tmpa_tl}

  \stex_debug:nn{sequences}{New~Sequence:~
    \expandafter\meaning\csname stex_varseq_\l_@@_name_str _cs\endcsname\\~\\
    \prop_to_keyval:N \l_tmpa_prop
  }
  \prop_set_eq:cN {l_stex_symdecl_varseq://\l_@@_name_str _prop}\l_tmpa_prop
  
  \stex_if_do_html:T{\stex_annotate_invisible:nnn{varseq}{\l_@@_name_str}{
    \tl_if_empty:NF \l_@@_type_tl {
      \stex_annotate:nnn {type}{}{$\l_@@_type_tl$}
    }
    \stex_annotate:nnn {args}{\int_use:N \l_@@_args_int}{}
    \str_if_empty:NF \l_@@_bind_str {
      \stex_annotate:nnn {bindtype}{\l_@@_bind_str}{}
    }
    \stex_annotate:nnn{startindex}{}{$#3$}
    \stex_annotate:nnn{endindex}{}{$#4$}

    \tl_clear:N \l_tmpa_tl
    \int_step_inline:nn \l_@@_args_int {
      \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { 
        \stex_annotate:nnn{argmarker}{##1}{}
      } }
    }
    \stex_annotate_invisible:nnn { notationcomp }{}{
      \str_set:Nx \STEXInternalCurrentSymbolStr {varseq://\l_@@_name_str }
      $ \exp_args:Nno \use:nn { \use:c {
        stex_varseq_\l_@@_name_str _cs
      } } { \l_tmpa_tl } $
    }
    \stex_annotate_invisible:nnn { notationopcomp }{}{
      $ \prop_item:Nn \l_tmpa_prop { notation } $
    }

  }}

  \ignorespacesandpars
}


\keys_define:nn { stex / mmtdecl } {
  name        .str_set_x:N  = \l_stex_symdecl_name_str ,
  args        .str_set_x:N  = \l_stex_symdecl_args_str ,
  deprecate   .str_set_x:N  = \l_stex_symdecl_deprecate_str ,
  reorder     .str_set_x:N  = \l_stex_symdecl_reorder_str ,
  argnames    .clist_set:N  = \l_stex_symdecl_argnames_clist ,
  assoc       .choices:nn   = 
      {bin,binl,binr,pre,conj,pwconj}
      {\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}}
}

\cs_new_protected:Nn \_stex_mmtdecl_args:n {
  \str_clear:N \l_stex_symdecl_name_str
  \str_clear:N \l_stex_symdecl_args_str
  \str_clear:N \l_stex_symdecl_deprecate_str
  \str_clear:N \l_stex_symdecl_reorder_str
  \str_clear:N \l_stex_symdecl_assoctype_str
  \bool_set_false:N \l_stex_symdecl_local_bool
  \clist_clear:N \l_stex_symdecl_argnames_clist
  
  \keys_set:nn { stex / symdecl } { #1 }
}

\NewDocumentCommand \mmtdecl { s m O{}} {
  \_stex_mmtdecl_args:n{#3}
  \IfBooleanTF #1 {
    \bool_set_false:N \l_stex_symdecl_make_macro_bool
  } {
    \bool_set_true:N \l_stex_symdecl_make_macro_bool
  }
  \str_if_empty:NT \l_stex_symdecl_name_str {
    \str_set:Nx \l_stex_symdecl_name_str { #1 }
  }
  %\tl_set:Nx \l_stex_symdecl_definiens_tl {
  %  \stex_annotate:nnn{ OMID }{
  %    \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str 
  %  }{}
  %}
  \stex_symdecl_do:n{#2}
  \MMTrule{rules.stex.mmt.kwarc.info?SubstitutionRule}{
    \stex_annotate:nnn{ OMID }{
      \l_stex_current_module_str ? \l_stex_symdecl_name_str
    }{},
    \stex_annotate:nnn{ OMID }{
      \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str 
    }{}
  }
  \stex_smsmode_do:
}

\stex_deactivate_macro:Nn \mmtdecl {mmtinterface~environments}
\stex_deactivate_macro:Nn \mmtdef {mmtinterface~environments}

%    \end{macrocode}
%
%    \begin{macrocode}
%</package>
%    \end{macrocode}
%
% \end{implementation}
% \ifinfulldoc\else\printbibliography\fi
%
% \PrintIndex

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