summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/structview/structview.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/structview/structview.dtx')
-rw-r--r--Master/texmf-dist/source/latex/stex/structview/structview.dtx325
1 files changed, 325 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/structview/structview.dtx b/Master/texmf-dist/source/latex/stex/structview/structview.dtx
new file mode 100644
index 00000000000..d16ad8b9b0f
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/structview/structview.dtx
@@ -0,0 +1,325 @@
+% \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
+%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+%<package>\ProvidesPackage{structview}[2016/04/07 v0.9 Structures and Views]
+%
+%<*driver>
+\documentclass{ltxdoc}
+\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}
+\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}
+%</driver>
+% \fi
+%
+% \CheckSum{926}
+%
+% \changes{v0.9}{2015/11/05}{Moved out of the \texttt{modules} package}
+%
+% \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}}
+% \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}}
+% \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}
+%
+% \newpage\setcounter{tocdepth}{2}\tableofcontents\newpage
+%
+% \section{Introduction}\label{sec:intro}
+% \ednote{What are structures and views?}
+% \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 |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.
+%
+% If the \DescribeMacro{showmeta}|showmeta| is set, then the metadata keys are shown
+% (see~\cite{Kohlhase:metakeys:ctan} for details and customization options).
+%
+% \subsection{Structures}\label{sec:user:structures}
+%
+% 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}
+% \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.
+% \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}.
+% \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}
+%
+%\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{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}}
+% ...
+% \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. \ednote{Document and make Examples}
+%
+% \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}.
+%
+% \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{Structures}\label{sec:impl:structures}
+%
+% \begin{macro}{\importmodulevia}
+% The |importmodulevia| 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|.
+% \begin{macrocode}
+\newenvironment{importmodulevia}[2][]{%
+ \gdef\@@doit{\importmodule[#1]{#2}}%
+ \ifmod@show\par\noindent importing module #2 via \@@doit\fi%
+}{%
+ \aftergroup\@@doit\ifmod@show end import\fi%
+}%
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{environment}{\*assign}
+% \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}%
+% \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}{from}
+\addmetakey{view}{to}
+\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}
+\newcounter{view}[section]
+\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][]{%
+ \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@from]{#1}{\view@ext}%
+ \@importmodule[\view@to]{#2}{\view@ext}%
+}{}%
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{viewsketch}
+% The |viewsketch| environment behaves like |view|, but only has text contents.
+% \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%
+% \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%
+}%
+%</package>
+% \end{macrocode}
+% \end{macro}
+% \Finale
+\endinput
+%%% Local Variables:
+%%% mode: doctex
+%%% TeX-master: t
+%%% End: