move Remove rule
This commit is contained in:
Andreas Stadelmeier
parent
5873fe68d6
commit
c742bc03f8
143
unify.tex
143
unify.tex
@ -297,48 +297,6 @@ Their upper and lower bounds are fresh type variables.
|
||||
% $
|
||||
% \end{tcolorbox}
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
\fbox{
|
||||
\begin{tabular}[t]{l@{~}l}
|
||||
\rulename{Remove}
|
||||
& $
|
||||
\begin{array}[c]{@{}ll}
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \\
|
||||
% \cup \, \set{ \wtv{a} \lessdot \type{T} }\\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \vdash [\tv{a}/\wtv{a}]C
|
||||
\end{array}
|
||||
&\begin{array}[c]{l}
|
||||
\wtv{a} \in C \\
|
||||
\tv{a} \ \text{fresh}
|
||||
\end{array}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
% \rulename{Trim}
|
||||
% & $
|
||||
% \begin{array}[c]{@{}ll}
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C
|
||||
% \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta', \wildcard{B}{\type{U}}{\type{L}}}{C}{\ol{S}} }\\
|
||||
% \hline
|
||||
% \vspace*{-0.4cm}\\
|
||||
% C \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta'}{C}{\ol{S}} }
|
||||
% \end{array}
|
||||
% &\begin{array}[c]{l}
|
||||
% \rwildcard{B} \notin \ol{S}
|
||||
% \end{array}
|
||||
% \end{array}
|
||||
% $
|
||||
% \\\\
|
||||
\end{tabular}}
|
||||
\end{center}
|
||||
\caption{Wildcard variable substitution rules}\label{fig:wtv-rules}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
\leavevmode
|
||||
@ -729,22 +687,86 @@ We have to consider both possibilities.
|
||||
\noindent
|
||||
\textbf{Step 3}
|
||||
\textbf{(Eliminate Wildcard Variables):}
|
||||
If no more rules in step 2 are applicable \unify{} has to eliminate all wildcard variables
|
||||
If no more rules in step 2 are applicable \unify{} has to eliminate all wildcard variables by applying the \rulename{Remove} rule
|
||||
and start over at step 1.
|
||||
If $C$ does not contain any wildcard variables the algorithm proceeds with step 4.
|
||||
\begin{center}
|
||||
\fbox{
|
||||
\begin{tabular}[t]{l@{~}l}
|
||||
\rulename{Remove}
|
||||
& $
|
||||
\begin{array}[c]{@{}ll}
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \\
|
||||
% \cup \, \set{ \wtv{a} \lessdot \type{T} }\\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash [\tv{a}/\wtv{a}]C
|
||||
\end{array}
|
||||
&\begin{array}[c]{l}
|
||||
\wtv{a} \in C \\
|
||||
\tv{a} \ \text{fresh}
|
||||
\end{array}
|
||||
\end{array}
|
||||
$
|
||||
\end{tabular}}
|
||||
\end{center}
|
||||
|
||||
We apply the \rulename{Clean} rule exhaustively to $C''$:
|
||||
\begin{gather*}
|
||||
\begin{array}[c]{lll}
|
||||
\rulename{Clean} &
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C\\
|
||||
\hline
|
||||
[\tv{a}/\wtv{a}]\wildcardEnv, [\tv{a}/\wtv{a}]\sigma \vdash [\tv{a}/\wtv{a}]C %\cup \set{\tv{b} \doteq \tv{a}}
|
||||
\end{array}
|
||||
\quad \wtv{a} \in C
|
||||
\end{array}
|
||||
\end{gather*}
|
||||
% \begin{figure}
|
||||
% \begin{center}
|
||||
% \fbox{
|
||||
% \begin{tabular}[t]{l@{~}l}
|
||||
% \rulename{Remove}
|
||||
% & $
|
||||
% \begin{array}[c]{@{}ll}
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C \\
|
||||
% % \cup \, \set{ \wtv{a} \lessdot \type{T} }\\
|
||||
% \hline
|
||||
% \vspace*{-0.4cm}\\
|
||||
% \wildcardEnv \vdash [\tv{a}/\wtv{a}]C
|
||||
% \end{array}
|
||||
% &\begin{array}[c]{l}
|
||||
% \wtv{a} \in C \\
|
||||
% \tv{a} \ \text{fresh}
|
||||
% \end{array}
|
||||
% \end{array}
|
||||
% $
|
||||
% \\\\
|
||||
% % \rulename{Trim}
|
||||
% % & $
|
||||
% % \begin{array}[c]{@{}ll}
|
||||
% % \begin{array}[c]{l}
|
||||
% % \wildcardEnv \vdash C
|
||||
% % \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta', \wildcard{B}{\type{U}}{\type{L}}}{C}{\ol{S}} }\\
|
||||
% % \hline
|
||||
% % \vspace*{-0.4cm}\\
|
||||
% % C \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta'}{C}{\ol{S}} }
|
||||
% % \end{array}
|
||||
% % &\begin{array}[c]{l}
|
||||
% % \rwildcard{B} \notin \ol{S}
|
||||
% % \end{array}
|
||||
% % \end{array}
|
||||
% % $
|
||||
% % \\\\
|
||||
% \end{tabular}}
|
||||
% \end{center}
|
||||
% \caption{Wildcard variable substitution rules}\label{fig:wtv-rules}
|
||||
% \end{figure}
|
||||
|
||||
|
||||
% We apply the \rulename{Clean} rule exhaustively to $C''$:
|
||||
% \begin{gather*}
|
||||
% \begin{array}[c]{lll}
|
||||
% \rulename{Clean} &
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C\\
|
||||
% \hline
|
||||
% [\tv{a}/\wtv{a}]\wildcardEnv, [\tv{a}/\wtv{a}]\sigma \vdash [\tv{a}/\wtv{a}]C %\cup \set{\tv{b} \doteq \tv{a}}
|
||||
% \end{array}
|
||||
% \quad \wtv{a} \in C
|
||||
% \end{array}
|
||||
% \end{gather*}
|
||||
|
||||
% \begin{gather*}
|
||||
% \begin{array}[c]{lll}
|
||||
@ -954,17 +976,20 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
%TODO: make Subst-WC to keep the wildcard flag on variables (the remove rule is not allowed to alter those constraints)
|
||||
% TODO: change solved-form accordingly
|
||||
% we can then proof (in soundness for TYPE), that when a constraint a <. T -> X.C<X> <. T , then only variables in X and Delta are used in T
|
||||
\rulename{AddSigma} %This rule adds the substitutions for a? variables
|
||||
& $
|
||||
\deduction{
|
||||
\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{T}} \implies \Delta, \sigma
|
||||
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{T}} \implies \Delta, \sigma
|
||||
}{
|
||||
\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{T}} \implies \Delta, \sigma
|
||||
\cup \set{\tv{a} \to \rwildcard{X}}
|
||||
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{T}} \implies \Delta, \sigma
|
||||
\cup \set{\wtv{a} \to \rwildcard{T}}
|
||||
} \quad
|
||||
\begin{array}{l}
|
||||
\tph(\type{T}) = \emptyset \\
|
||||
\tv{a} \notin \text{dom}(\sigma),\, \Delta \vdash \type{T} \ \ok
|
||||
\tv{a} \notin \text{dom}(\sigma)
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
|
||||
Loading…
Reference in New Issue
Block a user