% \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-Modules
% 	\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-modules} package.
% For a more high-level introduction, 
%  see \href{\basedocurl/manual.pdf}{the \sTeX Manual} or the
% \href{\basedocurl/stex.pdf}{full \sTeX documentation}.\fi
%
%
% \begin{documentation}\label{pkg:modules:doc}
%
% This sub package contains code related to Modules
%
% \ifinfulldoc\else
% \input{../../doc/packages/stex-modules}
% \fi
%
% \section{Macros and Environments}\label{pkg:modules:doc:macros}
%
% The content of a module with uri \meta{<URI>} is stored in four
% macros. All modifications of these macros are global:
% \begin{variable}{\c_stex_module_<URI>_prop}
%    A property list with the following fields:
% \begin{itemize}
%   \item[|name|] The \emph{name} of the module,
%   \item[|ns|] the \emph{namespace} in field |ns|,
%   \item[|file|] the \emph{file} containing the module, 
%       as a sequence of path fragments
%   \item[|lang|] the module's \emph{language},
%   \item[|sig|] the language of the signature module, if the
%     current file is a translation from some other language,
%   \item[|deprecate|] if this module is deprecated, the module
%     that replaces it,
%   \item[|meta|] the metatheory of the module.
% \end{itemize}
% \end{variable}
%
% \begin{variable}{\c_stex_module_<URI>_code}
%    The code to execute when this module is activated (i.e. imported),
%    e.g. to set all the semantic macros, notations, etc. 
% \end{variable}
%
% \begin{variable}{\c_stex_module_<URI>_constants}
%    The names of all constants declared in the module 
% \end{variable}
%
% \begin{variable}{\c_stex_module_<URI>_constants}
%    The full URIs of all modules imported in this module 
% \end{variable}
%
% \begin{variable}{\l_stex_current_module_str}
%   \cs{l_stex_current_module_str} always
%   contains the URI of the current module (if existent).
% \end{variable}
%
% \begin{variable}{\l_stex_all_modules_seq}
%   Stores full URIs for all modules currently in scope.
% \end{variable}
%
% \begin{function}[pTF]{\stex_if_in_module:}
%   Conditional for whether we are currently in a module
% \end{function}
%
% \begin{function}[pTF]{\stex_if_module_exists:n}
%   Conditional for whether a module with the provided URI
%   is already known.
% \end{function}
%
% \begin{function}{\stex_add_to_current_module:n,\STEXexport}
%   Adds the provided tokens to the |_code| control sequence of the
%   current module. 
%
%   \cs{stex_add_to_current_module:n} is used internally,
%   \cs{STEXexport} is intended for users and additionally executes
%   the provided code immediately.
% \end{function}
%
% \begin{function}{\stex_add_constant_to_current_module:n}
%   Adds the declaration with the provided name to the |_constants|
%   control sequence of the current module.
% \end{function}
%
% \begin{function}{\stex_add_import_to_current_module:n}
%   Adds the module with the provided full URI to the |_imports|
%   control sequence of the current module.
% \end{function}
%
% \begin{function}{\stex_collect_imports:n}
%   Iterates over all imports of the provided (full URI of a) module
%   and stores them as a topologically sorted list -- including
%   the provided module as the last element -- in
%   |\l_stex_collect_imports_seq|
% \end{function}
%
% \begin{function}{\stex_do_up_to_module:n}
%  Code that is \emph{exported} from module (such as symbol declarations)
%  should be local \emph{to the current module}. For that reason, ideally
%  all symbol declarations and similar commands should be called directly
%  in the module environment, however, that is not always feasible, e.g.
%  in structural features or |sparapraph|s. \cs{stex_do_up_to_module}
%  therefore executes the provided code repeatedly in an \cs{aftergroup}
%  up until the group level is equal to that of the innermost smodule environment. 
% \end{function}
%
% \begin{function}{\stex_modules_current_namespace:}
%   Computes the current namespace as follows:
%
%   If the current file is |.../source/sub/file.tex| in some archive
%   with namespace |http://some.namespace/foo|, then the namespace of
%   is |http://some.namespace/foo/sub/file|. Otherwise, the namespace
%   is the absolute file path of the current file (i.e. starting with |file:///|).
%
%  The result is stored in |\l_stex_module_ns_str|. Additionally, the sub path
%  relative to the current repository is stored in |\l_stex_module_subpath_str|.
% \end{function}
%
% \subsection{The \texttt{smodule} environment}
%
% \begin{environment}{module}
%   \begin{syntax} \cs{begin}|{module}[|\meta{options}|]|\Arg{name}\end{syntax}
% 
%   Opens a new module with name \meta{name}. Options are:
%   \begin{itemize}
%     \item[|title|] (\meta{token list}) to display in customizations.
%     \item[|type|] (\meta{string}$\ast$)  for use in customizations.
%     \item[|deprecate|] (\meta{module}) if set, will throw a warning
%       when loaded, urging to use \meta{module} instead.
%     \item[|id|] (\meta{string}) for cross-referencing.
%     \item[|ns|] (\meta{URI}) the namespace to use. \emph{Should not be used,
%       unless you know precisely what you're doing}. If not explicitly set, is
%       computed using \cs{stex_modules_current_namespace:}.
%     \item[|lang|] (\meta{language}) if not set, computed from the current file name (e.g. |foo.en.tex|).
%     \item[|sig|] (\meta{language}) if the current file is a translation of a file with the same base name
%       but a different language suffix, setting |sig=<lang>| will preload the module
%       from that language file. This helps ensuring that the (formal) content of both modules
%       is (almost) identical across languages and avoids duplication.
%     \item[|creators|] (\meta{string}$\ast$) names of the creators.
%     \item[|contributors|] (\meta{string}$\ast$) names of contributors.
%     \item[|srccite|] (\meta{string}) a source citation for the content of this module.
%   \end{itemize}
%
% \begin{function}{\stex_module_setup:nn}
%   \begin{syntax}\cs{stex_module_setup:nn}\Arg{params}\Arg{name}\end{syntax}
%   Sets up a new module with name \meta{name} and optional parameters
%   \meta{params}. In particular, sets
%   \cs{l_stex_current_module_str} appropriately.
% \end{function}
%
% \end{environment}
%
% \begin{function}{\stexpatchmodule}
%   \begin{syntax} \cs{stexpatchmodule} [\meta{type}] \Arg{begincode} \Arg{endcode} \end{syntax}
%   Customizes the presentation for those |smodule|-environments
%   with |type=|\meta{type}, or all others if no \meta{type} is given.
% \end{function}
%
% \begin{function}{\STEXModule}
%   \begin{syntax} \cs{STEXModule} \Arg{fragment} \end{syntax}
%   Attempts to find a module whose URI ends with \meta{fragment}
%   in the current scope and passes the full URI on to
%   \cs{stex_invoke_module:n}.
% \end{function}
%
% \begin{function}{\stex_invoke_module:n}
%   Invoked by \cs{STEXModule}. Needs to be followed either
%   by |!\macro| or |?|\Arg{symbolname}. In the first case,
%   it stores the full URI in \cs{macro}; in the second
%   case, it invokes the symbol \meta{symbolname} in the
%   selected module.
% \end{function}
%
% \begin{function}{\stex_activate_module:n}
%   Activate the module with the provided URI; i.e. executes
%   all macro code of the module's |_code|-macro (does
%   nothing if the module is already activated in the current
%   context) and adds the module to \cs{l_stex_all_modules_seq}.
% \end{function}
%
% \end{documentation}
%
% \begin{implementation}\label{pkg:modules:impl}
%
% \section{\sTeX-Modules Implementation}
%
%    \begin{macrocode}
%<*package>

%%%%%%%%%%%%%   modules.dtx   %%%%%%%%%%%%%

%<@@=stex_modules>
%    \end{macrocode}
%
% Warnings and error messages
%
%    \begin{macrocode}
\msg_new:nnn{stex}{error/unknownmodule}{
  No~module~#1~found
}
\msg_new:nnn{stex}{error/syntax}{
  Syntax~error:~#1
}
\msg_new:nnn{stex}{error/siglanguage}{
  Module~#1~declares~signature~#2,~but~does~not~
  declare~its~language
}
\msg_new:nnn{stex}{warning/deprecated}{
  #1~is~deprecated;~please~use~#2~instead!
}

\msg_new:nnn{stex}{error/conflictingmodules}{
  Conflicting~imports~for~module~#1
}
%    \end{macrocode}
%
%
% \begin{variable}{\l_stex_current_module_str}
%  The current module:
%    \begin{macrocode}
\str_new:N \l_stex_current_module_str
%    \end{macrocode}
% \end{variable}
%
% \begin{variable}{\l_stex_all_modules_seq}
%   Stores all available modules
%    \begin{macrocode}
\seq_new:N \l_stex_all_modules_seq
%    \end{macrocode}
% \end{variable}
%
% \begin{macro}[pTF]{\stex_if_in_module:}
%    \begin{macrocode}
\prg_new_conditional:Nnn \stex_if_in_module: {p, T, F, TF} {
  \str_if_empty:NTF \l_stex_current_module_str
    \prg_return_false: \prg_return_true:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}[pTF]{\stex_if_module_exists:n}
%    \begin{macrocode}
\prg_new_conditional:Nnn \stex_if_module_exists:n {p, T, F, TF} {
  \prop_if_exist:cTF { c_stex_module_#1_prop }
    \prg_return_true: \prg_return_false:
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_add_to_current_module:n,\STEXexport}
%
% Only allowed within modules:
%
%    \begin{macrocode}
\cs_new_protected:Nn \stex_execute_in_module:n { \stex_if_in_module:T {
  \stex_add_to_current_module:n { #1 }
  \stex_do_up_to_module:n { #1 }
}}
\cs_generate_variant:Nn \stex_execute_in_module:n {x}

\cs_new_protected:Nn \stex_add_to_current_module:n {
  \tl_gput_right:cn {c_stex_module_\l_stex_current_module_str _code} { #1 }
}
\cs_generate_variant:Nn \stex_add_to_current_module:n {x}
\cs_new_protected:Npn \STEXexport {
  \ExplSyntaxOn
  \_@@_export:n
}
\cs_new_protected:Nn \_@@_export:n {
  \ignorespacesandpars#1\ExplSyntaxOff
  \stex_add_to_current_module:n { \ignorespacesandpars#1}
  \stex_smsmode_do:
}
\let \stex_module_export_helper:n \use:n
\stex_deactivate_macro:Nn \STEXexport {module~environments}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_add_constant_to_current_module:n}
%    \begin{macrocode}
\cs_new_protected:Nn \stex_add_constant_to_current_module:n {
  \str_set:Nx \l_tmpa_str { #1 }
  \seq_gput_right:co {c_stex_module_\l_stex_current_module_str _constants} { \l_tmpa_str }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_add_import_to_current_module:n}
%    \begin{macrocode}
\cs_new_protected:Nn \stex_add_import_to_current_module:n {
  \str_set:Nx \l_tmpa_str { #1 }
  \exp_args:Nno
  \seq_if_in:cnF{c_stex_module_\l_stex_current_module_str _imports}\l_tmpa_str{
    \seq_gput_right:co{c_stex_module_\l_stex_current_module_str _imports}\l_tmpa_str
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_collect_imports:n}
%    \begin{macrocode}
\cs_new_protected:Nn \stex_collect_imports:n {
  \seq_clear:N \l_stex_collect_imports_seq
  \_@@_collect_imports:n {#1}
}
\cs_new_protected:Nn \_@@_collect_imports:n {
  \seq_map_inline:cn {c_stex_module_#1_imports} {
    \seq_if_in:NnF \l_stex_collect_imports_seq { ##1 } {
      \_@@_collect_imports:n { ##1 }
    }
  }
  \seq_if_in:NnF \l_stex_collect_imports_seq { #1 } {
    \seq_put_right:Nx \l_stex_collect_imports_seq { #1 }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_do_up_to_module:n}
%    \begin{macrocode}
\int_new:N \l_@@_group_depth_int
\cs_new_protected:Nn \stex_do_up_to_module:n {
  \int_compare:nNnTF \l_@@_group_depth_int = \currentgrouplevel {
    #1
  }{
    #1
    \expandafter \tl_gset:Nn 
    \csname l_@@_aftergroup_\l_stex_current_module_str _tl 
    \expandafter\expandafter\expandafter\endcsname
    \expandafter\expandafter\expandafter { \csname 
      l_@@_aftergroup_\l_stex_current_module_str _tl\endcsname #1 }
    \aftergroup\_@@_aftergroup_do:
  }
}
\cs_generate_variant:Nn \stex_do_up_to_module:n {x}
\cs_new_protected:Nn \_@@_aftergroup_do: {
  \stex_debug:nn{aftergroup}{\cs_meaning:c{
    l_@@_aftergroup_\l_stex_current_module_str _tl
  }}
  \int_compare:nNnTF \l_@@_group_depth_int = \currentgrouplevel {
    \use:c{l_@@_aftergroup_\l_stex_current_module_str _tl}
    \tl_gclear:c{l_@@_aftergroup_\l_stex_current_module_str _tl}
  }{
    \use:c{l_@@_aftergroup_\l_stex_current_module_str _tl}
    \aftergroup\_@@_aftergroup_do:
  }
}
\cs_new_protected:Nn \_stex_reset_up_to_module:n {
  \expandafter\let\csname l_@@_aftergroup_#1_tl\endcsname\undefined
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_modules_compute_namespace:nN}
% Computes the appropriate namespace from the top-level namespace
% of a repository (|#1|) and a file path
% (|#2|).
%
%
%    \begin{macrocode}

%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_modules_current_namespace:}
%
% Computes the current namespace based on the current
% MathHub repository (if existent) and the current file.
%
%    \begin{macrocode}
\str_new:N \l_stex_module_ns_str
\str_new:N \l_stex_module_subpath_str
\cs_new_protected:Nn \_@@_compute_namespace:nN {
  \seq_set_eq:NN \l_tmpa_seq #2
  % split off file extension
  \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str % <- filename
  \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str
  \seq_get_left:NN \l_tmpb_seq \l_tmpb_str % <- filename without suffixes
  \seq_put_right:No \l_tmpa_seq \l_tmpb_str % <- file path including name without suffixes

  \bool_set_true:N \l_tmpa_bool
  \bool_while_do:Nn \l_tmpa_bool {
    \seq_pop_left:NN \l_tmpa_seq \l_tmpb_str
    \exp_args:No \str_case:nnTF { \l_tmpb_str } {
      {source} { \bool_set_false:N \l_tmpa_bool }
    }{}{
      \seq_if_empty:NT \l_tmpa_seq {
        \bool_set_false:N \l_tmpa_bool
      }
    }
  }

  \stex_path_to_string:NN \l_tmpa_seq \l_stex_module_subpath_str
  % \l_tmpa_seq <- sub-path relative to archive
  \str_if_empty:NTF \l_stex_module_subpath_str {
    \str_set:Nx \l_stex_module_ns_str {#1}
  }{
    \str_set:Nx \l_stex_module_ns_str { 
      #1/\l_stex_module_subpath_str
    }
  }
}

\cs_new_protected:Nn \stex_modules_current_namespace: {
  \str_clear:N \l_stex_module_subpath_str
  \prop_if_exist:NTF \l_stex_current_repository_prop {
    \prop_get:NnN \l_stex_current_repository_prop { ns } \l_tmpa_str
    \_@@_compute_namespace:nN \l_tmpa_str \g_stex_currentfile_seq
  }{
    % split off file extension
    \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq
    \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str
    \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str
    \seq_get_left:NN \l_tmpb_seq \l_tmpb_str
    \seq_put_right:No \l_tmpa_seq \l_tmpb_str
    \str_set:Nx \l_stex_module_ns_str { 
      file:/\stex_path_to_string:N \l_tmpa_seq
    }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{The \texttt{smodule} environment}
%
% |smodule| arguments:
%
%    \begin{macrocode}
\keys_define:nn { stex / module } {
  title         .tl_set:N     = \smoduletitle ,
  type          .str_set_x:N  = \smoduletype ,
  id            .str_set_x:N  = \smoduleid ,
  deprecate     .str_set_x:N  = \l_stex_module_deprecate_str ,
  ns            .str_set_x:N  = \l_stex_module_ns_str ,
  lang          .str_set_x:N  = \l_stex_module_lang_str ,
  sig           .str_set_x:N  = \l_stex_module_sig_str ,
  creators      .str_set_x:N  = \l_stex_module_creators_str ,
  contributors  .str_set_x:N  = \l_stex_module_contributors_str ,
  meta          .str_set_x:N  = \l_stex_module_meta_str ,
  srccite       .str_set_x:N  = \l_stex_module_srccite_str
}

\cs_new_protected:Nn \_@@_args:n {
  \str_clear:N \smoduletitle
  \str_clear:N \smoduletype
  \str_clear:N \smoduleid
  \str_clear:N \l_stex_module_ns_str
  \str_clear:N \l_stex_module_deprecate_str
  \str_clear:N \l_stex_module_lang_str
  \str_clear:N \l_stex_module_sig_str
  \str_clear:N \l_stex_module_creators_str
  \str_clear:N \l_stex_module_contributors_str
  \str_clear:N \l_stex_module_meta_str
  \str_clear:N \l_stex_module_srccite_str
  \keys_set:nn { stex / module } { #1 }
}

% module parameters here? In the body?

%    \end{macrocode}
%
% \begin{macro}{\stex_module_setup:nn}
% Sets up a new module property list:
%    \begin{macrocode}
\cs_new_protected:Nn \stex_module_setup:nn {
  \int_set:Nn \l_@@_group_depth_int {\currentgrouplevel}
  \str_set:Nx \l_stex_module_name_str { #2 }
  \_@@_args:n { #1 }
%    \end{macrocode}
%
% First, we set up the name and namespace of the module.
%
% Are we in a nested module?
%
%    \begin{macrocode}
  \stex_if_in_module:TF {
    % Nested module
    \prop_get:cnN {c_stex_module_\l_stex_current_module_str _prop}
      { ns } \l_stex_module_ns_str
    \str_set:Nx \l_stex_module_name_str {
      \prop_item:cn {c_stex_module_\l_stex_current_module_str _prop}
        { name } / \l_stex_module_name_str
    }
    \str_if_empty:NT \l_stex_module_lang_str {
      \str_set:Nx \l_stex_module_lang_str {
        \prop_item:cn {c_stex_module_\l_stex_current_module_str _prop}
          { lang }
      }
    }
  }{
    % not nested:
    \str_if_empty:NT \l_stex_module_ns_str {
      \stex_modules_current_namespace:
      \exp_args:NNNo \seq_set_split:Nnn \l_tmpa_seq
          / {\l_stex_module_ns_str}
      \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str
      \str_if_eq:NNT \l_tmpa_str \l_stex_module_name_str {
        \str_set:Nx \l_stex_module_ns_str {
          \stex_path_to_string:N \l_tmpa_seq
        }
      }
    }
  }
%    \end{macrocode}
%
% Next, we determine the language of the module:
%
%    \begin{macrocode}
  \str_if_empty:NT \l_stex_module_lang_str {
    \seq_get_right:NN \g_stex_currentfile_seq \l_tmpa_str
    \seq_set_split:NnV \l_tmpa_seq . \l_tmpa_str
    \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str % .tex
    \exp_args:No \str_if_eq:nnF \l_tmpa_str {tex} {
      \exp_args:No \str_if_eq:nnF \l_tmpa_str {dtx} {
        \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq \l_tmpa_str
      }
    }
    \seq_pop_left:NN \l_tmpa_seq \l_tmpa_str % <filename>
    \seq_if_empty:NF \l_tmpa_seq { %remaining element should be [<something>.]language
      \seq_pop_right:NN \l_tmpa_seq \l_stex_module_lang_str
      \stex_debug:nn{modules} {Language~\l_stex_module_lang_str~
        inferred~from~file~name}
    }
  } 

  \stex_if_smsmode:F { \str_if_empty:NF \l_stex_module_lang_str {
    \exp_args:NNo \stex_set_language:Nn \l_tmpa_str \l_stex_module_lang_str
  }}
%    \end{macrocode}
%
% We check if we need to extend a signature module, and set
% \cs{l_stex_current_module_prop} accordingly:
%
%    \begin{macrocode}
  \str_if_empty:NTF \l_stex_module_sig_str {
    \exp_args:Nnx \prop_gset_from_keyval:cn {
      c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _prop
    } {
      name      = \l_stex_module_name_str ,
      ns        = \l_stex_module_ns_str ,
      file      = \exp_not:o { \g_stex_currentfile_seq } ,
      lang      = \l_stex_module_lang_str ,
      sig       = \l_stex_module_sig_str ,
      deprecate = \l_stex_module_deprecate_str ,
      meta      = \l_stex_module_meta_str
    }
    \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _imports}
    \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _constants}
    \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _copymodules}
    \tl_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _code}
    \str_set:Nx\l_stex_current_module_str{\l_stex_module_ns_str?\l_stex_module_name_str}
%    \end{macrocode}
%
% We load the metatheory:
%
%    \begin{macrocode}
    \str_if_empty:NT \l_stex_module_meta_str {
      \str_set:Nx \l_stex_module_meta_str {
        \c_stex_metatheory_ns_str ? Metatheory
      }
    }
    \str_if_eq:VnF \l_stex_module_meta_str {NONE} {
      \bool_set_true:N \l_stex_in_meta_bool
      \exp_args:Nx \stex_add_to_current_module:n { 
        \bool_set_true:N \l_stex_in_meta_bool
        \stex_activate_module:n {\l_stex_module_meta_str}
        \bool_set_false:N \l_stex_in_meta_bool
      }
      \stex_activate_module:n {\l_stex_module_meta_str}
      \bool_set_false:N \l_stex_in_meta_bool
    }
  }{
    \str_if_empty:NT \l_stex_module_lang_str {
      \msg_error:nnxx{stex}{error/siglanguage}{
        \l_stex_module_ns_str?\l_stex_module_name_str
      }{\l_stex_module_sig_str}
    }
    \stex_debug:nn{modules}{Signature~\l_stex_module_sig_str~for~\l_stex_module_ns_str?\l_stex_module_name_str}
    \stex_if_module_exists:nTF{\l_stex_module_ns_str?\l_stex_module_name_str}{
      \stex_debug:nn{modules}{(already exists)}
    }{
      \stex_debug:nn{modules}{(needs loading)}
      \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq
      \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str
      \seq_set_split:NnV \l_tmpb_seq . \l_tmpa_str
      \seq_pop_right:NN \l_tmpb_seq \l_tmpa_str % .tex
      \seq_pop_left:NN \l_tmpb_seq \l_tmpa_str % <filename>
      \str_set:Nx \l_tmpa_str {
        \stex_path_to_string:N \l_tmpa_seq /
        \l_tmpa_str . \l_stex_module_sig_str .tex
      }
      \IfFileExists \l_tmpa_str {
        \exp_args:No \stex_file_in_smsmode:nn { \l_tmpa_str } {
          \str_clear:N \l_stex_current_module_str
          \seq_clear:N \l_stex_all_modules_seq
          \stex_debug:nn{modules}{Loading~signature}
        }
      }{
        \msg_error:nnx{stex}{error/unknownmodule}{for~signature~\l_tmpa_str}
      }
    }
    \stex_if_smsmode:F {
      \stex_activate_module:n {
        \l_stex_module_ns_str ? \l_stex_module_name_str
      }
    }
    \str_set:Nx\l_stex_current_module_str{\l_stex_module_ns_str?\l_stex_module_name_str}
  }
  \str_if_empty:NF \l_stex_module_deprecate_str {
    \msg_warning:nnxx{stex}{warning/deprecated}{
      Module~\l_stex_current_module_str
    }{
      \l_stex_module_deprecate_str
    }
  }
  \seq_put_right:Nx \l_stex_all_modules_seq {
    \l_stex_module_ns_str ? \l_stex_module_name_str
  }
  \tl_clear:c{l_@@_aftergroup_\l_stex_module_ns_str ? \l_stex_module_name_str _tl}
}
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{smodule}
%
% The |module| environment.
%
% \begin{macro}{\_@@_begin_module:}
%
%   implements |\begin{smodule}|
%
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_begin_module: {
  \stex_reactivate_macro:N \STEXexport
  \stex_reactivate_macro:N \importmodule
  \stex_reactivate_macro:N \symdecl
  \stex_reactivate_macro:N \notation
  \stex_reactivate_macro:N \symdef

  \stex_debug:nn{modules}{
    New~module:\\
    Namespace:~\l_stex_module_ns_str\\
    Name:~\l_stex_module_name_str\\
    Language:~\l_stex_module_lang_str\\
    Signature:~\l_stex_module_sig_str\\
    Metatheory:~\l_stex_module_meta_str\\
    File:~\stex_path_to_string:N \g_stex_currentfile_seq
  }
  
  \stex_if_do_html:T{
    \begin{stex_annotate_env} {theory} {
      \l_stex_module_ns_str ? \l_stex_module_name_str
    }

    \stex_annotate_invisible:nnn{header}{} {
      \stex_annotate:nnn{language}{ \l_stex_module_lang_str }{}
      \stex_annotate:nnn{signature}{ \l_stex_module_sig_str }{}
      \str_if_eq:VnF \l_stex_module_meta_str {NONE} {
        \stex_annotate:nnn{metatheory}{ \l_stex_module_meta_str }{}
      }
      \str_if_empty:NF \smoduletype {
        \stex_annotate:nnn{type}{\smoduletype}{}
      }
    }
  }
  % TODO: Inherit metatheory for nested modules?
}
\iffalse \end{stex_annotate_env} \fi %^^A make syntax highlighting work again
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\_@@_end_module:}
%
%   implements |\end{module}|
%
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_end_module: {
  \stex_debug:nn{modules}{Closing~module~\prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} { name }}
  \_stex_reset_up_to_module:n \l_stex_current_module_str
  \stex_if_smsmode:T {
    \stex_persist:x {
      \prop_set_from_keyval:cn{c_stex_module_\l_stex_current_module_str _prop}{
        \exp_after:wN \prop_to_keyval:N \csname c_stex_module_\l_stex_current_module_str _prop\endcsname
      }
      \seq_set_from_clist:cn{c_stex_module_\l_stex_current_module_str _constants}{
        \seq_use:cn{c_stex_module_\l_stex_current_module_str _constants},
      }
      \seq_set_from_clist:cn{c_stex_module_\l_stex_current_module_str _imports}{
        \seq_use:cn{c_stex_module_\l_stex_current_module_str _imports},
      }
      \tl_set:cn {c_stex_module_\l_stex_current_module_str _code}
    }
    \exp_after:wN \let \exp_after:wN \l_tmpa_tl \csname c_stex_module_\l_stex_current_module_str _code\endcsname
    \exp_after:wN \stex_persist:n \exp_after:wN { \exp_after:wN { \l_tmpa_tl } }
  }
}
%    \end{macrocode}
% \end{macro}
%
%  The core environment
%    
%    \begin{macrocode}
\iffalse \begin{stex_annotate_env} \fi %^^A make syntax highlighting work again
\NewDocumentEnvironment { smodule } { O{} m } {
  \stex_module_setup:nn{#1}{#2}
  %\par
  \stex_if_smsmode:F{
    \tl_if_empty:NF \smoduletitle {
      \exp_args:No \stex_document_title:n \smoduletitle
    }
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \smoduletype {
      \tl_if_exist:cT {_@@_smodule_##1_start:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_smodule_##1_start:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_smodule_start:
    }{
      \l_tmpa_tl
    }
  }
  \_@@_begin_module:
  \str_if_empty:NF \smoduleid {
    \stex_ref_new_doc_target:n \smoduleid
  }
  \stex_smsmode_do:
} {
  \_@@_end_module:
  \stex_if_smsmode:F {
    \end{stex_annotate_env}
    \clist_set:No \l_tmpa_clist \smoduletype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_smodule_##1_end:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_smodule_##1_end:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_smodule_end:
    }{
      \l_tmpa_tl
    }
  }
}
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\stexpatchmodule}
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_smodule_start: {}
\cs_new_protected:Nn \_@@_smodule_end: {}

\newcommand\stexpatchmodule[3][] {
    \str_set:Nx \l_tmpa_str{ #1 }
    \str_if_empty:NTF \l_tmpa_str {
      \tl_set:Nn \_@@_smodule_start: { #2 }
      \tl_set:Nn \_@@_smodule_end: { #3 }
    }{
      \exp_after:wN \tl_set:Nn \csname _@@_smodule_#1_start:\endcsname{ #2 }
      \exp_after:wN \tl_set:Nn \csname _@@_smodule_#1_end:\endcsname{ #3 }
    }
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Invoking modules}
%
% \begin{macro}{\STEXModule,\stex_invoke_module:n}
%    \begin{macrocode}
\NewDocumentCommand \STEXModule { m } {
  \exp_args:NNx \str_set:Nn \l_tmpa_str { #1 }
  \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str }
  \tl_set:Nn \l_tmpa_tl {
    \msg_error:nnx{stex}{error/unknownmodule}{#1}
  }
  \seq_map_inline:Nn \l_stex_all_modules_seq {
    \str_set:Nn \l_tmpb_str { ##1 }
    \str_if_eq:eeT { \l_tmpa_str } {
      \str_range:Nnn \l_tmpb_str { -\l_tmpa_int } { -1 }
    } {
      \seq_map_break:n {
        \tl_set:Nn \l_tmpa_tl {
          \stex_invoke_module:n { ##1 }
        }
      }
    }
  }
  \l_tmpa_tl
}

\cs_new_protected:Nn \stex_invoke_module:n {
  \stex_debug:nn{modules}{Invoking~module~#1}
  \peek_charcode_remove:NTF ! {
    \_@@_invoke_uri:nN { #1 }
  } {
    \peek_charcode_remove:NTF ? {
      \_@@_invoke_symbol:nn { #1 }
    } {
      \msg_error:nnx{stex}{error/syntax}{
        ?~or~!~expected~after~
        \c_backslash_str STEXModule{#1}
      }
    }
  }
}

\cs_new_protected:Nn \_@@_invoke_uri:nN {
  \str_set:Nn #2 { #1 }
}

\cs_new_protected:Nn \_@@_invoke_symbol:nn {
  \stex_invoke_symbol:n{#1?#2}
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\stex_activate_module:n}
%    \begin{macrocode}
\bool_new:N \l_stex_in_meta_bool
\bool_set_false:N \l_stex_in_meta_bool
\cs_new_protected:Nn \stex_activate_module:n {
  \stex_debug:nn{modules}{Activating~module~#1}
  \exp_args:NNx \seq_if_in:NnF \l_stex_all_modules_seq { #1 } {
    \seq_put_right:Nx \l_stex_all_modules_seq { #1 }
    \use:c{ c_stex_module_#1_code }
  }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{mmtinterface}
%    \begin{macrocode}
\NewDocumentEnvironment { mmtinterface } { O{} m m } {
  \begin{smodule}[#1]{#3}
    \str_set:Nx \l_stex_module_mmtfor_str {#2}
    \MMTinclude{#2}
    \stex_reactivate_macro:N \mmtdecl
    \stex_reactivate_macro:N \mmtdef
}{
  \end{smodule}
}
%    \end{macrocode}
% \end{environment}
%
%    \begin{macrocode}
%</package>
%    \end{macrocode}
%
% \end{implementation}
% \ifinfulldoc\else\printbibliography\fi
%
% \PrintIndex
