hetcasl.sty revision 374a17994c7c43df4fe2fc6e266bee5601b8dd5f
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\ProvidesPackage{hetcasl}[2002/10/04 v0.1 LaTeX Package for CASL v1.0.1]
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher%% $Header$
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\NeedsTeXFormat{LaTeX2e}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% Required packages
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\RequirePackage{ifthen}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\RequirePackage{tabularx}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\RequirePackage{calc}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\RequirePackage[latin1]{inputenc}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\RequirePackage{xspace}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\RequirePackage{latexsym}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newcounter{@opentabulars}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\setcounter{@opentabulars}{0}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newlength{\@oldparindent}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newlength{\@hetcaslmaxwidth}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newlength{\@remhetcaslwidth}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newlength{\@KWwidth}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% The next two length variables will be used in \KW
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newlength{\@realWidth}\newlength{\@neededWidth}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newlength{\@EqSpace}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newlength{\@ABSpace}
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl\newlength{\@LeftABSpace}
5cd4414fce1e0eb4133dfc6fc828bf25c8a959f9Lukas Slebodnik\newlength{\@RightABSpace}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newif\ifhetcasl \hetcaslfalse
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newenvironment{hetcasl}[1][\textwidth]%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher{%begin stuff
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria\ifhetcasl%
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria\PackageError{hetcasl evironments cannot nested}%
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria\else\hetcasltrue\fi%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\begingroup%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\setlength{\@oldparindent}{\the\parindent}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\setlength{\parindent}{0cm}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\setlength{\@hetcaslmaxwidth}{#1}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\setlength{\@remhetcaslwidth}{\the\@hetcaslmaxwidth}%
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov%\begin{alltt}\begingroup\rmfamily
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov\begin{tabbing}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% a little line to set up three useful tabstops for rendering parts
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% of a library and or specification
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\KW{view} \=\KW{preds} \=~~~~~~~\=\kill
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria}%
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria{%end stuff
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria\end{tabbing}%
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria%\endgroup\end{alltt}
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria%\@CloseAllTabulars%
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria\setlength{\parindent}{\the\@oldparindent}%
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov\endgroup%
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria\hetcaslfalse%
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria}
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria
1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria\newcommand{\@HetCASLPrelude}{% HetCASL-Prelude
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\settowidth{\@KWwidth}{\textbf{view}}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher%%%% define all the makros needed for typesetting hetCASL
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% \KW prints a KeyWord within a box that is at least \@KWwidth wide.
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov% If the keyword needs more space the box is as wide as the kyeword
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% is. The optional argument overrides \@KWwidth with the width of the
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% mandatory argument in bold face. The mandatory argument is always
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% printed in bold face.
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newcommand{\KW}[2][no--format--keyword]%
7e394400eefd0e7c5ba0c64ab3fa28bee21ef2d7Sumit Bose{\ifthenelse{\equal{##1}{no--format--keyword}}%
7e394400eefd0e7c5ba0c64ab3fa28bee21ef2d7Sumit Bose{% no optional argument
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\settowidth{\@neededWidth}{\textbf{##2}}}%
7e394400eefd0e7c5ba0c64ab3fa28bee21ef2d7Sumit Bose{% optional argument given
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\settowidth{\@realWidth}{\textbf{##2}}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\settowidth{\@KWwidth}{\textbf{##1}}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\ifthenelse{\@KWwidth > \@realWidth}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher{\setlength{\@neededWidth}{\@KWwidth}}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher{\setlength{\@neededWidth}{\@realWidth}}}%
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov\makebox[% set the width of the box not smaller
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% than the width of the KeyWord
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\@neededWidth]%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher[l]{\textbf{##2}}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% print the first argument as is and use the second argument as label
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov\newcommand{\HetsLabel}[2]{##1}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% print label for ids
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newcommand{\IdDeclLabel}[2]{##1} %% {##1\label{##2}}
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newcommand{\IdApplLabel}[2]{##1} %% {##1\ref{##2}}
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek% \SId prints its argument in small caps as a Structured Id for names
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek% of specifications, views and libraries
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek\newcommand{\SId}[1]{\textsc{##1}}%
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek% \SIdIndex prints its argument like \SId but sets an Index Entry if
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek% redifined
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek\newcommand{\SIdIndex}[1]{\SId{##1}}%
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% \Id prints its argument in italic face as one word, for all other
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher% identifiers not covered by \SId and only containing letters, numbers
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl% and \_
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl\newcommand{\Id}[1]{\textit{##1}}%
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl% \AX prints its argument in math modus
b34ffbf33729c557c3d1aebf4707ad0ffe4f1904Petr Čech\newcommand{\Ax}[1]{\ensuremath{##1}}%
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl% \AltBar prints a | with the space of an = sign
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl\settowidth{\@EqSpace}{\Ax{=}}
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl\settowidth{\@ABSpace}{\Ax{|}}
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl\setlength{\@LeftABSpace}{(\@EqSpace - \@ABSpace) *1/2}
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl\setlength{\@RightABSpace}{\@EqSpace - \@ABSpace - \@LeftABSpace}
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl\newcommand{\AltBar}{\hspace*{\@LeftABSpace}\Ax{|}\hspace*{\@RightABSpace}}
aa8a8318aaa3270e9d9957d0c22dec6342360a37Pavel Reichl
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek\newcommand{\ANNOTEWORD}[1]{{\small{}\KW{\%##1}}}
77b13371c87702aee3f858f6b2b73826cf5a01bdJakub Hrozek
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher%%%%% Heng todo:
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher%% Makros aus casl.sty definieren
3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher\newcommand{\LBRACE} {\{}
\newcommand{\RBRACE} {\}}
\newcommand{\FREE} {\KW{free}\xspace} %plain_keyword
\newcommand{\FREELBRACE} {\FREE~\LBRACE}
\newcommand{\GENERATED} {\KW{generated}\xspace}
% \newcommand{\TYPE} {\KW{type}}
% \newcommand{\TYPES} {\KW{types}}
\newcommand{\FREETYPE} {\FREE~\TYPE\xspace}
\newcommand{\FREETYPES} {\FREE~\TYPES\xspace}
\newcommand{\GENERATEDTYPE} {\GENERATED~\TYPE\xspace} %{\KW{generated~type}}
\newcommand{\GENERATEDTYPES} {\GENERATED~\TYPES\xspace}
\newcommand{\VAR} {\KW[preds]{var}\xspace}
\newcommand{\VARS} {\KW[preds]{vars}\xspace}
\newcommand{\AXIOM} {\KW{axiom}\xspace}
\newcommand{\AXIOMS} {\KW{axioms}\xspace}
\newcommand{\HIDE} {\KW{hide}\xspace}
\newcommand{\REVEAL} {\KW{reveal}\xspace}
\newcommand{\WITH} {\KW{with}\xspace}
\newcommand{\THEN} {\KW[view]{then}\xspace} % hetcasl_keyword
\newcommand{\THENCONS} {\THEN~\ANNOTEWORD{cons}\xspace}
\newcommand{\THENDEF} {\THEN~\ANNOTEWORD{def}\xspace}
\newcommand{\THENIMPLIES} {\THEN~\ANNOTEWORD{implies}\xspace}
\newcommand{\THENMONO} {\THEN~\ANNOTEWORD{mono}\xspace}
\newcommand{\AND} {\KW[view]{and}\xspace}
\newcommand{\LOCAL} {\KW{local}\xspace}
\newcommand{\THENLOCAL} {\THEN~\LOCAL}
\newcommand{\WITHIN} {\KW{within}\xspace}
\newcommand{\CLOSED} {\KW{closed}\xspace}
\newcommand{\FIT} {\KW{fit}\xspace}
\newcommand{\TO} {\KW{to}\xspace}
\newcommand{\LOGIC} {\KW{logic}\xspace}
\newcommand{\SPEC} {\KW[view]{spec}\xspace}
\newcommand{\VIEW} {\KW[view]{view}\xspace}
\newcommand{\END} {\KW{end}\xspace}
\newcommand{\ARCH} {\KW{arch}\xspace}
\newcommand{\ARCHSPEC} {\ARCH~\KW{spec}\xspace}
\newcommand{\UNITSPEC} {\KW{unit}~\KW{spec}\xspace}
\newcommand{\UNITS} {\KW{units}\xspace}
\newcommand{\GIVEN} {\KW{given}\xspace}
\newcommand{\RESULT} {\KW{result}\xspace}
\newcommand{\LIBRARY} {\KW{library}\xspace}
\newcommand{\FROM} {\KW[view]{from}\xspace}
\newcommand{\GET} {\KW{get}\xspace}
\newcommand{\VERSION} {\KW{version}\xspace}
\newcommand{\PROD} {\Ax{\times}}
\newcommand{\TOTAL} {\Ax{\rightarrow}}
\newcommand{\PARTIAL} {\Ax{\rightarrow}}
\newcommand{\MAPSTO} {\Ax{\mapsto}}
\newcommand{\ASSOC} {\Id{assoc}}
\newcommand{\COMM} {\Id{comm}}
\newcommand{\IDEM} {\Id{idem}}
\newcommand{\UNIT} {\Id{unit}\xspace}
\newcommand{\EXISTS} {\Ax{\exists}}
\newcommand{\EXISTSUNIQUE} {\AX{\exists!}}
\newcommand{\IMPLIES} {\Ax{\Rightarrow}}
\newcommand{\IFF} {\Ax{\Leftrightarrow}}
\newcommand{\EEQ} {\Ax{\stackrel{e}{=}}}
\newcommand{\A} {\Ax{\wedge}}
\newcommand{\V} {\Ax{\vee}}
\newcommand{\IN} {\Ax{\in}}
\newcommand{\NOT} {\Ax{\neg}}
\newcommand{\FORALL} {\Ax{\forall}}
\newcommand{\BULLET} {\Ax{\;\bullet\;}}
\newcommand{\IF} {\Id{if}\xspace}
\newcommand{\WHEN} {\Id{when}\xspace}
\newcommand{\ELSE} {\Id{else}\xspace}
\newcommand{\DEF} {\Id{def}\xspace}
\newcommand{\AS} {\Id{as}\xspace}
\newcommand{\TRUE} {\Id{true}\xspace}
\newcommand{\FALSE} {\Id{false}\xspace}
%%%% SORT, OP, PRED : drei Varianten %% Type auch
\newcommand{\KWC}[2][preds]{%
\ifthenelse{\equal{##1}{KW}}%
{%KW as parameter
\KW{##2}}%
{% else to KW as parameter
\ifthenelse{\equal{##1}{ID}}%
{%ID as parameter
\Id{##2}}
{% else to ID as parameter
\KW[preds]{##2}}}%
}%% end of KWC definition
\newcommand{\SORT}[1][preds]{\KWC[##1]{sort}\xspace}
\newcommand{\SORTS}[1][preds]{\KWC[##1]{sorts}\xspace}
\newcommand{\OP}[1][preds]{\KWC[##1]{op}\xspace}
\newcommand{\OPS}[1][preds]{\KWC[##1]{ops}\xspace}
\newcommand{\PRED}[1][preds]{\KWC[##1]{pred}\xspace}
\newcommand{\PREDS}[1][preds]{\KWC[##1]{preds}\xspace}
\newcommand{\TYPE}[1][preds]{\KWC[##1]{type}\xspace}
\newcommand{\TYPES}[1][preds]{\KWC[##1]{types}\xspace}
%% 1. mit \KWC[preds]{} default
%% 2. mit \KWC[KW]{}
%% 3. mit \KWC[ID]{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% starting a library
\newcommand{\library}[1]{\KW{library}\ \SId{##1}\ }
% printing a version number
%\newcommand{\version}[1]{\KW{version}\ ##1}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% comments, annotations and labels
\newcommand{\commentline}[1]{\textbf{\%\%}{\small##1}}
%
\newenvironment{commentgroup}%
{\textbf{\%\{}\begingroup\small}%
{\endgroup\textbf{\}\%}}%
%
\newcommand{\annoteline}[2]{\textbf{\%##1}\ {\small \(##2\)}}%
%
\newenvironment{annotegroup}[1]%
{\textbf{\%##1(}\begingroup\small}%
{\endgroup\textbf{)\%}}%
%
\newcommand{\casllabel}[1]{\textbf{\%(}{\small##1}\textbf{)\%}}%
%
\newenvironment{mlabel}%
{\textbf{\%(}\begingroup\small}%
{\endgroup\textbf{)\%}}%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\place}{\_\_}%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% download items (from, get are automatically printed)
\newenvironment{downloaditem}[1]%
{\begingroup\sc
\textnormal{\textbf{from}}\ ##1\ %
%\textnormal{\ifthenelse{\equal{##1}{no-version}}{}{\version{##1}\ }}%
\textnormal{\textbf{get}}}%
{\endgroup}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% specifications
% specdefn starts a new spec defn
% arguments: ##1 ::= opt. semantic-anno
% ##2 ::= spec name
% ##3 ::= parameters (see parameterspecs-env)
% ##4 ::= imports (see importspecs-env)
\newenvironment{specdefn}[4][no-semantic-anno]%
{\textbf{spec}\ \textsc{##2}%
\ifthenelse{\equal{##3}{}}{}{##3}%
\ \(=\)%
}%
{}
% end of \@HetCASLPrelude
}
\@HetCASLPrelude%
%% helpers
% calculate a new width based on \@remhetcaslwidth and the fixed width
% given as argument.
\newcommand{\@calc@width}[1]{}
%\newcommand{\@tabnewline}{\\&}
\newcommand{\@condEOL}{\ifthenelse{\the@opentabulars=0}{\\}{\@tabnewline}}
\newcommand{\@CloseAllTabulars}{}