code_table2.tex 5.24 KB
 Kim Nguyễn committed May 06, 2021 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 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 \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} (* Assumes: add1 : Int -> Int *) let example1 = fun (x:Any) -> if x is Int then add1 x else 0 \end{lstlisting} & \vfill $\Int \to \Int$ \\\hline 2 & \begin{lstlisting} (* Assumes strlen: String -> Int *) let example2 = fun (x:String|Int) -> if x is Int then add1 x else strlen x \end{lstlisting} & \vfill $(\Int \to \Int) \land (\String \to \Int)$ \\\hline 3 & \begin{lstlisting} let example3 = fun (x: Any) -> if x is (Any \ False) then (x,x) else false \end{lstlisting} & \smallskip $(\False \to \False) \land (\lnot \False \lnot (\lnot \False,\lnot\False))$ \\\hline 4 & \begin{lstlisting} (*Uses is_int from Table 1.3 and or_ from Table 1.5, assumes f : (Int|String) -> Int *) let is_string = fun (x : Any) -> if x is String then true else false let example4 = fun (x : Any) -> if or (is_int x) (is_string x) is True then x else 'A' \end{lstlisting} & \vfill $(\String\to\Keyw{True})\land(\lnot\String\to\Keyw{False})$\newline ~\newline $(\Int \to \Int) \land (\String \to \String) \land$\newline $(\lnot \Int \to (\String \lor \Keyw{'A'})) \land$\newline $(\lnot \String \to (\Int \lor \Keyw{'A'})) \land$\newline $(\lnot(\String \lor \Int) \to \Keyw{'A'})$ \\\hline 5 & \begin{lstlisting} (*Uses and_ from Table 1.6, assumes strlen : String -> Int *) let example5 = fun (x : Any) -> fun (y : Any) -> if and_ (is_int x) (is_string y) is True then add x (strlen y) else 0 \end{lstlisting} & \smallskip\vfill $(\Int \to \String \to \Int) \land (\Int \to \lnot \String \to 0))~\land$\newline $(\lnot \Int \to \String \to 0) \land (\lnot \String \to 0)$ \\\hline 6 & \begin{lstlisting} let example6 = fun (x : Int|String) -> fun (y : Any) -> if and_ (is_int x) (is_string y) is True then add x (strlen y) else strlen x \end{lstlisting} & \vfill Type error for \texttt{strlen x}, \texttt{x} has type $\Int\lor\String$. \\\hline 7 & \begin{lstlisting} let example7 = fun (x : Any) -> fun (y : Any) -> if (if (is_int x) is True then (is_string y) else false) is True then add x (strlen y) else 0 \end{lstlisting} & $(\Int \to \String \to \Int) \land (\Int \to \lnot \String \to 0))~\land$\newline $(\lnot \Int \to \String \to 0) \land (\lnot \String \to 0)$ (identical to example 5) \\\hline 8 & \begin{lstlisting} let example8 = fun (x : Any) -> if or_ (is_int x) (is_string x) is True then true else false \end{lstlisting} & $(\Int \to \True)\land(\String \to \True)~\land$\newline $(\lnot(\String\lor\Int)\to \False)$ \\\hline 9 & \begin{lstlisting} let example9 = fun (x : Any) -> if (if is_int x is True then is_int x else is_string x) is True then f x else 0 \end{lstlisting} & $(\Int \to \Int) \land (\String \to \Int)~\land$\newline $(\lnot (\String\lor\Int)\to 0)$ \\\hline 10 & \begin{lstlisting} let example10 = fun (p : (Any,Any)) -> if is_int (fst p) is True then add1 (fst p) else 7 \end{lstlisting} & \vfill $((\Int,\Any) \to \Int) \land ((\lnot (\Int,\Any) \to 7)$ \\\hline 11 & \begin{lstlisting} let example11 = fun (p : (Any, Any)) -> if and_ (is_int (fst p)) (is_int (snd p)) is True then g p else no \end{lstlisting} & \vfill\medskip\smallskip $((\Int, \Int) \to \Int) \land (((\Any, \lnot \Int)\lor(\lnot Int, \Any))\to\Keyw{no})$ \\\hline 12 & \begin{lstlisting} let example12 = fun (p : (Any, Any)) -> if is_int (fst p) is True then true else false \end{lstlisting} & \vfill $((\Int,\Any) -> \True) \land ((\lnot \Int,\Any) -> \False) )$ \\\hline 13 & \begin{lstlisting} let example13 = fun (x : Any) -> fun (y : Any) -> if and_ (is_int x) (is_string y) is True then 1 else if is_int x is True then 2 else 3 \end{lstlisting} & \vfill $(\Int \to \String \to 1) \land (\Int \to \lnot\String \to 2)) \land$\newline $(\lnot \Int \to Any \to 3)$ \\\hline 14 & \begin{lstlisting} let example14_alt = fun (input : Int | String) -> fun (extra : (Any, Any)) -> if (input, is_int (fst extra)) is (Int, True) then add input (fst extra) else if (input, is_int (fst extra)) is (Any,True) then add (strlen input) (fst extra) else 0 \end{lstlisting} & \vfill $(\Int \to (\Int,\Any) \to \Int) ~\land~ (\Int \to (\lnot \Int, \Any) \to 0) ~\land~$\newline $(\String \to (\Int,\Any) \to \Int) ~\land~ (\String \to (\lnot \Int, \Any) \to 0)$ \\\hline \end{tabular} } \caption{Comparison with the 14 examples of \cite{THF10}} \ifsubmission% \svvspace{-10mm} \fi% \label{tab:implem2} \end{table}