Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ

prolog.tex

@@ -97,6 +97,8 @@
 \newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
 \newcommand{\expandLB}{\textit{expandLB}}
 
+\newcommand{\tph}{\text{tph}}
+
 \def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
 \def\exp#1#2{#1(\,#2\,)\xspace}
 \newcommand{\ldo}{, \ldots , }

unify.tex

@@ -522,7 +522,11 @@ The \rulename{Equals} rule is responsible for this.
     \end{array}
 \end{displaymath}
 
+\textbf{Helper functions:}
 \begin{description}
+\item[$\tph{}$] returns all type placeholders inside a given type.
+
+\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
 \item [$\ll$ relation:]
 The $\ll$ relation is the reflexive and transitive closure of the \texttt{extends} relations:
 \begin{displaymath}
@@ -676,10 +680,13 @@ This builds a search tree over multiple possible solutions.
 %There are two different ways of handling a $\type{T} \lessdot \tv{a}$ constraint:
 %TODO: why the \generalizeRule is basically the Same rule for regular type placeholders
 
+%where is the mistake in the old unify algorithm? 
+%when working with equality the problems arise! Free variables should not escape their scope
 % Replacing regular type placeholders causes problems related to method calls and capture conversion.
 
 % <X> List<X> same(List<X> a, List<X> b){}
 
+% This program has no correct type. the same method requires 
 % \begin{lstlisting}
 % List<?> f;
 % List<?> problem(){
@@ -938,7 +945,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
             \wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{N}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
             } \quad
             \begin{array}{l}
-            \text{tph}(\type{N}) = \emptyset, \text{fv}(\type{N}) = \emptyset \\
+            \tph(\type{N}) = \emptyset, \text{fv}(\type{N}) = \emptyset \\
             \rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma)
             \end{array}
           $
@@ -963,7 +970,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
       \set{\tv{a} \to \type{T} }
       } \quad 
       \begin{array}{l}
-      \text{tph}(\type{T}) = \emptyset \\
+      \tph(\type{T}) = \emptyset \\
       \tv{a} \notin \text{dom}(\sigma)
       \end{array}
       $