Commit a7afc2f3 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add 14 examples for THF10.

parent 3ef2ec85
\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}
......@@ -33,6 +33,9 @@ anonymized
online toplevel available at
\url{https://occtyping.github.io/}%
\input{code_table}
\input{code_table2}
In Table~\ref{tab:implem}, the second column gives a code fragment and the third
column the type deduced by our implementation. Code~1 is a
straightforward function similar to our introductory example \code{foo} in (\ref{foo},\ref{foo2}). Here the
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment