% File:    declarations.sty
% Author:  Florian Matthes
% Date:    23-FEB-94
% Purpose: Patechd Makros
%

% ------------------------------------------- Running Text

% Defintions and Referencing:
\newcommand{\define}[2]
  {\begin{tabular}{l}{\small\sl[#1]} \\ #2 \\ \ \end{tabular}}
\newcommand{\refdef}[1]{{\small[#1]}}
\newcommand{\refpar}[1]{$\S~\!$\ref{#1}}

% Spacing:
\newcommand{\medspc}{\hspace{1 ex}}
\newcommand{\bigspc}{\hspace{2.5 ex}}

% -------------------------------------------- Math
% Deduction:
\newcommand{\ded}[2]{\begin{tabular}{c}$ #1 $ \\ \hline $ #2 $ \end{tabular}}
\newcommand{\axiom}[1]{\ded{}{#1}}
\newcommand{\dedtwo}[3]{\begin{tabular}{c}
 $ #1 $ \\ 
 $ #2 $ \\
 \hline 
 $ #3 $ 
\end{tabular}}
\newcommand{\dedtwoh}[3]{\begin{tabular}{c}
 $ #1 $ \bigspc $ #2 $ \\
 \hline 
 $ #3 $ 
\end{tabular}}
\newcommand{\dedthreeh}[4]{\begin{tabular}{c}
 $ #1 $ \bigspc $ #2 $ \bigspc $ #3 $ \\
 \hline 
 $ #4 $ 
\end{tabular}}
\newcommand{\dedfourh}[5]{\begin{tabular}{c}
 $ #1 $ \bigspc $ #2 $ \bigspc $ #3 $  \bigspc $ #4 $ \\
 \hline 
 $ #5 $ 
\end{tabular}}
\newcommand{\dedthree}[4]{\begin{tabular}{c}
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 \hline 
 $ #4 $ 
\end{tabular}}
\newcommand{\dedfour}[5]{\begin{tabular}{c}
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 $ #4 $ \\
 \hline 
 $ #5 $ 
\end{tabular}}
\newcommand{\dedfive}[6]{\begin{tabular}{c}
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 $ #4 $ \\
 $ #5 $ \\
 \hline 
 $ #6 $ 
\end{tabular}}
\newcommand{\dedsix}[7]{\begin{tabular}{c}
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 $ #4 $ \\
 $ #5 $ \\
 $ #6 $ \\
 \hline 
 $ #7 $ 
\end{tabular}}

% General:
\newcommand{\NAT}{{\cal Z}}

\newcommand{\finitemap}[2]{#1 \stackrel{fin}{\longrightarrow} #2}
\newcommand{\mapdomain}[1]{Dom(#1)}
\newcommand{\maprange}[1]{Ran(#1)}
\newcommand{\mapelement}[2]{#1 \mapsto #2}
\newcommand{\makemap}[1]{\{ #1 \}}
\newcommand{\mapupdate}[2]{#1 + #2}

% substitute each #2 in #1 by #3
\newcommand{\substitute}[3]{{#1}[#2 \Leftarrow #3]}

%       +  2    3 
%  1  = |  
%       +  4    5
\newcommand{\choicetwo}[5]{#1 = \left\{
\begin{array}{ll}
   #2 & \mbox{#3} \\
   #4 & \mbox{#5}
\end{array} \right.}

% ------------------------------------------Syntax
\newcommand{\synopt}[1]{$[$ #1 $]$}
\newcommand{\synbrack}[1]{$($ #1 $)$}
\newcommand{\synrep}[1]{$\{$ #1 $\}$}
\newcommand{\synquot}[1]{\verb$"${\rm{#1}}\verb$"$}

% ------------------------------------------TL
% Signatures:
\newcommand{\tlemptysig}{\oslash}
\newcommand{\tlconssig}[2]{#1, #2}
\newcommand{\tlconstwosig}[3]{#1, #2, #3}
\newcommand{\tlRepeat}[1]{{\bf Repeat}({#1})}

% Types:
\newcommand{\tlCase}[2]{{\bf Case}(#1, #2)}
\newcommand{\tlemptyCase}{{\bf Case}(\k{?}, \tlemptysig)}

\newcommand{\tlNok}{{\bf Nok}}
\newcommand{\tlOk}{{\bf Ok}}
\newcommand{\tlDot}[2]{#1.#2}
\newcommand{\tlFun}[2]{{\bf Fun}(#1):#2}
\newcommand{\tlTup}[2]{{\bf Tup}(#1; #2)}
\newcommand{\tlRcd}[1]{{\bf Rcd}(#1)}
\newcommand{\tlExc}[1]{{\bf Exc}(#1)}
\newcommand{\tlRec}[5]{{\bf Rec}(#1, #2_1<:#3_1=#4_1 \ldots #2_#5<:#3_#5=#4_#5)}
\newcommand{\tlRectwo}[2]{{\bf Rec}(#1, #2)}
\newcommand{\tlVar}[1]{{\bf Var}(#1)}
\newcommand{\tlDyn}[1]{{\bf Dyn}(#1)}
\newcommand{\tlOper}[2]{{\bf Oper}(#1)#2}
\newcommand{\tlApply}[2]{#1(#2)}

\newcommand{\tlArr}[1]{{\bf Arr}(#1)}
\newcommand{\tlInt}{{\bf Int}}
\newcommand{\tlBool}{{\bf Bool}}
\newcommand{\tlString}{{\bf String}}

%Bindings:
\newcommand{\tlemptybnd}{\oslash}
\newcommand{\tlconsbnd}[2]{#1, #2}
\newcommand{\tlconstwobnd}[3]{#1, #2, #3}
\newcommand{\tlbnd}[2]{#1=#2}
\newcommand{\tlbndrestr}[3]{\tlhastype{#1}{#2}=#3}
\newcommand{\tlbndRestr}[3]{\tlsubtype{#1}{#2}=#3}

% Type rules:
\newcommand{\judge}[2]{#1 \vdash #2}

\newcommand{\tlissig}[1]{#1 \medspc sig}
\newcommand{\tlhassig}[2]{#1 \, ::  \,#2}
\newcommand{\tlsubsig}[2]{#1 \, <:: \,#2}
\newcommand{\tlisrcdsig}[1]{#1 \medspc rcdsig}
\newcommand{\tltupsubsig}[2]{#1 \, \stackrel{Tup}{<::} \,#2}
\newcommand{\tlrcdsubsig}[2]{#1 \, \stackrel{Rcd}{<::} \,#2}

\newcommand{\tlistype}[1]{#1 \medspc type}
\newcommand{\tlhastype}[2]{#1:#2}
\newcommand{\tlsubtype}[2]{#1<:#2}
\newcommand{\tllettype}[2]{#1=#2}
\newcommand{\tlsigtype}[2]{#1 \, \stackrel{Sig}{::} \,#2}
\newcommand{\tlselector}[2]{\tlsigtype{#1}{#2}}

% Substitutions:
\newcommand{\tlsubstbind}[2]{#1\{\Leftarrow #2\}}
\newcommand{\tlsubsttype}[3]{#1\{#2\leftarrow #3\}}

% Auxiliary:
\newcommand{\tlqualify}[3]{{\rm qualify}(#1;#2;#3)}
\newcommand{\tlcontractive}[2]{#1 \! \downarrow \! #2}
\newcommand{\tlLift}[3]{{[#1]_{#2}^{#3}}}

% ------------------------------------------TML

% TML Values:
\newcommand{\tmlnil}{{\sl nil}}

% TML Store:
\newcommand{\Ref}{{\it Ref}}
\newcommand{\tmlref}[1]{r_{#1}}
\newcommand{\tmlstore}{S}
\newcommand{\makestore}[3]{(#1, #2, #3)}
\newcommand{\storeinit}{{\sl init}}
\newcommand{\storenew}[2]{{\sl new}(#1, #2)}
   % store, size
\newcommand{\storeget}[3]{{\sl get}(#1, #2, #3)}
\newcommand{\storeset}[4]{{\sl set}(#1, #2, #3, #4)}
\newcommand{\storenewclosure}[5]{{\sl newclosure}(#1, #2, #3, #4, #5)}
    % store, locality, nGlob, lambda, literal
\newcommand{\storefixexecute}[2]{{\sl fixexecute}(#1, #2)}

% TML Code:
\newcommand{\tmlnop}{{\bf nop}}
\newcommand{\tmlimmediate}[1]{{\bf imm}(#1)}
\newcommand{\tmlliteral}[1]{{\bf lit}_{#1}}
\newcommand{\tmlgetlocal}[1]{{\bf loc}_{#1}}
\newcommand{\tmlgetparam}[1]{{\bf par}_{#1}}
\newcommand{\tmlgetglobal}[1]{{\bf glb}_{#1}}
\newcommand{\tmlgetindexed}[2]{#1{[#2]}}
\newcommand{\tmlsetlocal}[2]{{\bf loc}_{#1} \leftarrow #2}
\newcommand{\tmlsetglobal}[3]{{\bf glb}_{#2} #1 \leftarrow #3}
\newcommand{\tmlsetindexed}[3]{#1[#2] \leftarrow #3}
\newcommand{\tmlabstract}[4]{\nabla_{#1} \, #2 \, #3 \, #4}
\newcommand{\tmllambda}[2]{\lambda \, #2 \, #1}
\newcommand{\tmlapply}[2]{#1 (#2)}
\newcommand{\tmlseq}[2]{#1 \, ; #2}
\newcommand{\tmlloop}[1]{{\bf loop} \, #1}
\newcommand{\tmlexit}[1]{{\bf exit} \, #1}
\newcommand{\tmltrap}[3]{{\bf trap} \, #1 \, 
   {\bf with} \, l_{#2} \, {\bf do} \,#3}
\newcommand{\tmlraise}[1]{{\bf raise} \, #1}
% ##\newcommand{\tmlsuspend}[1]{{\bf suspend} \, #1}
% ##\newcommand{\tmlhalt}[1]{{\bf halt}(#1)}
\newcommand{\tmlapplybuiltin}[2]{{\bf builtin}(#1)(#2)}

% TML Code ``alt''
\newcommand{\tmltag}[2]{#1 \rightarrow #2}
\newcommand{\tmltags}[1]{\tmltag{b_1}{i_1} \, \ldots \, \tmltag{b_#1}{i_#1}}
\newcommand{\tmlbranches}[1]{c_1 \, \ldots \, c_{#1}}
\newcommand{\tmlalt}[4]{{\bf alt} \, #1 \, {\bf of} \, #2 \, 
  {\bf do} \, #3 \, {\bf else} \, #4}

% TML Evaluation:
\newcommand{\tmlenv}{E}
\newcommand{\tmlframe}[2]{[lit \medspc g_0 \ldots g_{#1} \medspc p_0 \ldots p_{#2}]} 
\newcommand{\tmllocals}{L}
\newcommand{\tmlconfig}[3]{\langle #1, #2, #3 \rangle}
\newcommand{\tmleval}[7]{#1, #2, #3 \vdash #4 
\Rightarrow \tmlconfig{#5}{#6}{#7}}
% no stack no store
\newcommand{\tmlevalnoss}[2]{\tmleval
  {\tmlenv}
  {\tmlstore}
  {\tmllocals}
  {#1}
  {\tmlstore}
  {\tmllocals}
  {#2}
}
% no stack
\newcommand{\tmlevalnos}[3]{\tmleval
  {#1}
  {\tmlstore}
  {\tmllocals}
  {#2}
  {\tmlstore}
  {\tmllocals}
  {#3}
}

% Run-Time-Values:
\newcommand{\tmlok}{{\sl ok}}
\newcommand{\tmlexceptionpack}[1]{{\sl exception}(#1)}
\newcommand{\tmlexitpack}[1]{{\sl exit}(#1)}

% Translation:
\newcommand{\translate}[1]{${\ll}#1{\gg}$}