stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add LessdotCC REmove to unify. Fix Soundness lemma

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-30 16:19:01 +01:00
parent 9aa89933ce
commit 319f080a8d
2 changed files with 26 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
soundness.tex
View File

@ -157,11 +157,14 @@ Method calls generate multiple constraints that share the same wildcard placehol
\begin{lemma}
\unify{} generates well-formed type environments
\begin{description}
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
\item[and] $\forall \Delta_w \in C: \vdash \type{L} <: \type{U}$
\item[then] TODO
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
\item[and] $\forall \Delta_w \in C: \ \vdash \type{L} <: \type{U}$
\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
\end{description}
\end{lemma}
Only the \rulename{General} rule generates fresh wildcards.
By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash $
By S-Exists and S-Trans
\begin{lemma}
Well-formedness is hereditary
@ -224,7 +227,7 @@ The \unify{} algorithm only produces correct output.
%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
\item[Then] there exists a $\sigma'$ with:
$\sigma \subseteq \sigma'$ and
$\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.

22
unify.tex
View File

@ -132,6 +132,13 @@ $
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{T} }
\end{array}
\quad \quad
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{T} }
\end{array}
$
\\\\
\rulename{Lower}
@ -361,12 +368,12 @@ Their upper and lower bounds are fresh type variables.
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \wctype{\Delta}{C}{\ol{T}} } \\
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \overline{\wildcard{C}{\type{U}}{\type{L}}}
\vdash C \cup \, \set{
[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \wctype{\Delta}{C}{\ol{T}} }
[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
@ -708,7 +715,7 @@ We have to consider both possibilities.
\noindent
\textbf{Step 3}
\textbf{(Eliminate Wildcard Variables):}
If no more rules in step 2 are applicable \unify{} has to eliminate all wildcard variables by applying the \rulename{Remove} rule
If no more rules in step 2 are applicable \unify{} has to eliminate all wildcard variables and $\lessdotCC$ constraints by applying the \rulename{Remove} rule
and start over at step 1.
If $C$ does not contain any wildcard variables the algorithm proceeds with step 4.
\begin{center}
@ -729,6 +736,15 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step
\tv{a} \ \text{fresh}
\end{array}
\end{array}
$
\\\\
\rulename{Remove-Cons} & $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\type{S} \lessdotCC \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \set{\type{S} \lessdot \type{T} }
\end{array}
$
\end{tabular}}
\end{center}