summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/structview/structview.dtx
blob: d16ad8b9b0fa703bb7b0ca3a70cf662014bb27d8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
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: