diff --git a/tesi/conv.py b/tesi/conv.py index 20477f4..15f2be9 100644 --- a/tesi/conv.py +++ b/tesi/conv.py @@ -3,8 +3,8 @@ import re from sys import argv allsymbols = json.load(open('./unicode-latex.json')) -mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒' ] -extrasymbols = {'〚': '\llbracket', '〛': '\rrbracket'} +mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', 'ε', '₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈' ] +extrasymbols = {'〚': '\llbracket', '〛': r'\rrbracket', '̸': '\neg', '¬̸': '\neg', '∈': '\in ', 'ₛ': '_S', 'ₜ': '_T'} symbols = {s: allsymbols[s] for s in mysymbols} symbols.update(extrasymbols) @@ -13,8 +13,8 @@ mathsymbols = {s: '$'+v+'$' for s, v in symbols.items()} def read_by_char(fname): # Yield character and True/False if inside mathmode block mathmode = False - mathmode_begin = set(['\\begin{equation*}', '\\begin{equation}']) - mathmode_end = set(['\\end{equation*}', '\\end{equation}']) + mathmode_begin = set(['\\begin{equation*}', '\\begin{equation}', '\[', '\\begin{mathpar}']) + mathmode_end = set(['\\end{equation*}', '\\end{equation}', '\]', '\\end{mathpar}']) cnt = 0 with open(fname, 'r') as fp: for line in fp.readlines(): @@ -50,11 +50,26 @@ def latex_errors_replacements(charlist): yield from word yield ' ' +def ll_rr_bracket(charlist): + llrr_mode = False + + for i, ch in enumerate(charlist): + if ch == '\\': + if charlist[i:i+10] == '\llbracket': + assert llrr_mode is False ; llrr_mode = True + elif charlist[i:i+10] == '\rrbracket': + assert llrr_mode is True ; llrr_mode = False + + if not (llrr_mode and ch == '$'): + yield ch + + # convert symbols except the one requiring math mode modifiers firstpass = [convert(*c) for c in read_by_char(argv[1])] # remove a latex error secondpass = latex_errors_replacements(firstpass) +thirdpass = ll_rr_bracket(list(secondpass)) -newfile = ''.join(secondpass) +newfile = ''.join(thirdpass) with open(argv[2], 'w') as f: f.write(newfile) diff --git a/tesi/files/symb_exec b/tesi/files/symb_exec new file mode 100644 index 0000000..e14d607 --- /dev/null +++ b/tesi/files/symb_exec @@ -0,0 +1 @@ +7VpLk+I2EP41rpoccFnyA/sIDJsckspjDsnuJaWxBahiW0QWC+yvj2RLfsmzDCwBdoYqCqyvpZb0dUvqlrHcWbb7kaH16hea4NSCTrKz3EcLwjAIxLcE9hXgRVEFLBlJKgg0wBP5ghXoKHRDElx0KnJKU07WXTCmeY5j3sEQY3TbrbagabfXNVpiA3iKUWqif5KEr9S0fKfBf8JkudI9A0dJMqQrK6BYoYRuW5A7t9wZo5RXT9luhlPJnealavfhBWk9MIZz/poGPz99+n3y6dcYzpztl+c/wH7ERiOl5TNKN2rCMc3WiAvswbbtH9TQ+V7zwegmT7BUCSx3ul0Rjp/WKJbSrXAAga14liqxUo4Zx7sXRw1qLoQPYZphzvaiimrgavq0/6jitjFGTfmqZQhdDyn7L2vNDUXiQbF0BGPQYMzyp8DyHw2qxKR5l4+CM/oPntGUMoHkNBc1pwuSpj0IpWSZi2IsSMICn0oKiXDKiRJkJElkN4MGaEzknMcGMOzawDdt4A2YAP5fJnBNE4zFPEV3QSoZL9Yo75gi+HcjV9k0xQvxMxEy33Ns33PXO9lMkiR2lXUlGvuBDUPYEi1ozkdFuTXJCiC0QQjCfoUFyki6r6oUKC9GBWZk0XQunpbl7+yDFdZjFQRUw1VCBUuNUo/eD7USMKBPz3rzbECvIMJ37MgZDxIRQNtzjHm2iACnczC3yrl8jQMJm3MSaEWOgsu+RtYcWmFoRfPKDVAmF4Kq7+jeBiTtZuM3vIS94OASBuNLrmHPXMN98nGeTOQJLllMUVGQuGsKvCP8L0mR7avSx5bkcafYKwt7XcjF4FuNZPFjW9Y0K0v7jglwYgQLPQOICdANi/HhI5cjtsT8K/WCYYO2LOYPGExjDKeIk8/d4Q5ZUfXwGyXljqOPXa/rL7VzaBXVNFWrdtTRV9RzPND3qIoHQ1HpVPW0T/ezwPCzjMg98aHcht1yAxAfQdCs3CnaILy98Kem72rxz3go/oHvKv4B7pUDoPAMAVDg2KEDjwiAXn22HzGIUGzDbnizUdgL8ImR1hjYILh8pFXuaKdEWm89Br1Q9Dl00hjHzIHQ1L2nN9+Va91KeiMl8CQHus5mdWDf/f5PlBO9OJJePLychTWCzkrvzSr6JieGxzlxqdS27bedS/uHw8E67blIPBgZ8WCMCv6w+VskVfJwuc2rXOhcO5cB5vX3e7mFCF55CxHd0i1E/Vbo6FuIqLdkg8veQoDBtwbuu8qaa+NdK2sG53hvcE+b72nzPW0+S1bjWCrLjayJZ9WJ8j0bfmsec8+G79nwPRt+o2GeB/2DYV4dfl8mzvO/Pas7Y6Z13Qxq3AvCo1MzqL6i8MIZlPkiV686ohccw4UcMV3ILWGFpQF3ON5wQnNd95kNrFnSYLd2RRKai+lcVySi2Pz5sDJT8w9Od/4f \ No newline at end of file diff --git a/tesi/files/symb_exec.png b/tesi/files/symb_exec.png new file mode 100644 index 0000000..365c1cd Binary files /dev/null and b/tesi/files/symb_exec.png differ diff --git a/tesi/files/symb_exec.svg b/tesi/files/symb_exec.svg new file mode 100644 index 0000000..b73b319 --- /dev/null +++ b/tesi/files/symb_exec.svg @@ -0,0 +1,3 @@ + + +
compat (...)
compat (...)
[1]
[1]
{ πα: -∞ < α < ∞ }
{ πα: -∞ < α < ∞ }
min (σ₁, σ₂)
min (σ₁, σ₂)
[2]
[2]
{ πσ: -∞ < (σ₁,σ₂) < ∞ ; πα: -∞ < α < β ; πβ: ...}
{ πσ: -∞ < (σ₁,σ₂) < ∞ ; πα: -∞ < α < β ; πβ: ...}
cast(u_int) (...)
cast(u_int) (...)
[3]
[3]
{ πσ: 0 ≤ (σ) < ∞ ; πα: -∞ < α < β ; πβ: ...}
{ πσ: 0 ≤ (σ) < ∞ ; πα: -∞ < α < β ; πβ: ...}
rest of the execution
rest of the exec...Viewer does not support full SVG 1.1 \ No newline at end of file diff --git a/tesi/mathpartir.sty b/tesi/mathpartir.sty new file mode 100644 index 0000000..bcd26a1 --- /dev/null +++ b/tesi/mathpartir.sty @@ -0,0 +1,469 @@ +%% +%% This is file `mathpartir.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% mathpartir.dtx (with options: `package') +%% +%% This is a generated file. +%% +%% Copyright (C) 2015, 2020 by Didier Remy +%% +%% This file is part of mathpartir. +%% +%% mathpartir is free software: you can redistribute it and/or modify +%% it under the terms of the GNU General Public License as published by +%% the Free Software Foundation, either version 2 of the License, or +%% (at your option) any later version. +%% +%% mathpartir is distributed in the hope that it will be useful, +%% but WITHOUT ANY WARRANTY; without even the implied warranty of +%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +%% GNU General Public License for more details. +%% +%% You should have received a copy of the GNU General Public License +%% along with mathpartir. If not, see . +%% +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{mathpartir} + [2020/02/15 version 1.4.0 Math Paragraph for Typesetting Inference Rules] +%% Identification +%% Preliminary declarations + +\RequirePackage {keyval} + +%% Options +%% More declarations + +%% PART I: Typesetting maths in paragraphe mode + +%% \newdimen \mpr@tmpdim +%% Dimens are a precious ressource. Uses seems to be local. +\let \mpr@tmpdim \@tempdima + +\let \mpr@hva \empty + +%% normal paragraph parametters, should rather be taken dynamically +\def \mpr@savepar {% + \edef \MathparNormalpar + {\noexpand \lineskiplimit \the\lineskiplimit + \noexpand \lineskip \the\lineskip}% + } + +\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em} +\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em} +\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} +\let \MathparLineskip \mpr@lineskip +\def \mpr@paroptions {\MathparLineskip} +\let \mpr@prebindings \relax + +\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em + +\def \mpr@goodbreakand + {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip} +\def \mpr@and {\hskip \mpr@andskip} +\def \mpr@andcr {\penalty 50\mpr@and} +\def \mpr@cr {\penalty -10000\mpr@and} +\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10} + +\def \mpr@bindings {% + \let \and \mpr@andcr + \let \par \mpr@andcr + \let \\\mpr@cr + \let \eqno \mpr@eqno + \let \hva \mpr@hva + } +\let \MathparBindings \mpr@bindings +\def \MathparBeginhook {} +\def \MathparEndhook {} + +\let \MathparCentering \centering +\newenvironment{mathpar}[1][] + {$$ + \MathparBeginhook + %% We save \lineskip parameters so that the user can restore them + %% inside math \MathparNormalpar + \mpr@savepar + %% We define the shape of the paragrah + \parskip 0em \hsize \linewidth \MathparCentering + \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else + \noindent $\displaystyle\fi + \MathparBindings} + {\MathparEndhook \unskip \ifmmode $\fi\egroup $$\ignorespacesafterend} + +\newenvironment{mathparpagebreakable}[1][] + {\begingroup + \par + \mpr@savepar \parskip 0em \hsize \linewidth \centering + \mpr@prebindings \mpr@paroptions #1% + \vskip \abovedisplayskip \vskip -\lineskip% + \ifmmode \else $\displaystyle\fi + \MathparBindings + } + {\unskip + \ifmmode $\fi \par\endgroup + \vskip \belowdisplayskip + \noindent + \ignorespacesafterend} + + +%%% HOV BOXES + +\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip + \vbox \bgroup \tabskip 0em \let \\ \cr + \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup + \egroup} + +\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize + \box0\else \mathvbox {#1}\fi} + +%% Part II -- operations on lists + +\newtoks \mpr@lista +\newtoks \mpr@listb + +\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter +{#2}\edef #2{\the \mpr@lista \the \mpr@listb}} + +\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter +{#2}\edef #2{\the \mpr@listb\the\mpr@lista}} + +\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb +\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}} + +\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2} +\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}} + +\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2} +\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}} + +\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}% + \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the + \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty + \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop + \mpr@flatten \mpr@all \mpr@to \mpr@one + \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof + \mpr@all \mpr@stripend + \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi + \ifx 1\mpr@isempty + \repeat +} + +\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty + \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp} + +%% Part III -- Type inference rules + +\newif \if@premisse +\newbox \mpr@hlist +\newbox \mpr@vlist +\newif \ifmpr@center \mpr@centertrue +\def \mpr@vskip {} +\let \mpr@vbox \vbox +\def \mpr@htovlist {% + \setbox \mpr@hlist + \hbox {\strut + \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi + \unhbox \mpr@hlist}% + \setbox \mpr@vlist + \mpr@vbox {\if@premisse + \box \mpr@hlist + \ifx \mpr@vskip \empty \else + \hrule height 0em depth \mpr@vskip width 0em + \fi + \unvbox \mpr@vlist + \else + \unvbox \mpr@vlist + \ifx \mpr@vskip \empty \else + \hrule height 0em depth \mpr@vskip width 0em + \fi + \box \mpr@hlist + \fi}% +} + +\def \mpr@item #1{$\displaystyle #1$} +\def \mpr@sep{2em} +\def \mpr@blank { } +\def \mpr@hovbox #1#2{\hbox + \bgroup + \ifx #1T\@premissetrue + \else \ifx #1B\@premissefalse + \else + \PackageError{mathpartir} + {Premisse orientation should either be T or B} + {Fatal error in Package}% + \fi \fi + \def \@test {#2}\ifx \@test \mpr@blank\else + \setbox \mpr@hlist \hbox {}% + \setbox \mpr@vlist \vbox {}% + \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi + \let \@hvlist \empty \let \@rev \empty + \mpr@tmpdim 0em + \expandafter \mpr@makelist #2\mpr@to \mpr@flat + \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi + \def \\##1{% + \def \@test {##1}\ifx \@test \empty + \mpr@htovlist + \mpr@tmpdim 0em %%% last bug fix not extensively checked + \else + \setbox0 \hbox{\mpr@item {##1}}\relax + \advance \mpr@tmpdim by \wd0 + %\mpr@tmpdim 1.02\mpr@tmpdim + \ifnum \mpr@tmpdim < \hsize + \ifnum \wd\mpr@hlist > 0 + \if@premisse + \setbox \mpr@hlist + \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}% + \else + \setbox \mpr@hlist + \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}% + \fi + \else + \setbox \mpr@hlist \hbox {\unhbox0}% + \fi + \else + \ifnum \wd \mpr@hlist > 0 + \mpr@htovlist + \mpr@tmpdim \wd0 + \fi + \setbox \mpr@hlist \hbox {\unhbox0}% + \fi + \advance \mpr@tmpdim by \mpr@sep + \fi + }% + \@rev + \mpr@htovlist + \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist + \fi + \egroup +} + +%%% INFERENCE RULES + +\@ifundefined{@@over}{% + \let\@@over\over % fallback if amsmath is not loaded + \let\@@overwithdelims\overwithdelims + \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims + \let\@@above\above \let\@@abovewithdelims\abovewithdelims + }{} + +%% The default + +\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em + $\displaystyle {#1\mpr@over #2}$}} +\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em + $\displaystyle {#1\@@atop #2}$}} + +\let \mpr@fraction \mpr@@fraction + +%% A generic solution to arrow + +\def \mpr@@fractionaboveskip {0ex} +\def \mpr@@fractionbelowskip {0.22ex} + +\def \mpr@make@fraction #1#2#3#4#5{\hbox {% + \def \mpr@tail{#1}% + \def \mpr@body{#2}% + \def \mpr@head{#3}% + \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}% + \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}% + \dimen0\ht3\advance\dimen0 by \dp3\relax + \dimen0 0.5\dimen0\relax + \advance \dimen0 by \mpr@@fractionaboveskip + \setbox1=\hbox {\raise \dimen0 \box1}\relax + \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0 + \advance \dimen0 by \mpr@@fractionbelowskip + \setbox2=\hbox {\lower \dimen0 \box2}\relax + \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}% + \dimen0=\wd0\box0 + \box0 \hskip -\dimen0\relax + \hbox to \dimen0 {$%\color{blue} + \mathrel{\mpr@tail}\joinrel + \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}% + $}}} + +%% Old stuff should be removed in next version +\def \mpr@@nothing #1#2 + {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$} +\def \mpr@@reduce #1#2{\hbox + {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}} +\def \mpr@@rewrite #1#2#3{\hbox + {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}} +\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}} + +\def \mpr@empty {} +\def \mpr@inferrule + {\bgroup + \ifnum \linewidth<\hsize \hsize \linewidth\fi + \mpr@rulelineskip + \let \and \qquad + \let \hva \mpr@hva + \let \@rulename \mpr@empty + \let \@rule@options \mpr@empty + \let \mpr@over \@@over + \mpr@inferrule@} +\newcommand {\mpr@inferrule@}[3][] + {\everymath={\displaystyle}% + \def \@test {#2}\ifx \empty \@test + \def \@test {#3}\ifx \empty \@test + \PackageWarning {mathpartir} + {\string\inferrule\space empty arguments substituted}{}% + \setbox0 \mpr@fraction {?}{?}% + \else + \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}% + \fi + \else + \def \@test {#3}\ifx \empty \@test + \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}% + \else + \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}% + \fi \fi + \def \@test {#1}\ifx \@test\empty \box0 + \else \vbox +%%% Suggestion de Francois pour les etiquettes longues +%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi + {\hbox {\DefTirName {#1}}\box0}\fi + \egroup} + +\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} + + +%% Version for Hoare triples + +\def \triple@hlinebox{\noalign{\setbox0\hbox {}\dp0 0.1ex\ht0 0.1ex\box0}} +\def \triple@hline {\triple@hlinebox\hline\triple@hlinebox} + +\newcommand{\triplerule}[4][] + {\bgroup + \ifnum \linewidth<\hsize \hsize \linewidth\fi + \mpr@rulelineskip + \let \and \qquad + \let \hva \mpr@hva + \setbox0 \hbox {\begin{array}[b]{@{}c@{}} + \mpr@hovbox{T}{#2}\cr\triple@hline + \mpr@hovbox{T}{#3}\cr\triple@hline + \let \mpr@vbox \vtop \ht0 0em + \setbox0 \strut \@tempdima \ht0 + \setbox0 \mpr@hovbox{B}{#4}\advance \@tempdima by -\ht0 + \setbox0 \hbox{\raise \@tempdima \box0}\box0 + \end{array}}% + \def \@test {#1}\ifx \@test\empty \box0 + \else \vbox + %%% Suggestion de Francois pour les etiquettes longues + %%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi + {\hbox {\DefTirName {#1}}\box0}\fi + \egroup} + + +%% Keys that make sence in all kinds of rules +\def \mprset #1{\setkeys{mprset}{#1}} +\define@key {mprset}{andskip}[]{\mpr@andskip=#1} +\define@key {mprset}{lineskip}[]{\lineskip=#1} +\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip} +\define@key {mprset}{flushleft}[]{\mpr@centerfalse} +\define@key {mprset}{center}[]{\mpr@centertrue} +\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} +\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction} +\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1} +\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} +\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction} +\define@key {mprset}{sep}{\def\mpr@sep{#1}} +\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}} +\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}} +\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def} +\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}} +\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} +\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}} + +\newbox \mpr@right +\define@key {mpr}{flushleft}[]{\mpr@centerfalse} +\define@key {mpr}{center}[]{\mpr@centertrue} +\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} +\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1} +\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} +\define@key {mpr}{width}{\hsize #1} +\define@key {mpr}{sep}{\def\mpr@sep{#1}} +\define@key {mpr}{before}{#1} +\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} +\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} +\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def} +\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}} +\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} +\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}} +\define@key {mpr}{narrower}{\hsize #1\hsize} +\define@key {mpr}{leftskip}{\hskip -#1} +\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce} +\define@key {mpr}{rightskip} + {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}} +\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax + \advance \hsize by -\wd0\box0} + +\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax + \advance \hsize by -\wd0\box0} +\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}} +\define@key {mpr}{right} + {\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0 + \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} +\define@key {mpr}{RIGHT} + {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0 + \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} +\define@key {mpr}{Right} + {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}} +\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} +\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} +\define@key {mpr}{vcenter}[]{\mpr@vcentertrue} + +\newif \ifmpr@vcenter \mpr@vcenterfalse +\newcommand \mpr@inferstar@ [3][]{\begingroup + \setbox0 \hbox + {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax + \setbox \mpr@right \hbox{}% + \setkeys{mpr}{#1}% + $\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else + \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi + \box \mpr@right \mpr@vdots$ + \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi} + \ifmpr@vcenter + \box0 + \else + \setbox1 \hbox {\strut} + \@tempdima \dp0 \advance \@tempdima by -\dp1 + \raise \@tempdima \box0 + \fi + \endgroup} + +\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}} +\newcommand \mpr@err@skipargs[3][]{} +\def \mpr@inferstar*{\ifmmode + \let \@do \mpr@inferstar@ + \else + \let \@do \mpr@err@skipargs + \PackageError {mathpartir} + {\string\inferrule* can only be used in math mode}{}% + \fi \@do} + +%%% Exports + + +\let \inferrule \mpr@infer + +\@ifundefined {infer}{\let \infer \mpr@infer}{} + +\def \TirNameStyle #1{\small \textsc{#1}} +\def \LeftTirNameStyle #1{\TirNameStyle {#1}} +\def \RightTirNameStyle #1{\TirNameStyle {#1}} + +\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}} +\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}} +\let \TirName \lefttir@name +\let \LeftTirName \lefttir@name +\let \DefTirName \lefttir@name +\let \LabTirName \lefttir@name +\let \RightTirName \righttir@name + +%%% Other Exports + +\endinput +%% +%% End of file `mathpartir.sty'. diff --git a/tesi/mumble_meeting_gabriel b/tesi/mumble_meeting_gabriel index 3436c00..d299e58 100644 --- a/tesi/mumble_meeting_gabriel +++ b/tesi/mumble_meeting_gabriel @@ -12,7 +12,7 @@ Test(S,true) = Yes ------------------------------- -equiv \emptyset Cs Ct gs ~> Yes +equiv \emptyset Cs Ct gs \to Yes ----------------------------------------- equiv S Failure (Leaf BBt) gs ~>No(vs, vt) diff --git a/tesi/notations.sty b/tesi/notations.sty new file mode 100644 index 0000000..a7c051c --- /dev/null +++ b/tesi/notations.sty @@ -0,0 +1,36 @@ +\newcommand{\bnfeq}{\mathrel{::=}\;} +\newcommand{\bnfor}{\mathrel{\vert}} + +\newcommand{\paramrel}[3]{#2 \mathrel{\approx_{#1}} #3} +\newcommand{\vrel}[2]{\paramrel{\mathsf{val}}{#1}{#2}} +\newcommand{\trel}[2]{\paramrel{\mathsf{term}}{#1}{#2}} + +\newcommand{\sem}[1]{{\llbracket{#1}\rrbracket}} + +\newcommand{\Fam}[2]{{(#2)}^{#1}} + +\newcommand{\match}[2]{\mathtt{match}(#1,#2)} + +\newcommand{\var}[1]{\mathtt{#1}} +\newcommand{\pK}{\mathtt{K}} +\newcommand{\any}{\mathtt{\_}} + +% \equiv is already taken +\newcommand{\Equiv}[4]{\mathsf{equiv}(#1, #2, #3, #4)} +\newcommand{\Equivrel}[4]{#1 \vdash_{#4} #2 \approx #3} + +\newcommand{\covers}[2]{#1 \mathrel{\mathsf{covers}} #2} + +\newcommand{\Yes}{\mathsf{Yes}} +\newcommand{\No}[2]{\mathsf{No}(#1, #2)} + +\newcommand{\Leaf}[1]{\mathsf{Leaf}(#1)} +\newcommand{\Failure}{\mathsf{Failure}} +\newcommand{\Switch}[3]{\mathsf{Switch}(#1, #2, #3)} +\newcommand{\Guard}[3]{\mathsf{Guard}(#1, #2, #3)} + +\newcommand{\emptyqueue}{\mathord{[]}} + +\newcommand{\Cfb}{C_{\mathsf{fb}}} + +\newcommand{\trim}[2]{\mathsf{trim}(#1, #2)} \ No newline at end of file diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf index 7089d0d..aba1c5e 100644 Binary files a/tesi/tesi.pdf and b/tesi/tesi.pdf differ diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index 336adb1..d718580 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -1,11 +1,11 @@ \begin{comment} * TODO Scaletta [1/6] - [X] Introduction - - [-] Background [60%] + - [-] Background [80%] - [X] Low level representation - [X] Lambda code [0%] - [X] Pattern matching - - [ ] Symbolic execution + - [X] Symbolic execution - [ ] Translation Validation - [ ] Translation validation of the Pattern Matching Compiler - [ ] Source translation @@ -31,6 +31,7 @@ Magari prima pattern matching poi compilatore? #+LANGUAGE: en #+LaTeX_CLASS: article +#+LaTeX_HEADER: \linespread{1.25} #+LaTeX_HEADER: \usepackage{algorithm} #+LaTeX_HEADER: \usepackage{comment} #+LaTeX_HEADER: \usepackage{algpseudocode} @@ -41,11 +42,32 @@ Magari prima pattern matching poi compilatore? #+LaTeX_HEADER: \usepackage{listings} #+LaTeX_HEADER: \usepackage{color} #+LaTeX_HEADER: \usepackage{stmaryrd} -#+LaTeX_HEADER: \newcommand{\sem}[1]{{\llbracket{#1}\rrbracket}} -#+LaTeX_HEADER: \newcommand{\Equiv}[3]{\mathsf{equiv}(#1, #2, #3)} % \equiv is already taken -#+LaTeX_HEADER: \newcommand{\covers}[2]{#1 \mathrel{\mathsf{covers}} #2} -#+LaTeX_HEADER: \newcommand{\Yes}{\mathsf{Yes}} -#+LaTeX_HEADER: \newcommand{\No}[2]{\mathsf{No}(#1, #2)} +#+LaTeX_HEADER: \newcommand{\semTEX}[1]{{\llbracket{#1}\rrbracket}} +#+LaTeX_HEADER: \newcommand{\EquivTEX}[3]{\mathsf{equiv}(#1, #2, #3)} % \equiv is already taken +#+LaTeX_HEADER: \newcommand{\coversTEX}[2]{#1 \mathrel{\mathsf{covers}} #2} +#+LaTeX_HEADER: \newcommand{\YesTEX}{\mathsf{Yes}} +#+LaTeX_HEADER: \newcommand{\NoTEX}[2]{\mathsf{No}(#1, #2)} +#+LaTeX_HEADER: \usepackage{comment} +#+LaTeX_HEADER: \usepackage{mathpartir} +#+LaTeX_HEADER: \usepackage{stmaryrd} % llbracket, rrbracket +#+LaTeX_HEADER: \usepackage{listings} +#+LaTeX_HEADER: \usepackage{notations} +#+LaTeX_HEADER: \lstset{ +#+LaTeX_HEADER: mathescape=true, +#+LaTeX_HEADER: language=[Objective]{Caml}, +#+LaTeX_HEADER: basicstyle=\ttfamily, +#+LaTeX_HEADER: extendedchars=true, +#+LaTeX_HEADER: showstringspaces=false, +#+LaTeX_HEADER: aboveskip=\smallskipamount, +#+LaTeX_HEADER: % belowskip=\smallskipamount, +#+LaTeX_HEADER: columns=fullflexible, +#+LaTeX_HEADER: moredelim=**[is][\color{blue}]{/*}{*/}, +#+LaTeX_HEADER: moredelim=**[is][\color{green!60!black}]{/!}{!/}, +#+LaTeX_HEADER: moredelim=**[is][\color{orange}]{/(}{)/}, +#+LaTeX_HEADER: moredelim=[is][\color{red}]{/[}{]/}, +#+LaTeX_HEADER: xleftmargin=1em, +#+LaTeX_HEADER: } +#+LaTeX_HEADER: \lstset{aboveskip=0.4ex,belowskip=0.4ex} #+EXPORT_SELECT_TAGS: export #+EXPORT_EXCLUDE_TAGS: noexport @@ -121,7 +143,6 @@ the case of a production compiler and to integrate with an existing code base. T black-box and proof only depends on our equivalence algorithm. \subsection{Our approach} -%% replace common TODO Our algorithm translates both source and target programs into a common representation, decision trees. Decision trees where chosen because they model the space of possible values at a given branch of @@ -206,12 +227,12 @@ matched by the source clauses. \texttt{Unreachable} is used when we statically know that no value can flow to that subtree. -We write $\sem{t_S}_S$ for the decision tree of the source program -$t_S$, computed by a matrix decomposition algorithm (each column +We write 〚tₛ〛ₛ for the decision tree of the source program +t_S, computed by a matrix decomposition algorithm (each column decomposition step gives a \texttt{Switch} node). It satisfies the following correctness statement: \[ -\forall t_S, \forall v_S, \quad t_S(v_S) = \sem{t_S}_S(v_S) +\forall t_s, \forall v_s, \quad t_s(v_s) = \semTEX{t_s}_s(v_s) \] Running any source value $v_S$ against the source program gives the same result as running it against the decision tree. @@ -229,10 +250,10 @@ nodes are never emitted. Guards result in branching. In comparison with the source decision trees, \texttt{Unreachable} nodes are never emitted. -We write $\sem{t_T}_T$ for the decision tree of the target program +We write $\semTEX{t_T}_T$ for the decision tree of the target program $t_T$, satisfying the following correctness statement: \[ -\forall t_T, \forall v_T, \quad t_T(v_T) = \sem{t_T}_T(v_T) +\forall t_T, \forall v_T, \quad t_T(v_T) = \semTEX{t_T}_T(v_T) \] \subsection{Equivalence checking} @@ -241,38 +262,38 @@ possible values \emph{S} and a pair of source and target decision trees and in case the two trees are not equivalent it returns a counter example. The algorithm respects the following correctness statement: \begin{comment} -% TODO: we have to define what \covers mean for readers to understand the specifications -% (or we use a simplifying lie by hiding \covers in the statements). +% TODO: we have to define what \coversTEX mean for readers to understand the specifications +% (or we use a simplifying lie by hiding \coversTEX in the statements). \end{comment} \begin{align*} - \Equiv S {C_S} {C_T} = \Yes \;\land\; \covers {C_T} S + \EquivTEX S {C_S} {C_T} = \YesTEX \;\land\; \coversTEX {C_T} S & \implies \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T) \\ - \Equiv S {C_S} {C_T} = \No {v_S} {v_T} \;\land\; \covers {C_T} S + \EquivTEX S {C_S} {C_T} = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S & \implies v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T) \end{align*} The algorithm proceeds by case analysis. Inference rules are shown. -If $S$ is empty the results is $\Yes$. - -\begin{verbatim} ------------------------- -equiv \emptyset Cs Ct gs -\end{verbatim} +If $S$ is empty the results is $\YesTEX$. +\begin{mathpar} + \infer{ } + {\EquivTEX \emptyset {C_S} {C_T} G} +\end{mathpar} If the two decision trees are both terminal nodes the algorithm checks for content equality. -\begin{verbatim} --------------------------- -equiv S Failure Failure [] +\begin{mathpar} + \infer{ } + {\EquivTEX S \Failure \Failure \emptyqueue} +\\ + \infer + {\trel {t_S} {t_T}} + {\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue} -equiv_BB BBs BBt -------------------------------- -equiv S (Leaf BBs) (Leaf BBt) [] -\end{verbatim} +\end{mathpar} If the source decision tree (left hand side) is a terminal while the target decistion tree (right hand side) is not, the algorithm proceeds @@ -280,13 +301,16 @@ by \emph{explosion} of the right hand side. Explosion means that every child of the right hand side is tested for equality against the left hand side. -\begin{verbatim} -(equiv S Cs Ci gs)^i -equiv S Cs Cf gs ------------------------------------------ -equiv S Cs (Node(a, (Domi,Ci)^i, Cf)) gs -\end{verbatim} - +\begin{mathpar} + \infer + {C_S \in {\Leaf t, \Failure} + \\ + \forall i,\; \EquivTEX {(S \land a \in D_i)} {C_S} {C_i} G + \\ + \EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G} + {\EquivTEX S + {C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G} +\end{mathpar} \begin{comment} % TODO: [Gabriel] in practice the $dom_S$ are constructors and the @@ -304,12 +328,20 @@ the accessors on both side are equal, and removing the branches that result in an empty intersection. If the accessors are different, \emph{$dom_T$} is left unchanged. -\begin{verbatim} -equiv S Ci (trim Ct a=Ki) gs -equiv S Cf (trim Ct (a\notin(K_i)^i) gs -------------------------------------- -equiv S (Node(a, (Ki,Ci)^i, Cf) Ct gs -\end{verbatim} +\begin{mathpar} + \infer + {\forall i,\; + \EquivTEX + {(S \land a = K_i)} + {C_i} {\trim {C_T} {a = K_i}} G + \\ + \EquivTEX + {(S \land a \notin \Fam i {K_i})} + \Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G + } + {\EquivTEX S + {\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G} +\end{mathpar} The equivalence checking algorithm deals with guards by storing a queue. A guard blackbox is pushed to the queue whenever the algorithm @@ -321,17 +353,21 @@ continues by exploding to two subtrees, one in which the guard condition evaluates to true, the other when it evaluates to false. Termination of the algorithm is successful only when the guards queue is empty. -\begin{verbatim} -equiv S Ctrue Ct (gs++[condition]) -equiv S Cfalse Ct (gs++[condition]) --------------------------------------------- -equiv S (Guard condition Ctrue Cfalse) Ct gs +\begin{mathpar} + \infer + {\EquivTEX S {C_0} {C_T} {G, (t_S = 0)} + \\ + \EquivTEX S {C_1} {C_T} {G, (t_S = 1)}} + {\EquivTEX S + {\Guard {t_S} {C_0} {C_1}} {C_T} G} -equiv S Cs Ctrue gs -equiv S Cs Cfalse gs --------------------------------------------- -equiv S Cs (Guard condition Ctrue Cfalse) ([condition]++gs) -\end{verbatim} + \infer + {\trel {t_S} {t_T} + \\ + \EquivTEX S {C_S} {C_b} G} + {\EquivTEX S + {C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}} +\end{mathpar} \begin{comment} TODO: replace inference rules with good latex @@ -678,8 +714,8 @@ bad: The tree of the execution when the function is evaluated considering /int len/ our symbolic variable α, sa->sa_len as symbolic variable β and π as the set of constraints on a symbolic variable: - -#+BEGIN_SRC +[[./files/symb_exec.png]] +\begin{comment} [1] compat (...) { π_{α}: -∞ < α < ∞ } | [2] min (σ₁, σ₂) { π_{σ}: -∞ < (σ₁,σ₂) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...} @@ -687,7 +723,7 @@ and π as the set of constraints on a symbolic variable: [3] cast(u_int) (...) { π_{σ}: 0 ≤ (σ) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...} | ... // rest of the execution -#+END_SRC +\end{comment} We can see that at step 3 the set of possible values of the scrutinee α is bigger than the set of possible values of the input σ to the /cast/ directive, that is: π_{α} ⊈ π_{σ}. For this reason the /cast/ may fail when α is /len/ @@ -695,9 +731,9 @@ negative number, outside the domain π_{σ}. In C this would trigger undefined b overflow) that made the exploitation possible. Every step of evaluation can be modelled as the following transition: -#+BEGIN_SRC +\[ (π_{σ}, (πᵢ)ⁱ) → (π'_{σ}, (π'ᵢ)ⁱ) -#+END_SRC +\] if we express the π constraints as logical formulas we can model the execution of the program in terms of Hoare Logic. State of the computation is a Hoare triple {P}C{Q} where P and Q are @@ -706,50 +742,47 @@ constitute the assertions of the program. C is the directive being executed. The language of the assertions P is: #+BEGIN_SRC -P ::= true | false | a < b | P₁ ∧ P₂ | P₁ ∨ P₂ | ~P +P ::= true | false | a < b | P_{1} \wedge P_{2} | P_{1} \lor P_{2} | \notP #+END_SRC where a and b are numbers. In the Hoare rules assertions could also take the form of #+BEGIN_SRC -P ::= ∀i. P | ∃i. P | P₁ ⇒ P₂ +P ::= \forall i. P | \exists i. P | P_{1} \Rightarrow P_{2} #+END_SRC where i is a logical variable, but assertions of these kinds increases the complexity of the symbolic engine. Execution follows the rules of Hoare logic: - Empty statement : -\begin{verbatim} -———————————— -{P}/skip/{P} -\end{verbatim} +\begin{mathpar} +\infer{ } +{ \{P\} skip \{P\} } +\end{mathpar} - Assignment statement : The truthness of P[a/x] is equivalent to the truth of {P} after the assignment. -\begin{verbatim} -———————————— -{P[a/x]}x:=a{P} -\end{verbatim} +\begin{mathpar} +\infer{ } +{ \{P[a/x]\}x:=a\{P\} } +\end{mathpar} - Composition : c₁ and c₂ are directives that are executed in order; - {Q} is the /midcondition/. -\begin{verbatim} -{P}c₁{R}, {R}c₂{Q} -—————————————————— - {P}c₁;c₂{Q} -\end{verbatim} + {Q} is called the /midcondition/. +\begin{mathpar} +\infer { \{P\}c_1\{R\}, \{R\}c_2\{Q\} } + { \{P\}c₁;c₂\{Q\} } +\end{mathpar} - Conditional : -\begin{verbatim} - {P∧b}c₁{Q}, {P∧~b}c₂{Q} -———————————————————————— -{P}if b then c₁ else c₂{Q} -\end{verbatim} +\begin{mathpar} +\infer { \{P \wedge b \} c_1 \{Q\}, \{P\wedge\not b\}c_2\{Q\} } +{ \{P\}if b then c_1 else c_2\{Q\} } +\end{mathpar} - Loop : {P} is the loop invariant. After the loop is finished /P/ - holds and ~b caused the loop to end. -\begin{verbatim} - {P∧b}c{P} -———————————————————————— -{P}while b do c{P∧~b} -\end{verbatim} + holds and ¬̸b caused the loop to end. +\begin{mathpar} +\infer { \{P \wedge b \}c\{P\} } +{ \{P\} while b do c \{P \wedge \neg b\} } +\end{mathpar} Even if the semantics of symbolic execution engines are well defined, the user may run into different complications when applying such @@ -1129,9 +1162,111 @@ following four rules: apply, and P₂ → L₂ containing the remaining rows. The algorithm is applied to both matrices. +** Target translation + +TODO + +** Equivalence checking + +The equivalence checking algorithm takes as input a domain of +possible values \emph{S} and a pair of source and target decision trees and +in case the two trees are not equivalent it returns a counter example. +The algorithm respects the following correctness statement: + +\begin{comment} +TODO: we have to define what \coversTEX mean for readers to understand the specifications +(or we use a simplifying lie by hiding \coversTEX in the statements). +\end{comment} + +\begin{align*} + \EquivTEX S {C_S} {C_T} \emptyqueue = \YesTEX \;\land\; \coversTEX {C_T} S + & \implies + \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T) +\\ + \EquivTEX S {C_S} {C_T} \emptyqueue = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S + & \implies + v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T) +\end{align*} + +Our equivalence-checking algorithm $\EquivTEX S {C_S} {C_T} G$ is +a exactly decision procedure for the provability of the judgment +$(\EquivTEX S {C_S} {C_T} G)$, defined below. +\begin{mathpar} + \begin{array}{l@{~}r@{~}l} + & & \text{\emph{constraint trees}} \\ + C & \bnfeq & \Leaf t \\ + & \bnfor & \Failure \\ + & \bnfor & \Switch a {\Fam i {\pi_i, C_i}} \Cfb \\ + & \bnfor & \Guard t {C_0} {C_1} \\ + \end{array} + + \begin{array}{l@{~}r@{~}l} + & & \text{\emph{boolean result}} \\ + b & \in & \{ 0, 1 \} \\[0.5em] + & & \text{\emph{guard queues}} \\ + G & \bnfeq & (t_1 = b_1), \dots, (t_n = b_n) \\ + \end{array} + + \begin{array}{l@{~}r@{~}l} + & & \text{\emph{input space}} \\ + S & \subseteq & \{ (v_S, v_T) \mid \vrel {v_S} {v_T} \} \\ + \end{array} + \\ + \infer{ } + {\EquivTEX \emptyset {C_S} {C_T} G} + + \infer{ } + {\EquivTEX S \Failure \Failure \emptyqueue} + + \infer + {\trel {t_S} {t_T}} + {\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue} + + \infer + {\forall i,\; + \EquivTEX + {(S \land a = K_i)} + {C_i} {\trim {C_T} {a = K_i}} G + \\ + \EquivTEX + {(S \land a \notin \Fam i {K_i})} + \Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G + } + {\EquivTEX S + {\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G} + +\begin{comment} + % TODO explain somewhere why the judgment is not symmetric: + % we avoid defining trimming on source trees, which would + % require more expressive conditions than just constructors +\end{comment} + \infer + {C_S \in {\Leaf t, \Failure} + \\ + \forall i,\; \EquivTEX {(S \land a \in D_i)} {C_S} {C_i} G + \\ + \EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G} + {\EquivTEX S + {C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G} + + \infer + {\EquivTEX S {C_0} {C_T} {G, (t_S = 0)} + \\ + \EquivTEX S {C_1} {C_T} {G, (t_S = 1)}} + {\EquivTEX S + {\Guard {t_S} {C_0} {C_1}} {C_T} G} + + \infer + {\trel {t_S} {t_T} + \\ + \EquivTEX S {C_S} {C_b} G} + {\EquivTEX S + {C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}} +\end{mathpar} + * Correctness of the algorithm Running a program tₛ or its translation 〚tₛ〛 against an input vₛ -produces as a result a result /r/ in the following way: +produces as a result /r/ in the following way: | ( 〚tₛ〛ₛ(vₛ) = Cₛ(vₛ) ) → r | tₛ(vₛ) → r Likewise @@ -1206,6 +1341,7 @@ and an optional fallback. Failure is emitted only when the patterns don't cover the whole set of possible input values /S/. The fallback is not needed when the user doesn't use a wildcard pattern. +%%% Give example of thing | Cₛ ::= Leaf bb | Node(a, (Kᵢ → Cᵢ)^{i∈S} , C?) | a ::= Here | n.a @@ -1216,17 +1352,17 @@ Are K and Here clear here? \end{comment} We define the decomposition matrix /mₛ/ as -| SMatrix mₛ := (aⱼ)^{j∈J}, ((pᵢⱼ)^{j∈J} → bbᵢ)^{i∈I} +| SMatrix mₛ := (aⱼ)^{j∈J}, ((p_{ij})^{j∈J} → bbᵢ)^{i∈I} \begin{comment} Correggi prendendo in considerazione l'accessor \end{comment} We define the decision tree of source programs - [|tₛ|] +〚tₛ〛 in terms of the decision tree of pattern matrices - [|mₛ|] + 〚mₛ〛 by the following: - 〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛 # i ∈ I + 〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛 decision tree computed from pattern matrices respect the following invariant: | ∀v (vᵢ)^{i∈I} = v(aᵢ)^{i∈I} → 〚m〛(v) = m(vᵢ)^{i∈I} for m = ((aᵢ)^{i∈I}, (rᵢ)^{i∈I}) @@ -1249,16 +1385,138 @@ Base cases: 2. [| (aⱼ)ʲ, ∅ |] := Failure Regarding non base cases: -We define -| let Idx(k) = [0; arity(k)[ -| let First(∅) = ⊥ -| let First((aⱼ)ʲ) = a_{min(j)} ## where j ∈ J ≠ ∅ +Let's first define +| let Idx(k) := [0; arity(k)[ +| let First(∅) := ⊥ +| let First((aⱼ)ʲ) := a_{min(j∈J≠∅)} +\[ +m := ((a_i)^i ((p_{ij})^i \to e_j)^{ij}) +\] +\[ + (k_k)^k := headconstructor(p_{i0})^i +\] +\begin{equation} +\begin{align} + Groups(m) := ( k_k \to ((a)_{0.l})^{l \in Idx(k_k)} +++ (a_i)^{i \in I\backslash \{0\} }), \\ + ( if p_{0j} is k(q_l) then \\ + (qₗ)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}} \to e_j \\ + if p_{0j} is \_ then \\ + (\_)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}} \to e_j \\ + else \bot )^j ), \\ + ((a_i)^{i \in I\backslash \{0\}}, ((p_{ij})^{i \in I\backslash \{0\}} \to eⱼ if p_{0j} is \_ else \bot)^{j \in J}) +\end{align} +\end{equation} + +Groups(m) is an auxiliary function that decomposes a matrix m into +submatrices, according to the head constructor of their first pattern. +Groups(m) returns one submatrix m_r for each head constructor k that +occurs on the first row of m, plus one "wildcard submatrix" m_{wild} +that matches on all values that do not start with one of those head +constructors. + +Intuitively, m is equivalent to its decompositionin the following +sense: if the first pattern of an input vector (v_i)^i starts with one +of the head constructors k, then running (v_i)^i against m is the same +as running it against the submatrix m_k; otherwise (its head +constructor is none of the k) it is equivalent to running it against +the wildcard submatrix. + +We formalize this intuition as follows: +Lemma (Groups): +Let \[m\] be a matrix with \[Groups(m) = (k_r \to m_r)^k, m_{wild}\]. +For any value vector \[(v_i)^l\] such that \[v_0 = k(v'_l)^l\] for some +constructor k, +we have: +\[ + if k = kₖ for some k then + m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)^{i∈I\backslash \{0\}}) + else + m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\backslash \{0\}} +\] + +*** Proof: +Let \[m\] be a matrix with \[Group(m) = (k_r \to m_r)^k, m_{wild}\]. +Let \[(v_i)^i\] be an input matrix with \[v_0 = k(v'_l)^l\] for some k. +We proceed by case analysis: +- either k is one of the kₖ for some k +- or k is none of the (kₖ)ᵏ + +Both m(vᵢ)ⁱ and mₖ(vₖ)ᵏ are defined as the first matching result of +a family over each row rⱼ of a matrix + +We know, from the definition of +Groups(m), that mₖ is +\[ + ((a){0.l})^{l∈Idx(kₖ)} +++ (aᵢ)^{i∈I\backslash \{0\}}), + ( + if p_{0j} is k(qₗ) then + (qₗ)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}} → eⱼ + if p_{0j} is _ then + (_)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}} → eⱼ + else ⊥ + )ʲ +\] + +By definition, m(vᵢ)ⁱ is +m(vᵢ)ⁱ = First(rⱼ(vᵢ)ⁱ)ʲ for m = ((aᵢ)ⁱ, (rⱼ)ʲ) +(pᵢ)ⁱ (vᵢ)ⁱ = { + if p₀ = k(qₗ)ˡ, v₀ = k'(v'ₖ)ᵏ, k=Idx(k') and l=Idx(k) + if k ≠ k' then ⊥ + if k = k' then ((qₗ)ˡ +++ (pᵢ)^{i∈I\backslash \{0\}}) ((v'ₖ)ᵏ +++ (vᵢ)^{i∈I\backslash \{0\}}) + if p₀ = (q₁|q₂) then + First( (q₁pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}}, (q₂pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}} ) +} + +For this reason, if we can prova that +| ∀j, rⱼ(vᵢ)ⁱ = r'ⱼ((v'ₖ)ᵏ ++ (vᵢ)ⁱ) +it follows that +| m(vᵢ)ⁱ = mₖ((v'ₖ)ᵏ ++ (vᵢ)ⁱ) +from the above definition. + +We can also show that aᵢ = a){0.l}ˡ +++ a_{i∈I\backslash \{0\}} because v(a₀) = K(v(a){0.l})ˡ) ** Proof of equivalence checking +\begin{comment} +TODO: put ^i∈I where needed +\end{comment} +\subsubsection{The trimming lemma} +The trimming lemma allows to reduce the size of a decision tree given +an accessor → π relation (In other words???) +| ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π(kᵢ)}(vₜ) + We prove this by induction on Cₜ: + a. Case where Cₜ = Leaf_{bb}: + Leaf_{bb/a→π}(v) = Leaf_{bb}(v) + That means that the result of trimming on a Leaf is + the Leaf itself + b. Same for failure terminal + e. Unreachabe → ⊥ + c. When Cₜ = Node(b, (π→Cᵢ)ⁱ)_{/a→π} then + we define πᵢ' = πᵢ if a≠b else πᵢ∩π ; + Node(b, (π→Cᵢ)ⁱ)_{/a→π} := Node(b, (π'ᵢ→C_{i/a→π})ⁱ) + Goal: prove that Cₜ(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) + Either vₜ∉(b→πᵢ)ⁱ and that means that the node is a Failure node + Or vₜ∈(b→πₖ) for some k, then + C_{k/a→π}(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) + because when a ≠ b then πₖ'= πₖ => vₜ∈πₖ' + while when a = b then πₖ'=(πₖ∩π) + - vₜ∈π because of hypothesis + - we already know that vₜ∈πₖ + So vₜ ∈ πₖ' and by induction Cₖ(vₜ) = C_{k/a→π}(vₜ) + and Cₜ(vₜ) = Cₖ(vₜ) when vₜ∈(b→πₖ) + This proves that Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) = Cₜ(vₜ) + + Covering lemma: + ∀a,π covers(Cₜ,S) => covers(C_{t/a→π}, (S∩a→π)) + Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %% +\begin{comment} +Should I swap π and π' +\end{comment} + +\subsubsection Proof of equivalence checking The equivalence checking algorithm takes as parameters an input space /S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/: | equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ) @@ -1292,10 +1550,15 @@ TODO: explain: \end{comment} We proceed by case analysis: -1. equiv(∅, Cₛ, Cₜ) := Yes \begin{comment} -Devo spiegarlo? +I start numbering from zero to leave the numbers as they were on the blackboard, were we skipped some things +I think the unreachable case should go at the end. \end{comment} +0. in case of unreachable: Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ +1. In the case of an empty input space +| equiv(∅, Cₛ, Cₜ) := Yes +and that is trivial to prove because there is no pair of values (vₛ, vₜ) that could be +tested against the decision trees. In the other subcases S is always non-empty. 2. equiv(S, Failure, Failure) := Yes the statement holds because of equality between Failure nodes in @@ -1318,3 +1581,24 @@ In the other subcases S is always non-empty. | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) and the result of the algorithm is | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I +4. equiv(S, Node(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) := + let π' = ⋃π(kᵢ) ∀i in + Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++ equiv(S∩(a→π(kᵢ)), Cₛ, C_{/a̸¬̸π'})) + The statement holds because: + a. Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ = Yes + In the yes case let's reason by case analysis: + i. When k∈(kᵢ)ⁱ + there is a k=kₖ for some k and this means that Cₛ(vₛ) = Cₛᵢ(vₛ) + By induction we know that Cₛᵢ(vₛ) = c_{t/a→πᵢ}(vₜ) + and because of the trimming lemma: + Cₜ(vₜ) = C_{t/a→πᵢ}(vₜ) + Putting all together: + Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) = Cₜ(vₜ) + + ii. when k∉(kᵢ)ⁱ ??? + + b. Forall(...) = No(vₛ, vₜ) + for a minimum k, equiv(Sₖ, Cₛₖ, C_{t/a→πₖ} = No(vₛ, vₜ) + then Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) and C_{t/a→πₖ}(vₜ) = Cₜ(vt) + => (Cₛₖ(vₛ) = Cₛ(vₛ)) ≠ Cₜ(vₜ) + # Same for fallback? diff --git a/tesi/tesi_unicode.pdf b/tesi/tesi_unicode.pdf new file mode 100644 index 0000000..6abaa16 Binary files /dev/null and b/tesi/tesi_unicode.pdf differ