BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits: 9ce6c688 by n3f4s at 2016-10-07T00:24:30+02:00 add debug output
- - - - - e71a2bde by n3f4s at 2016-10-07T00:24:30+02:00 update report
- - - - - fdf96490 by n3f4s at 2016-10-07T00:24:31+02:00 debug makefile
- - - - -
7 changed files:
- doc/rapport/Makefile - doc/rapport/infer.tex - doc/rapport/main.tex - doc/rapport/pres-univ.tex - doc/rapport/typer.tex - src/lparse.ml - tests/unify_test.ml
Changes:
===================================== doc/rapport/Makefile ===================================== --- a/doc/rapport/Makefile +++ b/doc/rapport/Makefile @@ -19,7 +19,7 @@ dvi: @echo -e "First compilation" @$(DVI) $(LATEXFLAGS) $(MAIN).tex @echo -e "Generating index" - @$(IDX) $(MAIN).idx + @$(IDX) $(OBJDIR)/$(MAIN).idx @echo -e "Generating bibliography" @$(BIB) --output-directory $(OBJDIR) $(MAIN) @echo -e "Generating glossary"
===================================== doc/rapport/infer.tex ===================================== --- a/doc/rapport/infer.tex +++ b/doc/rapport/infer.tex @@ -19,9 +19,9 @@ Elles sont utilisées uniquement pour faciliter la transformation des \sexp{} en \lexp{}.
\structpar{Les \lexp{}} - Les \lexp{}\ref{fig:ocmllxp} sont des expressions représentant les \textit{Lambda-Expressions} du $\lambda{}-calcul$. + Les \lexp{}~\ref{fig:ocmllxp} sont des expressions représentant les \textit{Lambda-Expressions} du $\lambda{}-calcul$. Elles servent de représentation intermédiaire du code \typer{}. - Les différentes opérations, comme la vérification de type, se fait sur les \lexp{}. + Les différentes opérations, comme la vérification de type, se font sur les \lexp{}.
\structpar{Détails} Lors de l'interprétation du code, il est tout d'abord \say{prélexé}. @@ -37,22 +37,41 @@ à avoir une information sur leur type.
\section{Unification} - L'unification est moyen permettant de déterminer si deux expressions sont équivalentes. - Dans le cas de l'inférence de type pour le compilateur \typer{}, - l'unification se fait sur les \lexp{}. - Deux \lexp{} sont unifiables si elles sont équivalentes. Si les expressions $S$ et $T$ - sont unifiables alors on peut écrire (en \typer{}) $S = T$. - - Dans le cas du compilateur \typer{}, l'unification permet de vérifier qu'il n'y a pas - d'erreur de typage. + \structpar{Définition} + L'unification est moyen permettant de déterminer si deux expressions sont équivalentes. + Dans le cas de l'inférence de type pour le compilateur \typer{}, + l'unification se fait sur les \lexp{}. + Deux \lexp{} sont unifiables si elles sont équivalentes. Si les expressions $S$ et $T$ + sont unifiables alors on peut écrire (en \typer{}) $S = T$. + + Dans le cas du compilateur \typer{}, l'unification permet de vérifier qu'il n'y a pas + d'erreur de typage. + + On note $e_1 \unif e_2$ l'unification de $e_1$ et $e_2$. + + \structpar{Exemple} + Par exemple: + \begin{itemize} + \item $3 + 3 \unif 2 * 3$ puisque ces deux opérations sont équivalentes. + \item $x + 1 \unif 10$ si et seulement si $x = 9$. + \item $1 + 2 \nunif "3"$ puisque les deux expressions n'ont pas le même type. + \end{itemize}
\subsection{Unification de premier ordre}
+ \structpar{Définition des méta-variable} + Une méta-variable est une variable libre. Elle sert de variable fictive et sera remplacée dès qu'on peut + associer cette méta-variable à une expression. + + Dans le reste du rapport, les méta-variables seront noté en majuscule. + % Par exemple: + % TODO : mettre un exemple + \structpar{L'unification des \lexp} L'unification de premier ordre permet de déterminer si deux \lexp{} sont équivalentes, dans les cas simples. Cependant, toutes les informations nécessaires ne sont pas toujours disponibles lors de l'unification. L'algorithme d'unification renvoie une liste de contraintes et une liste d'associations entre une méta-variable et une \lexp{} quelconque. - Le couple formé par ces deux listes est appelé le \textit{contexte d'unification}\ref{fig:ctxunif}. + Le couple formé par ces deux listes est appelé le \textit{contexte d'unification}~\ref{fig:ctxunif}.
\structpar{Cas Évident} Si deux \lexp{} sont équivalentes, elles sont unifiables. Par exemple, deux nombres égaux seront transformés en deux \lexp{} équivalentes. @@ -95,6 +114,17 @@ L'unification de premier ordre ne tient pas en compte des ajouts et suppressions de variables. C'est pourquoi cette forme d'unification ne suffit pas pour l'inférence de type requise par \typer{}.
+ Par exemple, si on essaie d'unifier + \begin{verbatim} + x + let x = 5 in x * y + \end{verbatim} + avec + \begin{verbatim} + A + let x = B in A * C + \end{verbatim} + l'unification renverra un résultat correct avec $A = x$. Cependant, le premier $x$ et le second $x$ de la première expression + ne correspondent pas à la même variable. L'unification devrait donc renvoyer une erreur. + \subsection{Unification des \hop{}} \structpar{\hop{}} L'unification de premier ordre ne suffit pas pour l'inférence de type requise par \typer{}. @@ -102,6 +132,16 @@ L'unification de \typer{} utilise un sous-ensemble de l'unification des \hop{} L'unification des \hop{} est un sous-ensemble décidable de l'unification d'ordre supérieur.
+ L'équation + \begin{equation} + F\ x\ y \unif x + y + \end{equation} + est un \hop{}. La solution de l'unification est $F = \lambda\ x\ y\ \rightarrow x + y$. + \begin{equation} + F\ x\ 1 \unif x + 1 + \end{equation} + n'est pas un \hop{}. Il y a plusieurs solutions non équivalentes: $F = \lambda\ x\ y \rightarrow x + y$ et $F = \lambda\ x\ y \rightarrow x + 1$ + \structpar{Les index de \textit{de Bruijn}} Les index de \textit{de Bruijn} sont une notation inventée par Nicolaas Govert de Bruijn qui sert à représenter les termes du $\lambda{}-calcul$. Cette notation utilise des index comme identificateur de variables (dans le code). L'index le plus grand @@ -113,6 +153,15 @@ Cependant, le décalage des index lié à l'ajout et la suppression de variables peut causer des erreurs lors de la comparaison d'une même variable dans des contextes différents.
+ Par exemple l'expression: + \begin{equation} + \lambda\ x \rightarrow (x, \lambda\ y \rightarrow x + y) + \end{equation} + sera encodé par: + \begin{equation} + \lambda \rightarrow (#0, \lambda \rightarrow #1 + #0) + \end{equation} + \structpar{La substitution des index de \textit{de Bruijn}} Pour remédier au problème de l'ajout et de la suppression de variables avec les index de \textit{de Bruijn}, on associe au contexte des variables une substitution. Cette substitution, une fois appliquée à un index, l'augmente ou le réduit. @@ -127,3 +176,10 @@ Cette modification permet de prendre en compte le contexte dans lequel la méta-variable a été créée et ainsi de pouvoir appliquer les substitutions lors de l'unification de variables dans des contextes différents.
+ Par exemple si on considère $A[\sigma]$ avec $A$ une méta-variable et $\sigma$ la substitution appliquée à $A$. + $A$ est une variable libre, sa valeur n'est pas connue. Il faut donc garder la substitution suspendue. + Pour résoudre $A[\sigma] \unif e$, avec $e$ une expression quelconque, il faut donc résoudre $A = e[\sigma^{-1}]$. + + $\sigma^{-1}$ est la substitution inverse de $\sigma$ tel que $\sigma \circ \sigma^{-1} = id$ et $e[\sigma \circ \sigma^{-1}] = e[id] = e$. + + % TODO : mettre un exemple concrèt ?
===================================== doc/rapport/main.tex ===================================== --- a/doc/rapport/main.tex +++ b/doc/rapport/main.tex @@ -45,8 +45,8 @@ morecomment=[l][\color{magenta}]{#} }
-\newcommand{\subsubsubsection}{\paragraph} -\renewcommand{\paragraph}{\subparagraph} +\AtBeginDocument{\renewcommand{\ref}[1]{(cf~\autoref{#1})}} + \setcounter{secnumdepth}{3}
\newcommand{\udem}{Université de Montréal} @@ -58,6 +58,9 @@ \newunicodechar{≡}{\ensuremath{\equiv}} \newunicodechar{α}{\ensuremath{\alpha}}
+\DeclareMathOperator{\unif}{\mathbin{=?}} +\DeclareMathOperator{\nunif}{\mathbin{\neq?}} + \title{Stage de quatrième année} \subtitle{Développement d'inférence de type pour le langage Typer} \author{BONNEVALLE Vincent}
===================================== doc/rapport/pres-univ.tex ===================================== --- a/doc/rapport/pres-univ.tex +++ b/doc/rapport/pres-univ.tex @@ -5,14 +5,17 @@ \structpar{Chiffres} L'\udem{} est une université située à Montréal au Canada. Elle a été créée en 1878. - Tout les départements de l'\udem{} sont situés sur le même campus sur le Mont Royal. + Une partie de l'université, dont le département informatique est située sur le Mont Royal. + L'école vétérinaire de l'université est à Sainte-Hyacinte, hors de Montréal. + Le reste de la faculté se situe sur le campus de Laval à Montréal. + Enfin, un nouveau campus est en train de se développer à Outremont et pourrait à terme remplacer celui du Mont Royal.
Elle est classée première université du Québec\cite{udemnum} et deuxième université du Canada\cite{udemnum}, que ce soit en nombre d'étudiants ou pour la recherche.
\structpar{Chiffres} Cette université accueille près de \num{67 000} étudiants et \num{2 700} chercheurs dans 16 facultés et écoles\cite{udemnum}. - Elle dispose d'un budget de \num{1,05} milliard de dollards canadiens\cite{wikinum} (en 2014). + Elle dispose d'un budget de \num{1,05} milliard de dollars canadiens\cite{wikinum} (en 2014).
L'\udem{} propose des programmes dans différents domaines d'études comme le droit, les sciences, la littérature \dots \begin{figure}[!h]
===================================== doc/rapport/typer.tex ===================================== --- a/doc/rapport/typer.tex +++ b/doc/rapport/typer.tex @@ -17,7 +17,7 @@ La syntaxe du code est proche de la syntaxe de \textit{ML}. L'inférence de type de \typer{} est un sur-ensemble de l'inférence de type \textit{Hindley-Milner} \structpar{Spécificités} - Les macros de \typer{} devraient, à terme, pouvoir être utilisées pour construire des preuves de programmes. % TODO : etoffer + Les macros de \typer{} devraient, à terme, pouvoir être utilisées pour construire des preuves de programmes.
\section{Motivations} \typer{} est un langage dont le but est de fournir des moyens d'écrire du code sûr.
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -77,54 +77,33 @@ type mdecl = | Ldecl of symbol * pexp option * pexp option | Lmcall of symbol * sexp list
- -let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = - match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with - | Sort (_, _) -> () (* All clear! *) - | _ -> lexp_error l ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_to_str ltp) - -let elab_check_proper_type (ctx : elab_context) ltp v = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp - with e -> print_string ("Exception while checking type `" - ^ lexp_to_str ltp ^ "` of var `" ^ - (let (_, name) = v in name) ^"`\n"); - print_lexp_ctx (ectx_to_lctx ctx); - raise e - -let elab_check_def (ctx : elab_context) var lxp ltype = - let lctx = ectx_to_lctx ctx in - if OL.conv_p ltype (OL.check lctx lxp) then - elab_check_proper_type ctx ltype var +let elab_check_def (ctx : lexp_context) var lxp ltype = + if OL.conv_p ltype (OL.check ctx lxp) then + () (* FIXME: Check ltype as well! *) else (print_string "¡¡ctx_define error!!\n"; lexp_print lxp; print_string " !: "; lexp_print ltype; print_string "\nbecause\n"; - lexp_print (OL.check lctx lxp); + lexp_print (OL.check ctx lxp); print_string " != "; lexp_print ltype; print_string "\n"; lexp_fatal (let (l,_) = var in l) "TC error")
let ctx_define (ctx: elab_context) var lxp ltype = - elab_check_def ctx var lxp ltype; + elab_check_def (ectx_to_lctx ctx) var lxp ltype; env_extend ctx var (LetDef lxp) ltype
let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in - let _ = List.fold_left (fun n (var, lxp, ltp) - -> elab_check_proper_type - nctx (push_susp ltp (S.shift n)) var; - n - 1) - (List.length decls) - decls in (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is * convertible to `Type_0`, because it doesn't have access to lctx. * + * let nlctx = ectx_to_lctx nctx in * let _ = List.fold_left (fun n (var, lxp, ltp) - * -> elab_check_def nctx var lxp + * -> elab_check_def nlctx var lxp * (push_susp ltp (S.shift n)); * n - 1) * (List.length decls) @@ -186,7 +165,16 @@ let mkMetavar () = let meta = Unif.create_metavar () let rec lexp_p_infer (p : pexp) (ctx : elab_context): lexp * ltype = _lexp_p_infer p ctx 1
-and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = +and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = + Debug_fun.do_debug (fun () -> + prerr_endline ("[StackTrace] ------------------------------------------"); + prerr_endline ("[StackTrace] let _lexp_p_infer p ctx i"); + prerr_endline ("[StackTrace] p = " ^ Fmt_lexp.string_of_pexp p); + prerr_endline ("[StackTrace] ctx = ???"); + prerr_endline ("[StackTrace] i = " ^ string_of_int i); + (* prerr_endline (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20)); *) + prerr_endline ("[StackTrace] ------------------------------------------"); + ());
let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) in let tloc = pexp_location p in @@ -339,7 +327,16 @@ and lexp_let_decls decls (body: lexp) ctx i = and lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context): lexp = _lexp_p_check p t ctx 1
-and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) i: lexp = +and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = + Debug_fun.do_debug (fun () -> + prerr_endline ("[StackTrace] ------------------------------------------"); + prerr_endline ("[StackTrace] let _lexp_p_check p t ctx i"); + prerr_endline ("[StackTrace] p = " ^ Fmt_lexp.string_of_pexp p); + prerr_endline ("[StackTrace] t = " ^ Fmt_lexp.string_of_lxp t); + prerr_endline ("[StackTrace] ctx = ???"); + prerr_endline ("[StackTrace] i = " ^ string_of_int i); + prerr_endline ("[StackTrace] ------------------------------------------"); + ()); let tloc = pexp_location p in
@@ -475,6 +472,15 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =
(* Identify Call Type and return processed call *) and lexp_call (func: pexp) (sargs: sexp list) ctx i = + Debug_fun.do_debug (fun () -> + prerr_endline ("[StackTrace] ------------------------------------------"); + prerr_endline ("[StackTrace] let lexp_call func sargs ctx i"); + prerr_endline ("[StackTrace] func = " ^ Fmt_lexp.string_of_pexp func); + prerr_endline ("[StackTrace] sargs = ???"); + prerr_endline ("[StackTrace] ctx = ???"); + prerr_endline ("[StackTrace] i = " ^ string_of_int i); + prerr_endline ("[StackTrace] ------------------------------------------"); + ()); let loc = pexp_location func in let meta_ctx, _ = !global_substitution in
@@ -741,6 +747,14 @@ and lexp_read_pattern_args args (args_type : lexp list) ctx:
(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx i = + Debug_fun.do_debug (fun () -> + prerr_endline ("[StackTrace] ------------------------------------------"); + prerr_endline ("[StackTrace] let lexp_parse_inductive ctors ctx i"); + prerr_endline ("[StackTrace] ctors = ???"); + prerr_endline ("[StackTrace] ctx = ???"); + prerr_endline ("[StackTrace] i = " ^ string_of_int i); + prerr_endline ("[StackTrace] ------------------------------------------"); + ()); let lexp_parse p ctx = _lexp_p_infer p ctx (i + 1) in
let make_args (args:(arg_kind * pvar option * pexp) list) ctx @@ -861,20 +875,8 @@ and lexp_decls_1 assert (pending_defs == [])); [], [], nctx
- | Ptype ((l, vname) as v, ptp) :: pdecls - -> let (ltp, lsort) = lexp_p_infer ptp nctx in - if SMap.mem vname pending_decls then - (lexp_error l ("Variable `" ^ vname ^ "` declared twice!"); - lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - else if List.exists (fun ((_, vname'), _, _) -> vname = vname') - pending_defs then - (lexp_error l ("Variable `" ^ vname ^ "` already defined!"); - lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - else (elab_check_sort nctx lsort v ltp; - lexp_decls_1 pdecls ectx - (env_extend nctx v ForwardRef ltp) - (SMap.add vname (l, ltp) pending_decls) - pending_defs) + let is_empty = (List.length !pending) = 0 in + let is_one = (List.length !pending) = 1 in
| Pexpr ((l, vname) as v, pexp) :: pdecls when SMap.is_empty pending_decls
===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -18,7 +18,8 @@ open Str open Debug
open Fmt_lexp -open Debug_fun + +open Log
type result = | Constraint
View it on GitLab: https://gitlab.com/monnier/typer/compare/c2626ca77dcdf2a236567807146ecc31371...