code_table.tex 3.64 KB
 Kim Nguyễn committed Jul 08, 2019 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 \lstset{language=[Objective]Caml,columns=fixed,basicstyle=\ttfamily\scriptsize,aboveskip=-1em,belowskip=-1em,xleftmargin=-0.5em} \begin{table} {\small \begin{tabular}{|@{\,}c@{\,}|p{0.47\textwidth}@{}|@{\,}p{0.47\textwidth}@{\,}|} \hline & Code & Infered 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} & $(\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} & $(\Int\to\Int)\land(\lnot\Int\to\lnot\Int)\land$ $(\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} & $(\Int\to\Keyw{True})\land(\lnot\Int\to\Keyw{False})$\newline ~\newline $(\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} & $(\Keyw{True}\to\Keyw{False})\land(\Keyw{False}\to\Keyw{True})$\\\hline 5 & \begin{lstlisting} let or_ = fun (x : Any) -> if x is True then (fun (y : Any) -> true) else fun (y : Any) -> if y is True then true else false \end{lstlisting} & $(\True\to\Any\to\True)\land(\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} & $(\True\to((\lnot\True\to\False)\land(\True\to\True))$\newline $\land(\lnot\True\to\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))$\newline $\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))$\newline $\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 ommitted) % \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))$ \\\hline & \begin{lstlisting} let test_1 = f 3 true let test_2 = f (42,42) 42 let test_3 = f nil nil \end{lstlisting}& $1$\newline $2$\newline $3$ \\\hline \end{tabular} } \caption{Types inferred by implementation} \label{tab:implem} \end{table}