Add GenDelta for WTVS. Restructure step 2. Comment out old version
This commit is contained in:
Andreas Stadelmeier
parent
17559170d0
commit
f2002ea833
@ -378,6 +378,7 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
|
|||||||
\begin{description}
|
\begin{description}
|
||||||
\item[AddDelta] $C$ is not changed
|
\item[AddDelta] $C$ is not changed
|
||||||
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
|
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
|
||||||
|
\item[GenDelta'] same as GenDelta by setting $\sigma'(\wtv{b}) = \rwildcard{B}$
|
||||||
\item[GenSigma] by definition and S-Refl.
|
\item[GenSigma] by definition and S-Refl.
|
||||||
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
|
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
|
||||||
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
|
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
|
||||||
|
|||||||
269
unify.tex
269
unify.tex
@ -830,6 +830,20 @@ This builds a search tree over multiple possible solutions.
|
|||||||
\begin{center}
|
\begin{center}
|
||||||
\fbox{
|
\fbox{
|
||||||
\begin{tabular}[t]{l@{~}l}
|
\begin{tabular}[t]{l@{~}l}
|
||||||
|
\rulename{SameW}
|
||||||
|
& $
|
||||||
|
\begin{array}[c]{l}
|
||||||
|
\wildcardEnv \vdash
|
||||||
|
C \cup \type{G} \lessdot \wtv{a}\\
|
||||||
|
\hline
|
||||||
|
\wildcardEnv \vdash
|
||||||
|
C \cup \set{
|
||||||
|
\wtv{a} \doteq \type{G}
|
||||||
|
}
|
||||||
|
\end{array}
|
||||||
|
$
|
||||||
|
\\\\
|
||||||
|
\cdashline{1-2} \\
|
||||||
\rulename{Same}
|
\rulename{Same}
|
||||||
& $
|
& $
|
||||||
\begin{array}[c]{l}
|
\begin{array}[c]{l}
|
||||||
@ -876,20 +890,20 @@ This builds a search tree over multiple possible solutions.
|
|||||||
\ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
|
\ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
|
||||||
\end{array}
|
\end{array}
|
||||||
$
|
$
|
||||||
\\\\
|
% \\\\
|
||||||
\hline \\
|
% \hline \\
|
||||||
\rulename{SameW}
|
% \rulename{SameW}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \vdash
|
% \wildcardEnv \vdash
|
||||||
C \cup \type{G} \lessdot \wtv{a}\\
|
% C \cup \type{G} \lessdot \wtv{a}\\
|
||||||
\hline
|
% \hline
|
||||||
\wildcardEnv \vdash
|
% \wildcardEnv \vdash
|
||||||
C \cup \set{
|
% C \cup \set{
|
||||||
\wtv{a} \doteq \type{G}
|
% \wtv{a} \doteq \type{G}
|
||||||
}
|
% }
|
||||||
\end{array}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
\\\\
|
||||||
\cdashline{1-2} \\
|
\cdashline{1-2} \\
|
||||||
\rulename{\generalizeRule{}W}
|
\rulename{\generalizeRule{}W}
|
||||||
@ -953,6 +967,8 @@ This builds a search tree over multiple possible solutions.
|
|||||||
\label{fig:step2-rules}
|
\label{fig:step2-rules}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
|
||||||
|
|
||||||
\begin{figure}
|
\begin{figure}
|
||||||
\begin{center}
|
\begin{center}
|
||||||
\fbox{
|
\fbox{
|
||||||
@ -986,110 +1002,110 @@ This builds a search tree over multiple possible solutions.
|
|||||||
\label{fig:step2-rules}
|
\label{fig:step2-rules}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
\begin{figure}
|
% \begin{figure}
|
||||||
\begin{center}
|
% \begin{center}
|
||||||
\fbox{
|
% \fbox{
|
||||||
\begin{tabular}[t]{l@{~}l}
|
% \begin{tabular}[t]{l@{~}l}
|
||||||
\rulename{Same}
|
% \rulename{Same}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \vdash
|
% \wildcardEnv \vdash
|
||||||
C \cup \type{G} \lessdot \tv{a}\\
|
% C \cup \type{G} \lessdot \tv{a}\\
|
||||||
\hline
|
% \hline
|
||||||
\wildcardEnv \vdash
|
% \wildcardEnv \vdash
|
||||||
C \cup \set{
|
% C \cup \set{
|
||||||
\tv{a} \doteq \type{G}
|
% \tv{a} \doteq \type{G}
|
||||||
}
|
% }
|
||||||
\end{array} \quad \begin{array}[c]{l}
|
% \end{array} \quad \begin{array}[c]{l}
|
||||||
\text{fv}(\type{G}) \in \Delta_{in}
|
% \text{fv}(\type{G}) \in \Delta_{in}
|
||||||
\end{array}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
% \\\\
|
||||||
\rulename{\generalizeRule}
|
% \rulename{\generalizeRule}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
|
% \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
|
||||||
\hline
|
% \hline
|
||||||
\wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a},
|
% \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a},
|
||||||
\tv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}},
|
% \tv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}},
|
||||||
%\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
|
% %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
|
||||||
\overline{\tv{u} \lessdot \type{S}}
|
% \overline{\tv{u} \lessdot \type{S}}
|
||||||
}
|
% }
|
||||||
\end{array} \quad \begin{array}[c]{l}
|
% \end{array} \quad \begin{array}[c]{l}
|
||||||
\texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\
|
% \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\
|
||||||
\text{fresh}\ \overline{\wildcard{X}{\tv{u}}{\tv{l}}}
|
% \text{fresh}\ \overline{\wildcard{X}{\tv{u}}{\tv{l}}}
|
||||||
\end{array}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
% \\\\
|
||||||
\rulename{Subst-X}
|
% \rulename{Subst-X}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||||
C \cup \rwildcard{X} \lessdot \tv{a}\\
|
% C \cup \rwildcard{X} \lessdot \tv{a}\\
|
||||||
\hline
|
% \hline
|
||||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||||
C \cup \set{
|
% C \cup \set{
|
||||||
\tv{a} \doteq \rwildcard{X}
|
% \tv{a} \doteq \rwildcard{X}
|
||||||
}
|
% }
|
||||||
\end{array} \quad \begin{array}[c]{l}
|
% \end{array} \quad \begin{array}[c]{l}
|
||||||
\rwildcard{X} \in \Delta_{in}
|
% \rwildcard{X} \in \Delta_{in}
|
||||||
\end{array}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
% \\\\
|
||||||
\rulename{Gen-X}
|
% \rulename{Gen-X}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||||
C \cup \rwildcard{X} \lessdot \tv{a}\\
|
% C \cup \rwildcard{X} \lessdot \tv{a}\\
|
||||||
\hline
|
% \hline
|
||||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||||
C \cup \set{
|
% C \cup \set{
|
||||||
\type{U} \lessdot \tv{a}
|
% \type{U} \lessdot \tv{a}
|
||||||
}
|
% }
|
||||||
\end{array}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
% \\\\
|
||||||
\rulename{Super}
|
% \rulename{Super}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
|
% \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
|
||||||
\hline
|
% \hline
|
||||||
\wildcardEnv \vdash C \cup \set{ \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a} }
|
% \wildcardEnv \vdash C \cup \set{ \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a} }
|
||||||
%\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}}
|
% %\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}}
|
||||||
\end{array} \quad
|
% \end{array} \quad
|
||||||
\begin{array}{l}
|
% \begin{array}{l}
|
||||||
\texttt{class} \ \exptype{C}{\ol{X}} \triangleleft \exptype{D}{\ol{N}} \\
|
% \texttt{class} \ \exptype{C}{\ol{X}} \triangleleft \exptype{D}{\ol{N}} \\
|
||||||
\ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
|
% \ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
|
||||||
\end{array}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
% \\\\
|
||||||
\rulename{Settle}
|
% \rulename{Settle}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
|
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
|
||||||
\tv{a} \lessdot \tv{b}}
|
% \tv{a} \lessdot \tv{b}}
|
||||||
\\
|
% \\
|
||||||
\hline
|
% \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}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
% \\\\
|
||||||
\rulename{Raise}
|
% \rulename{Raise}
|
||||||
& $
|
% & $
|
||||||
\begin{array}[c]{l}
|
% \begin{array}[c]{l}
|
||||||
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
|
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
|
||||||
\tv{a} \lessdot \tv{b}}
|
% \tv{a} \lessdot \tv{b}}
|
||||||
\\
|
% \\
|
||||||
\hline
|
% \hline
|
||||||
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
|
% \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
|
||||||
\end{array}
|
% \end{array}
|
||||||
$
|
% $
|
||||||
\\\\
|
% \\\\
|
||||||
\end{tabular}}
|
% \end{tabular}}
|
||||||
\end{center}
|
% \end{center}
|
||||||
\caption{Step 2 branching: Multiple rules can be applied to the same constraint}
|
% \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
|
||||||
\label{fig:step2-rules}
|
% \label{fig:step2-rules}
|
||||||
\end{figure}
|
% \end{figure}
|
||||||
|
|
||||||
|
|
||||||
%For every $\type{T} \lessdot \tv{a}$ constraint, the unify algorithm has to consider every possible supertype of $\type{T}$.
|
%For every $\type{T} \lessdot \tv{a}$ constraint, the unify algorithm has to consider every possible supertype of $\type{T}$.
|
||||||
@ -1330,6 +1346,8 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
|
|||||||
% \quad \rulename{AddDelta}
|
% \quad \rulename{AddDelta}
|
||||||
% \end{displaymath}
|
% \end{displaymath}
|
||||||
|
|
||||||
|
\dashbox{The \text{tph} function returns all type placeholders inside a given type.}
|
||||||
|
|
||||||
\begin{figure}
|
\begin{figure}
|
||||||
\begin{center}
|
\begin{center}
|
||||||
\fbox{
|
\fbox{
|
||||||
@ -1347,6 +1365,19 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
|
|||||||
\end{array}
|
\end{array}
|
||||||
$
|
$
|
||||||
\\\\
|
\\\\
|
||||||
|
\rulename{GenDelta'}
|
||||||
|
& $
|
||||||
|
\deduction{
|
||||||
|
\wildcardEnv \vdash C \cup \set{\wtv{b} \lessdot \type{T} } \implies \Delta, \sigma
|
||||||
|
}{
|
||||||
|
\wildcardEnv \vdash [\type{B}/\ntv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{T}}{\bot}}, \sigma
|
||||||
|
} \quad
|
||||||
|
\begin{array}{l}
|
||||||
|
\tph(\type{T}) = \emptyset, \text{fv}(\type{T}) \subseteq \Delta \cup \Delta_{in} \\
|
||||||
|
\rwildcard{B} \ \text{fresh}, \Delta, \Delta_{in} \vdash \type{T} \ \ok
|
||||||
|
\end{array}
|
||||||
|
$
|
||||||
|
\\\\
|
||||||
\rulename{GenSigma}
|
\rulename{GenSigma}
|
||||||
& $
|
& $
|
||||||
\deduction{
|
\deduction{
|
||||||
@ -1358,7 +1389,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
|
|||||||
} \quad
|
} \quad
|
||||||
\begin{array}{l}
|
\begin{array}{l}
|
||||||
\tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
|
\tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
|
||||||
\ntv{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 % TODO: Is it possible to imply well-formedness as long as input is well-formed?
|
||||||
\end{array}
|
\end{array}
|
||||||
$
|
$
|
||||||
\\\\
|
\\\\
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user