% \iffalse meta-comment % An Infrastructure for Mathematical Statements in sTeX % Copyright (C) 2004-2006 Michael Kohlhase, all rights reserved % this file is released under the % LaTeX Project Public License (LPPL) % % The development version of this file can be found at % https://svn.kwarc.info/repos/kwarc/projects/stex/sty/statements.dtx % \fi % % \iffalse %\NeedsTeXFormat{LaTeX2e}[1999/12/01] %\ProvidesPackage{statements}[2007/09/09 v0.9d Semantic Markup for Statements] % %<*driver> \documentclass{ltxdoc} \usepackage{url,array,stex,float} \usepackage[show]{ed} \usepackage{hyperref} \makeindex \floatstyle{boxed} \newfloat{exfig}{thp}{lop} \floatname{exfig}{Example} \begin{document}\DocInput{statements.dtx}\end{document} % % \fi % % \CheckSum{266} % % \changes{v0.9}{2005/06/14}{First Version with Documentation} % \changes{v0.9a}{2005/07/01}{Completed Documentation} % \changes{v0.9b}{2005/08/06}{Complete functionality and Updated Documentation} % \changes{v0.9c}{2006/01/13}{more packaging} % \changes{v0.9d}{2007/09/09}{moved omtext and friends to the omdoc package} % \changes{v0.9d}{2007/09/09}{made dependence on the omdoc package explicit} % \changes{v0.9d}{2007/09/09}{adding ids to many elements} % % \GetFileInfo{statements.sty} % % \MakeShortVerb{\|} %\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}} % \def\stex{{\raisebox{-.5ex}S\kern-.5ex\TeX}} % \def\sTeX{\stex} % \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\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}} % \title{Semantic Markup for Mathematical Statements\thanks{Version {\fileversion} (last revised % {\filedate})}} % \author{Michael Kohlhase\\ % Jacobs University, Bremen\\ % \url{http://kwarc.info/kohlhase}} % \maketitle % % \begin{abstract} % The |statements| packge 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 provides semantic markup facilities for mathematical statements like % Theorems, Lemmata, Axioms, Definitions, etc. in {\stex} files. This structure can be % used by MKM systems for added-value services, either directly from the {\sTeX} % sources, or after translation. % \end{abstract} %\newpage %\section{Introduction}\label{sec:statements} % % The motivation for the |statemets| package is very similar to that for semantic macros % in the |modules| package: We want to annotate the structural semantic properties of % statements in the source, but present them as usual in the formatted documents. In % contrast to the case for mathematical objects, the repertoire of mathematical statements % and their structure is more or less fixed. % % This structure can be used by MKM systems for added-value services, either directly from % the {\sTeX} sources, or after translation. Even though it is part of the {\stex} % collection, it can be used independently, like it's sister package |sproofs|. % % {\stex} is 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). % % \section{The User Interface} % % All the statements are marked up as envioronments, that take a |KeyVal| argument that % allows to annotate semantic information. \DescribeEnv{assertion} For instance, instead % of providing environments for ``Theorem'', ``Lemma'', ``Proposition'',... we have a % single |assertion| environment that generalizes all of these, and takes a |type| key % that allows to specify the ``type''. So instead of |\begin{Lemma}|\iffalse\end{Lemma}\fi % we have to write |\begin{assertion}[type=Lemma]|\iffalse\end{assertion}\fi (see % Example~\ref{fig:assertion} for an example).\ednote{talk about package options here! % Draft mode,...} %\begin{exfig} % \begin{verbatim} % \begin{assertion}[id=sum-over-odds,type=Lemma] % $\sum_{i=1}^n{2i-1}=n^2$ % \end{assertion} % \end{verbatim} % \vspace{-1em}will lead to the result\medskip\par\noindent % \begin{assertion}[id=sum-over-odds,type=Lemma] % $\sum_{i=1}^n{2i-1}=n^2$ % \end{assertion} % \caption{Semantic Markup for a Lemma in a {\tt{module}} context}\label{fig:assertion} % \end{exfig} % % Whether we will see the keyword ``Lemma'' will depend on the value of the optional % |display| key. In all of the |assertion| environments, the presentation expectation is % that the text will be presented in italic font. Generally, we distinguish two forms of % statements: % \begin{description} % \item[{\twintoo{block}{statement}s}] have explicit discourse markers that delimit their content in the % surrounding text, e.g. the boldface word ``{\bf{Theorem}:}'' as a start marker and a % little line-end box as an end marker of a proof. % \item[{\twintoo{flow}{statement}s}] do not have explicit markers, they are interspersed % with the surrounding text. % \end{description} % Since they have the same semantic status, they must both be marked up, but styled % differently. We distinguis between these two presentational forms with the |display| % key, which is allowed on all statement environments. If it has the value |block| (the % default), then the statement will be presented in a paragraph of its own, have explicit % discourse markers for its begin and end, possibly numbering, etc. If it has the value % |flow|, then no extra presentation will be added\ednote{in the flow case, the text % should not be made italic; implement this! } the semantic information is invisible to % the reader. % % Another key that is present on all statement environments in the |id| key it allows to % identify the statement with a name. % % \DescribeEnv{axiom} The |axiom| environment is similar to |assertion|, but the content % has a different ontological status: axioms are assumed without (formal) justification, % whereas assertions are expeceted to be justified from other assertions, axioms or % definitions. % % \DescribeEnv{definition} The |definition| environment is used for marking up % mathematical definitions. Its peculiarity is that it defines (i.e. gives a meaning to) % new mathematical concepts or objects. These\DescribeMacro{\definiendum} are identified by % the |definiendum| macro, which takes two arguments. The first one is the system name of % the symbol defined (for reference via |\termin| ), the second one is the text that is to % be emphasized in the presentation. Note that the |\definiendum| macro can only be used % inside the |definition| environment. If you find yourself in a situation where you want % to use it outside, you will most likely want to wrap the apporpriate text fragment in a % |\begin{definition}[display=flow]| ... and |\end{definition}|.\ednote{need to leave % hypertargets on the definiendum, so that we can crosslink} % % \DescribeMacro{\termin} If we have defined a concept with the |\definiendum| macro, then % we can mark up other occurrences of the term as referring to this concept. Note that % this process cannot be fully automatized yet, since that would need advanced lanauge % technology to get around problems of disambiguation, inflection, and non-contiguous % phrases\footnote{We do have a program that helps annotate larger text collections % spotting the easy cases; see {\url{http://kwarc.info/projects/stex}} and % look for the program |termin|.}. Therefore, the |\termin| can be used to make this % information explicit. % % \DescribeEnv{simpleDef} The |simpleDef| environment is a statement environment for % simple definitions, which introduce a new symbol that abbreviates another concept. The % envioronment takes an argument for the new concept % % \DescribeEnv{example} The |example| environment is a generic statement envionment, % except that the |for| key should be given to specify the identifier what this is an % example for. The |example| environment also expcets a |type| key to be specified, so % that we know whether this is an example or a counterexample\ednote{think about this some % more} % % \DescribeMacro{\defemph} The |\defemph| macro is a configuration hook that allows to % specify the style of presentation of the {\index*{definiendum}}. By default, it is set to % |\bf| as a fallback, since we can be sure that this is always available. It can be % customized by redefinition: For instance |\renewcommand{\defemph}[1]{\emph{#1}}|, % changes the default behavior to italics. % % \DescribeMacro{\termemph} The |\termenph| macro does the same for the style for % |\termin|, it is empty by default. Note the term might carry an implicit hyperreference % to the defining occurrance and that the presentation engine might mark this up, changing % this behavior. % % \DescribeMacro{\stDMemph} The |\stDMemph| macro does the same for the style for the % markup of the discourse markers like ``Theorem''. If it is not defined, it is set to % |\bf|; that allows to preset this in the class file. % % \StopEventually{\ednotemessage} % % \section{The Implementation}\label{sec:impl} % % 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). First we have the general options % \begin{macrocode} %<*package> \newif\ifst@env\st@envfalse \newif\ifst@id\st@idfalse \newif\ifst@display\st@displayfalse \DeclareOption{id}{\st@idtrue\st@envtrue} \DeclareOption{env}{\st@envtrue} \DeclareOption{display}{\st@displaytrue\st@envtrue} % \end{macrocode} % And then the options that are specific to the |statements| package. % \begin{macrocode} \newif\ifstat@for\stat@forfalse \newif\ifstat@from\stat@forfalse \newif\ifstat@type\stat@typefalse \newif\ifstat@title\stat@titlefalse \newif\ifstat@continues\stat@continuesfalse \DeclareOption{for}{\stat@fortrue\st@envtrue} \DeclareOption{from}{\stat@fromtrue\st@envtrue} \DeclareOption{type}{\stat@typetrue\st@envtrue} \DeclareOption{title}{\stat@titletrue\st@envtrue} \DeclareOption{continues}{\stat@continuestrue\st@envtrue} % \end{macrocode} % \begin{macro}{\stattrue} % For convenience, we collect the switches into one. % \begin{macrocode} \def\stattrue{\stat@fortrue\stat@fromtrue\stat@typetrue\stat@continuestrue} % \end{macrocode} % \end{macro} % Now, we define two collective options, which are equivalent to turning on all the other % options. % \begin{macrocode} \DeclareOption{draft}{\st@envtrue\st@idtrue\stat@fortrue\stat@fromtrue\typetrue\justtrue} \DeclareOption{all}{\st@envtrue\stattrue\justtrue} % \end{macrocode} % Finally, we need to declare the end of the option declaration section to {\LaTeX}. % \begin{macrocode} \ProcessOptions % % \end{macrocode} % % The next measure is to ensure that the |omdoc| package is loaded (in the right % version). For {\latexml}, we also initialize the package inclusions. % \begin{macrocode} %\RequirePackage{omdoc}[2007/09/09] %<*ltxml> # -*- CPERL -*- package LaTeXML::Package::Pool; use strict; use LaTeXML::Package; RequirePackage('omdoc'); RequirePackage('myindex'); % % \end{macrocode} % % \begin{macro}{\define@statement@env} % We define a meta-macro that allows us to define several variants of statements. Upon % beginning this environment, we first set the |KeyVal| attributes, then we decide % whether to print the discourse marker based on the value of the |display| key, then % (given the right Options were set), we show the semantic annotations, and finally % initialize the environment using the appropriate macro. Upon ending the environment, % we just run the respcective termination macro. % \begin{macrocode} %<*package> \def\define@statement@env#1#2{ \newenvironment{#1}[1][]{\setkeys{stat}{##1} \ifx\st@display\st@flow\else\stDMemph{#2}:\fi% \@ifundefined{stat@title}{}% {\space\ifx\st@display\st@flow\else(\fi\stDMemph{\stat@title}\ifx\st@display\st@flow:\else)\par\fi}\space% \ifst@env\show@stat@keys{#1}\fi\csname st@#1@initialize\endcsname} {\csname st@#1@terminate\endcsname}} % % \end{macrocode} % \end{macro} % % \begin{environment}{assertion} % \begin{macrocode} %<*package> \newenvironment{assertion}[1][]{\setkeys{stat}{#1} \ifx\st@display\st@flow\else{\stDMemph{\stat@type}:}\fi% \@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}% \ifst@env\show@stat@keys{#1}\fi\em}{} % %<*ltxml> DefCMPEnvironment('{assertion} OptionalKeyVals:stat', "" . "?&KeyVal(#1,'title')(&KeyVal(#1,'title'))()" . "#body" ."\n"); % % \end{macrocode} % \end{environment} % % \begin{environment}{simpleDef} % \begin{macrocode} %<*package> \newenvironment{simpleDef}[1][]{\setkeys{stat}{#1} \ifx\st@display\st@flow\else{\stDMemph{Definition}:}\fi% \@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}% \ifst@env\show@stat@keys{#1}\fi}{} % %<*ltxml> DefCMPEnvironment('{simpleDef} OptionalKeyVals:stat', "?&KeyVal(#1,'for')()()" . "" . "?&KeyVal(#1,'title')(&KeyVal(#1,'title'))()" . "#body" . "\n"); % % \end{macrocode} % \end{environment} % % \begin{environment}{PatternDef} % \begin{macrocode} %<*package> \newenvironment{PatternDef}[1][]{\setkeys{stat}{#1} \ifx\st@display\st@flow\else{\stDMemph{Definition}:}\fi% \@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}% \ifst@env\show@stat@keys{#1}\fi}{} \newenvironment{PatternRule}[1]{#1$\colon=$}{} \newenvironment{PatternCMP}{}{} % %<*ltxml> DefCMPEnvironment('{PatternDef} OptionalKeyVals:stat', "?&KeyVal(#1,'for')()()" . "" . "?&KeyVal(#1,'title')(&KeyVal(#1,'title'))()" . "#body" . "\n"); DefEnvironment('{PatternRule}{}', "#1 #body"); DefEnvironment('{PatternCMP}{}', "#body"); % % \end{macrocode} % \end{environment} % % \begin{environment}{RecDef} % \begin{macrocode} %<*package> \newenvironment{RecDef}[1][]{\setkeys{stat}{#1} \ifx\st@display\st@flow\else{\stDMemph{Definition}:}\fi% \@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}% \ifst@env\show@stat@keys{#1}\fi}{} % %<*ltxml> DefEnvironment('{RecDef} OptionalKeyVals:stat', "?&KeyVal(#1,'for')()()" . "" . "?&KeyVal(#1,'title')(&KeyVal(#1,'title'))()" . "#body" . "\n"); % % \end{macrocode} % \end{environment} % % \begin{environment}{example} % \begin{macrocode} %<*package> \def\st@example@initialize{}\def\st@example@terminate{} \define@statement@env{example}{Example} % %<*ltxml> DefCMPEnvironment('{example} OptionalKeyVals:stat', "" . "#body" . "\n"); % % \end{macrocode} % \end{environment} % % \begin{environment}{axiom} % \begin{macrocode} %<*package> \def\st@axiom@initialize{}\def\st@axiom@terminate{} \define@statement@env{axiom}{Axiom} % %<*ltxml> DefCMPEnvironment('{axiom} OptionalKeyVals:stat', "" . "?&KeyVal(#1,'title')(&KeyVal(#1,'title'))()" . "#body" . "\n"); % % \end{macrocode} % \end{environment} % % \begin{environment}{consymb} % \begin{macrocode} %<*package> \define@key{consymb}{type}{\def\consymb@type{#1}} \define@key{consymb}{title}{\def\consymb@title{#1}} \define@key{consymb}{name}{\def\consymb@name{#1}} \def\consymb@type{Symbol} \newenvironment{consymb}[1][]{\setkeys{consymb}{#1} \ifx\st@display\st@flow\else{\stDMemph{\consymb@type} \consymb@name:}\fi% \@ifundefined{consymb@title}{~}{~(\stDMemph{\consymb@title})\par}}{} % %<*ltxml> DefEnvironment('{consymb} OptionalKeyVals:stat', "" . "" . "" . "#body" . "" . "" . "\n"); % % \end{macrocode} % \end{environment} % % \begin{macro}{\symtype} % \begin{macrocode} %\newcommand{\symtype}[2]{Type (#1): #2} %DefConstructor('\symtype{}{}',"#2"); % \end{macrocode} % \end{macro} % % \begin{environment}{definition} % The |definition| environment itself is quite simple. The only interesting thing is % that it locally defines the |definiendum| macro, which we do in the initialization % macro. % \begin{macro}{\definiendum} % The |\definiendum| macro is very simple: at the moment we do not do anything with the % keyword arguments. % \end{macro} % \begin{macrocode} %<*package> \def\st@definition@initialize{% \newcommand{\notatiendum}[2][]{\notemph{##2}} \newcommand{\definiendum}[2][]{\defemph{##2}}} \def\st@definition@terminate{} \define@statement@env{definition}{Definition} % %<*ltxml> DefCMPEnvironment('{definition} OptionalKeyVals:stat', sub { my ($doc, $keyvals, %props) = @_; my @symbols = @{$props{defs} || []}; foreach my $symb(@symbols) { $doc->openElement('omdoc:symbol', name=>$symb); $doc->closeElement('omdoc:symbol'); } my %attrs = (); my $id = $keyvals->getValue('id') if $keyvals; $attrs{'xml:id'} = $id if $id; my $ffor = $keyvals->getValue('for') if $keyvals; my $for = $ffor . join(' ',@symbols) if $ffor; $attrs{for} = $for if $for; $doc->openElement('omdoc:definition', %attrs); my $title = $keyvals->getValue('title') if $keyvals; if ($title) { $doc->openElement('omdoc:metadata'); $doc->openElement('dc:title'); $doc->absorb($title); $doc->closeElement('dc:title'); $doc->closeElement('omdoc:metadata'); } $doc->openElement('omdoc:CMP'); $doc->openElement('omdoc:p'); $doc->absorb($props{body}) if $props{body}; $doc->closeElement('omdoc:p'); $doc->closeElement('omdoc:CMP'); $doc->closeElement('omdoc:definition'); return; }, afterDigestBegin=>sub { my ($stomach, $whatsit) = @_; my @symbols = (); $whatsit->setProperty(defs=>\@symbols); AssignValue('defs', \@symbols, 'global'); return; }, afterDigest => sub { AssignValue('defs', undef, 'global'); return; }); DefConstructor('\definiendum[]{}', "#2", afterDigest => sub { my ($stomach, $whatsit) = @_; my $addr = LookupValue('defs'); push(@$addr, $whatsit->getArg(1)->toString) if $addr; $whatsit->setProperty(theory=>LookupValue('current_module')); return; }); % % \end{macrocode} % \end{environment} % % We expand the {\latexml} bindings for |\defin|, |\twindef| and |\atwindef| into two % instances one will be used for the definition and the other for indexing % % \begin{macrocode} %<*ltxml> DefMacro('\defin{}', sub { my @args = (T_BEGIN, $_[1]->unlist, T_END); (T_CS('\definiendum'), T_OTHER('['), $_[1]->unlist, T_OTHER(']'), @args, T_CS('\defin@index'), @args); }); DefMacro('\twindef{}{}', sub { my @args = (T_BEGIN, $_[1]->unlist, T_END, T_BEGIN, $_[2]->unlist, T_END); (T_CS('\twindef@def'), @args, T_CS('\twindef@index'), @args); }); DefMacro('\atwindef{}{}{}', sub { my @args = (T_BEGIN, $_[1]->unlist, T_END, T_BEGIN, $_[2]->unlist, T_END, T_BEGIN, $_[3]->unlist, T_END); (T_CS('\atwindef@def'), @args, T_CS('\atwindef@index'), @args); }); DefConstructor('\twindef@def{}{}', "#1 #2", afterDigest => sub { my ($stomach, $whatsit) = @_; my $addr = LookupValue('defs'); push(@$addr, $whatsit->getArg(1)->toString.'-'.$whatsit->getArg(2)->toString) if $addr; $whatsit->setProperty(theory=>LookupValue('current_module')); return; }, alias => ''); DefConstructor('\atwindef@def{}{}{}', "#1 #2 #3", afterDigest => sub { my ($stomach, $whatsit) = @_; my $addr = LookupValue('defs'); push(@$addr, $whatsit->getArg(1)->toString.'-'.$whatsit->getArg(2)->toString .'-'.$whatsit->getArg(3)->toString) if $addr; $whatsit->setProperty(theory=>LookupValue('current_module')); return; }, alias => ''); % % \end{macrocode} % % \begin{environment}{notation} % \begin{macrocode} %<*package> \def\notemph#1{{\bf{#1}}} \def\st@notation@initialize{\newcommand{\notatiendum}[2][]{\notemph{##2}}} \def\st@notation@terminate{} \define@statement@env{notation}{Notation} % %<*ltxml> DefCMPEnvironment('{notation} OptionalKeyVals:stat', "" . "?&KeyVal(#1,'title')(&KeyVal(#1,'title'))()" . "#body" . "\n"); DefConstructor('\notatiendum OptionalKeyVals:notation {}', "#1"); % % \end{macrocode} % \end{environment} % % \begin{macro}{\termin} % The |termin| macro is very simple, it forgets the semantic annotations\ednote{use % those for hyperlinking in the future} and puts the % \begin{macrocode} %<*package> \def\termin{\@ifnextchar[{\@termin}{\@termin[]}} \def\@termin[#1]#2{{\termemph{\index*{#2}}}} % % \end{macrocode} % \end{macro} % % Now we care about the configuration switches, they are set to sensible values, if they % are not defined already. These are just configuration parameters, which should not % appear in documents, therefore we do not provide {\latexml} bindings for them. % % \begin{macrocode} %<*package> \providecommand{\termemph}[1]{#1} \providecommand{\defemph}[1]{{\bf{#1}}} \providecommand{\stDMemph}[1]{{\bf{#1}}} % % \end{macrocode} % % \subsection{Providing IDs for {\omdoc} Elements}\label{sec:impl:ids} % % To provide default identifiers, we tag all {\omdoc} % elements that allow |xml:id| attributes by excuting the |numberIt| procedure from |omdoc.sty.ltxml|. % % \begin{macrocode} %<*ltxml.sty> Tag('omdoc:assertion',afterOpen=>\&numberIt); Tag('omdoc:definition',afterOpen=>\&numberIt); % % \end{macrocode} % % \subsection{Finale} % % Finally, we need to terminate the file with a success mark for perl. % \begin{macrocode} %1; % \end{macrocode} % \Finale \endinput % \iffalse % LocalWords: GPL structuresharing STR dtx keyval env envfalse idfalse idtrue % LocalWords: displayfalse envtrue displaytrue forfalse typefalse titlefalse % LocalWords: continuesfalse fortrue fromtrue typetrue titletrue % LocalWords: continuestrue consymb omtext %%% Local Variables: %%% mode: doctex %%% TeX-master: t %%% End: % \fi