code_table.tex 4.76 KB
Newer Older
1
\lstset{language=[Objective]Caml,columns=fixed,basicstyle=\ttfamily\scriptsize\linespread{0.8},aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em}
Kim Nguyễn's avatar
Kim Nguyễn committed
2
\begin{table}
3
   {\scriptsize
Kim Nguyễn's avatar
Kim Nguyễn committed
4
5
  \begin{tabular}{|@{\,}c@{\,}|p{0.47\textwidth}@{}|@{\,}p{0.47\textwidth}@{\,}|}
\hline
6
    & Code & Inferred type\\
Kim Nguyễn's avatar
Kim Nguyễn committed
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
    \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))$
100
\\
Kim Nguyễn's avatar
Kim Nguyễn committed
101
102
103
104
105
106
107
108
& \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$
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
    \\\hline
    8 &
\begin{lstlisting}
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.nodeType is 3 then
    x.isElementContentWhiteSpace
  else
  if x.childNodes is Nil then true else false
\end{lstlisting} &
$\Keyw{Document}\to\False \land$\newline
$\orecord{ \texttt{nodeType}=1, \texttt{childNodes} = Nil }\to\True ~\land$\newline
$\orecord{ \texttt{nodeType}=1, \texttt{childNodes} = (\Keyw{Node},\Keyw{NodeList}) }\to\True ~\land$\newline
 $\Keyw{Text}\to\Bool~\land$ (ommitted 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} &
$\True\to((\True\to\False)\land(\lnot\True\to\True))~\land$\newline
$(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$
    \\\hline
Kim Nguyễn's avatar
Kim Nguyễn committed
142
143
144
145
146
  \end{tabular}
}
\caption{Types inferred by implementation}
\label{tab:implem}
\end{table}