\documentstyle[12pt]{article}
\input mssymb                                 
\input /jj/kt/tex/fixqmsfonts
\input /jj/kt/tex/laktex
\input /jj/kt/tex/illustrations
\input /var/arvind/idcompiler/macros/prelude


\pagestyle{empty}

\begin{document}


\subsection*{Variable rule}

{\large
\blank
\noindent
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{lllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}, & X_i, &  \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}, & Y_1, & \mv{P1_{i+1,n}}) & = E_1 \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\; \;\;\mid & (\mv{Pm_{1,i-1}}, & Y_m, & \mv{Pm_{i+1,n}}) & = E_m  \} ]\!] =
\end{array}\\
\\
\hspace{1cm}{
\{ \begin{array}[t]{l}
t  =  X_i;\\
t_f  =  {\tt PM}[\![
\begin{array}[t]{llll}
\{ {\sf Case} & (\mv{X_{1,i-1}},\! &\! \mv{X_{i+1,n}} ) & {\sf of} \\
\;\; \;\;\mid & (\mv{P1_{1,i-1}},\! &\! \mv{P1_{i+1,n}}) & = E_1[t/Y_1]_B \\ 
\multicolumn{3}{c}{ \vdots} \\
\;\; \;\;\mid & (\mv{Pm_{1,i-1}},\! & \! \mv{Pm_{i+1,n}}) & = E_m[t/Y_m]_B  \} ]\!]
\end{array}\\
\multicolumn{1}{l}{\;\; {\sf In} \; t_f \; \}}
\end{array}}
\end{array}$\\
}


\pagebreak

\subsection*{Irrefutable pattern rule}

{\large
\blank
\noindent
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{lllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}\;, & X_i\;, & \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}\;, & Y_1\;,& \mv{P1_{i+1,n}} ) & = E_1 \\
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & Y_k\;,& \mv{Pk_{i+1,n}} ) & = E_k \\
\;\;\;\; \mid & (\mv{Pl_{l,i-1}}\; , &  (Yl_1 \;{\sf ,}\; Yl_2) \; , & \mv{Pl_{i+1,n}} ) & = E_l  \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pm_{1,i-1}}\; , & (Ym_1 \;{\sf ,} \; Ym_2) \; , & \mv{Pm_{i+1,n}} ) & = E_m \}]\!] = 
\end{array}  \\
\\
\hspace{1cm}{\begin{array}[t]{lll}
\{ t_1,t_2 & = & {\sf Detuple_2} \; (X_i);\\
\;\; t & = & X_i;\\
\;\;t_f & = & {\tt PM}[\![ \begin{array}[t]{llllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}\;, & t_1 \;, & t_2 \; , & \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}\;, & t_{1,1}\;,& t_{1,2}\;,& \mv{P1_{i+1,n}} ) & = E_1 [t / Y_1]_B \\
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & t_{k,1}\;,& t_{k,2}\;,& \mv{Pk_{i+1,n}} ) & = E_k [t / Y_k ]_B \\
\;\;\;\; \mid & (\mv{Pl_{l,i-1}}\; , &  Yl_1 \;,&  Yl_2 \; , & \mv{Pl_{i+1,n}} ) & = E_l  \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pm_{1,i-1}}\; , & Ym_1 \;, & \; Ym_2 \; , & \mv{Pm_{i+1,n}} ) & = E_m \}]\!] 
\end{array}  \\
\multicolumn{3}{l}{ \;\;\;\; {\sf In} \; t_f  \} } 
\end{array}}
\end{array}$}

\newpage

\subsection*{Refutable pattern rule}


{\large
\blank
\noindent
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{lllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}\;, & X_i\;, & \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}\;, & {\sf Nil}\;,& \mv{P1_{i+1,n}} ) & = E_1 \\
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & {\sf Nil}\;,& \mv{Pk_{i+1,n}} ) & = E_k \\
\;\;\;\; \mid & (\mv{Pl_{l,i-1}}\; , &  Yl_1 \;{\sf :}\; Yl_2 \; , & \mv{Pl_{i+1,n}} ) & = E_l  \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pm_{1,i-1}}\; , & Ym_1 \;{\sf :} \; Ym_2 \; , & \mv{Pm_{i+1,n}} ) & = E_m \}]\!] = 
\end{array}  \\
\\
 \hspace{1cm}{\begin{array}[t]{lll}
 {\sf List\_case} & (X_i,  &  \\
\;\;\;\;  &  & 
	{\tt PM}[\![  \begin{array}[t]{llll} \{ {\sf Case} &
	(\mv{X_{1,i-1}}\; , &  \mv{X_{i+1,n}} ) & {\sf of} \\
        \;\;\;\; \mid & (\mv{P1_{1,i-1}}\; , & \mv{P1_{i+1,n}} ) & = E_1 \\ 
	\multicolumn{4}{c}{ \vdots} \\
        \;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & \mv{Pk_{i+1,n}} ) & = E_k \} ]\!],
	\end{array}\\
\\
\;\;\;\;  &   &   \{ \begin{array}[t]{l}
         t_h,t_t = {\sf Cons\_1}\;(X_i),\; {\sf Cons\_2} \; (X_i); \\
	 t_f= {\tt PM}[\![  \begin{array}[t]{llllll} \{ {\sf Case} &
	(t_h \;,& t_t\;,  & \mv{X_{1,i-1}}\;, &  \mv{X_{i+1,n}}) & {\sf of} \\
	\;\;\;\; \mid & (Yl_1 \;, & Yl_2\;, &  \mv{Pl_{1,i-1}}\;, & \mv{Pl_{i+1,n}} ) & = E_l \\ 
	\multicolumn{6}{c}{ \vdots} \\
	\;\;\;\; \mid & (Ym_1 \;, & Ym_2\;, &  \mv{Pm_{1,i-1}}\;, & \mv{Pm_{i+1,n}} ) & = E_m  \} ]\!] 
	\end{array}\\
         \;\;\; {\sf In} \; t_f \} \;)
         \end{array} 
