\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} atom nil 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 is { nodeType=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 11 & \begin{lstlisting} atom null type Object = Null | { prototype = Object ..} type ObjectWithPropertyL = { l = Any ..} | { prototype = ObjectWithPropertyL ..} let has_property_l = fun (o:Object) -> if o is ObjectWithPropertyL then true else false let has_own_property_l = fun (o:Object) -> if o is { l=Any ..} then true else false let get_property_l = fun (self:Object->Any) o -> if has_own_property_l o is True then o.l else if o is Nil then nil else self (o.prototype) \end{lstlisting} &\vfill\medskip\smallskip $(\Keyw{ObjectWithPropertyL}\to\True)$ $\land$ $(\Keyw{X1}\to\False) \texttt{ where}$\newline $\Keyw{X1}\,=\,(\Keyw{Nil}\,|\,\orecord{\texttt{l}\,{=}\,?\Keyw{Empty},\, \texttt{prototype}\,{=}\,\Keyw{X1}})$\newline ~\newline $(\orecord{\Keyw{l}\,=\,\Keyw{Any}, \texttt{prototype}\,=\,\Keyw{Object}}\to\True)$ $\land$\newline $((\Keyw{Nil}\,|\,\orecord{\texttt{l}\,=\,?\Keyw{Empty},\, \texttt{prototype}\,=\,\Keyw{Object}})\to\False)$\newline \newline ~\newline $\Keyw{Object}\to\Keyw{Any}$ \\\hline \end{tabular} } \caption{Types inferred by the implementation} \ifsubmission% \svvspace{-10mm} \fi% \label{tab:implem} \end{table}