% FILE. . . . . /home/hak/technical/papers/ilog/refect/main.mac % EDIT BY . . . Hassan Ait Kaci % ON MACHINE. . Latitude314.Ilog.Fr % STARTED ON. . Thu May 16 07:30:25 2002 % Last modified on Tue Jan 14 12:06:01 2003 by Hak % FILE. . . . . /usr/home/hak/Teaching/383/notes.mac % EDIT BY . . . Hassan Ait-Kaci % ON MACHINE. . Muenster % STARTED ON. . Sat May 23 15:21:15 1998 % Last modified on Mon May 14 13:24:28 2001 by Hak %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \long\def\ignore#{\relax} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \let\codesize=\footnotesize \let\endcodesize=\endfootnotesize \def\RR{\ensuremath{\mathbb{R}}} \def\NN{\ensuremath{\mathbb{N}}} \def\ZZ{\ensuremath{\mathbb{Z}}} \newcommand{\txt}[1]{\texttt{#1}} \newcommand{\CLASS}[1]{\texttt{#1}} \newcommand{\PACK}[1]{\texttt{#1}} \newcommand{\iPACK}[1]{\texttt{ilog.#1}} \newcommand{\lPACK}[1]{\texttt{language.#1}} \newcommand{\dPACK}[1]{\texttt{design.#1}} \newcommand{\kPACK}[1]{\texttt{kernel.#1}} \newcommand{\tPACK}[1]{\texttt{types.#1}} \newcommand{\bsPACK}[1]{\texttt{base.#1}} \newcommand{\bePACK}[1]{\texttt{backend.#1}} \usepackage{amsfonts} \usepackage[centertags]{amsmath} \usepackage{theorem} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\Chapter#1#2{\chapter{#1}\label{#2}} \def\CHAPTER#1{\chapter{#1}\label{#1}} \def\Section#1#2{\section{#1}\label{#2}} \def\SECTION#1{\section{#1}\label{#1}} \def\Subsection#1#2{\subsection{#1}\label{#2}} \def\SUBSECTION#1{\subsection{#1}\label{#1}} \def\Subsubsection#1#2{\subsubsection{#1}\label{#2}} \def\SUBSUBSECTION#1{\subsubsection{#1}\label{#1}} \def\Itemize{\itemize\itemsep0pt} \let\endItemize=\enditemize \def\Enumerate{\enumerate\itemsep0pt} \let\endEnumerate=\endenumerate \def\SYNTAX{\medskip\noindent\textsc{{\small\black abstract syntax}}\par} \def\SEMANTICS{\medskip\noindent\textsc{{\small\black operational semantics}}\par} \def\TYPING{\medskip\noindent\textsc{{\small\black typing rule}}\par} \def\COMPILING{\medskip\noindent\textsc{{\small\black compiling rule}}\par} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\ib#1{\textbf{\textit{#1}}} \usepackage{pstricks} \usepackage{pst-node} \usepackage{fancybox} \def\khstyle{\kkw{blue}} \def\shstyle{\skw{magenta}} \long\def\kw#1{\textbf{#1}} \long\def\kkw#1{\kw{\blue #1}} \long\def\skw#1{\kw{\magenta #1}} \long\def\nkw#1{{\black #1}} \def\nterm#1{\ensuremath{\langle\mbox{\textit{#1}}\rangle}} \def\term#1{\textsc{#1}} \long\def\desugar#1#2#3{\begin{equation}\label{desugar-#1} \skw{#2} \;\leadsto\; \kkw{#3}. \end{equation}} \def\order#1{\ensuremath{\mathbf{order}(#1)}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\numberwithin{equation}{section} %\numberwithin{equation}{chapter} \def\formula{\equation\split} \def\endformula{\endsplit\endequation} \theoremheaderfont{\scshape} \newtheorem{theorem}{Theorem}[section] \newtheorem{definition}{Definition}[section] \newtheorem{corollary}{Corollary}[section] \theorembodyfont{\normalfont\slshape} \newtheorem{example}{Example}[section] \newtheorem{exercise}{Exercise}[section] \def\proof{\small\textsc{Proof\ }} \def\endproof{\par} \def\empty{\emptyset} \def\dnt#1{\ensuremath{[\![#1]\!]}} \def\dnti#1#2{\ensuremath{[\![#1]\!]_{#2}}} \def\dntv#1#2{\ensuremath{[\![#1]\!]^{#2}}} \def\dntiv#1#2#3{\ensuremath{[\![#1]\!]_{#2}^{#3}}} \def\noarg{\,\_\:} \def\map{\rightarrow} \def\MAP{\;\leadsto\;} \def\rewrite{\;\Longrightarrow\;} \def\eqv{\leftrightarrow} \def\funtype#1#2{\ensuremath{#1\TYPE{\;\rightarrow\;}#2}} \def\FUNTYPE#1#2{\TYPE{#1\;\rightarrow\;#2}} \def\hastype#1#2{\ensuremath{\KRNL{#1}\;:\;\TYPE{#2}}} \def\judgment#1#2#3{\ensuremath{#1\;\vdash\;\KRNL{#2}\;:\;\TYPE{#3}}} \def\gammajudgment#1#2{\ensuremath{\Gamma\;\vdash\;\KRNL{#1}\;:\TYPE{\;#2}}} \def\ie{{\em i.e.}} \def\nb{{\em N.B.}} \def\eg{{\em e.g.}} \def\vs{{\em vs.}} \def\etc{{\em etc.}} \def\viz{{\em viz.}} \def\aka{{\em a.k.a.}} \def\c#1{\ensuremath{{\mathcal #1}}} \def\g#1{\ensuremath{\mathfrak{#1}}} \def\tt#1{\texttt{#1}} \def\T{\ensuremath{\g{T}_{\Sigma}}} \def\NN{\ensuremath{{\mathbb{N}}}} \def\WW{\ensuremath{{\mathbb{W}}}} \def\TSV{\ensuremath{\c{T}_{\Sigma,\c{V}}}} \def\TS{\ensuremath{\c{T}_{\Sigma}}} \def\GS{\ensuremath{\c{S}_{\Sigma}}} \def\setnotesmacros{ \gdef\A{\g{A}} \gdef\B{{\cal B}} \gdef\C{\g{C}} \gdef\E{\c{E}} \gdef\I{\g{I}} \gdef\J{\g{J}} \gdef\D{\c{D}} \gdef\V{\c{V}} \gdef\W{\c{W}} \gdef\gW{\g{W}} \gdef\Q{\g{Q}} \gdef\N{\g{N}} \gdef\P{\g{P}} \gdef\G{\g{G}} \gdef\TT{\g{T}} \gdef\powerset##1{\ensuremath{\g{2}^{##1}}} \gdef\unitset{\g{1}} \gdef\unitlang{\iota} \gdef\pr(##1,##2){\ensuremath{\langle ##1,##2\rangle}} \gdef\ID(##1){\ensuremath{1\!\!1_{##1}}} %\gdef\ID(##1){\ensuremath{\mbox{\textbf{\large1)}_{##1}}} \gdef\freevars(##1){\ensuremath{\mathbf{FV}(##1)}} \gdef\vars(##1){\ensuremath{\mathbf{V}(##1)}} \gdef\setmin{-} \gdef\tauteq{\vdash\!\dashv} \gdef\subst[##1/##2]{^{##2\leftarrow ##1}} \gdef\tsubst##1##2{[\KRNL{##1}:\TYPE{##2}]} \gdef\exitable##1{_{\KRNL{\aleph}\leftarrow\KRNL{##1}}} \def\ext[##1/##2]{^{##2\rightarrow ##1}} } \setnotesmacros \def\reducesto#1{\ensuremath{\stackrel{#1}{\rightarrow}}} \def\reducestostar#1{\ensuremath{\stackrel{#1}{\rightarrow}^*}} \def\reducestoinv#1{\ensuremath{\stackrel{#1}{\rightarrow}^{-1}}} \def\cnv#1{\ensuremath{\stackrel{#1}{\simeq}}} \def\bool{\g{boolean}} \def\int{\g{int}} \def\real{\g{real}} %\def\char{\g{char}} \def\true{\g{true}} \def\void{\g{void}} \def\Void{\g{Void}} \def\Null{\g{null}} \def\NULL#1{\g{null}\ensuremath{_\TYPE{#1}}} \def\false{\g{false}} \def\ite#1#2#3{\g{if}\;#1\;\g{then}\;#2\;\g{else}\;#3} \def\Quote(#1){\app{\g{quote}}{#1}} \def\eval(#1){\app{\g{eval}}{#1}} \def\rec{\g{rec}} \def\fst{\g{fst}} \def\snd{\g{snd}} \def\LT{\g{lt}} \def\GT{\g{gt}} \def\EQ{\g{eq}} \def\nil{\g{nil}} \def\cons{\g{pair}} \def\switch(#1){\app{\g{switch}}{#1}} \def\plus{\g{plus}} \def\mult{\g{times}} \def\succ{\g{succ}} \def\pred{\g{pred}} \def\add{\g{add}} \def\mul{\g{mul}} \def\dif{\g{dif}} \def\div{\g{div}} \def\con{\g{and}} \def\dis{\g{or}} \def\nt{\g{not}} \def\iszero{\g{is\_zero}} \def\cn#1{\underline{#1}} \def\program#1#2{ \def\k##1{\mathbf{##1}} \def\w##1{\mathit{##1}} \def\t##1{\textsc{##1}} \def\K##1{\mathbf{##1}\;\;} \def\W##1{\mathit{##1}\;\;} \def\T##1{\textsc{##1}\;\;} \def\+##1{\hskip1em\\ \hskip1em\hskip##1em} \def\<{\leftarrow} \def\LABEL{#1}\def\CAPTION{#2} \begin{figure} \begin{center}%\small% $\begin{array}{|l|}\hline \\ \hskip1em} \def\endprogram{\\ \\ \hline\end{array}$ \end{center}\caption{\CAPTION}\vskip.8ex\label{\LABEL} \end{figure}} \newcounter{algolistcounter} % \def\algolist{\list{$(u.\thealgolistcounter)$}{\def\makelabel##1{\hfil##1} \usecounter{algolistcounter} \rightmargin0pt \leftmargin3.5em \labelwidth3em \labelsep0.5em \listparindent\parindent \topsep7pt \parsep0pt \itemsep1ex}} \let\endalgolist=\endlist \newcounter{bnflistcounter} % \def\bnflist{\displaymath\stepcounter{bnflistcounter} \begin{array}{l@{\;\;}l@{\;\;::=\;\;}l}} \def\endbnflist{\end{array}\enddisplaymath} \newcounter{bnfrulecounter} % \def\bnfrule#1#2{\refstepcounter{bnfrulecounter}[\thebnfrulecounter] & \textit{#1} & \textit{#2} \\ [1.2ex]} \def\vect#1{\,\vec{#1}\:} \def\dom#1{\ensuremath{\mathbf{dom}(#1)}} \def\ran#1{\ensuremath{\mathbf{ran}(#1)}} \def\Ext#1{\ensuremath{\mathbf{ext}(#1)}} \def\mgu#1{\ensuremath{\textsc{mgu}(#1)}} \def\?{\mbox{\texttt{?-}}} \def\pif{\;\mbox{\texttt{:-}}\;} \newlength{\underscorelen} \def\underscore#1{\settowidth{\underscorelen}{#1}#1\hspace{-\underscorelen}% \raisebox{-1.5pt}{\vrule height .2pt width\underscorelen}} \newcounter{globenumcounter} % \def\globenum{\stepcounter{globenumcounter} \list{$\theglobenumcounter.$}{\def\makelabel##1{\hfil##1} \rightmargin0pt \leftmargin3.5em \labelwidth3em \labelsep0.5em \listparindent\parindent \topsep7pt \parsep0pt \itemsep1ex}} \let\endglobenum=\endlist %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\ae{\textsc{ae}} \def\lbd{{\ensuremath\lambda}} \def\app#1#2{#1\;#2} \def\abs#1#2{\lambda#1.\,#2} \def\context[#1]{\ensuremath{\mathbf{\bigl\langle}#1\mathbf{\bigr\rangle}}} \def\S{\ensuremath{\mathbf{S}}} \def\K{\ensuremath{\mathbf{K}}} \def\Id{\ensuremath{\mathbf{I}}} \def\Y{\ensuremath{\mathbf{Y}}} \def\F{\ensuremath{\mathbf{F}}} \def\Fact{\textbf{Fact}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \renewcommand\approx{\ensuremath{\sqsubseteq}} \renewcommand\sup{\ensuremath{\sqcup}} \renewcommand\inf{\ensuremath{\sqcap}} \newcommand\lat[4]{\ensuremath{\langle #1,#2,#3,#4 \rangle}} \newcommand\lats[5]{\ensuremath{\langle #2_{#1},#3_{#1},#4_{#1},#5_{#1} \rangle}} \newcommand\llat[5]{\ensuremath{#1 = \langle #2^{#1},#3^{#1},#4^{#1},#5^{#1} \rangle}} \newcommand\llats[6]{\ensuremath{#2_{#1} = \langle #3_{#1}^{#2},#4_{#1}^{#2},#5_{#1}^{#2},#6_{#1}^{#2} \rangle}} \newcommand\Lat{\lat{D}{\approx}{\sup}{\inf}} \newcommand\Latone{\lats{1}} \newcommand\Lattwo{\lats{2}} \newcommand\Latn{\lats{n}} \newcommand\Llat{{\llat{\L}{D}{\approx}{\sup}{\inf}}} \newcommand\Llatone{\llats{1}} \newcommand\Llattwo{\llats{2}} \newcommand\Llatn{\llats{n}} \renewcommand\L{\ensuremath{\mathcal{L}}} \def\hal{\textsc{hal}} \def\secd{\textsc{secd}} \def\fam{\textsc{fam}} \def\cam{\textsc{cam}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Some oft used names... \def\hak{Hassan A\"{\i}t-Kaci} \def\hassan{Hassan} \def\ak{A\"{\i}t-Kaci} \def\ilog{\textsc{Ilog}} \def\ilogsa{\textsc{Ilog}, S.A.} \def\opl{\textsc{Opl}} \def\ngo{\textsc{Ngo}} \def\NGO{\ensuremath{{\cal NGO}}} \def\hakl{\textsc{\texttt{hak\_ll}}} \def\jacc{\g{Jacc}} \def\yacc{\textsc{\texttt{Yacc}}} \def\lalr{\texttt{\textsc{lalr}}} \def\LALR(1){\texttt{\textsc{lalr(1)}}} \def\borneo{\g{Borneo}} \def\prolog{\textsc{\texttt{Prolog}}} \def\life{\textsc{\texttt{Life}}} \def\wildlife{\textsc{\texttt{Wild\_Life}}} \def\yacc{\texttt{yacc}} \def\jdk{\textsc{jdk}} \def\java{\textsc{Java}} \def\pizza{\textsc{pizza}} \def\gj{\textsc{gj}} \def\pajamas{\textsc{pajamas}} \def\wam{\textsc{wam}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\Mbox{\mbox} \def\address(#1){\g{address}(#1)} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % basic SECD machine instructions: \def\apply{\g{apply}} \def\load{\g{load}} \def\lpos{\g{load\_position}} \def\return{\g{return}} \long\def\ldcl(#1){\g{load\_closure}\map\hskip-\arraycolsep\begin{array}[t]{l}#1\end{array}} \def\Ldcl{\g{load\_closure}} \def\transitions{\begin{array}{|llll@{\;\;\leadsto\;\;}llll|} \hline\stickup{3ex}} \def\endtransitions{\stickdown{2ex} \\ \hline \end{array}} %\def\trans#1#2#3#4#5#6#7#8{[\;#1,,,\;]&[\;#5,,,\;]} \newcommand{\trans}[8]{[\;#1,,,\;]&[\;#5,,,\;]} \def\state(#1,#2,#3,#4){\ensuremath{\mathbf{\bigl[}#1,#2,#3,#4\mathbf{\bigr]}}} % \def\store{\g{store}} \newcommand{\store}{\g{store}} % \def\clos{\g{closure}} \newcommand{\clos}{\g{closure}} % \def\code{\g{code}} \newcommand{\code}{\g{code}} % \def\ic{\g{ic}} \newcommand{\ic}{\g{ic}} % \def\Stack#1{\hskip-\arraycolsep\begin{array}[t]{l}#1\end{array}} \newcommand{\Stack}[1]{\hskip-\arraycolsep\begin{array}[t]{l}#1\end{array}} % \def\Env#1{\redefinecomma\hskip-\arraycolsep\begin{array}[t]{r@{\ :\ }l} % #1 \\ % \end{array}} \newcommand{\Env}[1]{\redefinecomma\hskip-\arraycolsep\begin{array}[t]{r@{\ :\ }l} #1 \\ \end{array}} % \def\redefinecomma{\def\,{\\ }} \newcommand{\redefinecomma}{\renewcommand{\,}{\\ }} \def\Dump(#1,#2,#3,#4){\langle #1, #2, #3, #4\rangle} \def\secdtable{\begin{center}\footnotesize$\begin{array}{|l|l|r@{:\hskip1em}l|l|} \textbf{\small Stack}& \textbf{\small Environment}& \ic& \textbf{\small Code}& \textbf{\small Dump}} \def\endsecdtable{\stickdown{2ex} \\ \hline\end{array}$\end{center}} \def\SECD#1#2#3#4{\\ \hline \stickup{3.5ex}\stickdown{4ex}#1 & #2 & #3 & #4} \def\stickup#1{\vrule width 0pt height #1 depth 0pt} \def\stickdown#1{\vrule width 0pt height 0pt depth #1} % \def\lp{\textsc{lp}} \newcommand{\lp}{\textsc{lp}} % \def\clp{\textsc{csp}} \newcommand{\csp}{\textsc{csp}} % \def\clp{\textsc{clp}} \newcommand{\clp}{\textsc{clp}} % \def\osf{\textsc{osf}} \newcommand{\osf}{\textsc{osf}} % \def\scoop{\textsc{scoop}} \newcommand{\scoop}{\textsc{scoop}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\gradebox#1{\marginpar{\begin{tabular}{|c|} \hline \stickup{3ex}\stickdown{2ex}\underline{\mbox{\hskip2em}}$/#1$ \\ \hline \end{tabular}}} \def\Gradebox#1{\marginpar{\begin{tabular}{||c||} \hline\hline \stickup{3ex}\stickdown{2ex}\underline{\mbox{\hskip2em}}$/#1$ \\ \hline\hline \end{tabular}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcounter{tfcounter} \def\tflist{\setcounter{tfcounter}{0}\begin{tabular}{ll|c|c|}\cline{3-4} & & \true & \false} \def\endtflist{\\ \cline{3-4}\end{tabular}} \long\def\tfitem#1{\\ \cline{3-4}\stepcounter{tfcounter}\stickup{3ex}\stickdown{2ex} [\thetfcounter]: & \parbox[t]{.6\textwidth}{#1.} & & } \newcounter{qcounter} \newcounter{sqcounter} \def\question#1#2{\setcounter{sqcounter}{0}\stepcounter{qcounter}\par {\Large\bf Question \theqcounter\space:}(\textit{#1 points = #2 minutes})\Gradebox{#1}\\ [2ex]} \def\endquestion{\par} \def\subquestion#1#2{\stepcounter{sqcounter}\par {\large\bf \theqcounter.\thesqcounter\space}(\textit{#1 points = #2 minutes})% \gradebox{#1}\\ [2ex]}\let\endsubquestion=\endquestion \def\Question#1#2{\newpage\question{#1}{#2}}\let\endQuestion=\endquestion \def\Subquestion#1#2{\newpage\subquestion{#1}{#2}}\let\endSubquestion=\endquestion \def\answer#1{\par\parbox{\textwidth}{\vskip#1}\hrule\bigskip} % for grammars \def\bnfnt#1{\ensuremath{\langle\mbox{\textit{#1}}\rangle}} \def\bnft#1{\mbox{\textsc{#1}}} \def\bnflit#1{\mbox{`\texttt{#1}'}} \def\endBNFrule{.} \def\haklError{\bnfnt{error}} \def\haklSession{\bnfnt{program}} \def\haklExpressions{\bnfnt{expressions}} \def\haklExpression{\bnfnt{expression}} \def\haklApplicatExp{\bnfnt{applicative\_expression}} \def\haklDefinition{\bnfnt{definition}} \def\haklStructure{\bnfnt{structure}} \def\haklParameters{\bnfnt{parameters}} \def\haklAbstraction{\bnfnt{abstraction}} \def\haklApplication{\bnfnt{application}} \def\haklTerm{\bnfnt{term}} \def\haklParameter{\bnfnt{parameter}} \def\haklTerms{\bnfnt{terms}} \def\haklParameters{\bnfnt{parameters}} \def\haklList{\bnfnt{list}} \def\haklParamList{\bnfnt{parameter\_list}} \def\haklListcontents{\bnfnt{listcontents}} \def\haklParamListContents{\bnfnt{parameter\_list\_contents}} \def\haklCommalist{\bnfnt{commalist}} \def\haklParamCommalist{\bnfnt{parameter\_comma\_list}} \def\haklSubterms{\bnfnt{subterms}} \def\haklDynop{\bnfnt{operator}} \def\haklPreDynop{\bnft{\_operator}} \def\haklInDynop{\bnft{\_operator\_}} \def\haklPostDynop{\bnft{operator\_}} \def\haklExit{\bnfnt{exit}} \def\haklLAMBDA{\bnft{lambda}} \def\haklVARIABLE{\bnft{variable}} \def\haklSYMBOL{\bnft{symbol}} \def\haklNUMBER{\bnft{number}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % From ../prelim/main.mac \renewcommand{\c}[1]{\ensuremath{{\mathcal #1}}} \renewcommand{\t}[1]{\ensuremath{\mathtt{#1}}} \renewcommand{\b}[1]{\ensuremath{\mathbf{#1}}} \newcommand{\m}[1]{\ensuremath{\mathbb{#1}}} %\newcommand{\g}[1]{\ensuremath{\mathfrak{#1}}} % Constants: %\newcommand{\true}{\g{true}} %\newcommand{\false}{\g{false}} % sets: %\newcommand{\NN}{\m{N}} \newcommand{\BB}{\m{B}} %\newcommand{\C}{\b{C}} %\newcommand{\V}{\b{V}} %\newcommand{\T}{\b{T}} %\newcommand{\OP}{\b{O}} \newcommand{\BT}{\c{B}} \newcommand{\VT}{\c{V}} %\newcommand{\TT}{\c{T}} \newcommand{\MON}[3]{\ensuremath{\langle #1,#2,#3\rangle}} \newcommand{\Mon}[2]{\ensuremath{\langle #1,#2\rangle}} \newcommand{\Monoid}[1]{\Mon{#1}{\ID(#1)}} % lambda terms and types: %\newcommand{\abs}[2]{\lambda #1.#2} %\newcommand{\app}[2]{#1\;#2} %\newcommand{\arr}[2]{#1\rightarrow #2} %\newcommand{\pr}[2]{\langle #1,#2\rangle} \newcommand{\tp}[2]{\langle #1, \cdots, #2\rangle} \newcommand{\pj}[2]{#1.#2} %\newcommand{\ite}[3]{\g{if}\;#1\;\g{then}\;#2\;\g{else}\;#3} \newcommand{\fix}{\g{fix}} \newcommand{\op}{\g{op}} \newcommand{\integer}{\t{int}} %\newcommand{\bool}{\t{bool}} \newcommand{\gives}{\;\longrightarrow\;} \newcommand{\from}{\;\leftarrow\;} %\newcommand{\subst}[3]{#3[#1/#2]} % kernel expressions: \newcommand{\KRNL}[1]{\ensuremath{{\blue #1}}} \newcommand{\Constant}[1]{\KRNL{\g{{#1}}}} \newcommand{\Abstraction}[2]{\KRNL{\g{function}~#1\;\cdot\;#2}} \newcommand{\Application}[2]{\KRNL{#1(#2)}} \newcommand{\Local}[1]{\KRNL{\tt{#1}}} \newcommand{\Global}[1]{\KRNL{\tt{#1}}} \newcommand{\IfThenElse}[3]{\KRNL{\g{if}\;#1\;\g{then}\;#2\;\g{else}\;#3}} \newcommand{\AndOr}[2]{\KRNL{#1\;\g{and}/\g{or}\;#2}} \newcommand{\AND}[2]{\KRNL{#1\;\AndOp\;#2}} \newcommand{\AndOp}{\KRNL{\g{and}}} \newcommand{\OR}[2]{\KRNL{#1\;\OrOp\;#2}} \newcommand{\OrOp}{\KRNL{\g{or}}} \newcommand{\Max}[2]{\KRNL{#1\;\MaxOp\;#2}} \newcommand{\MaxOp}{\KRNL{\g{max}}} \newcommand{\Min}[2]{\KRNL{#1\;\MinOp\;#2}} \newcommand{\MinOp}{\KRNL{\g{min}}} \newcommand{\Sequence}[2]{\KRNL{\{\;#1;\;\dots;#2\;\}}} \newcommand{\Let}[2]{\KRNL{\g{let}\;#1\;\g{in}\;#2}} \newcommand{\Loop}[2]{\KRNL{\g{while}\;#1\;\g{do}\;#2}} \newcommand{\ExitWithValue}[1]{\KRNL{\g{exit}\;\g{with}\;#1}} \newcommand{\Definition}{} \newcommand{\Parameter}{} \newcommand{\Assignment}{} \newcommand{\NewObject}{} \newcommand{\FieldUpdate}{} \newcommand{\NewArray}{} \newcommand{\ArraySlot}{} \newcommand{\ArraySlotUpdate}{} \newcommand{\Tuple}[1]{\KRNL{\langle#1\rangle}} \newcommand{\NamedTuple}{} %\newcommand[2]{\TupleProjection}{\KRNL{#1\mathtt{\atsign}#2}} \def\TupleProjection#1#2{\ensuremath{\KRNL{#1\mathtt{\atsign}#2}}} \newcommand{\TupleUpdate}{} \newcommand{\Dummy}{} \newcommand{\Homomorphism}[4]{\KRNL{\g{hom}_{#3}^{#4}[#2](#1)}} \newcommand{\FilteredHomomorphism}[5]{\KRNL{\g{fhom}_{#3}^{#4\;:\;#5}[#2](#1)}} \def\Project#1{\KRNL{\g{project}}_{#1}} \def\atsign{\makeatletter@\makeatother} \newcommand{\New}{\KRNL{\g{new}}} \newcommand{\Def}{\KRNL{\g{def}}} \newcommand{\Class}{\KRNL{\g{class}}} \newcommand{\Method}{\KRNL{\g{method}}} \newcommand{\This}{\KRNL{\g{this}}} \newcommand{\Comprehension}[3]{\KRNL{\Mon{#1}{\ID(#1)}\{#2\;|\;#3\}}} \newcommand{\IN}[2]{\ensuremath{#1\;\leftarrow\;#2}} % type expressions: \newcommand{\TYPE}[1]{\ensuremath{{\red #1}}} %\newcommand{\TYPE}[1]{{\black #1}} \newcommand{\VOID}{\TYPE{\g{Void}}} \newcommand{\BOOL}{\TYPE{\g{Boolean}}} \newcommand{\INT}{\TYPE{\g{Int}}} \newcommand{\REAL}{\TYPE{\g{Real}}} \newcommand{\CHAR}{\TYPE{\g{Char}}} \newcommand{\STRING}{\TYPE{\g{String}}} \newcommand{\basetype}{\g{\basetype}} % Typing rules: \newcommand{\COND}[1]{\mbox{\small\meta{if\/}\hskip.7em}#1} \newcommand{\typerule}[2]{\ensuremath{\displaystyle\frac{#1}{#2}}} \newcommand{\ctyperule}[3]{\ensuremath{\displaystyle\frac{#1}{#2}\;\;\COND{#3}}} \newcommand{\typeaxiom}[1]{\typerule{}{#1}} \newcommand{\ctypeaxiom}[2]{\ctyperule{}{#1}{#2}} \newcommand{\sequent}[3]{#1\;\vdash\;\KRNL{#2} : \TYPE{#3}} % Compiling rules: \newcommand{\DNT}[1]{\KRNL{\dnt{#1}}} \newcommand{\TDNT}[1]{\TYPE{\dnt{#1}}} \newcommand{\meta}[1]{{\green\textbf{\texttt{\textit{#1}}}}} \newcommand{\LAB}[1]{{\green\texttt{\textit{#1}}}} \newcommand{\compile}[1]{\mbox{\magenta{\footnotesize\g{compile}}$[\![\KRNL{#1}]\!]$}} \newcommand{\compilerule}[2]{\ensuremath{\begin{array}{l@{\;=\;}l} \compile{#1} & \begin{array}[t]{rl} #2 \end{array} \end{array}}} % Meta: \newcommand{\META}[1]{{\green#1}} \newcommand{\Mangle}[1]{\ensuremath{\META{\g{mangle}(#1)}}} \newcommand{\Args}[1]{\ensuremath{\META{\g{args}(#1)}}} % Misc.: \newcommand{\type}{\b{type}} \newcommand{\eqd}{\ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}} % Monoids: \newcommand{\set}{\t{set}} \newcommand{\bag}{\t{bag}} \newcommand{\lst}{\t{list}} \newcommand{\conc}{\ensuremath{\!+\!\!+}} \newcommand{\Z}[1]{\g{z}_{#1}} \newcommand{\U}[1]{\g{u}_{#1}} \newcommand{\Ty}[1]{\g{T}_{#1}} \newcommand{\Co}[1]{\g{C}_{#1}} %\newcommand{\E}[1]{\Theta_{#1}} \newcommand{\mset}[1]{\{\!\!\{#1\}\!\!\}} \newcommand{\eset}{\{\}} \newcommand{\elst}{[]} \newcommand{\ebag}{\{\!\!\{\}\!\!\}} \newcommand{\HOM}[2]{\ensuremath{\g{hom}_{#1}^{#2}}} \newcommand{\subeq}[2]{\ensuremath{\E{#1}\subseteq\E{#2}}} % Comprehensions: \newcommand{\comp}[3]{\ensuremath{#1\{#2\;[\!]\;#3\}}} \newcommand{\COMP}[2]{\ensuremath{\{#1\;|\;#2\}}} \newcommand{\setcomp}[2]{\ensuremath{\{#1\;[\!]\;#2\}}} \newcommand{\Hom}[3]{\ensuremath{\g{hom}_{#3}^{\ID(#3)}[#2](#1)}} \renewcommand{\Join}{\vartriangleright\!\!\vartriangleleft} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \makeatletter \def\ClassNode{\@ifnextchar[{\oClassNode}{\xClassNode}} \def\oClassNode[#1]#2{\@ClassNode{#1}{{\black#2}}} \def\xClassNode#1{\@ClassNode{#1}{{\black#1}}} \def\@ClassNode{\ovalnode*[bordercolor=cyan, border=1pt, fillcolor=yellow]} \def\CNODE#1{\ClassNode[#1]{\CLABEL{#1}}} \def\CLABEL#1{\makebox[4em][c]{\scriptsize\textbf{#1}}} % Extends arrows \def\Extends#1#2{\ncline[doubleline=true,doublesep=2pt,doublecolor=yellow,linecolor=cyan]{cc->}{#1}{#2}} % HasProp arrows \def\HasProp#1#2#3{\ncline{->}{#1}{#2}\aput{:U}{#3}} \def\HasVProp#1#2#3{\ncline{->}{#1}{#2}\aput{:U}{\rotateleft{#3}}} % Abstract classes \def\AbsClassNode{\@ifnextchar[{\oAbsClassNode}{\xAbsClassNode}} \def\oAbsClassNode[#1]#2{\@AbsClassNode{#1}{{\black#2}}} \def\xAbsClassNode#1{\@AbsClassNode{#1}{{\black#1}}} \def\@AbsClassNode{\ovalnode*[bordercolor=cyan, border=1pt, fillcolor=cream]} \def\ACNODE#1{\AbsClassNode[#1]{\CLABEL{#1}}} % Some colors \newrgbcolor{cream}{1 1 .5} \makeatother %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\id}[1]{\mbox{\texttt{\black #1}}} \newcommand{\qid}[2]{\id{#1}\g{::}\id{#2}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%