Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
64a3d646
Commit
64a3d646
authored
Jul 09, 2019
by
Giuseppe Castagna
Browse files
space savers
parent
84ba31e7
Changes
2
Hide whitespace changes
Inline
Side-by-side
code_table.tex
View file @
64a3d646
\lstset
{
language=[Objective]Caml,columns=fixed,basicstyle=
\ttfamily\scriptsize
\linespread
{
0.8
}
,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em
}
\lstset
{
language=[Objective]Caml,columns=fixed,basicstyle=
\
linespread
{
0.55
}
\
ttfamily\scriptsize
,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em
}
\begin{table}
{
\scriptsize
\begin{tabular}
{
|@
{
\,
}
c@
{
\,
}
|p
{
0.4
7
\textwidth
}
@
{}
|@
{
\,
}
p
{
0.4
7
\textwidth
}
@
{
\,
}
|
}
\begin{tabular}
{
|@
{
\,
}
c@
{
\,
}
|p
{
0.4
8
\textwidth
}
@
{}
|@
{
\,
}
p
{
0.4
8
\textwidth
}
@
{
\,
}
|
}
\hline
&
Code
&
Inferred type
\\
\hline
...
...
@@ -10,7 +10,7 @@
\begin{lstlisting}
let basic
_
inf = fun (y : Int | Bool) ->
if y is Int then incr y else lnot y
\end{lstlisting}
&
&
\vfill
$
(
\Int\to\Int
)
\land
(
\Bool\to\Bool
)
$
\\\hline
2
&
...
...
@@ -18,8 +18,8 @@ let basic_inf = fun (y : Int | Bool) ->
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
$
\end{lstlisting}
&
\vfill
$
(
\Int\to\Int
)
\land
(
\lnot\Int\to\lnot\Int
)
\land
$
\newline
$
(
\Bool\to\Bool
)
\land
(
\lnot
(
\Int\vee\Bool
)
\to\lnot
(
\Int\vee\Bool
))
$
\\
\hline
...
...
@@ -33,9 +33,9 @@ let is_bool = fun (x : Any) ->
let is
_
char = fun (x : Any) ->
if x is Char then true else false
\end{lstlisting}
&
&
\smallskip
$
(
\Int\to\Keyw
{
True
}
)
\land
(
\lnot\Int\to\Keyw
{
False
}
)
$
\newline
~
\newline
~
\newline
\smallskip
$
(
\Bool\to\Keyw
{
True
}
)
\land
(
\lnot\Bool\to\Keyw
{
False
}
)
$
\newline
~
\newline
$
(
\Char\to\Keyw
{
True
}
)
\land
(
\lnot\Char\to\Keyw
{
False
}
)
$
...
...
@@ -44,8 +44,8 @@ let is_char = fun (x : Any) ->
\begin{lstlisting}
let not
_
= fun (x : Any) ->
if x is True then false else true
\end{lstlisting}
&
$
(
\Keyw
{
True
}
\to\Keyw
{
False
}
)
\land
(
\Keyw
{
Fals
e
}
\to\Keyw
{
True
}
)
$
\\\hline
\end{lstlisting}
&
\vfill
$
(
\Keyw
{
True
}
\to\Keyw
{
False
}
)
\land
(
\
lnot\
Keyw
{
Tru
e
}
\to\Keyw
{
True
}
)
$
\\\hline
5
&
\begin{lstlisting}
let or
_
= fun (x : Any) ->
...
...
@@ -53,7 +53,7 @@ let or_ = fun (x : Any) ->
else fun (y : Any) ->
if y is True then true else false
\end{lstlisting}
&
&
\smallskip\vfill
$
(
\True\to\Any\to\True
)
\land
(
\Any\to\True\to\True
)
\land
$
\newline
$
(
\lnot\True\to\lnot\True\to\False
)
$
\\\hline
...
...
@@ -63,7 +63,7 @@ let and_ = fun (x : Any) -> fun (y : Any) ->
if not
_
(or
_
(not
_
x) (not
_
y)) is True
then true else false
\end{lstlisting}
&
&
\vfill
$
(
\True\to
((
\lnot\True\to\False
)
\land
(
\True\to\True
))
$
\newline
$
\land
(
\lnot\True\to\Any\to\False
)
$
\\\hline
...
...
@@ -103,21 +103,21 @@ 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
$
$
\p
1
$
\newline
$
\p
2
$
\newline
$
\p
3
$
\\\hline
8
&
\begin{lstlisting}
type Document =
{
nodeType=9 ..
}
and Element =
{
nodeType=1,
childNodes = NodeList
and Element
=
{
nodeType=1,
childNodes = NodeList
..
}
and Text =
{
nodeType=3,
isElementContentWhiteSpace=Bool
..
}
and Node = Document | Element | Text
and NodeList = Nil | (Node, 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
...
...
@@ -125,22 +125,22 @@ let is_empty_node = fun (x : Node) ->
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
$
(om
m
itted redundant arrows)
\end{lstlisting}
&
\vspace
{
23mm
}
$
(
\Keyw
{
Document
}
\to\False
)
~
\land
$
\newline
$
(
\orecord
{
\texttt
{
nodeType
}
\,
{
=
}
\,
1
,
\texttt
{
childNodes
}
\,
{
=
}
\,\Keyw
{
Nil
}
}
\to\True
)
~
\land
$
\newline
$
(
\orecord
{
\texttt
{
nodeType
}
\,
{
=
}
\,
1
,
\texttt
{
childNodes
}
\,
{
=
}
\,
(
\Keyw
{
Node
}
,
\Keyw
{
NodeList
}
)
}
\
,
{
\to
}
\,\False
)
~
\land
$
\newline
$
(
\Keyw
{
Text
}
\to\Bool
)
~
\land
$
\newline
(omitted 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}
&
\end{lstlisting}
&
\vfill
$
\True\to
((
\True\to\False
)
\land
(
\lnot\True\to\True
))
~
\land
$
\newline
$
(
\lnot\True\to
((
\True\to\True
)
\land
(
\lnot\True\to\False
))
$
\\\hline
\end{tabular}
}
\caption
{
Types inferred by implementation
}
\caption
{
Types inferred by implementation
}
\vspace
{
-10mm
}
\label
{
tab:implem
}
\end{table}
\ No newline at end of file
\end{table}
setup.sty
View file @
64a3d646
...
...
@@ -17,6 +17,8 @@
\usepackage
{
color
}
\usepackage
{
listings
}
\definecolor
{
darkblue
}{
rgb
}{
0,0.2,0.4
}
\definecolor
{
darkred
}{
rgb
}{
0.7,0.4,0.4
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment