casl.sty revision 5500bb83555b7ac44f55f5da2f345879c81e2636
% CASL package for LaTeX formatting of CASL specifications
\typeout{Package: 'casl' v1.3 - for CASL v1.0}
% Last updated: 30 Nov 1998 by Peter D. Mosses, mosses@csl.sri.com
% Version 1.3:
% - documentation CoFI Note C-2 updated to v0.3
% - \math, \text provided; \Math, \Text removed
% Version 1.2:
% - \mbox{...} inserted in \margin
% - Usage of \[...\] changed, {Lines} removed
% - \footlinkindex removed
% Version 1.1:
% - Removed implicit \[...\] around #2 in some abstract commands
% - Adjusted italics
% Version 1.0:
% - Major revision, see CoFI Note C-2
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{casl}
% DEFAULT INDENTATION IN LISTS OF ITEMS
\newcommand{\Margin}{~~~~}
% PAGE-BREAKING IN SPECS
\newif\ifsamepage
\samepagefalse
% THE FOLLOWING COMMANDS MIGHT BE ALREADY DEFINED BY OTHER PACKAGES:
\providecommand{\text}[1] {\)#1\(}
\providecommand{\math}[1] {\(#1\)}
\providecommand{\M} {\Margin}
\providecommand{\tfun} {\rightarrow}
\providecommand{\pfun} {\mathrel{\rightarrow?}}
\providecommand{\imp} {\Rightarrow}
\providecommand{\eeq} {\stackrel{e}{=}}
\providecommand{\land} {\mathrel{\wedge}}
\providecommand{\lor} {\mathrel{\vee}}
% \caslInit OVERWRITES SOME COMMANDS:
\newcommand{\caslInit}
{\everymath{\it}%
\renewcommand{\.} {\mbox{ $\scriptstyle\bullet$ }}%
\renewcommand{\*} {\times}%
\renewcommand{\|} {\mid}%
\renewcommand{\iff} {\Leftrightarrow}%
\renewcommand{\[}
{\begingroup
\ifmmode
\renewcommand{\]}{\end{array}\endgroup}%
\begin{array}[t]{@{}l@{}l@{}l@{}}%
\else
\renewcommand{\]}{\end{tabular}\endgroup}%
\begin{tabular}[t]{@{}l@{}l@{}l@{}}%
\fi}%
\renewcommand{\M} {\Margin}%
\renewcommand{\tfun} {\rightarrow}%
\renewcommand{\pfun} {\mathrel{\rightarrow?}}%
\renewcommand{\imp} {\Rightarrow}%
\renewcommand{\eeq} {\stackrel{e}{=}}%
\renewcommand{\land} {\mathrel{\wedge}}%
\renewcommand{\lor} {\mathrel{\vee}}%
\ifsamepage\samepage\fi}
% CASL ENVIRONMENTS:
\newenvironment{casl} {\caslInit}{}
\newenvironment{BasicSpec}[1][\Pred]
{\caslInit\begin{Items}[#1]}
{\end{Items}}
\newenvironment{SpecDefn}[2][\Spec]
{\medskip\caslInit\begin{Items}[\Group]\item[#1{}] \SpecName{#2}}
{\end{Items}}
\newcommand{\SpecName}[1]{\textmd{\textsc{#1}}}
% THE FOLLOWING ARE FOR USE INSIDE THE ABOVE ENVIRONMENTS :
% ITEMS:
\newenvironment{Items}[1][\Margin]
{\begin{list}{}
{\renewcommand{\makelabel}[1]{##1\hfil}
\settowidth{\labelwidth}{#1}
\setlength{\leftmargin}{\labelwidth}
\addtolength{\leftmargin}{\labelsep}
\setlength{\topsep}{0pt}
\setlength{\itemsep}{0pt}
\setlength{\parsep}{0pt}
\setlength{\parskip}{0pt}}}
{\end{list}}
\newcommand{\I}[1]{\item[#1]}
% FOR USE IN TEXT AND MATH:
\newcommand{\Sort} {\textbf{sort}}
\newcommand{\Sorts} {\textbf{sorts}}
\newcommand{\Assoc} {\textbf{assoc}}
\newcommand{\Comm} {\textbf{comm}}
\newcommand{\Idem} {\textbf{idem}}
\newcommand{\Unit} {\textbf{unit}}
\newcommand{\Bullet} {\.}
% SYMBOLS AND KEYWORDS FOR USE ONLY IN MATH:
\newcommand{\Prod} {\*}
\newcommand{\Total} {\tfun}
\newcommand{\Partial} {\pfun}
\newcommand{\MapsTo} {\mapsto}
\newcommand{\Forall} {\forall}
\newcommand{\Exists} {\exists}
\newcommand{\ExistsUnique}{\exists!}
\newcommand{\Equiv} {\iff}
\newcommand{\Implies} {\imp}
\newcommand{\Conj} {\land}
\newcommand{\Disj} {\lor}
\newcommand{\Not} {\neg}
\newcommand{\ExistlEq} {\eeq}
\newcommand{\In} {\in}
\newcommand{\IF} {\mathit{if}}
\newcommand{\WHEN} {\mathit{when}}
\newcommand{\ELSE} {\mathit{else}}
\newcommand{\DEF} {\mathit{def}}
\newcommand{\AS} {\mathit{as}}
\newcommand{\TRUE} {\mathit{true}}
\newcommand{\FALSE} {\mathit{false}}
\newcommand{\NOT} {\Not}
\newcommand{\PRED} {\mathit{pred}}
\newcommand{\OP} {\mathit{op}}
\newcommand{\VAR} {\mathit{var}}
% SYMBOLS AND KEYWORDS FOR USE IN TEXT:
\newcommand{\Comment} {\textbf{\%\%}}
\newcommand{\Group} {\textbf{\{}}
\newcommand{\EndGroup} {\textbf{\}}}
\newcommand{\Op} {\textbf{op}}
\newcommand{\Ops} {\textbf{ops}}
\newcommand{\Pred} {\textbf{pred}}
\newcommand{\Preds} {\textbf{preds}}
\newcommand{\Free} {\textbf{free}}
\newcommand{\Generated} {\textbf{generated}}
\newcommand{\Type} {\textbf{type}}
\newcommand{\Types} {\textbf{types}}
\newcommand{\Var} {\textbf{var}}
\newcommand{\Vars} {\textbf{vars}}
\newcommand{\Axiom} {\textbf{axiom}}
\newcommand{\Axioms} {\textbf{axioms}}
\newcommand{\Spec} {\textbf{spec}}
\newcommand{\Hide} {\textbf{hide}}
\newcommand{\Reveal} {\textbf{reveal}}
\newcommand{\With} {\textbf{with}}
\newcommand{\Then} {\textbf{then}}
\newcommand{\And} {\textbf{and}}
\newcommand{\Local} {\textbf{local}}
\newcommand{\Within} {\textbf{within}}
\newcommand{\Closed} {\textbf{closed}}
\newcommand{\End} {\textbf{end}}
\newcommand{\Imports} {\textbf{imports}}
\newcommand{\Fit} {\textbf{fit}}
\newcommand{\View} {\textbf{view}}
\newcommand{\From} {\textbf{from}}
\newcommand{\To} {\textbf{to}}
\newcommand{\Arch} {\textbf{arch}}
\newcommand{\Units} {\textbf{units}}
\newcommand{\Given} {\textbf{given}}
\newcommand{\Result} {\textbf{result}}
\newcommand{\Library} {\textbf{library}}
\newcommand{\Get} {\textbf{get}}
\newcommand{\Version} {\textbf{version}}
% ABSTRACT SYNTAX CONSTRUCTS:
\newcommand{\SortDecl}[1] {\(#1\)}
\newcommand{\SubsortDecl}[2] {\(#1 < #2\)}
\newcommand{\SubsortDefn}[3] {\(#1 = \{~#2~\Bullet~#3~\}\)}
\newcommand{\IsoDecl}[1] {\(#1\)}
\newcommand{\OpDecl}[2] {\(#1 : #2\)}
\newcommand{\OpDefn}[3] {\(#1 #2~=~#3\)}
\newcommand{\PredDecl}[2] {\(#1 : #2\)}
\newcommand{\PredDefn}[3] {\(#1 #2~\Equiv~#3\)}
\newcommand{\VarDecl}[2] {\(#1 : #2\)}
\newcommand{\Formula}[1] {\(#1\)}
\newcommand{\Term}[1] {\(#1\)}
\newcommand{\Symb}[1] {\(#1\)}
\newcommand{\SymbMap}[2] {\(#1~\MapsTo~#2\)}
\newcommand{\DatatypeDecl}[2] {\(#1~::=~#2\)}
\newcommand{\Alternatives}[1] {\(#1\)}
\newcommand{\Construct}[1] {\(#1\)}
\newcommand{\Components}[1] {\(#1\)}
\newcommand{\Subsorts} {\Sorts}
\newcommand{\Subsort} {\Sort}
\newcommand{\UnitDecl}[2] {\(#1 : #2\)}
\newcommand{\UnitDefn}[2] {\(#1~=~#2\)}
\newcommand{\UnitName}[1] {\(#1\)}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%