:type 'integer)
(defvar smie-indent-rules 'unset
+ ;; TODO: For SML, we need more rule formats, so as to handle
+ ;; structure Foo =
+ ;; Bar (toto)
+ ;; and
+ ;; structure Foo =
+ ;; struct ... end
+ ;; I.e. the indentation after "=" depends on the parent ("structure")
+ ;; as well as on the following token ("struct").
"Rules of the following form.
\(TOK OFFSET) how to indent right after TOK.
\(TOK O1 O2) how to indent right after TOK:
(forward-char 1))
(skip-chars-forward " \t")
(eolp))
- (save-excursion (skip-chars-backward " \t") (not (bolp)))))
+ (not (smie-bolp))))
(defun smie-bolp ()
(save-excursion (skip-chars-backward " \t") (bolp)))
to be good only if it follows a line break.
- :hanging: means that the current indentation of point can be
trusted to be good except if the following token is hanging."
- ;; FIXME: This has accumulated a lot of rules, some of which aren't
- ;; clearly orthogonal any more, so we should probably try and
- ;; restructure it somewhat.
(or
;; Trust pre-existing indentation on other lines.
(and virtual
(forward-comment (point-max))
(skip-chars-forward " \t\r\n")
(smie-indent-calculate nil)))
- ;; indentation inside a comment.
- ;; FIXME: Hey, this is not generic!!
- (and (looking-at "\\*") (nth 4 (syntax-ppss))
+ ;; indentation of comment-continue lines.
+ (and (< 0 (length comment-continue))
+ (looking-at (regexp-quote comment-continue)) (nth 4 (syntax-ppss))
(let ((ppss (syntax-ppss)))
(save-excursion
(forward-line -1)
(if (<= (point) (nth 8 ppss))
(progn (goto-char (1+ (nth 8 ppss))) (current-column))
(skip-chars-forward " \t")
- (if (looking-at "\\*")
+ (if (looking-at (regexp-quote comment-continue))
(current-column))))))
;; Indentation right after a special keyword.
(save-excursion
(let* ((tok (funcall smie-backward-token-function))
(tokinfo (assoc tok smie-indent-rules))
- (toklevel (assoc tok smie-op-levels)))
- (when (or tokinfo (and toklevel (null (cadr toklevel))))
- (if (or (smie-indent-hanging-p)
- ;; If calculating the virtual indentation point, prefer
- ;; looking up the virtual indentation of the alignment
- ;; point as well. This is used for indentation after
- ;; "fn x => fn y =>".
- virtual)
+ (toklevel (if (and (zerop (length tok))
+ ;; 4 == Open paren syntax.
+ (eq (syntax-class (syntax-after (1- (point))))
+ 4))
+ (progn (forward-char -1)
+ (setq tok (buffer-substring
+ (point) (1+ (point))))
+ (setq tokinfo (assoc tok smie-indent-rules))
+ (list tok nil 0))
+ (assoc tok smie-op-levels))))
+ (if (and toklevel (null (cadr toklevel)) (null tokinfo))
+ (setq tokinfo (list (car toklevel) nil nil)))
+ (if (and tokinfo (null toklevel))
+ (error "Token %S has indent rule but has no parsing info" tok))
+ (when toklevel
+ (let ((default-offset
+ ;; The default indentation after a keyword/operator
+ ;; is 0 for infix and t for prefix.
+ ;; Using the BNF syntax, we could come up with
+ ;; better defaults, but we only have the
+ ;; precedence levels here.
+ (if (or tokinfo (null (cadr toklevel)))
+ (smie-indent-offset t) 0)))
+ ;; For indentation after "(let", we end up accumulating the
+ ;; offset of "(" and the offset of "let", so we use `min'
+ ;; to try and get it right either way.
+ (min
(+ (smie-indent-calculate :bolp)
- (or (caddr tokinfo) (cadr tokinfo) (smie-indent-offset t)))
+ (or (caddr tokinfo) (cadr tokinfo) default-offset))
(+ (current-column)
- (or (cadr tokinfo) (smie-indent-offset t)))))))
- ;; Main loop (FIXME: whatever that means!?).
+ (or (cadr tokinfo) default-offset)))))))
+ ;; Indentation of sequences of simple expressions without
+ ;; intervening keywords or operators. E.g. "a b c" or "g (balbla) f".
+ ;; Can be a list of expressions or a function call.
+ ;; If it's a function call, the first element is special (it's the
+ ;; function). We distinguish function calls from mere lists of
+ ;; expressions based on whether the preceding token is listed in
+ ;; the `list-intro' entry of smie-indent-rules.
+ ;;
+ ;; TODO: to indent Lisp code, we should add a way to specify
+ ;; particular indentation for particular args depending on the
+ ;; function (which would require always skipping back until the
+ ;; function).
+ ;; TODO: to indent C code, such as "if (...) {...}" we might need
+ ;; to add similar indentation hooks for particular positions, but
+ ;; based on the preceding token rather than based on the first exp.
(save-excursion
(let ((positions nil)
- (begline nil)
arg)
(while (and (null (car (smie-backward-sexp)))
(push (point) positions)
- (not (setq begline (smie-bolp)))))
+ (not (smie-bolp))))
(save-excursion
;; Figure out if the atom we just skipped is an argument rather
;; than a function.
(member (funcall smie-backward-token-function)
(cdr (assoc 'list-intro smie-indent-rules))))))
(cond
- ((and arg positions)
+ ((null positions)
+ ;; We're the first expression of the list. In that case, the
+ ;; indentation should be (have been) determined by its context.
+ nil)
+ (arg
+ ;; There's a previous element, and it's not special (it's not
+ ;; the function), so let's just align with that one.
(goto-char (car positions))
(current-column))
- ((and (null begline) (cdr positions))
+ ((cdr positions)
;; We skipped some args plus the function and bumped into something.
;; Align with the first arg.
(goto-char (cadr positions))
(current-column))
- ((and (null begline) positions)
+ (positions
;; We're the first arg.
- ;; FIXME: it might not be a funcall, in which case we might be the
- ;; second element.
(goto-char (car positions))
(+ (smie-indent-offset 'args)
;; We used to use (smie-indent-calculate :bolp), but that
;; doesn't seem right since it might then indent args less than
;; the function itself.
- (current-column)))
- ((and (null arg) (null positions))
- ;; We're the function itself. Not sure what to do here yet.
- ;; FIXME: This should not be possible, because it should mean
- ;; we're right after some special token.
- (if virtual (current-column)
- (save-excursion
- (let* ((pos (point))
- (tok (funcall smie-backward-token-function))
- (toklevels (cdr (assoc tok smie-op-levels))))
- (cond
- ((numberp (car toklevels))
- ;; We're right after an infix token. Let's skip over the
- ;; lefthand side.
- (goto-char pos)
- (let (res)
- (while (progn (setq res (smie-backward-sexp 'halfsexp))
- (and (not (smie-bolp))
- (equal (car res) (car toklevels)))))
- ;; We should be right after a token of equal or
- ;; higher precedence.
- (cond
- ((and (consp res) (memq (car res) '(t nil)))
- ;; The token of higher-precedence is like an open-paren.
- ;; Sample case for t: foo { bar, \n[TAB] baz }.
- ;; Sample case for nil: match ... with \n[TAB] | toto ...
- ;; (goto-char (cadr res))
- (smie-indent-calculate :hanging))
- ((and (consp res) (<= (car res) (car toklevels)))
- ;; We stopped at a token of equal or higher precedence
- ;; because we found a place with which to align.
- (current-column))
- )))
- ;; For other cases.... hmm... we'll see when we get there.
- )))))
- ((null positions)
- (funcall smie-backward-token-function)
- (+ (smie-indent-offset 'args) (smie-indent-calculate :bolp)))
- ((car (smie-backward-sexp))
- ;; No arg stands on its own line, but the function does:
- (if (cdr positions)
- (progn
- (goto-char (cadr positions))
- (current-column))
- (goto-char (car positions))
- (+ (current-column) (smie-indent-offset 'args))))
- (t
- ;; We've skipped to a previous arg on its own line: align.
- (goto-char (car positions))
- (current-column)))))))
+ (current-column))))))))
(defun smie-indent-line ()
"Indent current line using the SMIE indentation engine."
--- /dev/null
+%% -*- 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).
+%% Residualize the substitution when applied to an uninstantiated variable.
+%% subst(X, V, _, Y, app(lambda(X,_,Y),V)) :- var(Y).
+%% Rather than residualize and leave us with unifications that fail, let's
+%% rather assume that Y will not refer to X.
+subst(X, V, _, Y, Y) :- var(Y).
+subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)) :-
+ subst(X, V, FV, Ti, To),
+ (X = Y ->
+ %% If X is equal to Y, X is shadowed, so no subst can take place.
+ Y1 = Y, Bo = Bi;
+ (member((Y, _), FV) ->
+ %% If Y appears in FV, it can appear in V, so we need to
+ %% rename it to avoid name capture.
+ new_atom(Y, Y1),
+ subst(Y, Y1, [], Bi, Bi1);
+ Y1 = Y, Bi1 = Bi),
+ %% Perform substitution on the body.
+ subst(X, V, FV, Bi1, Bo)).
+subst(X, V, FV, pi(Y, Ti, Bi), pi(Y1, To, Bo)) :-
+ subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)).
+subst(X, V, FV, forall(Y, Ti, Bi), forall(Y1, To, Bo)) :-
+ subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)).
+subst(X, V, FV, app(E1i, E2i), app(E1o, E2o)) :-
+ subst(X, V, FV, E1i, E1o), subst(X, V, FV, E2i, E2o).
+
+%% apply(+F, +Arg, +Env, -E)
+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.
+normalize(X, _, X) :- integer(X); var(X); atom(X).
+%% normalize(X, Env, E) :- atom(X), member((X, E), Env).
+normalize(lambda(X, T, B), Env, lambda(X, Tn, Bn)) :-
+ normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn).
+normalize(pi(X, T, B), Env, pi(X, Tn, Bn)) :-
+ normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn).
+normalize(forall(X, T, B), Env, forall(X, Tn, Bn)) :-
+ normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn).
+normalize(app(E1, E2), Env, En) :-
+ normalize(E1, Env, E1n),
+ normalize(E2, Env, E2n),
+ (apply(E1n, E2n, Env, E) ->
+ normalize(E, Env, En);
+ En = app(E1n, E2n)).
+
+%% 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.
+ true).
+infer(lambda(X,T,B), Env, pi(Y,T,TB)) :-
+ infer(B, [(X,T)|Env], TBx),
+ (var(Y) ->
+ Y = X, TB = TBx;
+ subst(X, Y, Env, TBx, TB)).
+infer(app(E1, E2), Env, Tn) :-
+ infer(E1, Env, T1),
+ (T1 = pi(X,T2,B); T1 = forall(X,T2,B)),
+ infer(E2, Env, T2),
+ subst(X, E2, Env, B, T),
+ normalize(T, Env, Tn).
+infer(pi(X,T1,T2), Env, type) :-
+ infer(T1, Env, type),
+ infer(T2, [(X,T1)|Env], type).
+infer(forall(X,T1,T2), Env, type) :-
+ infer(T1, Env, type),
+ infer(T2, [(X,T1)|Env], type).
+
+%% 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 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).
+
+%% elab_type(+Ee, +Te, +Env, -Eg, -Tg)
+%% Ajoute les arguments implicites de E:T.
+generalize(Ee, Te, Env, Eg, Tg) :-
+ freevars(Te, Env, Vs),
+ append(Vs, Env, EnvX),
+ %% Essaie d'instancier les types des paramètres que `generalize' vient
+ %% d'ajouter.
+ infer(Te, EnvX, type),
+ closetype(Ee, Te, Vs, Eg, Tg).
+
+%% 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 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.
+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(lambda(X, T, B), Env, lambda(X, Te, Be)) :-
+ elaborate(T, Env, Te),
+ elaborate(B, [(X,Te)|Env], Be).
+elaborate(pi(X, T, B), Env, pi(X, Te, Be)) :-
+ elaborate(T, Env, Te),
+ elaborate(B, [(X,Te)|Env], Be).
+elaborate(app(E1, E2), Env, app(E1e, E2e)) :-
+ elaborate(E1, Env, E1e),
+ elaborate(E2, Env, E2e).
+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).
+%% Expansion du sucre syntaxique.
+elaborate((T1 -> T2), Env, Ee) :-
+ new_atom(X), elaborate(pi(X, T1, T2), Env, Ee).
+elaborate(app(E1, E2, E3, E4), Env, Ee) :-
+ elaborate(app(app(E1,E2,E3),E4), Env, Ee).
+elaborate(app(E1, E2, E3), Env, Ee) :- elaborate(app(app(E1,E2),E3), Env, Ee).
+elaborate(lambda(X, B), Env, Ee) :- elaborate(lambda(X, _, B), Env, Ee).
+elaborate(let(X, E1, E2), Env, Ee) :- elaborate(let(X, _, E1, E2), Env, Ee).
+elaborate(fix(F,B,E), Env, Ee) :- elaborate(fix(F,_,B,E), Env, Ee).
+elaborate(fix(F,T,B,E), Env, Ee) :-
+ elaborate(let(F,T,app(fix,lambda(F,T,B)),E), Env, Ee).
+
+%% elab_bindings(+TS, +Env, -TS).
+%% Applique `elaborate' sur l'environnment de type TS.
+elab_tenv([], _, []).
+elab_tenv([(X,T)|TS], Env, [(X, Tg)|TSe]) :-
+ elaborate(T, Env, Te),
+ infer(Te, Env, type),
+ generalize(_, Te, Env, _, Tg),
+ elab_tenv(TS, [(X, Tg)|Env], TSe).
+
+
+%% elaborate(+E1, -E2)
+%% Comme le `elaborate' ci-dessus, mais avec un environnement par défaut.
+elaborate(SRC, E) :-
+ elab_tenv([(int, type),
+ (fix, ((t -> t) -> t)),
+ %% list: type → int → type
+ (list, (type -> int -> type)),
+ %% plus: int → int → int
+ (plus, (int -> int -> int)),
+ %% minus: int → int → int
+ (minus, (int -> int -> int)),
+ %% nil: list t 0
+ (nil, app(app(list,t),0)),
+ %% cons: t -> list t n → list t (n + 1)
+ (cons, (t -> app(app(list,t),n) ->
+ app(app(list,t), app(app(plus,n),1)))) %fixindent
+ ],
+ [(type,type)],
+ Env),
+ elaborate(SRC, Env, E).
projects / emacs.git / commitdiff