summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/structview
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2019-03-20 22:31:24 +0000
committerKarl Berry <karl@freefriends.org>2019-03-20 22:31:24 +0000
commit2b006ec0e0cafe12255f874f9c44786ab6f38901 (patch)
treec40f5796e1b34e3f051abd84d049e092e4ffd0ab /Master/texmf-dist/source/latex/stex/structview
parent8e508e8b0218f17eb318645073096f2cf645cc78 (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.dtx289
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