From b2ca8e49df9b66425530c51003bdfd6ed8fa64cd Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Thu, 23 May 2024 14:18:50 +0200
Subject: [PATCH] Restructure

---
 conclusion.tex  | 6 ++++++
 constraints.tex | 5 ++++-
 tRules.tex      | 3 ---
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/conclusion.tex b/conclusion.tex
index 7213dcc..42b4b01 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,4 +1,10 @@
 \section{Properties of the Algorithm}
+\begin{itemize}
+    \item Our algorithm is designed for extensibility with the final goal of full support for Java.
+    \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
+    Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
+    
+\end{itemize}
 
 %TODO: how are the challenges solved: Describe this in the last chapter with examples!
 \section{Soundness}\label{sec:soundness}
diff --git a/constraints.tex b/constraints.tex
index 7cd5e74..6a5b0df 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -184,7 +184,10 @@ A normal type placeholder cannot hold types containing free variables.
 Normal type placeholders are assigned types which are also expressible with Java syntax.
 So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
 
-Type variables declared in the class header are passed to \unify{}.
+It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
+This is used for class generics see figure \ref{fig:constraints-for-classes}.
+The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
+containing the generics declared by this class.
 Those type variables count as regular types and can be held by normal type placeholders.
 
 %Why do we need a constraint generation step?
diff --git a/tRules.tex b/tRules.tex
index 6e4f430..3d7a521 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -30,9 +30,6 @@ which by default is also a correct Featherweight Java program (see chapter \ref{
 \begin{itemize}
 \item The calculus does not include method overriding for simplicity reasons.
 Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
-Our algorithm is designed for extensibility with the final goal of full support for Java.
-\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
-Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
 %\textit{Note:}
 \item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
 Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus