diff options
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages')
16 files changed, 2422 insertions, 97 deletions
diff --git a/macros/latex/contrib/stex/doc/packages/stex-basics.tex b/macros/latex/contrib/stex/doc/packages/stex-basics.tex index daa6d6418d..f766b9b22f 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-basics.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-basics.tex @@ -1,3 +1,9 @@ +We can use \sTeX by simply including the package with |\usepackage{stex}|, +or -- primarily for individual fragments to be included in other +documents -- by using the \sTeX document class with |\documentclass{stex}| +which combines the \pkg{standalone} document class with the \pkg{stex} +package. + Both the \pkg{stex} package and document class offer the following options: @@ -5,12 +11,31 @@ options: \item[\texttt{lang}] (\meta{language}$\ast$) Languages to load with the \pkg{babel} package. \item[\texttt{mathhub}] (\meta{directory}) MathHub folder - to search for repositories. - \item[\texttt{sms}] (\meta{boolean}) use \emph{persisted} - mode (not yet implemented). + to search for repositories -- this is not necessary if the + |MATHHUB| system variable is set. + \item[\texttt{writesms}] (\meta{boolean}) with this package + option, \sTeX will write the contents of all external + modules imported via \stexcode"\importmodule" or \stexcode"\usemodule" + into a file \stexcode"\jobname.sms" (analogously to + the table of contents \stexcode".toc"-file). + \item[\texttt{usems}] (\meta{boolean}) subsequently tells + \sTeX to read the generated sms-file at the beginning of the + document. This allows for e.g. collaborating on documents + without all authors having to have all used archives and + modules available -- one author can load the modules + with \texttt{writesms}, and the rest can use the + the modules with \texttt{usesms}. Furthermore, the sms + file can be submitted alongside a \texttt{tex}-file, + effectively making it ``standalone''. \item[\texttt{image}] (\meta{boolean}) passed on to \pkg{tikzinput}. \item[\texttt{debug}] (\meta{log-prefix}$\ast$) Logs debugging information with the given prefixes to the terminal, - or all if |all| is given. -\end{description}
\ No newline at end of file + or all if |all| is given. Largely irrelevant for the + majority of users. +\end{description} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex b/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex index 1c8fe97dac..f8d570ea5e 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex @@ -1 +1,155 @@ -\textcolor{red}{TODO: document-structure documentation}
\ No newline at end of file +The \pkg{document-structure} package supplies an infrastructure for writing {\omdoc} documents in {\LaTeX}. +This includes a simple structure sharing mechanism for \sTeX that allows to to move from +a copy-and-paste document development model to a copy-and-reference model, which +conserves space and simplifies document management. The augmented structure can be used +by MKM systems for added-value services, either directly from the \sTeX sources, or +after translation. + + + The \pkg{document-structure} package supplies macros and environments that allow to label document + fragments and to reference them later in the same document or in other documents. In + essence, this enhances the document-as-trees model to + documents-as-directed-acyclic-graphs (DAG) model. This structure can be used by MKM + systems for added-value services, either directly from the \sTeX sources, or after + translation. Currently, trans-document referencing provided by this package can only be + used in the \sTeX collection. + + DAG models of documents allow to replace the ``Copy and Paste'' in the source document + with a label-and-reference model where document are shared in the document source and the + formatter does the copying during document formatting/presentation. + +The \pkg{document-structure} package accepts the following options: +\begin{center} + \begin{tabular}{|l|p{10cm}|}\hline + \texttt{class=\meta{name}} & load \meta{name}|.cls| instead of |article.cls|\\\hline + \texttt{topsect=\meta{sect}} & The top-level sectioning level; the default for + \meta{sect} is \texttt{section}\\\hline + \end{tabular} +\end{center} + +\begin{environment}{sfragment} + The structure of the document is given by nested |sfragment| environments. In the + {\LaTeX} route, the |sfragment| environment is flexibly mapped to sectioning commands, + inducing the proper sectioning level from the nesting of |sfragment| + environments. Correspondingly, the |sfragment| environment takes an optional key/value + argument for metadata followed by a regular argument for the (section) title of the + sfragment. The optional metadata argument has the keys |id| for an identifier, + |creators| and |contributors| for the Dublin Core metadata~\cite{DCMI:dmt03}. The option + |short| allows to give a short title for the generated section. If the title contains + semantic macros, they need to be protected by |\protect|\ednote{MK: still?}, and we need + to give the |loadmodules| key it needs no value. For instance we would have +\begin{latexcode} +\begin{smodule}{foo} + \symdef{bar}{B^a_r} + ... + \begin{sfragment}[id=sec.barderiv,loadmodules] + {Introducing $\protect\bar$ Derivations} +\end{latexcode} + +\sTeX automatically computes the sectioning level, from the nesting of |sfragment| +environments. +\end{environment} + +But sometimes, we want to skip levels (e.g. to use a |\subsection*| as an introduction for +a chapter). + +\begin{environment}{blindfragment} + Therefore the \pkg{document-structure} package provides a variant |blindfragment| that + does not produce markup, but increments the sectioning level and logically groups + document parts that belong together, but where traditional document markup relies on + convention rather than explicit markup. The |blindfragment| environment is useful + e.g. for creating frontmatter at the correct level. The example below shows a typical + setup for the outer document structure of a book with parts and chapters. + +\begin{latexcode} +\begin{document} +\begin{blindfragment} +\begin{blindfragment} +\begin{frontmatter} +\maketitle\newpage +\begin{sfragment}{Preface} +... <<preface>> ... +\end{sfragment} +\clearpage\setcounter{tocdepth}{4}\tableofcontents\clearpage +\end{frontmatter} +\end{blindfragment} +... <<introductory remarks>> ... +\end{blindfragment} +\begin{sfragment}{Introduction} +... <<intro>> ... +\end{sfragment} +... <<more chapters>> ... +\bibliographystyle{alpha}\bibliography{kwarc} +\end{document} +\end{latexcode} + +Here we use two levels of |blindfragment|: +\begin{itemize} +\item The outer one groups the introductory parts of the book (which we assume to have a + sectioning hierarchy topping at the part level). This |blindfragment| makes sure that + the introductory remarks become a ``chapter'' instead of a ``part''. +\item The inner one groups the frontmatter\footnote{We shied away from redefining the + |frontmatter| to induce a blindfragment, but this may be the ``right'' way to go in + the future.} and makes the preface of the book a section-level construct.\ednote{MK: + We need a substitute for the ``Note that here the |display=flow| on the |sfragment| + environment prevents numbering as is traditional for prefaces.''} +\end{itemize} +\end{environment} + +\begin{function}{\skipfragment} + The |\skipfragment| ``skips an |sfragment|'', i.e. it just steps the respective sectioning + counter. This macro is useful, when we want to keep two documents in sync structurally, + so that section numbers match up: Any section that is left out in one becomes a + |\skipfragment|. +\end{function} + +\begin{function}{\currentsectionlevel,\CurrentSectionLevel} + The |\currentsectionlevel| macro supplies the name of the current sectioning level, + e.g. ``chapter'', or ``subsection''. |\CurrentSectionLevel| is the capitalized + variant. They are useful to write something like ``In this |\currentsectionlevel|, we + will\ldots'' in an |sfragment| environment, where we do not know which sectioning level we + will end up. +\end{function} + +\begin{function}{\prematurestop,\afterprematurestop} + For prematurely stopping the formatting of a document, \sTeX provides the + |\prematurestop| macro. It can be used everywhere in a document and ignores all input + after that -- backing out of the |sfragment| environment as needed. After that -- and + before the implicit |\end{document}| it calls the internal |\afterprematurestop|, which + can be customized to do additional cleanup or e.g. print the bibliography. + + |\prematurestop| is useful when one has a driver file, e.g. for a course taught multiple + years and wants to generate course notes up to the current point in the lecture. Instead + of commenting out the remaining parts, one can just move the |\prematurestop| macro. + This is especially useful, if we need the rest of the file for processing, e.g. to + generate a theory graph of the whole course with the already-covered parts marked up as + an overview over the progress; see |import_graph.py| from the |lmhtools| + utilities~\cite{lmhtools:github:on}. +\end{function} + +Text fragments and modules can be made more re-usable by the use of global variables. For +instance, the admin section of a course can be made course-independent (and therefore +re-usable) by using variables (actually token registers) |courseAcronym| and |courseTitle| +instead of the text itself. The variables can then be set in the \sTeX preamble of the +course notes file. + +\begin{function}{\setSGvar,\useSGvar} + |\setSGvar{|\meta{vname}|}{|\meta{text}|}| to set the global variable \meta{vname} to + \meta{text} and |\useSGvar{|\meta{vname}|}| to reference it. +\end{function} + +\begin{function}{\ifSGvar} + With|\ifSGvar| we can test for the contents of a global variable: the macro call + |\ifSGvar{|\meta{vname}|}{|\meta{val}|}{|\meta{ctext}|}| tests the content of the global + variable \meta{vname}, only if (after expansion) it is equal to \meta{val}, the + conditional text \meta{ctext} is formatted. +\end{function} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: article.cls topsect DCMI:dmt03 loadmodules lmhtools +% LocalWords: prematurestop afterprematurestop import_graph.py STRlabel STRcopy vname +% LocalWords: STRsemantics setSGvar ifSGvar ctext diff --git a/macros/latex/contrib/stex/doc/packages/stex-features.tex b/macros/latex/contrib/stex/doc/packages/stex-features.tex index e70bbaa0e8..b5ce5906d1 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-features.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-features.tex @@ -1,18 +1,173 @@ +\begin{sfragment}{The \texttt{mathstructure} Environment} +\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{MathStructures} + A common occurence in mathematics is bundling several + interrelated ``declarations'' together into \emph{structures}. + For example: + \begin{itemize} + \item A \emph{monoid} is a structure $\mathstruct{M,\circ,e}$ + with $\circ:M\times M\to M$ and $e\in M$ such that... + \item A \emph{topological space} is a structure + $\mathstruct{X,\mathcal T}$ where $X$ is a set and + $\mathcal T$ is a topology on $X$ + \item A \emph{partial order} is a structure $\mathstruct{S,\leq}$ + where $\leq$ is a binary relation on $S$ such that... + \end{itemize} + + This phenomenon is important and common enough to warrant special + support, in particular because it requires being able + to \emph{instantiate} such structures (or, rather, + structure \emph{signatures}) in order to talk about (concrete + or variable) \emph{particular} monoids, topological spaces, + partial orders etc. + + \begin{environment}{mathstructure} + The \stexcode"mathstructure" environment allows us to do + exactly that. It behaves exactly like the + \stexcode"smodule" environment, but is itself only allowed + inside an \stexcode"smodule" environment, and allows + for instantiation later on. + \end{environment} + + How this works is again best demonstrated by example: + \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2} + \symdef{fun}[args=bi]{#1 \comp\mapsto #2} + \symdef{set}{\comp{\texttt{Set}}} + + \stexexample{% +\begin{mathstructure}{monoid} + \symdef{universe}[type=\set]{\comp{U}} + \symdef{op}[ + args=2, + type=\funtype{\universe,\universe}{\universe}, + op=\circ + ]{#1 \comp{\circ} #2} + \symdef{unit}[type=\universe]{\comp{e}} +\end{mathstructure} + +A \symname{monoid} is... + } + Note that the \stexcode"\symname{monoid}" is appropriately + highlighted and (depending on your pdf viewer) + shows a URI on hovering -- implying that the \stexcode"mathstructure" + environment has generated a \emph{symbol} |monoid| for us. + It has not generated a semantic macro though, since + we can not use the |monoid|-symbol \emph{directly}. Instead, + we can instantiate it, for example for integers: + + \stexexample{% +\symdef{Int}[type=\set]{\comp{\mathbb Z}} +\symdef{addition}[ + type=\funtype{\Int,\Int}{\Int}, + args=2, + op=+ +]{##1 \comp{+} ##2} +\symdef{zero}[type=\Int]{\comp{0}} + +$\mathstruct{\Int,\addition!,\zero}$ is a \symname{monoid}. + } + + So far, we have not actually instantiated |monoid|, but now + that we have all the symbols to do so, we can: + + \stexexample{% +\instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[ + universe = Int , + op = addition , + unit = zero +] + +$\intmonoid{universe}$, $\intmonoid{unit}$ and $\intmonoid{op}{a}{b}$. + +Also: $\intmonoid!$ + } + \begin{function}{\instantiate} + So summarizing: + \stexcode"\instantiate" takes four arguments: The + (macro-)name of the instance, a key-value pair assigning + declarations in the corresponding \stexcode"mathstructure" + to symbols currently in scope, the name of the \stexcode"mathstructure" + to instantiate, and lastly a notation for the instance itself. + + It then generates a semantic macro that takes as argument + the name of a declaration in the instantiated \stexcode"mathstructure" + and resolves it to the corresponding instance of that particular declaration. + \end{function} + + \begin{mmtbox} + \stexcode"\instantiate" and \stexcode"mathstructure" make use of the + \emph{Theories-as-Types} paradigm (see \cite{MueRabKoh:tat18}): + + \stexcode"mathstructure{<name>}" simply creates a nested theory with name + |<name>-structure|. The \emph{constant} |<name>| is defined as + |Mod(<name>-structure)| -- a \emph{dependent record type with manifest fields}, + the fields of which are generated from (and correspond to) the constants in + |<name>-structure|. + + \stexcode"\instantiate" generates a constant whose definiens is a record term of + type |Mod(<name>-structure)|, with the fields assigned based on the respective + key-value-list. + \end{mmtbox} + + Notably, \stexcode"\instantiate" throws an error if not \emph{every} + declaration in the instantiated \stexcode"mathstructure" is being assigned. + + You might consequently ask what the usefulness of \stexcode"mathstructure" + even is. + + \begin{function}{\varinstantiate} + The answer is that we can also instantiate a + \stexcode"mathstructure" with a \emph{variable}. + The syntax of \stexcode"\varianstantiate" is equivalent + to that of \stexcode"\instantiate", but all of the key-value-pairs + are optional, and if not explicitly assigned (to a symbol \emph{or} + a variable declared with \stexcode"\vardef") inherit their notation + from the one in the \stexcode"mathstructure" environment. + \end{function} + + This allows us to do things like: + + \stexexample{% +\varinstantiate{varM}{monoid}{M} + +A \symname{monoid} is a structure +$\varM!:=\mathstruct{\varM{universe},\varM{op}!,\varM{unit}}$ +such that +$\varM{op}!:\funtype{\varM{universe},\varM{universe}}{\varM{universe}}$ ... +} + +and + +\stexexample{% + \varinstantiate{varMb}{monoid}{M_2}[universe = Int] + + Let $\varMb!:=\mathstruct{\varMb{universe},\varMb{op}!,\varMb{unit}}$ +be a \symname{monoid} on $\Int$ ... + } + + We will return to these two example later, when we also know + how to handle the \emph{axioms} of a monoid. +\end{smodule} +\end{sfragment} + +\begin{sfragment}{The \texttt{copymodule} Environment} + + \textcolor{red}{TODO: explain} + Given modules: -\stexexample{ - \begin{smodule}{magma} - \symdef{universe}{\comp{\mathcal U}} - \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2} - \end{smodule} - \begin{smodule}{monoid} - \importmodule{magma} - \symdef{unit}{\comp e} - \end{smodule} - \begin{smodule}{group} - \importmodule{monoid} - \symdef{inverse}[args=1]{{#1}^{\comp{-1}}} - \end{smodule} +\stexexample{% +\begin{smodule}{magma} + \symdef{universe}{\comp{\mathcal U}} + \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2} +\end{smodule} +\begin{smodule}{monoid} + \importmodule{magma} + \symdef{unit}{\comp e} +\end{smodule} +\begin{smodule}{group} + \importmodule{monoid} + \symdef{inverse}[args=1]{{#1}^{\comp{-1}}} +\end{smodule} } We can form a module for \emph{rings} by ``cloning'' @@ -20,48 +175,64 @@ an instance of |group| (for addition) and |monoid| (for multiplication), respectively, and ``glueing them together'' to ensure they share the same universe: -\stexexample{ - \begin{smodule}{ring} - \begin{copymodule}{group}{addition} - \renamedecl[name=universe]{universe}{runiverse} - \renamedecl[name=plus]{operation}{rplus} - \renamedecl[name=zero]{unit}{rzero} - \renamedecl[name=uminus]{inverse}{ruminus} - \end{copymodule} - \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2} - %\setnotation{rplus}{plus} - \notation*{rzero}[zero]{\comp0} - %\setnotation{rzero}{zero} - \notation*{ruminus}[uminus,op=-]{\comp- #1} - %\setnotation{ruminus}{uminus} - \begin{copymodule}{monoid}{multiplication} - \assign{universe}{\runiverse} - \renamedecl[name=times]{operation}{rtimes} - \renamedecl[name=one]{unit}{rone} - \end{copymodule} - \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2} - %\setnotation{rtimes}{cdot} - \notation*{rone}[one]{\comp1} - %\setnotation{rone}{one} - Test: $\rtimes a{\rplus c{\rtimes de}}$ - \end{smodule} +\stexexample{% +\begin{smodule}{ring} + \begin{copymodule}{group}{addition} + \renamedecl[name=universe]{universe}{runiverse} + \renamedecl[name=plus]{operation}{rplus} + \renamedecl[name=zero]{unit}{rzero} + \renamedecl[name=uminus]{inverse}{ruminus} + \end{copymodule} + \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2} +%\setnotation{rplus}{plus} + \notation*{rzero}[zero]{\comp0} +%\setnotation{rzero}{zero} + \notation*{ruminus}[uminus,op=-]{\comp- #1} +%\setnotation{ruminus}{uminus} + \begin{copymodule}{monoid}{multiplication} + \assign{universe}{\runiverse} + \renamedecl[name=times]{operation}{rtimes} + \renamedecl[name=one]{unit}{rone} + \end{copymodule} + \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2} +%\setnotation{rtimes}{cdot} + \notation*{rone}[one]{\comp1} +%\setnotation{rone}{one} + Test: $\rtimes a{\rplus c{\rtimes de}}$ +\end{smodule} } \textcolor{red}{TODO: explain donotclone} + +\end{sfragment} + +\begin{sfragment}{The \texttt{interpretmodule} Environment} + + \textcolor{red}{TODO: explain} + +\stexexample{% +\begin{smodule}{int} + \symdef{Integers}{\comp{\mathbb Z}} + \symdef{plus}[args=2,op=+]{#1 \comp+ #2} + \symdef{zero}{\comp0} + \symdef{uminus}[args=1,op=-]{\comp-#1} + + \begin{interpretmodule}{group}{intisgroup} + \assign{universe}{\Integers} + \assign{operation}{\plus!} + \assign{unit}{\zero} + \assign{inverse}{\uminus!} + \end{interpretmodule} +\end{smodule} +} + +\end{sfragment} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: -\stexexample{ - \begin{smodule}{int} - \symdef{Integers}{\comp{\mathbb Z}} - \symdef{plus}[args=2,op=+]{#1 \comp+ #2} - \symdef{zero}{\comp0} - \symdef{uminus}[args=1,op=-]{\comp-#1} - - \begin{interpretmodule}{group}{intisgroup} - \assign{universe}{\Integers} - \assign{operation}{\plus!} - \assign{unit}{\zero} - \assign{inverse}{\uminus!} - \end{interpretmodule} - \end{smodule} -}
\ No newline at end of file +% LocalWords: circ,e intmonoid MueRabKoh:tat18 varinstantiate 2,op runiverse rplus prec +% LocalWords: rzero uminus ruminus plus,op uminus,op rtimes cdot,op cdot,prec 1,op +% LocalWords: donotclone intisgroup diff --git a/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex b/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex index 5f1758b015..5aced96e66 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex @@ -1 +1,84 @@ -\textcolor{red}{TODO: hwexam documentation}
\ No newline at end of file + +The \pkg{hwexam} package and class supplies an infrastructure that allows to format +nice-looking assignment sheets by simply including problems from problem files marked up +with the \pkg{roblem} package. It is designed to be compatible with |problems.sty|, and +inherits some of the functionality. + +\begin{variable}{solutions,notes,hints,gnotes,pts,min} + The \pkg{wexam} package and class take the options |solutions|, |notes|, |hints|, + |gnotes|, |pts|, |min|, and |boxed| that are just passed on to the \pkg{problems} + package (cf. its documentation for a description of the intended behavior). +\end{variable} + +This package supplies the \DescribeEnv{assignment}|assignment| environment that groups +problems into assignment sheets. It takes an optional KeyVal argument with the keys +\DescribeMacro{number}|number| (for the assignment number; if none is given, 1 is +assumed as the default or --- in multi-assignment documents --- the ordinal of the +|assignment| environment), \DescribeMacro{title}|title| (for the assignment title; this +is referenced in the title of the assignment sheet), \DescribeMacro{type}|type| (for the +assignment type; e.g. ``quiz'', or ``homework''), \DescribeMacro{given}|given| (for the +date the assignment was given), and \DescribeMacro{due}|due| (for the date the +assignment is due). + +Furthermore, the \pkg{hwexam} package takes the option +\DescribeMacro{multiple}|multiple| that allows to combine multiple assignment sheets +into a compound document (the assignment sheets are treated as section, there is a table +of contents, etc.). + +Finally, there is the option \DescribeMacro{test}|test| that modifies the behavior to +facilitate formatting tests. Only in |test| mode, the macros |\testspace|, +|\testnewpage|, and |\testemptypage| have an effect: they generate space for the +students to solve the given problems. Thus they can be left in the {\LaTeX} source. + +\DescribeMacro{\testspace}|\testspace| takes an argument that expands to a dimension, +and leaves vertical space accordingly. \DescribeMacro{\testnewpage}|\testnewpage| makes +a new page in |test| mode, and \DescribeMacro{\testemptypage}|\testemptypage| generates +an empty page with the cautionary message that this page was intentionally left empty. + +Finally, the \DescribeEnv{testheading}|\testheading| takes an optional keyword argument +where the keys \DescribeMacro{duration}|duration| specifies a string that specifies the +duration of the test, \DescribeMacro{min}|min| specifies the equivalent in number of +minutes, and \DescribeMacro{reqpts}|reqpts| the points that are required for a perfect +grade. + +\begin{latexcode} +\title{320101 General Computer Science (Fall 2010)} +\begin{testheading}[duration=one hour,min=60,reqpts=27] + Good luck to all students! +\end{testheading} +\end{latexcode} + +Will result in +\begin{center} + \begin{minipage}{.9\textwidth} +\makeatletter +\@problem{1.1}{4}{10} +\@problem{2.1}{4}{8} +\@problem{2.2}{6}{10} +\@problem{2.3}{6}{10} +\@problem{3.1}{4}{8} +\@problem{3.2}{4}{8} +\@problem{3.3}{2}{4} +\makeatother +\title{320101 General Computer Science (Fall 2010)} +\begin{testheading}[duration=one hour,min=60,reqpts=27] + good luck +\end{testheading} +\end{minipage} +\end{center} +\ednote{MK: The first three ``problems'' come from the stex examples above, how do we get rid + of this?} + +\begin{function}{\inputassignment} + The |\inputassignment| macro can be used to input an assignment from another file. It + takes an optional KeyVal argument and a second argument which is a path to the file + containing the problem (the macro assumes that there is only one |assignment| + environment in the included file). The keys |number|, |title|, |type|, |given|, and + |due| are just as for the |assignment| environment and (if given) overwrite the ones + specified in the |assignment| environment in the included file. +\end{function} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/macros/latex/contrib/stex/doc/packages/stex-inheritance.tex b/macros/latex/contrib/stex/doc/packages/stex-inheritance.tex index 41631f94d2..be7c4e68ec 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-inheritance.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-inheritance.tex @@ -1 +1,131 @@ -\textcolor{red}{TODO: inheritance documentation}
\ No newline at end of file +\begin{sfragment}{Simple Inheritance and Namespaces} + + \begin{function}{\importmodule,\usemodule} + \stexcode"\importmodule[Some/Archive]{path?ModuleName}" is only allowed within an + \stexcode"smodule"-environment and makes the symbols declared in |ModuleName| + available therein. Additionally the symbols of |ModuleName| will be exported if the + current module is imported somewhere else via \stexcode"\importmodule". + + \stexcode"\usemodule" behaves the same way, but without exporting the content of the + used module. + \end{function} + + It is worth going into some detail how exactly \stexcode"\importmodule" + and \stexcode"\usemodule" resolve their arguments to find + the desired module -- which is closely related to the + \emph{namespace} generated for a module, that is used to generate + its URI. + + \begin{dangerbox} + 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 \stexcode"\begin{smodule}{Foo}" + \iffalse\end{smodule}\fi 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. + + 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. +\end{dangerbox} + +\begin{dangerbox} + Conversely, here is how namespaces/URIs and file paths are computed + in import statements, examplary \stexcode"\importmodule": + + \begin{itemize} + \item \stexcode"\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 \stexcode"\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, \stexcode"\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, \stexcode"\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 strongly discouraged, unless the module is delared in + the current file directly. + \end{itemize} + + \end{dangerbox} + + \begin{function}{\STEXexport} + \stexcode"\importmodule" and \stexcode"\usemodule" import all symbols, notations, + semantic macros and (recursively) \stexcode"\importmodule"s. If you want to + additionally export e.g. convenience macros and other (\sTeX) code from a module, you + can use the command \stexcode"\STEXexport{<code>}" in your module. Then |<code>| is + executed (both immediately and) every time the current module is opened via + \stexcode"\importmodule" or \stexcode"\usemodule". + \end{function} + + \begin{dangerbox} + For persistency reasons, everything in an \stexcode"\STEXexport" + is digested by \TeX in the \LaTeX3-category code scheme. + This means that the characters \stexcode"_" and \stexcode":" + are considered \emph{letters} and valid parts of + control sequence names, and space characters are ignored entirely. + For spaces, use the character \stexcode"~" instead, and + keep in mind, that if you want to use subscripts, you + should use \stexcode"\c_math_subscript_token" instead + of \stexcode"_"! + + + Also note, that \stexcode"\newcommand" defines macros \emph{globally} + and throws an error if the macro already exists, + potentially leading to low-level \LaTeX\xspace errors if + we put a \stexcode"\newcommand" in an \stexcode"\STEXexport" + and the |<code>| is executed more than once in a document + -- which can happen easily. + + A safer alternative is to use macro definition principles, + that are safe to use even if the macro being defined already + exists, and ideally are local to the current \TeX\xspace group, + such as \stexcode"\def" or \stexcode"\let". + \end{dangerbox} + +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex b/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex index 4b05134e70..fb872acfba 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex @@ -1,5 +1,6 @@ \begin{sfragment}{The Local MathHub-Directory} - |\usemodule|, |\importmodule|, |\inputref| etc. allow for + \stexcode"\usemodule", \stexcode"\importmodule", + \stexcode"\inputref" etc. allow for including content modularly without having to specify absolute paths, which would differ between users and machines. Instead, \sTeX uses \emph{archives} that determine the global @@ -7,30 +8,30 @@ for \sTeX to find content referenced via such URIs. All \sTeX archives need to exist in the local |MathHub|-directory. - \sTeX knows where this folder is via one of three means: + \sTeX knows where this folder is via one of four means: \begin{enumerate} - \item If the \sTeX package is loaded with the option - |mathhub=/path/to/mathhub|, then \sTeX will consider - |/path/to/mathhub| as the local |MathHub|-directory. - \item If the |mathhub| package option is \emph{not} - set, but the macro |\mathhub| exists when the - \sTeX-package is loaded, then this macro is - assumed to point to the local |MathHub|-directory; i.e. - |\def\mathhub{/path/to/mathhub}\usepackage{stex}| - will set the |MathHub|-directory as |path/to/mathhub|. - \item Otherwise, \sTeX will attempt to retrieve the - system variable |MATHHUB|, assuming it will - point to the local |MathHub|-directory. Since this - variant needs setting up only \emph{once} and is - machine-specific (rather than defined in tex code), - it is compatible with collaborating and sharing tex - content, and hence recommended. + \item If the \sTeX package is loaded with the option |mathhub=/path/to/mathhub|, then + \sTeX will consider |/path/to/mathhub| as the local |MathHub|-directory. + \item If the |mathhub| package option is \emph{not} set, but the macro |\mathhub| + exists when the \sTeX-package is loaded, then this macro is assumed to point to the + local |MathHub|-directory; i.e. + \stexcode"\def\mathhub{/path/to/mathhub}\usepackage{stex}" will set the + |MathHub|-directory as |path/to/mathhub|. + \item Otherwise, \sTeX will attempt to retrieve the system variable |MATHHUB|, + assuming it will point to the local |MathHub|-directory. Since this variant needs + setting up only \emph{once} and is machine-specific (rather than defined in tex + code), it is compatible with collaborating and sharing tex content, and hence + recommended. + \item Finally, if all else fails, \sTeX will look for a file + |~/.stex/mathhub.path|. If this file exists, \sTeX will assume that it contains the + path to the local |MathHub|-directory. This method is recommended on systems where + it is difficult to set environment variables. \end{enumerate} \end{sfragment} \begin{sfragment}{The Structure of \sTeX Archives} - An \sTeX archive |group/name| needs to be stored in the + An \sTeX archive |group/name| is stored in the directory |/path/to/mathhub/group/name|; e.g. assuming your local |MathHub|-directory is set as |/user/foo/MathHub|, then in order for the |smglom/calculus|-archive to be found by the @@ -43,19 +44,41 @@ |MANIFEST.MF|, the content of which we will consider shortly \end{itemize} An additional |lib|-directory is optional, and is where \sTeX will - look for files included via |\libinput|. + look for files included via \stexcode"\libinput". Additionally a \emph{group} of archives |group/name| may have an additional archive |group/meta-inf|. If this |meta-inf|-archive - has a |/lib|-subdirectory, it too will be searched by |\libinput| + has a |/lib|-subdirectory, it too will be searched by \stexcode"\libinput" from all tex files in any archive in the |group/*|-group. + + \paragraph{} We recommend the following additional directory structure in the + |source|-folder of an \sTeX archive: + \begin{itemize} + \item |/source/mod/| -- individual \sTeX modules, containing + symbol declarations, notations, and + \stexcode"\begin{sparagraph}[type=symdoc,for=...]" + environments for ``encyclopaedic'' symbol documentations + \iffalse\end{sparagraph}\fi + \item |/source/def/| -- definitions + \item |/source/ex/| -- examples + \item |/source/thm/| -- theorems, lemmata and proofs; preferably + proofs in separate files to allow for multiple proofs for the + same statement + \item |/source/snip/| -- individual text snippets such as remarks, + explanations etc. + \item |/source/frag/| -- individual document fragments, + ideally only \stexcode"\inputref"ing snippets, definitions, + examples etc. in some desirable order + \item |/source/tikz/| -- tikz images, as individual |.tex|-files + \item |/source/PIC/| -- image files. + \end{itemize} + \end{sfragment} \begin{sfragment}{MANIFEST.MF-Files} - The |MANIFEST.MF| in the |META-INF|-directory consists of - key-value-pairs, instructing \sTeX (and associated software) - of various properties of an archive. For example, - the |MANIFEST.MF| of the |smglom/calculus|-archive looks like this: + The |MANIFEST.MF| in the |META-INF|-directory consists of key-value-pairs, informing + \sTeX (and associated software) of various properties of an archive. For example, the + |MANIFEST.MF| of the |smglom/calculus|-archive looks like this: \begin{framed} \begin{verbatim} @@ -86,4 +109,95 @@ e.g. for |lmh install|. \end{itemize} -\end{sfragment}
\ No newline at end of file +\end{sfragment} + +\begin{sfragment}{Using Files in \sTeX Archives Directly} + Several macros provided by \sTeX allow for directly including + files in repositories. These are: + \begin{function}{\mhinput} + \stexcode"\mhinput[Some/Archive]{some/file}" directly + inputs the file |some/file| in the |source|-folder of + |Some/Archive|. + \end{function} + \begin{function}{\inputref} + \stexcode"\inputref[Some/Archive]{some/file}" behaves like \stexcode"\mhinput", but + wraps the input in a |\begingroup ... \endgroup|. When converting to |xhtml|, the + file is not input at all, and instead an |html|-annotation is inserted that + references the file, e.g. for lazy loading. + + In the majority of practical cases \stexcode"\inputref" is likely to be preferred + over \stexcode"\mhinput" because it leads to less duplication in the generated + |xhtml|. + \end{function} + \begin{function}{\ifinput} + Both \stexcode"\mhinput" and \stexcode"\inputref" + set \stexcode"\ifinput" to ``true'' during input. This allows + for selectively including e.g. bibliographies only if the + current file is not being currently included in a larger document. + \end{function} + \begin{function}{\addmhbibresource} + \stexcode"\addmhbibresource[Some/Archive]{some/file}" searches for a file like + \stexcode"\mhinput" does, but calls |\addbibresource| to the result and looks for + the file in the archive root directory directly, rather than the |source| + directory. Typical invocations are + \begin{itemize} + \item |\addmhbibresource{lib/refs.bib}|, which specifies a bibliography in the |lib| + folder in the local archive or + \item |\addmhbibresource[HW/meta-inf]{lib/refs.bib}| in another. + \end{itemize} + \end{function} + \begin{function}{\libinput} + \stexcode"\libinput{some/file}" + searches for a file |some/file| in + \begin{itemize} + \item the |lib|-directory of the current archive, and + \item the |lib|-directory of a |meta-inf|-archive in + (any of) the archive groups containing the current archive + \end{itemize} + and include all found files in reverse order; + e.g. \stexcode"\libinput{preamble}" in a |.tex|-file in + |smglom/calculus| will \emph{first} input |.../smglom/meta-inf/lib/preamble.tex| + and then |../smglom/calculus/lib/preamble.tex|. + + \stexcode|\libinput| will throw an error if \emph{no} candidate for |some/file| + is found. + \end{function} + \begin{function}{\libusepackage} + \stexcode"\libusepackage[package-options]{some/file}" searches for a file + |some/file.sty| in the same way that \stexcode"\libinput" does, but will + call\\ + |\usepackage[package-options]{path/to/some/file}| instead of |\input|. + + \stexcode|\libusepackage| throws an error if not \emph{exactly one} candidate for + |some/file| is found. + \end{function} + + \begin{remark} + A good practice is to have individual \sTeX fragments + follow basically this document frame: + \begin{latexcode}[gobble=12] + \documentclass{stex} + \libinput{preamble} + \begin{document} + ... + \ifinputref \else \libinput{postamble} \fi + \end{document} + \end{latexcode} + Then the |preamble.tex| files can take care of loading the generally required + packages, setting presentation customizations etc. (per archive or archive group + or both), and |postamble.tex| can e.g. print the bibliography, index etc. + + \stexcode|\libusepackage| is particularly useful in |preamble.tex| when we want to + use custom packages that are not part of {\TeX}Live. In this case we commit the + respective packages in one of the |lib| folders and use \stexcode|\libusepackage| + to load them. + \end{remark} +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +%%% LocalWords: mathhub symdoc,for lmh subdirs arithmetics,smglom sets,smglom mv,smglom +%%% LocalWords: linear-algebra,smglom diff --git a/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex b/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex index 1585ba504c..4feb646eb9 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex @@ -1 +1,30 @@ -\textcolor{red}{TODO: metatheory documentation}
\ No newline at end of file +The \pkg{stex-metatheory} package contains \sTeX symbols so ubiquitous, that it is +virtually impossible to describe any flexiformal content without them, or that are +required to annotate even the most primitive symbols with meaningful +(foundation-independent) ``type''-annotations, or required for basic structuring +principles (theorems, definitions). As such, it serves as the default meta theory for any +\sTeX module. + +We can also see the \pkg{stex-metatheory} as a foundation of mathematics in the sense of +\cite{rabe:future:15}, albeit an informal one (the ones discussed there are all formal +foundations). The state of the \pkg{stex-metatheory} is necessarily incomplete, and will +stay so for a long while: It arises as a collection of empirically useful symbols that are +collected as more and more mathematics are encoded in \sTeX and are classified as +foundational. + +Formal foundations should ideally instantiate these symbols with their formal counterparts, +e.g. |isa| corresponds to a typing operation in typed setting, or the $\in$-operator in +set-theoretic contexts; |bind| corresponds to a universal quantifier in ($n$th-order) +logic, or a $\Pi$ in dependent type theories. + +We make this theory part of the \sTeX collection due to the obiquity +of the symbols involved. Note however, that the metatheory is +for all practical purposes a ``normal'' \sTeX module, and the +symbols contained ``normal'' \sTeX symbols. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: stex-metatheory th-order diff --git a/macros/latex/contrib/stex/doc/packages/stex-modules.tex b/macros/latex/contrib/stex/doc/packages/stex-modules.tex index c067f28a1c..424c2200e8 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-modules.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-modules.tex @@ -1 +1,73 @@ -\textcolor{red}{TODO: modules documentation}
\ No newline at end of file +\begin{sfragment}{The \texttt{smodule}-Environment} + \begin{environment}{smodule} + A new module is declared using the basic syntax + \begin{center} + \stexcode"\begin{smodule}[options]{ModuleName}...\end{smodule}". + \end{center} + A module is required to declare any new formal content such as symbols or + notations (but not variables, which may be introduced anywhere). + + The |smodule|-environment takes several keyword arguments, all of which are + optional: + + \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} + \end{environment} + + \begin{mmtbox} + An \sTeX module corresponds to an \mmt/\omdoc \emph{theory}. + As such it gets assigned a module URI (\emph{universal resource identifier}) + of the form |<namespace>?<module-name>|. + \end{mmtbox} + + By default, opening a module will produce no output whatsoever, + e.g.: + \stexexample{% +\begin{smodule}[title={This is Some Module}]{SomeModule} + Hello World +\end{smodule} + } + + \begin{function}{\stexpatchmodule} + We can customize this behavior either for all modules or + only for modules with a specific |type| using the command + \stexcode"\stexpatchmodule[optional-type]{begin-code}{end-code}". + Some optional parameters are then available in |\smodule*|-macros, + specifically |\smoduletitle|, |\smoduletype| and |\smoduleid|. + \end{function} + For example: + + \stexexample{% +\stexpatchmodule[display] + {\textbf{Module (\smoduletitle)}\par} + {\par\noindent\textbf{End of Module (\smoduletitle)}} + +\begin{smodule}[type=display,title={Some New Module}]{SomeModule2} + Hello World +\end{smodule} + } +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: srccite mmtbox stexexample stexpatchmodule smoduletitle smoduleid +% LocalWords: display,title diff --git a/macros/latex/contrib/stex/doc/packages/stex-problem.tex b/macros/latex/contrib/stex/doc/packages/stex-problem.tex index 1ce5aaa3a2..a90c36412d 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-problem.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-problem.tex @@ -1 +1,151 @@ -\textcolor{red}{TODO: problem documentation}
\ No newline at end of file +The \pkg{problem} package supplies an infrastructure that allows specify problem. Problems +are text fragments that come with auxiliary functions: hints, notes, and +solutions\footnote{for the moment multiple choice problems are not supported, but may + well be in a future version}. Furthermore, we can specify how long the solution to a +given problem is estimated to take and how many points will be awarded for a perfect +solution. + +Finally, the \pkg{problem} package facilitates the management of problems in small files, +so that problems can be re-used in multiple environment. + +\begin{function}{solutions,notes,hints,gnotes,pts,min,boxed,test} + The \pkg{problem} package takes the options |solutions| (should solutions be output?), + |notes| (should the problem notes be presented?), |hints| (do we give the hints?), + |gnotes| (do we show grading notes?), |pts| (do we display the points awarded for + solving the problem?), |min| (do we display the estimated minutes for problem + soling). If theses are specified, then the corresponding auxiliary parts of the problems + are output, otherwise, they remain invisible. + + The |boxed| option specifies that problems should be formatted in framed boxes so that + they are more visible in the text. Finally, the |test| option signifies that we are in a + test situation, so this option does not show the solutions (of course), but leaves space + for the students to solve them. +\end{function} + +\begin{environment}{problem} + The main environment provided by the \pkg{problem}package is (surprise surprise) the + |problem| environment. It is used to mark up problems and exercises. The environment + takes an optional KeyVal argument with the keys |id| as an identifier that can be + reference later, |pts| for the points to be gained from this exercise in homework or + quiz situations, |min| for the estimated minutes needed to solve the problem, and + finally |title| for an informative title of the problem. +\end{environment} + +\stexexample{% +\documentclass{article} +\usepackage[solutions,hints,pts,min]{problem} +\begin{document} + \begin{sproblem}[id=elefants,pts=10,min=2,title=Fitting Elefants] + How many Elefants can you fit into a Volkswagen beetle? + \begin{hint} + Think positively, this is simple! + \end{hint} + \begin{exnote} + Justify your answer + \end{exnote} +\begin{solution}[for=elefants,height=3cm] + Four, two in the front seats, and two in the back. + \begin{gnote} + if they do not give the justification deduct 5 pts + \end{gnote} +\end{solution} +\end{sproblem} +\end{document} +} + +\begin{environment}{solution} + The |solution| environment can be to specify a solution to a problem. If the package + option |solutions| is set or |\solutionstrue| is set in the text, then the solution will + be presented in the output. The |solution| environment takes an optional KeyVal argument + with the keys |id| for an identifier that can be reference |for| to specify which + problem this is a solution for, and |height| that allows to specify the amount of space + to be left in test situations (i.e. if the |test| option is set in the |\usepackage| + statement). +\end{environment} + +\begin{environment}{hint,exnote,gnote} + The |hint| and |exnote| environments can be used in a |problem| environment to give + hints and to make notes that elaborate certain aspects of the problem. The |gnote| + (grading notes) environment can be used to document situtations that may arise in + grading. +\end{environment} + +\begin{function}{\startsolutions,\stopsolutions} + Sometimes we would like to locally override the |solutions| option we have given to the + package. To turn on solutions we use the |\startsolutions|, to turn them off, + |\stopsolutions|. These two can be used at any point in the documents. +\end{function} + +\begin{function}{\ifsolutions} + Also, sometimes, we want content (e.g. in an exam with master solutions) conditional on + whether solutions are shown. This can be done with the |\ifsolutions| conditional. +\end{function} + +\begin{environment}{mcb} + Multiple choice blocks can be formatted using the |mcb| environment, in which single + choices are marked up with |\mcc| macro. +\end{environment} + +\begin{function}{\mcc} + |\mcc[|\meta{keyvals}|]{|\meta{text}|}| takes an optional key/value argument + \meta{keyvals} for choice metadata and a required argument \meta{text} for the proposed + answer text. The following keys are supported + \begin{itemize} + \item |T| for true answers, |F| for false ones, + \item |Ttext| the verdict for true answers, |Ftext| for false ones, and + \item |feedback| for a short feedback text given to the student. + \end{itemize} +\end{function} + +If we start the solutions, then we get + +\stexexample{% +\startsolutions +\begin{sproblem}[title=Functions,name=functions1] + What is the keyword to introduce a function definition in python? + \begin{mcb} + \mcc[T]{def} + \mcc[F,feedback=that is for C and C++]{function} + \mcc[F,feedback=that is for Standard ML]{fun} + \mcc[F,Ftext=Nooooooooo,feedback=that is for Java]{public static void} + \end{mcb} +\end{sproblem} +} +without solutions (that is what the students see during the exam/quiz)\ednote{MK: that did +not work!} +\stexexample{% +\stopsolutions +\begin{sproblem}[title=Functions,name=functions1] + What is the keyword to introduce a function definition in python? + \begin{mcb} + \mcc[T]{def} + \mcc[F,feedback=that is for C and C++]{function} + \mcc[F,feedback=that is for Standard ML]{fun} + \mcc[F,Ftext=Nooooooooo,feedback=that is for Java]{public static void} + \end{mcb} +\end{sproblem} +} + +\begin{function}{\includeproblem} + The |\includeproblem| macro can be used to include a problem from another file. It takes + an optional KeyVal argument and a second argument which is a path to the file containing + the problem (the macro assumes that there is only one problem in the include file). The + keys |title|, |min|, and |pts| specify the problem title, the estimated minutes for + solving the problem and the points to be gained, and their values (if given) overwrite + the ones specified in the |problem| environment in the included file. +\end{function} + +The sum of the points and estimated minutes (that we specified in the |pts| and |min| keys +to the |problem| environment or the |\includeproblem| macro) to the log file and the +screen after each run. This is useful in preparing exams, where we want to make sure that +the students can indeed solve the problems in an allotted time period. + +The |\min| and |\pts| macros allow to specify (i.e. to print to the margin) the +distribution of time and reward to parts of a problem, if the |pts| and |pts| options are +set. This allows to give students hints about the estimated time and the points to be +awarded. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex index 0523c65948..d06db1282f 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex @@ -1 +1,214 @@ -\textcolor{red}{TODO: sproofs documentation}
\ No newline at end of file +The \pkg{stex-proof} package supplies macros and environment that allow to annotate the +structure of mathematical proofs in \sTeX document. This structure can be used by MKM +systems for added-value services, either directly from the \sTeX sources, or after +translation. + +We will go over the general intuition by way of a running example: + +\begin{latexcode} +\begin{sproof}[id=simple-proof] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + \begin{spfcases}{For the induction we have to consider three cases:} + \begin{spfcase}{$n=1$} + \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n=2$} + \begin{spfcomment}[type=inline] + This case is not really necessary, but we do it for the + fun of it (and to get more intuition). + \end{spfcomment} + \begin{spfstep}[type=inline] We compute $1+3=2^{2}=4$.\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n>1$} + \begin{spfstep}[type=assumption,id=ind-hyp] + Now, we assume that the assertion is true for a certain $k\geq 1$, + i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$. + \end{spfstep} + \begin{spfcomment} + We have to show that we can derive the assertion for $n=k+1$ from + this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. + \end{spfcomment} + \begin{spfstep} + We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$ + \spfjust[method=arith:split-sum]{by splitting the sum}. + \end{spfstep} + \begin{spfstep} + Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ + \spfjust[method=fertilize]{by inductive hypothesis}. + \end{spfstep} + \begin{spfstep}[type=conclusion] + We can \spfjust[method=simplify]{simplify} the right-hand side to + ${k+1}^2$, which proves the assertion. + \end{spfstep} + \end{spfcase} + \begin{spfstep}[type=conclusion] + We have considered all the cases, so we have proven the assertion. + \end{spfstep} + \end{spfcases} +\end{sproof} +\end{latexcode} + +This yields the following result: + +\begin{mdframed} + \begin{sproof}[id=simple-proof] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + \begin{spfcases}{For the induction we have to consider the following cases:} + \begin{spfcase}{$n=1$} + \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n=2$} + \begin{spfcomment}[type=inline] + This case is not really necessary, but we do it for the fun + of it (and to get more intuition). + \end{spfcomment} + \begin{spfstep}[type=inline] + We compute $1+3=2^{2}=4$ + \end{spfstep} + \end{spfcase} + \begin{spfcase}{$n>1$} + \begin{spfstep}[type=hypothesis,id=ind-hyp] + Now, we assume that the assertion is true for a certain $k\geq 1$, i.e. + $\sum_{i=1}^k{(2i-1)}=k^{2}$. + \end{spfstep} + \begin{spfcomment} + We have to show that we can derive the assertion for $n=k+1$ from this + assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. + \end{spfcomment} + \begin{spfstep}[id=splitit] + We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$ + \spfjust[method=arith:split-sum]{by splitting the sum}. + \end{spfstep} + \begin{spfstep}[id=byindhyp] + Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ + \spfjust[method=fertilize]{by \premise[ind-hyp]{inductive hypothesis}}. + \end{spfstep} + \begin{spfstep}[type=conclusion] + We can \spfjust[method=simplify-eq]{simplify the \justarg[rhs]{right-hand side}} to + $(k+1)^2$, which proves the assertion. + \end{spfstep} + \end{spfcase} + \begin{spfstep}[type=conclusion] + We have considered all the cases, so we have proven the assertion. + \end{spfstep} + \end{spfcases} +\end{sproof} +\end{mdframed} + +\begin{environment}{sproof} + The |sproof| environment is the main container for proofs. It takes an optional |KeyVal| + argument that allows to specify the |id| (identifier) and |for| (for which assertion is + this a proof) keys. The regular argument of the |proof| environment contains an + introductory comment, that may be used to announce the proof style. The |proof| + environment contains a sequence of |spfstep|, |spfcomment|, and |spfcases| environments + that are used to markup the proof steps. +\end{environment} + +\begin{function}{\spfidea} + The |\spfidea| macro allows to give a one-paragraph description of the proof idea. +\end{function} + +\begin{function}{\spfsketch} + For one-line proof sketches, we use the |\spfsketch| macro, which takes the same + optional argument as |sproof| and another one: a natural language text that sketches + the proof. +\end{function} + +\begin{environment}{spfstep} + Regular proof steps are marked up with the |step| environment, which takes an optional + |KeyVal| argument for annotations. A proof step usually contains a local assertion + (the text of the step) together with some kind of evidence that this can be derived + from already established assertions. +\end{environment} + +\begin{function}{\spfjust} + This evidence is marked up with the |\spfjust| macro in the \pkg{stex-proofs} + package. This environment totally invisible to the formatted result; it wraps the text + in the proof step that corresponds to the evidence. The environment takes an optional + |KeyVal| argument, which can have the |method| key, whose value is the name of a proof + method (this will only need to mean something to the application that consumes the + semantic annotations). Furthermore, the justification can contain ``premises'' + (specifications to assertions that were used justify the step) and ``arguments'' + (other information taken into account by the proof method). +\end{function} + +\begin{function}{\premise} + The |\premise| macro allows to mark up part of the text as reference to an assertion + that is used in the argumentation. In the running example we have used the |\premise| + macro to identify the inductive hypothesis. +\end{function} + +\begin{function}{\justarg} + The |\justarg| macro is very similar to |\premise| with the difference that it is used + to mark up arguments to the proof method. Therefore the content of the first argument + is interpreted as a mathematical object rather than as an identifier as in the case of + |\premise|. In our example, we specified that the simplification should take place on + the right hand side of the equation. Other examples include proof methods that + instantiate. Here we would indicate the substituted object in a |\justarg| macro. +\end{function} + +Note that both |\premise| and |\justarg| can be used with an empty second argument to +mark up premises and arguments that are not explicitly mentioned in the text. + +\begin{environment}{subproof} + The |spfcases| environment is used to mark up a subproof. This environment takes an + optional |KeyVal| argument for semantic annotations and a second argument that allows + to specify an introductory comment (just like in the |proof| environment). The + |method| key can be used to give the name of the proof method + executed to make this subproof. +\end{environment} + +\begin{environment}{spfcases} + The |spfcases| environment is used to mark up a proof by cases. Technically it is a + variant of the |subproof| where the |method| is |by-cases|. Its contents are |spfcase| + environments that mark up the cases one by one. +\end{environment} + +\begin{environment}{spfcase} + The content of a |spfcases| environment are a sequence of case proofs marked up in the + |spfcase| environment, which takes an optional |KeyVal| argument for semantic + annotations. The second argument is used to specify the the description of the case + under consideration. The content of a |spfcase| environment is the same as that of a + |sproof|, i.e. |spfstep|s, |spfcomment|s, and |spfcases| environments. +\end{environment} + +\begin{function}{\spfcasesketch} + |\spfcasesketch| is a variant of the |spfcase| environment that takes the same + arguments, but instead of the |spfstep|s in the body uses a third argument for a proof + sketch. +\end{function} + +\begin{environment}{spfcomment} + The |spfcomment| environment is much like a |step|, only that it does not have an + object-level assertion of its own. Rather than asserting some fact that is relevant + for the proof, it is used to explain where the proof is going, what we are attempting + to to, or what we have achieved so far. As such, it cannot be the target of a + |\premise|. +\end{environment} + +\begin{function}{\sproofend} + Traditionally, the end of a mathematical proof is marked with a little box at the end of + the last line of the proof (if there is space and on the end of the next line if there + isn't), like so:\sproofend + + The \pkg{stex-proofs} package provides the |\sproofend| macro for this. +\end{function} + +\begin{variable}{\sProofEndSymbol} + If a different symbol for the proof end is to be used (e.g. {\sl{q.e.d}}), then this can + be obtained by specifying it using the |\sProofEndSymbol| configuration macro (e.g. by + specifying |\sProofEndSymbol{q.e.d}|). +\end{variable} + +Some of the proof structuring macros above will insert proof end symbols for sub-proofs, +in most cases, this is desirable to make the proof structure explicit, but sometimes this +wastes space (especially, if a proof ends in a case analysis which will supply its own +proof end marker). To suppress it locally, just set |proofend={}| in them or use use +|\sProofEndSymbol{}|. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend diff --git a/macros/latex/contrib/stex/doc/packages/stex-references.tex b/macros/latex/contrib/stex/doc/packages/stex-references.tex index bf8a8ed66c..11de003e9b 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-references.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-references.tex @@ -1 +1,8 @@ -\textcolor{red}{TODO: references documentation}
\ No newline at end of file +\begin{sfragment}[id=sec.references]{Referencing Symbols and Statements} +\textcolor{red}{TODO: references documentation} +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/macros/latex/contrib/stex/doc/packages/stex-slides.tex b/macros/latex/contrib/stex/doc/packages/stex-slides.tex index 1f9d0c989d..a900c1fcbb 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-slides.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-slides.tex @@ -1 +1,212 @@ -\textcolor{red}{TODO: notesslides documentation}
\ No newline at end of file +The \pkg{notesslides} document class is derived from |beamer.cls|~\cite{beamerclass:on}, +it adds a ``notes version'' for course notes that is more suited to printing than the one +supplied by |beamer.cls|. + +The \pkg{notesslides} class takes the notion of a slide frame from Till Tantau's excellent +\pkg{beamer} class and adapts its notion of frames for use in the \sTeX and \omdoc. To +support semantic course notes, it extends the notion of mixing frames and explanatory +text, but rather than treating the frames as images (or integrating their contents into +the flowing text), the \pkg{notesslides} package displays the slides as such in the course +notes to give students a visual anchor into the slide presentation in the course (and to +distinguish the different writing styles in slides and course notes). + +In practice we want to generate two documents from the same source: the slides for +presentation in the lecture and the course notes as a narrative document for home +study. To achieve this, the \pkg{notesslides} class has two modes: \emph{slides mode} and +\emph{notes mode} which are determined by the package option. + + +\begin{variable}{slides,notes,sectocframes,frameimages,fiboxed} + The \pkg{notesslides} class takes a variety of class options: + \begin{itemize} + \item The options |slides| and |notes| switch between slides mode and notes mode (see + Section~\ref{sec:user:notesslides}). + \item If the option |sectocframes| is given, then for the |sfragment|s, special frames + with the |sfragment| title (and number) are generated. + \item If the option |frameimages| is set, then slide mode also shows the + |\frameimage|-generated frames (see section~\ref{sec:user:frameimage}). If also the + |fiboxed| option is given, the slides are surrounded by a box. + \end{itemize} +\end{variable} + +\begin{environment}{frame,note} + Slides are represented with the |frame| environment just like in the \pkg{beamer} class, + see~\cite{Tantau:ugbc} for details. The \pkg{notesslides} class adds the |note| + environment for encapsulating the course note fragments.\footnote{MK: it would be very + nice, if we did not need this environment, and this should be possible in principle, + but not without intensive LaTeX trickery. Hints to the author are welcome.} +\end{environment} + +\begin{dangerbox} + Note that it is essential to start and end the |notes| environment at the start of the + line -- in particular, there may not be leading blanks -- else {\LaTeX} becomes confused + and throws error messages that are difficult to decipher. +\end{dangerbox} + +By interleaving the |frame| and |note| environments, we can build course notes as shown +here: + +\begin{latexcode} +\ifnotes\maketitle\else +\frame[noframenumbering]\maketitle\fi + +\begin{note} + We start this course with ... +\end{note} + +\begin{frame} + \frametitle{The first slide} + ... +\end{frame} +\begin{note} + ... and more explanatory text +\end{note} + +\begin{frame} + \frametitle{The second slide} + ... +\end{frame} +... +\end{latexcode} + +\begin{function}{\ifnotes} + Note the use of the |\ifnotes| conditional, which allows different treatment between + |notes| and |slides| mode -- manually setting |\notestrue| or |\notesfalse| is strongly + discouraged however. +\end{function} + +\begin{dangerbox} + We need to give the title frame the |noframenumbering| option so that the frame + numbering is kept in sync between the slides and the course notes. +\end{dangerbox} + +\begin{dangerbox} + The \pkg{beamer} class recommends not to use the |allowframebreaks| option on frames + (even though it is very convenient). This holds even more in the |notesslides| case: At + least in conjunction with |\newpage|, frame numbering behaves funnily (we have tried to + fix this, but who knows). +\end{dangerbox} + +\begin{function}{\inputref*} + If we want to transclude a the contents of a file as a note, we can use a new variant + |\inputref*| of the |\inputref| macro: |\inputref*{foo}| is equivalent to + |\begin{note}\inputref{foo}\end{note}|. +\end{function} + +\begin{environment}{nparagraph, nparagraph, ndefinition, nexample, nsproof, nassertion} + There are some environments that tend to occur at the top-level of |note| + environments. We make convenience versions of these: e.g. the |nparagraph| environment + is just an |sparagraph| inside a |note| environment (but looks nicer in the source, + since it avoids one level of source indenting). Similarly, we have the |nfragment|, + |ndefinition|, |nexample|, |nsproof|, and |nassertion| environments. +\end{environment} + +\begin{function} {\setslidelogo} + The default logo provided by the \pkg{notesslides} package is the {\sTeX} logo it can be + customized using |\setslidelogo{|\meta{logo name}|}|. +\end{function} + +\begin{function}{\setsource} + The default footer line of the \pkg{notesslides} package mentions copyright and + licensing. In the \pkg{beamer} class, |\source| stores the author's name as the + copyright holder . By default it is \emph{Michael Kohlhase} in the \pkg{notesslides} + package since he is the main user and designer of this + package. |\setsource{|\meta{name}|}| can change the writer's name. +\end{function} + +\begin{function}{\setlicensing} + For licensing, we use the Creative Commons Attribuition-ShareAlike license by default to + strengthen the public domain. If package |hyperref| is loaded, then we can attach a + hyperlink to the license logo. |\setlicensing[|\meta{url}|]{|\meta{logo name}|}| is used + for customization, where \meta{url} is optional. +\end{function} + +Sometimes, we want to integrate slides as images after all -- e.g. because we already +have a PowerPoint presentation, to which we want to add \sTeX notes. + +\begin{function}{\frameimage,\mhframeimage} + In this case we can use |\frameimage[|\meta{opt}|]{|\meta{path}|}|, where \meta{opt} are + the options of |\includegraphics| from the \pkg{graphicx} package~\cite{CarRah:tpp99} + and \meta{path} is the file path (extension can be left off like in + |\includegraphics|). We have added the |label| key that allows to give a frame label + that can be referenced like a regular |beamer| frame. + +The |\mhframeimage| macro is a variant of |\frameimage| with repository support. Instead +of writing +\begin{latexcode} +\frameimage{\MathHub{fooMH/bar/source/baz/foobar}} +\end{latexcode} + we can simply write (assuming that |\MathHub| is defined as above) +\begin{latexcode} +\mhframeimage[fooMH/bar]{baz/foobar} +\end{latexcode} + Note that the |\mhframeimage| form is more semantic, which allows more advanced document +management features in \textsf{MathHub}. +\end{function} + +If |baz/foobar| is the ``current module'', i.e. if we are on the \textsf{MathHub} path +\ldots|MathHub/fooMH/bar|\ldots, then stating the repository in the first optional +argument is redundant, so we can just use +\begin{latexcode} +\mhframeimage{baz/foobar} +\end{latexcode} + +\begin{function}{\textwarning} + The |\textwarning| macro generates a warning sign: \textwarning +\end{function} + +In course notes, we sometimes want to point to an ``excursion'' -- material that is either +presupposed or tangential to the course at the moment -- e.g. in an appendix. The typical +setup is the following: + +\begin{latexcode} +\excursion{founif}{../ex/founif}{We will cover first-order unification in} +... +\begin{appendix}\printexcursions\end{appendix} +\end{latexcode} + +\begin{function}{\excursion} + The |\excursion{|\meta{ref}|}{|\meta{path}|}{|\meta{text}|}| is syntactic sugar for + +\begin{latexcode} +\begin{nparagraph}[title=Excursion] + \activateexcursion{founif}{../ex/founif} + We will cover first-order unification in \sref{founif}. +\end{nparagraph} +\end{latexcode} +\end{function} + +\begin{function}{\activateexcursion,\printexcursion,\excursionref} + Here |\activateexcursion{|\meta{path}|}| augments the |\printexcursions| macro by a call + |\inputref{|\meta{path}|}|. In this way, the |\printexcursions| macro (usually in the + appendix) will collect up all excursions that are specified in the main text. + + Sometimes, we want to reference -- in an excursion -- part of another. We can use + |\excursionref{|\meta{label}|}| for that. +\end{function} + +\begin{function}{\excursiongroup} + Finally, we usually want to put the excursions into an |sfragment| environment and add + an introduction, therefore we provide the a variant of the |\printexcursions| macro: + |\excursiongroup[id=|\meta{id}|,intro=|\meta{path}|]| is equivalent to +\begin{latexcode} +\begin{note} +\begin{sfragment}[id=<id>]{Excursions} + \inputref{<path>} + \printexcursions +\end{sfragment} +\end{note} +\end{latexcode} +\end{function} + +\begin{dangerbox} + When option |book| which uses |\pagestyle{headings}| is given and semantic macros are + given in the |sfragment| titles, then they sometimes are not defined by the time the + heading is formatted. Need to look into how the headings are made. This is a problem of + the underlying \pkg{document-structure} package. +\end{dangerbox} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/macros/latex/contrib/stex/doc/packages/stex-statements.tex b/macros/latex/contrib/stex/doc/packages/stex-statements.tex index aa9f5f76ab..6a2478fa7d 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-statements.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-statements.tex @@ -1 +1,145 @@ -\textcolor{red}{TODO: statements documentation}
\ No newline at end of file +\begin{sfragment}{Definitions, Theorems, Examples, Paragraphs} +\begin{smodule}{Statements} + As mentioned earlier, we can semantically mark-up + \emph{statements} such as definitions, theorems, lemmata, examples, etc. + + The corresponding environments for that are: + \begin{itemize} + \item \stexcode"sdefinition" for definitions, + \item \stexcode"sassertion" for assertions, i.e. + propositions that are declared to be \emph{true}, + such as theorems, lemmata, axioms, + \item \stexcode"sexample" for examples and counterexamples, and + \item \stexcode"sparagraph" for ``other'' semantic paragraphs, + such as comments, remarks, conjectures, etc. + \end{itemize} + + The \emph{presentation} of these environments can be customized + to use e.g. predefined |theorem|-environments, see \sref{sec.customhighlight} + for details. + + All of these environments take optional arguments in the form of + |key=value|-pairs. Common to all of them are the keys |id=| (for cross-referencing, + see \sref{sec.references}), |type=| for customization (see \sref{sec.customhighlight}) + and additional information (e.g. definition principles, ``difficulty'' etc), as well + as |title=| (for giving the paragraph a title), and finally |for=|. + + The |for=| key expects a comma-separated list of existing + symbols, allowing for e.g. things like + \symdef{addition}[args=a,prec=100]{#1}{##1 \comp+ ##2} + \symdef{multiplication}[args=a,prec=50]{#1}{##1 \comp\cdot ##2} + \stexexample{% +\begin{sexample}[ + id=additionandmultiplication.ex, + for={addition,multiplication}, + type={trivial,boring}, + title={An Example} +] + $\addition{2,3}$ is $5$, $\multiplication{2,3}$ is $6$. +\end{sexample} + } + + \begin{function}{\definiendum,\definame,\Definame} + \stexcode"sdefinition" (and \stexcode"sparagraph" with + |type=symdoc|) introduce three new macros: + \stexcode"definiendum" behaves like \stexcode"symref" + (and \stexcode"definame"/\stexcode"Definame" + like \stexcode"symname"/\stexcode"Symname", respectively), + but highlights the referenced symbol as \emph{being defined} + in the current definition. + \end{function} + + \begin{mmtbox} + The special |type=symdoc| for \stexcode"sparagraph" is intended to be used for + ``informal definitions'', or encyclopedia-style descriptions for symbols. + + The \mmt system can use those (in lieu of an actual \stexcode"sdefinition" in scope) + to present to users, e.g. when hovering over symbols. + \end{mmtbox} + + \begin{function}{\definiens} + Additionally, \stexcode"sdefinition" (and \stexcode"sparagraph" with + |type=symdoc|) introduces \stexcode"\definiens[<optional symbolname>]{<code>}" + which marks up |<code>| as being the explicit \emph{definiens} + of |<optional symbolname>| (in case |for=| has multiple symbols). + \end{function} + + All four statement environments -- i.e. \stexcode|sdefinition|, + \stexcode|sassertion|, \stexcode|sexample|, and \stexcode|sparagraph| -- also take an + optional parameter |name=| -- if this one is given a value, the environment will + generate a \emph{symbol} by that name (but with no semantic macro). Not only does this + allow for \stexcode"\symref" et al, it allows us to resume our earlier example for + monoids much more nicely:\ednote{MK: we should reference the example explicitly here.} + + \symdef{set}{\comp{\texttt{Set}}} + \symdef{equal}[args=2]{#1 \comp= #2} + \symdef{inset}[args=2]{#1 \comp\in #2} + \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2} + + \stexexample{% +\begin{mathstructure}{monoid} + \symdef{universe}[type=\set]{\comp{U}} + \symdef{op}[ + args=2, + type=\funtype{\universe,\universe}{\universe}, + op=\circ + ]{#1 \comp{\circ} #2} + \symdef{unit}[type=\universe]{\comp{e}} + + \begin{sparagraph}[type=symdoc,for=monoid] + A \definame{monoid} is a structure + $\mathstruct{\universe,\op!,\unit}$ + where $\op!:\funtype{\universe}{\universe}$ and + $\inset{\unit}{\universe}$ such that + + \begin{sassertion}[name=associative, + type=axiom, + title=Associativity] + $\op!$ is associative + \end{sassertion} + \begin{sassertion}[name=isunit, + type=axiom, + title=Unit] + $\equal{\op{\svar{x}}{\unit}}{\svar{x}}$ + for all $\inset{\svar{x}}{\universe}$ + \end{sassertion} + \end{sparagraph} +\end{mathstructure} + +An example for a \symname{monoid} is... + } + + The main difference to before\ednote{MK: reference} is that the two + \stexcode|sassertion|s now have |name=| attributes. Thus the \stexcode"mathstructure" + \symname{monoid} now contains two additional symbols, namely the axioms for + associativity and that $e$ is a unit. Note that both symbols do not represent the mere + \emph{propositions} that e.g. $\circ$ is associative, but \emph{the assertion that it + is actually true} that $\circ$ is associative. + + If we now want to instantiate |monoid| (unless with a variable, + of course), we also need to assign |associative| and |neutral| + to analogous assertions. So the earlier example + \begin{latexcode}[gobble=8] + \instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[ + universe = Int , + op = addition , + unit = zero + ] + \end{latexcode} + ...will not work anymore. We now need to give assertions that + |addition| is associative and that |zero| is a unit with respect + to addition.\footnote{Of course, \sTeX can not check that + the assertions are the ``correct'' ones -- but if + the assertions (both in |monoid| as well as those for addition and + zero) are properly marked up, \mmt can. \textcolor{red}{TODO: should}} + +\end{smodule} +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: sec.customhighlight a,prec additionandmultiplication.ex trivial,boring +% LocalWords: addition,multiplication symdoc symdoc,for isunit diff --git a/macros/latex/contrib/stex/doc/packages/stex-symbols.tex b/macros/latex/contrib/stex/doc/packages/stex-symbols.tex index 50b450a248..e7bafeda6b 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-symbols.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-symbols.tex @@ -1 +1,587 @@ -\textcolor{red}{TODO: symbols documentation}
\ No newline at end of file +\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{SymbolsAndNotations} +\begin{sfragment}{Declaring New Symbols and Notations} + Inside an \stexcode"smodule" environment, we can declare new \sTeX symbols. + +\begin{function}{\symdecl} + The most basic command for doing so is using \stexcode"\symdecl{symbolname}". This + introduces a new symbol with name |symbolname|, arity $0$ and semantic macro + \stexcode"\symbolname". + + The starred variant \stexcode"\symdecl*{symbolname}" will declare a symbol, but not + introduce a semantic macro. If we don't want to supply a notation (for example to + introduce concepts like ``abelian'', which is not something that has a notation), the + starred variant is likely to be what we want. +\end{function} +\begin{mmtbox} + \stexcode"\symdecl" introduces a new \omdoc/\mmt constant in the current module + (=\omdoc/\mmt theory). Correspondingly, they get assigned the URI + |<module-URI>?<constant-name>|. +\end{mmtbox} + +Without a semantic macro or a notation, the only meaningful way to reference a symbol is +via \stexcode"\symref",\stexcode"\symname" etc. + +\stexexample{% +\symdecl*{foo} +Given a \symname{foo}, we can... +} + +Obviously, most semantic macros should take actual \emph{arguments}, implying that the +symbol we introduce is an \emph{operator} or \emph{function}. We can let +\stexcode"\symdecl" know the \emph{arity} (i.e. number of arguments) of a symbol like +this: + +\stexexample{% +\symdecl{binarysymbol}[args=2] +\symref{binarysymbol}{this} is a symbol taking two arguments. +} + +So far we have gained exactly \ldots nothing by adding the arity information: we cannot do +anything with the arguments in the text. + +We will now see what we can gain with more machinery. + +\begin{function}{\notation} + We probably want to supply a notation as well, in which case we can finally actually use + the semantic macro in math mode. We can do so using the \stexcode"\notation" command, + like this: + +\stexexample{% +\notation{binarysymbol}{\text{First: }#1\text{; Second: }#2} +$\binarysymbol{a}{b}$ } +\end{function} + +\begin{mmtbox} + Applications of semantic macros, such as \stexcode"\binarysymbol{a}{b}" are translated + to \mmt/\omdoc as |OMA|-terms with head |<OMS name="...?binarysymbol"/>|. + + Semantic macros with no arguments correspond to |OMS| directly. +\end{mmtbox} + +\begin{function}{\comp} + For many semantic services e.g. semantic highlighting or \defemph{wikification} (linking + user-visible notation components to the definition of the respective symbol they come + from), we need to specify the notation components. Unfortunately, there is currently no + way the \sTeX engine can infer this by itself, so we have to specify it manually in the + notation specification. We can do so with the \stexcode"\comp" command. +\end{function} + +We can introduce a new notation |highlight| for \stexcode"\binarysymbol" that fixes this +flaw, which we can subsequently use with \stexcode"\binarysymbol[highlight]": + +\stexexample{% +\notation{binarysymbol}[highlight] + {\comp{\text{First: }}#1\comp{\text{; Second: }}#2} +$\binarysymbol[highlight]{a}{b}$ +} + +\begin{dangerbox} + Ideally, \stexcode"\comp" would not be necessary: Everything in a notation that is + \emph{not} an argument should be a notation component. Unfortunately, it is + computationally expensive to determine where an argument begins and ends, and the + argument markers |#n| may themselves be nested in other macro applications or + \TeX\xspace groups, making it ultimately almost impossible to determine them + automatically while also remaining compatible with arbitrary highlighting customizations + (such as tooltips, hyperlinks, colors) that users might employ, and that are ultimately + invoked by \stexcode"\comp". +\end{dangerbox} + +\begin{dangerbox} + Note that it is required that + \begin{enumerate} + \item the argument markers |#n| never occur inside a \stexcode"\comp", and + \item no semantic arguments may ever occur inside a notation. + \end{enumerate} + Both criteria are not just required for technical reasons, but conceptionally + meaningful: + + The underlying principle is that the arguments to a semantic macro represent + \emph{arguments to the mathematical operation} represented by a symbol. For example, a + semantic macro \stexcode"\addition{a}{b}" taking two arguments would represent \emph{the + actual addition of (mathematical objects) $a$ and $b$}. It should therefore be + impossible for $a$ or $b$ to be part of a notation component of \stexcode"\addition". + + Similarly, a semantic macro can not conceptually be part of the notation of + \stexcode"\addition", since a semantic macro represents a \emph{distinct mathematical + concept} with \emph{its own semantics}, whereas notations are syntactic + representations of the very symbol to which the notation belongs. + + If you want an argument to a semantic macro to be a purely syntactic parameter, then you + are likely somewhat confused with respect to the distinction between the precise + \emph{syntax} and \emph{semantics} of the symbol you are trying to declare (which + happens quite often even to experienced \sTeX users), and might want to give those + another thought - quite likely, the macro you aim to implement does not actually + represent a semantically meaningful mathematical concept, and you will want to use + \stexcode"\def" and similar native \LaTeX\xspace macro definitions rather than semantic + macros. +\end{dangerbox} + +\begin{function}{\symdef} + In the vast majority of cases where a symbol declaration should come with a semantic + macro, we will want to supply a notation immediately. For that reason, the + \stexcode"\symdef" command combines the functionality of both \stexcode"\symdecl" and + \stexcode"\notation" with the optional arguments of both: +\end{function} + +\stexexample{% +\symdef{newbinarysymbol}[hl,args=2] + {\comp{\text{1.: }}#1\comp{\text{; 2.: }}#2} +$\newbinarysymbol{a}{b}$ +} + +We just declared a new symbol |newbinarysymbol| with |args=2| and immediately provided it +with a notation with identifier |hl|. Since |hl| is the \emph{first} (and so far, only) +notation supplied for |newbinarysymbol|, using \stexcode"\newbinarysymbol" without +optional argument defaults to this notation.\bigskip + +But one man's meat is another man's poison: it is very subjective what the ``default +notation'' of an operator should be. Different communities have different practices. For +instance, the complex unit is written as $i$ in Mathematics and as $j$ in electrical +engineering. So to allow modular specification and facilitate re-use of document fragments +\sTeX allows to re-set notation defaults. + +\begin{function}{\setnotation} + The first notation provided will stay the default notation unless explicitly changed -- + this is enabled by the \stexcode"\setnotation" command: + \stexcode"\setnotation{symbolname}{notation-id}" sets the default notation of + \stexcode"\symbolname" to |notation-id|, i.e. henceforth, \stexcode"\symbolname" behaves + like \stexcode"\symbolname[notation-id]" from now on. +\end{function} + +Often, a default notation is set right after the corresponding notation is introduced -- +the starred version \stexcode"\notation*" for that reason introduces a new notation and +immediately sets it to be the new default notation. So expressed differently, the +\emph{first} \stexcode"\notation" for a symbol behaves exactly like \stexcode"\notation*", +and \stexcode"\notation*{foo}[bar]{...}" behaves exactly like +\stexcode"\notation{foo}[bar]{...}\setnotation{foo}{bar}". + +\begin{function}{\textsymdecl} + In the less mathematical settings where we want a symbol and + semantic macro for some concept with a notation \emph{beyond} + its mere name, but which should also be available in \TeX's text + mode, the command \stexcode"\textsymdecl" is useful. + For example, we can declare a symbol \stexcode"openmath" + with the notation \stexcode"\textsc{OpenMath}" using + \textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}} + \stexcode"\textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}}". + The \stexcode"\openmath" yields \openmath both in text and math + mode. +\end{function} + +\begin{sfragment}{Operator Notations} + Once we have a semantic macro with arguments, such as \stexcode"\newbinarysymbol", the + semantic macro represents the \emph{application} of the symbol to a list of + arguments. What if we want to refer to the operator \emph{itself}, though? + + We can do so by supplying the \stexcode"\notation" (or \stexcode"\symdef") with an + \emph{operator notation}, indicated with the optional argument |op=|. We can then + invoke the operator notation using \stexcode"\symbolname![notation-identifier]". Since + operator notations never take arguments, we do not need to use \stexcode"\comp" in it, + the whole notation is wrapped in a \stexcode"\comp" automatically: + + \stexexample{% + \notation{newbinarysymbol}[ab, op={\text{a:}\cdot\text{; b:}\cdot}] + {\comp{\text{a:}}#1\comp{\text{; b:}}#2} \symname{newbinarysymbol} is also + occasionally written $\newbinarysymbol![ab]$ + } + + \begin{mmtbox} + \stexcode"\symbolname!" is translated to \omdoc/\mmt as |<OMS name="...?symbolname"/>| + directly. + \end{mmtbox} + +\end{sfragment} +\end{sfragment} + +\begin{sfragment}{Argument Modes} + The notations so far used \emph{simple} arguments which we call \emph{mode}-|i| + arguments. Declaring a new symbol with \stexcode"\symdecl{foo}[args=3]" is equivalent to + writing \stexcode"\symdecl{foo}[args=iii]", indicating that the semantic macro takes + three mode-|i| arguments. However, there are three more argument modes which we will + investigate now, namely mode-|b|, mode-|a| and mode-|B| arguments. + +\begin{sfragment}{Mode-\texttt b Arguments} + +A mode-|b| argument represents a \emph{variable} that is \emph{bound} by the symbol in +its application, making the symbol a \emph{binding operator}. Typical examples of +binding operators are e.g. sums $\sum$, products $\prod$, integrals $\int$, quantifiers +like $\forall$ and $\exists$, that $\lambda$-operator, etc. + +\begin{mmtbox} + Mode-|b| arguments behave exactly like mode-|i| arguments within \TeX, but applications + of binding operators, i.e. symbols with mode-|b| arguments, are translated to + |OMBIND|-terms in \omdoc/\mmt, rather than |OMA|. +\end{mmtbox} + +For example, we can implement a summation operator binding an index variable and taking +lower and upper index bounds and the expression to sum over like this: + +\stexexample{% +\symdef{summation}[args=biii] + {\mathop{\comp{\sum}}_{#1\comp{=}#2}^{#3}#4} + $\summation{\svar{x}}{1}{\svar{n}}{\svar{x}}^2$ +} + +where the variable $\svar{x}$ is now \emph{bound} by the \stexcode"\summation"-symbol in +the expression. +\end{sfragment} + +\begin{sfragment}{Mode-\texttt a Arguments} + Mode-|a| arguments represent a \emph{flexary argument sequence}, i.e. a sequence of + arguments of arbitrary length. Formally, operators that take arbitrarily many arguments + don't ``exist'', but in informal mathematics, they are ubiquitous. Mode-|a| arguments + allow us to write e.g. \stexcode"\addition{a,b,c,d,e}" rather than having to write + something like \stexcode"\addition{a}{\addition{b}{\addition{c}{\addition{d}{e}}}}"! + + \stexcode"\notation" (and consequently \stexcode"\symdef", too) take one additional + argument for each mode-|a| argument that indicates how to ``accumulate'' a + comma-separated sequence of arguments. This is best demonstrated on an example. + + Let's say we want an operator representing quantification over an ascending chain of + elements in some set, i.e. \stexcode"\ascendingchain{S}{a,b,c,d,e}{t}" should yield + $\forall a{<_S}b{<_S}c{<_S}d{<_S}e.\,t$. The ``base''-notation for this operator is + simply\\ \stexcode"{\comp{\forall} #2\comp{.\,}#3}", where |#2| represents the full + notation fragment \emph{accumulated} from |{a,b,c,d,e}|. + + The \emph{additional} argument to \stexcode"\notation" (or \stexcode"\symdef") takes the + same arguments as the base notation and two \emph{additional} arguments |##1| and |##2| + representing successive pairs in the mode-|a| argument, and accumulates them into |#2|, + i.e. to produce $a<_Sb<_Sc<_Sd<_Se$, we do \stexcode"{##1 \comp{<}_{#1} ##2}": + + \stexexample{% +\symdef{ascendingchain}[args=iai] + {\comp{\forall} #2\comp{.\,}#3} + {##1 \comp{<}_{#1} ##2} + +Tadaa: $\ascendingchain{S}{a,b,c,d,e}{t}$ +} + +If this seems overkill, keep in mind that you will rarely need the single-hash arguments +|#1|,|#2| etc. in the |a|-notation-argument. For a much more representative and simpler +example, we can introduce flexary addition via: +\stexexample{% + \symdef{addition}[args=a]{#1}{##1 \comp{+} ##2} + +Tadaa: $\addition{a,b,c,d,e}$ +} + +\begin{sfragment}{The \texttt{assoc}-key} + We mentioned earlier that ``formally'', flexary arguments don't really + ``exist''. Indeed, formally, addition is usually defined as a binary operation, + quantifiers bind a single variable etc. + + Consequently, we can tell \sTeX (or, rather, \mmt/\omdoc) how to ``resolve'' flexary + arguments by providing \stexcode"\symdecl" or \stexcode"\symdef" with an optional + |assoc|-argument, as in \stexcode"\symdecl{addition}[args=a,assoc=bin]". The possible + values for the |assoc|-key are: + \begin{itemize} + \item[|bin|:] A binary, associative argument, e.g. as in \stexcode"\addition" + \item[|binl|:] A binary, left-associative argument, e.g. + $a^{\scriptstyle b^{\scriptstyle c^d}}$, which stands for $((a^b)^c)^d$ + \item[|binr|:] A binary, right-associative argument, e.g. as in $A\to B\to C\to D$, + which stands for $A \to (B \to (C \to D))$ + \item[|pre|:] Successively prefixed, e.g. as in $\forall x,y,z.\,P$, which stands for + $\forall x.\, \forall y.\, \forall z.\,P$ + \item[|conj|:] Conjunctive, e.g. as in $a=b=c=d$ or $a,b,c,d\in A$, which stand for + $a=d\wedge b=d\wedge c=d$ and $a\in A\wedge b\in A \wedge c\in A\wedge d\in A$, + respectively + \item[|pwconj|:] Pairwise conjunctive, e.g. as in $a\neq b\neq c\neq d$, which stands + for $a\neq b\wedge a\neq c\wedge a\neq d\wedge b\neq c\wedge b\neq d\wedge c\neq d$ + \end{itemize} + As before, at the PDF level, this annotation is invisible (and without effect), but at + the level of the generated OMDoc/MMT this leads to more semantical expressions. +\end{sfragment} +\end{sfragment} + +\begin{sfragment}{Mode-\texttt B Arguments} + Finally, mode-|B| arguments simply combine the functionality of both |a| and |b| - + i.e. they represent an arbitrarily long sequence of variables to be bound, e.g. for + implementing quantifiers: + + \stexexample{% +\symdef{quantforall}[args=Bi] + {\comp{\forall}#1\comp{.}#2} + {##1\comp,##2} + +$\quantforall{\svar{x},\svar{y},\svar{z}}{P}$ +} +\end{sfragment} +\end{sfragment} + +\begin{sfragment}{Type and Definiens Components} + \stexcode"\symdecl" and \stexcode"\symdef" take two more optional arguments. \TeX\xspace + largely ignores them (except for special situations we will talk about later), but \mmt + can pick up on them for additional services. These are the |type| and |def| keys, which + expect expressions in math-mode (ideally using semantic macros, of course!) + + \begin{mmtbox} + The |type| and |def| keys correspond to the |type| and |definiens| components of + \omdoc/\mmt constants. + + Correspondingly, the name ``type'' should be taken with a grain of salt, since + \omdoc/\mmt -- being foundation-independent -- does not a priori implement a fixed + typing system. + \end{mmtbox} + + \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2} + \symdef{fun}[args=bi]{#1 \comp\mapsto #2} + \symdef{set}{\comp{\texttt{Set}}} + + The |type|-key allows us to provide additional information + (given the necessary \sTeX symbols), e.g. for + addition on natural numbers: + + \stexexample{% +\symdef{Nat}[type=\set]{\comp{\mathbb N}} +\symdef{addition}[ + type=\funtype{\Nat,\Nat}{\Nat}, + op=+, + args=a +]{#1}{##1 \comp+ ##2} + +\symname{addition} is an operation $\funtype{\Nat,\Nat}{\Nat}$ +} + +The |def|-key allows for declaring symbols as abbreviations: +\stexexample{% +\symdef{successor}[ + type=\funtype{\Nat}{\Nat}, + def=\fun{\svar{x}}{\addition{\svar{x},1}}, + op=\mathtt{succ}, + args=1 +]{\comp{\mathtt{succ(}#1\comp{)}}} + +The \symname{successor} operation $\funtype{\Nat}{\Nat}$ +is defined as $\fun{\svar{x}}{\addition{\svar{x},1}}$ +} +\end{sfragment} + +\begin{sfragment}{Precedences and Automated Bracketing} + Having done \stexcode"\addition", the obvious next thing to implement is + \stexcode"\multiplication". This is straight-forward in theory: + + \stexexample{% +\symdef{multiplication}[ + type=\funtype{\Nat,\Nat}{\Nat}, + op=\cdot, + args=a +]{#1}{##1 \comp\cdot ##2} + +\symname{multiplication} is an operation $\funtype{\Nat,\Nat}{\Nat}$ +} + +However, if we \emph{combine} \stexcode"\addition" and \stexcode"\multiplication", we +notice a problem: + +\stexexample{% +$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ +} + +We all know that $\multiplication!$ binds stronger than $\addition!$, so the output +$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ does not actually +reflect the term we wrote. We can of course insert parentheses manually + +\stexexample{% +$\addition{a,\multiplication{b,(\addition{c,\multiplication{d,e}})}}$ +} +but we can also do better by supplying \emph{precedences} and +have \sTeX insert parentheses automatically. + +For that purpose, \stexcode"\notation" (and hence \stexcode"\symdef") take an optional +argument |prec=<opprec>;<argprec1>x...x<argprec n>|. + +We will investigate the precise meaning of |<opprec>| and the |<argprec>|s shortly -- in +the vast majority of cases, it is perfectly sufficient to think of |prec=| taking a single +number and having that be \emph{the} precedence of the notation, where lower precedences +(somewhat counterintuitively) bind stronger than higher precedences. So fixing our +notations for \stexcode"\addition" and \stexcode"\multiplication", we get: + +\stexexample{% +\notation{multiplication}[ + op=\cdot, + prec=50 +]{#1}{##1 \comp\cdot ##2} +\notation{addition}[ + op=+, + prec=100 +]{#1}{##1 \comp+ ##2} + +$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ +} + +Note that the precise numbers used for precedences are pretty arbitrary - what matters is +which precedences are higher than which other precedences when used in conjunction. +\begin{variable}{\infprec,\neginfprec} + It is occasionally useful to have ``infinitely'' high or low precedences to enforce or + forbid automated bracketing entirely -- for those purposes, \stexcode"\infprec" and + \stexcode"\neginfprec" exist (which are implemented as the maximal and minimal integer + values accordingly). +\end{variable} + +\begin{dangerbox} + More precisely, each notation takes + \begin{enumerate} + \item One \emph{operator precedence} and + \item one \emph{argument precedence} for each argument. + \end{enumerate} + By default, all precedences are $0$, unless the symbol takes no argument, in which case + the operator precedence is \stexcode"\neginfprec" (negative infinity). If we only + provide a single number, this is taken as both the operator precedence and all argument + precedences. + + \sTeX decides whether to insert parentheses by comparing operator precedences to a + \emph{downward precedence} $p_d$ with initial value \stexcode"\infprec". When + encountering a semantic macro, \sTeX takes the operator precedence $p_{op}$ of the + notation used and checks whether $p_{op}>p_d$. If so, \sTeX insert parentheses. + + When \sTeX steps into an argument of a semantic macro, it sets $p_d$ to the respective + argument precedence of the notation used. + + In the example above: + \begin{enumerate} + \item \sTeX starts out with $p_d=$\stexcode"\infprec". + \item \sTeX encounters \stexcode"\addition" with $p_{op}=100$. Since + $100\not>$\stexcode"\infprec", it inserts no parentheses. + \item Next, \sTeX encounters the two arguments for \stexcode"\addition". Both have no + specifically provided argument precedence, so \sTeX uses $p_d=p_{op}=100$ for both and + recurses. + \item Next, \sTeX encounters \stexcode"\multiplication{b,...}", whose notation has + $p_{op}=50$. + \item We compare to the current downward precedence $p_d$ set by \stexcode"\addition", + arriving at $p_{op}=50\not>100=p_d$, so \sTeX again inserts no parentheses. + \item Since the notation of \stexcode"\multiplication" has no explicitly set argument + precedences, \sTeX uses the operator precedence for all arguments of + \stexcode"\multiplication", hence sets $p_d=p_{op}=50$ and recurses. + \item Next, \sTeX encounters the inner \stexcode"\addition{c,...}" whose notation has + $p_{op}=100$. + \item We compare to the current downward precedence $p_d$ set by + \stexcode"\multiplication", arriving at $p_{op}=100>50=p_d$ -- which finally prompts + \sTeX to insert parentheses, and we proceed as before. + \end{enumerate} +\end{dangerbox} +\end{sfragment} + +\begin{sfragment}{Variables} + All symbol and notation declarations require a module with which they are associated, + hence the commands \stexcode"\symdecl", \stexcode"\notation", \stexcode"\symdef" + etc. are disabled outside of |smodule|-environments. + + Variables are different -- variables are allowed everywhere, are not exported when the + current module (if one exists) is imported (via \stexcode"\importmodule" or + \stexcode"\usemodule") and (also unlike symbol declarations) ``disappear'' at the end of + the current \TeX\xspace group. + + \begin{function}{\svar} + So far, we have always used variables using \stexcode"\svar{n}", which marks-up $n$ as + a variable with name |n|. More generally, \stexcode"\svar[foo]{<texcode>}" marks-up + the arbitrary |<texcode>| as representing a variable with name |foo|. + \end{function} + + Of course, this makes it difficult to reuse variables, or introduce ``functional'' + variables with arities $>0$, or provide them with a type or definiens. + + \begin{function}{\vardef} + For that, we can use the \stexcode"\vardef" command. Its syntax is largely the same as + that of \stexcode"\symdef", but unlike symbols, variables have only one notation + (\textcolor{red}{TODO: so far?}), hence there is only \stexcode"\vardef" and no + \stexcode"\vardecl". + \end{function} + +\stexexample{% +\vardef{varf}[ + name=f, + type=\funtype{\Nat}{\Nat}, + op=f, + args=1, + prec=0;\neginfprec +]{\comp{f}#1} +\vardef{varn}[name=n,type=\Nat]{\comp{n}} +\vardef{varx}[name=x,type=\Nat]{\comp{x}} + +Given a function $\varf!:\funtype{\Nat}{\Nat}$, +by $\addition{\varf!,\varn}$ we mean the function +$\fun{\varx}{\varf{\addition{\varx,\varn}}}$ +} + +(of course, ``lifting'' addition in the way described in the previous example is an +operation that deserves its own symbol rather than abusing \stexcode"\addition", +but... well.) + +\textcolor{red}{TODO: bind=forall/exists} +\end{sfragment} + +\begin{sfragment}{Variable Sequences} + Variable \emph{sequences} occur quite frequently in informal mathematics, hence they + deserve special support. Variable sequences behave like variables in that they disappear + at the end of the current \TeX\xspace group and are not exported from modules, but their + declaration is quite different. + + \begin{function}{\varseq} + A variable sequence is introduced via the command \stexcode"\varseq", which takes the + usual optional arguments |name| and |type|. It then takes a starting index, an end + index and a \emph{notation} for the individual elements of the sequence parametric in + an index. Note that both the starting as well as the ending index may be variables. + \end{function} + + This is best shown by example: + \stexexample{% +\vardef{varn}[name=n,type=\Nat]{\comp{n}} +\varseq{seqa}[name=a,type=\Nat]{1}{\varn}{\comp{a}_{#1}} + +The $i$th index of $\seqa!$ is $\seqa{i}$. +} + +Note that the syntax |\seqa!| now automatically generates a presentation based on the +starting and ending index. + +\textcolor{red}{TODO: more notations for invoking sequences}. + +\vardef{varn}[name=n,type=\Nat]{\comp{n}} +\varseq{seqa}[name=a]{1}{\varn}{\comp{a}_{#1}} + +Notably, variable sequences are nicely compatible with |a|-type arguments, so we can do +the following: + +\stexexample{% +$\addition{\seqa}$ +} + +Sequences can be \emph{multidimensional} using the |args|-key, in which case the +notation's arity increases and starting and ending indices have to be provided as a +comma-separated list: + +\stexexample{% +\vardef{varm}[name=m,type=\Nat]{\comp{m}} +\varseq{seqa}[ + name=a, + args=2, + type=\Nat, +]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}} + +$\seqa!$ and $\addition{\seqa}$ +} +\vardef{varm}[name=m,type=\Nat]{\comp{m}} + +We can also explicitly provide a ``middle'' segment to be used, like such: + +\stexexample{% +\varseq{seqa}[ + name=a, + type=\Nat, + args=2, + mid={\comp{a}_{\varn}^1,\comp{a}_1^2,\ellipses,\comp{a}_{1}^{\varm}} +]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}} + +$\seqa!$ and $\addition{\seqa}$ +} +\end{sfragment} +\end{smodule} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: binarysymbol newbinarysymbol hl,args a,b,c,d,e ascendingchain assoc binl +% LocalWords: a,assoc binr x,y,z conj a,b,c,d pwconj funtype succ prec opprec argprec1 +% LocalWords: argprec texcode varf varn n,type varx x,type varseq seqa a,type th m,type diff --git a/macros/latex/contrib/stex/doc/packages/stex-terms.tex b/macros/latex/contrib/stex/doc/packages/stex-terms.tex index cc67ce0c7f..759b3f5fdd 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-terms.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-terms.tex @@ -1 +1,177 @@ -\textcolor{red}{TODO: terms documentation}
\ No newline at end of file +\begin{smodule}{SymbolsInText} + \symdef{set}{\comp{\texttt{Set}}} + + Given a symbol declaration \stexcode"\symdecl{symbolname}", + we obtain a semantic macro \stexcode"\symbolname". + We can use this semantic macro in math mode to use its notation(s), + and we can use \stexcode"\symbolname!" + in math mode to use its operator notation(s). + What else can we do? + +\begin{sfragment}{\texttt{\textbackslash symref} and its variants} + + \begin{function}{\symref,\symname} + We have already seen \stexcode"\symname" and + \stexcode"\symref", the latter being the more general. + + \stexcode"\symref{<symbolname>}{<code>}" marks-up |<code>| + as referencing |<symbolname>|. Since quite often, the |<code>| + should be (a variant of) the name of the symbol anyway, + we also have \stexcode"\symname{<symbolname>}". + \end{function} + + Note that \stexcode"\symname" uses the \emph{name} + of a symbol, not its macroname. More precisely, + \stexcode"\symname" will insert the name of the symbol + with ``|-|'' replaced by spaces. + If a symbol does not have + an explicit |name=| given, the two are equal -- but + for \stexcode"\symname" it often makes sense to make the + two explicitly distinct. For example: + \stexexample{% +\symdef{Nat}[ + name=natural-number, + type=\set +]{\comp{\mathbb{N}}} + +A \symname{Nat} is... + } + + \stexcode"\symname" takes two additional optional + arguments, |pre=| and |post=| that get prepended or appended + respectively to the symbol name. + + \begin{function}{\Symname} + Additionally, \stexcode"\Symname" behaves exactly + like \stexcode"\symname", but will capitalize the first + letter of the name: + \end{function} + \stexexample{% +\Symname[post=s]{Nat} are... + } + + \begin{dangerbox} + This is as good a place as any other to explain how + \sTeX resolves a string |symbolname| to an actual symbol. + + If \stexcode"\symbolname" is a semantic macro, then + \sTeX has no trouble resolving |symbolname| to the full + URI of the symbol that is being invoked. + + However, especially in \stexcode"\symname" (or if a symbol + was introduced using \stexcode"\symdecl*" without + generating a semantic macro), we might + prefer to use the \emph{name} of a symbol directly for + readability -- e.g. we would want to write + \stexcode"A \symname{natural-number} is..." rather than + \stexcode"A \symname{Nat} is...". \sTeX attempts to handle + this case thusly: + + If |string| does \emph{not} correspond to a semantic + macro \stexcode"\string" and does \emph{not} + contain a |?|, then \sTeX checks + all symbols currently in scope until it finds one, + whose name is |string|. If |string| is of the + form |pre?name|, \sTeX first looks through all modules + currently in scope, whose full URI ends with |pre|, + and then looks for a symbol with name |name| in those. + This allows + for disambiguating more precisely, e.g. by + saying \stexcode"\symname{Integers?addition}" + or \stexcode"\symname{RealNumbers?addition}" in the + case where several |addition|s are in scope. + \end{dangerbox} +\end{sfragment} + +\symdef{addition}[op=+,prec=100,args=2]{#1 \comp+ #2} +\symdef{multiplication}[op=\cdot,prec=50,args=a]{#1}{##1 \comp\cdot ##2} + +\begin{sfragment}{Marking Up Text and On-the-Fly Notations} + We can also use semantic macros outside of text mode though, + which allows us to annotate arbitrary text fragments. + + Let us assume again, that we have + \stexcode"\symdef{addition}[args=2]{#1 \comp+ #2}". Then we + can do + \stexexample{% +\addition{\comp{The sum of} \arg{$\svar{n}$} \comp{ and }\arg{$\svar{m}$}} +is... + } + ...which marks up the text fragment as representing + an \emph{application} of the |addition|-symbol to two + argument $\svar{n}$ and $\svar{m}$. + + \begin{mmtbox} + As expected, the above example is translated to \omdoc/\mmt + as an |OMA| with |<OMS name="...?addition"/>| as head and + |<OMV name="n"/>| and |<OMV name="m"/>| as arguments. + \end{mmtbox} + + \begin{dangerbox} + Note the difference in treating ``arguments'' between math mode and text mode. In + math mode the (in this case two) tokens/groups following the \stexcode|\addition| + macro are treated as arguments to the addition function, whereas in text mode the + group following \stexcode|\addition| is taken to be the ad-hoc presentation. We + drill in on this now. + \end{dangerbox} + + \begin{function}{\arg} + In text mode, every semantic macro takes exactly one + argument, namely the text-fragment to be annotated. + The \stexcode"\arg" command is only valid within the + argument to a semantic macro and marks up the + \emph{individual arguments} for the symbol. + \end{function} + + We can also use semantic macros in text mode to invoke + an operator itself instead of its application, with the + usual syntax using |!|: + \stexexample{% +\addition!{Addition} is... + } + + Indeed, \stexcode"\symbolname!{<code>}" is exactly equivalent to + \stexcode"\symref{symbolname}{<code>}" (the latter is in fact implemented in terms of + the former). + + \stexcode"\arg" also allows us to switch the order of arguments + around and ``hide'' arguments: For example, \stexcode"\arg[3]{<code>}" + signifies that |<code>| represents the \emph{third} + argument to the current operator, and \stexcode"\arg*[i]{<code>}" + signifies that |<code>| represents the $i$th argument, but it + should not produce any output (it is exported in the |xhtml| + however, so that \mmt and other systems can pick up on it).\ednote{MK: I do not + understand why we have to/want to give the second arg*; I think this must be + elaborated on.} + \stexexample{% +\addition{\comp{adding} + \arg[2]{$\svar{k}$} + \arg*{$\addition{\svar{n}}{\svar{m}}$}} yields... + } + Note that since the second \stexcode"\arg" has no explicit argument + number, it automatically represents the first not-yet-given + argument -- i.e. in this case the first one.\ednote{MK: I do not understand this at + all. } + + \paragraph{} The same syntax can be used in math mod as well. This allows us to + spontaneously introduce new notations on the fly. We can activate it using the starred + variants of semantic macros: + + \stexexample{% +Given $\addition{\svar{n}}{\svar{m}}$, then +$\addition*{ + \arg*{\addition{\svar{n}}{\svar{m}}} + \comp{+} + \arg{\svar{k}} +}$ yields... + } + +\end{sfragment} +\end{smodule} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: prec cdot,prec 50,args th diff --git a/macros/latex/contrib/stex/doc/packages/stex-tikzinput.tex b/macros/latex/contrib/stex/doc/packages/stex-tikzinput.tex index fb7d0c1e5b..ac321f129c 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-tikzinput.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-tikzinput.tex @@ -1 +1,61 @@ -\textcolor{red}{TODO: tikzinput documentation}
\ No newline at end of file +\begin{function}{image} + The behavior of the \pkg{ikzinput} package is determined by whether the |image| option + is given. If it is not, then the \pkg{tikz} package is loaded, all other options are + passed on to it and |\tikzinput{|\meta{file}|}| inputs the TIKZ file \meta{file}|.tex|; + if not, only the \pkg{graphicx} package is loaded and |\tikzinput{|\meta{file}|}| loads + an image file \meta{file}|.|\meta{ext} generated from \meta{file}|.tex|. +\end{function} + +The selective input functionality of the \pkg{tikzinput} package assumes that the TIKZ +pictures are externalized into a standalone picture file, such as the following one + +\begin{latexcode} +\documentclass{standalone} +\usepackage{tikz} +\usetikzpackage{...} +\begin{document} + \begin{tikzpicture} + ... + \end{tikzpicture} +\end{document} +\end{latexcode} + + The \pkg{standalone} class is a minimal {\LaTeX} class that when loaded in a document + that uses the \pkg{standalone} package: the preamble and the |documenat| environment + are disregarded during loading, so they do not pose any problems. In effect, an + |\input| of the file above only sees the |tikzpicture| environment, but the file itself + is standalone in the sense that we can run {\LaTeX} over it separately, e.g. for + generating an image file from it. + +\begin{function}{\tikzinput,\ctikzinput} + This is exactly where the \pkg{tikzinput} package comes in: it supplies the |\tikzinput| + macro, which -- depending on the |image| option -- either directly inputs the TIKZ + picture (source) or tries to load an image file generated from it. + + Concretely, if the |image| option is not set for the \pkg{tikzinput} package, then + |\tikzinput[|\meta{opt}|]{|\meta{file}|}| disregards the optional argument \meta{opt} + and inputs \meta{file}|.tex| via |\input| and resizes it to as specified in the |width| + and |height| keys. If it is, |\tikzinput[|\meta{opt}|]{|\meta{file}|}| expands to + |\includegraphics[|\meta{opt}|]{|\meta{file}|}|. + + |\ctizkinput| is a version of |\tikzinput| that is centered. +\end{function} + +\begin{function}{\mhtikzinput,\cmhtikzinput} + |\mhtizkinput| is a variant of |\tikzinput| that treats its file path argument as a + relative path in a math archive in analogy to \stexcode|\inputref|. To give the archive + path, we use the |mhrepos=| key. Again, |\cmhtizkinput| is a version of |\mhtikzinput| + that is centered. +\end{function} + +\begin{function}{\libusetikzlibrary} + Sometimes, we want to supply archive-specific TIKZ libraries in the |lib| folder of the + archive or the |meta-inf/lib| of the archive group. Then we need an analogon to + \stexcode|\libinput| for \stexcode|\usetikzlibrary|. The \pkg{stex-tikzinput} package + provides the \stexcode|libusetikzlibrary| for this purpose. +\end{function} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: |