From 3904304a1d29fe36a768102aab23d4c2a7e91149 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Mon, 4 Mar 2024 16:51:20 +0100 Subject: [PATCH] Cleanup --- constraints.tex | 88 +++++-------------------------------------------- tRules.tex | 77 +++---------------------------------------- unify.tex | 19 ++++++++++- 3 files changed, 30 insertions(+), 154 deletions(-) diff --git a/constraints.tex b/constraints.tex index 92b412b..3eeef6c 100644 --- a/constraints.tex +++ b/constraints.tex @@ -138,7 +138,8 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi \orCons\set{ \set{ & \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} , \, \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. 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 and C on both sides -% what to do with ? , C <. C -% add the free variables to \Delta' proof that they cannot escape the scope (they have to be treated differently than \Delta') \begin{displaymath} \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} \textbf{let} & \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} \constraint = \orCons\set{ & \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{\tv{r}} \lessdotCC \ol{T}, - \ol{X} \lessdot \ol{N}, - \ol{Y} \lessdot \ol{N'} \} + \overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, + \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} } + (\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}} \end{array}\\ \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \end{array} \end{array} \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] \noindent \textbf{Example:} diff --git a/tRules.tex b/tRules.tex index 8fefe08..9ff417f 100644 --- a/tRules.tex +++ b/tRules.tex @@ -214,68 +214,19 @@ $\begin{array}{l} \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}} \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. -% 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 as that and not convert to X,Y.Pair -% 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] +\\[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 + \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} \ \ok \quad \quad - \Delta | \Gamma \vdash \texttt{e} : \type{T}_r \quad \quad - \Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad - \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad + \Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \quad \quad \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 \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} @@ -286,26 +237,6 @@ $\begin{array}{l} \end{array} \end{array}$ \\[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} \typerule{T-Elvis}\\ \begin{array}{@{}c} diff --git a/unify.tex b/unify.tex index 89e228b..e49b0dd 100644 --- a/unify.tex +++ b/unify.tex @@ -1,12 +1,29 @@ % TODO: unify changes % a? <. T can be deleted in the last step -% remove lessdotCC constraints completely % delete wildcard tphs a? when needed % aswell ass free variables: % 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 % the algorithm only removes wildcards, never adds them +% lessdotCC constraint cannot be removed. we do not know what to capture +% example add(List l, X v) +% here we need to generate constraints p1 , p2 : + +% class Box{} + +% class Test{ + +% static Box add(Box b, X x){return null;} +% static Box empty(){return null;} +% static Box> empty2(){return null;} +% public static void main(String args[]){ +% Box b = null; +% Box> b2 = add(empty2(), b); +% } +% } + \section{Unify}\label{sec:unify} %TODO: Remove lessdotC constraints. those have to be handeld during constraint generation