\end{array} }  \\
\end{array}$
} \\


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & Y_1 \; {\sf :} \; Y_2   & = E  \} ]\!]
\end{array} & = &  
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & Y_1 \; {\sf :} \; Y_2   & = E  \\
\;\; \;\;\mid & {\sf Nil}   & = {\sf Error} \}   ]\!]
\end{array}
\end{array}$ \\


\blank
\noindent
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & {\sf Nil}  & = E  \} ]\!]
\end{array} & = &  
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & {\sf Nil}   & = E  \\
\;\; \;\;\mid & t_1 \; {\sf :} \; t_2   & = {\sf Error} \}  ]\!]
\end{array}
\end{array}$ \\
}



\newpage


\subsection*{Mixed variable-refutable patterns}

{\large
\blank
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{llllll}
\{ {\sf Case} & (X_1, &   X_2, & X_3 & ) & {\sf of} \\
\;\;\;\; \mid & ({\sf Nil} \;,& Y_{1,1} \; {\sf :} \; Y_{1,2} \; ,  & Y_1 & ) &  = E_1 \\
\;\;\;\; \mid & (Y_{2,1} \; {\sf :} \; Y_{2,2} \; ,  &  Y_2 \;, & {\sf Nil} & ) & = E_2 \\
\;\;\;\; \mid & (Y_3 \; , & {\sf Nil} \; , & Y_{3,1} \; {\sf :} \; Y_{3,2} & ) & =
E_3 \} ]\!] =
\end{array}   \\
\\
\hspace{1cm}{
\{ \begin{array}[t]{lll}
\mv{t_3} & = & \mv{X_3} ;\\
\;\; t_f & = & {\tt PM}[\![ \begin{array}[t]{llllll}
\{ {\sf Case} & (X_1, &   X_2, & X_3 & ) & {\sf of} \\
\;\;\;\; \mid & ({\sf Nil} \;,& Y_{1,1} \; {\sf :} \; Y_{1,2} \; ,  & {\sf Nil} & )  & = E_1[t_3 / Y_1 ]_B \\
\;\;\;\; \mid & ({\sf Nil} \;,& Y_{1,1} \; {\sf :} \; Y_{1,2} \; ,  &
t_{1,1} \; {\sf :} \; t_{1,2} & )  & = E_1[t_3 / Y_1 ]_B \\
\;\;\;\; \mid & (Y_{2,1} \; {\sf :} \; Y_{2,2} \; ,  &  {\sf Nil} \;, & {\sf Nil} & ) & = E_2[t_2 / Y_2 ]_B \\
\;\;\;\; \mid & (Y_{2,1} \; {\sf :} \; Y_{2,2} \; ,  & 
t_{2,1} \; {\sf :} \; t_{2,2} \; , & {\sf Nil} & ) & = E_2[t_2 / Y_2]_B \\
\;\;\;\; \mid & ({\sf Nil} \; , & {\sf Nil} \; , & Y_{3,1} \; {\sf :} \; Y_{3,2} & ) & = E_3[t_1 / Y_3]_B \\
\;\;\;\; \mid & (t_{3,1} \; {\sf :} \; t_{3,2} \;  , & {\sf Nil} \; , & Y_{3,1} \; {\sf :} \; Y_{3,2} & ) & = E_3[t_1 / Y_3]_B \} ]\!] 
\end{array}  \\
\multicolumn{3}{l}{ \;\;\;\; {\sf In} \; t_f  \} } 
\end{array}}
\end{array}$
}\\

\subsection*{Empty variable rule}


{\large
\blank
\noindent
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & () & {\sf of} \\
\;\; \;\;\mid & () & = E_1 \\ 
\multicolumn{3}{c}{ \vdots} \\
\;\; \;\;\mid & () & = E_m  \} ]\!]
\end{array} & = & {\bf \mbox{Compiler Error ``overlapping patterns" } } \\ 
\end{array}$\\


\blank
\noindent
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & () & {\sf of} \\
\;\; \;\;\mid & ()  & = E  \} ]\!]
\end{array} & = & E \\
\end{array}$ \\
}

\end{document}
