Add New-Cons

constraints.tex

@@ -348,12 +348,39 @@ This practice hinders free variables to leave their scope.
 The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
 cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
 
-\subsection{Examples}
+\subsection{Constraint Generation}
+The constraint generation is defined on a subset of Java displayed in figure \ref{fig:miniJavaSyntax}.
+The input language includes only a small set of expressions like method calls, field access and a elvis operator $\elvis$
+which acts as a replacement for if-else expressions.
+\begin{figure}
+\par\noindent\rule{\textwidth}{0.4pt}
+\center
+$
+\begin{array}{lrcl}
+%\hline
+\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
+\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
+\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
+\text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
+\text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
+\text{Method declarations} &  \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
+\text{Terms} & \expr{e} & ::= & \expr{x} \\
+& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
+& & \ \ | & \expr{e}.f\\
+& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
+& & \ \ | & \expr{e} \elvis{} \expr{e}\\
+\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}}
+%\hline
+\end{array}
+$
+\par\noindent\rule{\textwidth}{0.4pt}
+\caption{Input Syntax with optional type annotations}\label{fig:miniJavaSyntax}
+\end{figure}
 
-
+We explain the process using the following example input.
-% v.m(v, v.f, this.id(v));
+The classes \texttt{List} and \texttt{Id} are already fully typed and we want to create constraints for the class
-
+\texttt{CExample} now.
-% let x1 = v, x2 = v, x3 = v.f, x4 = |this.id(v)| in x1.m(x2, x3, x4)
 
 \begin{lstlisting}{java}
 class Id{
@@ -361,7 +388,7 @@ class Id{
 }
 
 class List<X> {
-  List<X> concat(List<X> l){ ... }
+  <Y extends X> List<X> concat(List<Y> l){ ... }
 }
 
 class CExample{
@@ -371,7 +398,7 @@ class CExample{
 }
 \end{lstlisting}
 
-At first we assign a type placeholder to every expression in the input program.
+The first step of constraint generation is to assign type placeholders to every expression in the input program.
 Type placeholders also fill in for missing type annotations in method headers.
 
 \begin{lstlisting}{java}
@@ -394,16 +421,28 @@ The type of local variable expressions like \expr{p1} and \expr{p2} is already k
 $\expr{p1}:\tv{b}$ and $\expr{p2}:\tv{c}$ in this case.
 The method call to \texttt{id} gets the fresh type placeholder $\tv{d}$ as type and the method call to \texttt{concat} is assigned the placeholder $\tv{e}$.
 
-Afterwards a method type environment $\mtypeEnvironment$ containing all method declarations is created.
+Afterwards we create a method type environment $\mtypeEnvironment$ containing all method declarations.
-Note how type placeholders are used for the \texttt{example} method:
+Each entry has the form $\texttt{m} : \generics{\ol{X \triangleleft N}} \ol{T} \to \type{T}$.
+The type arguments of the surrounding class and the type arguments of each method are merged together
+leading to the list $\generics{\type{X}, \type{Y} \triangleleft \type{X}}$ for the \texttt{concat} method
+($\triangleleft$ is short for \texttt{extends}).
+Also the type of the surrounding class is added to the parameter list of the method.
+This leads to the \texttt{id} method having two arguments.
+One is the \texttt{Id} class itself and the second one is the actual arguemnt of the method.
 
 $\mtypeEnvironment{} = \left\{ \begin{array}{l}
 \texttt{id} : \generics{\type{X}}\type{Id},\type{X} \to \type{X}, \\
-\texttt{concat} : \generics{\type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{X}} \to \exptype{List}{\type{X}}, \\
+\texttt{concat} : \generics{\type{X}, \type{Y} \triangleleft \type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{Y}} \to \exptype{List}{\type{X}}, \\
 \texttt{example} : \type{CExample},\tv{b},\tv{c} \to \tv{a}, \\
 \end{array} \right\} 
 $
 
+Note: type placeholders are used for the \texttt{example} method.
+
+Our constraint generation rules have the form:
+$\mtypeEnvironment \vdash \expr{e} : \tv{a} \implies C$,
+that given a method environment $\mtypeEnvironment$ and an expression $\expr{e}$ with type $\tv{a}$ generates the constraint set $C$.
+
 \begin{mathpar}
   \inferrule[Method-Cons]{
       \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
@@ -415,8 +454,39 @@ $
   }{
       \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies C \cup \overline{C} \cup C_m
   }
+  \and
+%  \inferrule[Field-Cons]{
+%    \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
+%    C_f = \set{}
+%  }{
+%    \mtypeEnvironment \vdash \expr{e}.\texttt{f} : \tv{a} \implies C \cup C_f \\
+%  }
+%  \and
+  \inferrule[Var-Cons]{
+  }{
+    \mtypeEnvironment \vdash \expr{x} : \tv{a} \implies \emptyset
+  }
+  \and
+  \inferrule[Elvis-Cons]{
+    \mtypeEnvironment \vdash \expr{e}_1 : \tv{e}_1 \implies C_1 \\
+    \mtypeEnvironment \vdash \expr{e}_2 : \tv{e}_2 \implies C_2
+  }{
+    \mtypeEnvironment \vdash \expr{e}_1 \elvis{} \expr{e}_2 : \tv{a} \implies C_1 \cup C_2 \cup \set{\tv{e}_1 \lessdot \tv{a}, \tv{e}_2 \lessdot \tv{a}}
+  }
+  \and
+  \inferrule[New-Cons]{
+      \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
+      \texttt{class} \ \exptype{D}{\ol{X \triangleleft N}} \set{ \ol{T\ f}; \ldots }
+  }{
+    \mtypeEnvironment \vdash \texttt{new}\ \type{D}(\ol{e}) : \tv{a} \implies \overline{C} \cup [\ol{\wtv{b}}/\ol{X}]\set{ \overline{\tv{e} \lessdot \type{T}}, \exptype{D}{\ol{X}} \lessdot \tv{a}, \ol{X \lessdot N} }
+  }
 \end{mathpar}
 
+According to the Method-Cons rule the constraints generated by the call to \texttt{id} are:
+$\mtypeEnvironment \vdash (p1:\tv{b}).id(p2:\tv{c}):\tv{d} \implies \set{\tv{b} \lessdot \tv{x}_1, \tv{c} \lessdot \tv{x}_2, \tv{x}_1 \lessdotCC \type{Id},
+\tv{x}_2 \lessdotCC \wtv{b}, \wtv{b} \lessdot \tv{d}}$.
+
+\subsection{Or-Constraints}
 In case the input program contains multiple method declarations holding the same name and same amount of parameters then so called Or-Constraints must be generated.
 Usually Java is able to determine which method to call based on the argument's types passed to the method. %'
 During the constraint generation step the argument types are unknown and we have to assume multiple methods as invocation target.