Add prepare rule

soundness.tex

@@ -188,12 +188,16 @@ This rule is only applied for the outer wildcard environments for each type.
 % Y.Box<Y> <. Box<a?>
 % Y =. a?
 
+% Box<Y.Box<Y>> <. Box<? extends Box<a>>
+% Y.Box<Y> <. Box<a>
+
+% Problem: für tvs dürfen keine Wildcards eingesetzt werden, außer für die 
 
 \begin{lemma}
 The \unify{} algorithm only produces correct output for constraints not containing free variables.
 \begin{description}
-\item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
+\item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
-\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
+%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
 \item[Then] there exists a $\Delta'$ with:
 $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
 and $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
@@ -265,6 +269,18 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \item[Adapt] Assumption, S-Extends, S-Trans
 \item[Adopt] Assumption, because $C \subset C'$
 %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
+\item[Prepare] 
+To show 
+$\Delta \vdash \wctype{\overline{\wildcard{B}{U}{L}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof:
+\begin{gather}
+\Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\
+\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
+\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta) \\
+\label{rp:4}
+\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
+\end{gather}
+\ref{rp:4} is always true.
+
 \item[Capture]
 If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
 If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ the preposition holds because
@@ -286,7 +302,9 @@ $\Delta' \Delta \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}
 %, which implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}})$.
 
 %We are doing a capture conversion. If $\type{T}$ does not contain free variables, this does not affect the subtype relation.
-\item[Reduce] %Assumption and S-Exists.
+\item[Reduce]
+
+%Assumption and S-Exists.
 % Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:
 % \begin{description} 
 %     \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset, \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$:]

unify.tex

@@ -68,7 +68,7 @@ and a name $\mathtt{X}$.
 
 The \rulename{Normalize} rule eliminates wildcards. % TODO
 This is done by setting the upper and lower bound to the same value.
-We generate wildcards with the \rulename{\generalizeRule} rule.
+\unify{} generates wildcards with the \rulename{\generalizeRule} rule.
 It is important to generate new wildcards in a standardized fashion.
 When having two constraints $\type{T} \lessdot \tv{a}$ and $\type{T} \lessdot \tv{b}$,
 then after applying the \rulename{\generalizeRule} rule the freshly generated constraints are
@@ -359,10 +359,10 @@ Their upper and lower bounds are fresh type variables.
       \begin{array}[c]{@{}ll}
       \begin{array}[c]{l}
           \wildcardEnv \vdash 
-          C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} \lessdotCC \wctype{\Delta}{C}{\ol{T}} } \\ 
+          C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \wctype{\Delta}{C}{\ol{T}} } \\ 
         \hline
         \vspace*{-0.4cm}\\
-        \wildcardEnv \cup \overline{\wildcard{C}{\type{U'}}{\type{L'}}}
+        \wildcardEnv \cup \overline{\wildcard{C}{\type{U}}{\type{L}}}
          \vdash C \cup \, \set{  
           [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \wctype{\Delta}{C}{\ol{T}} }
       \end{array}
@@ -373,6 +373,29 @@ Their upper and lower bounds are fresh type variables.
         \end{array}
       \end{array}
       $
+    \\\\
+      \rulename{Prepare}
+      & 
+      $
+      \begin{array}[c]{@{}ll}
+      \begin{array}[c]{l}
+          \wildcardEnv \vdash 
+          C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ 
+        \hline
+        \vspace*{-0.4cm}\\
+        \wildcardEnv \cup \overline{\wildcard{B}{\type{U}}{\type{L}}}
+         \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}
+       %\quad \ol{Y} = \textit{fresh}(\ol{X})
+       \quad \begin{array}[c]{l}
+        \ol{\rwildcard{C}} \ \text{fresh}\\
+        \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset\\
+        \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
+        \end{array}
+      \end{array}
+      $
     \\\\
         \rulename{Adopt}
         & $