diff options
author | Karl Berry <karl@freefriends.org> | 2008-05-20 17:50:33 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2008-05-20 17:50:33 +0000 |
commit | a62e1d4e096be4d689f337c35488333116c5e3e4 (patch) | |
tree | 803679fd4f27b12d609e5920df24f6855150c00c /Master/texmf-dist/source/latex/stex/sproof.dtx | |
parent | 9f0169e9cace9e8a9a261e3095ea97dac44f3d4a (diff) |
new package stex (10may08)
git-svn-id: svn://tug.org/texlive/trunk@8255 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/sproof.dtx')
-rw-r--r-- | Master/texmf-dist/source/latex/stex/sproof.dtx | 770 |
1 files changed, 770 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/sproof.dtx b/Master/texmf-dist/source/latex/stex/sproof.dtx new file mode 100644 index 00000000000..eb3581d1a53 --- /dev/null +++ b/Master/texmf-dist/source/latex/stex/sproof.dtx @@ -0,0 +1,770 @@ +% \iffalse meta-comment +% An Infrastructure for Structural Markup for Proofs +% 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 +% $URL: https://svn.kwarc.info/repos/stex/sty/stex/sproof/sproof.dtx $ +% $Rev: 423 $; last modified by $Author: kohlhase $ +% $Date: 2008-05-07 15:39:51 +0200 (Wed, 07 May 2008) $ +% \fi +% +% \iffalse +%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01] +%<package>\ProvidesPackage{sproof}[2006/01/13 v0.9a Semantic Markup for Proofs] +% +%<*driver> +\documentclass{ltxdoc} +\usepackage{url,array,stex,float,moreverb} +\usepackage[show]{ed} +\usepackage{hyperref} +\makeindex +\floatstyle{boxed} +\newfloat{exfig}{thp}{lop} +\floatname{exfig}{Example} +\begin{document}\DocInput{sproof.dtx}\end{document} +%</driver> +% \fi +% +% \CheckSum{407} +% +% \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}{2006/10/31}{made sproof.dtx independent of statements.dtx} +% \changes{v0.9d}{2006/10/31}{revamped the proof end mark management} +% +% \GetFileInfo{sproofs.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\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}} +% \title{Structural Markup for Proofs\thanks{Version {\fileversion} (last revised +% {\filedate})}} +% \author{Michael Kohlhase\\ +% Jacobs University, Bremen\\ +% \url{http://kwarc.info/kohlhase}} +% \maketitle +% +% \begin{abstract} +% The |sproof| 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 supplies macros and environment that allow to annotate the structure of +% mathematical proofs 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} +% +%\section{Introduction}\label{sec:sproof} +% +% The |sproof| ({\twintoo{semantic}{proofs}}) package supplies macros and environment that +% allow to annotate the structure of mathematical proofs in {\stex} files. 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 |statements|. +% +% {\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). +% +% \begin{exfig}\scriptsize +% \begin{verbatim} +% \begin{sproof}[id=simple-proof,for=sum-over-odds] +% {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} +% \begin{spfcases}{For the induction we have to consider the following cases:} +% \begin{spfcase}{$n=1$} +% \begin{spfstep}[display=flow] then we compute $1=1^2$\end{spfstep} +% \end{spfcase} +% \begin{spfcase}{$n=2$} +% \begin{sproofcomment}[display=flow] +% This case is not really necessary, but we do it for the +% fun of it (and to get more intuition). +% \end{sproofcomment} +% \begin{spfstep}[display=flow] We compute $1+3=2^{2}=4$.\end{spfstep} +% \end{spfcase} +% \begin{spfcase}{$n>1$} +% \begin{spfstep}[type=assumption,id=ind-hyp] +% Now, we assume that the assertion is true for a certain $k\geq 1$, +% i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$. +% \end{spfstep} +% \begin{sproofcomment} +% We have to show that we can derive the assertion for $n=k+1$ from +% this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. +% \end{sproofcomment} +% \begin{spfstep} +% We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$ +% \begin{justification}[method=arith:split-sum] +% by splitting the sum. +% \end{justification} +% \end{spfstep} +% \begin{spfstep} +% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ +% \begin{justification}[method=fertilize] by inductive hypothesis.\end{justification} +% \end{spfstep} +% \begin{spfstep}[type=conclusion] +% We can \begin{justification}[method=simplify]simplify\end{justification} +% the right-hand side to ${k+1}^2$, which proves the assertion. +% \end{spfstep} +% \end{spfcase} +% \begin{spfstep}[type=conclusion] +% We have considered all the cases, so we have proven the assertion. +% \end{spfstep} +% \end{spfcases} +% \end{sproof} +% \end{verbatim} +% \vspace*{-.5cm} +% \caption{A very explicit proof, marked up semantically}\label{fig:proof:src} +% \end{exfig} +% +% We will go over the general intuition by way of our running example (see +% Figure~\ref{fig:proof:src} for the source and Figure~\ref{fig:proof:result} for the +% formatted result).\ednote{talk a bit more about proofs and their structure,... maybe +% copy from OMDoc spec. } +% +% \section{The User Interface} +% +% \subsection{Proofs and Proof steps} +% +% \DescribeEnv{sproof} The |proof| environment is the main container for proofs. It takes +% an optional |KeyVal| argument that allows to specify the |id| (identifier) and |for| +% (for which assertion is this a proof) keys. The regular argument of the |proof| +% environment contains an introductory comment, that may be used to announce the proof +% style. The |proof| environment contains a sequence of |\step|, |proofcomment|, and +% |pfcases| environments that are used to markup the proof steps. The |proof| environment +% has a variant |Proof|, which does not use the proof end marker. This is convenient, if a +% proof ends in a case distinction, which brings it's own proof end marker with it. +% \DescribeEnv{sProof} The |Proof| environment is a variant of |proof| that does not mark +% the end of a proof with a little box; presumably, since one of the subproofs already has +% one and then a box supplied by the outer proof would generate an otherwise empty line. +% \DescribeMacro{\sproofidea} The |\sproofidea| macro allows to give a one-paragraph +% description of the proof idea. +% +% \DescribeEnv{spfstep} Regular proof steps are marked up with the |step| environment, which +% takes an optional |KeyVal| argument for annotations. A proof step usually contains a +% local assertion (the text of the step) together with some kind of evidence that this can +% be derived from already established assertions. +% +% Note that both |\premise| and |\justarg| can be used with an empty second argument to +% mark up premises and arguments that are not explicitly mentioned in the text. +% +% \begin{exfig} +% \begin{sproof}[id=simple-proof,for=sum-over-odds] +% {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} +% \begin{spfcases}{For the induction we have to consider the following cases:} +% \begin{spfcase}{$n=1$} +% \begin{spfstep}[display=flow] then we compute $1=1^2$\end{spfstep} +% \end{spfcase} +% \begin{spfcase}{$n=2$} +% \begin{sproofcomment}[display=flow] +% This case is not really necessary, but we do it for the fun +% of it (and to get more intuition). +% \end{sproofcomment} +% \begin{spfstep}[display=flow] +% We compute $1+3=2^{2}=4$ +% \end{spfstep} +% \end{spfcase} +% \begin{spfcase}{$n>1$} +% \begin{spfstep}[type=hypothesis,id=ind-hyp] +% Now, we assume that the assertion is true for a certain $k\geq 1$, i.e. +% $\sum_{i=1}^k{(2i-1)}=k^{2}$. +% \end{spfstep} +% \begin{sproofcomment} +% We have to show that we can derive the assertion for $n=k+1$ from this +% assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. +% \end{sproofcomment} +% \begin{spfstep}[id=splitit] +% We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$ +% \begin{justification}[method=arith:split-sum] +% by splitting the sum +% \end{justification} +% \end{spfstep} +% \begin{spfstep}[id=byindhyp] +% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ +% \begin{justification}[method=fertilize] +% by \premise[ind-hyp]{inductive hypothesis}. +% \end{justification} +% \end{spfstep} +% \begin{spfstep}[type=conclusion] +% We can \begin{justification}[method=simplify-eq] +% simplify the {\justarg[rhs]{right-hand side}} +% \end{justification} to ${k+1}^2$, which proves the assertion. +% \end{spfstep} +% \end{spfcase} +% \begin{spfstep}[type=conclusion] +% We have considered all the cases, so we have proven the assertion. +% \end{spfstep} +% \end{spfcases} +% \end{sproof} +% \caption{The formatted result of the proof in Figure~\ref{fig:proof:src}}\label{fig:proof:result} +% \end{exfig} +% +% \subsection{Justifications} +% +% \DescribeEnv{justification} This evidence is marked up with the |justification| +% environment in the |sproof| package. This environment totally invisible to the formatted +% result; it wraps the text in the proof step that corresponds to the evidence. The +% environment takes an optional |KeyVal| argument, which can have the |method| key, whose +% value is the name of a proof method (this will only need to mean something to the +% application that consumes the semantic annotations). Furthermore, the justification can +% contain ``premises'' (specifications to assertions that were used justify the step) and +% ``arguments'' (other information taken into account by the proof method). +% +% \DescribeMacro{\premise} The |\premise| macro allows to mark up part of the text as +% reference to an assertion that is used in the argumentation. In the example in +% Figure~\ref{fig:proof:src} we have used the |\premise| macro to identify the inductive +% hypothesis. +% +% \DescribeMacro{\justarg} The |\justarg| macro is very similar to |\premise| with the +% difference that it is used to mark up arguments to the proof method. Therefore the +% content of the first argument is interpreted as a mathematical object rather than as an +% identifier as in the case of |\premise|. In our example, we specified that the +% simplification should take place on the right hand side of the equation. Other examples +% include proof methods that instantiate. Here we would indicate the substituted object in +% a |\justarg| macro. +% +% \subsection{Proof Structure} +% +% \DescribeEnv{spfcases} The |pfcases| environment is used to mark up a proof by +% cases. This environment takes an optional |KeyVal| argument for semantic annotations and +% a second argument that allows to specify an introductory comment (just like in the +% |proof| environment). +% +% \DescribeEnv{spfcase} The content of a |pfcases| environment are a sequence of case +% proofs marked up in the |pfcase| environment, which takes an optional |KeyVal| argument +% for semantic annotations. The second argument is used to specify the the description of +% the case under considertation. The content of a |pfcase| environment is the same as that +% of a |proof|, i.e. |step|s, |proofcomment|s, and |pfcases| environments. +% +% \DescribeEnv{sproofcomment} The |proofcomment| environment is much like a |step|, only +% that it does not have an obejct-level assertion of its own. Rather than asserting some +% fact that is relevant for the proof, it is used to explain where the proof is going, +% what we are attempting to to, or what we have achieved so far. As such, it cannot be the +% target of a |\premise|. +% +% \subsection{Proof End Markers} +% +% Traditionally, the end of a mathematical proof is marked with a little box at the end of +% the last line of the proof (if there is space and on the end of the next line if there +% isn't), like so:\sproofend +% +% The |sproof| package provides the \DescribeMacro{\sproofend}|\sproofend| macro for +% this. If a different symbol for the proof end is to be used (e.g. {\sl{q.e.d}}), then +% this can be obtained by specifying it using the +% \DescribeMacro{\sProofEndSymbol}|\sProofEndSymbol| configuration macro (e.g. by specifying +% |\sProofEndSymbol{q.e.d}|). +% +% Some of the proof structuring macros above will insert proof end symbols for sub-proofs, +% in most cases, this is desirable to make the proof structure explicit, but sometimes +% this wastes space (especially, if a proof ends in a case analysis which will supply its +% own proof end marker). Therefore, all proof environments have the +% \DescribeMacro{noproofend}|noproofend| keyword that suppresses the proof end markers for +% this element. It can be specified on its own, and does not need a value (if one is +% specified, that is completely ignored). +% +% \StopEventually{\ednotemessage} +% +% \section{The Implementation} +% +% We first set up the Perl Packages for {\latexml} +% \begin{macrocode} +%<*ltxml> +# -*- CPERL -*- +package LaTeXML::Package::Pool; +use strict; +use LaTeXML::Package; +RequirePackage('omdoc'); +%</ltxml> +% Then we make sure that the {\stex} |omdoc| package is loaded. +% \begin{macrocode} +%<*package> +\RequirePackage{omdoc}[2007/09/09] +%</package> +% \end{macrocode} +% Then we define the pacakge options and what they do. +% \begin{macrocode} +%<*package> +\newif\ifjust@method\just@methodfalse +\DeclareOption{method}{\just@methodtrue} +%</package> +% \end{macrocode} +% 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). Firpf we have the general options +% \begin{macrocode} +%<*package> +\newif\ifspf@env\spf@envfalse +\newif\ifspf@id\spf@idfalse +\newif\ifspf@display\spf@displayfalse +\DeclareOption{id}{\spf@idtrue\spf@envtrue} +\DeclareOption{env}{\spf@envtrue} +\DeclareOption{display}{\spf@displaytrue\spf@envtrue} +% \end{macrocode} +% And then the options that are specific to the |sproof| package. +% \begin{macrocode} +\newif\ifspf@for\spf@forfalse +\newif\ifspf@from\spf@forfalse +\newif\ifspf@type\spf@typefalse +\newif\ifspf@title\spf@titlefalse +\newif\ifspf@proofend\spf@proofendtrue +\newif\ifspf@continues\spf@continuesfalse +\DeclareOption{for}{\spf@fortrue\spf@envtrue} +\DeclareOption{from}{\spf@fromtrue\spf@envtrue} +\DeclareOption{type}{\spf@typetrue\spf@envtrue} +\DeclareOption{title}{\spf@titletrue\spf@envtrue} +\DeclareOption{continues}{\spf@continuepfrue\spf@envtrue} +\DeclareOption{noproofend}{\spf@proofendfalse\spf@envtrue} +% \end{macrocode} +% \begin{macro}{\spftrue} +% For convenience, we collect the switches into one. +% \begin{macrocode} +\def\spftrue{\spf@fortrue\spf@fromtrue\spf@typetrue\spf@continuepfrue} +% \end{macrocode} +% \end{macro} +% +% Now, we define a set of collective options and tell {\LaTeX} about the end of the +% declaration section. +% \begin{macrocode} +\DeclareOption{draft}{\spf@envtrue\just@methodtrue} +\DeclareOption{all}{\spf@envtrue\just@medhodtrue} +\ProcessOptions +%</package> +% \end{macrocode} +% +% \subsection{Proofs}\label{sec:impl:proofs} +% +% \begin{macrocode} +%<*package> +\define@key{spf}{id}{\def\spf@id{#1}} +\define@key{spf}{display}{\def\spf@display{#1}} +\define@key{spf}{for}{\def\spf@for{#1}} +\define@key{spf}{from}{\def\spf@from{#1}} +\define@key{spf}{sproofend}{\spf@proofendtrue\def\sproof@box{#1}} +\define@key{spf}{noproofend}[imeanit]{\spf@proofendfalse} +\define@key{spf}{type}{\def\spf@type{#1}} +\define@key{spf}{title}{\def\spf@title{#1}} +\define@key{spf}{continues}{\def\spf@continues{#1}} +%</package> +%<*ltxml> +DefKeyVal('pf','id','Semiverbatim'); +DefKeyVal('pf','display','Semiverbatim'); # not used at the moment +DefKeyVal('pf','for','Semiverbatim'); +DefKeyVal('pf','from','Semiverbatim'); +DefKeyVal('pf','proofend','Semiverbatim'); +DefKeyVal('pf','noproofend','Semiverbatim'); +DefKeyVal('pf','type','Semiverbatim'); +DefKeyVal('pf','title','Semiverbatim'); +DefKeyVal('pf','continues','Semiverbatim'); +%</ltxml> +% \end{macrocode} +% +% \begin{macro}{\show@st@keys@aux} +% We now define a macro that shows the |st| keys, if in draft mode, they annotate the +% document with key/value pairs. +% \begin{macrocode} +%<*package> +\def\show@st@keys@aux{% +\@ifundefined{spf@id}{}{\ifspf@id{id=\spf@id},\fi}% +\@ifundefined{spf@display}{}{\ifspf@display{display=\spf@display}\fi}} +\def\clear@pf@keys{\let\spf@id=\relax\let\spf@display=\relax} +%</package> +% \end{macrocode} +% \end{macro} +% \begin{macro}{\show@pf@keys@aux} +% we do the same for the |pf| keys. +% \begin{macrocode} +%<*package> +\def\show@pf@keys@aux{% +\@ifundefined{spf@for}{}{\ifspf@for{for=\spf@for},\fi}% +\@ifundefined{spf@from}{}{\ifspf@from{from=\spf@from},\fi}% +\@ifundefined{spf@prefix}{}{\ifspf@prefix{prefix=\spf@prefix},\fi}% +\@ifundefined{spf@type}{}{\ifspf@type{type=\spf@type},\fi}% +\@ifundefined{spf@title}{}{\ifspf@title{title=\spf@title},\fi}% +\@ifundefined{spf@continues}{}{\ifspf@continues{continues=\spf@continues}\fi}} +%</package> +% \end{macrocode} +% \end{macro} +% \begin{macro}{\show@pf@keys} +% and combine them, so that the code is more readable. +% \begin{macrocode} +%<*package> +\def\show@pf@keys#1{\footnote{#1[\show@pf@keys@aux\show@pf@keys@aux]}% +\clear@pf@keys\clear@pf@keys} +\def\clear@pf@keys{\let\spf@for=\relax\let\spf@from=\relax\let\spf@prefix=\relax% +\let\spf@type=\relax\let\spf@title=\relax\let\spf@continues=\relax} +%</package> +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\spf@flow} +% We define this macro, so that we can test whether the |display| key has the value |flow| +% \begin{macrocode} +%<package>\def\spf@flow{flow} +% \end{macrocode} +% \end{macro} +% +% For proofs, we will have to have deeply nested structures of enumerated list-like +% environments. However, {\LaTeX} only allows |enumerate| environments up to nesing depth +% 4 and general list environments up to listing depth 6. This is not enough for us. +% Therefore we have decided to go along the route proposed by Leslie Lamport to use a +% single top-level list with dotted sequences of numbers to identify the position in the +% proof tree. Unfortunately, we could not use his |pf.sty| package directly, since it does +% not do automatic numbering, and we have to add keyword arguments all over the place, to +% accomodate semantic information. +% +% \begin{environment}{pst@with@label} +% This environment manages\ednote{This gets the labeling right but only works 8 levels +% deep} the path labeling of the proof steps in the description envionment of the +% outermost |proof| environment. The argument is the label prefix up to now; which we +% cache in |\pst@label| (we need evaluate it first, since are in the right place +% now!). Then we increment the proof depth which is stored in |\count10| (lower +% counters are used by {\TeX} for page numbering) and initialize +% the next level counter |\count\count10| with 1. In the end call for this environment, +% we just decrease the proof depth counter by 1 again. +% \begin{macrocode} +%<*package> +\newenvironment{pst@with@label}[1]{\edef\pst@label{#1}\advance\count10 by 1\count\count10=1} +{\advance\count10 by -1} +% \end{macrocode} +% \end{environment} +% +% \begin{macro}{\the@pst@label} +% |\the@pst@label| evaluates to the current step label. +% \begin{macrocode} +\def\the@pst@label{\pst@label.\number\count\count10} +% \end{macrocode} +%\end{macro} +% +% \begin{macro}{\next@pst@label} +% |\next@pst@label| increments the step label at the current level. +% \begin{macrocode} +\def\next@pst@label{\global\advance\count\count10 by 1} +% \end{macrocode} +%\end{macro} +% +%\begin{macro}{\sproofend} +% This macro places a little box at the end of the line if there is space, or at the +% end of the next line if there isn't +% \begin{macrocode} +\def\sproof@box{\hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}} +\def\sproofend{\ifspf@proofend\hfil\null\nobreak\hfill\sproof@box\par\smallskip\fi} +\def\sProofEndSymbol#1{\def\sproof@box{#1}} +%</package> +%<ltxml>DefConstructor('\sproofend',""); +% \end{macrocode} +% \end{macro} +% +% \begin{environment}{sproof} +% In this environment, we initialize the proof depth counter |\count10| to 10, and set +% up the description environment that will take the proof steps. At the end of the +% proof, we position the proof end into the last line. +% \begin{macrocode} +%<*package> +\newenvironment{@proof}[2][]{\setkeys{spf}{#1} +\count10=10\ifx\spf@display\spf@flow\else{\stDMemph{Proof}:}\fi% +\ifspf@env\show@pf@keys{sproof}\fi{ #2}% +\def\pst@label{}\newcount\pst@count% initialize the labeling mechanism +\begin{description}\begin{pst@with@label}{P}} +{\end{pst@with@label}\end{description}} +\newenvironment{sproof}[2][]{\begin{@proof}[#1]{#2}}{\sproofend\end{@proof}} +%</package> +%<*ltxml> +DefEnvironment('{sproof} OptionalKeyVals:pf{}', + "<omdoc:proof ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n" + . "?#2(<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n)()" + . "#body" + . "</omdoc:proof>\n"); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% \begin{environment}{sproofidea} +% \begin{macrocode} +%<package>\newcommand{\sproofidea}[2][]{{\stDMemph{Proof Idea}:} #2\sproofend} +%<*ltxml> +DefEnvironment('{sproofidea} OptionalKeyVals:pf {}', + "<omdoc:proof ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n" + . "<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n" + . "</omdoc:proof>\n"); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% The next two environments (proof steps) and comments, are mostly semantical, they take +% |KeyVal| arguments that specify their semantic role. In draft mode, they read these +% values and show them. If the surrounging proof had |display=flow|, then no new |\item| is +% generated, otherwise it is. In any case, the proof step number (at the current level) is +% incremented. +% \begin{environment}{spfstep} +% \begin{macrocode} +%<*package> +\newenvironment{spfstep}[1][]{\setkeys{spf}{#1} +\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi +\@ifundefined{spf@title}{}{(\stDMemph{\spf@title})}% +\ifspf@env\show@pf@keys{spfstep}\fi} +{\next@pst@label} +%</package> +%<*ltxml> +DefCMPEnvironment('{spfstep} OptionalKeyVals:pf', + "<omdoc:derive ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>" + . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>" + . "</omdoc:derive>\n"); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% \begin{environment}{sproofcomment} +% \begin{macrocode} +%<*package> +\newenvironment{sproofcomment}[1][]{\setkeys{spf}{#1} +\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi +\ifspf@env\show@pf@keys{sproofcomment}\fi} +{\next@pst@label} +%</package> +%<*ltxml> +DefCMPEnvironment('{sproofcomment} OptionalKeyVals:pf', + "<omdoc:omtext ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>" + . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>" + . "</omdoc:omtext>"); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% The next two environments also take a |KeyVal| arguement, but also a regular one, which +% contains a start text. Both environments start a new numbered proof level. +% +% \begin{environment}{spfcases} +% In the |pfcases| environment, the start text is displayed as the first comment of the +% proof. +% \begin{macrocode} +%<*package> +\newenvironment{spfcases}[2][]{\setkeys{spf}{#1} +\def\@test{#2}\ifx\@test\empty\else +\ifx\spf@display\spf@flow {#2}\else\item[\the@pst@label]{#2} \fi\fi +\ifspf@env\show@pf@keys{spfcases}\fi +\begin{pst@with@label}{\pst@label.\number\count\count10}} +{\end{pst@with@label}\next@pst@label} +%</package> +%<*ltxml> +DefEnvironment('{spfcases} OptionalKeyVals:pf {}', + "<omdoc:derive ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n" + . "<omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP>\n" + . "<omdoc:method xref='#proof-by-cases'>" + . "#body" + . "</omdoc:method>" + . "</omdoc:derive>\n"); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% \begin{environment}{spfcase} +% In the |pfcase| environment, the start text is displayed specification of the case +% after the |\item| +% \begin{macrocode} +%<*package> +\newenvironment{spfcase}[2][]{\setkeys{spf}{#1} +\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi +\def\@test{#2}\ifx\@test\empty\else{\stDMemph{#2}:}\fi +\ifspf@env\show@pf@keys{spfcase}\fi +\begin{pst@with@label}{\pst@label.\number\count\count10}} +{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}\next@pst@label} +%</package> +%<*ltxml> +DefEnvironment('{spfcase} OptionalKeyVals:pf{}', + "<omdoc:proof ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n" + . "?#2(<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n)()" + . "#body" + . "</omdoc:proof>\n"); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% \begin{environment}{subproof} +% In the |subproof| environment, a new (lower-level) proof environment is +% started.\ednote{document this above} +% \begin{macrocode} +%<*package> +\newenvironment{subproof}{\begin{pst@with@label}{\pst@label.\number\count\count10}} +{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}} +%</package> +%<*ltxml> +DefEnvironment('{subproof}', + "<omdoc:proof>\n #body\n</omdoc:proof>\n"); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% \subsection{Justifications} +% +% We define the actions that are undertaken, when the keys for justifications are +% encountered. Here this is very simple, we just define an internal macro with the value, +% so that we can use it later.\ednote{why are there more in ltxml?, why st@id?} +% \begin{macrocode} +%<*package> +\define@key{just}{id}{\def\just@id{#1}} +\define@key{just}{method}{\def\just@method{#1}} +%</package> +%<*ltxml> +DefKeyVal('just','id','Semiverbatim'); +DefKeyVal('just','method','Semiverbatim'); +DefKeyVal('just','premises','Semiverbatim'); +DefKeyVal('just','args','Semiverbatim'); +%</ltxml> +% \end{macrocode} +% +% \begin{macro}{\show@just@keys} +% This macro shows all the key/value pairs when in draft mode. +% \begin{macrocode} +%<*package> +\def\show@just@keys#1{\footnote{#1[\show@pf@keys@aux\show@just@keys@aux]}}% +\def\show@just@keys@aux{% +\@ifundefined{just@method}{\relax}{\ifjust@method{method=\just@method},\fi}% +\clear@pf@keys\clear@just@keys} +\def\clear@just@keys{\let\just@method=\relax} +%</package> +% \end{macrocode} +% \end{macro} +% +% The next three environments and macros are purely semantic, so we ignore the keyval +% arguments for now and only display the content.\ednote{need to do something about the +% premise in draft mode.} +% +% \begin{environment}{justification} +% \begin{macrocode} +%<*package> +\newenvironment{justification}[1][]{\ifspf@env\setkeys{just}{#1} + \show@just@keys{justification}\fi}{} +%</package> +%<*ltxml> +sub extractBodyText { + my ($box, $remove) = @_; + my $str = ''; + my @boxes = $box->unlist; + foreach my $b(@boxes) { + my $s = ''; + if ($b =~ /LaTeXML::Whatsit/) { + my $body = $b->getBody; + $s = $body ? extractBodyText($body, $remove) : ''; + } elsif ($b =~ /LaTeXML::Box/) { + $s = $b->toString || ''; + @{$b}[0] = '' if $remove; } + $str .= $s; } + $str =~ s/\s+/ /g; + $str; } + +DefEnvironment('{justification} OptionalKeyVals:just', sub { + my ($doc, $keys, %props) = @_; + my $text = extractBodyText($props{body}, 1); + my $node = LookupValue('_LastSeenCMP'); + $node->appendText($text) if $node; + my $method = $keys ? $keys->getValue('method') : undef; + $doc->openElement("omdoc:method", $method ? (xref => $method) : ()); + $doc->absorb($props{body}) if $props{body}; + $doc->closeElement("omdoc:method"); + return; }); +%</ltxml> +% \end{macrocode} +% \end{environment} +% +% \begin{macro}{\premise} +% \begin{macrocode} +%<*package> +\newcommand{\premise}[2][]{#2} +%</package> +%<*ltxml> +DefMacro('\premise[]{}', sub { + my ($xref, $text) = ($_[1], $_[2]); + my @res = (T_CS('\premise@content')); + push(@res, T_OTHER('['), $xref->unlist, T_OTHER(']')) if $xref; + push(@res, T_SPACE, $text->unlist) if $text; + @res; }); +DefConstructor('\premise@content[]', "<omdoc:premise xref='#1'/>"); +%</ltxml> +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\justarg} +% the |\justarg| macro is purely semantic, so we ignore the keyval arguments for now and +% only display the content. +% \begin{macrocode} +%<*package> +\newcommand{\justarg}[2][]{#2} +%</package> +%<*ltxml> +DefMacro('\justarg[]{}', sub { (($_[1] ? $_[1]->unlist : ()), + T_SPACE, $_[2]->unlist, T_SPACE); }); + +Tag('omdoc:derive', afterClose=>sub { + my ($doc, $node) = @_; + my @children = grep($_->nodeType == XML_ELEMENT_NODE, $node->childNodes); + my $firstCMP = undef; + foreach my $child(@children) { + next unless ($child->localname || '') eq 'CMP'; + if ($child->hasChildNodes()) { + next unless $#{$child->childNodes} == 0; + next unless $child->firstChild->nodeType == XML_TEXT_NODE; } + + if ($firstCMP) { + $firstCMP->appendText($child->textContent); + $node->removeChild($child); + } else { $firstCMP = $child; } + } + }); + +%</ltxml> +% \end{macrocode} +% \end{macro} +% +% \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> +Tag('omdoc:proof',afterOpen=>\&numberIt); +Tag('omdoc:derive',afterOpen=>\&numberIt); +Tag('omdoc:method',afterOpen=>\&numberIt); +%</ltxml> +% \end{macrocode} +% +% \section{Finale} +% +% Finally, we need to terminate the file with a success mark for perl. +% \begin{macrocode} +%<ltxml>1; +% \end{macrocode} +% \Finale +\endinput + +% \iffalse +% LocalWords: GPL structuresharing STR sproof dtx CPERL keyval methodfalse env +%%% Local Variables: +%%% mode: doctex +%%% TeX-master: t +%%% End: +% \fi +% LocalWords: methodtrue envtrue medhodtrue DefKeyVal Semiverbatim omdoc args +% LocalWords: DefEnvironment OptionalKeyVals KeyVal omtext DefConstructor str +% LocalWords: proofidea KeyVal pfstep DefCMPEnvironment KeyVal proofcomment eq +% LocalWords: KeyVal pfcases KeyVal pfcase KeyVal extractBodyText unlist elsif +% LocalWords: foreach getBody toString str str str LookupValue LastSeenCMP +% LocalWords: appendText getValue undef openElement closeElement DefMacro +% LocalWords: afterClose nodeType childNodes firstCMP localname hasChildNodes +% LocalWords: firstChild textContent removeChild |