% File:    tml.sty
% Author:  AG
% Date:    17-DEC-1993
% Purpose: LaTeX commands and environments for tml.tex

\newcommand{\leaveout}[1]{}

% also defined in tycoon.sty

\newcommand{\dq}{\verb$"$}

%%% define environment xple and commands xbegin, xmiddle, xend for program examples:
% \begin{xple} TEXT \end{xple}
% Typeset TEXT as a programming language example:
% Obey linebreaks and multiple spaces, use sans-serif font
\def\@xple{\small\sf\trivlist \item[]\if@minipage\else\vskip\parskip\fi
\leftskip\parindent
%##\leftskip\@totalleftmargin 
\rightskip\z@
\topsep\z@\partopsep\z@\parskip\z@\parsep\z@\itemsep\z@   % ## FM
\parindent\z@\parfillskip\@flushglue\parskip\z@
\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
\obeylines}

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

\newcommand{\xbegin}{\begin{tabular}{ll} \begin{minipage}[t]{5cm}\begin{xple}\sf}
\newcommand{\xmiddle}{\end{xple} \end{minipage} &
 \begin{minipage}[t]{8cm} \begin{xple}\sf}
\newcommand{\xend}{\end{xple} \end{minipage} \end{tabular} \vspace{3ex}}

\renewcommand{\xbegin}{\begin{tabular}{ll} \begin{minipage}[t]{6cm}\begin{xple}\sf}
\renewcommand{\xmiddle}{\end{xple} \end{minipage} &
 \begin{minipage}[t]{10cm} \begin{xple}\sf}
\renewcommand{\xend}{\end{xple} \end{minipage} \end{tabular} \vspace{0ex}}

\newcommand{\xxbegin}{\begin{tabular}{lll}\mbox\bgroup}
\newcommand{\xxmiddle}{\egroup&}
\newcommand{\xxcomment}{&\begin{xple}\sf}
\newcommand{\xxcommentend}{\end{xple}\end{tabular}}
\newcommand{\xxend}{\end{tabular}}

% emphasize
\newcommand{\e}[1]{{\em #1\/}}

% program text embedded within main document text
\newcommand{\p}[1]{{\frenchspacing\sl{}#1}}

% program keyword
\newcommand{\k}[1]{\mbox{\bf #1}}

%plain vector: x1...xn
\newcommand{\pvec}[1]{\mbox{$#1_1\ldots{}#1_n$}}

\newcommand{\arrayget}{\mbox{$[\,]$}}
\newcommand{\arrayset}{\mbox{$[\,]$:=}}

\newcommand{\epsfbild}[2]{
  \begin{center}
   \leavevmode
   #2
   \epsffile{#1}
  \end{center}}


\newcommand{\comment}[1]{\par{[*** #1 ***]}\par}
\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}$}}

\newcommand{\tspoid} {OID}


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

% 
\newenvironment{grammar}
{\begin{xple}\begin{tabbing}XXXX\=XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\=XXXXXXXXX\=\kill}{\end{tabbing}\end{xple}}


% Translation:
\newcommand{\lll}{$\ll$}	% <<
\newcommand{\ggg}{$\gg$}	% >>

\newcommand{\mv}[1]{$#1$}	% meta-variable, use slanted math font




% ------------------------------------------- Running Text
% Formatting: 

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

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

%------------------------------------------TL

% ...not copied yet from ~wetzel/IW/Diss/deduction.sty

% -------------------------------------------- Math

% Deduction:
\newcommand{\ded}[3]{ \raggedright
  $
  \begin{array}{l}
  \mbox{{\it [#1]}} \\
  \begin{array}{c}
   #2 \\[0.2ex]
   \hline
   #3 \rule{0cm}{2.5ex}
  \end{array}
  \end{array} $
}

\newcommand{\axiom}[1]{\ded{}{#1}}

% General:
\newcommand{\Dom}{\, \mbox{\it Dom}}
\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$"$}

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

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

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

\def\indent{\list{}{
  \topsep -\parskip
  \listparindent-2ex
  \leftmargin2ex}\item[]}
\let\endindent=\endlist

\newcommand{\stuetze}{\rule[-2pt]{0pt}{10pt}}

\newcommand{\hboxni}[1]{\hbox{\noindent\stuetze #1}}
  
  
\newcommand{\hboxrparen}[1]{\hboxni{\setbox254=\hboxni{#1}\setbox255=\hboxni{)}\dimen255=\dp254\advance\dimen255 by -\dp255\box254\lower\dimen255\box255}}

%\hboxni{\copy\bbb\vbox{\hboxni{)}}}}

%\renewcommand{\hboxrparen}[1]{\hboxni{#1)}}

%\renewcommand{\hboxrparen}[1]{\hboxni{\hboxni{#1}\vbox{\vss\hboxni{)}}}}

%\renewcommand{\hboxrparen}[1]{\hboxni{\newbox\aaa\setbox\aaa=\vbox{\hboxni{#1}}\box\aaa}}

%\setbox\bbb=\vbox{\hboxni{)}}
%\newdimen\ccc
%\ccc=\dp\aaa
%\advance\ccc by -\dp\bbb
%\box\aaa\lower\ccc\box\bbb}}

\newcount\tmllevel
\newcount\savetmllevel
\tmllevel=0

\newcommand{\tmlarg}[1]
{\savetmllevel=\tmllevel
\global\tmllevel=0
\hboxni{$#1$}
\global\tmllevel=\savetmllevel}

\newcommand{\tmlarglast}[1]{\global\advance\tmllevel by 1\hboxni{$#1$\closeparens}}

\newcommand{\tmlbody}[1]{\hboxni{\hspace{-0.5ex}$#1\closeparens$}}

\newcommand{\closeparens}[0]{\ifnum\tmllevel>0
\hboxni{\loop \ifnum\tmllevel>0 )\global\advance\tmllevel by -1 \repeat}
\fi}

%\newcommand{\funfun}[3]{\hboxni{\tmlarg{(#1}$(#2)\,$\tmlarglast{#3}}}
\newcommand{\funfun}[3]{\hboxni{\tmlarg{#1(#2)}\tmlbody{#3}}}

  
%\newcommand{\funfunb}[3]{\hboxni{\vtop{\hboxni{\tmlarg{(#1}$(#2)$}\hboxni{\hspace*{2ex}\tmlarglast{#3}}}}}

\newcommand{\funfunb}[3]{
\hboxni{\vtop{\hboxni{\tmlarg{#1(#2)}}\hboxni{\hspace*{2ex}\tmlbody{#3}}}}}

% \fun{x y z}{body}
% (lambda (x y z) body)
      
\newcommand{\fun}[2]{\funfun{\lambda}{#1}{#2}}
\newcommand{\proc}[2]{\funfun{\k{proc}}{#1}{#2}}
\newcommand{\cont}[2]{\funfun{\k{cont}}{#1}{#2}}

\newcommand{\contni}[3]{\vtop{\hboxni{\tmlarg{#1} \k{cont}$(#2)$} \tmlbody{#3}}}

% \funb{x y z}{body}
% (lambda (x y z)
%    body)

\newcommand{\funb}[2]{\funfunb{\lambda}{#1}{#2}}
\newcommand{\procb}[2]{\funfunb{\k{proc}}{#1}{#2}}
\newcommand{\contb}[2]{\funfunb{\k{cont}}{#1}{#2}}

% \applyiii{f}{x}{y}{z}
% (f x y z)

\newcommand{\xlat}[3]{\hboxni{$\ll$#1,#2,#3$\gg$}}

\newcommand{\app}[2]{\hboxni{(\tmlarg{#1}\,#2}}
%\newcommand{\app}[2]{\hboxni{\tmlarg{#1(#2}}}

\newcommand{\apply}[1]{\tmlarg{(#1)}}
\newcommand{\applyi}[2]{\app{#1}{\tmlarglast{#2}}}
\newcommand{\applyii}[3]{\app{#1}{\tmlarg{#2}\,\tmlarglast{#3}}}
\newcommand{\applyiii}[4]{\app{#1}{\tmlarg{#2}\,\tmlarg{#3}\,\tmlarglast{#4}}}
\newcommand{\applyiv}[5]{\app{#1}{\tmlarg{#2}\,\tmlarg{#3}\,\tmlarg{#4}\,\tmlarglast{#5}}}

\newcommand{\applyv}[6]{\app{#1}{\tmlarg{#2}\,\tmlarg{#3}\,\tmlarg{#4}\,\tmlarg{#5}\,\tmlarglast{#6}}}

\newcommand{\applyvi}[7]{\app{#1}{\tmlarg{#2}\,\tmlarg{#3}\,\tmlarg{#4}\,\tmlarg{#5}\,\tmlarg{#6}\,\tmlarglast{#7}}}

\newcommand{\applyvii}[8]{\app{#1}{\tmlarg{#2}\,\tmlarg{#3}\,\tmlarg{#4}\,\tmlarg{#5}\,\tmlarg{#6}\,\tmlarg{#7}\,\tmlarglast{#8}}}

\newcommand{\applyviii}[9]{\app{#1}{\tmlarg{#2}\,\tmlarg{#3}\,\tmlarg{#4}\,\tmlarg{#5}\,\tmlarg{#6}\,\tmlarg{#7}\,\tmlarg{#8}\,\tmlarglast{#9}}}


% \applybiii{f}{x}{y}{z}
% (f x
%    y
%    z)

\newcommand{\applyb}[2]{\hboxni{\tmlarg{(#1}\,\vtop{#2}}}
%\newcommand{\applyb}[2]{\hboxni{\tmlarg{#1}(\vtop{\tmlarglast{#2}}}}

\newcommand{\applybi}[2]{\applyb{#1}{\tmlarglast{#2}}}

\newcommand{\applybii}[3]{\applyb{#1}{\tmlarg{#2}\tmlarglast{#3}}}

\newcommand{\applybiii}[4]{\applyb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarglast{#4}}}

\newcommand{\applybiv}[5]{\applyb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarg{#4}\tmlarglast{#5}}}

\newcommand{\applybv}[6]{\applyb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarg{#4}\tmlarg{#5}\tmlarg{#6}\tmlarglast{#6}}}

\newcommand{\applybvi}[7]{\applyb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarg{#4}\tmlarg{#5}\tmlarg{#6}\tmlarglast{#7}}}

\newcommand{\applybvii}[8]{\applyb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarg{#4}\tmlarg{#5}\tmlarg{#6}\tmlarg{#7}\tmlarglast{#8}}}

\newcommand{\applybviii}[9]{\applyb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarg{#4}\tmlarg{#5}\tmlarg{#6}\tmlarg{#7}\tmlarg{#8}\tmlarglast{#9}}}


% \applybbiii{f}{x}{y}{z}
% (f
%    x
%    y
%    z)

% \applybbiii{f}{x}{y}{z}
% f
%  (x
%   y
%   z)

\newcommand{\applybb}[2]{\vtop{\tmlarg{(#1}\moveright2ex\vtop{#2}}}
%\newcommand{\applybb}[2]{\vtop{\tmlarg{#1}\moveright2ex\hboxni{(\vtop{#2}}}}

\newcommand{\applybbi}[2]{\applybb{#1}{\tmlarglast{#2}}}
\newcommand{\applybbii}[3]{\applybb{#1}{\tmlarg{#2}\tmlarglast{#3}}}
\newcommand{\applybbiii}[4]{\applybb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarglast{#4}}}
\newcommand{\applybbiiii}[5]{\applybb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarg{#4}\tmlarglast{#5}}}
\newcommand{\applybbiiiii}[6]{\applybb{#1}{\tmlarg{#2}\tmlarg{#3}\tmlarg{#4}\tmlarg{#5}\tmlarglast{#6}}}

% Rewriting:

\newcommand{\tmlrewrite}[4]{\mbox{$\fded{#3}{#2}{#1}{#4}$}}
      
\renewcommand{\tmlrewrite}[4]
{\[ \mbox{$#3$}
\hspace{1ex}\frac{\mbox{\it #1}}{\mbox{$$}}
\mbox{\hspace{-2pt}$\triangleright\hspace{1ex}
\,#4$
\hspace{5ex} $#2$ } \]}
 
% substitute each #3 in #1 by #2
\newcommand{\tmlsubst}[3]{#1[#2/#3]}

\newcommand{\tmlrefcount}[2]{|#1|_{#2}}

\newcommand{\tmlcons}[2]{(#1\,.\,#2)}

\newcommand{\tmlnil}{()}

\newcommand{\tmlappend}[2]{#1::#2}

\newcommand{\tmlsingleton}[1]{(#1)}


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

%\newcommand{\fded}[4]
%  {\mbox{$#1$}\,\begin{tabular}{c}
%   \mbox{$#2$} \\ \hline
%   \mbox{\it #3}
%   \end{tabular}\triangleright\,\mbox{$#4$}}
 
\newcommand{\fded}[4]{\begin{tabular}{rcl}
    & \mbox{$#2$}   & \\ \cline{2-2}
    \raisebox{1.5ex}[-1.5ex]{$#1$} & \mbox{\it #3} &
    \raisebox{1.5ex}[-1.5ex]{\hspace{-2ex} $\triangleright\,#4$} \\
    &  &
\end{tabular} }

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



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