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

Move Crunch

Browse Source
This commit is contained in:
JanUlrich 2024-02-14 05:32:47 +01:00
parent eab6907624
commit 3398cccd96
1 changed files with 28 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
unify.tex
View File

@ -574,6 +574,34 @@ Their upper and lower bounds are fresh type variables.
\end{array}
\end{array}
$
\\\\
\rulename{Crunch}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
\end{array}
&\begin{array}[c]{l}
\ol{U} = \ol{L}
\end{array}
\end{array}$
\\\\
\rulename{Crunch}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
\end{array}
&\begin{array}[c]{l}
\ol{U} = \ol{L}
\end{array}
\end{array}$
\end{tabular}}
\end{center}
\caption{Constraint reduce rules}\label{fig:reduce-rules}
@ -1148,34 +1176,6 @@ C \cup \set{ \tv{a} \doteq \bot }
%\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1
\end{array}
\end{array}$
\\\\
\rulename{Crunch}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
\end{array}
&\begin{array}[c]{l}
\ol{U} = \ol{L}
\end{array}
\end{array}$
\\\\
\rulename{Crunch}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
\end{array}
&\begin{array}[c]{l}
\ol{U} = \ol{L}
\end{array}
\end{array}$
% \\\\ % The force rule is unnecessary because every type placeholder has an upper bound Object (a <. Object) The match rule eliminates those wildcards
% \rulename{Force} &$
% \begin{array}[c]{@{}ll}