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

% ------------------------------------------- Running Text
%------neu aus fm-diss.tex
\newcommand{\e}[1]{{\em #1\/}}
\newcommand{\k}[1]{\mathbf {#1}}
\newcommand{\kb}[1]{{\bf #1}}
\newcommand{\s}[1]{{\sl #1\/}}
\newcommand{\r}{$\Rightarrow$}


\newcommand{\comment}[1]{\par{[*** #1 ***]}\par}
\newcommand{\p}[1]{{\frenchspacing\sl{}#1}}
\newcommand{\reply}[1]{{\mathbf$\Rightarrow$} #1}
\def\longhrule{\par\hbox to \linewidth{\hss
               \hbox to \textwidth{\hrulefill}}\par}

%------neu aus fm-diss.tex
% 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{\tlconsimp}[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}(\k{?}, \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_{11}=#4_{21} \ldots #2_#5<:#3_{1n}=#4_{2n})}
\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{\tlInter}[3]{\mathbf{interface}(#1,\;#2,\;#3)}
\newcommand{\tlModul}[3]{\mathbf{module}(#1,\;#2,\;#3)}

\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{\tlvbnd}[2]{\mathbf{ 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}}
\newcommand{\dedseven}[8]{\begin{tabular}{c}
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 $ #4 $ \\
 $ #5 $ \\
 $ #6 $ \\
 $ #7 $ \\
 \hline 
 $ #8 $ 
\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]{\mathbf{Def}(#1)}
\newcommand{\refide}[1]{\mathbf{Ref}(#1)}
\newcommand{\labelide}[1]{\mathbf{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]{\mathbf{ COPY}(#1)}
\newcommand{\callprod}[2]{#1(\downarrow #2)}
\newcommand{\phdef}[2]{#1 : #2}
\newcommand{\basetyp}[1]{\mathbf{Typ}(#1)}
\newcommand{\baseval}[1]{\mathbf{Val}(#1)}
\newcommand{\basesigs}[1]{\mathbf{Sigs}(#1)}
\newcommand{\basebnds}[1]{\mathbf{Bnds}(#1)}
\newcommand{\expand}[1]{\mathbf{Exp}(#1)}
\newcommand{\ph}[1]{\mathbf{Placeholder}(#1)}
\newcommand{\SortTyp}{\mathbf{SortTyp}}
\newcommand{\SortVal}{\mathbf{SortVal}}
\newcommand{\SortSigs}{\mathbf{SortSigs}}
\newcommand{\SortBnds}{\mathbf{SortBnds}}
\newcommand{\SortIde}{\mathbf{SortIde}}
\newcommand{\gramsort}[2]{\mathbf{SortGram}(\downarrow #1)(\uparrow #2)}
\newcommand{\phsort}[1]{\mathbf{SortPlaceholder}(#1)}
\newcommand{\hassort}[2]{#1 : #2}

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


% ------------------------------------------OM1 

\newcommand{\istype}[1]{\is{#1}{type}}
\newcommand{\isclass}[1]{\is{#1}{class}}
\newcommand{\isschema}[1]{\is{#1}{schema}}
\newcommand{\istypeide}[1]{\is{#1}{typeIde}}
\newcommand{\isrcdsigs}[1]{\is{#1}{rcdSigs}}
\newcommand{\isoptsigs}[1]{\is{#1}{optSigs}}


%\newcommand{\isClassInterface}[1]{\is{#1}{isOM1ClassInterface}}
%\newcommand{\hasCompleteImports}[1]{\is{#1}{hasCompleteImports}}
%\newcommand{\hasCompleteExports}[1]{\is{#1}{hasCompleteExports}}
%\newcommand{\hasCorrespClass}[1]{\is{#1}{hasCorrespOM1Class}}
%\newcommand{\refList}[1]{\is{#1}{refList}}
%\newcommand{\refs}[1]{\is{#1}{refsdvia}}


\newcommand{\tlind}{_{TL}}
\newcommand{\tl}{_{T}}
\newcommand{\omind}{_{OM1}}
\newcommand{\om}{_{O}}
\newcommand{\tltoom}{_{TL \rightarrow OM1}}
\newcommand{\omtotl}{_{OM1 \rightarrow TL}}

%\newcommand{\omNok}{\mathbf{Nok}}
%\newcommand{\omOk}{\mathbf{Ok}}
%\newcommand{\omRcd}{\mathbf{Rcd}}
%\newcommand{\omSet}{\mathbf{Set}}
%\newcommand{\omList}{\mathbf{List}}
%\newcommand{\omArr}{\mathbf{Arr}}
%\newcommand{\omOpt}{\mathbf{Opt}}


\newcommand{\genN}{_{genN}}
\newcommand{\genC}{_{genC}}
\newcommand{\genS}{_{genS}}
\newcommand{\auxOM}{_{auxOM}}
\newcommand{\auxTL}{_{auxTL}}
\newcommand{\auxTLc}{_{auxTLc}}
\newcommand{\str}{_{str}}
\newcommand{\bricks}{_{bricks}}

\newcommand{\omnok}{\mathbf{Nok}}
\newcommand{\omok}{\mathbf{Ok}}
\newcommand{\omint}{\mathbf{Int}}
\newcommand{\ombool}{\mathbf{Bool}}
\newcommand{\omstring}{\mathbf{String}}
\newcommand{\omrcd}[1]{\mathbf{Rcd}\,(#1)}
\newcommand{\omopt}[1]{\mathbf{Opt}\,(#1)}
\newcommand{\omset}[1]{\mathbf{Set}\,(#1)}
\newcommand{\omlist}[1]{\mathbf{List}\,(#1)}
\newcommand{\omarray}[2]{\mathbf{Array}\,(#1 \;#2)}
\newcommand{\omcomp}{\mathbf{Comp}}
\newcommand{\omtypedef}{\mathbf{TypeDef}}
\newcommand{\omclassdef}{\mathbf{ClassDef}}
\newcommand{\omclass}[3]{\mathbf{Class}\,(#1 \;#2 \;#3)}
\newcommand{\omtype}{\mathbf{Type}}


%----------------auszulassen

\newcommand{\leaveOut}[1]{}

%----------------function deduction rules

\newcommand{\fded}[4]{$#1\,$\begin{tabular}{c}$ #2 $ \\ \hline $ #3 $ \end{tabular}$\triangleright\, #4$ }
 


\newcommand{\fdedtm}[4]{$#1\,$\begin{tabular}{c}$ #3 $ \\ \hline $ #4 $ \end{tabular}$\triangleright\,#2$}



%------- Wiederholung der ded-Befehle ohne mathmode um Parameter (n fuer naked)
\newcommand{\dedn}[2]{\begin{tabular}{c} #1 \\ \hline #2 \end{tabular}}
\newcommand{\axiomn}[1]{\dedn{}{#1}}
\newcommand{\dedtwon}[3]{\begin{tabular}{c}
 #1 \\ 
 #2 \\
 \hline 
 #3 
\end{tabular}}
\newcommand{\dedtwohn}[3]{\begin{tabular}{c}
 #1 \bigspc #2 \\
 \hline 
 #3
\end{tabular}}
\newcommand{\dedthreehn}[4]{\begin{tabular}{c}
 #1 \bigspc #2 \bigspc #3 \\
 \hline 
 #4 
\end{tabular}}
\newcommand{\dedfourhn}[5]{\begin{tabular}{c}
 #1 \bigspc #2 \bigspc #3 \bigspc #4 \\
 \hline 
 #5 
\end{tabular}}
\newcommand{\dedthreen}[4]{\begin{tabular}{c}
 #1 \\ 
 #2 \\
 #3 \\
 \hline 
 #4 
\end{tabular}}
\newcommand{\dedfourn}[5]{\begin{tabular}{c}
 #1 \\ 
 #2 \\
 #3 \\
 #4 \\
 \hline 
 #5 
\end{tabular}}
\newcommand{\dedfiven}[6]{\begin{tabular}{c}
 #1 \\ 
 #2 \\
 #3 \\
 #4 \\
 #5 \\
 \hline 
 #6 
\end{tabular}}
\newcommand{\dedsixn}[7]{\begin{tabular}{c}
 #1 \\ 
 #2 \\
 #3 \\
 #4 \\
 #5 \\
 #6 \\
 \hline 
 #7 
\end{tabular}}
\newcommand{\dedsevenn}[8]{\begin{tabular}{c}
 #1 \\ 
 #2 \\
 #3 \\
 #4 \\
 #5 \\
 #6 \\
 #7 \\
 \hline 
 #8 
\end{tabular}}

%--------------------------------tltext
\newcommand{\tlbegin}[1]
{\begin{minipage}[t]{#1}
%\begin{tabular*}{7.8cm}{l}
%{\bf #1}\\
%\hline
%\end{tabular*}
\begin{tabbing}
xx \= xx \= xx \= xx\= xx\= xx\= xx\= xx\= xx\= xx\= xxxxxxxxxxx\= \kill
}
\newcommand{\tlend}{ \end{tabbing}\end{minipage} }
\newcommand{\tltext}[2]{\framebox[#1][l]{\tlbegin{#1} 
#2 \tlend}}

%------------------- hinzugefuegt
\newcommand{\tlfun}[3]{\mathbf{fun}(#1):#2\;#3}
\newcommand{\tlseq}[3]{\mathbf{seq}(#1,\;#2,\;#3)}
\newcommand{\tlextend}[2]{\mathbf{extend}(#1,\;#2)}

\newcommand{\omref}[1]{\mathbf{ref}\,(#1)}