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

Cleanup

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-03-04 16:51:20 +01:00
parent 4eb7b1ce19
commit 3904304a1d
3 changed files with 30 additions and 154 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
constraints.tex
View File

@ -138,7 +138,8 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
\orCons\set{ \orCons\set{
\set{ & \set{ &
\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} , \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N} [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
\ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
} \\ } \\
& \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots} & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
, \, \overline{\wtv{a}} \text{ fresh} , \, \overline{\wtv{a}} \text{ fresh}
@ -154,14 +155,9 @@ The set of method assumptions returned by the \textit{mtypes} function is used t
There are two kinds of method calls. There are two kinds of method calls.
The ones to already typed methods and calls to untyped methods. The ones to already typed methods and calls to untyped methods.
LetFJ version: %TODO: or use the old version with \lessdotCC constraints. then there is no problem with \Delta'
% or only use the \lessdotCC with X.C<X> and C<X> on both sides
% what to do with ? <c X constraints? Just ignore them! they result in X <. X and can be ignored
% generate a function which converts method types and parameter types to constraints of the form a <. X.C<X>, C<X> <. C<x>
% add the free variables to \Delta' proof that they cannot escape the scope (they have to be treated differently than \Delta')
\begin{displaymath} \begin{displaymath}
\begin{array}{@{}l@{}l} \begin{array}{@{}l@{}l}
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\ \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a}) = \\
& \begin{array}{ll} & \begin{array}{ll}
\textbf{let} \textbf{let}
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\ & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
@ -171,87 +167,19 @@ LetFJ version: %TODO: or use the old version with \lessdotCC constraints. then t
& \begin{array}{@{}l@{}l} & \begin{array}{@{}l@{}l}
\constraint = \orCons\set{ & \constraint = \orCons\set{ &
\begin{array}[t]{l} \begin{array}[t]{l}
%TODO: add \ol{\wildcard{X}{\wtv{u}}{\wtv{l}}} to \Delta'
[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\ol{X}}, \exptype{C}{\ol{X}} \lessdot \exptype{C}{\ol{X}},
%[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
\overline{\tv{r}} \lessdot \ol{T},
\ol{X} \lessdot \ol{N},
\ol{Y} \lessdot \ol{N'} \}
\end{array}\\
& \ |\
(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in
{\mtypeEnvironment}, \, |\ol{T}| = |\ol{e}|
, \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
\end{array}\\
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
\end{array}
\end{array}
\end{displaymath}
Java version:
\begin{displaymath}
\begin{array}{@{}l@{}l}
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
& \begin{array}{ll}
\textbf{let}
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
& \consSet_R = \typeExpr(({\mtypeEnvironment} ;
\overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\
& \begin{array}{@{}l@{}l}
\constraint = \orCons\set{ &
\begin{array}[t]{l}
%[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}}, \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}} \lessdotCC \exptype{C}{\ol{X}},
[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}}, [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
\overline{\tv{r}} \lessdotCC \ol{T}, \overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a},
\ol{X} \lessdot \ol{N}, \ol{Y} \lessdot \ol{N} \}
\ol{Y} \lessdot \ol{N'} \}
\end{array}\\ \end{array}\\
& \ |\ & \ |\
(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in (\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in
{\mtypeEnvironment}, \, |\ol{T}| = |\ol{e}| {\mtypeEnvironment} %, \, |\ol{T}| = |\ol{e}|
, \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} } , \, \overline{\wtv{a}} \text{ fresh}}
\end{array}\\ \end{array}\\
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
\end{array} \end{array}
\end{array} \end{array}
\end{displaymath} \end{displaymath}
% \begin{displaymath}
% \typeExpr{}' ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \
% \typeExpr{} ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}}
% \end{displaymath}
\begin{displaymath}
\typeExpr{}' ({\mtypeEnvironment} , \texttt{return e;}, \tv{a} ) = \
\typeExpr{} ({\mtypeEnvironment} , \texttt{e}, \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}} \quad \quad \tv{a}, \wtv{b} \ \text{fresh}
\end{displaymath}
% \begin{displaymath}
% \begin{array}{@{}l@{}l}
% \typeExpr{} & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \\
% & \begin{array}{ll}
% \textbf{let}
% & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
% & \consSet_R = \typeExpr(({\mtypeEnvironment} ;
% \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
% & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\
% & \begin{array}{@{}l@{}l}
% \constraint = \orCons\set{ &
% \begin{array}[t]{l}
% [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
% \overline{\tv{r}} \lessdot \ol{T},
% \type{T} \lessdot \tv{a},
% \ol{X} \lessdot \ol{N},
% \ol{Y} \lessdot \ol{N'} \}
% \end{array}\\
% & \ |\
% (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in
% {\mtypeEnvironment}
% , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
% \end{array}\\
% \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
% \end{array}
% \end{array}
% \end{displaymath}
\\[1em] \\[1em]
\noindent \noindent
\textbf{Example:} \textbf{Example:}

77
tRules.tex
View File

@ -214,68 +214,19 @@ $\begin{array}{l}
\triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}} \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
\end{array} \end{array}
\end{array}$ \end{array}$
\\[1em] % TODO: we need subtyping for FJ without let statements. Problem is \Delta \vdash T witnessed. The \Delta here contains all the let statements beforehand. \\[1em]
% TODO: maybe do a rule which adds let statements at any place! Goal: a program which Unify calculates a type for is also correct under our type laws and can be converted to LefFJ
% motivation: do not use normal types as intermediate types. Keep a Pair<X,X> as that and not convert to X,Y.Pair<X,Y>
% it is possible because the parameters of the method are normal types. we can start capture converting them
% is it possible to say there exists any \Delta which makes the method body possible?
$\begin{array}{l}
\typerule{T-Call}\\
\begin{array}{@{}c}
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\type{T}} \ \ok \quad \quad
\Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
\\
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
\Delta | \Gamma \vdash \texttt{e} : \type{T}_r \mid \Delta_G \quad \quad
\Delta | \Gamma \vdash \ol{e} : \ol{T} \mid \overline{\Delta_G} \quad \quad
\Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
\\
\overline{\Delta_G}, \Delta_G, \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \Delta', \overline{\Delta}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
\typerule{T-Call}\\
\begin{array}{@{}c}
\Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
\generics{\ol{X \triangleleft U'}}\ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
\\
\Delta \vdash \ol{S} \ \ok \quad \quad
\Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \mid \overline{\Delta'} \quad \quad
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
\Delta \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T}
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \overline{\Delta}, \overline{\Delta'}
\end{array}
\end{array}$
% \Delta is not allowed to have wildcards depending on eachother. X^Y, Y^T for example
\\[1em]
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Call}\\ \typerule{T-Call}\\
\begin{array}{@{}c} \begin{array}{@{}c}
\Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
\\ \\
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
\Delta | \Gamma \vdash \texttt{e} : \type{T}_r \quad \quad \Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \quad \quad
\Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
\Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
\\ \\
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
@ -286,26 +237,6 @@ $\begin{array}{l}
\end{array} \end{array}
\end{array}$ \end{array}$
\\[1em] \\[1em]
$\begin{array}{l}
\typerule{T-Call}\\
\begin{array}{@{}c}
\Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok
\\
\Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
\Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \texttt{m}(\ol{e}) : \type{T}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Elvis}\\ \typerule{T-Elvis}\\
\begin{array}{@{}c} \begin{array}{@{}c}

19
unify.tex
View File

@ -1,12 +1,29 @@
% TODO: unify changes % TODO: unify changes
% a? <. T can be deleted in the last step % a? <. T can be deleted in the last step
% remove lessdotCC constraints completely
% delete wildcard tphs a? when needed % delete wildcard tphs a? when needed
% aswell ass free variables: % aswell ass free variables:
% a <. T with fv(T) not empty and not in \Delta' must be removed by U = L % a <. T with fv(T) not empty and not in \Delta' must be removed by U = L
% also in T <. T constraints no free variables are allowed on both sides % also in T <. T constraints no free variables are allowed on both sides
% the algorithm only removes wildcards, never adds them % the algorithm only removes wildcards, never adds them
% lessdotCC constraint cannot be removed. we do not know what to capture
% example <X> add(List<X> l, X v)
% here we need to generate constraints p1 <c List<x>, p2 <c x
% because x can become List<a?>:
% class Box<X>{}
% class Test{
% static <X> Box<X> add(Box<X> b, X x){return null;}
% static <X> Box<X> empty(){return null;}
% static <X> Box<Box<X>> empty2(){return null;}
% public static void main(String args[]){
% Box<?> b = null;
% Box<? extends Box<?>> b2 = add(empty2(), b);
% }
% }
\section{Unify}\label{sec:unify} \section{Unify}\label{sec:unify}
%TODO: Remove lessdotC constraints. those have to be handeld during constraint generation %TODO: Remove lessdotC constraints. those have to be handeld during constraint generation