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

LessDotCC constraints stay preserved

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-03-19 20:52:04 +01:00
parent e9f86ffda3
commit 17559170d0
1 changed files with 42 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

70
unify.tex
View File

@ -259,6 +259,12 @@ $
\end{figure}
The capture constraints are preserved when applying the \rulename{Upper} rule.
%because \texttt{let} statements like
%let x : X = v in
%can be transformed to
%let x : U = v in
\begin{figure}
\begin{center}
\leavevmode
@ -277,37 +283,38 @@ $
\rulename{Upper}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{G} } \\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot_1 \type{G} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{G} }
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot_1 \type{G} }
\end{array}
\quad \quad
\begin{array}[c]{l} %TODO: can the second part be removed by adding a X.C<X> <. C<a?> constraint at method invocation?
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\
$
% \quad \quad
% \begin{array}[c]{l} %TODO: can the second part be removed by adding a X.C<X> <. C<a?> constraint at method invocation?
% \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G} }
% \end{array}
% $
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G} }
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{L} }
\end{array}
$
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{A} } \\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{L} }
\end{array}
$
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot \type{L} }
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{L} }
\end{array} \quad \type{A} \notin \Delta_{in}
$ %TODO: a <. X with X in Delta_in => a =. X
% other possibliity: is it allowed to see X extends List<X> as class X extends List<X> {}
@ -316,7 +323,7 @@ $
\rulename{Bot}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\
\wildcardEnv \vdash C \cup \set{ \bot \lessdot_1 \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C
@ -326,7 +333,7 @@ $
\rulename{Pit}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \bot } \\
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot }
@ -695,6 +702,11 @@ Removing a wildcard works by setting its lower and upper bound to be equal.
(Def: $\type{Object} = \wildcard{A}{Object}{Object}$).
The \rulename{Equals} rule is responsible for this.
The subtype constraints are a subset of the capture constraints $(\type{T} \lessdot \type{S}) \implies (\type{T} \lessdotCC \type{S})$.
Every transformation on a subtype constraint can also be applied to a capture constraint, but the capture constraints need to be preserved.
We indicate this by numbering the constraints in each transformation.
Constraints with the same number stay the same type.
\textbf{Example:}
\begin{displaymath}
\begin{array}[c]{@{}ll}
@ -821,15 +833,15 @@ This builds a search tree over multiple possible solutions.
\rulename{Same}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \type{G} \lessdot \ntv{a}\\
\wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
C \cup \wctype{\Delta'}{C}{\ol{X}} \lessdot \ntv{a}\\
\hline
\wildcardEnv \vdash
\wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
C \cup \set{
\ntv{a} \doteq \type{G}
\ntv{a} \doteq \wctype{\Delta',\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{X}}
}
\end{array} \quad \begin{array}[c]{l}
\text{fv}(\type{G}) \in \Delta_{in}
\text{fv}(\wctype{\Delta'}{C}{\ol{X}}) / \Delta_{in} = \overline{\rwildcard{A}}
\end{array}
$
\\\\
@ -949,10 +961,10 @@ This builds a search tree over multiple possible solutions.
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\tv{a} \lessdot \tv{b}}
\tv{a} \lessdot_1 \tv{b}}
\\
\hline
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \tv{b}, \tv{b} \lessdot \type{N} }
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \tv{b}, \tv{b} \lessdot \type{N} }
\end{array}
$
\\\\
@ -960,11 +972,11 @@ This builds a search tree over multiple possible solutions.
\rulename{Raise}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \type{N},
\tv{a} \lessdot \tv{b}}
\\
\hline
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot_1 \type{N}, \type{N} \lessdot \tv{b} }
\end{array}
$
\end{tabular}