diff --git a/anno3/logica/EsameLogica_v4_soluzioni.pdf b/anno3/logica/EsameLogica_v4_soluzioni.pdf new file mode 100644 index 0000000..866d71b Binary files /dev/null and b/anno3/logica/EsameLogica_v4_soluzioni.pdf differ diff --git a/tesi/prova.aux b/tesi/prova.aux index f9dd2bd..652b85a 100644 --- a/tesi/prova.aux +++ b/tesi/prova.aux @@ -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<>} \@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}{}} diff --git a/tesi/prova.bbl b/tesi/prova.bbl deleted file mode 100644 index e69de29..0000000 diff --git a/tesi/prova.blg b/tesi/prova.blg deleted file mode 100644 index 69ab818..0000000 --- a/tesi/prova.blg +++ /dev/null @@ -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) diff --git a/tesi/prova.log b/tesi/prova.log index 9ec79ea..255966f 100644 --- a/tesi/prova.log +++ b/tesi/prova.log @@ -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 &. + & + +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 &. + & + +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: -(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} -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). diff --git a/tesi/prova.md b/tesi/prova.md new file mode 100644 index 0000000..d7f71c1 --- /dev/null +++ b/tesi/prova.md @@ -0,0 +1,320 @@ + +# TODO Scaletta [1/2] + +- [X] Abstract +- [-] Background [25%] + - [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 [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 + + 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: + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
pattern ::=Patterns
\_wildcard
xvariable
c(p1,p2,…,pnconstructor pattern
(p1| p2)or-pattern
+ + + + + + + + + + + + + + + + + + + + + + +
values ::=Values
c(v1, v2, …, vn)constructor value
+ + The entire pattern matching code can be represented as a clause matrix + that associates rows of patterns (pi,1, pi,2, …, pi,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 + + 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 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
\_≼v 
x≼v 
(p₁ |\\ p₂)≼viff 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 + diff --git a/tesi/prova.org b/tesi/prova.org index f46f443..5dd2bbc 100644 --- a/tesi/prova.org +++ b/tesi/prova.org @@ -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*} diff --git a/tesi/prova.out b/tesi/prova.out index 946788b..ac99723 100644 --- a/tesi/prova.out +++ b/tesi/prova.out @@ -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 diff --git a/tesi/prova.pdf b/tesi/prova.pdf index 85a9192..ca95d00 100644 Binary files a/tesi/prova.pdf and b/tesi/prova.pdf differ diff --git a/tesi/prova.tex b/tesi/prova.tex index 9dad6ba..bed774a 100644 --- a/tesi/prova.tex +++ b/tesi/prova.tex @@ -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} diff --git a/tesi/referenze/opt-pat.pdf b/tesi/referenze/opt-pat.pdf new file mode 100644 index 0000000..bc0b518 Binary files /dev/null and b/tesi/referenze/opt-pat.pdf differ