% \iffalse meta-comment % An Infrastructure for Structures and Views % Copyright (C) 2004-2013 Michael Kohlhase, all rights reserved % this file is released under the % LaTeX Project Public License (LPPL) % % The original of this file is in the public repository at % http://github.com/KWARC/sTeX/ % \fi % % \iffalse %\NeedsTeXFormat{LaTeX2e}[1999/12/01] %\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} \usepackage[hyperref=auto,style=alphabetic]{biblatex} \addbibresource{kwarcpubs.bib} \addbibresource{extpubs.bib} \addbibresource{kwarccrossrefs.bib} \addbibresource{extcrossrefs.bib} \usepackage{listings} \usepackage{amsfonts} \usepackage{ctangit} \usepackage{xspace} \usepackage{hyperref} \usepackage{tikz} \usetikzlibrary{mmt} \makeindex \floatstyle{boxed} \newfloat{exfig}{thp}{lop} \floatname{exfig}{Example} \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} % % \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}} % \def\mathml{\scsys{MathML}} % \def\omdoc{\scsys{OMDoc}} % \def\openmath{\scsys{OpenMath}} % \def\latexml{\scsys{LaTeXML}} % \def\perl{\scsys{Perl}} % \def\cmathml{Content-{\sc MathML}\index{Content {\sc MathML}}\index{MathML@{\sc MathML}!content}} % \def\activemath{\scsys{ActiveMath}} % \def\twin#1#2{\index{#1!#2}\index{#2!#1}} % \def\twintoo#1#2{{#1 #2}\twin{#1}{#2}} % \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}} % \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}} % \def\cT{\mathcal{T}}\def\cD{\mathcal{D}} % \def\cn#1{\mathsf{#1}} % \title{{\texttt{structview.sty}}: Structures and Views in {\stex}\thanks{Version {\fileversion} (last revised % {\filedate})}} % \author{Michael Kohlhase\\ % FAU Erlangen-N\"urnberg\\ % FAU Erlangen-N\"urnberg\\ % \url{http://kwarc.info/kohlhase}} % \maketitle % % \begin{abstract} % The |structview| package is part of the {\stex} collection, a version of {\TeX/\LaTeX} % that allows to markup {\TeX/\LaTeX} documents semantically without leaving the % document format, essentially turning {\TeX/\LaTeX} into a document format for % mathematical knowledge management (MKM). % % This package supplies infrastructure for \omdoc structures and views: complex semantic % relations between modules/theories. % \end{abstract} % % \setcounter{tocdepth}{2}\tableofcontents\newpage % % \section{Introduction}\label{sec:intro} % % 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 % allows for lexical scoping of semantic macros with inheritance and the |\symdef| macro % for declaration of semantic macros that underly the |module| scoping. % % \subsection{Package Options}\label{sec:options} % % The \DescribeMacro{mh}|mh| option turns on MathHub support. % % \subsection{Theory Morphisms}\label{sec:user:assignments} % % 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. % % 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 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 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{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] % \symdef{rbase}{R} % \symdef{rtimes}[2]{\infix\cdot{#1}{#2}} % \symdef{rone}{1} % \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} % \caption{A Module for Rings with inheritance from monoids and commutative groups}\label{fig:ring} % \end{exfig} % % \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. 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:github:on}. % % \section{The Implementation}\label{sec:impl} % % \subsection{Package Options}\label{sec:impl:options} % % We declare some switches which will modify the behavior according to the package % options. Generally, an option |xxx| will just set the appropriate switches to true % (otherwise they stay false). The options we are not using, we pass on to the |sref| % package we require next. % \begin{macrocode} %<*package> \newif\if@structview@mh@\@structview@mh@false \DeclareOption{mh}{\@structview@mh@true \PassOptionsToPackage{\CurrentOption}{modules}} \DeclareOption*{\PassOptionsToPackage{\CurrentOption}{modules}} \ProcessOptions % \end{macrocode} % % The next measure is to ensure that the |sref| and |xcomment| packages are loaded (in the % right version). For {\latexml}, we also initialize the package inclusions. % \begin{macrocode} \if@structview@mh@\RequirePackage{structview-mh}\fi \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{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 |structure|. % \begin{macrocode} \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{environment} % % \begin{environment}{importmodulevia} % This is now deprecated, we give an error, but punt to |structure|. % \begin{macrocode} \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} % % \subsection{Views}\label{sec:impl:views} % % We first prepare the ground by defining the keys for the |view| environment. % \begin{macrocode} \srefaddidkey{view} \addmetakey*{view}{title} \addmetakey{view}{display} \addmetakey{view}{loadfrom} \addmetakey{view}{loadto} \addmetakey{view}{creators} \addmetakey{view}{contributors} \addmetakey{view}{srccite} \addmetakey{view}{type} \addmetakey[sms]{view}{ext} % \end{macrocode} % % \begin{macro}{\view@heading} % Then we make a convenience macro for the view heading. This can be customized. % \begin{macrocode} \ifdef{\thesection}{\newcounter{view}[section]}{\newcounter{view}} \newrobustcmd\view@heading[4]{% \if@importing% \else% \stepcounter{view}% \edef\@display{#3}\edef\@title{#4}% \noindent% \ifx\@display\st@flow% \else% {\textbf{View} {\thesection.\theview} from \textsf{#1} to \textsf{#2}}% \sref@label@id{View \thesection.\theview}% \ifx\@title\@empty% \quad% \else% \quad(\@title)% \fi% \par\noindent% \fi% \ignorespaces% \fi% }%ifmod@show % \end{macrocode} % \end{macro} % % \begin{environment}{view} % The |view| environment relies on the |@view| environment (used also in the \sTeX % module signatures) for module bookkeeping and adds presentation (a heading and a box) % if the |showmods| option is set. % \begin{macrocode} \newenvironment{view}[3][]{% keys, from, to \metasetkeys{view}{#1}% \sref@target% \begin{@view}{#2}{#3}% \view@heading{#2}{#3}{\view@display}{\view@title}% }{% \end{@view}% \ignorespaces% }% \ifmod@show\surroundwithmdframed{view}\fi% % \end{macrocode} % \end{environment} % % \begin{environment}{@view} % The |@view| does the actual bookkeeping at the module level. % \begin{macrocode} \newenvironment{@view}[2]{%from, to \@importmodule[\view@loadfrom]{#1}{\view@ext}% \@importmodule[\view@loadto]{#2}{\view@ext}% }{}% % \end{macrocode} % \end{environment} % % \begin{environment}{viewsketch} % The |viewsketch| environment is deprecated, we give an error % \begin{macrocode} \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} % % \begin{macro}{\obligation} % The |\obligation| element does not do anything yet on the latexml % side.\ednote{document above} % \begin{macrocode} \newrobustcmd\obligation[3][]{% \if@importing% \else Axiom #2 is proven by \sref{#3}% \fi% }% % % \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