bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

logica che palle

Browse source
This commit is contained in:
Francesco Mecca 2020-02-21 11:29:04 +01:00
parent 0d7ed5e91d
commit 8bd79b8e39
11 changed files with 1096 additions and 305 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
anno3/logica/EsameLogica_v4_soluzioni.pdf Normal file
View file

Binary file not shown.

18
tesi/prova.aux
View file

@ -14,11 +14,15 @@
\fi}
\global\let\hyper@last\relax
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\providecommand*\HyPL@Entry[1]{}
\HyPL@Entry{0<</S/D>>}
\@writefile{toc}{\contentsline {section}{\numberline {1}{\bfseries \sffamily TODO} Scaletta [1/2]}{1}{section.1}\protected@file@percent }
\newlabel{sec:org5a6f376}{{1}{1}{{\bfseries \sffamily TODO} Scaletta [1/2]}{section.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Introduction}{1}{section.2}\protected@file@percent }
\newlabel{sec:orgef00ecd}{{2}{1}{Introduction}{section.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}{\bfseries \sffamily TODO} OCaml}{1}{subsection.2.1}\protected@file@percent }
\newlabel{sec:org5659ec2}{{2.1}{1}{{\bfseries \sffamily TODO} OCaml}{subsection.2.1}{}}
\newlabel{sec:org6c3943f}{{1}{1}{{\bfseries \sffamily TODO} Scaletta [1/2]}{section.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {2}1. Background}{2}{section.2}\protected@file@percent }
\newlabel{sec:orgad08c62}{{2}{2}{1. Background}{section.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}1.1 OCaml}{2}{subsection.2.1}\protected@file@percent }
\newlabel{sec:orgca8d200}{{2.1}{2}{1.1 OCaml}{subsection.2.1}{}}
\newlabel{sec:org83a2e95}{{1}{3}{1.1 OCaml}{Item.1}{}}
\newlabel{sec:org2127ffb}{{2}{5}{1.1 OCaml}{Item.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}1.2.1.1 Initial state of the compilation}{6}{subsection.2.2}\protected@file@percent }
\newlabel{sec:org0b0c254}{{2.2}{6}{1.2.1.1 Initial state of the compilation}{subsection.2.2}{}}

0
tesi/prova.bbl
View file

48
tesi/prova.blg
View file

@ -1,48 +0,0 @@
This is BibTeX, Version 0.99d (TeX Live 2019 Gentoo Linux)
Capacity: max_strings=100000, hash_size=100000, hash_prime=85009
The top-level auxiliary file: prova.aux
I found no \citation commands---while reading file prova.aux
I found no \bibdata command---while reading file prova.aux
I found no \bibstyle command---while reading file prova.aux
You've used 0 entries,
0 wiz_defined-function locations,
83 strings with 484 characters,
and the built_in function-call counts, 0 in all, are:
= -- 0
> -- 0
< -- 0
+ -- 0
- -- 0
* -- 0
:= -- 0
add.period$ -- 0
call.type$ -- 0
change.case$ -- 0
chr.to.int$ -- 0
cite$ -- 0
duplicate$ -- 0
empty$ -- 0
format.name$ -- 0
if$ -- 0
int.to.chr$ -- 0
int.to.str$ -- 0
missing$ -- 0
newline$ -- 0
num.names$ -- 0
pop$ -- 0
preamble$ -- 0
purify$ -- 0
quote$ -- 0
skip$ -- 0
stack$ -- 0
substring$ -- 0
swap$ -- 0
text.length$ -- 0
text.prefix$ -- 0
top$ -- 0
type$ -- 0
warning$ -- 0
while$ -- 0
width$ -- 0
write$ -- 0
(There were 3 error messages)

491
tesi/prova.log
View file

