%% -*- mode: prolog; coding: utf-8 -*- %% wf(+E) %% Vérifie que E est une expression syntaxiquement correcte. wf(X) :- atom(X); integer(X); var(X). %Une variable ou un entier. wf(lambda(X, T, B)) :- atom(X), wf(T), wf(B). %Une fonction. wf(app(E1, E2)) :- wf(E1), wf(E2). %Un appel de fonction. wf(pi(X, T, B)) :- atom(X), wf(T), wf(B). %Le type d'une fonction. %% Éléments additionnels utilisés dans le langage source. wf(lambda(X, B)) :- atom(X), wf(B). wf(let(X, E1, E2)) :- atom(X), wf(E1), wf(E2). wf(let(X, T, E1, E2)) :- atom(X), wf(T), wf(E1), wf(E2). wf((T1 -> T2)) :- wf(T1), wf(T2). wf(forall(X, T, B)) :- atom(X), wf(T), wf(B). wf(fix(X,T,E1,E2)) :- atom(X), wf(T), wf(E1), wf(E2). wf(fix(X,E1,E2)) :- atom(X), wf(E1), wf(E2). wf(app(E1,E2,E3)) :- wf(E1), wf(E2), wf(E3). wf(app(E1,E2,E3,E4)) :- wf(E1), wf(E2), wf(E3), wf(E4). %% subst(+X, +V, +FV, +Ei, -Eo) %% Remplace X par V dans Ei. Les variables qui apparaissent libres dans %% V et peuvent aussi apparaître dans Ei doivent toutes être inclues %% dans l'environnement FV. subst(X, V, _, X, E) :- !, E = V. subst(_, _, _, Y, Y) :- atom(Y); integer(Y). %% En fait, si Y est un terme non-instancié, la substitution ne peut pas %% encore se faire. On pourrait renvoyer app(lambda(X,Y),V), mais dans %% beaucoup de cas le terme dont on a besoin dans Y ne peut pas faire %% référence à X. Donc on impose ici cette contrainte. Le faire vraiment %% correctement est beaucoup plus difficile. subst(_, _, _, Y, Y) :- var(Y). %% !!!À COMPLÉTER!!! %% apply(+F, +Arg, +Env, -E) %% Les règles d'évaluations primitives. Env donne le types des variables %% libres qui peuvent apparaîtres. apply(lambda(X, _, B), Arg, Env, E) :- \+ var(B), subst(X, Arg, Env, B, E). apply(app(plus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 + N2. apply(app(minus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 - N2. %% normalize(+E1, +Env, -E2) %% Applique toutes les réductions possibles sur E1. %% Utilisé pour tester si deux types sont équivalents. normalize(X, _, X) :- integer(X); var(X); atom(X). %% !!!À COMPLÉTER!!! %% infer(+E, +Env, -T) %% Infère le type de E dans Env. On essaie d'être permissif, dans le sens %% que l'on présume que l'expression est typée correctement. infer(X, _, int) :- integer(X). infer(X, _, _) :- var(X). %Une expression encore inconnue. infer(X, Env, T) :- atom(X), (member((X, T1), Env) -> %% X est déjà dans Env: vérifie que le type est correct. T = T1; %% X est une variable libre, on ne connait donc pas encore son type. true). infer(forall(X,T1,T2), Env, type) :- infer(pi(X,T1,T2), Env, type). %% !!!À COMPLÉTER!!! %% freevars(+E, +Env, -Vs) %% Renvoie les variables libres de E. Vs est une liste associative %% où chaque élément est de la forme (X,T) où X est une variable et T est %% son type. freevars(X, _, []) :- integer(X). freevars(X, Env, Vs) :- atom(X), (member((X,_), Env) -> %% Variable liée. Vs = []; %% Variable libre. Type encore inconnu :-( Vs = [(X,_)]). %% Les variables non-instanciées peuvent être remplacées par des paramètres %% qui seront liés par `closetype' selon le principe de Hindley-Milner. freevars(X, _, [(X, _)]) :- var(X), new_atom(X). freevars(app(E1, E2), Env, Vs) :- freevars(E1, Env, Vs1), append(Vs1, Env, Env1), freevars(E2, Env1, Vs2), append(Vs1, Vs2, Vs). freevars(lambda(X, T, B), Env, Vs) :- freevars(T, Env, TVs), append(TVs, Env, Env1), freevars(B, [(X,T)|Env1], BVs), append(TVs, BVs, Vs). freevars(pi(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs). freevars(forall(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs). %% close(+Eo, +To, +Vs, -Ec, -Tc) %% Ferme un type ouvert To en liant chaque variable libre (listées dans Vs) %% avec `forall'. closetype(E, T, [], E, T). closetype(Eo, To, [(X,T)|Vs], lambda(X, T, Ec), forall(X, T, Tc)) :- closetype(Eo, To, Vs, Ec, Tc). %% generalize(+Ee, +Te, +Env, -Eg, -Tg) %% Ajoute les arguments implicites de Ee:Te. generalize(Ee, Te, Env, Eg, Tg) :- freevars(Te, Env, Vs), append(Vs, Env, EnvX), closetype(Ee, Te, Vs, Eg, Tg), %% Essaie d'instancier les types des paramètres que `closetype' vient %% d'ajouter. infer(Tg, EnvX, type). %% instantiate(+X, +T, -E) %% Utilise la variable X de type T. Le résultat E est X auquel on ajoute %% tous les arguments implicites (de valeur encore inconnue). instantiate(X, T, X) :- var(T), !. instantiate(X, forall(_, _, T), app(E, _)) :- !, instantiate(X, T, E). instantiate(X, _, X). %% elaborate(+E1, +Env, -E2) %% Transforme E1 en une expression E2 où le sucre syntaxique a été éliminé %% et où les arguments implicites ont été rendus explicites. I.e. E2 ne %% contiendra plus de sucre syntaxique, et tous les types seront fournis %% explicitement. elaborate(X, _, X) :- integer(X); var(X). elaborate(X, Env, E) :- atom(X), (member((X, T), Env) -> instantiate(X, T, E); %% Si X n'est pas dans l'environnement, c'est une variable libre que %% l'on voudra probablement généraliser. X = E). elaborate(let(X, T, E1, E2), Env, app(lambda(X, Tg, E2e), E1g)) :- elaborate(E1, Env, E1e), elaborate(T, Env, Te), infer(E1e, Env, Te), generalize(E1e, Te, Env, E1g, Tg), elaborate(E2, [(X,Te)|Env], E2e). %% !!!À COMPLÉTER!!! %% elaborate(+E1, -E2) %% Comme le `elaborate' ci-dessus, mais avec un environnement par défaut. elaborate(SRC, E) :- elaborate(SRC, [(type, type), (int, type), %% fix: (t → t) → t (fix, forall(t,type,pi(x,pi(x,t,t),t))), %% list: type → int → type (list, pi(x,type,pi(x,int,type))), %% plus: int → int → int (plus, pi(x,int,pi(x,int,int))), %% minus: int → int → int (minus,pi(x,int,pi(x,int,int))), %% nil: list t 0 (nil, forall(t,type,app(app(list,t),0))), %% cons: t -> list t n → list t (n + 1) (cons, forall(t,type, pi(x,t, forall(n,int, pi(x,app(app(list,t),n), app(app(list,t), app(app(plus,n),1)))))))], E).