diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 36 |
1 files changed, 35 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index b0d3028..653b8bb 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -4796,7 +4796,7 @@ autres se dérivent par substitution. \end{frame} % \begin{frame} -\frametitle{Collection des contraintes} +\frametitle{Première phase : collection des contraintes} La première phase de l'algorithme de H-M fonctionne comme la vérification de type du $\lambda$CST @@ -4858,4 +4858,38 @@ et on renvoie finalement le type $\eta_1 \to \eta_2$. \end{frame} % +\begin{frame} +\frametitle{Seconde phase : résolution des contraintes} + +L'algorithme d'\textbf{unification} prend en entrée un ensemble +$\mathscr{C}$ de contraintes (équations $\zeta_1 = \zeta_2$ avec +$\zeta_1,\zeta_2$ deux types) et renvoie une \textbf{substitution} des +variables de type ($\{\eta \mapsto \tau\}$ avec $\eta$ des variables +de type et $\tau$ des types \alert{ne faisant pas intervenir} les +variables substituées) qui vérifie les contraintes, ou « échec » : + +\medskip + +\itempoint Si $\mathscr{C}$ est vide, renvoyer la substitution vide. + +\smallskip + +\itempoint Sinon, soit $\zeta_1 = \zeta_2$ une contrainte, et +$\mathscr{C}' := \mathscr{C} \setminus \{(\zeta_1 = \zeta_2)\}$ le +reste des contraintes : +\begin{itemize} +\item si $\zeta_1 = \zeta_2$ déjà, unifier $\mathscr{C}'$, +\item si $\zeta_1$ est une \alert{variable} de type $\eta$ : + \alert{si} $\zeta_2$ ne fait pas intervenir $\eta$, ajouter $\eta + \mapsto \zeta_2$ à la substitution, et unifier $\mathscr{C}'$ où + $\eta$ est remplacé par $\zeta_2$ ; \alert{sinon}, \alert{échouer} + (« type récursif ») ; +\item si $\zeta_2$ est une variable de type : symétriquement ; +\item sinon, $\zeta_1 = (\xi_1 \to \chi_1)$ et $\zeta_2 = (\xi_2 \to + \chi_2)$ : unifier $\mathscr{C}'' := \mathscr{C}' \cup \{(\xi_1 = + \xi_2), (\chi_1 = \chi_2)\}$. +\end{itemize} + +\end{frame} +% \end{document} |