1 %% -*- mode: prolog; coding: utf-8; fill-column: 78 -*-
25 %% Testing correct tokenizing.
28 foo(X) :- '\x45\' = X.
33 %% Vérifie que E est une expression syntaxiquement correcte.
34 wf(X) :- atom(X); integer(X); var(X). %Une variable ou un entier.
35 wf(lambda(X, T, B)) :- atom(X), wf(T), wf(B). %Une fonction.
36 wf(app(E1, E2)) :- wf(E1), wf(E2). %Un appel de fonction.
37 wf(pi(X, T, B)) :- atom(X), wf(T), wf(B). %Le type d'une fonction.
39 %% Éléments additionnels utilisés dans le langage source.
40 wf(lambda(X, B)) :- atom(X), wf(B).
41 wf(let(X, E1, E2)) :- atom(X), wf(E1), wf(E2).
42 wf(let(X, T, E1, E2)) :- atom(X), wf(T), wf(E1), wf(E2).
43 wf((T1 -> T2)) :- wf(T1), wf(T2).
44 wf(forall(X, T, B)) :- atom(X), wf(T), wf(B).
45 wf(fix(X,T,E1,E2)) :- atom(X), wf(T), wf(E1), wf(E2).
46 wf(fix(X,E1,E2)) :- atom(X), wf(E1), wf(E2).
47 wf(app(E1,E2,E3)) :- wf(E1), wf(E2), wf(E3).
48 wf(app(E1,E2,E3,E4)) :- wf(E1), wf(E2), wf(E3), wf(E4).
50 %% subst(+X, +V, +FV, +Ei, -Eo)
51 %% Remplace X par V dans Ei. Les variables qui apparaissent libres dans
52 %% V et peuvent aussi apparaître dans Ei doivent toutes être inclues
53 %% dans l'environnement FV.
54 subst(X, V, _, X, E) :- !, E = V.
55 subst(_, _, _, Y, Y) :- atom(Y); integer(Y).
56 %% Residualize the substitution when applied to an uninstantiated variable.
57 %% subst(X, V, _, Y, app(lambda(X,_,Y),V)) :- var(Y).
58 %% Rather than residualize and leave us with unifications that fail, let's
59 %% rather assume that Y will not refer to X.
60 subst(X, V, _, Y, Y) :- var(Y).
61 subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)) :-
62 subst(X, V, FV, Ti, To),
64 %% If X is equal to Y, X is shadowed, so no subst can take place.
66 (member((Y, _), FV) ->
67 %% If Y appears in FV, it can appear in V, so we need to
68 %% rename it to avoid name capture.
70 subst(Y, Y1, [], Bi, Bi1);
72 %% Perform substitution on the body.
73 subst(X, V, FV, Bi1, Bo)),
75 %% If X is equal to Y, X is shadowed, so no subst can take place.
78 %% If Y appears in FV, it can appear in V, so we need to
79 %% rename it to avoid name capture.
81 subst(Y, Y1, [], Bi, Bi1)
83 %% Perform substitution on the body.
84 subst(X, V, FV, Bi1, Bo)
86 subst(X, V, FV, pi(Y, Ti, Bi), pi(Y1, To, Bo)) :-
87 subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)).
88 subst(X, V, FV, forall(Y, Ti, Bi), forall(Y1, To, Bo)) :-
89 subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)).
90 subst(X, V, FV, app(E1i, E2i), app(E1o, E2o)) :-
91 subst(X, V, FV, E1i, E1o), subst(X, V, FV, E2i, E2o).
93 %% apply(+F, +Arg, +Env, -E)
94 apply(lambda(X, _, B), Arg, Env, E) :- \+ var(B), subst(X, Arg, Env, B, E).
95 apply(app(plus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 + N2.
96 apply(app(minus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 - N2.
99 %% normalize(+E1, +Env, -E2)
100 %% Applique toutes les réductions possibles sur E1.
101 normalize(X, _, X) :- integer(X); var(X); atom(X).
102 %% normalize(X, Env, E) :- atom(X), member((X, E), Env).
103 normalize(lambda(X, T, B), Env, lambda(X, Tn, Bn)) :-
104 normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn).
105 normalize(pi(X, T, B), Env, pi(X, Tn, Bn)) :-
106 normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn).
107 normalize(forall(X, T, B), Env, forall(X, Tn, Bn)) :-
108 normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn).
109 normalize(app(E1, E2), Env, En) :-
110 normalize(E1, Env, E1n),
111 normalize(E2, Env, E2n),
112 (apply(E1n, E2n, Env, E) ->
113 normalize(E, Env, En);
116 %% infer(+E, +Env, -T)
117 %% Infère le type de E dans Env. On essaie d'être permissif, dans le sens
118 %% que l'on présume que l'expression est typée correctement.
119 infer(X, _, int) :- integer(X).
120 infer(X, _, _) :- var(X). %Une expression encore inconnue.
123 (member((X, T1), Env) ->
124 %% X est déjà dans Env: vérifie que le type est correct.
126 %% X est une variable libre.
128 infer(lambda(X,T,B), Env, pi(Y,T,TB)) :-
129 infer(B, [(X,T)|Env], TBx),
132 subst(X, Y, Env, TBx, TB)).
133 infer(app(E1, E2), Env, Tn) :-
135 (T1 = pi(X,T2,B); T1 = forall(X,T2,B)),
137 subst(X, E2, Env, B, T),
138 normalize(T, Env, Tn).
139 infer(pi(X,T1,T2), Env, type) :-
140 infer(T1, Env, type),
141 infer(T2, [(X,T1)|Env], type).
142 infer(forall(X,T1,T2), Env, type) :-
143 infer(T1, Env, type),
144 infer(T2, [(X,T1)|Env], type).
146 %% freevars(+E, +Env, -Vs)
147 %% Renvoie les variables libres de E. Vs est une liste associative
148 %% où chaque élément est de la forme (X,T) où X est une variable et T est
150 freevars(X, _, []) :- integer(X).
151 freevars(X, Env, Vs) :-
153 (member((X,_), Env) ->
156 %% Variable libre. Type inconnu :-(
158 %% Les variables non-instanciées peuvent être remplacées par des paramètres
159 %% qui seront liés par `closetype' selon le principe de Hindley-Milner.
160 freevars(X, _, [(X, _)]) :- var(X), new_atom(X).
161 freevars(app(E1, E2), Env, Vs) :-
162 freevars(E1, Env, Vs1),
163 append(Vs1, Env, Env1),
164 freevars(E2, Env1, Vs2),
165 append(Vs1, Vs2, Vs).
166 freevars(lambda(X, T, B), Env, Vs) :-
167 freevars(T, Env, TVs),
168 append(TVs, Env, Env1),
169 freevars(B, [(X,T)|Env1], BVs),
170 append(TVs, BVs, Vs).
171 freevars(pi(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs).
172 freevars(forall(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs).
174 %% close(+Eo, +To, +Vs, -Ec, -Tc)
175 %% Ferme un type ouvert To en liant chaque variable libre (listées dans Vs)
177 closetype(E, T, [], E, T).
178 closetype(Eo, To, [(X,T)|Vs], lambda(X, T, Ec), forall(X, T, Tc)) :-
179 closetype(Eo, To, Vs, Ec, Tc).
181 %% elab_type(+Ee, +Te, +Env, -Eg, -Tg)
182 %% Ajoute les arguments implicites de E:T.
183 generalize(Ee, Te, Env, Eg, Tg) :-
184 freevars(Te, Env, Vs),
185 append(Vs, Env, EnvX),
186 %% Essaie d'instancier les types des paramètres que `generalize' vient
188 infer(Te, EnvX, type),
189 closetype(Ee, Te, Vs, Eg, Tg).
191 %% instantiate(+X, +T, -E)
192 %% Utilise la variable X de type T. Le résultat E est X auquel on ajoute
193 %% tous les arguments implicites (de valeur inconnue).
194 instantiate(X, T, X) :- var(T), !.
195 instantiate(X, forall(_, _, T), app(E, _)) :- !, instantiate(X, T, E).
196 instantiate(X, _, X).
198 %% elaborate(+E1, +Env, -E2)
199 %% Transforme E1 en une expression E2 où le sucre syntaxique a été éliminé
200 %% et où les arguments implicites ont été rendus explicites.
201 elaborate(X, _, X) :- integer(X); var(X).
202 elaborate(X, Env, E) :-
204 (member((X, T), Env) ->
205 instantiate(X, T, E);
206 %% Si X n'est pas dans l'environnement, c'est une variable libre que
207 %% l'on voudra probablement généraliser.
209 elaborate(lambda(X, T, B), Env, lambda(X, Te, Be)) :-
210 elaborate(T, Env, Te),
211 elaborate(B, [(X,Te)|Env], Be).
212 elaborate(pi(X, T, B), Env, pi(X, Te, Be)) :-
213 elaborate(T, Env, Te),
214 elaborate(B, [(X,Te)|Env], Be).
215 elaborate(app(E1, E2), Env, app(E1e, E2e)) :-
216 elaborate(E1, Env, E1e),
217 elaborate(E2, Env, E2e).
218 elaborate(let(X, T, E1, E2), Env, app(lambda(X, Tg, E2e), E1g)) :-
219 elaborate(E1, Env, E1e),
220 elaborate(T, Env, Te),
222 generalize(E1e, Te, Env, E1g, Tg),
223 elaborate(E2, [(X,Te)|Env], E2e).
224 %% Expansion du sucre syntaxique.
225 elaborate((T1 -> T2), Env, Ee) :-
226 new_atom(X), elaborate(pi(X, T1, T2), Env, Ee).
227 elaborate(app(E1, E2, E3, E4), Env, Ee) :-
228 elaborate(app(app(E1,E2,E3),E4), Env, Ee).
229 elaborate(app(E1, E2, E3), Env, Ee) :- elaborate(app(app(E1,E2),E3), Env, Ee).
230 elaborate(lambda(X, B), Env, Ee) :- elaborate(lambda(X, _, B), Env, Ee).
231 elaborate(let(X, E1, E2), Env, Ee) :- elaborate(let(X, _, E1, E2), Env, Ee).
232 elaborate(fix(F,B,E), Env, Ee) :- elaborate(fix(F,_,B,E), Env, Ee).
233 elaborate(fix(F,T,B,E), Env, Ee) :-
234 elaborate(let(F,T,app(fix,lambda(F,T,B)),E), Env, Ee).
236 %% elab_bindings(+TS, +Env, -TS).
237 %% Applique `elaborate' sur l'environnement de type TS.
238 elab_tenv([], _, []).
239 elab_tenv([(X,T)|TS], Env, [(X, Tg)|TSe]) :-
240 elaborate(T, Env, Te),
241 infer(Te, Env, type),
242 generalize(_, Te, Env, _, Tg),
243 elab_tenv(TS, [(X, Tg)|Env], TSe).
246 %% elaborate(+E1, -E2)
247 %% Comme le `elaborate' ci-dessus, mais avec un environnement par défaut.
249 elab_tenv([(int, type),
250 (fix, ((t -> t) -> t)),
251 %% list: type → int → type
252 (list, (type -> int -> type)),
253 %% plus: int → int → int
254 (plus, (int -> int -> int)),
255 %% minus: int → int → int
256 (minus, (int -> int -> int)),
258 (nil, app(app(list,t),0)),
259 %% cons: t -> list t n → list t (n + 1)
260 (cons, (t -> app(app(list,t),n) ->
261 app(app(list,t), app(app(plus,n),1)))) %fixindent
265 elaborate(SRC, Env, E).