annotate test/indent/prolog.prolog @ 112434:9de5a68b57e1

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