code_table2.tex 5.24 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
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}