% File:    declarations.sty
% Author:  Florian Matthes
% Date:    20-FEB-1993
% Purpose: Makros fuer die Diss, TML, TL
%

% ------------------------------------------- Running Text
% Formatting:
\newcommand{\TL}{{\sc Tl}}
\newcommand{\TML}{{\sc Tml}}
\newcommand{\TSP}{{\sc Tsp}}
\newcommand{\engl}[1]{{\em #1\/}}
\newcommand{\fsub}{{F$_{\leq}$}}

% \begin{xple} TEXT \end{xple}
% Typeset TEXT as a programming language example:
% Obey linebreaks and multiple spaces, use slanted font
\def\@xple{\small\trivlist \item[]\if@minipage\else\vskip\parskip\fi
\leftskip\@totalleftmargin\advance\leftskip\parindent
\rightskip\z@
\parindent\z@\parfillskip\@flushglue\parskip\z@
\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
\obeylines \sl}

\def\xple{\@xple \frenchspacing\@vobeyspaces}
\let\endxple=\endtrivlist


% 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}}

\newcommand{\definetk}[2]
  {\begin{tabular}{l}{\small\sl[#1]} \\ {\small #2} \\ \ \end{tabular}}

% Environments;
\newcounter{bspcount}[section]
\newenvironment{bsp}{\begin{trivlist}\stepcounter{bspcount}\item[]{\bf Beispiel~
\thesection.\thebspcount:}}{$\Box$\end{trivlist}}

% Framed and centered figures:
\newcommand{\framedcenter}[1]{\framebox{\parbox{\textwidth}{\centering#1}}}

% Replace Bullets by Triangles:
\renewcommand{\labelitemi}{$\triangleright$}

% 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{\dedone}[2]{\begin{tabular}{c}
 $ #1 $ \\
 \hline
 $ #2 $
\end{tabular}}
\newcommand{\dedonetwo}[3]{\begin{tabular}{c}
 $ #1 $ \\
 \hline
 $ #2 $ \\
 $ #3 $
\end{tabular}}
\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{\dedthreetk}[4]{\begin{tabular}{c}
 {\vspace{-1.8mm} $ #1 $} \\
 {\vspace{-1.8mm} $ #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]}

\newcommand{\choiceone}[4]{#1 = \{
\begin{array}{ll}
   #2 & \mbox{#3} \\
      & \mbox{#4}
\end{array}}

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

\newcommand{\cchoicetwo}[7]{#1 = \left\{
\begin{array}{ll}
   #2 & \mbox{#3} \\
      & \mbox{#4} \\
   #5 & \mbox{#6} \\
      & \mbox{#7} 
\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{\judgetk}[2]{#1 \Rightarrow #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{\Prin}{{\it Prin}}
\newcommand{\tmlref}[1]{r_{#1}}
\newcommand{\tmlstore}{S}
\newcommand{\makestore}[4]{(#1, #2, #3, #4)}
\newcommand{\storeinit}{{\sl store.init}}
\newcommand{\storenewNoParam}{{\sl store.new}}
\newcommand{\storenew}[4]{{\sl \storenewNoParam}(#1, #2, #3, #4)}
   % store, locality, size
\newcommand{\storegetNoParam}{{\sl store.get}}
\newcommand{\storeget}[3]{{\sl \storegetNoParam}(#1, #2, #3)}
\newcommand{\storesetNoParam}{{\sl store.set}}
\newcommand{\storeset}[4]{{\sl \storesetNoParam}(#1, #2, #3, #4)}
\newcommand{\storenewclosure}[6]{{\sl store.\-new\-clos\-ure}(#1, #2, #3, 
#4, #5, #6)}
    % store, locality, nGlob, lambda, literal
\newcommand{\storefixexecute}[2]{{\sl store.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{\tmlseccon}{SC}
\newcommand{\tmlframe}[2]{[lit \medspc g_0 \ldots g_{#1} \medspc p_0 \ldots p_{#2}]}
\newcommand{\tmlsec}{[eP, rP]}
\newcommand{\tmllocals}{L}
\newcommand{\tmlconfig}[3]{\langle #1, #2, #3 \rangle}
\newcommand{\tmlseceval}[8]{#1, #2, #3, #4 \vdash #5
\Rightarrow \tmlconfig{#6}{#7}{#8}}
\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}$}


