]> matita.cs.unibo.it Git - helm.git/commitdiff
continuationals semantics: first draft
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 30 Sep 2005 13:44:36 +0000 (13:44 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 30 Sep 2005 13:44:36 +0000 (13:44 +0000)
helm/ocaml/tactics/doc/.cvsignore [new file with mode: 0644]
helm/ocaml/tactics/doc/Makefile [new file with mode: 0644]
helm/ocaml/tactics/doc/infernce.sty [new file with mode: 0644]
helm/ocaml/tactics/doc/ligature.sty [new file with mode: 0644]
helm/ocaml/tactics/doc/main.tex [new file with mode: 0644]
helm/ocaml/tactics/doc/reserved.sty [new file with mode: 0644]
helm/ocaml/tactics/doc/semantic.sty [new file with mode: 0644]
helm/ocaml/tactics/doc/shrthand.sty [new file with mode: 0644]
helm/ocaml/tactics/doc/tdiagram.sty [new file with mode: 0644]

diff --git a/helm/ocaml/tactics/doc/.cvsignore b/helm/ocaml/tactics/doc/.cvsignore
new file mode 100644 (file)
index 0000000..583537c
--- /dev/null
@@ -0,0 +1,6 @@
+main.aux
+main.dvi
+main.log
+main.out
+main.pdf
+main.ps
diff --git a/helm/ocaml/tactics/doc/Makefile b/helm/ocaml/tactics/doc/Makefile
new file mode 100644 (file)
index 0000000..4db53fd
--- /dev/null
@@ -0,0 +1,120 @@
+
+#
+# Generic makefile for latex
+#
+# Author: Stefano Zacchiroli <zack@bononia.it>
+#
+# Created:       Sun, 29 Jun 2003 12:00:55 +0200 zack
+# Last-Modified: Tue, 05 Apr 2005 10:25:38 +0200 zack
+#
+
+########################################################################
+
+# list of .tex _main_ files
+TEXS = main.tex
+
+# number of runs of latex (for table of contents, list of figures, ...)
+RUNS = 1
+
+# do you need bibtex?
+BIBTEX = no
+
+# would you like to use pdflatex?
+PDF_VIA_PDFLATEX = yes
+
+# which formats generated by default ("all" target)?
+# (others will be generated by "world" target)
+# see AVAILABLE_FORMATS below 
+BUILD_FORMATS = dvi
+
+# which format to be shown on "make show"
+SHOW_FORMAT = dvi
+
+########################################################################
+
+AVAILABLE_FORMATS = dvi ps ps.gz pdf html
+
+ADVI = advi
+BIBTEX = bibtex
+BROWSER = galeon
+DVIPDF = dvipdf
+DVIPS = dvips
+GV = gv
+GZIP = gzip
+HEVEA = hevea
+ISPELL = ispell
+LATEX = latex
+XDVI = xdvi
+XPDF = xpdf
+PDFLATEX = pdflatex
+
+ALL_FORMATS = $(BUILD_FORMATS)
+WORLD_FORMATS = $(AVAILABLE_FORMATS)
+
+all: $(ALL_FORMATS)
+world: $(WORLD_FORMATS)
+
+DVIS = $(TEXS:.tex=.dvi)
+PSS = $(TEXS:.tex=.ps)
+PSGZS = $(TEXS:.tex=.ps.gz)
+PDFS = $(TEXS:.tex=.pdf)
+HTMLS = $(TEXS:.tex=.html)
+
+dvi: $(DVIS)
+ps: $(PSS)
+ps.gz: $(PSGZS)
+pdf: $(PDFS)
+html: $(HTMLS)
+
+show: show$(SHOW_FORMAT)
+showdvi: $(DVIS)
+       $(XDVI) $<
+showps: $(PSS)
+       $(GV) $<
+showpdf: $(PDFS)
+       $(XPDF) $<
+showpsgz: $(PSGZS)
+       $(GV) $<
+showps.gz: showpsgz
+showhtml: $(HTMLS)
+       $(BROWSER) $<
+
+clean:
+       rm -f \
+               $(TEXS:.tex=.dvi) $(TEXS:.tex=.ps) $(TEXS:.tex=.ps.gz) \
+               $(TEXS:.tex=.pdf) $(TEXS:.tex=.aux) $(TEXS:.tex=.log) \
+               $(TEXS:.tex=.html) $(TEXS:.tex=.out) $(TEXS:.tex=.haux) \
+               $(TEXS:.tex=.htoc) $(TEXS:.tex=.tmp)
+
+%.dvi: %.tex
+       $(LATEX) $<
+       if [ "$(BIBTEX)" = "yes" ]; then $(BIBTEX) $*; fi
+       if [ "$(RUNS)" -gt 1 ]; then \
+               for i in seq 1 `expr $(RUNS) - 1`; do \
+                       $(LATEX) $<; \
+               done; \
+       fi
+ifeq ($(PDF_VIA_PDFLATEX),yes)
+%.pdf: %.tex
+       $(PDFLATEX) $<
+       if [ "$(BIBTEX)" = "yes" ]; then $(BIBTEX) $*; fi
+       if [ "$(RUNS)" -gt 1 ]; then \
+               for i in seq 1 `expr $(RUNS) - 1`; do \
+                       $(PDFLATEX) $<; \
+               done; \
+       fi
+else
+%.pdf: %.dvi
+       $(DVIPDF) $< $@
+endif
+%.ps: %.dvi
+       $(DVIPS) $<
+%.ps.gz: %.ps
+       $(GZIP) -c $< > $@
+%.html: %.tex
+       $(HEVEA) -fix $<
+
+.PHONY: all ps pdf html clean
+
+########################################################################
+
diff --git a/helm/ocaml/tactics/doc/infernce.sty b/helm/ocaml/tactics/doc/infernce.sty
new file mode 100644 (file)
index 0000000..fc4afea
--- /dev/null
@@ -0,0 +1,217 @@
+%%
+%% This is file `infernce.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,inference')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from infernce.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak
+      but by using \protect\usepackage{semantic} in your document
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+\TestForConflict{\@@tempa,\@@tempb,\@adjustPremises,\@inference}
+\TestForConflict{\@inferenceBack,\@inferenceFront,\@inferenceOrPremis}
+\TestForConflict{\@premises,\@processInference,\@processPremiseLine}
+\TestForConflict{\@setLengths,\inference,\predicate,\predicatebegin}
+\TestForConflict{\predicateend,\setnamespace,\setpremisesend}
+\TestForConflict{\setpremisesspace,\@makeLength,\@@space}
+\TestForConflict{\@@aLineBox,\if@@shortDivider}
+\newtoks\@@tempa
+\newtoks\@@tempb
+\newcommand{\@makeLength}[4]{
+  \@@tempa=\expandafter{\csname @@#2\endcsname}
+  \@@tempb=\expandafter{\csname @set#2\endcsname} %
+  \expandafter \newlength \the\@@tempa
+  \expandafter \newcommand \the\@@tempb {}
+  \expandafter \newcommand \csname set#1\endcsname[1]{}
+  \expandafter \xdef \csname set#1\endcsname##1%
+    {{\dimen0=##1}%
+      \noexpand\renewcommand{\the\@@tempb}{%
+        \noexpand\setlength{\the \@@tempa}{##1 #4}}%
+    }%
+  \csname set#1\endcsname{#3}
+  \@@tempa=\expandafter{\@setLengths} %
+  \edef\@setLengths{\the\@@tempa \the\@@tempb} %
+  }
+
+\newcommand{\@setLengths}{%
+  \setlength{\baselineskip}{1.166em}%
+  \setlength{\lineskip}{1pt}%
+  \setlength{\lineskiplimit}{1pt}}
+\@makeLength{premisesspace}{pSpace}{1.5em}{plus 1fil}
+\@makeLength{premisesend}{pEnd}{.75em}{plus 0.5fil}
+\@makeLength{namespace}{nSpace}{.5em}{}
+\newbox\@@aLineBox
+\newif\if@@shortDivider
+\newcommand{\@@space}{ }
+\newcommand{\predicate}[1]{\predicatebegin #1\predicateend}
+\newcommand{\predicatebegin}{$}
+\newcommand{\predicateend}{$}
+\def\inference{%
+  \@@shortDividerfalse
+  \expandafter\hbox\bgroup
+  \@ifstar{\@@shortDividertrue\@inferenceFront}%
+          \@inferenceFront
+}
+\def\@inferenceFront{%
+  \@ifnextchar[%
+     {\@inferenceFrontName}%
+     {\@inferenceMiddle}%
+}
+\def\@inferenceFrontName[#1]{%
+  \setbox3=\hbox{\footnotesize #1}%
+  \ifdim \wd3 > \z@
+    \unhbox3%
+    \hskip\@@nSpace
+  \fi
+  \@inferenceMiddle
+}
+\long\def\@inferenceMiddle#1{%
+  \@setLengths%
+  \setbox\@@pBox=
+    \vbox{%
+      \@premises{#1}%
+      \unvbox\@@pBox
+    }%
+  \@inferenceBack
+}
+\long\def\@inferenceBack#1{%
+  \setbox\@@cBox=%
+   \hbox{\hskip\@@pEnd \predicate{\ignorespaces#1}\unskip\hskip\@@pEnd}%
+  \setbox1=\hbox{$ $}%
+  \setbox\@@pBox=\vtop{\unvbox\@@pBox
+                 \vskip 4\fontdimen8\textfont3}%
+  \setbox\@@cBox=\vbox{\vskip 4\fontdimen8\textfont3%
+                 \box\@@cBox}%
+  \if@@shortDivider
+    \ifdim\wd\@@pBox >\wd\@@cBox%
+      \dimen1=\wd\@@pBox%
+    \else%
+      \dimen1=\wd\@@cBox%
+    \fi%
+    \dimen0=\wd\@@cBox%
+    \hbox to \dimen1{%
+      \hss
+      $\frac{\hbox to \dimen0{\hss\box\@@pBox\hss}}%
+        {\box\@@cBox}$%
+      \hss
+    }%
+  \else
+    $\frac{\box\@@pBox}%
+          {\box\@@cBox}$%
+  \fi
+  \@ifnextchar[%
+     {\@inferenceBackName}%{}%
+     {\egroup}
+}
+\def\@inferenceBackName[#1]{%
+  \setbox3=\hbox{\footnotesize #1}%
+  \ifdim \wd3 > \z@
+    \hskip\@@nSpace
+    \unhbox3%
+  \fi
+  \egroup
+}
+\newcommand{\@premises}[1]{%
+  \setbox\@@pBox=\vbox{}%
+  \dimen\@@maxwidth=\wd\@@cBox%
+  \@processPremises #1\\\end%
+  \@adjustPremises%
+}
+\newcommand{\@adjustPremises}{%
+  \setbox\@@pBox=\vbox{%
+    \@@moreLinestrue %
+    \loop %
+      \setbox\@@pBox=\vbox{%
+        \unvbox\@@pBox %
+        \global\setbox\@@aLineBox=\lastbox %
+      }%
+      \ifvoid\@@aLineBox %
+        \@@moreLinesfalse %
+      \else %
+        \hbox to \dimen\@@maxwidth{\unhbox\@@aLineBox}%
+      \fi %
+    \if@@moreLines\repeat%
+  }%
+}
+\def\@processPremises#1\\#2\end{%
+  \setbox\@@pLineBox=\hbox{}%
+  \@processPremiseLine #1&\end%
+  \setbox\@@pLineBox=\hbox{\unhbox\@@pLineBox \unskip}%
+  \ifdim \wd\@@pLineBox > \z@ %
+    \setbox\@@pLineBox=%
+      \hbox{\hskip\@@pEnd \unhbox\@@pLineBox \hskip\@@pEnd}%
+    \ifdim \wd\@@pLineBox > \dimen\@@maxwidth %
+      \dimen\@@maxwidth=\wd\@@pLineBox %
+    \fi %
+    \setbox\@@pBox=\vbox{\box\@@pLineBox\unvbox\@@pBox}%
+  \fi %
+  \def\sem@tmp{#2}%
+  \ifx \sem@tmp\empty \else %
+    \@ReturnAfterFi{%
+      \@processPremises #2\end %
+    }%
+  \fi%
+}
+\def\@processPremiseLine#1&#2\end{%
+  \def\sem@tmp{#1}%
+  \ifx \sem@tmp\empty \else%
+    \ifx \sem@tmp\@@space \else%
+    \setbox\@@pLineBox=%
+      \hbox{\unhbox\@@pLineBox%
+            \@inferenceOrPremis #1\inference\end%
+            \hskip\@@pSpace}%
+    \fi%
+  \fi%
+  \def\sem@tmp{#2}%
+  \ifx \sem@tmp\empty \else%
+    \@ReturnAfterFi{%
+      \@processPremiseLine#2\end%
+    }%
+  \fi%
+}
+\def\@inferenceOrPremis#1\inference{%
+  \@ifnext \end
+    {\@dropnext{\predicate{\ignorespaces #1}\unskip}}%
+    {\@processInference #1\inference}%
+}
+\def\@processInference#1\inference\end{%
+  \ignorespaces #1%
+  \setbox3=\lastbox
+  \dimen3=\dp3
+  \advance\dimen3 by -\fontdimen22\textfont2
+  \advance\dimen3 by \fontdimen8\textfont3
+  \expandafter\raise\dimen3\box3%
+}
+\long\def\@ReturnAfterFi#1\fi{\fi#1}
+\fi
+\endinput
+%%
+%% End of file `infernce.sty'.
diff --git a/helm/ocaml/tactics/doc/ligature.sty b/helm/ocaml/tactics/doc/ligature.sty
new file mode 100644 (file)
index 0000000..a914d91
--- /dev/null
@@ -0,0 +1,169 @@
+%%
+%% This is file `ligature.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,ligature')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from ligature.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak
+      but by using \protect\usepackage{semantic} in your document
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+\TestForConflict{\@addligto,\@addligtofollowlist,\@def@ligstep}
+\TestForConflict{\@@trymathlig,\@defactive,\@defligstep}
+\TestForConflict{\@definemathlig,\@domathligfirsts,\@domathligfollows}
+\TestForConflict{\@exitmathlig,\@firstmathligs,\@ifactive,\@ifcharacter}
+\TestForConflict{\@ifinlist,\@lastvalidmathlig,\@mathliglink}
+\TestForConflict{\@mathligredefactive,\@mathligsoff,\@mathligson}
+\TestForConflict{\@seentoks,\@setupfirstligchar,\@try@mathlig}
+\TestForConflict{\@trymathlig,\if@mathligon,\mathlig,\mathligprotect}
+\TestForConflict{\mathligsoff,\mathligson,\@startmathlig,\@pushedtoks}
+\newif\if@mathligon
+\DeclareRobustCommand\mathlig[1]{\@addligtolists#1\@@
+  \if@mathligon\mathligson\fi
+  \@setupfirstligchar#1\@@
+  \@defligstep{}#1\@@}
+\def\@mathligson{\if@mathligon\mathligson\fi}
+\def\@mathligsoff{\if@mathligon\mathligsoff\@mathligontrue\fi}
+\DeclareRobustCommand\mathligprotect[1]{\expandafter
+  \def\expandafter#1\expandafter{%
+    \expandafter\@mathligsoff#1\@mathligson}}
+\DeclareRobustCommand\mathligson{\def\do##1##2##3{\mathcode`##1="8000}%
+  \@domathligfirsts\@mathligontrue}
+\AtBeginDocument{\mathligson}
+\DeclareRobustCommand\mathligsoff{\def\do##1##2##3{\mathcode`##1=##2}%
+  \@domathligfirsts\@mathligonfalse}
+\edef\@mathliglink{Error: \noexpand\verb|\string\@mathliglink| expanded}
+{\catcode`\A=11\catcode`\1=12\catcode`\~=13 % Letter, Other and Active
+\gdef\@ifcharacter#1{\ifcat A\noexpand#1\let\next\@firstoftwo
+                \else\ifcat 1\noexpand#1\let\next\@firstoftwo
+                \else\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+                \else\let\next\@secondoftwo\fi\fi\fi\next}%
+\gdef\@ifactive#1{\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+                  \else\let\next\@secondoftwo\fi\next}}
+\def\@domathligfollows{}\def\@domathligfirsts{}
+\def\@makemathligsactive{\mathligson
+  \def\do##1##2##3{\catcode`##1=12}\@domathligfollows}
+\def\@makemathligsnormal{\mathligsoff
+  \def\do##1##2##3{\catcode`##1=##3}\@domathligfollows}
+\def\@ifinlist#1#2{\@tempswafalse
+  \def\do##1##2##3{\ifnum`##1=`#2\relax\@tempswatrue\fi}#1%
+  \if@tempswa\let\next\@firstoftwo\else\let\next\@secondoftwo\fi\next}
+\def\@addligto#1#2{%
+  \@ifinlist#1#2{\def\do##1##2##3{\noexpand\do\noexpand##1%
+      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+      \else{##2}{##3}\fi}%
+    \edef#1{#1}}%
+  {\def\do##1##2##3{\noexpand\do\noexpand##1%
+      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+      \else{##2}{##3}\fi}%
+    \edef#1{#1\do#2{\the\mathcode`#2}{\the\catcode`#2}}}}
+\def\@addligtolists#1{\expandafter\@addligto
+  \expandafter\@domathligfirsts
+  \csname\string#1\endcsname\@addligtofollowlist}
+\def\@addligtofollowlist#1{\ifx#1\@@\let\next\relax\else
+  \def\next{\expandafter\@addligto
+    \expandafter\@domathligfollows
+    \csname\string#1\endcsname
+    \@addligtofollowlist}\fi\next}
+\def\@defligstep#1#2{\def\@tempa##1{\ifx##1\endcsname
+    \expandafter\endcsname\else
+    \string##1\expandafter\@tempa\fi}%
+  \expandafter\@def@ligstep\csname @mathlig\@tempa#1#2\endcsname{#1#2}}
+\def\@def@ligstep#1#2#3{%
+  \ifx#3\@@
+    \def\next{\def#1}%
+  \else
+    \ifx#1\relax
+      \def\next{\let#1\@mathliglink\@defligstep{#2}#3}%
+    \else
+      \def\next{\@defligstep{#2}#3}%
+    \fi
+  \fi\next}
+\def\@setupfirstligchar#1#2\@@{%
+  \@ifactive{#1}{%
+    \expandafter\expandafter\expandafter\@mathligredefactive
+    \expandafter\string\expandafter#1\expandafter{#1}{#1}}%
+  {\@defactive#1{\@startmathlig #1}\@namedef{@mathlig#1}{#1}}}
+\def\@mathligredefactive#1#2#3{%
+  \def#3{{}\ifmmode\def\next{\@startmathlig#1}\else
+    \def\next{#2}\fi\next}%
+  \@namedef{@mathlig#1}{#2}}
+\def\@defactive#1{\@ifundefined{@definemathlig\string#1}%
+  {\@latex@error{Illegal first character in math ligature}
+    {You can only use \@firstmathligs\space as the first^^J
+      character of a math ligature}}%
+  {\csname @definemathlig\string#1\endcsname}}
+
+{\def\@firstmathligs{}\def\do#1{\catcode`#1=\active
+    \expandafter\gdef\expandafter\@firstmathligs
+    \expandafter{\@firstmathligs\space\string#1}\next}
+  \def\next#1{\expandafter\gdef\csname
+    @definemathlig\string#1\endcsname{\def#1}}
+  \do{"}"\do{@}@\do{/}/\do{(}(\do{)})\do{[}[\do{]}]\do{=}=
+  \do{?}?\do{!}!\do{`}`\do{'}'\do{|}|\do{~}~\do{<}<\do{>}>
+  \do{+}+\do{-}-\do{*}*\do{.}.\do{,},\do{:}:\do{;};}
+\newtoks\@pushedtoks
+\newtoks\@seentoks
+\def\@startmathlig{\def\@lastvalidmathlig{}\@pushedtoks{}%
+  \@seentoks{}\@trymathlig}
+\def\@trymathlig{\futurelet\next\@@trymathlig}
+\def\@@trymathlig{\@ifcharacter\next{\@try@mathlig}{\@exitmathlig{}}}
+\def\@exitmathlig#1{%
+  \expandafter\@makemathligsnormal\@lastvalidmathlig\mathligson
+  \the\@pushedtoks#1}
+\def\@try@mathlig#1{%\typeout{char: #1 catcode: \the\catcode`#1
+  \@ifundefined{@mathlig\the\@seentoks#1}{\@exitmathlig{#1}}%
+  {\expandafter\ifx
+                 \csname @mathlig\the\@seentoks#1\endcsname
+                 \@mathliglink
+      \expandafter\@pushedtoks
+        \expandafter=\expandafter{\the\@pushedtoks#1}%
+    \else
+      \expandafter\let\expandafter\@lastvalidmathlig
+      \csname @mathlig\the\@seentoks#1\endcsname
+      \@pushedtoks={}%
+    \fi
+    \expandafter\@seentoks\expandafter=\expandafter%
+    {\the\@seentoks#1}\@makemathligsactive\obeyspaces\@trymathlig}}
+\edef\patch@newmcodes@{%
+  \mathcode\number`\'=39
+  \mathcode\number`\*=42
+  \mathcode\number`\.=\string "613A
+  \mathchardef\noexpand\std@minus=\the\mathcode`\-\relax
+  \mathcode\number`\-=45
+  \mathcode\number`\/=47
+  \mathcode\number`\:=\string "603A\relax
+}
+\AtBeginDocument{\let\newmcodes@=\patch@newmcodes@}
+\fi
+\endinput
+%%
+%% End of file `ligature.sty'.
diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
new file mode 100644 (file)
index 0000000..43e17eb
--- /dev/null
@@ -0,0 +1,194 @@
+\documentclass[a4paper,draft]{article}
+
+\usepackage{a4wide}
+\usepackage{pifont}
+\usepackage{semantic}
+\usepackage{stmaryrd}
+
+\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
+
+\title{Continuationals semantics for \MATITA}
+\author{Enrico Tassi \qquad Stefano Zacchiroli \\
+\small Department of Computer Science, University of Bologna \\
+\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
+\small \{\texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
+
+\newcommand{\DOT}{\mbox{\textbf{.}}}
+\newcommand{\SEMICOLON}{\mbox{\textbf{;}}}
+\newcommand{\BRANCH}{\mbox{\textbf{[}}}
+\newcommand{\SHIFT}{\mbox{\textbf{\textbar}}}
+\newcommand{\MERGE}{\mbox{\textbf{]}}}
+\newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
+\newcommand{\SKIP}{\ensuremath{\mathtt{skip}}}
+\newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}}
+\newcommand{\GOTO}[2]{\ensuremath{\mathtt{goal} ~ #1 ~ #2}}
+
+\newcommand{\GOAL}{\ensuremath{\mathit{goal}}}
+\newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}}
+\newcommand{\LIST}{\ensuremath{\mathtt{list}}}
+\newcommand{\STACK}{\ensuremath{\mathtt{stack}}}
+\newcommand{\OPEN}[1]{\ensuremath{\mathtt{Open}~#1}}
+\newcommand{\CLOSED}[1]{\ensuremath{\mathtt{Closed}~#1}}
+
+\newcommand{\SEMOP}[1]{|[#1|]}
+\newcommand{\TSEMOP}[1]{{}_t|[#1|]}
+\newcommand{\SEM}[5]{\SEMOP{#1}_{#2,#3,#4,#5}}
+\newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
+
+\newcommand{\FUN}[2]{\ensuremath{\mathit{#1}(#2)}}
+\newcommand{\FILTEROPEN}[1]{\FUN{filter\_open}{#1}}
+\newcommand{\MAPOPEN}[1]{\FUN{map\_open}{#1}}
+\newcommand{\DEEPCLOSE}[1]{\FUN{deep\_close}{#1}}
+
+\begin{document}
+\maketitle
+
+\section{Foo}
+
+\subsection{Language}
+
+\[
+\begin{array}{rcll}
+ C & ::= & & \mbox{(\textbf{continuationals})} \\
+   &     & \DOT & \mbox{(dot)} \\
+   &  |  & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\
+   &  |  & \BRANCH & \mbox{(branch)} \\
+   &  |  & \SHIFT & \mbox{(shift)} \\
+   &  |  & \MERGE & \mbox{(merge)} \\
+   &  |  & \GOTO{n}{C} & \mbox{(goto)} \\
+   &  |  & \TACTICAL{T} & \mbox{(tactical)} \\[2ex]
+
+ T & ::= & & \mbox{(\textbf{tacticals})} \\
+   &     & \APPLY{tac} & \mbox{(tactic application)} \\
+   &  |  & \SKIP & \mbox{(closed goal skipping)} \\
+\end{array}
+\]
+
+\subsection{Status}
+
+\[
+\begin{array}{rcll}
+ \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\
+ \xi & & & \mbox{(metasenv)} \\
+ \Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\
+ \GOALSWITCH & = & \OPEN{g} \quad | \quad \CLOSED{g} & \\
+ \tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\
+ \kappa & = & \GOAL~\LIST~\STACK & \mbox{(dot continuations)} \\
+\end{array}
+\]
+
+\subsection{Semantics}
+
+\[
+\begin{array}{rcll}
+ \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
+  \mbox{(continuationals semantics)} \\
+ \TSEMOP{\cdot} & : & T -> \xi -> \GOALSWITCH ->
+  \GOAL~\LIST \times \GOAL~\LIST & \mbox{(tacticals semantics)} \\
+\end{array}
+\]
+
+\[
+\begin{array}{rcl}
+ \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL ->
+  \GOAL~\LIST\times\GOAL~\LIST \\
+ \mathit{map\_open} & : & \GOAL~\LIST -> \GOALSWITCH~\LIST \\
+ \mathit{filter\_open} & : & \GOALSWITCH~\LIST -> \GOAL~\LIST \\
+ \mathit{deep\_close} & :
+ & \GOAL~\LIST -> \GOALSWITCH~\LIST~\STACK -> \GOALSWITCH~\LIST~\STACK \\
+ \cup & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
+ \setminus & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
+\end{array}
+\]
+
+\[
+\begin{array}{rlcc}
+ \TSEM{\APPLY{tac}}{\xi}{\OPEN{g}} & =
+ & \mathit{apply\_tac}(\mathit{tac},\xi,g) & \\
+ \TSEM{\SKIP}{\xi}{\CLOSED{g}} & = & \langle [], [g]\rangle & \\
+\end{array}
+\]
+
+\[
+\begin{array}{rcl}
+ \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
+ & =
+ & \langle\xi_n,\MAPOPEN{G^O_n}::\DEEPCLOSE{G^C_n,\Gamma},\tau,\kappa\rangle
+ \\[1ex]
+
+ \multicolumn{3}{l}{\hspace{2em}
+ \left\{
+ \begin{array}{rcll}
+  \langle\xi_0, G^O_0, G^C_0\rangle & = & \langle\xi, [], []\rangle \\
+  \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
+  & =
+  & \langle\xi_i, G^O_i, G^C_i\rangle
+  & g_i\in G^C_i \\
+  \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
+  & =
+  & \langle\xi, (G^O_i\setminus G^C)\cup G^O, G^C_i\cup G^C\rangle
+  & g_i\not\in G^C_i \\
+  & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
+  \\
+ \end{array}
+ \right.
+ }
+ \\[2ex]
+
+ \SEM{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa}
+ & =
+ & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'}
+ \\[1ex]
+
+ & & \mathit{where} ~
+ \langle\xi',\Gamma',\tau',\kappa',\rangle =
+ \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa}
+ \\[2ex]
+
+ \SEM{~\DOT~}{\xi}{(g::G)::\Gamma}{\tau}{K::\kappa}
+ & =
+ & \langle\xi, [g]::\Gamma, \tau,
+   (\FILTEROPEN{G}\cup K)::\kappa\rangle
+ \\[2ex]
+
+ \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(g::G)::\kappa}
+ & =
+ & \langle\xi, [g]::\Gamma, \tau, G::\kappa\rangle
+ \\[2ex]
+
+ \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
+ & =
+ & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle
+ \\[2ex]
+
+ \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
+ & =
+ & \langle\xi,
+   [g_i]::[g_{i+1};\dots;g_n]::\Gamma,
+   (T\cup\FILTEROPEN{G}\cup K)::\tau,
+   []::\kappa\rangle
+ \\[2ex]
+
+ \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
+ & =
+ & \langle\xi,
+   (T\cup G\cup[g_i;\dots;g_n]\cup\MAPOPEN{K})::\Gamma,
+   \tau,
+   \kappa\rangle
+ \\[2ex]
+
+ \SEM{\GOTO{g}{C}}{\xi}{\Gamma}{\tau}{\kappa}
+ & = 
+ & \langle\xi',\Gamma',\tau\setminus[g],\kappa\setminus[g]\rangle
+ \\[1ex]
+
+ & & \mathit{where} ~
+ \langle \xi', []::\Gamma', []::\tau, []::\kappa\rangle
+ = \SEM{C}{\xi}{[g]::\Gamma}{[]::\tau}{[]::\kappa}
+ \\[2ex]
+
+\end{array}
+\]
+
+\end{document}
+
diff --git a/helm/ocaml/tactics/doc/reserved.sty b/helm/ocaml/tactics/doc/reserved.sty
new file mode 100644 (file)
index 0000000..c0d56b8
--- /dev/null
@@ -0,0 +1,80 @@
+%%
+%% This is file `reserved.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,reservedWords')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from reserved.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak
+      but by using \protect\usepackage{semantic} in your document
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+\TestForConflict{\reservestyle,\@reservestyle,\setreserved,\<}
+\TestForConflict{\@parseDefineReserved,\@xparseDefineReserved}
+\TestForConflict{\@defineReserved,\@xdefineReserved}
+\newcommand{\reservestyle}[3][]{
+  \newcommand{#2}{\@parseDefineReserved{#1}{#3}}
+   \expandafter\expandafter\expandafter\def
+     \expandafter\csname set\expandafter\@gobble\string#2\endcsname##1%
+   {#1{#3{##1}}}}
+\newtoks\@@spacing
+\newtoks\@@formating
+\def\@parseDefineReserved#1#2{%
+  \@ifnextchar[{\@xparseDefineReserved{#2}}%
+     {\@xparseDefineReserved{#2}[#1]}}
+\def\@xparseDefineReserved#1[#2]#3{%
+  \@@formating{#1}%
+  \@@spacing{#2}%
+  \expandafter\@defineReserved#3,\end
+}
+\def\@defineReserved#1,{%
+  \@ifnextchar\end
+  {\@xdefineReserved #1[]\END\@gobble}%
+  {\@xdefineReserved#1[]\END\@defineReserved}}
+\def\@xdefineReserved#1[#2]#3\END{%
+  \def\reserved@a{#2}%
+  \ifx \reserved@a\empty \toks0{#1}\else \toks0{#2} \fi
+    \expandafter\edef\csname\expandafter<#1>\endcsname
+    {\the\@@formating{\the\@@spacing{\the\toks0}}}}
+\def\setreserved#1>{%
+  \expandafter\let\expandafter\reserved@a\csname<#1>\endcsname
+  \@ifundefined{reserved@a}{\PackageError{Semantic}
+      {``#1'' is not defined as a reserved word}%
+      {Before referring to a name as a reserved word, it %
+      should be defined\MessageBreak using an appropriate style
+      definer.  A style definer is defined \MessageBreak
+      using \protect\reservestyle.\MessageBreak%
+      Type <return> to proceed --- nothing will be set.}}%
+  {\reserved@a}}
+\let\<=\setreserved
+\fi
+\endinput
+%%
+%% End of file `reserved.sty'.
diff --git a/helm/ocaml/tactics/doc/semantic.sty b/helm/ocaml/tactics/doc/semantic.sty
new file mode 100644 (file)
index 0000000..98257ca
--- /dev/null
@@ -0,0 +1,137 @@
+%%
+%% This is file `semantic.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `general')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from semantic.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\NeedsTeXFormat{LaTeX2e}
+\newcommand{\semanticVersion}{2.0(epsilon)}
+\newcommand{\semanticDate}{2003/10/28}
+\ProvidesPackage{semantic}
+  [\semanticDate\space v\semanticVersion\space]
+\typeout{Semantic Package v\semanticVersion\space [\semanticDate]}
+\typeout{CVSId: $Id$}
+\newcounter{@@conflict}
+\newcommand{\@semanticNotDefinable}{%
+  \typeout{Command \@backslashchar\reserved@a\space already defined}
+  \stepcounter{@@conflict}}
+\newcommand{\@oldNotDefinable}{}
+\let\@oldNotDefinable=\@notdefinable
+\let\@notdefinable=\@semanticNotDefinable
+\newcommand{\TestForConflict}{}
+\def\TestForConflict#1{\sem@test #1,,}
+\newcommand{\sem@test}{}
+\newcommand{\sem@tmp}{}
+\newcommand{\@@next}{}
+\def\sem@test#1,{%
+  \def\sem@tmp{#1}%
+  \ifx \sem@tmp\empty \let\@@next=\relax \else
+    \@ifdefinable{#1}{} \let\@@next=\sem@test \fi
+  \@@next}
+\TestForConflict{\@inputLigature,\@inputInference,\@inputTdiagram}
+\TestForConflict{\@inputReservedWords,\@inputShorthand}
+\TestForConflict{\@ddInput,\sem@nticsLoader,\lo@d}
+\def\@inputLigature{\input{ligature.sty}\message{ math mode ligatures,}%
+                     \let\@inputLigature\relax}
+\def\@inputInference{\input{infernce.sty}\message{ inference rules,}%
+                     \let\@inputInference\relax}
+\def\@inputTdiagram{\input{tdiagram.sty}\message{ T diagrams,}%
+                     \let\@inputTdiagram\relax}
+\def\@inputReservedWords{\input{reserved.sty}\message{ reserved words,}%
+                     \let\@inputReservedWords\relax}
+\def\@inputShorthand{\input{shrthand.sty}\message{ short hands,}%
+                     \let\@inputShorthand\relax}
+\toks1={}
+\newcommand{\@ddInput}[1]{%
+  \toks1=\expandafter{\the\toks1\noexpand#1}}
+\DeclareOption{ligature}{\@ddInput\@inputLigature}
+\DeclareOption{inference}{\@ddInput\@inputInference}
+\DeclareOption{tdiagram}{\@ddInput\@inputTdiagram}
+\DeclareOption{reserved}{\@ddInput\@inputReservedWords}
+\DeclareOption{shorthand}{\@ddInput\@inputLigature
+   \@ddInput\@inputShorthand}
+\ProcessOptions*
+\typeout{Loading features: }
+\def\sem@nticsLoader{}
+\edef\lo@d{\the\toks1}
+\ifx\lo@d\empty
+  \@inputLigature
+  \@inputInference
+  \@inputTdiagram
+  \@inputReservedWords
+  \@inputShorthand
+\else
+  \lo@d
+\fi
+\typeout{and general definitions.^^J}
+\let\@ddInput\relax
+\let\@inputInference\relax
+\let\@inputLigature\relax
+\let\@inputTdiagram\relax
+\let\@inputReservedWords\relax
+\let\@inputShorthand\relax
+\let\sem@nticsLoader\realx
+\let\lo@d\relax
+\TestForConflict{\@dropnext,\@ifnext,\@ifn,\@ifNextMacro,\@ifnMacro}
+\TestForConflict{\@@maxwidth,\@@pLineBox,\if@@Nested,\@@cBox}
+\TestForConflict{\if@@moreLines,\@@pBox}
+\def\@ifnext#1#2#3{%
+  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet%
+  \reserved@c\@ifn}
+\def\@ifn{%
+      \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else%
+          \let\reserved@d\reserved@b\fi \reserved@d}
+\def\@ifNextMacro#1#2{%
+  \def\reserved@a{#1}\def\reserved@b{#2}%
+    \futurelet\reserved@c\@ifnMacro}
+\def\@ifnMacro{%
+  \ifcat\noexpand\reserved@c\noexpand\@ifnMacro
+    \let\reserved@d\reserved@a
+  \else \let\reserved@d\reserved@b\fi \reserved@d}
+\newcommand{\@dropnext}[2]{#1}
+\ifnum \value{@@conflict} > 0
+   \PackageError{Semantic}
+     {The \the@@conflict\space command(s) listed above have been
+      redefined.\MessageBreak
+      Please report this to turtle@bu.edu}
+     {Some of the commands defined in semantic was already defined %
+      and has\MessageBreak now be redefined. There is a risk that %
+      these commands will be used\MessageBreak by other packages %
+      leading to spurious errors.\MessageBreak
+      \space\space Type <return> and cross your fingers%
+}\fi
+\let\@notdefinable=\@oldNotDefinable
+\let\@semanticNotDefinable=\relax
+\let\@oldNotDefinable=\relax
+\let\TestForConflict=\relax
+\let\@endmark=\relax
+\let\sem@test=\relax
+\newdimen\@@maxwidth
+\newbox\@@pLineBox
+\newbox\@@cBox
+\newbox\@@pBox
+\newif\if@@moreLines
+\newif\if@@Nested \@@Nestedfalse
+\endinput
+%%
+%% End of file `semantic.sty'.
diff --git a/helm/ocaml/tactics/doc/shrthand.sty b/helm/ocaml/tactics/doc/shrthand.sty
new file mode 100644 (file)
index 0000000..b73af44
--- /dev/null
@@ -0,0 +1,96 @@
+%%
+%% This is file `shrthand.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,shorthand')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from shrthand.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak
+      but by using \protect\usepackage{semantic} in your document
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+\IfFileExists{DONOTUSEmathbbol.sty}{%
+  \RequirePackage{mathbbol}
+  \newcommand{\@bblb}{\textbb{[}}
+  \newcommand{\@bbrb}{\textbb{]}}
+  \newcommand{\@mbblb}{\mathopen{\mbox{\textbb{[}}}}
+  \newcommand{\@mbbrb}{\mathclose{\mbox{\textbb{]}}}}
+}
+{ \newcommand{\@bblb}{\textnormal{[\kern-.15em[}}
+  \newcommand{\@bbrb}{\textnormal{]\kern-.15em]}}
+  \newcommand{\@mbblb}{\mathopen{[\mkern-2.67mu[}}
+  \newcommand{\@mbbrb}{\mathclose{]\mkern-2.67mu]}}
+}
+\mathlig{|-}{\vdash}
+\mathlig{|=}{\models}
+\mathlig{->}{\rightarrow}
+\mathlig{->*}{\mathrel{\rightarrow^*}}
+\mathlig{->+}{\mathrel{\rightarrow^+}}
+\mathlig{-->}{\longrightarrow}
+\mathlig{-->*}{\mathrel{\longrightarrow^*}}
+\mathlig{-->+}{\mathrel{\longrightarrow^+}}
+\mathlig{=>}{\Rightarrow}
+\mathlig{=>*}{\mathrel{\Rightarrow^*}}
+\mathlig{=>+}{\mathrel{\Rightarrow^+}}
+\mathlig{==>}{\Longrightarrow}
+\mathlig{==>*}{\mathrel{\Longrightarrow^*}}
+\mathlig{==>+}{\mathrel{\Longrightarrow^+}}
+\mathlig{<-}{\leftarrow}
+\mathlig{*<-}{\mathrel{{}^*\mkern-1mu\mathord\leftarrow}}
+\mathlig{+<-}{\mathrel{{}^+\mkern-1mu\mathord\leftarrow}}
+\mathlig{<--}{\longleftarrow}
+\mathlig{*<--}{\mathrel{{}^*\mkern-1mu\mathord{\longleftarrow}}}
+\mathlig{+<--}{\mathrel{{}^+\mkern-1mu\mathord{\longleftarrow}}}
+\mathlig{<=}{\Leftarrow}
+\mathlig{*<=}{\mathrel{{}^*\mkern-1mu\mathord\Leftarrow}}
+\mathlig{+<=}{\mathrel{{}^+\mkern-1mu\mathord\Leftarrow}}
+\mathlig{<==}{\Longleftarrow}
+\mathlig{*<==}{\mathrel{{}^*\mkern-1mu\mathord{\Longleftarrow}}}
+\mathlig{+<==}{\mathrel{{}^+\mkern-1mu\mathord{\Longleftarrow}}}
+\mathlig{<->}{\longleftrightarrow}
+\mathlig{<=>}{\Longleftrightarrow}
+\mathlig{|[}{\@mbblb}
+\mathlig{|]}{\@mbbrb}
+\newcommand{\evalsymbol}[1][]{\ensuremath{\mathcal{E}^{#1}}}
+\newcommand{\compsymbol}[1][]{\ensuremath{\mathcal{C}^{#1}}}
+\newcommand{\eval}[3][]%
+  {\mbox{$\mathcal{E}^{#1}$\@bblb \texttt{#2}\@bbrb}%
+   \ensuremath{\mathtt{#3}}}
+\newcommand{\comp}[3][]%
+  {\mbox{$\mathcal{C}^{#1}$\@bblb \texttt{#2}\@bbrb}%
+   \ensuremath{\mathtt{#3}}}
+\newcommand{\@exe}[3]{}
+\newcommand{\exe}[1]{\@ifnextchar[{\@exe{#1}}{\@exe{#1}[]}}
+\def\@exe#1[#2]#3{%
+  \mbox{\@bblb\texttt{#1}\@bbrb$^\mathtt{#2}\mathtt{(#3)}$}}
+\fi
+\endinput
+%%
+%% End of file `shrthand.sty'.
diff --git a/helm/ocaml/tactics/doc/tdiagram.sty b/helm/ocaml/tactics/doc/tdiagram.sty
new file mode 100644 (file)
index 0000000..02202b3
--- /dev/null
@@ -0,0 +1,166 @@
+%%
+%% This is file `tdiagram.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,Tdiagram')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from tdiagram.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak
+      but by using \protect\usepackage{semantic} in your document
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+\TestForConflict{\@getSymbol,\@interpreter,\@parseArg,\@program}
+\TestForConflict{\@putSymbol,\@saveBeforeSymbolMacro,\compiler}
+\TestForConflict{\interpreter,\machine,\program,\@compiler}
+\newif\if@@Left
+\newif\if@@Up
+\newcount\@@xShift
+\newcount\@@yShift
+\newtoks\@@symbol
+\newtoks\@@tempSymbol
+\newcommand{\compiler}[1]{\@compiler#1\end}
+\def\@compiler#1,#2,#3\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=40 \if@@Left \@@xShift=-50 \else \@@xShift=-30 \fi
+    \else%
+      \@@yShift=20 \@@xShift =0 %
+    \fi%
+  \else%
+    \@@yShift=40 \@@xShift=-40%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(1,0){80}}%
+    \put(0,-20){\line(1,0){30}}%
+    \put(50,-20){\line(1,0){30}}%
+    \put(30,-40){\line(1,0){20}}%
+    \put(0,0){\line(0,-1){20}}%
+    \put(80,0){\line(0,-1){20}}%
+    \put(30,-20){\line(0,-1){20}}%
+    \put(50,-20){\line(0,-1){20}}%
+    \put(30,-20){\makebox(20,20){$\rightarrow$}} %
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,-20)(5,-20)#1\end}%
+   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+   {\@@Uptrue \@@Leftfalse \@parseArg(80,-20)(55,-20)#3\end}%
+   {\@@Upfalse \@@Lefttrue \@parseArg(50,-40)(30,-40)#2\end}%
+   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
+  }%
+}
+\newcommand{\interpreter}[1]{\@interpreter#1\end}
+\def\@interpreter#1,#2\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=40 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
+    \else%
+      \@@yShift=0 \@@xShift =0 %
+    \fi%
+  \else%
+    \@@yShift=40 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}}%
+    \put(0,-40){\line(-1,0){20}}%
+    \put(0,0){\line(0,-1){40}}%
+    \put(-20,0){\line(0,-1){40}}%
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-20)#1\end}%
+   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+   {\@@Upfalse \@@Lefttrue \@parseArg(0,-40)(-20,-40)#2\end}%
+   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
+  }%
+}
+\newcommand{\program}[1]{\@program#1\end}
+\def\@program#1,#2\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=0 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
+    \else%
+      \PackageError{semantic}{%
+        A program cannot be at the bottom}
+        {%
+          You have tried to use a \protect\program\space as the
+          bottom\MessageBreak parameter to \protect\compiler,
+          \protect\interpreter\space or \protect\program.\MessageBreak
+         Type <return> to proceed --- Output can be distorted.}%
+    \fi%
+  \else%
+    \@@yShift=0 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}}%
+    \put(0,0){\line(0,1){30}}%
+    \put(-20,0){\line(0,1){30}}%
+    \put(-10,30){\oval(20,20)[t]}%
+    \@putSymbol[#1]{-20,20}%
+   {\@@Upfalse \@@Lefttrue \@parseArg(0,0)(-20,0)#2\end}%
+  }%
+}
+\newcommand{\machine}[1]{%
+  \if@@Nested %
+    \if@@Up %
+      \PackageError{semantic}{%
+        A machine cannot be at the top}
+        {%
+          You have tried to use a \protect\machine\space as a
+          top\MessageBreak parameter to \protect\compiler or
+          \protect\interpreter.\MessageBreak
+         Type <return> to proceed --- Output can be distorted.}%
+       \else \@@yShift=0 \@@xShift=0
+    \fi%
+  \else%
+    \@@yShift=20 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}} \put(-20,0){\line(3,-5){10}}
+    \put(0,0){\line(-3,-5){10}}%
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-15)#1\end}%
+  }%
+}
+\def\@parseArg(#1)(#2){%
+  \@ifNextMacro{\@doSymbolMacro(#1)(#2)}{\@getSymbol(#2)}}
+\def\@getSymbol(#1)#2\end{\@putSymbol[#2]{#1}}
+\def\@doSymbolMacro(#1)(#2)#3{%
+  \@ifnextchar[{\@saveBeforeSymbolMacro(#1)(#2)#3}%
+               {\@symbolMacro(#1)(#2)#3}}
+\def\@saveBeforeSymbolMacro(#1)(#2)#3[#4]#5\end{%
+  \@@tempSymbol={#4}%
+  \@@Nestedtrue\put(#1){#3#5}%
+  \@putSymbol[\the\@@tempSymbol]{#2}}
+\def\@symbolMacro(#1)(#2)#3\end{%
+  \@@Nestedtrue\put(#1){#3}%
+  \@putSymbol{#2}}
+\newcommand{\@putSymbol}[2][\the\@@symbol]{%
+  \global\@@symbol=\expandafter{#1}%
+  \put(#2){\makebox(20,20){\texttt{\the\@@symbol}}}}
+\fi
+\endinput
+%%
+%% End of file `tdiagram.sty'.