\section{Constraint generation}
Our type inference algorithm is split into two parts.
A constraint generation step \textbf{TYPE} and a \unify{} step.

Method names are not unique.
It is possible to define the same method in multiple classes.
The \TYPE{} algorithm accounts for that by generating Or-Constraints.
This can lead to multiple possible solutions.

%\subsection{Well-Formedness}


%Why do we need a constraint generation step?
%% The problem is NP-Hard
%% a method call, does not know which type it will produce
%% depending on its type the 

%NO equals constraints during the constraint generation step!
\begin{figure}[tp]
  \begin{align*}
    % Type
    \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
    \type{N} &::= \exptype{C}{\il{T}} && \text{class type (with type variables)} \\
    % Constraints
    \simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\
    \orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\
    \constraint &::= \simpleCons \mid \orCons && \text{constraint}\\
    \consSet &::= \set{\constraints} && \text{constraint set}\\
    % Method assumptions:
    \methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \exptype{}{\ol{Y}
                        \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
                                                                \text{method
                                                                type assumption}\\
    \localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
                                                       assumption}\\
    \mtypeEnvironment & ::= \overline{\methodAssumption} &
                & \text{method type environment} \\
    \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
  \end{align*}
  \caption{Syntax of constraints and type assumptions.}
  \label{fig:syntax-constraints}
\end{figure}

\begin{figure}[tp]
  \begin{gather*}
    \begin{array}{@{}l@{}l}
      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, K \, \overline{M} \}}) =\\
              & \begin{array}{ll@{}l}
\textbf{let} & \forall \texttt{m} \in \ol{M}: \tv{a}_\texttt{m}, \ol{\tv{a}_m} \ \text{fresh} \\
             & \ol{\methodAssumption} = \begin{array}[t]{l}
                \set{ \mv{m'} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}} \to \tv{a}) \mid
                  \mv{m'} \in \ol{M} \setminus \set{\mv{m}}, \, \tv{a}\, \ol{\tv{a}}\ \text{fresh} } \\
\ \cup \, \set{\mv{m} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}_m} \to \tv{a}_\mv{m})}
\end{array}
 \\
              & C_m = \typeExpr(\mtypeEnvironment \cup \set{\mv{this} :
                \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}_m} }, \texttt{e}, \tv{a}_\texttt{m}) \\
\textbf{in} 
              & { ( \mtypeEnvironment \cup \ol{\methodAssumption}, \,
                \bigcup_{\texttt{m} \in \ol{M}} C_m )
                } 
                \end{array}
    \end{array}
  \end{gather*}
  \caption{Constraint generation for classes}
  \label{fig:constraints-for-classes}
\end{figure}

% \textbf{Method Assumptions}

% %$\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.

% % \begin{verbatim}
% % class Example<X> {
% %   <Y> Y m(Example<Y> p){ ... }
% % }
% % \end{verbatim}

% In Featherweight Java a method type is bound to a specific class.
% The class \texttt{Example} shown above contains one method \texttt{m}:

% \begin{displaymath}
% \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y}
% \end{displaymath}

% $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
% It's a map of method types to method names.
% Every method name has a set of possible types,
% because there could be more than one method with the same name in a program consisting out of multiple classes.
% To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list:

% \begin{displaymath}
% \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}}
% \end{displaymath}

% \begin{verbatim}
% class Example<X> { }

% <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
% \end{verbatim}

The constraint generation step is the same as the one for regular Generic Featherweight Java.
Wildcard types are not used during the constraint generation step and have no influence on it.

\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{r} \ \text{fresh} \\
                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\
                    & \constraint = \begin{array}[t]{@{}l@{}l}
                      \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}
                      } \\
                      & \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}
                      }\end{array}\\
                    {\mathbf{in}} & {
                    \consSet_R \cup \set{\constraint}}
                  \end{array} 
  \end{array}
\end{displaymath}

The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression:

There are two kinds of method calls.
The ones to already typed methods and calls to untyped methods.

%Soundness: TODO


\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}
                  \{ \tv{r} \lessdot \exptype{C}{\ol{\wtv{a}}},
                  \overline{\tv{r}} \lessdot \ol{T},
                  \type{T} \lessdot \tv{a}, 
                  \overline{\wtv{a}} \lessdot \ol{N} \}
                \end{array}\\
          & \ |\ 
          (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \overline{\type{T}} \to \type{T}) \in 
              {\mtypeEnvironment}
          , \, \overline{\wtv{a}} \text{ fresh} }
      \end{array}\\
    \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
    \end{array}
    \end{array}
\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:}
\begin{verbatim}
class Class1{
  <X> X m(List<X> lx, List<? extends X> lt){ ... }
  List<? extends String> wGet(){ ... }
  List<String> get() { ... }
}

class Class2{
  example(c1){
    return c1.m(c1.get(), c1.wGet());
  }
}
\end{verbatim}
%This example comes with predefined type annotations.
We assume the class \texttt{Class1} has already been processed by our type inference algorithm,
which has lead to the given type annotations for \texttt{Class1}.
Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
\begin{displaymath}
\mtypeEnvironment =  \left\{\begin{array}{l}
    \type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \ 
      (\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\
     \type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\
     \type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}}
\end{array} \right\} 
\end{displaymath}

The result of the $\typeExpr{}$ function is the constraint set
\begin{displaymath}
C = \left\{ \begin{array}{l}
\tv{c1} \lessdot \type{Class1}, \\
\tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\
\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
\tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2} 
\end{array} \right\}
\end{displaymath}


