code_table.tex

\lstset{language=[Objective]Caml,columns=fixed,basicstyle=\linespread{0.43}\ttfamily\scriptsize,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em}
\begin{table}
   {\scriptsize
  \begin{tabular}{|@{\,}c@{\,}|p{0.54\textwidth}@{}|@{\,}p{0.41\textwidth}@{\,}|}
\hline
    & Code & Inferred type\\
%    \hline
    \hline
    1 &
          \begin{lstlisting}
let basic_inf = fun (y : Int | Bool) ->
  if y is Int then incr y else lnot y\end{lstlisting}
         &\vfill
           $(\Int\to\Int)\land(\Bool\to\Bool)$
    \\\hline
    2 &
\begin{lstlisting}
let any_inf = fun (x : Any) ->
  if x is Int then incr x else
  if x is Bool then lnot x else x
\end{lstlisting} &\vfill
 $(\Int\to\Int)\land(\lnot\Int\to\lnot\Int)\;\land$\newline
 $(\Bool\to\Bool)\land(\lnot(\Int\vee\Bool)\to\lnot(\Int\vee\Bool))$\\
    \hline

    3 &\begin{lstlisting}
let is_int = fun (x : Any) ->
 if x is Int then true else false

let is_bool = fun (x : Any) ->
 if x is Bool then true else false

let is_char = fun (x : Any) ->
 if x is Char then true else false
\end{lstlisting}
           &\smallskip
             $(\Int\to\Keyw{True})\land(\lnot\Int\to\Keyw{False})$\newline
             ~\newline\smallskip
             $(\Bool\to\Keyw{True})\land(\lnot\Bool\to\Keyw{False})$\newline
             ~\newline
             $(\Char\to\Keyw{True})\land(\lnot\Char\to\Keyw{False})$
\\\hline
    4 &
          \begin{lstlisting}
let not_ = fun (x : Any) ->
   if x is True then false else true
 \end{lstlisting} &\vfill
 $(\Keyw{True}\to\Keyw{False})\land(\lnot\Keyw{True}\to\Keyw{True})$\\\hline
    5 &
          \begin{lstlisting}
let or_ = fun (x : Any) -> fun (y: Any) ->
 if x is True then true
 else if y is True then true else false
\end{lstlisting}
 &\smallskip\vfill
   $(\True\to\textsf{Any}\to\True)\land(\textsf{Any}\to\True\to\True)\;\land$\newline
   $(\lnot\True\to\lnot\True\to\False)$
\\\hline
    6 &
          \begin{lstlisting}
let and_ = fun (x : Any) -> fun (y : Any) ->
  if not_ (or_ (not_ x) (not_ y)) is True
  then true else false
\end{lstlisting}
 &\vfill
   $(\True\to((\lnot\True\to\False)\land(\True\to\True))$\newline
   $ \land(\lnot\True\to\textsf{Any}\to\False)$
\\\hline
    7 &
\begin{lstlisting}
let f = fun (x : Any) -> fun (y : Any) ->
  if and_ (is_int x) (is_bool y) is True
  then 1 else
     if or_ (is_char x) (is_int y) is True
     then 2 else 3
\end{lstlisting}&
$(\Int \to (\Int \to 2) \land (\lnot\Int \to 1 \lor 3) \land (\Bool \to 1) \land$\newline
 \hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 3) \land
          (\lnot\Bool \to 2\lor3))$~~$\land$\newline
$(\Char \to (\Int \to 2) \land (\lnot\Int \to 2) \land (\Bool \to 2) \land$\newline
\hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 2) \land
          (\lnot\Bool \to 2))$~~$\land$\newline
$(\lnot(\Int \lor \Char) \to (\Int \to 2) \land
          (\lnot\Int \to 3) \land$\newline
\hspace*{0.2cm}$(\Bool \to 3) \land(\lnot(\Bool \lor \Int) \to 3)
          \land (\lnot\Bool \to 2
                  \lor 3))$\newline
                  $\land \ldots$ (two other redundant cases omitted)
%                   \newline
% $(\lnot\Char \to (\Int \to 2) \land (\lnot\Int \to 1 \lor 3) \land (\Bool \to 1 \lor 3) \land$\newline
% \hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 3) \land
%           (\lnot\Bool \to 2\lor 3)) \land$\newline
%           $(\lnot\Int \to (\Int \to 2) \land (\lnot\Int \to 2
%           \lor 3) \land (\Bool \to 2\lor 3) \land$\newline
%           \hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 2
%           \lor 3) \land (\lnot\Bool \to 2\lor 3))$
\\
& \begin{lstlisting}
let test_1 = f 3 true
let test_2 = f (42,42) 42
let test_3 = f nil nil
\end{lstlisting}&
                  $\p 1$\newline
                  $\p 2$\newline
                  $\p 3$
    \\\hline
    8 &
\begin{lstlisting}
type Document = { nodeType=9 ..}
and Element = { nodeType=1, childNodes=NodeList ..}
and Text = { nodeType=3,
             isElementContentWhiteSpace=Bool ..}
and Node = Document | Element | Text
and NodeList = Nil | (Node, NodeList)

let is_empty_node = fun (x : Node) ->
  if x.nodeType is 9 then false
  else if x.nodeType is 3 then
    x.isElementContentWhiteSpace
  else
  if x.childNodes is Nil then true else false
\end{lstlisting} &\vspace{12mm}
$(\Keyw{Document}\to\False)~\land$\newline
$(\orecord{ \texttt{nodeType}\,{=}\,1, \texttt{childNodes}\,{=}\,\Keyw{Nil} }\to\True) ~\land$\newline
$(\orecord{ \texttt{nodeType}\,{=}\,1,
                   \texttt{childNodes}\,{=}\,(\Keyw{Node},\Keyw{NodeList})
                   }$\newline
                   \hspace*{4.5cm}$\to\False) ~\land$\newline
$(\Keyw{Text}\to\Bool)~\land$\newline (omitted redundant arrows)
    \\\hline
    9 & \begin{lstlisting}
let xor_ = fun (x : Any) -> fun (y : Any) ->
 if and_ (or_ x y) (not_ (and_ x y)) is True
 then true else false
\end{lstlisting} &\vfill
$\True\to((\True\to\False)\land(\lnot\True\to\True))~\land$\newline
$(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$
    \\\hline

 10 & \begin{lstlisting}
(* f, g have type: (Int->Int) & (Any->Bool) *)

let example10 = fun (x : Any) ->
  if (f x, g x) is (Int, Bool) then 1 else 2
\end{lstlisting} &\vfill\medskip\smallskip
$(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
\texttt{Warning: line 4, 39-40: unreachable expression}
    \\\hline
  \end{tabular}
}
\caption{Types inferred by the implementation}
\ifsubmission%
\svvspace{-10mm}
\fi%
\label{tab:implem}
\end{table}