% File:    declarations.sty
% Author:  Florian Matthes
% Date:    21-JUL-1992
% Purpose: Makros fuer die Diss, TML, TL
% Update:  3-JUL-1993 (GS) fuer Diplomarbeit $$
%          14-AUG-1993 (GS)
%          6-SEP-1995 (Oliver Nietsch)

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

% Leere Seiten ohne Seitennummerierung:
\newcommand{\clearemptydoublepage}{\newpage{\pagestyle{empty}\cleardoublepage}}

% Formatting: 
\newcommand{\TLExt}{{TLExt}} % $$
\newcommand{\TLMin}{{TLMin}} % $$
\newcommand{\TL}{{\sc Tl}}
\newcommand{\TML}{{\sc Tml}}
\newcommand{\TSP}{{\sc Tsp}}
\newcommand{\fsub}{{F$_{\leq}$}}

% Highlight english quotes:
\newcommand{\engl}[1]{{\em #1\/}}

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


% \begin{xpletab} TEXT \end{xpletab}
% Typeset TEXT as a tabulated programming language example:
% Obey linebreaks and multiple spaces, use slanted font
\newenvironment{xpletab}[1]{\begin{xple}\begin{tabular}{#1}%
}{\end{tabular}\end{xple}%
}

% Definitions and Referencing:
\newcommand{\define}[3]
{\begin{tabular}{l}{\small\sl[#1]} \\ #2 \end{tabular}%
\def\test{#3}%
\ifx\test\empty%
\else\par{\small\test}%
\fi%
}
\newcommand{\refdef}[1]{{\small[#1]}}
\newcommand{\refpar}[1]{$\S~\!$\ref{#1}}

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

% $$ geht nicht mit \caption{}. warum?
%\newcounter{bspcount}[section]
%\def\thebsp{\thesection.\@arabic\c@bsp}
%\def\fps@bsp{tbp}
%\def\ftype@bsp{3}
%\def\ext@bsp{lof} % ???
%\def\bspname{Beispiel} % <----------
%\def\fnum@bsp{\bspname{} \thebsp}
%\def\bsp{\@float{bsp}}
%\let\endbsp\end@float
%\@namedef{bsp*}{\@dblfloat{bsp}}
%\@namedef{endbsp*}{\end@dblfloat}

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

% ------------------------------------------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}[1]{{\bf Tup}(#1)} %$$
%$$\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{\tlvbnd}[2]{{\bf var}\ #1=#2}
%$$\newcommand{\tlbndrestr}[3]{\tlhastype{#1}{#2}=#3}
%$$\newcommand{\tlbndRestr}[3]{\tlsubtype{#1}{#2}=#3}

\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{\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}}}

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

% Type rules:
\newcommand{\judge}[2]{#1\,\vdash\,#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.}

% -- Generic:
\newcommand{\nil}{\oslash}
\newcommand{\cons}[2]{(#1, \, #2)}
\newcommand{\consthree}[3]{(#1, \, #2, \, #3)}
\newcommand{\consfour}[4]{(#1, \, #2 \, #3, \, #4)}
\newcommand{\has}[2]{#1 \, :: \, #2}
\newcommand{\is}[2]{#1 \medspc #2}
\newcommand{\ifthenelse}[4]{
  \left\{
   \begin{array}{l@{\quad\Rightarrow\quad}l}
     #1 & #2\\
     #3 & #4
   \end{array}
  \right.}

% -- Context:
\newcommand{\ctxt}{Ctxt}
\newcommand{\cpred}[2]{#1(#2)}
\newcommand{\cpredone}[3]{#1(#2 = #3)}
\newcommand{\cpredtwo}[5]{#1(#2 = #3, \, #4 = #5)}
\newcommand{\cpredthree}[7]{#1(#2 = #3, \, #4 = #5, \, #6 = #7)}
\newcommand{\getenv}[2]{#1[#2]}
\newcommand{\emptyrepl}{Id}
\newcommand{\replace}[2]{#1 \Leftarrow #2}
%\newcommand{\replone}[2]{#1\{#2\}}
%\newcommand{\repltwo}[3]{#1\{#2, \, #3\}}
%\newcommand{\replthree}[4]{#1\{#2, \, #3, \, #4\}}
%\newcommand{\replfour}[5]{#1\{#2, \, #3, \, #4, \, #5\}}

% -- Predicates:
%$$\newcommand{\iside}[1]{\is{#1}{ide}}
\newcommand{\istype}[1]{\is{#1}{type}}
\newcommand{\isvalue}[1]{\is{#1}{value}}
\newcommand{\issig}[1]{\is{#1}{sig}}
\newcommand{\aresigs}[1]{\is{#1}{sigs}}
\newcommand{\isbnd}[1]{\is{#1}{bnd}}
\newcommand{\arebnds}[1]{\is{#1}{bnds}}
\newcommand{\equalIde}[2]{#1 = #2}
\newcommand{\scoped}[1]{#1}
%$$\newcommand{\scopedLabel}[1]{\is{#1}{label}}
\newcommand{\equivsortsigs}[2]{#1 \, \Leftrightarrow \, #2}

% ------------------------------------------ TLExt - Abstract Syntax $$
\newcommand{\defide}[1]{{\bf Def}(#1)}
\newcommand{\refide}[1]{{\bf Ref}(#1)}
\newcommand{\labelide}[1]{{\bf Label}(#1)}
\newcommand{\defnont}[3]{#1(#2) = #3}
\newcommand{\refnont}[3]{#1(#2) ::= #3}
\newcommand{\altprod}[2]{#1 \, | \, #2}
\newcommand{\expprod}[2]{#1 \Rightarrow #2}
\newcommand{\copyprod}[1]{{\bf COPY}(#1)}
\newcommand{\callprod}[2]{#1(\downarrow #2)}
\newcommand{\phdef}[2]{#1 : #2}
\newcommand{\basetyp}[1]{{\bf Typ}(#1)}
\newcommand{\baseval}[1]{{\bf Val}(#1)}
\newcommand{\basesigs}[1]{{\bf Sigs}(#1)}
\newcommand{\basebnds}[1]{{\bf Bnds}(#1)}
\newcommand{\expand}[1]{{\bf Exp}(#1)}
\newcommand{\ph}[1]{{\bf Placeholder}(#1)}
\newcommand{\SortTyp}{{\bf SortTyp}}
\newcommand{\SortVal}{{\bf SortVal}}
\newcommand{\SortSigs}{{\bf SortSigs}}
\newcommand{\SortBnds}{{\bf SortBnds}}
\newcommand{\SortIde}{{\bf SortIde}}
\newcommand{\gramsort}[2]{{\bf SortGram}(\downarrow #1)(\uparrow #2)}
\newcommand{\phsort}[1]{{\bf SortPlaceholder}(#1)}
\newcommand{\hassort}[2]{#1 : #2}

% ------------------------------------------- TLExt Static Semantics $$


% ------------------------------------------TML ($$ removed)