code_table.tex 3.64 KB
Newer Older
Kim Nguyễn's avatar
Kim Nguyễn committed
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}