The first parameter of a method assumption is the receiver type $\type{T}_r$.
\texttt{Class1} for this example.
Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint.
The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method.

or a simplified version:

\begin{displaymath}
C = \left\{ \begin{array}{l}
\tv{c1} \lessdot \type{Class1}, \\
\exptype{List}{\type{String}} 
 \lessdot \exptype{List}{\wtv{x}}, \\
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}
 \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}
\end{array} \right\}
\end{displaymath}


$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable.
%TODO: Do an example where wildcards are inserted and we need capture conversion

\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$

% \\[1em]
% \noindent
% \textbf{Example:}
% \begin{verbatim}
% class Class1 {
%   <X> Pair<X, X> make(List<X> l){ ... }
%   <Y> boolean compare(Pair<Y,Y> p) { ... }

%   example(l){
%     return compare(make(l));
%   }
% }
% \end{verbatim}

% The method call \texttt{make(l)} generates the constraints
% \begin{displaymath}
%   \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}
% \end{displaymath}
% with $\tv{l}$ being the type placeholder for the variable \texttt{l}
% and $\tv{m}$ is the type variable for the return type of the method call.
% $\tv{m}$ is then used as the parameter for the \texttt{compare} method:
% \begin{displaymath}
%   \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}}
% \end{displaymath}
% Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$.



% Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$,
% when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint.

\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , e_1 \elvis{} e_2, \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, e_1, \tv{r}_2)\\
                    & \consSet_2 = \typeExpr({\mtypeEnvironment}, e_2, \tv{r}_2)\\
                    {\mathbf{in}} & {
                    \consSet_1 \cup \consSet_2 \cup
                        \set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}}
                  \end{array} 
  \end{array}
\end{displaymath}

%We could skip wfresh here:
\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , x, \tv{a}) = 
    \mtypeEnvironment(x)
  \end{array}
\end{displaymath}

\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \ol{\tv{r}} \ \text{fresh} \\
                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
                    & C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
                    {\mathbf{in}} & {
                    \overline{\consSet} \cup
                        \set{\tv{a} \doteq \exptype{C}{\ol{a}}}}
                  \end{array} 
  \end{array}
\end{displaymath}

% Problem:
% <X, A extends List<X>> void t2(List<A> l){}

% void test(List<List<?>> l){
%    t2(l);
% }
% Problem:
% List<Y.List<Y>> <. List<a>, a <. List<x>
% Y.List<Y> =. a
% Z.List<Z> <. List<x>

% These constraints should fail!

\section{Result Generation}
If \unify{} returns atleast one type solution $(\Delta, \sigma)$
the last step of the type inference algorithm is to generate a typed class.

This section presents our type inference algorithm.
The algorithm is given method assumptions $\mv\Pi$ and applied to a
single class $\mv L$ at a time:
\begin{gather*}
\fjtypeinference(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
\quad \quad \begin{array}[t]{rll}
  \textbf{let}\ 
  (\overline{\methodAssumption}, \consSet) &= \fjtype{}(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
  \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \ldots \}) &
                                                                     \text{// constraint generation}\\
              {(\Delta, \sigma)} &= \unify{}(\consSet,\, \ol{X} <: \ol{N}) & \text{// constraint solving}\\
              \generics{\ol{Y} \triangleleft \ol{S}} &= \set{ \type{Y} \triangleleft \type{S} \mid \wildcard{Y}{\type{P}}{\bot} \in \Delta} \\
  \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
  %TODO: Describe whole algorithm (Insert types, try out every unify solution by backtracking (describe it as Non Deterministic algorithm))
\end{array}\\
\textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
\textbf{in}\ \mtypeEnvironment \cup
\set{(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \generics{\ol{Y} \triangleleft \ol{S}}\ \ol{\sigma(\tv{a})} \to \sigma(\tv{a})) \ |\ (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
% \fjtypeInsert(\overline{\methodAssumption}, (\sigma, \unifyGenerics{}) )
\end{gather*}

The overall algorithm is nondeterministic. The function $\unify{}$ may
return finitely many times as there may be multiple solutions for a constraint
set.  A local solution for class $\mv C$ may not
be compatible with the constraints generated for a subsequent class. In this case, we have to backtrack to $\mv C$ and proceed to the next
local solution; if thats fail we have to backtrack further to an earlier class.

% \begin{gather*}
%   \textbf{ApplyTypes}(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
%   \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
%   \quad \quad \begin{array}[t]{rl}
%     \textbf{let}\ 
%     \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
%   \end{array}\\
%   \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
%   \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
% \end{gather*}

% %TODO: Rules to create let statements
% % Input is type solution and untyped program.
% % Output is typed program
% % describe conversion for each expression

% Given a result $(\Delta, \sigma)$ and the type placeholders generated by $\TYPE{}$
% we can construct a \wildFJ{} program.

% %TODO: show soundness by comparing constraints and type rules
% % untyped expression | constraints | typed expression (making use of constraints and sigma)
% $\begin{array}{l|c|r}
% m(x) = e & r m(p x) = e & \Delta \sigma(r) m(\sigma(p) x) = |e| \\
% e \elvis{} e' \\
% e.m(\ol{e}) & (e:a).m(\ol{e:p}) & a <. T, p <. T & let x : sigma(a) = e in e.m(x); %TODO
% \end{array}$
% \begin{displaymath}
% \begin{array}[c]{l}
%    \\ 
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv
%  \vdash C \cup \, \set{ 
%  \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
% \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
% \end{array}
% \end{displaymath}