From c742bc03f844d5c3198844db03889f52d773cd34 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 9 Jan 2024 07:33:02 +0100 Subject: [PATCH] move Remove rule --- unify.tex | 143 ++++++++++++++++++++++++++++++++---------------------- 1 file changed, 84 insertions(+), 59 deletions(-) diff --git a/unify.tex b/unify.tex index 110803b..0c2908e 100644 --- a/unify.tex +++ b/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 <. 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} $ \\\\