diff options
Diffstat (limited to 'Master/texmf-dist/doc/latex/stex/stex-manual.tex')
-rw-r--r-- | Master/texmf-dist/doc/latex/stex/stex-manual.tex | 829 |
1 files changed, 829 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/stex-manual.tex b/Master/texmf-dist/doc/latex/stex/stex-manual.tex new file mode 100644 index 00000000000..92834af1c5e --- /dev/null +++ b/Master/texmf-dist/doc/latex/stex/stex-manual.tex @@ -0,0 +1,829 @@ +\makeatletter +\ifcsname if@infulldoc\endcsname\else + \expandafter\newif\csname if@infulldoc\endcsname\@infulldocfalse +\fi +\makeatother + +\csname if@infulldoc\endcsname\else + +\def\bibfolder{../lib/bib} + +\input{stex-docheader} + +\infulldoctrue + +\csname bool_set_true:N\expandafter\endcsname\csname stex_dtx_tests_bool\endcsname + +\begin{document} + \csname if@infulldoc\endcsname\else + \title{ + The {\stex{3}} Manual + \thanks{Version {\fileversion} (last revised {\filedate})} + } + \author{Michael Kohlhase, Dennis Müller\\ + FAU Erlangen-Nürnberg\\ + \url{http://kwarc.info/} + } + \pagenumbering{roman} + \maketitle + + \input{stex-abstract}\bigskip + + This is the user manual for the \sTeX package and + associated software. It is primarily directed at end-users + who want to use \sTeX to author semantically + enriched documents. For the full documentation, see + \href{\basedocurl/stex.pdf}{the \sTeX documentation} + + \makeatletter + \renewcommand\part{% + \clearpage + \thispagestyle{plain}% + \@tempswafalse + \null\vfil + \secdef\@part\@spart% + } + \newcounter{chapter} + \numberwithin{section}{chapter} + \renewcommand\thechapter{\@arabic\c@chapter} + \renewcommand\thesection{\thechapter.\@arabic\c@section} + \newcommand*\chaptermark[1]{} + \setcounter{secnumdepth}{2} + \newcommand\@chapapp{\chaptername} + %\newcommand\chaptername{Chapter} + \def\ps@headings{% + \let\@oddfoot\@empty + \def\@oddhead{{\slshape\rightmark}\hfil\thepage}% + \let\@mkboth\markboth + \def\chaptermark##1{% + \markright{\MakeUppercase{% + \ifnum \c@secnumdepth >\m@ne + \@chapapp\ \thechapter. \ % + \fi + ##1}}% + }% + } + \newcommand\chapter{\clearpage + \thispagestyle{plain}% + \global\@topnum\z@ + \@afterindentfalse + \secdef\@chapter\@schapter% + } + \def\@chapter[#1]#2{\refstepcounter{chapter}% + \typeout{\@chapapp\space\thechapter.}% + \addcontentsline{toc}{chapter}% + {\protect\numberline{\thechapter}#1}% + \chaptermark{#1}% + \addtocontents{lof}{\protect\addvspace{10\p@}}% + \addtocontents{lot}{\protect\addvspace{10\p@}}% + \@makechapterhead{#2}% + \@afterheading% + } + \def\@makechapterhead#1{% + \vspace*{50\p@}% + {\parindent \z@ \raggedright \normalfont + \huge\bfseries \@chapapp\space \thechapter + \par\nobreak + \vskip 20\p@ + \interlinepenalty\@M + \Huge \bfseries #1\par\nobreak + \vskip 40\p@ + }% + } +\newcommand*\l@chapter[2]{% + \ifnum \c@tocdepth >\m@ne + \addpenalty{-\@highpenalty}% + \vskip 1.0em \@plus\p@ + \setlength\@tempdima{1.5em}% + \begingroup + \parindent \z@ \rightskip \@pnumwidth + \parfillskip -\@pnumwidth + \leavevmode \bfseries + \advance\leftskip\@tempdima + \hskip -\leftskip + #1\nobreak\hfil + \nobreak\hb@xt@\@pnumwidth{\hss #2% + \kern-\p@\kern\p@}\par + \penalty\@highpenalty + \endgroup + \fi} +\renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.8em}} +\renewcommand*\l@subsection{\@dottedtocline{2}{3.8em}{3.2em}} +\renewcommand*\l@subsubsection{\@dottedtocline{3}{7.0em}{4.1em}} +\def\partname{Part} +\def\toclevel@part{-1} +\def\maketitle{\chapter{\@title}} +\let\thanks\@gobble +\let\DelayPrintIndex\PrintIndex +\let\PrintIndex\@empty +\providecommand*{\hexnum}[1]{\text{\texttt{\char`\"}#1}} +\makeatother + +\ExplSyntaxOn +\int_set:Nn \l_document_structure_section_level_int {1} +\ExplSyntaxOff + +\clearpage + +{% + \def\\{:}% fix "newlines" in the ToC + \tableofcontents +} + +\clearpage +\pagenumbering{arabic} + +\fi + +\long\def\ignore#1{} + +\begin{sfragment}{What is \sTeX?} + +Formal systems for mathematics (such as interactive theorem provers) +have the potential to significantly increase both the accessibility +of published knowledge, as well as the confidence in its veracity, +by rendering the precise semantics of statements machine actionable. +This allows for a plurality of added-value services, from semantic +search up to verification and automated theorem proving. +Unfortunately, their usefulness is hidden behind severe barriers +to accessibility; primarily related to their surface languages +reminiscent of programming languages and very unlike informal +standards of presentation. + +\sTeX minimizes this gap between informal and formal +mathematics by integrating formal methods into established +and widespread authoring workflows, primarily \LaTeX, via +non-intrusive semantic +annotations of arbitrary informal document fragments. That way +formal knowledge management services become available for informal +documents, accessible via an IDE for authors and via generated +\emph{active} documents for readers, while remaining fully compatible +with existing authoring workflows and publishing systems. + +Additionally, an extensible library of reusable +document fragments is being developed, that serve as reference targets +for global disambiguation, intermediaries for content exchange +between systems and other services. + +Every component of the system is designed modularly and extensibly, +and thus lay the groundwork for a potential full integration of +interactive theorem proving systems into established informal document +authoring workflows. + +\paragraph{} The general \sTeX workflow combines functionalities +provided by several pieces of software: +\begin{itemize} + \item The \sTeX package to use semantic annotations in + {\LaTeX} documents, + \item \RusTeX to convert |tex| sources to (semantically enriched) + |xhtml|, + \item The \mmt software, that extracts semantic information + from the thus generated |xhtml| and provides semantically informed + added value services. +\end{itemize} + + +% ---------------------------- + +\ignore{The objectives of this project will be achieved by developing a +language and system +that uses non-intrusive annotations +to augment informal documents with semantic information +(ranging from \textbf{fully formal} to \textbf{purely informal}) + without +impacting linguistic presentation or document layout. +That way, the system +remains compatible with established publishing +pipelines and practices, while additionally providing flexiformal +information that +enables formal knowledge management services, and hence produces +\emph{rich active documents}, satisfying \textbf{R3}, \textbf{R4} and +\textbf{R5}. +In particular, it will avoid commitment to a fixed logical foundation. +Instead, it will be designed as a modular pipeline of consecutive +and compositional +annotations, semantics extraction and translation steps, extensible +via new structuring mechanisms (\textbf{R1}), library content +(\textbf{R2}), +NLP techniques, foundations, translation methods and +end-user services. + +Naturally, the benefits of formal knowledge management services scale +with the amount of mathematics involved. Consequently I will primarily +focus on those +STEM fields in which mathematical methods are most prominently +used (e.g. mathematics, physics, computer science). Since in those fields +\LaTeX~is the most commonly used scientific writing tool, I will also +primarily focus on \LaTeX~as a development and evaluation target, but +the system will be designed such that all components apart from +the surface language will be integrable with other writing tools +(e.g. WYSIWYG word processors). + +\paragraph{} The basic architecture of the proposed system is sketched in +\autoref{fig:architecture}. +\begin{figure}\centering + \resizebox{0.95\textwidth}{!}{\tikzinput[]{diagram}} + {\small (Note, that the syntax used + in the box on the top right is prototypical and subject to change during the project. + Details and open questions regarding the syntax are discussed here: + \url{https://github.com/KWARC/FoMID/issues/1})} + \caption{Basic Architecture of the Proposed System}\label{fig:architecture} +\end{figure} +A user can write their content using standard \LaTeX\ in an IDE; +ideally using semantic annotations provided by \sTeX +%and the library developed in \OBJref{smglom} +(as in the upper right of +\autoref{fig:architecture}), but not necessarily so. + +The document is converted to xhtml with \omdoc annotations +using \LaTeX ML in the background, +thus becoming actionable by the \mmt system. Both the source document +as well as the generated xhtml/\omdoc are accessible to a natural language +processing pripeline that can supply additional inferred semantic +information or suggest annotations to the user, in the latter case +augmenting the source document directly. This pipeline can use both +classical NLP techniques using the GLIF system, as well as machine +learning models such as \cite{own:fifom}. + +A semiformal fragment is converted +into an appropriate syntax tree (possibly containing opaque +informal nodes), +thus becoming amenable +to flexiformal knowledge management services. In a consecutive step +-- if sufficiently annotated --, these are +additionally translated +to a fully formal foundation, e.g. using the techniques from +\cite{DMueller:phd:19,own:translations}, allowing +more powerful services and conversion to established formal +systems. All three representations +are thus available from within the \mmt system for various +knowledge management services, interfaces for which can be +implemented in the IDE. + +Importantly, every non-trivial arrow in the figure is +composable and extensible -- +translations to a foundation can be provided +by supplying an appropriate formalization and alignment-based +translations (or entirely new methods), +services can be implemented generically using the \mmt API, +NLP techniques can be implemented both inside and alongside of +GLIF, and the concrete syntax within \sTeX can be extended +by convenience macros in \LaTeX\ (enabling new +structuring mechanisms as in \textbf{R1} via +\mmt extensions, see +\cite{MueRabRot:rslffml20}) as well as via additions to +the library, which will be extensible both from within the IDE +as well as on MathHub, +remaining backwards compatible with existing content in a surface +language. Additionally, sufficiently disambiguated +statements can be translated to the syntax of +external systems (such as interactive theorem prover systems +or computer algebra systems), +which can thus be integrated as additional services into the system. +} + +\end{sfragment} + +\begin{sfragment}{Quickstart} + + \begin{sfragment}{Setup} + \begin{sfragment}{The \sTeX IDE} + TODO: VSCode Plugin + \end{sfragment} + \begin{sfragment}{Manual Setup} + Foregoing on the \sTeX IDE, we will need several + pieces of software; namely: + \begin{itemize} + \item \textbf{The \sTeX-Package} available + \href{https://github.com/slatex/sTeX/blob/latex3/doc/stex.pdf}{here}% + \ednote{For now, we require the \texttt{latex3}-branch}. + Note, that the CTAN repository for \LaTeX{} packages + may contain outdated versions of the \sTeX package, so + make sure, that your |TEXMF| system variable is configured such + that the packages available in the linked repository are prioritized + over potential default packages that come with your \TeX{} distribution. + + %If you are only interested in using semantic macros in (ultimately) + %|pdf|s generated by |pdflatex|, this is all you need. + + \item \textbf{The \mmt System} available + \href{https://github.com/uniformal/MMT/tree/sTeX}{here}% + \ednote{For now, we require the \texttt{sTeX}-branch, requiring manually + compiling the MMT sources}. We recommend following + the setup routine documented + \href{https://uniformal.github.io//doc/setup/}{here}. + + Following the setup routine (Step 3) will entail designating + a |MathHub|-directory on your local file system, where + the \mmt system will look for \sTeX/\mmt content archives. + + \item To make sure that \sTeX too knows where to find its + archives, we need to set a global system variable |MATHHUB|, + that points to your local |MathHub|-directory + (see \sref{sec.stexarchives}). + \item \textbf{\sTeX Archives} If we only care about {\LaTeX} and generating |pdf|s, we do not + technically need \mmt at all; however, we still need the |MATHHUB| + system variable to be set. Furthermore, \mmt can make downloading + content archives we might want to use significantly easier, since + it makes sure that all dependencies of (often highly interrelated) + \sTeX archives are cloned as well. + + Once set up, we can run |mmt| in a shell and download an archive along with + all of its dependencies like this: |lmh install <name-of-repository>|, + or a whole \emph{group} of archives; for example, + |lmh install smglom| will download all smglom archives. + \item \textbf{\RusTeX} The \mmt system will also set up \RusTeX for you, + which is used to generate (semantically annotated) + |xhtml| from tex sources. In lieu of using \mmt, you + can also download and use \RusTeX directly + \href{https://github.com/slatex/RusTeX}{here}. + + \end{itemize} + \end{sfragment} + \end{sfragment} + \begin{sfragment}{A First \sTeX Document} + Having set everything up, we can write a first + \sTeX document. As an example, we will use the + |smglom/calculus| and |smglom/arithmetics| archives, + which should be present in the designated |MathHub|-folder. + + The document we will consider is the following: + \begin{framed}\begin{latexcode} +\documentclass{article} +\usepackage{stex} +\usepackage{xcolor} +\def\compemph#1{\textcolor{blue}{#1}} + +\begin{document} + \usemodule[smglom/calculus]{series} + \usemodule[smglom/arithmetics]{realarith} + + The \symref{series}{series} $\infinitesum{n}{1}{ + \realdivide[frac]{1}{ + \realpower{2}{n} + } + }$ \symref{converges}{converges} towards $1$. + +\end{document} + \end{latexcode}\end{framed} + + Compiling this document with |pdflatex| should yield + the output + + \begin{framed} + The \textbf{series} + $\textcolor{blue}{\sum}_{n=1}^{\textcolor{blue}\infty} \frac{1}{2^n}$ + \textbf{converges} towards $1$. + \end{framed} + + Note that the $\sum$ and $\infty$-symbols are highlighted in blue, + and the words ``series'' and ``converges'' in bold. + This signifies that these words and symbols + reference \sTeX \emph{symbols} + formally declared somewhere; associating their + \emph{presentation} in the document with their (formal) + definition - i.e. their semantics. The precise way + in which they are highlighted (if at all) can of course + be customized (see \ednote{somewhere later}). + + \begin{function}{\usemodule} + The command |\usemodule[some/archive]{modulename}| + finds some module in the appropriate archive -- in the first + case (|\usemodule[smglom/calculus]{series}|), \sTeX + looks for the archive |smglom/calculus| in our local + MathHub-directory (see \sref{sec.stexarchives}), and + in its source-folder for a file |series.tex|. Since no such + file exists, and by default the document is assumed to be + in \emph{english}, it picks the file |series.en.tex|, and + indeed, in here we find a statement |\begin{smodule}{series}|. + \iffalse\end{smodule}\fi + + \sTeX now reads this file and makes all semantic macros therein + available to use, along with all its dependencies. + This enables the usage of |\infinitesum| later on. + + Analogously, |\usemodule[smglom/arithmetics]{realarith}| + opens the file |realarith.en.tex| in the |.../smglom/arithmetics/source|-folder + and makes its contents available, e.g. |\realdivide| and |\realpower|. + \end{function} + + \begin{function}{\symref,\symname} + The command |\symref{symbolname}{text}| marks the |text| + in the second argument as representing the |symbolname| + in the first argument -- which is why the word ``series'' + is set in boldface. In the pdf, this is all that happens. + In the |xhtml| (which we will investigate shortly) however, + we will note that the word ``series'' is now annotated with the + full URI of the symbol denoting the \emph{mathematical concept of + a series}. In other words, the word is associated with an unambiguous + semantics. + + Notably, in both cases above (\emph{series} and \emph{converges}) + the text that \emph{references} the symbol and the name of the symbol + are identical. Since this occurs quite often, the shorthand + |\symname{converges}| would have worked as well, where + |\symname{foo-bar}| behaves exactly like |\symref{foo-bar}{foo bar}| + - i.e. the text is simply the name of the symbol with ``|-|'' replaced by + a space. + \end{function} + + \begin{function}{\importmodule} + If you investigated the contents of the imported modules + (|realarith| and |series|) more closely, you'll note that + none of them contain a symbol ``|converges|''. Yet, we + can use |\symref| to refer to ``converges''. That is because + the symbol |converges| is found in + |smglom/calculus/source/sequenceConvergence.en.tex|, and + |series.en.tex| contains the line + |\importmodule{sequenceConvergence}|. The |\importmodule|-statement + makes the module referenced available to all documents + that include the current module. As such, a ``current module'' + has to exist for |\importmodule| to work, which is why the command + is only allowed within a |module|-environment. + \end{function} + + \textcolor{red}{TODO} explain |xhtml| conversion, MMT compilation + (requires an archive...?). + + \end{sfragment} +\end{sfragment} + +\begin{sfragment}{Using \sTeX} + \input{packages/stex-basics} + + \input{packages/stex-terms} + + \input{packages/stex-references} +\end{sfragment} + +\begin{sfragment}[id=sec.stexarchives]{\sTeX Archives} + \input{packages/stex-mathhub} +\end{sfragment} + +\begin{sfragment}{Creating New Modules and Symbols} + \textcolor{red}{TODO} + + \stexexample{ + \begin{smodule}{assoctest} + \symdef{foo}[args=iia]{\comp{a:}#1\comp{;b:}#2\comp{;c:}#3}{\comp[#1\comp{;}##1\comp+##2\comp;#2\comp]} + $\foo {w_1}{w_2}{x,y,z}$ + \end{smodule} + } + + \input{packages/stex-modules} + + \input{packages/stex-symbols} + + \input{packages/stex-inheritance} + + \begin{sfragment}{Advanced Structuring Mechanisms} + \input{packages/stex-features} + \end{sfragment} + \begin{sfragment}{Primitive Symbols (The \sTeX Metatheory)} + \input{packages/stex-metatheory} + \end{sfragment} +\end{sfragment} + +\begin{sfragment}{\sTeX Statements (Definitions, Theorems, Examples, ...)} + \input{packages/stex-statements} + + \input{packages/stex-proofs} +\end{sfragment} + +\begin{sfragment}{Additional Packages} + \input{packages/stex-tikzinput} + \begin{sfragment}{Modular Document Structuring} + \input{packages/stex-document-structure} + \end{sfragment} + \begin{sfragment}{Slides and Course Notes} + \input{packages/stex-slides} + \end{sfragment} + \begin{sfragment}{Homework, Problems and Exams} + \input{packages/stex-problem} + + \input{packages/stex-hwexam} + \end{sfragment} + +\end{sfragment} + +\chapter{Stuff} + +\section{Modules} + + +\begin{function}{\sTeX , \stex} + Both print this \stex logo. +\end{function} + + \subsection{Semantic Macros and Notations} + + Semantic macros invoke a formally declared symbol. + + To declare a symbol (in a module), we use \cs{symdecl}, + which takes as argument the name of the corresponding + semantic macro, e.g. |\symdecl{foo}| introduces the macro + \cs{foo}. Additionally, \cs{symdecl} takes several options, + the most important one being its arity. |foo| as declared above + yields a \emph{constant} symbol. To introduce an \emph{operator} + which takes arguments, we have to specify which arguments it takes. + + \begin{smodule}{SemanticMacrosExample} + For example, to introduce binary multiplication, + we can do |\symdecl{mult}[args=2]|. We can then supply + the semantic macro with arbitrarily many notations, such as + |\notation{mult}{#1 #2}|. + + \stexexample{ + \symdecl{mult}[args=2] + \notation{mult}{#1 #2} + $\mult{a}{b}$ +} + + Since usually, a freshly introduced symbol also comes with a + notation from the start, the \cs{symdef} command combines + \cs{symdecl} and \cs{notation}. So instead of the above, + we could have also written + \begin{center} |\symdef{mult}[args=2]{#1 #2}| \end{center} + + \symdecl{mult}[args=2] + \notation{mult}{#1 #2} + + \notation{mult}[cdot]{#1 \comp{\cdot} #2} + \notation{mult}[times]{#1 \comp{\times} #2} + Adding more notations like + |\notation{mult}[cdot]{#1 \comp{\cdot} #2}| or + |\notation{mult}[times]{#1 \comp{\times} #2}| + allows us to write |$\mult[cdot]{a}{b}$| and + |$\mult[times]{a}{b}$|: + \stexexample{ + \notation{mult}[cdot]{#1 \comp{\cdot} #2} + \notation{mult}[times]{#1 \comp{\times} #2} + $\mult[cdot]{a}{b}$ and $\mult[times]{a}{b}$ +} + \notation{mult}[cdot]{#1 \comp{\cdot} #2} + \notation{mult}[times]{#1 \comp{\times} #2} + + Not using an explicit option with a semantic macro yields + the first declared notation, unless changed\ednote{TODO}. + + Outside of math mode, or by using the starred variant + |\foo*|, allows to provide a custom notation, where + notational (or textual) components can be given + explicitly in square brackets. + \stexexample{ + $\mult*{\arg{a}\comp{\ast}\arg{b}}$ is the + \mult{\comp{product of} \arg{$a$} \comp{and} \arg{$b$}} +} + + In custom mode, prefixing an argument with a star will not + print that argument, but still export it to \omdoc: + \stexexample{ + \mult{\comp{Multiplying} \arg*{$\mult{a}{b}$} again by \arg{$b$}} yields... +} + The syntax |*[|\meta{int}|]| allows switching + the order of arguments. For example, given a 2-ary semantic + macro |\forevery| with exemplary notation + |\forall #1. #2|, we can write + \stexexample{ + \symdecl{forevery}[args=2] + \forevery{\arg[2]{The proposition $P$} \comp{holds for every} \arg[1]{$x\in A$}} +} + + When using |*[|$n$|]|, after reading the provided ($n$th) argument, + the ``argument counter'' automatically + continues where we left off, so the |*[1]| in the above example + can be omitted. + + For a macro with arity $>0$, we can refer to the operator + \emph{itself} semantically by suffixing the semantic macro + with an exclamation point |!| in either text or math mode. + For that reason \cs{notation} (and thus \cs{symdef}) take an + additional optional argument |op=|, which allows to assign + a notation for the operator itself. e.g. + \stexexample{ + \symdef{add}[args=2,op={+}]{#1 \comp+ #2} + The operator $\add!$ adds two elements, as in $\add ab$. + } + + |*| is composable with |!| for custom notations, as in: + + \stexexample{ + \mult!{\comp{Multiplication}} (denoted by $\mult!*{\comp\cdot}$) is defined by... +} + + The macro \cs{comp} as used everywhere above is responsible + for highlighting, linking, and tooltips, and should be wrapped + around the notation (or text) components that should be treated + accordingly. While it is attractive to just wrap a whole notation, + this would also wrap around e.g. the arguments themselves, so + instead, the user is tasked with marking the notation components + themself. + + The precise behaviour of \cs{comp} is governed by + the macro \cs{@comp}, which takes two arguments: The tex code + of the text + (unexpanded) to highlight, and the URI of the current symbol. + \cs{@comp} can be safely redefined to customize the behaviour. + + + The starred variant |\symdecl*{foo}| does not introduce a semantic + macro, but still declares a corresponding symbol. |foo| (like + any other symbol, for that matter) can + then be accessed via \cs{STEXsymbol}|{foo}| or (if |foo| was declared + in a module |Foo|) via \cs{STEXModule}|{Foo}?{foo}|. + + both \cs{STEXsymbol} and \cs{STEXModule} take any + arbitrary ending segment of a full URI to determine + which symbol or module is meant. e.g. + \cs{STEXsymbol}|{Foo?foo}| is also valid, as are e.g. + \cs{STEXModule}|{path?Foo}?{foo}| or + \cs{STEXsymbol}|{path?Foo?foo}| + + There's also a convient shortcut \cs{symref}|{?foo}{some text}| for + \cs{STEXsymbol}|{?foo}![some text]|. + + \end{smodule} + + \subsubsection{Other Argument Types} + + So far, we have stated the arity of a semantic macro directly. + This works if we only have ``normal'' (or more precisely: |i|-type) arguments. + To make use of other argument types, instead of providing the arity + numerically, we can provide it as a sequence of characters representing + the argument types -- e.g. instead of writing |args=2|, we + can equivalently write |args=ii|, indicating that the macro + takes two |i|-type arguments. + + Besides |i|-type arguments, \sTeX has two other types, which we will + discuss now. + + The first are \emph{binding} (|b|-type) arguments, representing + variables that are \emph{bound} by the operator. This is the + case for example in the above \cs{forevery}-macro: + The first argument is not actually an argument that the + |forevery| ``function'' is ``applied'' to; rather, the first argument + is a new variable (e.g. $x$) that is \emph{bound} in the subsequent + argument. More accurately, the macro should therefore have been + implemented thusly: + \begin{center}|\symdef{forevery}[args=bi]{\forall #1.\; #2}|\end{center} + + \begin{smodule}{OtherArgs} + |b|-type arguments are indistinguishable from |i|-type arguments + within \sTeX, but are treated very differently in \omdoc and by \mmt. + More interesting \emph{within} \sTeX are |a|-type arguments, + which represent (associative) arguments of flexible arity, which are + provided as comma-separated lists. + This allows e.g. better representing the \cs{mult}-macro above: + + \stexexample{ + \symdef{mult}[args=a]{#1}{##1 \comp\cdot ##2} + $\mult{a,b,c,{d^e},f}$ +} + As the example above shows, notations get a little more complicated + for associative arguments. For every |a|-type argument, the + \cs{notation}-macro takes an additional argument that declares + how individual entries in an |a|-type argument list are aggregated. + The first notation argument then describes how the aggregated + expression is combined into the full representation. + + For a more interesting example, consider a flexary operator + for ordered sequences in ordered set, that taking + arguments |{a,b,c}| and |\mathbb{R}| prints + $a \leq b \leq c\in \mathbb R$. This operator takes + two arguments (an |a|-type argument and an |i|-type argument), + aggregates the individuals of the associative argument using |\leq|, + and combines the result with |\in| and the second argument thusly: + + \stexexample{ + \symdef{numseq}[args=ai]{#1 \comp\in #2}{##1 \comp\leq ##2} + $\numseq{a,b,c}{\mathbb R}$ +} + + Finally, |B|-type arguments combine the functionalities of |a| + and |b|, i.e. they represent flexary binding operator arguments. + +\ednote{what about e.g. \detokenize{\int_x\int_y\int_z f dx dy dz}?} +\ednote{``decompose'' a-type arguments into fixed-arity operators?} + + \end{smodule} + + \subsubsection{Precedences} + + Every notation has an (upwards) \emph{operator precedence} and + for each argument a (downwards) \emph{argument precedence} + used for automated bracketing. For example, a notation + for a binary operator \cs{foo} could be declared like this: + \begin{center} |\notation{foo}[prec=200;500x600]{#1 \comp{+} #2}| \end{center} + assigning an operator precedence of 200, an argument precedence + of 500 for the first argument, and an argument precedence of 600 + for the second argument. + + \sTeX insert brackets thusly: Upon encountering a semantic + macro (such as \cs{foo}), its operator precedence (e.g. 200) + is compared to the current downwards precedence (initially + \cs{neginfprec}). If the operator precedence is \emph{larger} + than the current downwards precedence, parentheses are inserted + around the semantic macro. + + Notations for symbols of arity 0 have a default precedence of \cs{infprec}, + i.e. by default, parentheses are never inserted around constants. + Notations for symbols with arity $>0$ have a default operator + precedence of $0$. + If no argument precedences are explicitly provided, then by + default they are equal to the operator precedence. + + Consequently, if some operator $A$ should bind stronger than + some operator $B$, then $A$s operator precedence should be + smaller than $B$s argument precedences. + + For example: + \begin{smodule}{NotationsEx} + \symdecl{plus}[args=2] + \symdecl{times}[args=2] + \stexexample{ +\notation{plus}[prec=100]{#1 \comp{+} #2} +\notation{times}[prec=50]{#1 \comp{\cdot} #2} +$\plus{a}{\times{b}{c}}$ and $\times{a}{\plus{b}{c}}$ +} + + + \end{smodule} + + \subsection{Archives and Imports} + + \subsubsection{Namespaces} + Ideally, \sTeX would use arbitrary URIs for modules, with no + forced relationships between the \emph{logical} namespace + of a module and the \emph{physical} location of the file + declaring the module -- like \mmt does things. + + Unfortunately, \TeX\ only provides very restricted access to + the file system, so we are forced to generate namespaces + systematically in such a way that they reflect the physical + location of the associated files, so that \sTeX can resolve + them accordingly. Largely, users need not concern themselves + with namespaces at all, but for completenesses sake, we describe + how they are constructed: + + \begin{itemize} + \item If \cs{begin}|{module}{Foo}| occurs in a file + |/path/to/file/Foo[.|\meta{lang}|].tex| which does not belong + to an archive, the namespace is |file://path/to/file|. + \item If the same statement occurs in a file + |/path/to/file/bar[.|\meta{lang}|].tex|, the namespace is + |file://path/to/file/bar|. + \end{itemize} + + In other words: outside of archives, the namespace corresponds to + the file URI with the filename dropped iff it is equal to the + module name, and ignoring the (optional) language suffix^^A + \footnote{which is internally attached to the module name instead, + but a user need not worry about that.}. + + If the current file is in an archive, the procedure is the same + except that the initial segment of the file path up to the archive's + |source|-folder is replaced by the archive's namespace URI. + + \subsubsection{Paths in Import-Statements} + + Conversely, here is how namespaces/URIs and file paths are computed + in import statements, examplary \cs{importmodule}: + + \begin{itemize} + \item \cs{importmodule}|{Foo}| outside of an archive refers + to module |Foo| in the current namespace. Consequently, |Foo| + must have been declared earlier in the same document or, if not, + in a file |Foo[.|\meta{lang}|].tex| in the same directory. + \item The same statement \emph{within} an archive refers to either + the module |Foo| declared earlier in the same document, or + otherwise to the module |Foo| in the archive's top-level namespace. + In the latter case, is has to be declared in a file |Foo[.|\meta{lang}|].tex| + directly in the archive's |source|-folder. + \item Similarly, in \cs{importmodule}|{some/path?Foo}| the path + |some/path| refers to either the sub-directory and relative + namespace path of the current directory and namespace outside of an archive, + or relative to the current archive's top-level namespace and |source|-folder, + respectively. + + The module |Foo| must either be declared in the file + \meta{top-directory}|/some/path/Foo[.|\meta{lang}|].tex|, or in + \meta{top-directory}|/some/path[.|\meta{lang}|].tex| (which are + checked in that order). + \item Similarly, \cs{importmodule}|[Some/Archive]{some/path?Foo}| + is resolved like the previous cases, but relative to the archive + |Some/Archive| in the mathhub-directory. + \item Finally, \cs{importmodule}|{full://uri?Foo}| naturally refers to the + module |Foo| in the namespace |full://uri|. Since the file this module + is declared in can not be determined directly from the URI, the module + must be in memory already, e.g. by being referenced earlier in the + same document. + + Since this is less compatible with a modular development, using full + URIs directly is discouraged. + + \end{itemize} + + + + +\csname if@infulldoc\endcsname\else\end{document}\fi |