stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Include Adopt, Settle and Raise again

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-10 08:18:58 +01:00
parent 669837d6ac
commit 7ed1529710
1 changed files with 65 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

122
unify.tex
View File

@ -463,24 +463,24 @@ Their upper and lower bounds are fresh type variables.
\end{array}
$
\\\\
% \rulename{Adopt}
% & $
% \begin{array}[c]{@{}ll}
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \, \set{
% \tv{b} \lessdot \tv{a},
% \tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv \vdash C \cup \, \set{
% \tv{b} \lessdot \type{N},
% \tv{b} \lessdot \tv{a},
% \tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
% }
% \end{array}
% \end{array}
% $
% \\\\
\rulename{Adopt}
& $
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{
\tv{b} \lessdot \tv{a},
\tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \, \set{
\tv{b} \lessdot \type{N},
\tv{b} \lessdot \tv{a},
\tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
}
\end{array}
\end{array}
$
\\\\
\rulename{Adapt}
&
$
@ -747,28 +747,28 @@ This builds a search tree over multiple possible solutions.
\end{array}
$
\\\\
% \rulename{Settle}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
% \tv{a} \lessdot^* \tv{b}}
% \\
% \hline
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} }
% \end{array}
% $
% \\\\
% \rulename{Raise}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
% \tv{a} \lessdot \tv{b}}
% \\
% \hline
% \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
% \end{array}
% $
% \\\\
\rulename{Settle}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\tv{a} \lessdot^* \tv{b}}
\\
\hline
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} }
\end{array}
$
\\\\
\rulename{Raise}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\tv{a} \lessdot \tv{b}}
\\
\hline
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
\end{array}
$
\\\\
\end{tabular}}
\end{center}
\caption{Step 2 branching: Multiple rules can be applied to the same constraint}
@ -860,25 +860,25 @@ $
\end{tabular}}
\end{center}
\textbf{Step 4:}
If there are constraints of the form $(\tv{a} \lessdot \tv{b})$ remaining in the constraint set then
apply the \rulename{Sub-Elim} rule and start over with step 1.
Otherwise continue to step 5.
\begin{center}
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{SubElim}
& $\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
\hline
[\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
\end{array}
$
\end{tabular}}
\end{center}
% \textbf{Step 4:}
% If there are constraints of the form $(\tv{a} \lessdot \tv{b})$ remaining in the constraint set then
% apply the \rulename{Sub-Elim} rule and start over with step 1.
% Otherwise continue to step 5.
% \begin{center}
% \fbox{
% \begin{tabular}[t]{l@{~}l}
% \rulename{SubElim}
% & $\begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
% \hline
% [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
% \end{array}
% $
% \end{tabular}}
% \end{center}
\noindent
\textbf{Step 5:}
\textbf{Step 4:}
We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 6.
\begin{figure}
@ -886,6 +886,14 @@ We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed wi
\leavevmode
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{SubElim}
& $\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
\hline
[\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
\end{array}
$
\\\\
\rulename{Ground}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}