diff options
author | Karl Berry <karl@freefriends.org> | 2019-03-20 22:31:24 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2019-03-20 22:31:24 +0000 |
commit | 2b006ec0e0cafe12255f874f9c44786ab6f38901 (patch) | |
tree | c40f5796e1b34e3f051abd84d049e092e4ffd0ab /Master/texmf-dist/source/latex/stex/structview | |
parent | 8e508e8b0218f17eb318645073096f2cf645cc78 (diff) |
stex (20mar19)
git-svn-id: svn://tug.org/texlive/trunk@50489 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/structview')
-rw-r--r-- | Master/texmf-dist/source/latex/stex/structview/structview.dtx | 289 |
1 files changed, 195 insertions, 94 deletions
diff --git a/Master/texmf-dist/source/latex/stex/structview/structview.dtx b/Master/texmf-dist/source/latex/stex/structview/structview.dtx index d16ad8b9b0f..c87f5924648 100644 --- a/Master/texmf-dist/source/latex/stex/structview/structview.dtx +++ b/Master/texmf-dist/source/latex/stex/structview/structview.dtx @@ -10,10 +10,11 @@ % % \iffalse %<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01] -%<package>\ProvidesPackage{structview}[2016/04/07 v0.9 Structures and Views] +%<package>\ProvidesPackage{structview}[2019/03/20 v0.9 Structures and Views] % %<*driver> \documentclass{ltxdoc} +\usepackage[utf8]{inputenc} \usepackage{stex-logo,structview} \usepackage{url,array,float,textcomp} \usepackage[show]{ed} @@ -27,21 +28,28 @@ \usepackage{ctangit} \usepackage{xspace} \usepackage{hyperref} +\usepackage{tikz} +\usetikzlibrary{mmt} \makeindex \floatstyle{boxed} \newfloat{exfig}{thp}{lop} \floatname{exfig}{Example} -\def\tracissue#1{\cite{sTeX:online}, \hyperlink{http://trac.kwarc.info/sTeX/ticket/#1}{issue #1}} -\begin{document}\DocInput{structview.dtx}\end{document} +\def\githubissue#1{\cite{sTeX:github:on},\hyperlink{https://github.com/KWARC/sTeX/issues/#1}{issue #1}} +\def\gray#1{\textcolor{gray}{#1}} +\def\map#1#2{#1\mapsto #2} +\begin{document} +\RecordChanges +\DocInput{structview.dtx} +\end{document} %</driver> % \fi % % \CheckSum{926} % % \changes{v0.9}{2015/11/05}{Moved out of the \texttt{modules} package} +% \changes{v0.9}{2016/06/11}{Deprecated \texttt{viewsketch}} % % \GetFileInfo{modules.sty} -% % \MakeShortVerb{\|} %\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}\xspace} % \def\xml{\scsys{Xml}} @@ -57,11 +65,13 @@ % \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}} % \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}} % \def\cT{\mathcal{T}}\def\cD{\mathcal{D}} +% \def\cn#1{\mathsf{#1}} % \title{{\texttt{structview.sty}}: Structures and Views in {\stex}\thanks{Version {\fileversion} (last revised % {\filedate})}} % \author{Michael Kohlhase\\ -% Jacobs University, Bremen\\ -% \url{http://kwarc.info/kohlhase}} +% FAU Erlangen-N\"urnberg\\ +% FAU Erlangen-N\"urnberg\\ +% \url{http://kwarc.info/kohlhase}} % \maketitle % % \begin{abstract} @@ -74,10 +84,62 @@ % relations between modules/theories. % \end{abstract} % -% \newpage\setcounter{tocdepth}{2}\tableofcontents\newpage +% \setcounter{tocdepth}{2}\tableofcontents\newpage % % \section{Introduction}\label{sec:intro} -% \ednote{What are structures and views?} +% +% Structures and views constitute ways of defining and relating theories in a theory graph +% that considerably extend the ``object-oriented inheritance'' constituted by the imports +% relation given by the \sTeX |module| package. +% +% Structures are like imports, only that they allow to define new theories via inheritance +% with renaming. Views relate pre-existing theories and model conceptual refinements, +% framing, and implementation relations, again via a mapping between the languages defined +% by the source and target theories; we call these mappings \textbf{theory morphisms}. +% +% For details about theory morphisms we refer to~\cite{RabKoh:WSMSML13}, but hope to make +% the underlying concepts clear with examples. +% +%\begin{figure}[ht]\centering +% \begin{tikzpicture}[scale=.9]\footnotesize +% \node[thy] (Mon) at (0,1.2) {$\mmtthy{monoid}{\gray{\cn{op},\;\cn{unit}}}{}$}; +% \node[thy] (CGr) at (0,3) {$\mmtthy{cgp}{\gray{\cn{mon},\;\cn{inv}}}{}$}; +% \node[thy] (Ring) at (-3.5,3) {$\mmtthy{ring}{\gray{\cn{add}},\;\gray{\cn{mul}}}{}$}; +% \draw[struct](Mon) -- node[left,near end]{$\cn{cgp}?\cn{mon}$} (CGr); +% \draw[struct](CGr) -- node[below]{$\cn{ring}?\cn{add}$}(Ring); +% \draw[struct](Mon) -- node[left]{$\cn{ring}?\cn{mul}$} (Ring); +% \node[thy] (Int) at (3,3) {$\mmtthy{integers}{\gray{+,0,-,\cdot,1}}{}$}; +% \node[draw] (v2) at (1.5,4.8) { +% $\begin{array}{l} +% v_2\colon \\ +% \gray{\left\{\begin{array}{c} +% \map{\cn{mon}/\cn{op}}{+} \\ +% \map{\cn{mon}/\cn{unit}}{0} +% \end{array} +% \right\}} +% \;\mathrm{or}\; \gray{\map{\cn{mon}}{v_1}} \\ +% \gray{\map{\cn{inv}}{-}} +% \end{array}$}; +% \node[draw] at (2.5,1.4) { +% $\begin{array}{l} +% v_1\colon\\ +% \gray{\map{\cn{op}}{+}} \\ +% \gray{\map{\cn{unit}}{0}} +% \end{array}$}; +% \draw[view](Mon) -- (Int); +% \draw[view](CGr) -- node[below]{$v_2$} (Int); +% \draw[struct] (-4,4.5) -- +(1,0); +% \draw[view] (-4,5) -- +(1,0); +% \node[right] at (-3,4.5) {import}; +% \node[right] at (-3,5) {view}; +% \draw[view] (Ring) to[out=17,in=163] node[above,very near start] {$v_3$} (Int); +% \draw[view] (Mon) to[loop left] node[left,draw,solid,outer sep=3pt,thin]{$v_4\colon\map{x\,\cn{op}\,y}{y\,\cn{op}\,x}$}(Mon); +% \end{tikzpicture} +% \caption{A Theory Graph with Structures and Views}\label{fig:structview} +% \end{figure} +% \ednote{explain the contribution of structures and views to theory graphs and +% synchronize with Figure~\ref{fig:ring}.} +% % \section{The User Interface} % % The main contributions of the |modules| package are the |module| environment, which @@ -86,73 +148,68 @@ % % \subsection{Package Options}\label{sec:options} % -% The |modules| package takes two options: If we set -% \DescribeMacro{showmods}|showmods|\ednote{This mechanism does not work yet, since we -% cannot disable it when importing modules and that leads to unwanted boxes. What we need -% to do instead is to tweak the sms utility to use an internal version that never shows -% anything during sms reading.}, then the views (see Section~\ref{sec:user:views}) are -% shown. If we set the \DescribeMacro{qualifiedimports}|qualifiedimports| option, then -% qualified imports are enabled. Qualified imports give more flexibility in module -% inheritance, but consume more internal memory. As qualified imports are not fully -% implemented at the moment, they are turned off by default see -% Limitation~\ref{sec:limitations:qualified-imports}. The option -% \DescribeMacro{noauxreq}|noauxreq| prohibits the registration of |\@requiremodules| -% commands in the |aux| file. They are necessary for preloading the module signatures so -% that entries in the table of contents can have semantic macros; but as they sometimes -% cause trouble the option allows to turn off preloading. +% The \DescribeMacro{mh}|mh| option turns on MathHub support. % -% If the \DescribeMacro{showmeta}|showmeta| is set, then the metadata keys are shown -% (see~\cite{Kohlhase:metakeys:ctan} for details and customization options). +% \subsection{Theory Morphisms}\label{sec:user:assignments} % -% \subsection{Structures}\label{sec:user:structures} +% A theory morphism is a mapping between the languages of its source and target +% theory. This can be described mathematically using all the structures in the \sTeX +% distribution. However, in many situations, the language transformation of a morphism can +% be given in form of \textbf{assignments} that map symbols of the source theory to +% expressions of the target theory. % -% The |\importmodule| macro has a variant -% \DescribeMacro{importmodulevia}|\importmodulevia| that allows the specification of a -% theory morphism to be applied. |\importmodulevia{|\meta{thyid}|}{|\meta{assignments}|}| -% specifies the ``source theory'' via its identifier \meta{thyid} and the morphism by -% \meta{assignments}. There are four kinds:\ednote{MK: this needs to be consolidated and -% researched better.} -% \begin{compactdesc} +% There are three kinds assignments:\ednote{MK: we need better macros here.} +% \begin{description} % \item[symbol assignments] via -% \DescribeMacro{\vassign}|\vassign{|\meta{sym}|}{|\meta{exp}|}|, which defines the -% symbol \meta{sym} introduced in the current theory by an expression \meta{exp} in the -% source theory. +% \DescribeMacro{\vassign}|\vassign{|\meta{sym}|}{|\meta{exp}|}|, which maps a symbol +% \meta{sym} from source theory an expression \meta{exp} in the target theory. % \item[function assignments] via % \DescribeMacro{\fassign}|\fassign{|\meta{bvars}|}{|\meta{pat}|}{|\meta{exp}|}|, is a -% variant which defines a function symbol \meta{sym} introduced in the current theory by -% mapping a pattern expression \meta{pat} (\meta{sym} applied to \meta{bvars}) to an -% expression \meta{exp} in the source theory on bound variables \meta{bvars}. +% variant which maps a function symbol \meta{sym} by mapping a pattern expression +% \meta{pat} (\meta{sym} applied to \meta{bvars}) to an expression \meta{exp} in the +% target theory on bound variables \meta{bvars}. % \item[term assignments] via -% \DescribeMacro{\tassign}|\tassign[|\meta{source-cd}|]{|\meta{tname}|}{|\meta{source-tname}|}|, -% which assigns to the term with name \meta{tname} in the current theory a term with -% name \meta{source-tname} in the theory \meta{source-cd} whose default value is the -% source theory. -% \item[term text assignments] via -% \DescribeMacro{\ttassign}|\tassign{|\meta{tname}|}{|\meta{text}|}|, which defines a -% term with name \meta{tname} in the current theory via a definitional text. -% \end{compactdesc} +% \DescribeMacro{\tassign}|\tassign{|\meta{sym}|}{|\meta{tname}|}|, another special +% case, where the value is the symbol with name \meta{tname} in the target theory. +% \end{description} +% Figure~\ref{fig:ring} shows a concrete example\ednote{adapt when we fully understand +% this, and the implementation works.} +% +% The assignments above can be seen as abbreviations for a simple, formal definitions, +% which define a symbol of the source theory by an expression in the target theory. +% +% \subsection{Structures}\label{sec:user:structures} % +% Structures are specified by the \DescribeEnv{structure}|sstructure|\footnote{The old +% |importmodulevia| environment is now deprecated.} environment: +% \begin{center} +% |\begin{sstructure}[|\meta{keys}|]{|\meta{name}|}{|\meta{sthy}|}|\meta{morph}|\end{sstructure}| +% \end{center} +% gives the structure the name \meta{name}, specifies the ``source theory'' via its +% identifier \meta{sthy}, and the morphism \meta{morph}. The |structure| environment takes +% the same keys as the |\importmodule| macro, which it generalizes. The morphism +% \meta{morph} in the body of the |structure| environment specifies the morphism +% (see~\ref{sec:user:assignments} above). In a structure, we take the target theory to be +% the current theory. +% %\begin{exfig} % \begin{verbatim} % \begin{module}[id=ring] -% \begin{importmodulevia}{monoid} -% \vassign{rbase}\magbase -% \fassign{a,b}{\rtimes{A}B}{\magmaop{a}b} -% \vassign{rone}\monunit -% \end{importmodulevia} -% \symdef{rbase}{G} -% \symdef[name=rtimes]{rtimesOp}{\cdot} -% \symdef{rtimes}[2]{\infix\rtimesOp{#1}{#2}} +% \symdef{rbase}{R} +% \symdef{rtimes}[2]{\infix\cdot{#1}{#2}} % \symdef{rone}{1} -% \begin{importmodulevia}{cgroup} -% \vassign{rplus}\magmaop -% \vassign{rzero}\monunit -% \vassign{rinvOp}\cginvOp -% \end{importmodulevia} -% \symdef[name=rplus]{rplusOp}{+} -% \symdef{rplus}[2]{\infix\rplusOp{#1}{#2}} -% \symdef[name=rminus]{rminusOp}{-} -% \symdef{rminus}[1]{\infix\rminusOp{#1}{#2}} +% \begin{sstructure}{mul}{monoid} +% \tassign{magbase}{rbase} +% \fassign{a,b}{\magmaop{a}b}{\rtimes{a}b} +% \tassign{monunit}{rone} +% \end{sstructure} +% \symdef{rplus}[2]{\infix+{#1}{#2}} +% \symdef{rminus}[1]{\infix-{#1}{#2}} +% \begin{sstructure}{add}{cgroup} +% \fassign{a,b}{\magmaop{a}b}{\rplus{a}b} +% \tassign{monunit}{rzero} +% \tassign{cginvOp}{\rminus} +% \end{sstructure} % ... % \end{module} % \end{verbatim} @@ -162,13 +219,35 @@ % \subsection{Views}\label{sec:user:views} % % A view is a mapping between modules, such that all model assumptions (axioms) of the -% source module are satisfied in the target module. \ednote{Document and make Examples} +% source module are satisfied in the target module. For marking up views the |structview| +% package supplies the \DescribeEnv{view}|view| environment; see Figure~\ref{fig:view} for +% the \stex markup of view $v_1$ from Figure~\ref{fig:structview}. The |view| environment +% takes one optional key/value argument followed by two mandatory ones: the names of the +% source and target modules. The |view| environment takes the following keys: |id| for a +% name, |title| and |display| for visual presentation, |loadfrom|, |loadto|, and +% |ext|\ednote{MK: we probably need toext and fromext here, but this never came up yet.} +% for specifying the source files that supply the source and target modules, |creators|, +% |contributors|, |srccite| for document metadata, and |type|\ednote{????}. +% +%\begin{exfig} +% \begin{verbatim} +% \begin{view}{monoid}{integers} +% \vassign{magbase}{base} +% \fassign{a,b}{\magmaop{a}b}{\inttimes{a,b}} +% \tassign{monunit}{\intzero} +% \begin{assertion} +% The Integers with addition form a monoid in the obvious way. +% \end{assertion} +% \end{view} +% \end{verbatim} +% \caption{A view from monoids to integers}\label{fig:view} +% \end{exfig} % % \section{Limitations \& Extensions}\label{sec:limitations} % % In this section we will discuss limitations and possible extensions of the |modules| % package. Any contributions and extension ideas are welcome; please discuss ideas, -% requests, fixes, etc on the {\sTeX} TRAC~\cite{sTeX:online}. +% requests, fixes, etc on the {\sTeX} TRAC~\cite{sTeX:github:on}. % % \section{The Implementation}\label{sec:impl} % @@ -194,28 +273,41 @@ \RequirePackage{modules} % \end{macrocode} % +% \subsection{Theory Morphisms by Assignments}\label{sec:impl:assignments} +% +% \begin{environment}{\*assign} +% \ednote{probably get rid of the optional argument} +% \begin{macrocode} +\newrobustcmd\vassign[3][]{\ifmod@show\ensuremath{#2\mapsto #3}, \fi}% +\newrobustcmd\fassign[4][]{\ifmod@show \ensuremath{#3(#2)\mapsto #4}, \fi}% +\newrobustcmd\tassign[3][]{\ifmod@show \ensuremath{#2\mapsto} #3, \fi}% +% \end{macrocode} +% \end{environment} +% % \subsection{Structures}\label{sec:impl:structures} % -% \begin{macro}{\importmodulevia} -% The |importmodulevia| environment just calls |\importmodule|, but to get around the +% \begin{environment}{sstructure} +% The |structure| environment just calls |\importmodule|, but to get around the % group, we first define a local macro |\@@doit|, which does that and can be called with -% an |\aftergroup| to escape the environment grouping introduced by |importmodulevia|. +% an |\aftergroup| to escape the environment grouping introduced by |structure|. % \begin{macrocode} -\newenvironment{importmodulevia}[2][]{% - \gdef\@@doit{\importmodule[#1]{#2}}% - \ifmod@show\par\noindent importing module #2 via \@@doit\fi% +\newenvironment{sstructure}[3][]{% + \gdef\@@doit{\importmodule[#1]{#3}}% + \ifmod@show\par\noindent importing module #3 via \@@doit\fi% }{% \aftergroup\@@doit\ifmod@show end import\fi% }% % \end{macrocode} -% \end{macro} -% -% \begin{environment}{\*assign} +% \end{environment} +% +% \begin{environment}{importmodulevia} +% This is now deprecated, we give an error, but punt to |structure|. % \begin{macrocode} -\newrobustcmd\vassign[3][]{\ifmod@show\ensuremath{#2\mapsto #3}, \fi}% -\newrobustcmd\tassign[3][]{\ifmod@show #2\ensuremath{\mapsto} #3, \fi}% -\newrobustcmd\fassign[4][]{\ifmod@show \ensuremath{#3\mapsto #4}, \fi}% -\newrobustcmd\ttassign[3][]{\ifmod@show #2\ensuremath{\mapsto} ``#3'', \fi}% +\newenvironment{importmodulevia}[2][]% +{\PackageError{structview}% + {The {importmodulevia} environment is deprecated}{use the {sstructure} instead!}% + \begin{sstructure}[#1]{missing}{#2}} +{\end{sstructure}} % \end{macrocode} % \end{environment} % @@ -226,8 +318,8 @@ \srefaddidkey{view} \addmetakey*{view}{title} \addmetakey{view}{display} -\addmetakey{view}{from} -\addmetakey{view}{to} +\addmetakey{view}{loadfrom} +\addmetakey{view}{loadto} \addmetakey{view}{creators} \addmetakey{view}{contributors} \addmetakey{view}{srccite} @@ -238,7 +330,7 @@ % \begin{macro}{\view@heading} % Then we make a convenience macro for the view heading. This can be customized. % \begin{macrocode} -\newcounter{view}[section] +\ifdef{\thesection}{\newcounter{view}[section]}{\newcounter{view}} \newrobustcmd\view@heading[4]{% \if@importing% \else% @@ -267,7 +359,7 @@ % module signatures) for module bookkeeping and adds presentation (a heading and a box) % if the |showmods| option is set. % \begin{macrocode} -\newenvironment{view}[3][]{% +\newenvironment{view}[3][]{% keys, from, to \metasetkeys{view}{#1}% \sref@target% \begin{@view}{#2}{#3}% @@ -284,24 +376,20 @@ % The |@view| does the actual bookkeeping at the module level. % \begin{macrocode} \newenvironment{@view}[2]{%from, to - \@importmodule[\view@from]{#1}{\view@ext}% - \@importmodule[\view@to]{#2}{\view@ext}% + \@importmodule[\view@loadfrom]{#1}{\view@ext}% + \@importmodule[\view@loadto]{#2}{\view@ext}% }{}% % \end{macrocode} % \end{environment} % % \begin{environment}{viewsketch} -% The |viewsketch| environment behaves like |view|, but only has text contents. +% The |viewsketch| environment is deprecated, we give an error % \begin{macrocode} -\newenvironment{viewsketch}[3][]{% - \metasetkeys{view}{#1}% - \sref@target% - \begin{@view}{#2}{#3}% - \view@heading{#2}{#3}{\view@display}{\view@title}% -}{% - \end{@view}% -}% -\ifmod@show\surroundwithmdframed{viewsketch}\fi% +\newenvironment{viewsketch}[3][]% +{\PackageError{structview}% + {The {viewsketch} environment is deprecated}{use the {view} instead!}% + \begin{view}[#1]{#2}{#3}} +{\end{view}} % \end{macrocode} % \end{environment} % @@ -317,9 +405,22 @@ %</package> % \end{macrocode} % \end{macro} +% % \Finale \endinput %%% Local Variables: %%% mode: doctex %%% TeX-master: t %%% End: + +% LocalWords: iffalse NeedsTeXFormat structview.dtx texttt scsys sc sc xspace mathml cn +% LocalWords: omdoc latexml cmathml activemath twintoo atwin atwintoo mathcal mathcal +% LocalWords: structview.sty stex maketitle newpage setcounter tocdepth tableofcontents +% LocalWords: newpage symdef importmodulevia thyid ednote compactdesc vassign vassign +% LocalWords: sym exp fassign fassign bvars tassign tassign tname source-tname exfig +% LocalWords: monoids impl behavior sref newif xcomment initialize structview-mh gdef +% LocalWords: aftergroup newenvironment ifmod@show noindent newrobustcmd ensuremath ifx +% LocalWords: mapsto srefaddidkey addmetakey srccite customized newcounter stepcounter +% LocalWords: textbf thesection theview textsf textsf ignorespaces metasetkeys doctex +% LocalWords: surroundwithmdframed mathsf RabKoh centering tikzpicture mmtthy CGr cgp +% LocalWords: inv cdot mathrm synchronize sstructure sthy loadfrom loadto toext fromext |