@ -1,4 +1,4 @@
This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019 Gentoo Linux) (preloaded format=pdflatex 2020.2.15) 17 FEB 2020 17:30
This is XeTeX, Version 3.14159265-2.6-0.999991 (TeX Live 2019 Gentoo Linux) (preloaded format=xelatex 2020.2.19) 19 FEB 2020 16:42
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
@ -26,13 +26,21 @@ File: size11.clo 2018/09/03 v1.4i Standard LaTeX file (size option)
Package: inputenc 2018/08/11 v1.3c Input encoding file
\inpenc@prehook=\toks14
\inpenc@posthook=\toks15
)
(/usr/share/texmf-dist/tex/latex/base/fontenc.sty
Package inputenc Warning: inputenc package ignored with utf8 based engines.
) (/usr/share/texmf-dist/tex/latex/base/fontenc.sty
Package: fontenc 2018/08/11 v2.0j Standard LaTeX package
(/usr/share/texmf-dist/tex/latex/base/t1enc.def
File: t1enc.def 2018/08/11 v2.0j Standard LaTeX file
LaTeX Font Info: Redeclaring font encoding T1 on input line 48.
)
LaTeX Font Info: Try loading font information for T1+lmr on input line 105.
(/usr/share/texmf-dist/tex/latex/lm/t1lmr.fd
File: t1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern
))
(/usr/share/texmf-dist/tex/latex/graphics/graphicx.sty
Package: graphicx 2017/06/01 v1.1a Enhanced LaTeX Graphics (DPC,SPQR)
@ -50,10 +58,10 @@ Package: trig 2016/01/03 v1.10 sin cos tan (DPC)
(/usr/share/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration
)
Package graphics Info: Driver file: pdftex.def on input line 99.
Package graphics Info: Driver file: xetex.def on input line 99.
(/usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def
File: pdftex.def 2018/01/08 v1.0l Graphics/color driver for pdftex
(/usr/share/texmf-dist/tex/latex/graphics-def/xetex.def
File: xetex.def 2017/06/24 v5.0h Graphics/color driver for xetex
))
\Gin@req@height=\dimen103
\Gin@req@width=\dimen104
@ -90,9 +98,10 @@ Package ifluatex Info: LuaTeX not detected.
Package: pdftexcmds 2018/09/10 v0.29 Utility functions of pdfTeX for LuaTeX (HO
)
Package pdftexcmds Info: LuaTeX not detected.
Package pdftexcmds Info: pdfTeX >= 1.30 not detected.
Package pdftexcmds Info: \pdf@primitive is available.
Package pdftexcmds Info: \pdf@ifprimitive is available.
Package pdftexcmds Info: \pdfdraftmode found.
Package pdftexcmds Info: \pdfdraftmode not found.
)
Package grffile Info: Option `multidot' is set to `true'.
Package grffile Info: Option `extendedchars' is set to `false'.
@ -224,82 +233,7 @@ Package textcomp Info: Setting ? sub-encoding to TS1/1 on input line 79.
(/usr/share/texmf-dist/tex/latex/base/ts1enc.def
File: ts1enc.def 2001/06/05 v3.0e (jk/car/fm) Standard LaTeX file
Now handling font encoding TS1 ...
... processing UTF-8 mapping file for font encoding TS1
(/usr/share/texmf-dist/tex/latex/base/ts1enc.dfu
File: ts1enc.dfu 2018/10/05 v1.2f UTF-8 support for inputenc
defining Unicode char U+00A2 (decimal 162)
defining Unicode char U+00A3 (decimal 163)
defining Unicode char U+00A4 (decimal 164)
defining Unicode char U+00A5 (decimal 165)
defining Unicode char U+00A6 (decimal 166)
defining Unicode char U+00A7 (decimal 167)
defining Unicode char U+00A8 (decimal 168)
defining Unicode char U+00A9 (decimal 169)
defining Unicode char U+00AA (decimal 170)
defining Unicode char U+00AC (decimal 172)
defining Unicode char U+00AE (decimal 174)
defining Unicode char U+00AF (decimal 175)
defining Unicode char U+00B0 (decimal 176)
defining Unicode char U+00B1 (decimal 177)
defining Unicode char U+00B2 (decimal 178)
defining Unicode char U+00B3 (decimal 179)
defining Unicode char U+00B4 (decimal 180)
defining Unicode char U+00B5 (decimal 181)
defining Unicode char U+00B6 (decimal 182)
defining Unicode char U+00B7 (decimal 183)
defining Unicode char U+00B9 (decimal 185)
defining Unicode char U+00BA (decimal 186)
defining Unicode char U+00BC (decimal 188)
defining Unicode char U+00BD (decimal 189)
defining Unicode char U+00BE (decimal 190)
defining Unicode char U+00D7 (decimal 215)
defining Unicode char U+00F7 (decimal 247)
defining Unicode char U+0192 (decimal 402)
defining Unicode char U+02C7 (decimal 711)
defining Unicode char U+02D8 (decimal 728)
defining Unicode char U+02DD (decimal 733)
defining Unicode char U+0E3F (decimal 3647)
defining Unicode char U+2016 (decimal 8214)
defining Unicode char U+2020 (decimal 8224)
defining Unicode char U+2021 (decimal 8225)
defining Unicode char U+2022 (decimal 8226)
defining Unicode char U+2030 (decimal 8240)
defining Unicode char U+2031 (decimal 8241)
defining Unicode char U+203B (decimal 8251)
defining Unicode char U+203D (decimal 8253)
defining Unicode char U+2044 (decimal 8260)
defining Unicode char U+204E (decimal 8270)
defining Unicode char U+2052 (decimal 8274)
defining Unicode char U+20A1 (decimal 8353)
defining Unicode char U+20A4 (decimal 8356)
defining Unicode char U+20A6 (decimal 8358)
defining Unicode char U+20A9 (decimal 8361)
defining Unicode char U+20AB (decimal 8363)
defining Unicode char U+20AC (decimal 8364)
defining Unicode char U+20B1 (decimal 8369)
defining Unicode char U+2103 (decimal 8451)
defining Unicode char U+2116 (decimal 8470)
defining Unicode char U+2117 (decimal 8471)
defining Unicode char U+211E (decimal 8478)
defining Unicode char U+2120 (decimal 8480)
defining Unicode char U+2122 (decimal 8482)
defining Unicode char U+2126 (decimal 8486)
defining Unicode char U+2127 (decimal 8487)
defining Unicode char U+212E (decimal 8494)
defining Unicode char U+2190 (decimal 8592)
defining Unicode char U+2191 (decimal 8593)
defining Unicode char U+2192 (decimal 8594)
defining Unicode char U+2193 (decimal 8595)
defining Unicode char U+2329 (decimal 9001)
defining Unicode char U+232A (decimal 9002)
defining Unicode char U+2422 (decimal 9250)
defining Unicode char U+25E6 (decimal 9702)
defining Unicode char U+25EF (decimal 9711)
defining Unicode char U+266A (decimal 9834)
defining Unicode char U+FEFF (decimal 65279)
))
)
LaTeX Info: Redefining \oldstylenums on input line 334.
Package textcomp Info: Setting cmr sub-encoding to TS1/0 on input line 349.
Package textcomp Info: Setting cmss sub-encoding to TS1/0 on input line 350.
@ -423,8 +357,6 @@ Package: auxhook 2016/05/16 v1.4 Hooks for auxiliary files (HO)
(/usr/share/texmf-dist/tex/latex/hyperref/pd1enc.def
File: pd1enc.def 2018/11/30 v6.88e Hyperref: PDFDocEncoding definition (HO)
Now handling font encoding PD1 ...
... no UTF-8 mapping file for font encoding PD1
)
\Hy@SavedSpaceFactor=\count110
@ -462,12 +394,23 @@ LaTeX Info: Redefining \pageref on input line 6454.
\c@Item=\count114
\c@Hfootnote=\count115
)
Package hyperref Info: Driver (autodetected): hpdftex.
Package hyperref Info: Driver (autodetected): hxetex.
(/usr/share/texmf-dist/tex/latex/hyperref/hpdftex.def
File: hpdftex.def 2018/11/30 v6.88e Hyperref driver for pdfTeX
\Fld@listcount=\count116
\c@bookmark@seq@number=\count117
(/usr/share/texmf-dist/tex/latex/hyperref/hxetex.def
File: hxetex.def 2018/11/30 v6.88e Hyperref driver for XeTeX
(/usr/share/texmf-dist/tex/latex/hyperref/puenc.def
File: puenc.def 2018/11/30 v6.88e Hyperref: PDF Unicode definition (HO)
)
(/usr/share/texmf-dist/tex/generic/oberdiek/stringenc.sty
Package: stringenc 2016/05/16 v1.11 Convert strings between diff. encodings (HO
)
)
\pdfm@box=\box38
\c@Hy@AnnotLevel=\count116
\HyField@AnnotCount=\count117
\Fld@listcount=\count118
\c@bookmark@seq@number=\count119
(/usr/share/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty
Package: rerunfilecheck 2016/05/16 v1.8 Rerun checks for auxiliary files (HO)
@ -477,19 +420,20 @@ Package uniquecounter Info: New unique counter `rerunfilecheck' on input line 2
\Hy@SectionHShift=\skip53
)
(/usr/share/texmf-dist/tex/latex/algorithms/algorithm.sty
Invalid UTF-8 byte or sequence at line 11 replaced by U+FFFD.
Package: algorithm 2009/08/24 v0.1 Document Style `algorithm' - floating enviro
nment
(/usr/share/texmf-dist/tex/latex/float/float.sty
Package: float 2001/11/08 v1.3d Float enhancements (AL)
\c@float@type=\count118
\c@float@type=\count120
\float@exts=\toks26
\float@box=\box38
\float@box=\box39
\@float@everytoks=\toks27
\@floatcapt=\box39
\@floatcapt=\box40
)
\@float@every@algorithm=\toks28
\c@algorithm=\count119
\c@algorithm=\count121
)
(/usr/share/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty
Package: algpseudocode
@ -498,15 +442,15 @@ Package: algpseudocode
Package: algorithmicx 2005/04/27 v1.2 Algorithmicx
Document Style algorithmicx 1.2 - a greatly improved `algorithmic' style
\c@ALG@line=\count120
\c@ALG@rem=\count121
\c@ALG@nested=\count122
\c@ALG@line=\count122
\c@ALG@rem=\count123
\c@ALG@nested=\count124
\ALG@tlm=\skip54
\ALG@thistlm=\skip55
\c@ALG@Lnr=\count123
\c@ALG@blocknr=\count124
\c@ALG@storecount=\count125
\c@ALG@tmpcounter=\count126
\c@ALG@Lnr=\count125
\c@ALG@blocknr=\count126
\c@ALG@storecount=\count127
\c@ALG@tmpcounter=\count128
\ALG@tmplength=\skip56
)
Document Style - pseudocode environments for use with the `algorithmicx' style
@ -522,27 +466,34 @@ Package: amsthm 2017/10/31 v2.20.4
\thm@headsep=\skip59
\dth@everypar=\toks34
)
\c@definition=\count127
(/usr/share/texmf-dist/tex/latex/base/fontenc.sty
Package: fontenc 2018/08/11 v2.0j Standard LaTeX package
(/usr/share/texmf-dist/tex/latex/base/t1enc.def
File: t1enc.def 2018/08/11 v2.0j Standard LaTeX file
LaTeX Font Info: Redeclaring font encoding T1 on input line 48.
))
\c@definition=\count129
(/usr/share/texmf-dist/tex/latex/listings/listings.sty
\lst@mode=\count128
\lst@gtempboxa=\box40
\lst@mode=\count130
\lst@gtempboxa=\box41
\lst@token=\toks35
\lst@length=\count129
\lst@length=\count131
\lst@currlwidth=\dimen124
\lst@column=\count130
\lst@pos=\count131
\lst@column=\count132
\lst@pos=\count133
\lst@lostspace=\dimen125
\lst@width=\dimen126
\lst@newlines=\count132
\lst@lineno=\count133
\lst@newlines=\count134
\lst@lineno=\count135
\lst@maxwidth=\dimen127
(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
File: lstmisc.sty 2019/02/27 1.8b (Carsten Heinz)
\c@lstnumber=\count134
\lst@skipnumbers=\count135
\lst@framebox=\box41
\c@lstnumber=\count136
\lst@skipnumbers=\count137
\lst@framebox=\box42
)
(/usr/share/texmf-dist/tex/latex/listings/listings.cfg
File: listings.cfg 2019/02/27 1.8b listings configuration
@ -555,64 +506,41 @@ Package: color 2016/07/10 v1.1e Standard LaTeX Color (DPC)
(/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration
)
Package color Info: Driver file: pdftex.def on input line 147.
Package color Info: Driver file: xetex.def on input line 147.
)
No file prova.aux.
(/usr/share/texmf-dist/tex/generic/oberdiek/se-ascii-print.def
File: se-ascii-print.def 2016/05/16 v1.11 stringenc: Printable ASCII characters
) (./prova.aux)
\openout1 = `prova.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 35.
LaTeX Font Info: ... okay on input line 35.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 35.
LaTeX Font Info: ... okay on input line 35.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 35.
LaTeX Font Info: ... okay on input line 35.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 35.
LaTeX Font Info: ... okay on input line 35.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 35.
LaTeX Font Info: ... okay on input line 35.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 35.
LaTeX Font Info: ... okay on input line 35.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 35.
LaTeX Font Info: Try loading font information for TS1+cmr on input line 35.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for TU/lmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 37.
LaTeX Font Info: Try loading font information for TS1+cmr on input line 37.
(/usr/share/texmf-dist/tex/latex/base/ts1cmr.fd
File: ts1cmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions
)
LaTeX Font Info: ... okay on input line 35.
LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 35.
LaTeX Font Info: ... okay on input line 35.
(/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count136
\scratchdimen=\dimen128
\scratchbox=\box42
\nofMPsegments=\count137
\nofMParguments=\count138
\everyMPshowfont=\toks36
\MPscratchCnt=\count139
\MPscratchDim=\dimen129
\MPnumerator=\count140
\makeMPintoPDFobject=\count141
\everyMPtoPDFconversion=\toks37
) (/usr/share/texmf-dist/tex/latex/oberdiek/epstopdf-base.sty
Package: epstopdf-base 2016/05/15 v2.6 Base part for package epstopdf
(/usr/share/texmf-dist/tex/latex/oberdiek/grfext.sty
Package: grfext 2016/05/16 v1.2 Manage graphics extensions (HO)
)
Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4
38.
Package grfext Info: Graphics extension search list:
(grfext) [.pdf,.png,.jpg,.mps,.jpeg,.jbig2,.jb2,.PDF,.PNG,.JPG,.JPE
G,.JBIG2,.JB2,.eps]
(grfext) \AppendGraphicsExtensions on input line 456.
(/usr/share/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv
e
))
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for PU/pdf/m/n on input line 37.
LaTeX Font Info: ... okay on input line 37.
\AtBeginShipoutBox=\box43
Package hyperref Info: Link coloring OFF on input line 35.
Package hyperref Info: Link coloring OFF on input line 37.
(/usr/share/texmf-dist/tex/latex/hyperref/nameref.sty
Package: nameref 2016/05/21 v2.44 Cross-referencing by name of section
@ -620,38 +548,203 @@ Package: nameref 2016/05/21 v2.44 Cross-referencing by name of section
(/usr/share/texmf-dist/tex/generic/oberdiek/gettitlestring.sty
Package: gettitlestring 2016/05/16 v1.5 Cleanup title references (HO)
)
\c@section@level=\count142
\c@section@level=\count138
)
LaTeX Info: Redefining \ref on input line 35.
LaTeX Info: Redefining \pageref on input line 35.
LaTeX Info: Redefining \nameref on input line 35.
LaTeX Info: Redefining \ref on input line 37.
LaTeX Info: Redefining \pageref on input line 37.
LaTeX Info: Redefining \nameref on input line 37.
(./prova.out)
(./prova.out)
\@outlinefile=\write3
\openout3 = `prova.out'.
\c@lstlisting=\count143
LaTeX Font Info: Try loading font information for U+msa on input line 38.
(/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd
\c@lstlisting=\count139
LaTeX Font Info: Try loading font information for U+msa on input line 40.
(/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd
File: umsa.fd 2013/01/14 v3.01 AMS symbols A
)
LaTeX Font Info: Try loading font information for U+msb on input line 38.
LaTeX Font Info: Try loading font information for U+msb on input line 40.
(/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
)
LaTeX Font Info: Try loading font information for T1+cmss on input line 38.
LaTeX Font Info: Try loading font information for T1+lmss on input line 40.
(/usr/share/texmf-dist/tex/latex/base/t1cmss.fd
File: t1cmss.fd 2014/09/29 v2.5h Standard LaTeX font definitions
(/usr/share/texmf-dist/tex/latex/lm/t1lmss.fd
File: t1lmss.fd 2009/10/30 v1.6 Font defs for Latin Modern
) [1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Package atveryend Info: Empty hook `BeforeClearDocument' on input line 98.
[2]
Package atveryend Info: Empty hook `AfterLastShipout' on input line 98.
]
LaTeX Font Info: Try loading font information for TS1+lmr on input line 82.
(/usr/share/texmf-dist/tex/latex/lm/ts1lmr.fd
File: ts1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern
) [2]
LaTeX Font Info: Try loading font information for T1+lmtt on input line 145.
(/usr/share/texmf-dist/tex/latex/lm/t1lmtt.fd
File: t1lmtt.fd 2009/10/30 v1.6 Font defs for Latin Modern
) [3]
Overfull \hbox (18.04773pt too wide) in paragraph at lines 180--180
[]\T1/lmtt/m/n/10.95 | (Some _, None) -> print "Pair of optional types, last n
ull"[]
[]
Overfull \hbox (23.79646pt too wide) in paragraph at lines 180--180
[]\T1/lmtt/m/n/10.95 | (None, Some _) -> print "Pair of optional types, first
null"[]
[]
Overfull \hbox (6.55026pt too wide) in paragraph at lines 180--180
[]\T1/lmtt/m/n/10.95 | (None, None) -> print "Pair of optional types, both nul
l"[]
[]
[4]
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₙ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₙ in font ec-lmr10!
Missing character: There is no ⁱ in font ec-lmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no ₁ in font cmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no ₂ in font cmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no ₘ in font cmmi10!
Missing character: There is no → in font cmr10!
Overfull \hbox (2.96298pt too wide) in paragraph at lines 259--261
[]\T1/lmr/m/n/10.95 Most na-tive data types in OCaml, such as in-te-gers, tu-pl
es, lists, records,
[]
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₐ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₐ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₐ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₐ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₐ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₐ in font ec-lmr10!
Missing character: There is no ᵢ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ᵢ in font ec-lmr10!
Missing character: There is no ∀ in font ec-lmr10!
Missing character: There is no ∈ in font ec-lmr10!
! Undefined control sequence.
l.285 \vv
{v} = (v₁, v₂, \ldots{}, vᵢ) matches the line number i in P if and...
?
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ᵢ in font ec-lmr10!
[5]
! Misplaced alignment tab character &.
l.288 \item \[ p_{i,1} &
p_{i,2} & \cdots & p_{i,n} \] ≼ (v₁, v₂, \ldots{}, vᵢ)
?
! Misplaced alignment tab character &.
l.288 \item \[ p_{i,1} & p_{i,2} &
\cdots & p_{i,n} \] ≼ (v₁, v₂, \ldots{}, vᵢ)
?
! Misplaced alignment tab character &.
<recently read> &
l.288 \item \[ p_{i,1} & p_{i,2} & \cdots &
p_{i,n} \] ≼ (v₁, v₂, \ldots{}, vᵢ)
?
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ᵢ in font ec-lmr10!
! Misplaced alignment tab character &.
l.289 \item \[ ∀j < i p_{j,1} &
p_{j,2} & \cdots & p_{j,n} \] ⋠ (v₁, v₂, \ld...
?
! Misplaced alignment tab character &.
l.289 \item \[ ∀j < i p_{j,1} & p_{j,2} &
\cdots & p_{j,n} \] ⋠ (v₁, v₂, \ld...
?
! Misplaced alignment tab character &.
<recently read> &
l.289 \item \[ ∀j < i p_{j,1} & p_{j,2} & \cdots &
p_{j,n} \] ⋠ (v₁, v₂, \ld...
?
Missing character: There is no ∀ in font cmr10!
Missing character: There is no ⋠ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ᵢ in font ec-lmr10!
Missing character: There is no ≼ in font ec-lmr10!
Missing character: There is no ≡ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₘ in font ec-lmr10!
Missing character: There is no ₘ in font ec-lmr10!
! Undefined control sequence.
l.324 \vv
{x} = (x₁, x₂, \ldots{}, xₙ) of size n
?
Missing character: There is no ₁ in font ec-lmr10!
Missing character: There is no ₂ in font ec-lmr10!
Missing character: There is no ₙ in font ec-lmr10!
Missing character: There is no → in font ec-lmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no ₁ in font cmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no ₂ in font cmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no → in font cmr10!
Missing character: There is no ₘ in font cmmi10!
Missing character: There is no → in font cmr10!
Package atveryend Info: Empty hook `BeforeClearDocument' on input line 336.
[6]
Package atveryend Info: Empty hook `AfterLastShipout' on input line 336.
(./prova.aux)
Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 98.
Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 98.
Package atveryend Info: Empty hook `AtVeryEndDocument' on input line 336.
Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 336.
Package rerunfilecheck Warning: File `prova.out' has changed.
@ -659,36 +752,20 @@ Package rerunfilecheck Warning: File `prova.out' has changed.
(rerunfilecheck) or use package `bookmark'.
Package rerunfilecheck Info: Checksums for `prova.out':
(rerunfilecheck) Before: <no file>
(rerunfilecheck) After: 7405D30B8D200DFB9FDA8AFBCA5DCCFE;160.
(rerunfilecheck) Before: 25CD49CE93FE2EBDE0A77084F183FACA
(rerunfilecheck) After: 4C10F3A28DB5B56905D83B509FE58CA0.
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 98.
Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 336.
)
Here is how much of TeX's memory you used:
9008 strings out of 494553
127405 string characters out of 6177841
211891 words of memory out of 5000000
12522 multiletter control sequences out of 15000+600000
18671 words of font info for 51 fonts, out of 8000000 for 9000
11724 strings out of 494894
164120 string characters out of 6177622
238134 words of memory out of 5000000
15485 multiletter control sequences out of 15000+600000
53749 words of font info for 57 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191
36i,6n,32p,286b,345s stack positions out of 5000i,500n,10000p,200000b,80000s
{/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc}{/usr/share/t
exmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}</usr/share/texmf-dist/font
s/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texmf-dist/fonts/type1/p
ublic/cm-super/sfbx1000.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/
sfbx1200.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb></
usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb></usr/share/texmf
-dist/fonts/type1/public/cm-super/sfrm1095.pfb></usr/share/texmf-dist/fonts/typ
e1/public/cm-super/sfrm1200.pfb></usr/share/texmf-dist/fonts/type1/public/cm-su
per/sfrm1728.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfsx1200.pf
b></usr/share/texmf-dist/fonts/type1/public/cm-super/sfsx1440.pfb></usr/share/t
exmf-dist/fonts/type1/public/cm-super/sfti1095.pfb>
Output written on prova.pdf (2 pages, 133009 bytes).
PDF statistics:
68 PDF objects out of 1000 (max. 8388607)
52 compressed objects within 1 object stream
6 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
36i,9n,45p,286b,536s stack positions out of 5000i,500n,10000p,200000b,80000s
Output written on prova.pdf (6 pages).

320
tesi/prova.md Normal file
View file

@ -0,0 +1,320 @@
# TODO Scaletta <code>[1/2]</code>
- [X] Abstract
- [-] Background <code>[25%]</code>
- [X] Ocaml
- [ ] Lambda code
- [ ] Pattern matching
- [ ] Translation Verification
- [ ] Symbolic execution
\begin{abstract}
This dissertation presents an algorithm for the translation validation of the OCaml
pattern matching compiler. Given the source representation of the target program and the
target program compiled in untyped lambda form, the algoritmhm is capable of modelling
the source program in terms of symbolic constraints on it's branches and apply symbolic
execution on the untyped lambda representation in order to validate wheter the compilation
produced a valid result.
In this context a valid result means that for every input in the domain of the source
program the untyped lambda translation produces the same output as the source program.
The input of the program is modelled in terms of symbolic constraints closely related to
the runtime representation of OCaml objects and the output consists of OCaml code
blackboxes that are not evaluated in the context of the verification.
\end{abstract}
# 1. Background
## 1.1 OCaml
Objective Caml (OCaml) is a dialect of the ML (Meta-Language) family of programming
languages.
OCaml shares many features with other dialects of ML, such as SML and Caml Light,
The main features of ML languages are the use of the Hindley-Milner type system that
provides many advantages with respect to static type systems of traditional imperative and object
oriented language such as C, C++ and Java, such as:
- Parametric polymorphism: in certain scenarios a function can accept more than one
type for the input parameters. For example a function that computes the lenght of a
list doesn't need to inspect the type of the elements of the list and for this reason
a List.length function can accept list of integers, list of strings and in general
list of any type. Such languages offer polymorphic functions through subtyping at
runtime only, while other languages such as C++ offer polymorphism through compile
time templates and function overloading.
With the Hindley-Milner type system each well typed function can have more than one
type but always has a unique best type, called the *principal type*.
For example the principal type of the List.length function is "For any *a*, function from
list of *a* to *int*" and *a* is called the *type parameter*.
- Strong typing: Languages such as C and C++ allow the programmer to operate on data
without considering its type, mainly through pointers. Other languages such as C#
and Go allow type erasure so at runtime the type of the data can't be queried.
In the case of programming languages using an Hindley-Milner type system the
programmer is not allowed to operate on data by ignoring or promoting its type.
- Type Inference: the principal type of a well formed term can be inferred without any
annotation or declaration.
- Algebraic data types: types that are modelled by the use of two
algebraic operations, sum and product.
A sum type is a type that can hold of many different types of
objects, but only one at a time. For example the sum type defined
as *A + B* can hold at any moment a value of type A or a value of
type B. Sum types are also called tagged union or variants.
A product type is a type constructed as a direct product
of multiple types and contains at any moment one instance for
every type of its operands. Product types are also called tuples
or records. Algebraic data types can be recursive
in their definition and can be combined.
Moreover ML languages are functional, meaning that functions are
treated as first class citizens and variables are immutable,
although mutable statements and imperative constructs are permitted.
In addition to that OCaml features an object system, that provides
inheritance, subtyping and dynamic binding, and modules, that
provide a way to encapsulate definitions. Modules are checked
statically and can be reificated through functors.
1. TODO 1.2 Pattern matching <code>[37%]</code>
- [ ] capisci come mettere gli esempi uno accanto all'altro
Pattern matching is a widely adopted mechanism to interact with ADT.
C family languages provide branching on predicates through the use of
if statements and switch statements.
Pattern matching is a mechanism for destructuring and analyzing data
structures for the presence of values simbolically represented as
tokens. One common example of pattern matching is the use of regular
expressions on strings. OCaml provides pattern matching on ADT,
primitive data types.
- [X] Esempio enum, C e Ocaml
type color = | Red | Blue | Green
begin match color with
| Red -> print "red"
| Blue -> print "red"
| Green -> print "red"
OCaml provides tokens to express data destructoring
- [X] Esempio destructor list
begin match list with
| [ ] -> print "empty list"
| element1 :: [ ] -> print "one element"
| element1 :: element2 :: [ ] -> print "two elements"
| head :: tail-> print "head followed by many elements"
- [X] Esempio destructor tuples
begin match tuple with
| (Some _, Some _) -> print "Pair of optional types"
| (Some _, None) -> print "Pair of optional types, last null"
| (None, Some _) -> print "Pair of optional types, first null"
| (None, None) -> print "Pair of optional types, both null"
Pattern clauses can make the use of *guards* to test predicates and
variables can be binded in scope.
- [ ] Esempio binding e guards
begin match token_list with
| "switch"::var::"{"::rest ->
| "case"::":"::var::rest when is_int var ->
| "case"::":"::var::rest when is_string var ->
| "}"::[ ] -> stop ()
| "}"::rest -> error "syntax error: " rest
- [ ] Un altro esempio con destructors e tutto i lresto
In general pattern matching on primitive and algebraic data types takes the
following form.
- [ ] Esempio informale
It can be described more formally through a BNF grammar.
- [ ] BNF
- [ ] Come funziona il pattern matching?
2. TODO 1.2.1 Pattern matching compilation to lambda code
- [ ] Da tabella a matrice
Formally, pattern and values are defined as follow:
<table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
<colgroup>
<col class="org-left" />
<col class="org-left" />
</colgroup>
<thead>
<tr>
<th scope="col" class="org-left">pattern ::=</th>
<th scope="col" class="org-left">Patterns</th>
</tr>
</thead>
<tbody>
<tr>
<td class="org-left">\_</td>
<td class="org-left">wildcard</td>
</tr>
<tr>
<td class="org-left">x</td>
<td class="org-left">variable</td>
</tr>
<tr>
<td class="org-left">c(p1,p2,&#x2026;,pn</td>
<td class="org-left">constructor pattern</td>
</tr>
<tr>
<td class="org-left">(p1&vert; p2)</td>
<td class="org-left">or-pattern</td>
</tr>
</tbody>
</table>
<table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
<colgroup>
<col class="org-left" />
<col class="org-left" />
</colgroup>
<thead>
<tr>
<th scope="col" class="org-left">values ::=</th>
<th scope="col" class="org-left">Values</th>
</tr>
</thead>
<tbody>
<tr>
<td class="org-left">c(v1, v2, &#x2026;, vn)</td>
<td class="org-left">constructor value</td>
</tr>
</tbody>
</table>
The entire pattern matching code can be represented as a clause matrix
that associates rows of patterns (p<sub>i,1</sub>, p<sub>i,2</sub>, &#x2026;, p<sub>i,n</sub>) to
lambda code action lⁱ
\begin{equation*}
(P → L) =
\begin{pmatrix}
p_{1,1} & p_{1,2} & \cdots & p_{1,n} → l₁ \\
p_{2,1} & p_{2,2} & \cdots & p_{2,n} → l₂ \\
\vdots & \vdots & \ddots \vdots → \vdots \\
p_{m,1} & p_{m,2} & \cdots & p_{m,n} → lₘ
\end{pmatrix}
\end{equation*}
Most native data types in OCaml, such as integers, tuples, lists,
records, can be seen as instances of the following definition
type t = Nil | One of int | Cons of int * t
that is a type *t* with three constructors that define its complete
signature.
Every constructor has an arity. Nil, a constructor of arity 0, is
called a constant constructor.
The pattern *p* matches a value *v*, written as p ≼ v, when
one of the following rules apply
<table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
<colgroup>
<col class="org-left" />
<col class="org-left" />
<col class="org-left" />
<col class="org-left" />
</colgroup>
<tbody>
<tr>
<td class="org-left">\_</td>
<td class="org-left">≼</td>
<td class="org-left">v</td>
<td class="org-left">&#xa0;</td>
</tr>
<tr>
<td class="org-left">x</td>
<td class="org-left">≼</td>
<td class="org-left">v</td>
<td class="org-left">&#xa0;</td>
</tr>
<tr>
<td class="org-left">(p₁ &vert;\\ p₂)</td>
<td class="org-left">≼</td>
<td class="org-left">v</td>
<td class="org-left">iff p₁ ≼ v or p₂ ≼ v</td>
</tr>
<tr>
<td class="org-left">c(p₁, p₂, &#x2026;, pₐ)</td>
<td class="org-left">≼</td>
<td class="org-left">c(v₁, v₂, &#x2026;, vₐ)</td>
<td class="org-left">iff (p₁, p₂, &#x2026;, pₐ) ≼ (v₁, v₂, &#x2026;, vₐ)</td>
</tr>
<tr>
<td class="org-left">(p₁, p₂, &#x2026;, pₐ)</td>
<td class="org-left">≼</td>
<td class="org-left">(v₁, v₂, &#x2026;, vₐ)</td>
<td class="org-left">iff pᵢ ≼ vᵢ ∀i ∈ [1..a]</td>
</tr>
</tbody>
</table>
We can also say that *v* is an *instance* of *p*.
When we consider the pattern matrix P we say that the value vector
\vv{v} = (v₁, v₂, &#x2026;, vᵢ) matches the line number i in P if and only if the following two
conditions are satisfied:
- \[ p_{i,1} & p_{i,2} & \cdots & p_{i,n} \] ≼ (v₁, v₂, &#x2026;, vᵢ)
- \[ ∀j < i p_{j,1} & p_{j,2} & \cdots & p_{j,n} \] ⋠ (v₁, v₂, &#x2026;, vᵢ)
We can define the following three relations with respect to patterns:
- Patter p is less precise than pattern q, writtens p ≼ q when all
instances of q are instances of p
- Pattern p and q are equivalent, written p ≡ q, when their instances
are the same
- Patterns p and q are compatible when they share a common instance

257
tesi/prova.org
View file

@ -1,10 +1,25 @@
* TODO Scaletta [1/2]
- [X] Abstract
- [ ] Introduction [0%]
- [ ] Ocaml
- [ ] Pattern matching
- [-] Background [20%]
- [X] Ocaml
- [ ] Lambda code [0%]
- [ ] Untyped lambda form
- [ ] OCaml specific instructions
- [-] Pattern matching [50%]
- [X] Introduzione
- [ ] Compilation to lambda form
- [ ] Translation Verification
- [ ] Symbolic execution
- [ ] Translation verification of the Pattern Matching Compiler
- [ ] Source translation
- [ ] Formal Grammar
- [ ] Compilation of source patterns
- [ ] Target translation
- [ ] Formal Grammar
- [ ] Symbolic execution of the lambda target
- [ ] Equivalence between source and target
- [ ] Practical results
#+TITLE: Translation Verification of the OCaml pattern matching compiler
#+AUTHOR: Francesco Mecca
@ -17,6 +32,8 @@
#+LaTeX_HEADER: \usepackage{algorithm}
#+LaTeX_HEADER: \usepackage{algpseudocode}
#+LaTeX_HEADER: \usepackage{amsmath,amssymb,amsthm}
#+LaTeX_HEADER: \usepackage[utf8]{inputenc}
#+LaTeX_HEADER: \usepackage[T1]{fontenc}
#+Latex_HEADER: \newtheorem{definition}{Definition}
#+LaTeX_HEADER: \usepackage{graphicx}
#+LaTeX_HEADER: \usepackage{listings}
@ -41,30 +58,212 @@ blackboxes that are not evaluated in the context of the verification.
\end{abstract}
* Introduction
* 1. Background
** TODO OCaml
Objective Caml (OCaml) is a dialect of the ML (Meta-Language) family of programming
languages.
OCaml shares many features with other dialects of ML, such as SML and Caml Light,
The main features of ML languages are the use of the Hindley-Milner type system that
provides with respect to static type systems of traditional imperative and/or object
oriented language such as C, C++ and Java many advantages such as:
- Parametric polymorphism: in certain scenarios a function can accept more than one
type for the input parameters. For example a function that computes the lenght of a
list doesn't need to inspect the type of the elements of the list and for this reason
a List.length function can accept list of integers, list of strings and in general
list of any type. Such languages offer polymorphic functions through subtyping at
runtime only, while other languages such as C++ offer polymorphism through compile
time templates and function overloading.
With the Hindley-Milner type system each well typed function can have more than one
type but always has a unique best type, called the /principal type/.
For example the principal type of the List.length function is "For any /a/, function from
list of /a/ to /int/" and /a/ is called the /type parameter/.
- Strong typing: Languages such as C and C++ allow the programmer to operate on data
without considering its type, mainly through pointers. Other languages such as C#
and Go allow type erasure so at runtime the type of the data can't be queried.
In the case of programming languages using an Hindley-Milner type system the
programmer is not allowed to operate on data by ignoring or promoting its type.
- Type Inference: the principal type of a well formed term can be inferred without any
annotation or declaration.
** 1.1 OCaml
Objective Caml (OCaml) is a dialect of the ML (Meta-Language) family of programming
languages.
OCaml shares many features with other dialects of ML, such as SML and Caml Light,
The main features of ML languages are the use of the Hindley-Milner type system that
provides many advantages with respect to static type systems of traditional imperative and object
oriented language such as C, C++ and Java, such as:
- Parametric polymorphism: in certain scenarios a function can accept more than one
type for the input parameters. For example a function that computes the lenght of a
list doesn't need to inspect the type of the elements of the list and for this reason
a List.length function can accept list of integers, list of strings and in general
list of any type. Such languages offer polymorphic functions through subtyping at
runtime only, while other languages such as C++ offer polymorphism through compile
time templates and function overloading.
With the Hindley-Milner type system each well typed function can have more than one
type but always has a unique best type, called the /principal type/.
For example the principal type of the List.length function is "For any /a/, function from
list of /a/ to /int/" and /a/ is called the /type parameter/.
- Strong typing: Languages such as C and C++ allow the programmer to operate on data
without considering its type, mainly through pointers. Other languages such as C#
and Go allow type erasure so at runtime the type of the data can't be queried.
In the case of programming languages using an Hindley-Milner type system the
programmer is not allowed to operate on data by ignoring or promoting its type.
- Type Inference: the principal type of a well formed term can be inferred without any
annotation or declaration.
- Algebraic data types: types that are modelled by the use of two
algebraic operations, sum and product.
A sum type is a type that can hold of many different types of
objects, but only one at a time. For example the sum type defined
as /A + B/ can hold at any moment a value of type A or a value of
type B. Sum types are also called tagged union or variants.
A product type is a type constructed as a direct product
of multiple types and contains at any moment one instance for
every type of its operands. Product types are also called tuples
or records. Algebraic data types can be recursive
in their definition and can be combined.
Moreover ML languages are functional, meaning that functions are
treated as first class citizens and variables are immutable,
although mutable statements and imperative constructs are permitted.
In addition to that OCaml features an object system, that provides
inheritance, subtyping and dynamic binding, and modules, that
provide a way to encapsulate definitions. Modules are checked
statically and can be reificated through functors.
*** TODO 1.2 Pattern matching [37%]
- [ ] capisci come mettere gli esempi uno accanto all'altro
Pattern matching is a widely adopted mechanism to interact with ADT.
C family languages provide branching on predicates through the use of
if statements and switch statements.
Pattern matching is a mechanism for destructuring and analyzing data
structures for the presence of values simbolically represented as
tokens. One common example of pattern matching is the use of regular
expressions on strings. OCaml provides pattern matching on ADT,
primitive data types.
- [X] Esempio enum, C e Ocaml
#+BEGIN_SRC ocaml
type color = | Red | Blue | Green
begin match color with
| Red -> print "red"
| Blue -> print "red"
| Green -> print "red"
#+END_SRC
OCaml provides tokens to express data destructoring
- [X] Esempio destructor list
#+BEGIN_SRC ocaml
begin match list with
| [ ] -> print "empty list"
| element1 :: [ ] -> print "one element"
| element1 :: element2 :: [ ] -> print "two elements"
| head :: tail-> print "head followed by many elements"
#+END_SRC
- [X] Esempio destructor tuples
#+BEGIN_SRC ocaml
begin match tuple with
| (Some _, Some _) -> print "Pair of optional types"
| (Some _, None) -> print "Pair of optional types, last null"
| (None, Some _) -> print "Pair of optional types, first null"
| (None, None) -> print "Pair of optional types, both null"
#+END_SRC
Pattern clauses can make the use of /guards/ to test predicates and
variables can be binded in scope.
- [ ] Esempio binding e guards
#+BEGIN_SRC ocaml
begin match token_list with
| "switch"::var::"{"::rest ->
| "case"::":"::var::rest when is_int var ->
| "case"::":"::var::rest when is_string var ->
| "}"::[ ] -> stop ()
| "}"::rest -> error "syntax error: " rest
#+END_SRC
- [ ] Un altro esempio con destructors e tutto i lresto
In general pattern matching on primitive and algebraic data types takes the
following form.
- [ ] Esempio informale
It can be described more formally through a BNF grammar.
- [ ] BNF
- [ ] Come funziona il pattern matching?
*** TODO 1.2.1 Pattern matching compilation to lambda code
- [ ] Da tabella a matrice
Formally, pattern are defined as follows:
| pattern ::= | Patterns |
|----------------+---------------------|
| _ | wildcard |
| x | variable |
| c(p₁,p₂,...,pₙ | constructor pattern |
| (p₁\vert p₂) | or-pattern |
Values are defined as follows:
| values ::= | Values |
|---------------------+-------------------|
| c(v₁, v₂, ..., vₙ) | constructor value |
The entire pattern matching code can be represented as a clause matrix
that associates rows of patterns (p_{i,1}, p_{i,2}, ..., p_{i,n}) to
lambda code action lⁱ
\begin{equation*}
(P → L) =
\begin{pmatrix}
p_{1,1} & p_{1,2} & \cdots & p_{1,n} → l₁ \\
p_{2,1} & p_{2,2} & \cdots & p_{2,n} → l₂ \\
\vdots & \vdots & \ddots \vdots → \vdots \\
p_{m,1} & p_{m,2} & \cdots & p_{m,n} → lₘ
\end{pmatrix}
\end{equation*}
Most native data types in OCaml, such as integers, tuples, lists,
records, can be seen as instances of the following definition
#+BEGIN_SRC ocaml
type t = Nil | One of int | Cons of int * t
#+END_SRC
that is a type /t/ with three constructors that define its complete
signature.
Every constructor has an arity. Nil, a constructor of arity 0, is
called a constant constructor.
The pattern /p/ matches a value /v/, written as p ≼ v, when
one of the following rules apply
| _ | ≼ | v | |
| x | ≼ | v | |
| (p₁ \vert\ p₂) | ≼ | v | iff p₁ ≼ v or p₂ ≼ v |
| c(p₁, p₂, ..., pₐ) | ≼ | c(v₁, v₂, ..., vₐ) | iff (p₁, p₂, ..., pₐ) ≼ (v₁, v₂, ..., vₐ) |
| (p₁, p₂, ..., pₐ) | ≼ | (v₁, v₂, ..., vₐ) | iff pᵢ ≼ vᵢ ∀i ∈ [1..a] |
We can also say that /v/ is an /instance/ of /p/.
When we consider the pattern matrix P we say that the value vector
\vv{v} = (v₁, v₂, ..., vᵢ) matches the line number i in P if and only if the following two
conditions are satisfied:
- \[ p_{i,1} & p_{i,2} & \cdots & p_{i,n} \] ≼ (v₁, v₂, ..., vᵢ)
- \[ ∀j < i p_{j,1} & p_{j,2} & \cdots & p_{j,n} \] ⋠ (v₁, v₂, ..., vᵢ)
We can define the following three relations with respect to patterns:
- Patter p is less precise than pattern q, writtens p ≼ q when all
instances of q are instances of p
- Pattern p and q are equivalent, written p ≡ q, when their instances
are the same
- Patterns p and q are compatible when they share a common instance
** 1.2.1.1 Initial state of the compilation
Given a source of the following form:
#+BEGIN_SRC ocaml
match x with
| p₁ -> e₁
| p₂ -> e₂
...
| pₘ -> eₘ
#+END_SRC ocaml
the initial input of the algorithm consists of a vector of variables
\vv{x} = (x₁, x₂, ..., xₙ) of size n
and a clause matrix P → L of width n and height m.
\begin{equation*}
(P → L) =
\begin{pmatrix}
p_{1,1} & p_{1,2} & \cdots & p_{1,n} → l₁ \\
p_{2,1} & p_{2,2} & \cdots & p_{2,n} → l₂ \\
\vdots & \vdots & \ddots \vdots → \vdots \\
p_{m,1} & p_{m,2} & \cdots & p_{m,n} → lₘ
\end{pmatrix}
\end{equation*}

7
tesi/prova.out
View file

@ -1,3 +1,4 @@
\BOOKMARK [1][-]{section.1}{TODO Scaletta [1/2]}{}% 1
\BOOKMARK [1][-]{section.2}{Introduction}{}% 2
\BOOKMARK [2][-]{subsection.2.1}{TODO OCaml}{section.2}% 3
\BOOKMARK [1][-]{section.1}{TODO\040Scaletta\040[1/2]}{}% 1
\BOOKMARK [1][-]{section.2}{1.\040Background}{}% 2
\BOOKMARK [2][-]{subsection.2.1}{1.1\040OCaml}{section.2}% 3
\BOOKMARK [2][-]{subsection.2.2}{1.2.1.1\040Initial\040state\040of\040the\040compilation}{section.2}% 4

BIN
tesi/prova.pdf
View file

Binary file not shown.

260
tesi/prova.tex
View file

@ -1,4 +1,4 @@
% Created 2020-02-17 Mon 17:30
% Created 2020-02-19 Wed 16:42
% Intended LaTeX compiler: pdflatex
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
@ -18,6 +18,8 @@
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{amsmath,amssymb,amsthm}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\newtheorem{definition}{Definition}
\usepackage{graphicx}
\usepackage{listings}
@ -36,12 +38,13 @@
\maketitle
\section{{\bfseries\sffamily TODO} Scaletta [1/2]}
\label{sec:org5a6f376}
\label{sec:org6c3943f}
\begin{itemize}
\item[{$\boxtimes$}] Abstract
\item[{$\square$}] Introduction [0\%]
\item[{$\boxminus$}] Background [25\%]
\begin{itemize}
\item[{$\square$}] Ocaml
\item[{$\boxtimes$}] Ocaml
\item[{$\square$}] Lambda code
\item[{$\square$}] Pattern matching
\item[{$\square$}] Translation Verification
\item[{$\square$}] Symbolic execution
@ -64,19 +67,20 @@ blackboxes that are not evaluated in the context of the verification.
\end{abstract}
\section{Introduction}
\label{sec:orgef00ecd}
\section{1. Background}
\label{sec:orgad08c62}
\subsection{{\bfseries\sffamily TODO} OCaml}
\label{sec:org5659ec2}
\subsection{1.1 OCaml}
\label{sec:orgca8d200}
Objective Caml (OCaml) is a dialect of the ML (Meta-Language) family of programming
languages.
OCaml shares many features with other dialects of ML, such as SML and Caml Light,
The main features of ML languages are the use of the Hindley-Milner type system that
provides with respect to static type systems of traditional imperative and/or object
oriented language such as C, C++ and Java many advantages such as:
provides many advantages with respect to static type systems of traditional imperative and object
oriented language such as C, C++ and Java, such as:
\begin{itemize}
\item Parametric polymorphism: in certain scenarios a function can accept more than one
\end{itemize}
type for the input parameters. For example a function that computes the lenght of a
list doesn't need to inspect the type of the elements of the list and for this reason
a List.length function can accept list of integers, list of strings and in general
@ -87,12 +91,246 @@ With the Hindley-Milner type system each well typed function can have more than
type but always has a unique best type, called the \emph{principal type}.
For example the principal type of the List.length function is "For any \emph{a}, function from
list of \emph{a} to \emph{int}" and \emph{a} is called the \emph{type parameter}.
\begin{itemize}
\item Strong typing: Languages such as C and C++ allow the programmer to operate on data
\end{itemize}
without considering its type, mainly through pointers. Other languages such as C\#
and Go allow type erasure so at runtime the type of the data can't be queried.
In the case of programming languages using an Hindley-Milner type system the
programmer is not allowed to operate on data by ignoring or promoting its type.
\begin{itemize}
\item Type Inference: the principal type of a well formed term can be inferred without any
annotation or declaration.
\end{itemize}
annotation or declaration.
\begin{itemize}
\item Algebraic data types: types that are modelled by the use of two
\end{itemize}
algebraic operations, sum and product.
A sum type is a type that can hold of many different types of
objects, but only one at a time. For example the sum type defined
as \emph{A + B} can hold at any moment a value of type A or a value of
type B. Sum types are also called tagged union or variants.
A product type is a type constructed as a direct product
of multiple types and contains at any moment one instance for
every type of its operands. Product types are also called tuples
or records. Algebraic data types can be recursive
in their definition and can be combined.
Moreover ML languages are functional, meaning that functions are
treated as first class citizens and variables are immutable,
although mutable statements and imperative constructs are permitted.
In addition to that OCaml features an object system, that provides
inheritance, subtyping and dynamic binding, and modules, that
provide a way to encapsulate definitions. Modules are checked
statically and can be reificated through functors.
\begin{enumerate}
\item {\bfseries\sffamily TODO} 1.2 Pattern matching [37\%]
\label{sec:org83a2e95}
\begin{itemize}
\item[{$\square$}] capisci come mettere gli esempi uno accanto all'altro
\end{itemize}
Pattern matching is a widely adopted mechanism to interact with ADT.
C family languages provide branching on predicates through the use of
if statements and switch statements.
Pattern matching is a mechanism for destructuring and analyzing data
structures for the presence of values simbolically represented as
tokens. One common example of pattern matching is the use of regular
expressions on strings. OCaml provides pattern matching on ADT,
primitive data types.
\begin{itemize}
\item[{$\boxtimes$}] Esempio enum, C e Ocaml
\end{itemize}
\begin{verbatim}
type color = | Red | Blue | Green
begin match color with
| Red -> print "red"
| Blue -> print "red"
| Green -> print "red"
\end{verbatim}
OCaml provides tokens to express data destructoring
\begin{itemize}
\item[{$\boxtimes$}] Esempio destructor list
\end{itemize}
\begin{verbatim}
begin match list with
| [ ] -> print "empty list"
| element1 :: [ ] -> print "one element"
| element1 :: element2 :: [ ] -> print "two elements"
| head :: tail-> print "head followed by many elements"
\end{verbatim}
\begin{itemize}
\item[{$\boxtimes$}] Esempio destructor tuples
\end{itemize}
\begin{verbatim}
begin match tuple with
| (Some _, Some _) -> print "Pair of optional types"
| (Some _, None) -> print "Pair of optional types, last null"
| (None, Some _) -> print "Pair of optional types, first null"
| (None, None) -> print "Pair of optional types, both null"
\end{verbatim}
Pattern clauses can make the use of \emph{guards} to test predicates and
variables can be binded in scope.
\begin{itemize}
\item[{$\square$}] Esempio binding e guards
\end{itemize}
\begin{verbatim}
begin match token_list with
| "switch"::var::"{"::rest ->
| "case"::":"::var::rest when is_int var ->
| "case"::":"::var::rest when is_string var ->
| "}"::[ ] -> stop ()
| "}"::rest -> error "syntax error: " rest
\end{verbatim}
\begin{itemize}
\item[{$\square$}] Un altro esempio con destructors e tutto i lresto
\end{itemize}
In general pattern matching on primitive and algebraic data types takes the
following form.
\begin{itemize}
\item[{$\square$}] Esempio informale
\end{itemize}
It can be described more formally through a BNF grammar.
\begin{itemize}
\item[{$\square$}] BNF
\item[{$\square$}] Come funziona il pattern matching?
\end{itemize}
\item {\bfseries\sffamily TODO} 1.2.1 Pattern matching compilation to lambda code
\label{sec:org2127ffb}
\begin{itemize}
\item[{$\square$}] Da tabella a matrice
\end{itemize}
Formally, pattern are defined as follows:
\begin{center}
\begin{tabular}{ll}
pattern ::= & Patterns\\
\hline
\_ & wildcard\\
x & variable\\
c(p₁,p₂,\ldots{},pₙ & constructor pattern\\
(p₁\(\vert{}\) p₂) & or-pattern\\
\end{tabular}
\end{center}
Values are defined as follows:
\begin{center}
\begin{tabular}{ll}
values ::= & Values\\
\hline
c(v₁, v₂, \ldots{}, vₙ) & constructor value\\
\end{tabular}
\end{center}
The entire pattern matching code can be represented as a clause matrix
that associates rows of patterns (p\(_{\text{i,1}}\), p\(_{\text{i,2}}\), \ldots{}, p\(_{\text{i,n}}\)) to
lambda code action lⁱ
\begin{equation*}
(P → L) =
\begin{pmatrix}
p_{1,1} & p_{1,2} & \cdots & p_{1,n} → l₁ \\
p_{2,1} & p_{2,2} & \cdots & p_{2,n} → l₂ \\
\vdots & \vdots & \ddots \vdots → \vdots \\
p_{m,1} & p_{m,2} & \cdots & p_{m,n} → lₘ
\end{pmatrix}
\end{equation*}
Most native data types in OCaml, such as integers, tuples, lists,
records, can be seen as instances of the following definition
\begin{verbatim}
type t = Nil | One of int | Cons of int * t
\end{verbatim}
that is a type \emph{t} with three constructors that define its complete
signature.
Every constructor has an arity. Nil, a constructor of arity 0, is
called a constant constructor.
The pattern \emph{p} matches a value \emph{v}, written as p ≼ v, when
one of the following rules apply
\begin{center}
\begin{tabular}{llll}
\_ & ≼ & v & \\
x & ≼ & v & \\
(p₁ \(\vert{}\)$\backslash$ p₂) & ≼ & v & iff p₁ ≼ v or p₂ ≼ v\\
c(p₁, p₂, \ldots{}, pₐ) & ≼ & c(v₁, v₂, \ldots{}, vₐ) & iff (p₁, p₂, \ldots{}, pₐ) ≼ (v₁, v₂, \ldots{}, vₐ)\\
(p₁, p₂, \ldots{}, pₐ) & ≼ & (v₁, v₂, \ldots{}, vₐ) & iff pᵢ ≼ vᵢ ∀i ∈ [1..a]\\
\end{tabular}
\end{center}
We can also say that \emph{v} is an \emph{instance} of \emph{p}.
When we consider the pattern matrix P we say that the value vector
\vv{v} = (v₁, v₂, \ldots{}, vᵢ) matches the line number i in P if and only if the following two
conditions are satisfied:
\begin{itemize}
\item \[ p_{i,1} & p_{i,2} & \cdots & p_{i,n} \] ≼ (v₁, v₂, \ldots{}, vᵢ)
\item \[ ∀j < i p_{j,1} & p_{j,2} & \cdots & p_{j,n} \] ⋠ (v₁, v₂, \ldots{}, vᵢ)
\end{itemize}
We can define the following three relations with respect to patterns:
\begin{itemize}
\item Patter p is less precise than pattern q, writtens p ≼ q when all
instances of q are instances of p
\item Pattern p and q are equivalent, written p ≡ q, when their instances
are the same
\item Patterns p and q are compatible when they share a common instance
\end{itemize}
\end{enumerate}
\subsection{1.2.1.1 Initial state of the compilation}
\label{sec:org0b0c254}
Given a source of the following form:
\#+BEGIN\_SRC ocaml
match x with
\begin{center}
\begin{tabular}{l}
p₁ -> e₁\\
p₂ -> e₂\\
\end{tabular}
\end{center}
\ldots{}
\begin{center}
\begin{tabular}{l}
pₘ -> eₘ\\
\end{tabular}
\end{center}
\#+END\_SRC ocaml
the initial input of the algorithm consists of a vector of variables
\vv{x} = (x₁, x₂, \ldots{}, xₙ) of size n
and a clause matrix P → L of width n and height m.
\begin{equation*}
(P → L) =
\begin{pmatrix}
p_{1,1} & p_{1,2} & \cdots & p_{1,n} → l₁ \\
p_{2,1} & p_{2,2} & \cdots & p_{2,n} → l₂ \\
\vdots & \vdots & \ddots \vdots → \vdots \\
p_{m,1} & p_{m,2} & \cdots & p_{m,n} → lₘ
\end{pmatrix}
\end{equation*}
\end{document}

BIN
tesi/referenze/opt-pat.pdf Normal file
View file

Binary file not shown.