Make match rule remember constraint type

prolog.tex

@@ -111,6 +111,7 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
+\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}

unify.tex

@@ -1,6 +1,18 @@
 
 \section{Unify}\label{sec:unify}
 
+The wildcard placeholders are used for intermediat types.
+It is not possible to create all super types of a type.
+The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}.
+%thats not true. it can spawn X^T_T2.List<X> where T and T2 are types and we need to choose one inbetween them
+Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java.
+
+Any type can be inserted into wildcard placeholders.
+Normal placeholders have to contain types, which are well-formed under the supplied environment.
+% It is important that the algorithm also works for any subset of constraints
+%TODO: The unify algorithm can do any operation on wildcard placeholders the same as on normal ones.
+%TODO: Unify could make way more substitutions for wtvs especially in step 2
+
 \subsection{Description}
 The \unify{} algorithm tries to find a solution for a set of constraints like
 $\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$.
@@ -137,13 +149,13 @@ This is necessary for the \rulename{Equals} rule to work properly.
     \begin{tabular}[t]{l@{~}l}
     \rulename{Subst} &
                      $\begin{array}[c]{l}
-\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{T}}\\
+\wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
                        \hline
 [\type{T}/\tv{a}]\wildcardEnv \vdash [\type{T}/\tv{a}]
-C \cup \set{\tv{a} \doteq \type{T}}
+C \cup \set{\ntv{a} \doteq \type{T}}
                      \end{array}
                    \quad \begin{array}{c}
-                    \tv{a} \notin \type{T} \\
+                    \ntv{a} \notin \type{T} \\
                     \text{fv}(\type{T}) \subseteq \Delta'
                    \end{array}$\\
 \\
@@ -184,7 +196,7 @@ $
     \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{G}   }
     \end{array}
     \quad \quad
-    \begin{array}[c]{l}
+    \begin{array}[c]{l} %TODO: can the second part be removed by adding a X.C<X> <. C<a?> constraint at method invocation?
     \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\ 
     \hline
     \vspace*{-0.4cm}\\
@@ -329,24 +341,24 @@ $
 The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
 Their upper and lower bounds are fresh type variables.
 
-%Unify only renames the wildcards in the reduce rule
-% It's the only place where wildcards are coming into play (theres always a reduce step before a wildcard substitution is possible)
 
-
-% die wildcard variablen sollten erst am Ende ausgetauscht werden gegen normale variablen
-% das funktioniert, da die im Reduce step erstellten direkt substituiert werden
-% die anderen erlauben Capture Conversion aber nur wenn der Methodentyp und Parametertyp schon feststeht! (gleich Mächtig wie TI in Java)
-% a? <. T -> 
-% T <. a? -> 
-% a? =. T -> substitute!
-% bei normalen Typvariablen werden keine Wildcards substituiert
-
-% \begin{tcolorbox}
-% $
-% \wctype{\rwildcard{X}}{Box}{\rwildcard{X}} \lessdot \exptype{Box}{\tv{a}_?}, \\
-% \exptype{Box}{\tv{a}_?} \lessdot \wctype{\rwildcard{X}}{Box}{\rwildcard{X}}
-% $
-% \end{tcolorbox}
+\begin{figure}
+  \begin{center}
+      \leavevmode
+      \fbox{
+      \begin{tabular}[t]{l@{~}l}
+        \rulename{Circle} & $
+        \begin{array}[c]{l}
+          \wildcardEnv \vdash C \cup \, \set{\tv{a}_1 \lessdot
+          \tv{a}_2, \tv{a}_2 \lessdot \tv{a}_3, \dots, \tv{a}_n \lessdot \tv{a}_1}\\
+          \hline
+          \wildcardEnv \vdash C \cup \, \set{\tv{a}_1 \doteq \tv{a}_2, \tv{a}_2 \doteq \tv{a}_3, \dots , \tv{a}_n \doteq \tv{a}_1} 
+        \end{array} \quad n>0
+              $
+      \end{tabular}}
+  \end{center}
+    \caption{Rules for normal placeholders}\label{fig:reduce-rules}
+\end{figure}
 
 \begin{figure}
     \begin{center}
@@ -358,16 +370,16 @@ Their upper and lower bounds are fresh type variables.
           \begin{array}[c]{@{}ll}
           \begin{array}[c]{l}
              \wildcardEnv \vdash C \cup \, \set{
-                \tv{a} \lessdot \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot \wctype{\Delta'}{D'}{\ol{T'}} }\\ 
+                \tv{a} \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}} }\\ 
             \hline
             \vspace*{-0.4cm}\\
 \wildcardEnv \vdash C \cup \, \left\{ \begin{array}[c]{l}
                 \tv{a} \lessdot \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}},
               \ol{\tv{l}} \lessdot \ol{\tv{u}}, \\
             \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
-                     \lessdot \wctype{\Delta}{D}{\ol{T}}, \\
+                     \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \\
             \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
-                     \lessdot \wctype{\Delta'}{D'}{\ol{T'}}
+                     \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}}
 \end{array}
 \right\}
           \end{array}
@@ -751,10 +763,10 @@ This builds a search tree over multiple possible solutions.
       & $
       \begin{array}[c]{l}
         \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-        \tv{a} \lessdot^* \tv{b}}
+        \tv{a} \lessdot \tv{b}}
         \\
         \hline
-        \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N}  }
+        \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot \tv{b}, \tv{b} \lessdot \type{N}  }
       \end{array}
       $
     \\\\ 
@@ -1049,13 +1061,13 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
           \rulename{GenDelta}
           & $
           \deduction{
-            \wildcardEnv \vdash C \cup \set{\tv{b} \lessdot \type{T} } \implies \Delta, \sigma
+            \wildcardEnv \vdash C \cup \set{\ntv{b} \lessdot \type{T} } \implies \Delta, \sigma
             }{
-            \wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{T}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
+            \wildcardEnv \vdash [\type{B}/\ntv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{T}}{\bot}}, \sigma \cup \set{\ntv{b} \to \type{B}}
             } \quad
             \begin{array}{l}
             \tph(\type{T}) = \emptyset, \text{fv}(\type{T}) \subseteq \Delta \cup \Delta_{in} \\
-            \rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta, \Delta_{in} \vdash \type{T} \ \ok
+            \rwildcard{B} \ \text{fresh}, \ntv{b} \notin \text{dom}(\sigma), \Delta, \Delta_{in} \vdash \type{T} \ \ok
             \end{array}
           $
         \\\\ 
@@ -1063,14 +1075,14 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
       & $
       \deduction{
       \wildcardEnv \vdash C \cup
-      \set{\tv{a} \doteq \type{T} }  \implies \Delta, \sigma
+      \set{\ntv{a} \doteq \type{T} }  \implies \Delta, \sigma
       }{
       \wildcardEnv \vdash C   \implies \Delta,  \sigma \cup
-      \set{\tv{a} \to \type{T} }
+      \set{\ntv{a} \to \type{T} }
       } \quad 
       \begin{array}{l}
       \tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
-      \tv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_{in} \vdash \type{T} \ \ok
+      \ntv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_{in} \vdash \type{T} \ \ok
       \end{array}
       $
     \\\\