% \iffalse meta-comment
% An Infrastructure for Semantic Macros and Module Scoping
% Copyright (C) 2004-2010 Michael Kohlhase, all rights reserved
% this file is released under the
% LaTeX Project Public License (LPPL)
%
% The development version of this file can be found at
% $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/modules/modules.dtx $
% \fi
%
% \iffalse
%\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%\ProvidesPackage{modules}[2012/01/28 v1.1 Semantic Markup]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{stex-logo,modules}
\usepackage{url,array,float,textcomp}
\usepackage[show]{ed}
\usepackage[hyperref=auto,style=alphabetic]{biblatex}
\usepackage{listings}
\usepackage{amsfonts}
\bibliography{kwarc}
\usepackage[eso-foot,today]{svninfo}
\svnInfo $Id: modules.dtx 1999 2012-01-28 07:32:11Z kohlhase $
\svnKeyword $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/modules/modules.dtx $
\usepackage{../ctansvn}
\usepackage{hyperref}
\makeindex
\floatstyle{boxed}
\newfloat{exfig}{thp}{lop}
\floatname{exfig}{Example}
\def\tracissue#1{\cite{sTeX:online}, \hyperlink{http://trac.kwarc.info/sTeX/ticket/#1}{issue #1}}
\begin{document}\DocInput{modules.dtx}\end{document}
%
% \fi
%
% \CheckSum{941}
%
% \changes{v0.9}{2005/06/14}{First Version with Documentation}
% \changes{v0.9a}{2005/07/01}{Completed Documentation}
% \changes{v0.9b}{2005/08/06}{Complete functionality and Updated Documentation}
% \changes{v0.9c}{2006/01/13}{more packaging}
% \changes{v0.9d}{2007/12/12}{fixing double loading of .tex and .sms}
% \changes{v0.9e}{2008/06/17}{fixing LaTeXML}
% \changes{v0.9f}{2008/06/17}{remove unused options uses and usesqualified}
% \changes{v0.9g}{2009/05/02}{adding resymdef functionality}
% \changes{v0.9g}{2009/08/12}{adding importOMDocmodule}
% \changes{v0.9h}{2010/01/19}{using {\texttt{\textbackslash mod@newcommand}} instead of
% {\texttt{\textbackslash providecommand}} for more intuitive inheritance.}
% \changes{v0.9h}{2010/03/05}{adding {\texttt{\textbackslash metalanguage}}}
% \changes{v1.0}{2010/06/18}{minor fixes}
% \changes{v1.1}{2010/12/30}{adding optional arguments to semantic macros for display
% variants. The resymdef functionality introduced in 0.9g is now deprecated. It was hardly
% used.}
%
% \GetFileInfo{modules.sty}
%
% \MakeShortVerb{\|}
%\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}}
% \def\xml{\scsys{Xml}}
% \def\mathml{\scsys{MathML}}
% \def\omdoc{\scsys{OMDoc}}
% \def\openmath{\scsys{OpenMath}}
% \def\latexml{\scsys{LaTeXML}}
% \def\perl{\scsys{Perl}}
% \def\cmathml{Content-{\sc MathML}\index{Content {\sc MathML}}\index{MathML@{\sc MathML}!content}}
% \def\activemath{\scsys{ActiveMath}}
% \def\twin#1#2{\index{#1!#2}\index{#2!#1}}
% \def\twintoo#1#2{{#1 #2}\twin{#1}{#2}}
% \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}}
% \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}}
% \def\cT{\mathcal{T}}\def\cD{\mathcal{D}}
% \title{{\texttt{modules.sty}}: Semantic Macros and Module Scoping in {\stex}\thanks{Version {\fileversion} (last revised
% {\filedate})}}
% \author{Michael Kohlhase \& Deyan Ginev \& Rares Ambrus\\
% Jacobs University, Bremen\\
% \url{http://kwarc.info/kohlhase}}
% \maketitle
%
% \begin{abstract}
% The |modules| package is a central 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).
%
% This package supplies a definition mechanism for semantic macros and a non-standard
% scoping construct for them, which is oriented at the semantic dependency relation
% rather than the document structure. This structure can be used by MKM systems for
% added-value services, either directly from the {\sTeX} sources, or after translation.
% \end{abstract}
%
% \newpage\setcounter{tocdepth}{2}\tableofcontents\newpage
%
% \section{Introduction}\label{sec:intro}
%
% Following general practice in the {\TeX/\LaTeX} community, we use the term ``semantic
% macro'' for a macro whose expansion stands for a mathematical object, and whose name
% (the command sequence) is inspired by the name of the mathematical object. This can
% range from simple definitions like |\def\Reals{\mathbb{R}}| for individual mathematical
% objects to more complex (functional) ones object constructors like
% |\def\SmoothFunctionsOn#1{\mathcal{C}^\infty(#1,#1)}|. Semantic macros are traditionally
% used to make {\TeX/\LaTeX} code more portable. However, the {\TeX/\LaTeX} scoping model
% (macro definitions are scoped either in the local group or until the rest of the
% document), does not mirror mathematical practice, where notations are scoped by
% mathematical environments like statements, theories, or such. For an in-depth discussion
% of semantic macros and scoping we refer the reader~\cite{Kohlhase:ulsmf08}.
%
% The |modules| package provides a {\LaTeX}-based markup infrastructure for defining
% module-scoped semantic macros and {\latexml} bindings~\cite{Miller:latexml:online} to
% create {\omdoc}~\cite{Kohlhase:omdoc1.2} from {\stex} documents. In the {\stex} world
% semantic macros have a special status, since they allow the transformation of
% {\TeX/\LaTeX} formulae into a content-oriented markup format like
% {\openmath}~\cite{BusCapCar:2oms04} and (strict) content
% {\mathml}~\cite{CarlisleEd:MathML3}; see Figure~\ref{fig:omsemmac} for an example, where
% the semantic macros above have been defined by the |\symdef| macros (see
% Section~\ref{sec:symdef}) in the scope of a |\begin{module}[id=calculus]| (see
% Section~\ref{sec:modules}).
%
% \begin{exfig}\lstset{basicstyle=\scriptsize,aboveskip=-.5em,belowskip=-1.5em}
% \begin{tabular}{l|p{9.7cm}}
% \LaTeX & \verb|\SmoothFunctionsOn\Reals| \\\hline
% PDF/DVI & ${\mathcal{C}^\infty(\mathbb{R},\mathbb{R})}$\\\hline
% {\openmath} & \lstset{morekeywords={OMA,OMS}}
% \begin{lstlisting}
%
%
%
% \end{lstlisting}\\\hline
% {\mathml} & \lstset{morekeywords={apply,csymbol}}
% \begin{lstlisting}
%
% SmoothFunctionsOn
% Reals
% \end{lstlisting}\\
% \end{tabular}
% \caption{{\openmath} and {\mathml} generated from Semantic Macros}\label{fig:omsemmac}
% \end{exfig}
%
% \section{The User Interface}
%
% The main contributions of the |modules| package are the |module| environment, which
% allows for lexical scoping of semantic macros with inheritance and the |\symdef| macro
% for declaration of semantic macros that underly the |module| scoping.
%
% \subsection{Package Options}\label{sec:options}
%
% The |modules| package takes two options: If we set \DescribeMacro{showviews}|showviews|,
% then the views (see Section~\ref{sec:user:views}) are shown. If we set the
% \DescribeMacro{qualifiedimports}|qualifiedimports| option, then qualified imports are
% enabled. Qualified imports give more flexibility in module inheritance, but consume more
% internal memory. As qualified imports are not fully implemented at the moment, they are
% turned off by default see Limitation~\ref{sec:limitations:qualified-imports}.
%
% If the \DescribeMacro{showmeta}|showmeta| is set, then the metadata keys are shown
% (see~\cite{Kohlhase:metakeys:ctan} for details and customization options).
%
% \subsection{Semantic Macros}\label{sec:symdef}
%
% The \DescribeMacro{\symdef} is the main constructor for semantic macros in {\sTeX}. A
% call to the |\symdef| macro has the general form
% \begin{quote}
% |\symdef[|\meta{keys}|]{|\meta{cseq}|}[|\meta{args}|]{|\meta{definiens}|}|
% \end{quote}
% where {\meta{cseq}} is a control sequence (the name of the semantic macro) {\meta{args}}
% is a number between 0 and 9 for the number of arguments {\meta{definiens}} is the token
% sequence used in macro expansion for {\meta{cseq}}. Finally {\meta{keys}} is a keyword
% list that further specifies the semantic status of the defined macro.
%
% The two semantic macros in Figure~\ref{fig:omsemmac} would have been declared by
% invocations of the |\symdef| macro of the form:
% \begin{verbatim}
% \symdef{Reals}{\mathbb{R}}
% \symdef{SmoothFunctionsOn}[1]{\mathcal{C}^\infty(#1,#1)}
% \end{verbatim}
%
% Note that both semantic macros correspond to {\openmath} or {\mathml} ``symbols'',
% i.e. named representations of mathematical concepts (the real numbers and the
% constructor for the space of smooth functions over a set); we call these names the
% {\textbf{symbol name}} of a semantic macro. Normally, the symbol name of a semantic
% macro declared by a |\symdef| directive is just \meta{cseq}. The key-value pair
% \DescribeMacro{name}|name=|\meta{symname} can be used to override this behavior and
% specify a differing name. There are two main use cases for this.
%
% The first one is shown in Example~\ref{fig:symvariant}, where we define semantic macros
% for the ``exclusive or'' operator. Note that we define two semantic macros: |\xorOp| and
% |\xor| for the applied form and the operator. As both relate to the same mathematical
% concept, their symbol names should be the same, so we specify |name=xor| on the
% definition of |\xorOp|.
%
% A key \DescribeMacro{local}|local| can be added to {\meta{keys}} to specify that the
% symbol is local to the module and is invisible outside. Note that even though |\symdef|
% has no advantage over |\def| for defining local semantic macros, it is still considered
% good style to use |\symdef| and |\abbrdef|, if only to make switching between local and
% exported semantic macros easier.
%
% \DescribeMacro{\abbrdef}The |\abbrdef| macro is a variant of |\symdef| that is only
% different in semantics, not in presentation. An abbreviative macro is like a semantic
% macro, and underlies the same scoping and inheritance rules, but it is just an
% abbreviation that is meant to be expanded, it does not stand for an atomic mathematical
% object.
%
% We will use a simple module for natural number arithmetics as a running example. It
% defines exponentiation and summation as new concepts while drawing on the basic
% operations like $+$ and $-$ from {\LaTeX}. In our example, we will define a semantic
% macro for summation |\Sumfromto|, which will allow us to express an expression like
% $\sum{i=1}^nx^i$ as |\Sumfromto{i}1n{2i-1}| (see Example~\ref{fig:semmodule} for an
% example). In this example we have also made use of a local semantic symbol for $n$,
% which is treated as an arbitrary (but fixed) symbol.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=arith]
% \symdef{Sumfromto}[4]{\sum_{#1=#2}^{#3}{#4}}
% \symdef[local]{arbitraryn}{n}
% What is the sum of the first $\arbitraryn$ odd numbers, i.e.
% $\Sumfromto{i}1\arbitraryn{2i-1}?$
% \end{module}
% \end{verbatim}
% \vspace*{-3.5ex}\hrule\vspace*{1ex}
% \begin{module}[id=arith]
% \symdef{Sumfromto}[4]{\sum_{#1=#2}^{#3}{#4}}
% \symdef[local]{arbitraryn}{n}
% What is the sum of the first $\arbitraryn$ odd numbers, i.e.
% $\Sumfromto{i}1\arbitraryn{2i-1}?$
% \end{module}
% \caption{Semantic Markup in a {\texttt{module}} Context}\label{fig:semmodule}
% \end{exfig}
%
% The \DescribeMacro{\symvariant}|\symvariant| macro can be used to define presentation
% variants for semantic macros previously defined via the |\symdef| directive. In an
% invocation
% \begin{quote}
% |\symdef[|\meta{keys}|]{|\meta{cseq}|}[|\meta{args}|]{|\meta{pres}|}|\\
% |\symvariant{|\meta{cseq}|}[|\meta{args}|]{|\meta{var}|}{|\meta{varpres}|}|
% \end{quote}
% the first line defines the semantic macro |\|\meta{cseq} that when applied to
% \meta{args} arguments is presented as \meta{pres}. The second line allows the semantic
% macro to be called with an optional argument \meta{var}: |\|\meta{cseq}|[var]| (applied
% to \meta{args} arguments) is then presented as \meta{varpres}. We can define a variant
% presentation for |\xor|; see Figure~\ref{fig:symvariant} for an example.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=xbool]
% \symdef[name=xor]{xorOp}{\oplus}
% \symvariant{xorOp}{uvee}{\underline{\vee}}
% \symdef{xor}[2]{#1\xorOp #2}
% \symvariant{xor}[2]{uvee}{#1\xorOp[uvee] #2}
% Exclusive disjunction is commutative: $\xor{p}q=\xor{q}p$\\
% Some authors also write exclusive or with the $\xorOp[uvee]$ operator,
% then the formula above is $\xor[uvee]{p}q=\xor[uvee]{q}p$
% \end{module}
% \end{verbatim}
% \vspace*{-3.5ex}\hrule\vspace*{1ex}
% \begin{module}[id=xbool]
% \symdef[name=xor]{xorOp}{\oplus}
% \symvariant{xorOp}{uvee}{\underline{\vee}}
% \symdef{xor}[2]{#1\xorOp #2}
% \symvariant{xor}[2]{uvee}{#1\xorOp[uvee] #2}
% Exclusive disjunction is commutative: $\xor{p}q=\xor{q}p$\\
% Some authors also write exclusive or with the $\xorOp[uvee]$ operator,
% then the formula above is $\xor[uvee]{p}q=\xor[uvee]{q}p$
% \end{module}
% \caption{Presentation Variants of a Semantic Macro}\label{fig:symvariant}
% \end{exfig}
%
% Version 1.0 of the |modules| package had the \DescribeMacro{\resymdef}|\resymdef| macro
% that allowed to locally redefine the presentation of a macro. But this did not interact
% well with the |beamer| package and was less useful than the |\symvariant|
% functionality. Therefore it is deprecated now and leads to an according error message.
%
% \subsection{Symbol and Concept Names}\label{sec:user:termdef}
%
% Just as the |\symdef| declarations define semantic macros for mathematical symbols, the
% |modules| package provides an infrastructure for {\emph{mathematical concepts}} that are
% expressed in mathematical vernacular. The key observation here is that concept names
% like ``finite symplectic group'' follow the same scoping rules as mathematical symbols,
% i.e. they are module-scoped. The \DescribeMacro{\termdef}|\termdef| macro is an analogue
% to |\symdef| that supports this: use
% |\termdef[|\meta{keys}|]{|\meta{cseq}|}{|\meta{concept}|}| to declare the macro
% |\|\meta{cseq} that expands to \meta{concept}. See Figure~\ref{fig:termref} for an
% example, where we use the \DescribeMacro{\capitalize}|\captitalize| macro to adapt
% \meta{concept} to the sentence beginning.\ednote{continue, describe \meta{keys}, they
% will have to to with plurals,\ldots once implemented}. The main use of the
% |\termdef|-defined concepts lies in automatic cross-referencing facilities via the
% \DescribeMacro{\termref}|\termref| and \DescribeMacro{\symref}|\symref| macros provided
% by the |statements| package~\ctancite{Kohlhase:smms}. Together with the |hyperref|
% package~\cite{RahObe:hmlmh10}, this provide cross-referencing to the definitions of the
% symbols and concepts. As discussed in section~\ref{sec:limitations:crossref}, the
% |\symdef| and |\termdef| declarations must be on top-level in a module, so the
% infrastructure provided in the |modules| package alone cannot be used to locate the
% definitions, so we use the infrastructure for mathematical statements for that.
%
%\begin{exfig}
% \begin{verbatim}
% \termdef[name=xor]{xdisjunction}{exclusive disjunction}
% \captitalize\xdisjunction is commutative: $\xor{p}q=\xor{q}p$
% \end{verbatim}
% \vspace*{-3.5ex}
% \caption{Extending Example~\ref{fig:symvariant} with Term References}\label{fig:termref}
% \end{exfig}
%
% \subsection{Modules and Inheritance}\label{sec:modules}
%
% The\DescribeEnv{module}|module| environment takes an optional |KeyVal|
% argument. Currently, only the |id| key is supported for specifying the identifier of a
% module (also called the {\twintoo{module}{name}}). A module introduced by
% |\begin{module}[id=foo]| restricts the scope the semantic macros defined by the
% |\symdef| form to the end of this module given by the corresponding |\end{module}|,
% and to any other |module| environments that import them by a |\importmodule{foo}|
% directive. If the module |foo| contains |\importmodule| directives of its own, these are
% also exported to the importing module.
%
% Thus the \DescribeMacro{\importmodule}|\importmodule| declarations induce the
% {\atwintoo{semantic}{inheritance}{relation}}. Figure~\ref{exf:importmodule} shows a
% module that imports the semantic macros from three others. In the simplest form,
% |\importmodule{|\meta{mod}|}| will activate the semantic macros and concepts declared by
% |\symdef| and |\termdef| in module \meta{mod} in the current module\footnote{Actually,
% in the current {\TeX} group, therefore \texttt{\textbackslash importmodule} should be
% placed directly after the \texttt{\textbackslash begin\{module\}}.}. To understand the
% mechanics of this, we need to understand a bit of the internals. The |module|
% environment sets up an internal macro pool, to which all the macros defined by the
% |\symdef| and |\termdef| declarations are added; |\importmodule| only activates this
% macro pool. Therefore |\importmodule{|\meta{mod}|}| can only work, if the {\TeX} parser
% --- which linearly goes through the {\sTeX} sources --- already came across the module
% \meta{mod}. In many situations, this is not obtainable; e.g. for ``semantic forward
% references'', where symbols or concepts are previewed or motivated to knowledgeable
% readers before they are formally introduced or for modularizations of documents into
% multiple files. To enable situations like these, the |module| package uses auxiliary
% files called {\textbf{\sTeX module signatures}}. For any file, \meta{file}|.tex|, we
% generate a corresponding \sTeX module signature \meta{file}|.sms| with the |sms| utility
% (see also Limitation~\ref{sec:limitations:sms}), which contains (copies of) all
% |\begin|/|\end{module}|, |\importmodule|, |\symdef|, and |\termdef| invocations in
% \meta{file}|.tex|. The value of an \sTeX module signature is that it can be loaded
% instead its corresponding \sTeX document, if we are only interested in the semantic
% macros. So |\importmodule[|\meta{filepath}|]{|\meta{mod}|}| will load the \sTeX module
% signature \meta{filepath}|.sms| (if it exists and has not been loaded before) and
% activate the semantic macros from module \meta{mod} (which was supposedly defined in
% \meta{filepath}|.tex|). Note that since \meta{filepath}|.sms| contains all
% |\importmodule| statements that \meta{filepath}|.tex| does, an |\importmodule|
% recursively loads all necessary files to supply the semantic macros inherited by the
% current module.
%
% The |\importmodule| macro has a variant
% \DescribeMacro{importmodulevia}|\importmodulevia| that allows the specification of a
% theory morphism to be applied. |\importmodulevia{|\meta{thyid}|}{|\meta{assignments}|}|
% specifies the ``source theory'' via its identifier \meta{thyid} and the morphism by
% \meta{assignments}. There are three kinds:
% \begin{compactdesc}
% \item[symbol assignments] via
% \DescribeMacro{\vassign}|\vassign{|\meta{sym}|}{|\meta{exp}|}|, which defines the
% symbol \meta{sym} introduced in the current theory by an expression \meta{exp} in the
% source theory.
% \item[term assignments] via
% \DescribeMacro{\tassign}|\tassign[||\meta{source-cd}]{|\meta{tname}|}{|\meta{source-tname}|}|,
% which defines the term with name \meta{tname} in the current via a term with
% name\meta{source-tname} in the theory \meta{source-cd} whose default value is the
% source theory.
% \item[term text assignments] via
% \DescribeMacro{\ttassign}|\tassign{|\meta{tname}|}{|\meta{text}|}|, which defines a
% term with name \meta{tname} in the current theory via a definitional text.
% \end{compactdesc}
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=ring]
% \begin{importmodulevia}{monoid}
% \vassign{rbase}\magbase
% \vassign{rtimesOp}\magmaop
% \vassign{rone}\monunit
% \end{importmodulevia}
% \symdef{rbase}{G}
% \symdef[name=rtimes]{rtimesOp}{\cdot}
% \symdef{rtimes}[2]{\infix\rtimesOp{#1}{#2}}
% \symdef{rone}{1}
% \begin{importmodulevia}{cgroup}
% \vassign{rplus}\magmaop
% \vassign{rzero}\monunit
% \vassign{rinvOp}\cginvOp
% \end{importmodulevia}
% \symdef[name=rplus]{rplusOp}{+}
% \symdef{rplus}[2]{\infix\rplusOp{#1}{#2}}
% \symdef[name=rminus]{rminusOp}{-}
% \symdef{rminus}[1]{\infix\rminusOp{#1}{#2}}
% ...
% \end{module}
% \end{verbatim}
% \caption{A Module for Rings with inheritance from monoids and commutative groups}\label{fig:ring}
% \end{exfig}
%
% The \DescribeMacro{\metalanguage} |metalanguage| macro is a variant of
% \lstinline|importmodule| that imports the meta language, i.e. the language in which the
% meaning of the new symbols is expressed. For mathematics this is often first-order logic
% with some set theory; see~\cite{RabKoh:WSMSML10} for discussion.
%
% \subsection{Dealing with multiple Files}\label{sec:user:multiple}
%
% The infrastructure presented above works well if we are dealing with small files or
% small collections of modules. In reality, collections of modules tend to grow, get
% re-used, etc, making it much more difficult to keep everything in one file. This general
% trend towards increasing entropy is aggravated by the fact that modules are very
% self-contained objects that are ideal for re-used. Therefore in the absence of a
% content management system for {\LaTeX} document (fragments), module collections tend to
% develop towards the ``one module one file'' rule, which leads to situations with lots
% and lots of little files.
%
% Moreover, most mathematical documents are not self-contained, i.e. they do not build up
% the theory from scratch, but pre-suppose the knowledge (and notation) from other
% documents. In this case we want to make use of the semantic macros from these
% prerequisite documents without including their text into the current document. One way
% to do this would be to have {\LaTeX} read the prerequisite documents without producing
% output. For efficiency reasons, {\stex} chooses a different route. It comes with a
% utility |sms| (see Section~\ref{sec:utilities}) that exports the modules and macros
% defined inside them from a particular document and stores them inside |.sms| files. This
% way we can avoid overloading LaTeX with useless information, while retaining the
% important information which can then be imported in a more efficient way.
%
% \DescribeMacro{\importmodule} For such situations, the |\importmodule| macro can be
% given an optional first argument that is a path to a file that contains a path to the
% module file, whose module definition (the |.sms| file) is read. Note that the
% |\importmodule| macro can be used to make module files truly self-contained. To arrive
% at a file-based content management system, it is good practice to reuse the module
% identifiers as module names and to prefix module files with corresponding
% |\importmodule| statements that pre-load the corresponding module files.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=foo]
% \importmodule[../other/bar]{bar}
% \importmodule[../mycolleaguesmodules]{baz}
% \importmodule[../other/bar]{foobar}
% ...
% \end{module}
% \end{verbatim}
% \vspace{-1.7em}
% \caption{Self-contained Modules via {\texttt{importmodule}}}\label{exf:importmodule}
% \end{exfig}
%
% In Example~\ref{exf:importmodule}, we have shown the typical setup of a module
% file. The |\importmodule| macro takes great care that files are only read once, as
% {\sTeX} allows multiple inheritance and this setup would lead to an exponential (in the
% module inheritance depth) number of file loads.
%
% Sometimes we want to import an existing {\omdoc} theory\footnote{{\omdoc} theories are
% the counterpart of {\stex} modules.} $\widehat\cT$ into (the {\omdoc} document
% $\widehat\cD$ generated from) a {\stex} document $\cD$. Naturally, we have to provide an
% {\stex} stub module $\cT$ that provides |\symdef| declarations for all symbols we use in
% $\cD$. In this situation, we use\DescribeMacro{\importOMDocmodule}
% |\importOMDocmodule[|\meta{spath}|]{|\meta{OURI}|}{|\meta{name}|}|, where \meta{spath}
% is the file system path to $\cT$ (as in |\importmodule|, this argument must not contain
% the file extension), \meta{OURI} is the URI to the {\omdoc} module (this time with
% extension), and \meta{name} is the name of the theory $\widehat\cT$ and the module in
% $\cT$ (they have to be identical for this to work). Note that since the \meta{spath}
% argument is optional, we can make ``local imports'', where the stub $\cT$ is in $\cD$
% and only contains the |\symdef|s needed there.
%
% Note that the recursive (depth-first) nature of the file loads induced by this setup is
% very natural, but can lead to problems with the depth of the file stack in the {\TeX}
% formatter (it is usually set to something like 15\footnote{If you have sufficient rights
% to change your {\TeX} installation, you can also increase the variable
% {\texttt{max\_in\_open}} in the relevant {\texttt{texmf.cnf}} file. Setting it to 50
% usually suffices}). Therefore, it may be necessary to circumvent the recursive load
% pattern providing (logically spurious) |\importmodule| commands. Consider for instance
% module |bar| in Example~\ref{exf:importmodule}, say that |bar| already has load depth
% 15, then we cannot naively import it in this way. If module |bar| depended say on a
% module |base| on the critical load path, then we could add a statement
% \DescribeMacro{\requiremodules} |\requiremodules{../base}| in the second line. This
% would load the modules from |../base.sms| in advance (uncritical, since it has load
% depth 10) without activating them, so that it would not have to be re-loaded in the
% critical path of the module |foo|. Solving the load depth problem.
%
% \DescribeMacro{\sinput} In all of the above, we do not want to load an |sms| file, if
% the corresponding file has already been loaded, since the semantic macros are already in
% memory. Therefore the |modules| package supplies a semantic variant of the |\input|
% macro, which records in an internal register that the modules in the file have already
% been loaded. Thus if we consistently use |\sinput| instead of |\input| or |\include| for
% files that contain modules\footnote{files without modules should be treated by the
% regular {\LaTeX} input mechanism, since they do not need to be registered.}, we can
% prevent double loading of files and therefore gain efficiency. The
% \DescribeMacro{\sinputref} |\sinputref| macro behaves just like |\sinput| in the
% {\LaTeX} workflow, but in the {\latexml} conversion process creates a reference to the
% transformed version of the input file instead.
%
% Finally, the separation of documents into multiple modules often profits from a symbolic
% management of file paths. To simplify this, the |modules| package supplies the
% \DescribeMacro{\defpath}|\defpath| macro: |\defpath{|\meta{cname}|}{|\meta{path}|}|
% defines a command, so that |\|\meta{csname}|{|\meta{name}|}| expands to
% \meta{path}|/|\meta{name}. So we could have used
% \begin{lstlisting}
% \defpath{OPaths}{../other}
% \importmodule[\OPhats{bar}]{bar}
% \end{lstlisting}
% instead of the second line in Example~\ref{exf:importmodule}. The variant |\OPaths| has
% the big advantage that we can get around the fact that {\TeX/\LaTeX} does not set the
% current directory in |\input|, so that we can use systematically deployed
% |\defpath|-defined path macros to make modules relocatable by defining the path macros
% locally.
%
% \subsection{Including Externally Defined Semantic Macros }
%
% In some cases, we use an existing {\LaTeX} macro package for typesetting objects that
% have a conventionalized mathematical meaning. In this case, the macros are ``semantic''
% even though they have not been defined by a |\symdef|. This is no problem, if we are
% only interested in the {\LaTeX} workflow. But if we want to e.g. transform them to
% {\omdoc} via {\latexml}, the {\latexml} bindings will need to contain references to an
% {\omdoc} theory that semantically corresponds to the {\LaTeX} package. In particular,
% this theory will have to be imported in the generated {\omdoc} file to make it
% {\omdoc}-valid.
%
% \DescribeMacro{\requirepackage} To deal with this situation, the |modules| package
% provides the |\requirepackage| macro. It takes two arguments: a package name, and a URI
% of the corresponding {\omdoc} theory. In the {\LaTeX} workflow this macro behaves like a
% |\usepackage| on the first argument, except that it can --- and should --- be used
% outside the {\LaTeX} preamble. In the {\latexml} workflow, this loads the {\latexml}
% bindings of the package specified in the first argument and generates an appropriate
% |imports| element using the URI in the second argument.
%
% \subsection{Views}\label{sec:user:views}
%
% A view is a mapping between modules, such that all model assumptions (axioms) of the
% source module are satisfied in the target module. \ednote{Document and make Examples}
%
% \section{Limitations \& Extensions}\label{sec:limitations}
%
% In this section we will discuss limitations and possible extensions of the |modules|
% package. Any contributions and extension ideas are welcome; please discuss ideas,
% requests, fixes, etc on the {\sTeX} TRAC~\cite{sTeX:online}.
%
% \subsection{Perl Utility \texttt{sms}}\label{sec:limitations:sms}
%
% Currently we have to use an external perl utility |sms| to extract \sTeX module
% signatures from \sTeX files. This considerably adds to the complexity of the \sTeX
% installation and workflow. If we can solve security setting problems that allows us to
% write to \sTeX module signatures outside the current directory, writing them from \sTeX
% may be an avenue of future development see~\cite[issue \#1522]{sTeX:online} for a
% discussion.
%
% \subsection{Qualified Imports}\label{sec:limitations:qualified-imports}
%
% In an earlier version of the \texttt{modules} package we used the \texttt{usesqualified}
% for importing macros with a disambiguating prefix (this is used whenever we have
% conflicting names for macros inherited from different modules). This is not accessible
% from the current interface. We need something like a |\importqualified| macro for this;
% see~\cite[issue \#1505]{sTeX:online}. Until this is implemented the infrastructure is
% turned off by default, but we have already introduced the
% \DescribeMacro{qualifiedimports}|qualifiedimports| option for the future.
%
% \subsection{Error Messages}\label{sec:limitations:errormsg}
%
% The error messages generated by the |modules| package are still quite bad. For instance
% if |thyA| does note exists we get the cryptic error message
% \begin{verbatim}
% ! Undefined control sequence.
% \module@defs@thyA ...hy
% \expandafter \mod@newcomma...
% l.490 ...ortmodule{thyA}
% \end{verbatim}
% This should definitely be improved.
%
% \subsection{Crossreferencing}\label{sec:limitations:crossref}
%
% Note that the macros defined by |\symdef| are still subject to the normal {\TeX} scoping
% rules. Thus they have to be at the top level of a module to be visible throughout the
% module as intended. As a consequence, the location of the |\symdef| elements cannot be
% used as targets for crossreferencing, which is currently supplied by the |statement|
% package~\ctancite{Kohlhase:smms}. A way around this limitation would be to import
% the current module from the \sTeX module signature (see Section~\ref{sec:modules}) via
% the |\importmodule| declaration.
%
% \subsection{No Forward Imports}\label{sec:limitations:forward-imports}
%
% {\sTeX} allows imports in the same file via |\importmodule{|\meta{mod}|}|, but due to
% the single-pass linear processing model of {\TeX}, \meta{mod} must be the name of a
% module declared {\emph{before}} the current point. So we cannot have forward imports as
% in
% \begin{verbatim}
% \begin{module}[id=foo]
% \importmodule{mod}
% ...
% \end{module}
% ...
% \begin{module}[id=mod]
% ...
% \end{module}
% \end{verbatim}
% a workaround, we can extract the module \meta{mod} into a file {{{mod.tex}}} and replace
% it with |\sinput{mod}|, as in
% \begin{verbatim}
% \begin{module}[id=foo]
% \importmodule[mod]{mod}
% ...
% \end{module}
% ...
% \sinput{mod}
% \end{verbatim}
% then the |\importmodule| command can read |mod.sms| (created via the |sms| utility)
% without having to wait for the module \meta{mod} to be defined.
%
% \StopEventually{\newpage\PrintIndex\newpage\PrintChanges\newpage\printbibliography}\newpage
%
% \section{The Implementation}
%
% The |modules| package generates two files: the {\LaTeX} package (all the code between
% {\textlangle\textsf{*package}\textrangle} and {\textsf{\textlangle/package\textrangle}})
% and the {\latexml} bindings (between {\textsf{\textlangle*ltxml\textrangle}} and
% {\textsf{\textlangle/ltxml\textrangle}}). We keep the corresponding code fragments
% together, since the documentation applies to both of them and to prevent them from
% getting out of sync.
%
% \subsection{Package Options}\label{sec:impl:options}
%
% We declare some switches which will modify the behavior according to the package
% options. Generally, an option |xxx| will just set the appropriate switches to true
% (otherwise they stay false).
% \begin{macrocode}
%<*package>
\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}}
\newif\ifmod@show\mod@showfalse
\DeclareOption{showmods}{\mod@showtrue}
\newif\ifmod@qualified\mod@qualifiedfalse
\DeclareOption{qualifiedimports}{\mod@qualifiedtrue}
% \end{macrocode}
% Finally, we need to declare the end of the option declaration section to {\LaTeX}.
% \begin{macrocode}
\ProcessOptions
%
% \end{macrocode}
%
% {\latexml} does not support module options yet, so we do not have to do anything here
% for the {\latexml} bindings. We only set up the {\perl} packages (and tell {\texttt{emacs}}
% about the appropriate mode for convenience
%
% The next measure is to ensure that the |sref| and |xcomment| packages are loaded (in the
% right version). For {\latexml}, we also initialize the package inclusions.
% \begin{macrocode}
%<*package>
\RequirePackage{sref}
\RequirePackage{xspace}
\RequirePackage{xcomment}
%
%<*ltxml>
# -*- CPERL -*-
package LaTeXML::Package::Pool;
use strict;
use LaTeXML::Global;
use LaTeXML::Package;
%
% \end{macrocode}
%
% \subsection{Modules and Inheritance}\label{sec:impl:modules}
%
% We define the keys for the |module| environment and the actions that are undertaken,
% when the keys are encountered.
%
% \begin{macro}{module:cd}
% This |KeyVal| key is only needed for {\latexml} at the moment; use this to specify a
% content dictionary name that is different from the module name.
% \begin{macrocode}
%<*package>
\addmetakey{module}{cd}
\addmetakey{module}{title}
%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{module:id}
% For a module with |[id=|\meta{name}|]|, we have a macro |\module@defs@|\meta{name}
% that acts as a repository for semantic macros of the current module. I will be called
% by |\importmodule| to activate them. We will add the internal forms of the semantic
% macros whenever |\symdef| is invoked. To do this, we will need an unexpended form
% |\this@module| that expands to |\module@defs@|\meta{name}; we define it first and then
% initialize |\module@defs@|\meta{name} as empty. Then we do the same for qualified
% imports as well (if the |qualifiedimports| option was specified). Furthermore, we save
% the module name in |\mod@id| and the module path in |\|\meta{name}|@cd@file@base|
% which we add to |\module@defs@|\meta{name}, so that we can use it in the importing
% module.
% \begin{macrocode}
%<*package>
\define@key{module}{id}{%
\edef\this@module{\expandafter\noexpand\csname module@defs@#1\endcsname}%
\global\@namedef{module@defs@#1}{}%
\ifmod@qualified
\edef\this@qualified@module{\expandafter\noexpand\csname module@defs@qualified@#1\endcsname}%
\global\@namedef{module@defs@qualified@#1}{}%
\fi
\def\mod@id{#1}%
\expandafter\edef\csname #1@cd@file@base\endcsname{\mod@path}%
\expandafter\g@addto@macro\csname module@defs@#1\expandafter\endcsname\expandafter%
{\expandafter\def\csname #1@cd@file@base\expandafter\endcsname\expandafter{\mod@path}}}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{module@heading}
% Then we make a convenience macro for the module heading. This can be customized.
% \begin{macrocode}
\newcounter{module}[section]
\newcommand\module@heading{\stepcounter{module}%
\noindent{\textbf{Module} \thesection.\themodule [\mod@id]}%
\sref@label@id{Module \thesection.\themodule [\mod@id]}%
\ifx\module@title\@empty :\quad\else\quad(\module@title)\hfill\\\fi}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{module@footer}
% Then we make a convenience macro for the module heading. This can be customized.
% \begin{macrocode}
\newcommand\module@footer{\noindent{\textbf{EndModule} \thesection.\themodule}}
% \end{macrocode}
% \end{macro}
%
% \begin{environment}{module}
% Finally, we define the begin module command for the module environment. All the work
% has already been done in the keyval bindings, so this is very simple.
% \begin{macrocode}
\newenvironment{module}[1][]%
{\metasetkeys{module}{#1}\ifmod@show\module@heading\fi}
{\ifmod@show\module@footer\fi}
%
% \end{macrocode}
% for the {\latexml} bindings, we have to do the work all at once.
% \begin{macrocode}
%<*ltxml>
DefKeyVal('Module','id','Semiverbatim');
DefKeyVal('Module','cd','Semiverbatim');
DefEnvironment('{module} OptionalKeyVals:Module',
"?#excluded()(#body)",
# beforeDigest=>\&useTheoryItemizations,
afterDigestBegin=>sub {
my($stomach, $whatsit)=@_;
$whatsit->setProperty(excluded=>LookupValue('excluding_modules'));
my $keys = $whatsit->getArg(1);
my($id, $cd)=$keys
&& map(ToString($keys->getValue($_)),qw(id cd));
#make sure we have an id or give a stub one otherwise:
if (not $id) {
#do magic to get a unique id for this theory
#$whatsit->setProperties(beginItemize('theory'));
#$id = ToString($whatsit->getProperty('id'));
# changed: beginItemize returns the hash returned by RefStepCounter.
# RefStepCounter deactivates any scopes for the current value of the
# counter which causes the stored prop. of the env. not to be
# visible anymore.
$id = LookupValue('stex:theory:id') || 0;
AssignValue('stex:theory:id', $id+1);
$id = "I$id";
}
$cd = $id unless $cd;
# update the catalog with paths for modules
my $module_paths = LookupValue('module_paths') || {};
$module_paths->{$id} = LookupValue('last_module_path');
AssignValue('module_paths', $module_paths, 'global');
#Update the current module position
AssignValue(current_module => $id);
AssignValue(module_cd => $cd) if $cd;
#activate the module in our current scope
$STATE->activateScope("module:".$id);
#Activate parent scope, if present
my $parentmod = LookupValue('parent_module');
use_module($parentmod) if $parentmod;
#Update the current parent module
AssignValue("parent_of_$id"=>$parentmod,'global');
AssignValue("parent_module" => $id);
return; },
afterDigest => sub {
#Move a step up on the module ancestry
AssignValue("parent_module" => LookupValue("parent_of_".LookupValue("parent_module")));
return;
});
%
% \end{macrocode}
% \end{environment}
%
%
% \begin{macro}{usemodule}
% The |use_module| subroutine performs depth-first load of definitions of the used
% modules
% \begin{macrocode}
%<*ltxml>
sub use_module {
my($module,%ancestors)=@_;
$module = ToString($module);
if (defined $ancestors{$module}) {
Fatal(":module \"$module\" leads to import cycle!");
}
$ancestors{$module}=1;
# Depth-first load definitions from used modules, disregarding cycles
foreach my $used_module (@{ LookupValue("module_${module}_uses") || []}){
use_module($used_module,%ancestors);
}
# then load definitions for this module
$STATE->activateScope("module:$module"); }#$
%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\activate@defs}
% To activate the |\symdef|s from a given module \meta{mod}, we call the macro
% |\module@defs@|\meta{mod}.
% \begin{macrocode}
%<*package>
\def\activate@defs#1{\csname module@defs@#1\endcsname}
%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\export@defs}
% To export a the |\symdef|s from the current module, we all the macros
% |\module@defs@|\meta{mod} to |\module@defs@|\meta{mod} (if the current module has a
% name and it is \meta{mod})
% \begin{macrocode}
%<*package>
\def\export@defs#1{\@ifundefined{mod@id}{}%
{\expandafter\expandafter\expandafter\g@addto@macro\expandafter%
\this@module\expandafter{\csname module@defs@#1\endcsname}}}
%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\coolurion/off}
% \ednote{@DG: this needs to be documented somewhere in section 1}
% \begin{macrocode}
%<*package>
\def\coolurion{}
\def\coolurioff{}
%
%<*ltxml>
DefMacro('\coolurion',sub {AssignValue('cooluri'=>1);});
DefMacro('\coolurioff',sub {AssignValue('cooluri'=>0);});
%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\importmodule}
% The |\importmodule[|\meta{file}|]{|\meta{mod}|}| macro is an interface macro that
% loads \meta{file} and activates and re-exports the |\symdef|s from module
% \meta{mod}. It also remembers the file name in |\mod@path|.
% \begin{macrocode}
%<*package>
\newcommand{\importmodule}[2][]{{\def\mod@path{#1}%
\ifx\mod@path\@empty\else\requiremodules{#1}\fi}%
\activate@defs{#2}\export@defs{#2}}
%
%<*ltxml>
sub omext {
my ($mod)=@_; my $dest='';
$mod = ToString($mod);
if ($mod) {
#We need a constellation of abs_path invocations
# to make sure that all symbolic links get resolved
if ($mod=~/^(\w)+:\/\//) { $dest=$mod; } else {
my ($d,$f,$t) = pathname_split(abs_path($mod));
$d = pathname_relative(abs_path($d),abs_path(cwd()));
$dest=$d."/".$f;
}
}
$dest.=".omdoc" if (ToString($mod) && !LookupValue('cooluri'));
return Tokenize($dest);}
sub importmoduleI {
my($stomach,$whatsit)=@_;
my $file = ToString($whatsit->getArg(1));
my $omdocmod = $file.".omdoc" if $file;
my $module = ToString($whatsit->getArg(2));
my $containing_module = LookupValue('current_module');
AssignValue('last_import_module',$module);
#set the relation between the current module and the one to be imported
PushValue("module_".$containing_module."_uses"=>$module) if $containing_module;
#check if we've already loaded this module file or no file path given
if((!$file) || (LookupValue('file_'.$module.'_loaded'))) {use_module($module);} #if so activate it!
else {
#if not:
my $gullet = $stomach->getGullet;
#1) mark as loaded
AssignValue('file_'.$module.'_loaded' => 1, 'global');
#open a group for its definitions so that they are localized
$stomach->bgroup;
#update the last module path
AssignValue('last_module_path', $file);
#queue the closing tag for this module in the gullet where it will be executed
#after all other definitions of the imported module have been taken care of
$gullet->unread(Invocation(T_CS('\end@requiredmodule'), Tokens(Explode($module)))->unlist);
#we only need to load the sms definitions without generating any xml output, so we set the flag to 1
AssignValue('excluding_modules' => 1);
#queue this module's sms file in the gullet so that its definitions are imported
$gullet->input($file,['sms']);
}
return;}
DefConstructor('\importmodule OptionalSemiverbatim {}',
"",
afterDigest=>sub{ importmoduleI(@_)});
%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\importmodulevia}
% The |importmodulevia| environment just calls |\importmodule|, but to get around the
% group, we first define a local macro |\@@doit|, which does that and can be called with
% an |\aftergroup| to escape the environment groupling introduced by
% |importmodulevia|. For {\latexml}, we have to\ednote{MK@DG: needs implementation}
% \begin{macrocode}
%<*package>
\newenvironment{importmodulevia}[2][]{\gdef\@@doit{\importmodule[#1]{#2}}%
\ifmod@show\par\noindent importing module #2 via \@@doit\fi}
{\aftergroup\@@doit\ifmod@show end import\fi}
%
%<*ltxml>
DefMacro('\importmodulevia OptionalSemiverbatim {}','\endgroup\importmoduleI[#1]{#2}\begin{importmoduleenv}[#1]{#2}');
DefMacroI('\end{importmodulevia}',undef,'\end{importmoduleenv}');
DefEnvironment('{importmoduleenv} OptionalSemiverbatim {}',
""
. "#body"
."");
DefConstructor('\importmoduleI OptionalSemiverbatim {}', '',
afterDigest=>sub{ importmoduleI(@_)});
%
% \end{macrocode}
% \end{macro}
%
% \begin{environment}{vassign}
% \begin{macrocode}
%<*package>
\newcommand\vassign[2]{\ifmod@show\ensuremath{#1\mapsto #2}, \fi}
%
%<*ltxml>
DefConstructor('\vassign{}{}',
""
. "#1"
. "#2"
."");
%
% \end{macrocode}
% \end{environment}
%
% \begin{environment}{tassign}
% \begin{macrocode}
%<*package>
\newcommand\tassign[3][]{\ifmod@show #2\ensuremath{\mapsto} #3, \fi}
%
%<*ltxml>
DefConstructor('\tassign[]{}{}',
""
. ""
. ""
."",
afterDigest=> sub {
my ($stomach,$whatsit) = @_;
$whatsit->setProperty('currentModule',LookupValue("current_module"));
$whatsit->setProperty('lastImportModule',LookupValue("last_import_module"));
});
%
% \end{macrocode}
% \end{environment}
%
% \begin{environment}{ttassign}
% \begin{macrocode}
%<*package>
\newcommand\ttassign[3][]{\ifmod@show #1\ensuremath{\mapsto} ``#2'', \fi}
%
%<*ltxml>
DefConstructor('\ttassign{}{}',
""
. "#1"
. "#2"
."");
%
% \end{macrocode}
% \end{environment}
%
% \begin{macro}{\importOMDocmodule}
% for the {\LaTeX} side we can just re-use |\importmodule|, for the {\latexml} side we
% have a full URI anyways. So things are easy.
% \begin{macrocode}
%<*package>
\newcommand{\importOMDocmodule}[3][]{\importmodule[#1]{#3}}
%
%<*ltxml>
DefConstructor('\importOMDocmodule OptionalSemiverbatim {}{}',"",
afterDigest=>sub{
#Same as \importmodule, just switch second and third argument.
my ($stomach,$whatsit) = @_;
my $path = $whatsit->getArg(1);
my $ouri = $whatsit->getArg(2);
my $module = $whatsit->getArg(3);
$whatsit->setArgs(($path, $module,$ouri));
importmoduleI($stomach,$whatsit);
return;
});
%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\metalanguage}
% |\metalanguage| behaves exactly like |\importmodule| for formatting. For {\latexml},
% we only add the |type| attribute.
% \begin{macrocode}
%<*package>
\let\metalanguage=\importmodule
%
%<*ltxml>
DefConstructor('\metalanguage OptionalSemiverbatim {}',
"",
afterDigest=>sub{ importmoduleI(@_)});
%
% \end{macrocode}
% \end{macro}
%
% \subsection{Semantic Macros}\label{sec:impl:symdef}
%
% \begin{macro}{\mod@newcommand}
% We first hack the {\LaTeX} kernel macros to obtain a version of the |\newcommand|
% macro that does not check for definedness. This is just a copy of the code from
% |latex.ltx| where I have removed the |\@ifdefinable| check.\footnote{Someone must have
% done this before, I would be very happy to hear about a package that provides this.}
% \begin{macrocode}
%<*package>
\def\mod@newcommand{\@star@or@long\mod@new@command}
\def\mod@new@command#1{\@testopt{\@mod@newcommand#1}0}
\def\@mod@newcommand#1[#2]{\kernel@ifnextchar [{\mod@xargdef#1[#2]}{\mod@argdef#1[#2]}}
\long\def\mod@argdef#1[#2]#3{\@yargdef#1\@ne{#2}{#3}}
\long\def\mod@xargdef#1[#2][#3]#4{\expandafter\def\expandafter#1\expandafter{%
\expandafter\@protected@testopt\expandafter #1\csname\string#1\endcsname{#3}}%
\expandafter\@yargdef\csname\string#1\endcsname\tw@{#2}{#4}}
%
% \end{macrocode}
% \end{macro}
%
% Now we define the optional KeyVal arguments for the |\symdef| form and the actions that
% are taken when they are encountered.
%
% \begin{macro}{symdef:keys}
% The optional argument local specifies the scope of the function to be defined. If
% local is not present as an optional argument then |\symdef| assumes the scope of the
% function is global and it will include it in the pool of macros of the current
% module. Otherwise, if local is present then the function will be defined only locally
% and it will not be added to the current module (i.e. we cannot inherit a local
% function). Note, the optional key local does not need a value: we write
% |\symdef[local]{somefunction}[0]{some expansion}|. The other keys are not used in the
% {\LaTeX} part.
% \begin{macrocode}
%<*package>
\newif\if@symdeflocal
\define@key{symdef}{local}[true]{\@symdeflocaltrue}
\define@key{symdef}{name}{}
\define@key{symdef}{assocarg}{}
\define@key{symdef}{bvars}{}
\define@key{symdef}{bvar}{}
\define@key{symdef}{bindargs}{}
%
% \end{macrocode}
% \end{macro}
% \ednote{MK@MK: we need to document the binder keys above.}
% \begin{macro}{\symdef}
% The the |\symdef|, and |\@symdef| macros just handle optional arguments.
% \begin{macrocode}
%<*package>
\def\symdef{\@ifnextchar[{\@symdef}{\@symdef[]}}
\def\@symdef[#1]#2{\@ifnextchar[{\@@symdef[#1]{#2}}{\@@symdef[#1]{#2}[0]}}
% \end{macrocode}
% next we locally abbreviate |\mod@newcommand| to simplify argument passing.
% \begin{macrocode}
\def\@mod@nc#1{\mod@newcommand{#1}[1]}
% \end{macrocode}
% now comes the real meat: the |\@@symdef| macro does two things, it adds the macro
% definition to the macro definition pool of the current module and also provides it.
% \begin{macrocode}
\def\@@symdef[#1]#2[#3]#4{%
% \end{macrocode}
% We use a switch to keep track of the local optional argument. We initialize the switch
% to false and set all the keys that have been provided as arguments: |name|, |local|.
% \begin{macrocode}
\@symdeflocalfalse\setkeys{symdef}{#1}%
% \end{macrocode}
% First, using |\mod@newcommand| we initialize the intermediate macro
% |\module@|\meta{sym}|@pres@|, the one that can be extended with |\symvariant|
% \begin{macrocode}
\expandafter\mod@newcommand\csname modules@#2@pres@\endcsname[#3]{#4}%
% \end{macrocode}
% and then we define the actual semantic macro. Note that this can take an optional
% argument, for which we provide with |\@ifnextchar| and an internal macro |\@|\meta{sym},
% which when invoked with an optional argument \meta{opt} calls
% |\modules@|\meta{sym}|@pres@|\meta{opt}.
% \begin{macrocode}
\expandafter\def\csname #2\endcsname%
{\@ifnextchar[{\csname modules@#2\endcsname}{\csname modules@#2\endcsname[]}}%
\expandafter\def\csname modules@#2\endcsname[##1]%
{\csname modules@#2@pres@##1\endcsname}%
% \end{macrocode}
% Finally, we prepare the internal macro to be used in the |\symref| call.
% \begin{macrocode}
\expandafter\@mod@nc\csname mod@symref@#2\expandafter\endcsname\expandafter%
{\expandafter\mod@termref\expandafter{\mod@id}{#2}{##1}}%
% \end{macrocode}
% We check if the switch for the local scope is set: if it is we are done, since this
% function has a local scope. Similarly, if we are not inside a module, which we could
% export from.
% \begin{macrocode}
\if@symdeflocal\else%
\@ifundefined{mod@id}{}{%
% \end{macrocode}
% Otherwise, we add three functions to the module's pool of defined macros using
% |\g@addto@macro|. We first add the definition of the intermediate function
% |\modules@|\meta{sym}|@pres@|.
% \begin{macrocode}
\expandafter\g@addto@macro\this@module%
{\expandafter\mod@newcommand\csname modules@#2@pres@\endcsname[#3]{#4}}%
% \end{macrocode}
% Then we add add the definition of |\|\meta{sym} in terms of the function |\@|\meta{sym}
% to handle the optional argument.
% \begin{macrocode}
\expandafter\g@addto@macro\this@module%
{\expandafter\def\csname#2\endcsname%
{\@ifnextchar[{\csname modules@#2\endcsname}{\csname modules@#2\endcsname[]}}}%
% \end{macrocode}
% Finally, we add add the definition of |\@|\meta{sym}, which calls the intermediate
% function.
% \begin{macrocode}
\expandafter\g@addto@macro\this@module%
{\expandafter\def\csname modules@#2\endcsname[##1]%
{\csname modules@#2@pres@##1\endcsname}}%
% \end{macrocode}
% We also add |\mod@symref@|\meta{sym} macro to the macro pool so that the |\symref| macro
% can pick it up.
% \begin{macrocode}
\expandafter\g@addto@macro\csname module@defs@\mod@id\expandafter\endcsname\expandafter%
{\expandafter\@mod@nc\csname mod@symref@#2\expandafter\endcsname\expandafter%
{\expandafter\mod@termref\expandafter{\mod@id}{#2}{##1}}}%
% \end{macrocode}
% Finally, using |\g@addto@macro| we add the two functions to the qualified version of the
% module if the |qualifiedimports| option was set.
% \begin{macrocode}
\ifmod@qualified%
\expandafter\g@addto@macro\this@qualified@module%
{\expandafter\mod@newcommand\csname modules@#2@pres@qualified\endcsname[#3]{#4}}%
\expandafter\g@addto@macro\this@qualified@module%
{\expandafter\def\csname#2atqualified\endcsname{\csname modules@#2@pres@qualified\endcsname}}%
\fi%
% \end{macrocode}
% So now we only need to close all brackets and the macro is done.
% \begin{macrocode}
}\fi}
%
% \end{macrocode}
% In the {\latexml} bindings, we have a top-level macro that delegates the work to two
% internal macros: |\@symdef|, which defines the content macro and |\@symdef@pres|, which
% generates the {\omdoc} |symbol| and |presentation| elements (see
% Section~\ref{sec:impl:presentation}).
% \begin{macrocode}
%<*package>
\define@key{DefMathOp}{name}{\def\defmathop@name{#1}}
\newcommand\DefMathOp[2][]{%
\setkeys{DefMathOp}{#1}%
\symdef[#1]{\defmathop@name}{#2}}
%
%<*ltxml>
DefMacro('\DefMathOp OptionalKeyVals:symdef {}',
sub {
my($self,$keyval,$pres)=@_;
my $name = KeyVal($keyval,'name') if $keyval;
#Rewrite this token
my $scopes = $STATE->getActiveScopes;
DefMathRewrite(xpath=>'descendant-or-self::ltx:XMath',match=>ToString($pres),
replace=>sub{
map {$STATE->activateScope($_);} @$scopes;
$_[0]->absorb(Digest("\\".ToString($name)));
});
#Invoke symdef
(Invocation(T_CS('\symdef'),$keyval,$name,undef,$pres)->unlist);
});
DefMacro('\symdef OptionalKeyVals:symdef {}[]{}',
sub {
my($self,@args)=@_;
((Invocation(T_CS('\@symdef'),@args)->unlist),
(LookupValue('excluding_modules') ? ()
: (Invocation(T_CS('\@symdef@pres'), @args)->unlist))); });
#Current list of recognized formatter command sequences:
our @PresFormatters = qw (infix prefix postfix assoc mixfixi mixfixa mixfixii mixfixia mixfixai mixfixaii mixfixiii);
DefPrimitive('\@symdef OptionalKeyVals:symdef {}[]{}', sub {
my($stomach,$keys,$cs,$nargs,$presentation)=@_;
my($name,$cd,$role,$bvars,$bvar)=$keys
&& map($_ && $_->toString,map($keys->getValue($_), qw(name cd role
bvars bvar)));
$cd = LookupValue('module_cd') unless $cd;
$name = $cs unless $name;
#Store for later lookup
AssignValue("symdef.".ToString($cs).".cd"=>ToString($cd),'global');
AssignValue("symdef.".ToString($cs).".name"=>ToString($name),'global');
$nargs = (ref $nargs ? $nargs->toString : $nargs || 0);
my $module = LookupValue('current_module');
my $scope = (($keys && ($keys->getValue('local') || '' eq 'true')) ? 'module_local' : 'module').":".$module;
#The DefConstructorI Factory is responsible for creating the \symbol command sequences as dictated by the \symdef
DefConstructorI("\\".$cs->toString,convertLaTeXArgs($nargs+1,'default'), sub {
my ($document,@args) = @_;
my $icvariant = shift @args;
my @props = @args;
#Lookup the presentation from the State, if a variant:
@args = splice(@props,0,$nargs);
my %prs = @props;
my $localpres = $prs{presentation};
$prs{isbound} = "BINDER" if ($bvars || $bvar);
my $wrapped;
my $parent=$document->getNode;
if(! defined $parent->lookupNamespacePrefix("http://omdoc.org/ns")){ # namespace not already declared?
$document->getDocument->documentElement->setNamespace("http://omdoc.org/ns","omdoc",0); }
my $symdef_scope=$parent->exists('ancestor::omdoc:rendering'); #Are we in a \symdef rendering?
if (($localpres =~/^LaTeXML::Token/) && $symdef_scope) {
#Note: We should probably ask Bruce whether this maneuver makes sense
# We jump back to digestion, at a processing stage where it has been already completed
# Hence need to reinitialize all scopes and make a new group. This is probably expensive to do.
my @toks = $localpres->unlist;
while(@toks && $toks[0]->equals(T_SPACE)){ shift(@toks); } # Remove leading space
my $formatters = join("|",@PresFormatters);
$formatters = qr/$formatters/;
$wrapped = (@toks && ($toks[0]->toString =~ /^\\($formatters)$/));
$localpres = Invocation(T_CS('\@use'),$localpres) unless $wrapped;
# Plug in the provided arguments, doing a nasty reversion:
my @sargs = map (Tokens($_->revert), @args);
$localpres = Tokens(LaTeXML::Expandable::substituteTokens($localpres,@sargs)) if $nargs>0;
#Digest:
my $stomach = $STATE->getStomach;
$stomach->beginMode('inline-math');
$STATE->activateScope($scope);
use_module($module);
use_module(LookupValue("parent_of_".$module)) if LookupValue("parent_of_".$module);
$localpres=$stomach->digest($localpres);
$stomach->endMode('inline-math');
}
else { #Some are already digested to Whatsit, usually when dropped from a wrapping constructor
}
if ($nargs == 0) {
if (!$symdef_scope) { #Simple case - discourse flow, only a single XMTok
#Referencing XMTok when not in \symdefs:
$document->insertElement('ltx:XMTok',undef,(name=>$cs->toString, meaning=>$name,omcd=>$cd,role => $role,scriptpos=>$prs{'scriptpos'}));
}
else {
if ($symdef_scope && ($localpres =~/^LaTeXML::Whatsit/) && (!$wrapped)) {#1. Simple case: converts to a single token
$localpres->setProperties((name=>$cs->toString, meaning=>$name,omcd=>$cd,role => $role,scriptpos=>$prs{'scriptpos'}));
}
else {
#Experimental treatment - COMPLEXTOKEN
#$role=$role||'COMPLEXTOKEN';
#$document->openElement('ltx:XMApp',role=>'COMPLEXTOKEN');
#$document->insertElement('ltx:XMTok',undef,(name=>$cs->toString, meaning=>$name, omcd=>$cd, role=>$role, scriptpos=>$prs{'scriptpos'}));
#$document->openElement('ltx:XMWrap');
#$document->absorb($localpres);
#$document->closeElement('ltx:XMWrap');
#$document->closeElement('ltx:XMApp');
}
#We need expanded presentation when invoked in \symdef scope:
#Suppress errors from rendering attributes when absorbing.
#This is bad style, but we have no way around it due to the digestion acrobatics.
my $verbosity = $LaTeXML::Global::STATE->lookupValue('VERBOSITY');
my $errors = $LaTeXML::Global::STATE->getStatus('error');
$LaTeXML::Global::STATE->assignValue('VERBOSITY',-5);
#Absorb presentation:
$document->absorb($localpres);
#Return to original verbosity and error state:
$LaTeXML::Global::STATE->assignValue('VERBOSITY',$verbosity);
$LaTeXML::Global::STATE->setStatus('error',$errors);
#Strip all/any