Start Constraint generation using implication rules

constraints.tex

@@ -348,6 +348,113 @@ 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}
+
+
+% v.m(v, v.f, this.id(v));
+
+% let x1 = v, x2 = v, x3 = v.f, x4 = |this.id(v)| in x1.m(x2, x3, x4)
+
+\begin{lstlisting}{java}
+class Id{
+  <X> X id(X x){ return x; }
+}
+
+class List<X> {
+  List<X> concat(List<X> l){ ... }
+}
+
+class CExample{
+  example(p1, p2) {
+    return p1.id(p2).concat(p2);
+  }
+}
+\end{lstlisting}
+
+At first we assign a type placeholder to every expression in the input program.
+Type placeholders also fill in for missing type annotations in method headers.
+
+\begin{lstlisting}{java}
+class CExample{
+  example(p1, p2) {
+    return p1.id(p2).concat(p2);
+  }
+}
+\end{lstlisting}  
+\begin{lstlisting}{java}
+class CExample{
+  (*@$\tv{a}$@*) example((*@$\tv{b}$@*) p1, (*@$\tv{c}$@*) p2) {
+    return ((p1:(*@$\tv{b}$@*)).id(p2:(*@$\tv{c}$@*)):(*@$\tv{d}$@*)).concat(p2:(*@$\tv{c}$@*)) : (*@$\tv{e}$@*);
+  }
+}
+\end{lstlisting}  
+
+The placeholders $\tv{a}-\tv{e}$ are freshly created in this example and added to every expression.
+The type of local variable expressions like \expr{p1} and \expr{p2} is already known and can be assigned directly.
+$\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.
+Note how type placeholders are used for the \texttt{example} 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{example} : \type{CExample},\tv{b},\tv{c} \to \tv{a}, \\
+\end{array} \right\} 
+$
+
+\begin{mathpar}
+  \inferrule[Method-Cons]{
+      \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
+      \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
+      \texttt{m} : \generics{\ol{Y \triangleleft N}}\type{T}_r, \overline{\type{T}} \to \type{T} \in { \mtypeEnvironment }\\
+      \overline{\wtv{b}}, \tv{x}, \overline{\tv{x}} \ \text{fresh} \\
+      C_m = \set{\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}} \cup
+      [\overline{\wtv{b}}/\ol{Y}]\set{ \tv{x} \lessdotCC \type{T}_r, \overline{\tv{x} \lessdotCC \type{T}}, \type{T} \lessdot \tv{a}, \overline{Y \lessdot N} } 
+  }{
+      \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies C \cup \overline{C} \cup C_m
+  }
+\end{mathpar}
+
+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.
+
+\begin{lstlisting}
+class String{
+  bool equals(String s){ .. }
+}
+class Int{
+  bool equals(Int i){ .. }
+}
+class OrConsExample{
+  m(a, b){
+    return a.equals(b);
+  }
+}
+\end{lstlisting}
+
+The method call to \texttt{equals} now has multiple possibilities.
+It could either be a call to the method in the class \texttt{Int} or in \texttt{String}.
+The method type environment therfore contains two versions of the \texttt{equals} method:
+
+$\mtypeEnvironment{} = \set{ \texttt{equals}_1 : \type{String}, \type{String} \to \type{bool}, 
+\texttt{equals}_2 : \type{Int}, \type{Int} \to \type{bool}}$
+
+The Or-Cons rule considers multiple declarations of the same method separately and joins all of them into a Or-Constraint.
+
+\begin{mathpar}
+  \inferrule[Or-Cons]{
+    \texttt{m}_1 \ldots \texttt{m}_n \in \text{dom}(\mtypeEnvironment{}) \\
+    \mtypeEnvironment \vdash \expr{e}.\texttt{m}_1(\overline{\expr{e}}) : \tv{a} \implies C_1 \quad
+    \ldots \quad
+    \mtypeEnvironment \vdash \expr{e}.\texttt{m}_n(\overline{\expr{e}}) : \tv{a} \implies C_n
+  }{
+      \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies \orCons{}(C_1, \ldots, C_n)
+  }
+\end{mathpar}
+
 % Problem:
 % <X, A extends List<X>> void t2(List<A> l){}