Mercurial > emacs
comparison test/indent/prolog.prolog @ 108864:f241d9fe71fe
* lisp/emacs-lisp/smie.el (smie-indent-calculate): Simplify and cleanup.
(smie-indent-hanging-p): Use smie-bolp.
* test/indent: New dir.
author | Stefan Monnier <monnier@iro.umontreal.ca> |
---|---|
date | Wed, 02 Jun 2010 16:13:11 -0400 |
parents | |
children | f81447dd641c |
comparison
equal
deleted
inserted
replaced
108863:608a41397301 | 108864:f241d9fe71fe |
---|---|
1 %% -*- mode: prolog; coding: utf-8 -*- | |
2 | |
3 %% wf(+E) | |
4 %% Vérifie que E est une expression syntaxiquement correcte. | |
5 wf(X) :- atom(X); integer(X); var(X). %Une variable ou un entier. | |
6 wf(lambda(X, T, B)) :- atom(X), wf(T), wf(B). %Une fonction. | |
7 wf(app(E1, E2)) :- wf(E1), wf(E2). %Un appel de fonction. | |
8 wf(pi(X, T, B)) :- atom(X), wf(T), wf(B). %Le type d'une fonction. | |
9 | |
10 %% Éléments additionnels utilisés dans le langage source. | |
11 wf(lambda(X, B)) :- atom(X), wf(B). | |
12 wf(let(X, E1, E2)) :- atom(X), wf(E1), wf(E2). | |
13 wf(let(X, T, E1, E2)) :- atom(X), wf(T), wf(E1), wf(E2). | |
14 wf((T1 -> T2)) :- wf(T1), wf(T2). | |
15 wf(forall(X, T, B)) :- atom(X), wf(T), wf(B). | |
16 wf(fix(X,T,E1,E2)) :- atom(X), wf(T), wf(E1), wf(E2). | |
17 wf(fix(X,E1,E2)) :- atom(X), wf(E1), wf(E2). | |
18 wf(app(E1,E2,E3)) :- wf(E1), wf(E2), wf(E3). | |
19 wf(app(E1,E2,E3,E4)) :- wf(E1), wf(E2), wf(E3), wf(E4). | |
20 | |
21 %% subst(+X, +V, +FV, +Ei, -Eo) | |
22 %% Remplace X par V dans Ei. Les variables qui apparaissent libres dans | |
23 %% V et peuvent aussi apparaître dans Ei doivent toutes être inclues | |
24 %% dans l'environnement FV. | |
25 subst(X, V, _, X, E) :- !, E = V. | |
26 subst(_, _, _, Y, Y) :- atom(Y); integer(Y). | |
27 %% Residualize the substitution when applied to an uninstantiated variable. | |
28 %% subst(X, V, _, Y, app(lambda(X,_,Y),V)) :- var(Y). | |
29 %% Rather than residualize and leave us with unifications that fail, let's | |
30 %% rather assume that Y will not refer to X. | |
31 subst(X, V, _, Y, Y) :- var(Y). | |
32 subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)) :- | |
33 subst(X, V, FV, Ti, To), | |
34 (X = Y -> | |
35 %% If X is equal to Y, X is shadowed, so no subst can take place. | |
36 Y1 = Y, Bo = Bi; | |
37 (member((Y, _), FV) -> | |
38 %% If Y appears in FV, it can appear in V, so we need to | |
39 %% rename it to avoid name capture. | |
40 new_atom(Y, Y1), | |
41 subst(Y, Y1, [], Bi, Bi1); | |
42 Y1 = Y, Bi1 = Bi), | |
43 %% Perform substitution on the body. | |
44 subst(X, V, FV, Bi1, Bo)). | |
45 subst(X, V, FV, pi(Y, Ti, Bi), pi(Y1, To, Bo)) :- | |
46 subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)). | |
47 subst(X, V, FV, forall(Y, Ti, Bi), forall(Y1, To, Bo)) :- | |
48 subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)). | |
49 subst(X, V, FV, app(E1i, E2i), app(E1o, E2o)) :- | |
50 subst(X, V, FV, E1i, E1o), subst(X, V, FV, E2i, E2o). | |
51 | |
52 %% apply(+F, +Arg, +Env, -E) | |
53 apply(lambda(X, _, B), Arg, Env, E) :- \+ var(B), subst(X, Arg, Env, B, E). | |
54 apply(app(plus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 + N2. | |
55 apply(app(minus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 - N2. | |
56 | |
57 | |
58 %% normalize(+E1, +Env, -E2) | |
59 %% Applique toutes les réductions possibles sur E1. | |
60 normalize(X, _, X) :- integer(X); var(X); atom(X). | |
61 %% normalize(X, Env, E) :- atom(X), member((X, E), Env). | |
62 normalize(lambda(X, T, B), Env, lambda(X, Tn, Bn)) :- | |
63 normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn). | |
64 normalize(pi(X, T, B), Env, pi(X, Tn, Bn)) :- | |
65 normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn). | |
66 normalize(forall(X, T, B), Env, forall(X, Tn, Bn)) :- | |
67 normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn). | |
68 normalize(app(E1, E2), Env, En) :- | |
69 normalize(E1, Env, E1n), | |
70 normalize(E2, Env, E2n), | |
71 (apply(E1n, E2n, Env, E) -> | |
72 normalize(E, Env, En); | |
73 En = app(E1n, E2n)). | |
74 | |
75 %% infer(+E, +Env, -T) | |
76 %% Infère le type de E dans Env. On essaie d'être permissif, dans le sens | |
77 %% que l'on présume que l'expression est typée correctement. | |
78 infer(X, _, int) :- integer(X). | |
79 infer(X, _, _) :- var(X). %Une expression encore inconnue. | |
80 infer(X, Env, T) :- | |
81 atom(X), | |
82 (member((X, T1), Env) -> | |
83 %% X est déjà dans Env: vérifie que le type est correct. | |
84 T = T1; | |
85 %% X est une variable libre. | |
86 true). | |
87 infer(lambda(X,T,B), Env, pi(Y,T,TB)) :- | |
88 infer(B, [(X,T)|Env], TBx), | |
89 (var(Y) -> | |
90 Y = X, TB = TBx; | |
91 subst(X, Y, Env, TBx, TB)). | |
92 infer(app(E1, E2), Env, Tn) :- | |
93 infer(E1, Env, T1), | |
94 (T1 = pi(X,T2,B); T1 = forall(X,T2,B)), | |
95 infer(E2, Env, T2), | |
96 subst(X, E2, Env, B, T), | |
97 normalize(T, Env, Tn). | |
98 infer(pi(X,T1,T2), Env, type) :- | |
99 infer(T1, Env, type), | |
100 infer(T2, [(X,T1)|Env], type). | |
101 infer(forall(X,T1,T2), Env, type) :- | |
102 infer(T1, Env, type), | |
103 infer(T2, [(X,T1)|Env], type). | |
104 | |
105 %% freevars(+E, +Env, -Vs) | |
106 %% Renvoie les variables libres de E. Vs est une liste associative | |
107 %% où chaque élément est de la forme (X,T) où X est une variable et T est | |
108 %% son type. | |
109 freevars(X, _, []) :- integer(X). | |
110 freevars(X, Env, Vs) :- | |
111 atom(X), | |
112 (member((X,_), Env) -> | |
113 %% Variable liée. | |
114 Vs = []; | |
115 %% Variable libre. Type inconnu :-( | |
116 Vs = [(X,_)]). | |
117 %% Les variables non-instanciées peuvent être remplacées par des paramètres | |
118 %% qui seront liés par `closetype' selon le principe de Hindley-Milner. | |
119 freevars(X, _, [(X, _)]) :- var(X), new_atom(X). | |
120 freevars(app(E1, E2), Env, Vs) :- | |
121 freevars(E1, Env, Vs1), | |
122 append(Vs1, Env, Env1), | |
123 freevars(E2, Env1, Vs2), | |
124 append(Vs1, Vs2, Vs). | |
125 freevars(lambda(X, T, B), Env, Vs) :- | |
126 freevars(T, Env, TVs), | |
127 append(TVs, Env, Env1), | |
128 freevars(B, [(X,T)|Env1], BVs), | |
129 append(TVs, BVs, Vs). | |
130 freevars(pi(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs). | |
131 freevars(forall(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs). | |
132 | |
133 %% close(+Eo, +To, +Vs, -Ec, -Tc) | |
134 %% Ferme un type ouvert To en liant chaque variable libre (listées dans Vs) | |
135 %% avec `forall'. | |
136 closetype(E, T, [], E, T). | |
137 closetype(Eo, To, [(X,T)|Vs], lambda(X, T, Ec), forall(X, T, Tc)) :- | |
138 closetype(Eo, To, Vs, Ec, Tc). | |
139 | |
140 %% elab_type(+Ee, +Te, +Env, -Eg, -Tg) | |
141 %% Ajoute les arguments implicites de E:T. | |
142 generalize(Ee, Te, Env, Eg, Tg) :- | |
143 freevars(Te, Env, Vs), | |
144 append(Vs, Env, EnvX), | |
145 %% Essaie d'instancier les types des paramètres que `generalize' vient | |
146 %% d'ajouter. | |
147 infer(Te, EnvX, type), | |
148 closetype(Ee, Te, Vs, Eg, Tg). | |
149 | |
150 %% instantiate(+X, +T, -E) | |
151 %% Utilise la variable X de type T. Le résultat E est X auquel on ajoute | |
152 %% tous les arguments implicites (de valeur inconnue). | |
153 instantiate(X, T, X) :- var(T), ! . | |
154 instantiate(X, forall(_, _, T), app(E, _)) :- !, instantiate(X, T, E). | |
155 instantiate(X, _, X). | |
156 | |
157 %% elaborate(+E1, +Env, -E2) | |
158 %% Transforme E1 en une expression E2 où le sucre syntaxique a été éliminé | |
159 %% et où les arguments implicites ont été rendus explicites. | |
160 elaborate(X, _, X) :- integer(X); var(X). | |
161 elaborate(X, Env, E) :- | |
162 atom(X), | |
163 (member((X, T), Env) -> | |
164 instantiate(X, T, E); | |
165 %% Si X n'est pas dans l'environnement, c'est une variable libre que | |
166 %% l'on voudra probablement généraliser. | |
167 X = E). | |
168 elaborate(lambda(X, T, B), Env, lambda(X, Te, Be)) :- | |
169 elaborate(T, Env, Te), | |
170 elaborate(B, [(X,Te)|Env], Be). | |
171 elaborate(pi(X, T, B), Env, pi(X, Te, Be)) :- | |
172 elaborate(T, Env, Te), | |
173 elaborate(B, [(X,Te)|Env], Be). | |
174 elaborate(app(E1, E2), Env, app(E1e, E2e)) :- | |
175 elaborate(E1, Env, E1e), | |
176 elaborate(E2, Env, E2e). | |
177 elaborate(let(X, T, E1, E2), Env, app(lambda(X, Tg, E2e), E1g)) :- | |
178 elaborate(E1, Env, E1e), | |
179 elaborate(T, Env, Te), | |
180 infer(E1e, Env, Te), | |
181 generalize(E1e, Te, Env, E1g, Tg), | |
182 elaborate(E2, [(X,Te)|Env], E2e). | |
183 %% Expansion du sucre syntaxique. | |
184 elaborate((T1 -> T2), Env, Ee) :- | |
185 new_atom(X), elaborate(pi(X, T1, T2), Env, Ee). | |
186 elaborate(app(E1, E2, E3, E4), Env, Ee) :- | |
187 elaborate(app(app(E1,E2,E3),E4), Env, Ee). | |
188 elaborate(app(E1, E2, E3), Env, Ee) :- elaborate(app(app(E1,E2),E3), Env, Ee). | |
189 elaborate(lambda(X, B), Env, Ee) :- elaborate(lambda(X, _, B), Env, Ee). | |
190 elaborate(let(X, E1, E2), Env, Ee) :- elaborate(let(X, _, E1, E2), Env, Ee). | |
191 elaborate(fix(F,B,E), Env, Ee) :- elaborate(fix(F,_,B,E), Env, Ee). | |
192 elaborate(fix(F,T,B,E), Env, Ee) :- | |
193 elaborate(let(F,T,app(fix,lambda(F,T,B)),E), Env, Ee). | |
194 | |
195 %% elab_bindings(+TS, +Env, -TS). | |
196 %% Applique `elaborate' sur l'environnment de type TS. | |
197 elab_tenv([], _, []). | |
198 elab_tenv([(X,T)|TS], Env, [(X, Tg)|TSe]) :- | |
199 elaborate(T, Env, Te), | |
200 infer(Te, Env, type), | |
201 generalize(_, Te, Env, _, Tg), | |
202 elab_tenv(TS, [(X, Tg)|Env], TSe). | |
203 | |
204 | |
205 %% elaborate(+E1, -E2) | |
206 %% Comme le `elaborate' ci-dessus, mais avec un environnement par défaut. | |
207 elaborate(SRC, E) :- | |
208 elab_tenv([(int, type), | |
209 (fix, ((t -> t) -> t)), | |
210 %% list: type → int → type | |
211 (list, (type -> int -> type)), | |
212 %% plus: int → int → int | |
213 (plus, (int -> int -> int)), | |
214 %% minus: int → int → int | |
215 (minus, (int -> int -> int)), | |
216 %% nil: list t 0 | |
217 (nil, app(app(list,t),0)), | |
218 %% cons: t -> list t n → list t (n + 1) | |
219 (cons, (t -> app(app(list,t),n) -> | |
220 app(app(list,t), app(app(plus,n),1)))) %fixindent | |
221 ], | |
222 [(type,type)], | |
223 Env), | |
224 elaborate(SRC, Env, E). |