test/manual/indent/prolog.prolog

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