code_table.tex 5.13 KB
Newer Older
Giuseppe Castagna's avatar
Giuseppe Castagna committed
1
\lstset{language=[Objective]Caml,columns=fixed,basicstyle=\linespread{0.43}\ttfamily\scriptsize,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em}
Kim Nguyễn's avatar
Kim Nguyễn committed
2
\begin{table}
3
   {\scriptsize
Giuseppe Castagna's avatar
Giuseppe Castagna committed
4
  \begin{tabular}{|@{\,}c@{\,}|p{0.482\textwidth}@{}|@{\,}p{0.482\textwidth}@{\,}|}
Kim Nguyễn's avatar
Kim Nguyễn committed
5
\hline
6
    & Code & Inferred type\\
Kim Nguyễn's avatar
Kim Nguyễn committed
7
8
9
10
11
12
    \hline
    \hline
    1 &
          \begin{lstlisting}
let basic_inf = fun (y : Int | Bool) ->
  if y is Int then incr y else lnot y\end{lstlisting}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
13
         &\vfill
Kim Nguyễn's avatar
Kim Nguyễn committed
14
15
16
17
18
19
20
           $(\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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
21
22
\end{lstlisting} &\vfill
 $(\Int\to\Int)\land(\lnot\Int\to\lnot\Int)\land$\newline
Kim Nguyễn's avatar
Kim Nguyễn committed
23
24
25
26
27
28
29
30
31
32
33
34
35
 $(\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}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
36
           &\smallskip
Kim Nguyễn's avatar
Kim Nguyễn committed
37
             $(\Int\to\Keyw{True})\land(\lnot\Int\to\Keyw{False})$\newline
Giuseppe Castagna's avatar
Giuseppe Castagna committed
38
             ~\newline\smallskip
Kim Nguyễn's avatar
Kim Nguyễn committed
39
40
41
42
43
44
45
46
             $(\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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
47
48
 \end{lstlisting} &\vfill
 $(\Keyw{True}\to\Keyw{False})\land(\lnot\Keyw{True}\to\Keyw{True})$\\\hline
Kim Nguyễn's avatar
Kim Nguyễn committed
49
50
    5 &
          \begin{lstlisting}
51
52
53
let or_ = fun (x : Any) -> fun (y: Any) ->
 if x is True then true
 else if y is True then true else false
Kim Nguyễn's avatar
Kim Nguyễn committed
54
\end{lstlisting}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
55
 &\smallskip\vfill
Kim Nguyễn's avatar
Kim Nguyễn committed
56
57
58
59
60
61
62
63
64
   $(\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}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
65
 &\vfill
Kim Nguyễn's avatar
Kim Nguyễn committed
66
67
68
69
70
71
72
73
74
75
76
77
78
   $(\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
79
          (\lnot\Bool \to 2\lor3))$~~$\land$\newline
Kim Nguyễn's avatar
Kim Nguyễn committed
80
81
$(\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
82
          (\lnot\Bool \to 2))$~~$\land$\newline
Kim Nguyễn's avatar
Kim Nguyễn committed
83
84
85
86
$(\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
87
          \lor 3))$~~$\land \ldots$ (two other redundant cases ommitted)
Kim Nguyễn's avatar
Kim Nguyễn committed
88
89
90
91
92
93
94
95
%                   \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))$
96
\\
Kim Nguyễn's avatar
Kim Nguyễn committed
97
98
99
100
101
& \begin{lstlisting}
let test_1 = f 3 true
let test_2 = f (42,42) 42
let test_3 = f nil nil
\end{lstlisting}&
Giuseppe Castagna's avatar
Giuseppe Castagna committed
102
103
104
                  $\p 1$\newline
                  $\p 2$\newline
                  $\p 3$
105
106
107
108
    \\\hline
    8 &
\begin{lstlisting}
type Document = { nodeType=9 ..}
109
110
111
112
113
114
and Element  = { childNodes=NodeList,
                 nodeType=1 ..}
and Text = { isElementContentWhiteSpace=Bool,
             nodeType=3, ..}
and Node = Document | Element | Text
and NodeList = Nil | (Node, NodeList)
115
116
117
118
119
120
121

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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
122
\end{lstlisting} &\vspace{19mm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
123
124
$(\Keyw{Document}\to\False)~\land$\newline
$(\orecord{ \texttt{nodeType}\,{=}\,1, \texttt{childNodes}\,{=}\,\Keyw{Nil} }\to\True) ~\land$\newline
Giuseppe Castagna's avatar
Giuseppe Castagna committed
125
$(\orecord{ \texttt{nodeType}\,{=}\,1, \texttt{childNodes}\,{=}\,(\Keyw{Node},\Keyw{NodeList}) }\to\False) ~\land$\newline
Giuseppe Castagna's avatar
Giuseppe Castagna committed
126
$(\Keyw{Text}\to\Bool)~\land$\newline (omitted redundant arrows)
127
128
129
130
131
    \\\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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
132
\end{lstlisting} &\vfill
133
134
135
$\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
136
137

 10 & \begin{lstlisting}
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
138
(* f, g have type: (Int->Int) & (Any->Bool) *)
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
139

Kim Nguyễn's avatar
.    
Kim Nguyễn committed
140
let example10 = fun (x : Any) ->
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
141
  if (f x, g x) is (Int, Bool) then 1 else 2
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
142
\end{lstlisting} &\vfill
Giuseppe Castagna's avatar
empty    
Giuseppe Castagna committed
143
$(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
144
\texttt{Warning: line 4, 39-40: unreachable expression}
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
145
    \\\hline
Kim Nguyễn's avatar
Kim Nguyễn committed
146
147
  \end{tabular}
}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
148
\caption{Types inferred by implementation}\vspace{-10mm}
Kim Nguyễn's avatar
Kim Nguyễn committed
149
\label{tab:implem}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
150
\end{table}