% $Id: rep-trans.sty,v 1.1 1998/11/02 21:18:14 jbw Exp $

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{rep-trans}[1998/10/28 Representation Transformation Framework macros]

\RequirePackage{jbw-math}
\RequirePackage{cil}

% Evaluate sexp on next line in Emacs for outline minor mode with this file.
% (progn(outline-minor-mode 1)(setq outline-regexp "%%%+ "))

%%% Intermediate Results of Rep. Trans. Framework %%%%%%%%%%%%%%%%%%%%

\let\langIn=\lang
\let\langFA=\langDLO
\let\langFS=\langDLS
\let\langST=\langDLS
\let\langOut=\lang

\newcommand{\ProgIn}{\ensuremath{P_0}}
\newcommand{\ProgFA}{\ensuremath{P_1}}
\newcommand{\ProgFS}{\ensuremath{P_2}}
\newcommand{\ProgST}{\ensuremath{P_3}}
\newcommand{\ProgOut}{\ensuremath{P_4}}
\newcommand{\ProgUnknown}{\ensuremath{P}}

%%% Flow Separation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\FS}[1]{\overline{#1}}
\newcommand{\typeRespecting}{type/label consistent}
\newcommand{\uniquelyLabelled}{distinctly labelled}

%%% Representation Choices %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\R}{{\ensuremath{\cal R}}} %Representation choice

\newcommand{\Rep}{\R}
\newcommand{\Rsup}[1]{\ensuremath{\Rep^{\text{\tiny\textup{#1}}}}}

\newcommand{\RabsSym}{\ensuremath{\Rep^\lambda}}
\newcommand{\Rabs}[4]{\ensuremath{\RabsSym\!\Parens{{#1},{#2},{#3},{#4}}}}
\newcommand{\RappSym}{\ensuremath{\Rep^@}}
\newcommand{\Rapp}[5]{\ensuremath{\RappSym\!\Parens{{#1},{#2},{#3},{#4},{#5}}}}
\newcommand{\RvarSym}{\ensuremath{\Rsup{var}}}
\newcommand{\Rvar}[3]{\ensuremath{\RvarSym\!\Parens{{#1},{#2},{#3}}}}
\newcommand{\RarrSym}{\ensuremath{\Rep^\to}}
\newcommand{\Rarr}[4]{\ensuremath{\RarrSym\!\Parens{{#1},{#2},{#3},{#4}}}}

\newcommand{\rtquad}{\ensuremath{\langle \RabsSym,\RappSym,
			              \RvarSym,\RarrSym\rangle}}

\newcommand{\C}{{\ensuremath{\cal C}}} % closure representation choice

\newcommand{\Clo}{\C}
\newcommand{\Csup}[1]{\ensuremath{\Clo^{\text{\tiny\textup{#1}}}}}

\newcommand{\CabsSym}{\ensuremath{\Clo^\lambda}}
\newcommand{\Cabs}[4]{\ensuremath{\CabsSym\!\Parens{{#1},{#2},{#3},{#4}}}}
\newcommand{\CappSym}{\ensuremath{\Clo^@}}
\newcommand{\Capp}[2]{\ensuremath{\CappSym\!\Parens{{#1},{#2}}}}
\newcommand{\CvarSym}{\ensuremath{\Csup{var}}}
\newcommand{\Cvar}[2]{\ensuremath{\CvarSym\!\Parens{{#1},{#2}}}}
\newcommand{\CarrSym}{\ensuremath{\Clo^\to}}
\newcommand{\Carr}[4]{\ensuremath{\CarrSym\!\Parens{{#1},{#2},{#3},{#4}}}}

\newcommand{\CloQuad}{\ensuremath{\langle \CabsSym,\CappSym,
				       \CvarSym,\CarrSym\rangle}}

\newcommand{\E}{{\ensuremath{\cal E}}} % environment epresentation choice

\newcommand{\Env}{\E}
\newcommand{\Esup}[1]{\ensuremath{\Env^{\text{\tiny\textup{#1}}}}}

\newcommand{\EabsSym}{\ensuremath{\Env^\lambda}}
\newcommand{\Eabs}[3]{\ensuremath{\EabsSym\!\Parens{{#1},{#2},{#3}}}}
\newcommand{\EappSym}{\ensuremath{\Env^@}}
\newcommand{\Eapp}[5]{\ensuremath{\EappSym\!\Parens{{#1},{#2},{#3},{#4},{#5}}}}
\newcommand{\EvarSym}{\ensuremath{\Esup{var}}}
\newcommand{\Evar}[2]{\ensuremath{\EvarSym\!\Parens{{#1},{#2}}}}
\newcommand{\EarrSym}{\ensuremath{\Env^\to}}
\newcommand{\Earr}[2]{\ensuremath{\EarrSym\!\Parens{{#1},{#2}}}}

\newcommand{\EnvQuad}{\ensuremath{\langle \EabsSym,\EappSym,
				       \EvarSym,\EarrSym\rangle}}

\newcommand{\RenvtypeSym}{\ensuremath{\Rsup{envtype}}}
\newcommand{\Renvtype}[1]{\ensuremath{\RenvtypeSym\!\Parens{#1}}}
\let\envtype=\Renvtype
\newcommand{\RenvtermSym}{\ensuremath{\Rsup{envterm}}}
\newcommand{\Renvterm}[2]{\ensuremath{\RenvtermSym\!\Parens{{#1},{#2}}}}

\newcommand{\RcodeqSym}{\ensuremath{\Rsup{code?}}}
\newcommand{\Rcodeq}[1]{\ensuremath{\Rsup{code?}\!\Parens{#1}}}

\newcommand{\RenvqSym}{\ensuremath{\Rsup{env?}}}
\newcommand{\Renvq}[1]{\ensuremath{\Rsup{env?}\!\Parens{#1}}}

% The identity function on vars that translates their types
\newcommand{\IdFunType}{\ensuremath{\mathrm{id}^{\BBracks{\cdot}}}}

\newcommand{\VarAccessEnv}{\ensuremath{E}} % variable access code environment

%%% Representation Transformation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\RXtermX}[3]{\BBracks{#1}_{\Rep,{#2},{#3}}} %Term transformation
\newcommand{\RXterm}[1]{\RXtermX{#1}{\VarAccessEnv}{N}} % E,N wired in!!!
\newcommand{\RXtermV}[3]{\RXtermX{#2}{\Rvar{#1}{\VarAccessEnv}{#3}}{#3}}
% Type transformation
\newcommand{\RXtypeY}[3]{\BBracks{#1}_{{#2},{#3}}}
\newcommand{\RXtypeX}[2]{\BBracks{#1}_{{\Rep},{#2}}}
\newcommand{\RXtype}[1]{\BBracks{#1}_{{\Rep},{N}}}   % N is wired in!!!
 
%%% Rep. Choices vs. Label Separation and Splitting/Tagging %%%%%%%%%%

\newcommand{\RepInfoFSSym}{\ensuremath{\Pi^{\mathtiny{\R}}_{\mathrm{FS}}}}
\newcommand{\RepInfoFS}[1]{\ensuremath{\RepInfoFSSym\Parens{{#1}}}}
\newcommand{\RepInfoSTSym}%
  {\ensuremath{\Pi^{\mathtiny{\R}}_{\mathrm{ST}}}}
\newcommand{\RepInfoSTAppSym}%
  {\ensuremath{\Pi^{\mathtiny{\R},@}_{\mathrm{ST}}}}
\newcommand{\RepInfoSTApp}[1]{\ensuremath{\RepInfoSTAppSym\Parens{{#1}}}}
\newcommand{\RepInfoSTAbsSym}%
  {\ensuremath{\Pi^{\mathtiny{\R},\lambda}_{\mathrm{ST}}}}
\newcommand{\RepInfoSTAbs}[1]{\ensuremath{\RepInfoSTAbsSym\Parens{{#1}}}}

\newcommand{\RepInfoSTPair}{\ensuremath{\Angles{\RepInfoSTAbsSym,
					       \RepInfoSTAppSym}}}

%%% Emacs File-Local Variables %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Local variables:
% outline-regexp: "%%%+ "
% end:
