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

Solution gen methods. Do not generate Generics

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-06-18 18:45:29 +02:00
parent 0a1644617a
commit 6ca45c06d3
1 changed files with 58 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

73
aspUnify.tex
View File

@ -94,29 +94,52 @@ We want to bring type inference for Java to the next level.
}
\end{mathpar}
\begin{mathpar}
\inferrule[N-Refl]{}{
\type{C} << \type{C}
}
\and
\inferrule[N-Trans]{\type{T}_1 << \type{T}_2 \\ \type{T}_2 << \type{T}_3}{
\type{T}_1 << \type{T}_3
}
\and
\inferrule[N-Class]{\texttt{class}\ \exptype{C}{\ldots} \triangleleft \exptype{D}{\ldots}}{
\type{C} << \type{D}
}
\end{mathpar}
\section{Unify}
Input: Every type placeholder must have an upper bound.
Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a
The $\tv{a} \lessdot \type{Object}$ rule has to be ensured by the incoming constraints.
The need to have an upper bound to every type placeholder.
We have to formulate the unification algorithm with implication rules.
Those can be directly translated to ASP.
\begin{mathpar}
\inferrule[Subst]{
\tv{a} \doteq \type{N}
}{
\tv{a} \mapsto \type{N}
}
\and
\inferrule[Subst-L]{
\tv{a} \doteq \type{T}_1 \\
\tv{a} \mapsto \type{T}_1 \\
\tv{a} \lessdot \type{T}_2
}{
\type{T}_1 \lessdot \type{T}_2
}
\and
\inferrule[Subst-R]{
\tv{a} \doteq \type{T}_1 \\
\tv{a} \mapsto \type{T}_1 \\
\type{T}_2 \lessdot \tv{a}
}{
\type{T}_2 \lessdot \type{T}_1
}
\and
\inferrule[Subst-Equal]{
\tv{a} \doteq \type{T}_1 \\
\tv{a} \mapsto \type{T}_1 \\
\tv{a} \doteq \type{T}_2
}{
\type{T}_1 \doteq \type{T}_2
@ -135,10 +158,10 @@ Those can be directly translated to ASP.
}
\and
\inferrule[Subst-Param]{
\tv{a} \doteq \type{G} \\
\tv{a} \mapsto \type{S} \\
\type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \tv{a}, \ldots \type{T}_n} \\
}{
\type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{G}, \ldots \type{T}_n}
\type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
}
\and
\inferrule[S-Object]{}{\tv{a} \lessdot \type{Object}}
@ -225,20 +248,35 @@ Result:
\sigma(\tv{a}) = \type{N}
}
\and
\inferrule[Solution-Sub]{
\tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
\forall i: \type{C_m} << \type{C_i} \\
\text{not}\ \tv{a} \doteq \type{N}
\inferrule[Generic]{
\tv{a} \lessdot \type{N} %, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
\\
\text{not}\ \tv{a} \doteq \type{N}'
}{
\Delta(\type{A}) = \exptype{C_m}{\ol{T_m}} \\ \tv{a} \mapsto \type{A}
% \Delta(\type{A}) = \exptype{C_m}{\ol{T_m}} \\
\tv{a} \mapsto \type{A}
}
% \and
% \inferrule[Solution-Sub]{
% \tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
% \forall i: \type{C_m} << \type{C_i} \\
% \text{not}\ \tv{a} \doteq \type{N}
% }{
% \Delta(\type{A}) = \exptype{C_m}{\ol{T_m}} \\ \sigma(\tv{a}) = \type{A}
% }
\and
\inferrule[Solution-Gen]{
\tv{a} \lessdot \type{G}_1, \ldots, \tv{a} \lessdot \type{G}_n \\
\forall i: \type{G} <: \type{G}_i \\
}{
\Delta(\type{A}) = \type{G} \\ \sigma(\tv{a}) = \type{A}
}
\and
\inferrule[Solution-Sub]{
\tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
\forall i: \type{C_m} << \type{C_i} \\
\text{not}\ \tv{a} \doteq \type{N}
\inferrule[Solution-Gen]{
\tv{a} \lessdot \type{C}_1, \ldots, \tv{a} \lessdot \type{C}_n \\
\forall i: \type{C}_m << \type{C}_i \\
}{
\Delta(\type{A}) = \exptype{C_m}{\ol{T_m}} \\ \sigma(\tv{a}) = \type{A}
\tv{a} \doteq \type{C}_m
}
\end{mathpar}
@ -288,6 +326,11 @@ Fail:
The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
\section{ASP Encoding}
\begin{tabular}{l | r}
$\exptype{C}{\ol{X}}$ & \texttt{type("C", paramX)}\\
\end{tabular}
\section{Completeness}
To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.