% File:    declarations.sty
% Author:  Florian Matthes
% Date:    21-JUL-1992
% 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{\trivlist \item[]\if@minipage\else\vskip\parskip\fi
\leftskip 1cm
%\@totalleftmargin
\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}}

% 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{\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]{\mathbf{Repeat}({#1})}

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

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

\newcommand{\tlArr}[1]{\mathbf{Arr}(#1)}
\newcommand{\tlInt}{\mathbf{Int}}
\newcommand{\tlBool}{\mathbf{Bool}}
\newcommand{\tlString}{\mathbf{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]{\mathbf{qualify}(#1;#2;#3)}
\newcommand{\tlcontractive}[2]{#1 \! \downarrow \! #2}
\newcommand{\tlLift}[3]{{[#1]_{#2}^{#3}}}

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

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

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

% TML Code:
\newcommand{\tmlnop}{\mathbf{nop}}
\newcommand{\tmlimmediate}[1]{\mathbf{imm}(#1)}
\newcommand{\tmlliteral}[1]{\mathbf{lit}_{#1}}
\newcommand{\tmlgetlocal}[1]{\mathbf{loc}_{#1}}
\newcommand{\tmlgetparam}[1]{\mathbf{par}_{#1}}
\newcommand{\tmlgetglobal}[1]{\mathbf{glb}_{#1}}
\newcommand{\tmlgetindexed}[2]{#1{[#2]}}
\newcommand{\tmlsetlocal}[2]{\mathbf{loc}_{#1} \leftarrow #2}
\newcommand{\tmlsetglobal}[3]{\mathbf{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]{\mathbf{loop} \, #1}
\newcommand{\tmlexit}[1]{\mathbf{exit} \, #1}
\newcommand{\tmltrap}[3]{\mathbf{trap} \, #1 \, 
   \mathbf{with} \, l_{#2} \, \mathbf{do} \,#3}
\newcommand{\tmlraise}[1]{\mathbf{raise} \, #1}
% ##\newcommand{\tmlsuspend}[1]{\mathbf{suspend} \, #1}
% ##\newcommand{\tmlhalt}[1]{\mathbf{halt}(#1)}
\newcommand{\tmlapplybuiltin}[2]{\mathbf{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]{\mathbf{alt} \, #1 \, \mathbf{of} \, #2 \, 
  \mathbf{do} \, #3 \, \mathbf{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}$}