Permalink
Browse files

added some docs

  • Loading branch information...
1 parent 9952cb4 commit 3dbb5c67a8e48e622b6a593e2f829e3ea36e1aa5 @rubendg rubendg committed Jul 8, 2011
Showing with 31 additions and 62 deletions.
  1. +31 −62 doc/main.tex
View
@@ -13,6 +13,7 @@
\usepackage{array}
\usepackage{bussproofs}
\usepackage{latexsym}
+\usepackage{verbatim}
% things for the semantic package
\reservestyle{\command}{\textbf}
@@ -117,7 +118,9 @@ \subsection{Type System}
Our type system has variables, arrows, and type environments, as well as
annotations, which is what makes it different from a normal polymorphic type
system. Table \ref{tab:typingelems} and \ref{tab:typing} show the elements of
-the type system.
+the type system. In the var and let/letrec case \emph{inst} and \emph{gen} are mentioned.
+Their definition is identical to the ones found in literature on the standard
+Hindley Milner let-polymorphic type system. The final syntax-directed type system is given in table \ref{tab:typing-rules}.
\begin{table}
\begin{centering}
@@ -149,11 +152,6 @@ \subsection{Type System}
\end{centering}
\end{table}
-Next a list of typing judgements will be given. This constitutes the final type
-system. %See weijers fig 5.3 for a reference.
-
-These rules are formulated in a syntax-directed fashion.
-
\begin{table}
\begin{centering}
\begin{tabular}{ll}
@@ -346,57 +344,6 @@ \subsection{Natural semantics}
\end{centering}
\end{table}
-\subsection{Control Flow Analysis}
-
-We have the usual set of rules including, for example, \emph{cfa-var} or
-\emph{cfa-let}, which has been extended to support lists, see \emph{cfa-nil}
-and \emph{cfa-cons}, the rules specifying list-typing, Table
-\ref{tab:cfa-rules}. CFA judgements look like {$\widehat{\Gamma}\:\vdash_{CFA}
-t : \widehat{\sigma}$}, meaning that some term $t$ has inferred type
-$\widehat{\sigma}$ in context $\widehat{\Gamma}$. See Table 5.2 in \cite{nnh}
-for reference.
-
-
-\begin{table}
- \begin{centering}
- \begin{tabular}{ll}
- \hline
- $ [$\emph{cfa-var}$] $& \inference{\widehat{\Gamma}(x) = \widehat{\sigma}}
-{\widehat{\Gamma} |-_{CFA} x : \widehat{\sigma}} \\
-~&~\\
-$[$\emph{cfa-let}$] $& \inference{\widehat{\Gamma} |-_{CFA} t_1:\widehat{\sigma}_1
-& \widehat{\Gamma}[x \mapsto \widehat{\sigma}_1] |-_{CFA} t_2 : \widehat{\tau}}
-{\widehat{\Gamma} |-_{CFA}\: \<let>\: x = t_1\: \<in>\: t_2 : \widehat{\tau}} \\
-~&~\\
-$[$\emph{cfa-nil}$] $&
-\inference{}
-{\widehat{\Gamma} |-_{CFA} [\,] : [\widehat{\sigma}]} \\
-~&~\\
-$[$\emph{cfa-cons}$] $& \inference{\widehat{\Gamma} |-_{CFA} t_1:\widehat{\sigma}
- \widehat{\Gamma}|-_{CFA} t_2 : [\widehat{\sigma}]}
-{\widehat{\Gamma} |-_{CFA} t_1 \<:> t_2 : [\widehat{\sigma}]} \\
-~&~\\
-% $[$\emph{cfa-pair}$] $& \inference{\widehat{\Gamma} |-_{CFA} t_1 : \widehat{\tau}_1 & \widehat{\Gamma} |-_{CFA} t_2 : \widehat{\tau}_2 }
-% {\widehat{\Gamma} |-_{CFA} (t_1,t_2) : \widehat{\tau}_1 \times^\varphi \widehat{\tau}_2 } \\
-% ~&~\\
-% $[$\emph{cfa-case-pair}$] $& \inference{\widehat{\Gamma} |-_{CFA} e_0 : \widehat{\tau}_1 \times^\varphi \widehat{\tau}_2
-% & \widehat{\Gamma} |-_{CFA} e_1 : \widehat{\tau} }
-% {\widehat{\Gamma} |-_{CFA} \:\<case>\: e_0\: \<of>\: (x_1,x_2) \Rightarrow e_1 : \widehat{\tau} } \\
-% ~&~\\
-$[$\emph{cfa-case-nil}$] $& \inference{\widehat{\Gamma} |-_{CFA} e_0 : [\widehat{\tau}_1] & \widehat{\Gamma} |-_{CFA} e_1 : \widehat{\tau} }
-{\widehat{\Gamma} |-_{CFA} \:\<case>\: e_0\: \<of>\: [] \Rightarrow e_1 : \widehat{\tau} }, if $e_0$ empty\\
-~&~\\
-$[$\emph{cfa-case-cons}$] $& \inference{\widehat{\Gamma} |-_{CFA} e_0 : [\widehat{\tau}_1] & \widehat{\Gamma} |-_{CFA} e_1 : \widehat{\tau} }
-{\widehat{\Gamma} |-_{CFA} \:\<case>\: e_0\: \<of>\: (x\<:>xs) \Rightarrow e_1 : \widehat{\tau} }, if $e_0$ nonempty\\
-
- \hline
- \end{tabular}
- \caption{Control Flow Analysis rules. }
- \label{tab:cfa-rules}
- \end{centering}
-\end{table}
-
-
\section{Program design}
The program compiles to a single executable, named \emph{cfa}. It relies heavily
on the UU Attribute Grammar system. Below is a list with filenames and a short
@@ -435,14 +382,36 @@ \section{Features and Limitations}
how to support it in the generalisation and instantiation functions and which
constraints we should generate for it.
-We are currently also missing support for pairs. Instead, we offer support for
- lists. While pairs pose the problem of potentially having two different types in
-the pair, their fixed size would make them relatively straight-forward to implement.
-
-Another limitation is that our case blocks only support exactly two alternatives.
+Our case blocks are limited to support for exactly two alternatives.
Generalising to $n$ alternatives would be quite straight-forward, but was dropped
due to time constraints.
+We currently know of one particular case in which our current implementation fails to
+deliver the expected output:
+
+\begin{verbatim}
+let f = \lambda x -> x + 1 in
+ let g = \lambda y -> y * 2 in
+ let h = \lambda z -> z 3 in
+ h g + h f
+\end{verbatim}
+
+We expect the result of \emph{h} to be:
+
+\begin{verbatim}
+(Nat -> t) ^ {x,y} -> t ^ {z}
+\end{verbatim}
+
+But what we actually get is:
+
+\begin{verbatim}
+ (Nat -> t) ^ {x} -> t ^ {z}
+\end{verbatim}
+
+We could not figure out within the time allotted what was causing this to happen. Although
+we suspect that somewhere a substitution is going wrong or a constraint that should have been
+present isn't generated.
+
\section{Example programs}

0 comments on commit 3dbb5c6

Please sign in to comment.